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



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



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



end