(* acq off *)
theory Demo
imports Main Efficient_Nat
begin

section{*Ackermann's function*}

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

lemma "n < ack m n"
apply(induct m n rule: ack.induct)
apply auto
done


section{*Definition of Huffman's algorithm*}

datatype 'a tree = Leaf nat 'a | Node nat "('a tree)" "('a tree)"

primrec "value" where
"value (Leaf n _) = n" |
"value (Node n _ _) = n"

definition "merge t1 t2 = Node (value t1 + value t2) t1 t2"

fun ins where
"ins u (t#ts) = (if value u \<le> value t then u # t # ts else t # ins u ts)" |
"ins u [] = [u]"

lemma size_ins[termination_simp]:  "size(ins u ts) = size ts + 1"
apply (induct ts)
apply simp_all
done

fun mkTree where
"mkTree(t1#t2#ts) = mkTree(ins (merge t1 t2) ts)" |
"mkTree[t] = t"

normal_form
  "mkTree[Leaf 3 a, Leaf 6 b, Leaf 12 c, Leaf 24 d]"


section{*Indirectly recursive data types*}

datatype t = C "t list"

fun mirror where
"mirror(C ts) = C (rev (map mirror ts))"

lemma "mirror(mirror t) = t"
apply(induct t rule: mirror.induct)
apply(simp)
sorry


section{*Inductive definitions*}

datatype alpha = A | B

inductive_set S :: "alpha list set" where
S1: "[] \<in> S" |
S2: "w \<in> S \<Longrightarrow> [A] @ w @ [B] \<in> S" |
S3: "v \<in> S \<Longrightarrow> w \<in> S \<Longrightarrow> v @ w \<in> S"


subsection {* Introduction proof *}

lemma "[A, B] \<in> S"
apply(subgoal_tac "[A] @ [] @ [B] \<in> S")
 apply simp
apply(rule S2)
apply(rule S1)
done

lemma "[A, B] \<in> S"
proof -
  have "[] \<in> S" by (rule S1)
  then have "[A] @ [] @ [B] \<in> S" by (rule S2)
  then show ?thesis by simp
qed

lemma "[A, B] \<in> S"
sorry

subsection {* Induction proof *}

lemma "w \<in> S \<Longrightarrow> \<not> (EX v. w = B # v)"
proof(induct set:S)
  case S1
  then show ?case by simp
next
  case S2
  then show ?case by simp
next
  case S3
  then show ?case sorry
qed


section{* Classes *}

class order = type +
fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<preceq>" 50)
assumes refl: "x \<preceq> x"
    and trans: "x \<preceq> y \<Longrightarrow> y \<preceq> z \<Longrightarrow> x \<preceq> z"
    and antisym: "x \<preceq> y \<Longrightarrow> y \<preceq> x \<Longrightarrow> x = y"

thm refl

context order
begin

definition less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<prec>" 50)
where "x \<prec> y \<longleftrightarrow> x \<preceq> y \<and> \<not> y \<preceq> x"

lemma irrefl: "\<not> x \<prec> x"
by (auto simp:less_def)

lemma less_trans: "x \<prec> y \<Longrightarrow> y \<prec> z \<Longrightarrow> x \<prec> z"
by (auto simp:less_def intro: trans)

lemma asym: "x \<prec> y \<Longrightarrow> y \<prec> x \<Longrightarrow> P"
by (auto simp:less_def)

end


subsection {* Subclass *}

class linorder = order +
assumes linear: "x \<preceq> y \<or> y \<preceq> x"
begin

lemma "x \<prec> y \<or> x=y \<or> x \<prec> x"
sorry

end


subsection {* Class instantiation *}

instantiation * :: (order, order) order
begin

inductive less_eq_prod :: "'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" where
less_eq_fst: "x \<prec> v \<Longrightarrow> (x, y) \<preceq> (v, w)" |
less_eq_snd: "x = v \<Longrightarrow> y \<preceq> w \<Longrightarrow> (x, y) \<preceq> (v, w)"

instance
proof
  fix p :: "'a \<times> 'b"
  show "p \<preceq> p" by (cases p) (auto intro!: less_eq_snd refl)
next
  fix p q r :: "'a \<times> 'b"
  assume "p \<preceq> r" and "r \<preceq> q"
  then show "p \<preceq> q"
    by (induct p r rule: less_eq_prod.induct)
      (auto elim!: less_eq_prod.cases intro: less_eq_fst less_eq_snd trans less_trans)
next
  fix p q :: "'a \<times> 'b"
  assume "p \<preceq> q" and "q \<preceq> p"
  then show "p = q"
    by (induct p q rule: less_eq_prod.induct)
      (auto elim!: less_eq_prod.cases elim: asym intro: antisym simp: irrefl)
qed

end

term "(a,b) \<preceq> (c,d)"


section{* Locales *}


locale Order =
fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubseteq>" 50)
assumes refl: "x \<sqsubseteq> x"
    and trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
    and antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"

thm refl
thm Order.refl
thm Order_def


locale LinOrder = Order +
assumes linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"


interpretation Order_imp: Order["op \<longrightarrow>"]
proof
  fix P show "P \<longrightarrow> P" by blast
next
  fix P Q R show "P \<longrightarrow> Q \<Longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<longrightarrow> R" by blast
next
  fix P Q show "P \<longrightarrow> Q \<Longrightarrow> Q \<longrightarrow> P \<Longrightarrow> P = Q" by blast
qed

interpretation Order_dvd: Order["op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"]
proof
  fix n::nat show "n dvd n" by simp
next
  fix i j k::nat show "i dvd j \<Longrightarrow> j dvd k \<Longrightarrow> i dvd k" by(rule dvd.order_trans)
next
  fix m n::nat show "m dvd n \<Longrightarrow> n dvd m \<Longrightarrow> m = n" by(metis dvd.less_le_trans)
qed


locale Mono =
  Order  le1 (infix "\<sqsubseteq>\<^isub>1" 50)  +
  Order  le2 (infix "\<sqsubseteq>\<^isub>2" 50)  +
fixes f :: "'a \<Rightarrow> 'b"
assumes mono: "x \<sqsubseteq>\<^isub>1 y \<Longrightarrow> f(x) \<sqsubseteq>\<^isub>2 f(y)"

lemma (in Mono) wow: "x \<sqsubseteq>\<^isub>1 y \<Longrightarrow> y \<sqsubseteq>\<^isub>1 z \<Longrightarrow> f(x) \<sqsubseteq>\<^isub>2 f(z)"
by (metis le1.trans mono)

thm Mono.wow
context Mono begin thm wow end

interpretation Mono["op dvd" "op \<longrightarrow>" "\<lambda>n::nat. 2 dvd n"]
proof
  fix x y :: nat show "x dvd y \<Longrightarrow> 2 dvd x \<longrightarrow> 2 dvd y"
    by (metis Order_dvd.trans Suc_plus1 add_eq_if comp_arith(66))
qed

thm wow


section{* Structured Proofs: Induction and Chaining *}

theorem
  assumes f_ax: "\<And>n. f (f n) < f (Suc n)"
  shows "f n = n"
proof (rule order_antisym)
  {
    fix n show "n \<le> f n"
    proof (induct k \<equiv> "f n" arbitrary: n rule: less_induct)
      case (less k n)
      then have hyp: "\<And>m. f m < f n \<Longrightarrow> m \<le> f m" by (simp only:)
      show "n \<le> f n"
      proof (cases n)
         case (Suc m)
         from f_ax have "f (f m) < f n" by (simp only: Suc)
         with hyp have "f m \<le> f (f m)" .
         also from f_ax have "\<dots> < f n" by (simp only: Suc)
         finally have "f m < f n" .
         with hyp have "m \<le> f m" .
         also note `\<dots> < f n`
         finally have "m < f n" .
         then have "n \<le> f n" by (simp only: Suc)
         then show ?thesis .
      next
        case 0
        then show ?thesis by simp
      qed
    qed
  } note ge = this

  {
    fix m n :: nat
    assume "m \<le> n"
    then have "f m \<le> f n"
    proof (induct n)
      case 0
      then have "m = 0" by simp
      then show ?case by simp
    next
      case (Suc n)
      from Suc.prems show "f m \<le> f (Suc n)"
      proof (rule le_SucE)
        assume "m \<le> n"
        with Suc.hyps have "f m \<le> f n" .
        also from ge f_ax have "\<dots> < f (Suc n)"  by (rule le_less_trans)
        finally show ?thesis by simp
      next
        assume "m = Suc n"
        then show ?thesis by simp
      qed
    qed
  } note mono = this

  show "f n \<le> n"
  proof -
    have "\<not> n < f n"
    proof
      assume "n < f n"
      then have "Suc n \<le> f n" by simp
      then have "f (Suc n) \<le> f (f n)" by (rule mono)
      also have "\<dots> < f (Suc n)" by (rule f_ax)
      finally have "\<dots> < \<dots>" . then show False ..
    qed
    then show ?thesis by simp
  qed
qed


section{* Proof Automation *}

subsection{* blast *}

lemma UN_Un_distrib:
  "(\<Union>i\<in>K. M i \<union> N i) = (\<Union>i\<in>K. M i) \<union> (\<Union>i\<in>K. N i)"
by blast

subsection{* arith *}

lemma "\<forall> (k::nat) > 7. \<exists> i j. k = 3*i + 5*j"
by arith

lemma "\<forall> (k::nat) > 119. \<exists> i j. k = 9*i + 16*j"
by arith

text{* \<rightarrow> Frobenius number *}


text {* A challenge by John Harrison *}

lemma
  "((p\<^isub>1::int)^2 + q\<^isub>1^2 + r\<^isub>1^2 + s\<^isub>1^2 + t\<^isub>1^2 + u\<^isub>1^2 + v\<^isub>1^2 + w\<^isub>1^2) * 
   (p\<^isub>2^2 + q\<^isub>2^2 + r\<^isub>2^2 + s\<^isub>2^2 + t\<^isub>2^2 + u\<^isub>2^2 + v\<^isub>2^2 + w\<^isub>2^2) 
    = (p\<^isub>1*p\<^isub>2 - q\<^isub>1*q\<^isub>2 - r\<^isub>1*r\<^isub>2 - s\<^isub>1*s\<^isub>2 - t\<^isub>1*t\<^isub>2 - u\<^isub>1*u\<^isub>2 - v\<^isub>1*v\<^isub>2 - w\<^isub>1*w\<^isub>2)^2 + 
      (p\<^isub>1*q\<^isub>2 + q\<^isub>1*p\<^isub>2 + r\<^isub>1*s\<^isub>2 - s\<^isub>1*r\<^isub>2 + t\<^isub>1*u\<^isub>2 - u\<^isub>1*t\<^isub>2 - v\<^isub>1*w\<^isub>2 + w\<^isub>1*v\<^isub>2)^2 +
      (p\<^isub>1*r\<^isub>2 - q\<^isub>1*s\<^isub>2 + r\<^isub>1*p\<^isub>2 + s\<^isub>1*q\<^isub>2 + t\<^isub>1*v\<^isub>2 + u\<^isub>1*w\<^isub>2 - v\<^isub>1*t\<^isub>2 - w\<^isub>1*u\<^isub>2)^2 +
      (p\<^isub>1*s\<^isub>2 + q\<^isub>1*r\<^isub>2 - r\<^isub>1*q\<^isub>2 + s\<^isub>1*p\<^isub>2 + t\<^isub>1*w\<^isub>2 - u\<^isub>1*v\<^isub>2 + v\<^isub>1*u\<^isub>2 - w\<^isub>1*t\<^isub>2)^2 +
      (p\<^isub>1*t\<^isub>2 - q\<^isub>1*u\<^isub>2 - r\<^isub>1*v\<^isub>2 - s\<^isub>1*w\<^isub>2 + t\<^isub>1*p\<^isub>2 + u\<^isub>1*q\<^isub>2 + v\<^isub>1*r\<^isub>2 + w\<^isub>1*s\<^isub>2)^2 +
      (p\<^isub>1*u\<^isub>2 + q\<^isub>1*t\<^isub>2 - r\<^isub>1*w\<^isub>2 + s\<^isub>1*v\<^isub>2 - t\<^isub>1*q\<^isub>2 + u\<^isub>1*p\<^isub>2 - v\<^isub>1*s\<^isub>2 + w\<^isub>1*r\<^isub>2)^2 +
      (p\<^isub>1*v\<^isub>2 + q\<^isub>1*w\<^isub>2 + r\<^isub>1*t\<^isub>2 - s\<^isub>1*u\<^isub>2 - t\<^isub>1*r\<^isub>2 + u\<^isub>1*s\<^isub>2 + v\<^isub>1*p\<^isub>2 - w\<^isub>1*q\<^isub>2)^2 +
      (p\<^isub>1*w\<^isub>2 - q\<^isub>1*v\<^isub>2 + r\<^isub>1*u\<^isub>2 + s\<^isub>1*t\<^isub>2 - t\<^isub>1*s\<^isub>2 - u\<^isub>1*r\<^isub>2 + v\<^isub>1*q\<^isub>2 + w\<^isub>1*p\<^isub>2)^2"
by algebra

lemma "(x::int)^3  - x^2  - 5*x - 3 = 0 \<longleftrightarrow> (x = 3 \<or> x = -1)"
by algebra


section{* Quickcheck *}

lemma "(n::nat)+m < n*m"
sorry

lemma "mirror t = t"
oops

lemma "map g (map f xs) = map (f o g) xs"
oops

lemma "m*n < ack m n"
oops


definition prime :: "nat \<Rightarrow> bool" where
"prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m<p. p mod m = 0 \<longrightarrow> m = 1))"

lemma "prime(n*n + n + 41)"
sorry

value "\<forall>n<40. prime(n*n + n + 41)"

section{* Code generation *}

export_code mkTree in Haskell file "Huff"


end