theory Demo11 imports Main begin

(* Simple Higher-Order Recursion *)
datatype 'a tree = 
  Leaf 'a 
  | Branch "'a tree list"

lemma lem:"x \<in> set l \<Longrightarrow> size x < Suc (list_size size l)"
by (induct l, auto)

function treemap :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
where
  "treemap fn (Leaf n) = (Leaf (fn n))"
| "treemap fn (Branch l) = (Branch (map (treemap fn) l))"
by pat_completeness auto
termination by (lexicographic_order simp:lem)

declare lem[simp]

fun tinc :: "nat tree \<Rightarrow> nat tree"
where
  "tinc (Leaf n) = Leaf (Suc n)"
| "tinc (Branch l) = Branch (map tinc l)"


(* Pattern matching on records *)
record point =
  Xcoord :: int
  Ycoord :: int

function swp :: "point \<Rightarrow> point"
where
  "swp \<lparr> Xcoord = x, Ycoord = y \<rparr> = \<lparr> Xcoord = y, Ycoord = x \<rparr>"
proof -
  fix P x
  assume "\<And>xa y. x = \<lparr>Xcoord = xa, Ycoord = y\<rparr> \<Longrightarrow> P"
  thus "P"
    by (cases x)
qed auto
termination by lexicographic_order

-- "another (simple) function that cannot be defined with fun"
function (sequential) extend :: "'a => nat => 'a list => 'a list" where
  "extend a n xs = (if (length xs < n) then extend a n (a#xs) else xs)"
  by pat_completeness auto

fun mesr where
  "mesr (a,n,xs) = n - length xs"

termination extend
  apply(relation "measure mesr")
   by(auto)

-- "some single-step proofs to show why/how tailored induction principle works"
lemma length_extend_ge_xs: "length (extend a n xs) \<ge> length xs"
  apply(induct a n xs rule: extend.induct)
  apply(subst extend.simps)
  apply(subst split_if)
  apply(rule conjI)
   apply(rule impI)
   apply(drule impI, erule (1) impE)
   apply(subst (asm) list.size)
   apply(drule add_leD1)
   apply(assumption)
  apply(rule impI)
  apply(rule le_refl)
  done

lemma length_extend_ge_n: "length (extend a n xs) \<ge> n"
  apply(induct a n xs rule: extend.induct)
  apply(subst extend.simps)
  apply(subst split_if)
  apply(rule conjI)
   apply(rule impI)
   apply(drule impI, erule (1) impE)
   apply assumption
  apply(rule impI)
  apply(rule leI)
  apply(assumption)
  done

lemma "length (extend a n xs) \<ge> max n (length xs)"
  apply(rule min_max.le_supI)
   apply(rule length_extend_ge_n)
  apply(rule length_extend_ge_xs)
  done
  
 
-- ---------------------------------------------------------------

-- "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 algebra_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"

definition
  g :: "nat \<Rightarrow> nat" where
  "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::nat) \<in> L"

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

ML "DSeq.pull (T.y)"

ML "Seq.pull (snd (the it))"
ML "Seq.pull (snd (the it))"
ML "Seq.pull (snd (the it))"
ML "Seq.pull (snd (the it))"
ML "Seq.pull (snd (the it))"

end