theory week11B_demo imports Main begin
  

-- ---------------------------------------------------------------
 
-- {* Isar, case distinction *}

declare length_tl[simp del]

(* isar style, just using "proof (cases xs)", not using case *)
lemma "length (tl xs) = length xs - 1"
proof(cases xs)
  assume "xs = []" thus ?thesis by simp
next
  fix y ys assume "xs = y#ys" thus ?thesis by simp
qed

(* isar style, using case *)
lemma "length (tl xs) = length xs - 1"
proof(cases xs)
  case Nil
  thus ?thesis by simp
next
  case (Cons y ys) from Cons show ?thesis by simp
qed


-- {* structural induction *}

(* apply style *)
lemma "2 * (\<Sum>i<n+1. i) = n*(n+1::nat)"
  apply(induct n, simp_all)
  done

(* isar style, not using case *)  
lemma "2 * (\<Sum>i<n+1. i) = n*(n+1::nat)" (is "?P n")
proof(induct n)
  show "?P 0" by simp
next
  fix n
  assume "?P n" thus "?P (Suc n)" by simp
qed

(* isar style, using case *)
lemma "2 * (\<Sum>i<n+1. i) = n*(n+1::nat)"
proof(induct n)
  case 0
  show ?case by simp
next
  case (Suc n)
  from Suc show ?case by simp
qed


lemma
  fixes n::nat
  shows "n < n*n + 1"
proof(induct n)
  case 0 show ?case by simp
next
  case (Suc n) thus ?case by simp
qed

-- {* induction with @{text"\<And>"} or @{text"\<Longrightarrow>"} *}

lemma
  assumes A: "(\<And>n. (\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
  shows "P (n::nat)"
proof(rule A)
  show "\<And>m. m < n \<Longrightarrow> P m"
  proof(induct n)
    case 0
    thus ?case by simp
  next
    case (Suc n)
    show ?case
    proof(cases)
      assume eq: "m = n"
      from A Suc have "P n" by blast
      with eq show "P m" by simp
    next
      assume neq: "m \<noteq> n"
      from Suc neq have "m < n" by arith
      thus "P m" by(rule Suc)
    qed
  qed
qed
  
  
-- ---------------------------------------------------------------

-- "calculational reasoning"

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

print_trans_rules

-- "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 "2*y + 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
    
print_trans_rules

-- "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)\<^sup>2 \<le> 2*(a\<^sup>2 + b\<^sup>2)"
proof -
       have "(a+b)\<^sup>2 \<le> (a+b)\<^sup>2 + (a-b)\<^sup>2"  by simp thm numeral_2_eq_2
  also have "(a+b)\<^sup>2 \<le> a\<^sup>2 + b\<^sup>2 + 2*a*b"  by (simp add: numeral_2_eq_2)
  also have "(a-b)\<^sup>2 = a\<^sup>2 + b\<^sup>2 - 2*a*b"  by (simp add:numeral_2_eq_2)
  finally show ?thesis by simp
qed

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

-- "code generation"



-- "code export"

datatype 'a queue = AQueue "'a list" "'a list"

definition empty :: "'a queue" where 
  "empty = AQueue [] [] "
  
primrec enqueue :: " 'a  \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where 
  "enqueue x (AQueue xs ys ) = AQueue (x # xs ) ys "

fun dequeue :: "'a queue \<Rightarrow> 'a option * 'a queue" where 
  "dequeue (AQueue [] []) = (None , AQueue [] []) "
| "dequeue (AQueue xs (y # ys )) = (Some y , AQueue xs ys ) "
| "dequeue (AQueue xs []) = 
(case rev xs of y # ys 
\<Rightarrow> (Some y , AQueue [] ys )) "

export_code empty dequeue enqueue in SML  module_name Example file "examples.ML" 
export_code empty dequeue enqueue in Haskell  module_name Example file "." 


-- "program refinement" 

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

export_code fib in SML  module_name Fib file "fib1.ML" 

definition fib_step :: "nat \<Rightarrow> nat * nat" where 
  "fib_step n = (fib (Suc n ), fib n )"

lemma [code]: 
"fib_step 0 = (Suc 0, 0) "
"fib_step (Suc n ) = (let (m , q ) = fib_step n in (m + q , m )) "
by (simp_all add : fib_step_def )

lemma [code]: 
"fib 0 = 0 "
"fib (Suc n ) = fst (fib_step n ) "
by (simp_all add : fib_step_def ) 



export_code fib in SML  module_name Fib file "fib.ML"


-- "inductive predicates"

inductive append :: "'a list \<Rightarrow>'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
    "append [] xs xs"
  | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"

code_pred append . 

thm append.equation


values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}"

thm append.equation

code_pred (modes: i => i => o => bool as "concat", 
o => o => i => bool as "slice",  
o => i => i => bool as prefix,
i => o => i => bool as suffix) append .


end