theory Demo11 imports Main begin

-- ---------------------------------------------------------------

-- "also/finally"

lemma right_inverse:
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>" 70)
  fixes inv :: "'a \<Rightarrow> 'a"    ("(_\<^sup>-)" [1000] 999)
  fixes one :: 'a    ("\<one>")

  assumes assoc: "\<And>x y z. (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
  assumes left_inv: "\<And>x. x\<^sup>- \<cdot> x = \<one>"
  assumes left_one: "\<And>x. \<one> \<cdot> x = x"

  shows "x \<cdot> x\<^sup>- = \<one>"
proof -
  have "x \<cdot> x\<^sup>- = \<one> \<cdot> (x \<cdot> x\<^sup>-)" by (simp only: left_one)
  also have "\<dots> = \<one> \<cdot> x \<cdot> x\<^sup>-" by (simp only: assoc)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> x\<^sup>- \<cdot> x \<cdot> x\<^sup>-" by (simp only: left_inv)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> (x\<^sup>- \<cdot> x) \<cdot> x\<^sup>-" by (simp only: assoc)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> \<one> \<cdot> x\<^sup>-" by (simp only: left_inv)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> (\<one> \<cdot> x\<^sup>-)" by (simp only: assoc)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> x\<^sup>-" by (simp only: left_one)
  also have "\<dots> = \<one>" by (simp only: left_inv)
  finally show ?thesis .
qed



-- "mixed operators"
lemma "1 < (5::nat)"
proof -
  have "1 < Suc 1" by simp
  also
  have "Suc 1 = 2" by simp
  also
  have "2 \<le> (5::nat)" by simp
  finally
  show ?thesis .
qed
  
-- "substitution"
lemma blah
proof -
  have "x + 2*y = (0::nat)" sorry
  also
  have "2*y = x" sorry
  also
  have "(0::nat) \<le> 2*c" sorry
  also
  have "c = d div 2" sorry
  also
  have "d = 2 * x" sorry  
  finally
  have "x + x \<le> 2 * x " by simp
oops
    
-- "antisymmetry"
lemma blub
proof -
  have "a < (b::nat)" sorry
  also
  have "b < a" sorry
  finally
  show blub .
qed


-- "notE as trans"

thm notE
declare notE [trans]

lemma blub
proof -
  have "\<not>P" sorry
  also
  have "P" sorry
  finally
  show blub .
qed


-- "monotonicity"

lemma "a+b \<le> 2*a + 2*(b::nat)" 
proof -
  have "a + b \<le> 2*a + b" by simp
  also
  have "b \<le> 2*b" by simp
  finally
  show "a+b \<le> 2*a + 2*b" by simp
qed

lemma "a+b \<le> 2*a + 2*(b::nat)" 
proof -
  have "a + b \<le> 2*a + b" by simp
  also
  have "b \<le> 2*b" by simp
  also
  have "\<And>x y. x \<le> y \<Longrightarrow> 2 * a + x \<le> 2 * a + y" by simp
  ultimately
  show "a+b \<le> 2*a + 2*(b::nat)" .
qed
  

declare ring_simps [simp] 
lemma "(a+b::int)\<twosuperior> \<le> 2*(a\<twosuperior> + b\<twosuperior>)"
proof -
       have "(a+b)\<twosuperior> \<le> (a+b)\<twosuperior> + (a-b)\<twosuperior>"  by simp
  also have "(a+b)\<twosuperior> \<le> a\<twosuperior> + b\<twosuperior> + 2*a*b"  by (simp add: numeral_2_eq_2)
  also have "(a-b)\<twosuperior> = a\<twosuperior> + b\<twosuperior> - 2*a*b"  by (simp add:numeral_2_eq_2)
  finally show ?thesis by simp
qed

-- ---------------------------------------------------------------

-- "code generation"


-- "generate structure S, put into current context"
code_module S 
contains
  test = "\<lambda>x. (1::nat) < x"

ML "S.test S.zero"
ML "S.test (S.Suc (S.Suc S.zero))"


-- "generate structure S, put into file test.ML"
code_module S file "test.ML"
contains
  test = "\<lambda>x. (1::nat) < x"


-- "generate one structure for each theory, put into dir test"
code_library S file "test"
contains
  test = "\<lambda>x. (1::nat) < x"


-- "value and quickcheck"

value "(999::nat) < 1000"

lemma "rev xs = xs"
  quickcheck
  oops


-- "customisation"

constdefs
  g :: "nat \<Rightarrow> nat"
  "g x \<equiv> THE y. y = x + 2"

(*
code_module T file "test2.ML" contains g = "g"
*)

lemma [code]: "g x = x+2" by (simp add: g_def)

code_module T file "test2.ML" contains g = "g"


-- "own code with {* .. *} antiquotation"
consts_code g ("_ + {* Suc 1 *}")
code_module T file "test2.ML" contains g = "g"   


-- "own type code"
datatype bla = some | other
types_code bla ("int") 
code_module T file "test2.ML" contains v = "x::bla" 

fun f :: "nat \<Rightarrow> nat" where
  "f 0 = 0" |
  "f (Suc n) = f n + 1"


-- "ignoring arguments, attaching aux definitions"
consts_code "f" ("f?") attach {* val f = 7; *}
code_module T file "test2.ML" 
  contains r = "f"


-- "code for inductive defs"
inductive_set L :: "(nat \<times> nat) set" where
  "(0, Suc n) \<in> L"
| "(n,m) \<in> L \<Longrightarrow> (Suc n, Suc m) \<in> L"

code_module T 
contains 
  x = "\<lambda>x y. (x, y) \<in> L"
  y = "(_, 5) \<in> L"

ML "T.x (T.nat 8) (T.nat 7)"

ML "DSeq.pull T.y"
ML "DSeq.pull (snd (the it))"
ML "DSeq.pull (snd (the it))"
ML "DSeq.pull (snd (the it))"
ML "DSeq.pull (snd (the it))"
ML "DSeq.pull (snd (the it))"

end