--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Examples/LarryInt.thy	Fri Dec 11 15:58:15 2009 +0100
@@ -0,0 +1,416 @@
+
+header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}
+
+theory LarryInt 
+imports Nat "../QuotMain"
+begin
+
+fun
+  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" 
+where
+  "intrel (x, y) (u, v) = (x + v = u + y)"
+
+quotient int = "nat \<times> nat" / intrel
+  by (auto simp add: equivp_def expand_fun_eq)
+
+instantiation int :: "{zero, one, plus, uminus, minus, times, ord}"
+begin
+
+quotient_def 
+  Zero_int_def: "0::int" as "(0::nat, 0::nat)"
+
+quotient_def
+  One_int_def: "1::int" as "(1::nat, 0::nat)"
+
+quotient_def
+  "(op +) :: int \<Rightarrow> int \<Rightarrow> int" 
+as 
+  "\<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"
+
+quotient_def
+  "uminus :: int \<Rightarrow> int" 
+as 
+  "\<lambda>(x, y). (y::nat, x::nat)"
+
+fun
+  mult_aux::"nat \<times> nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
+where
+  "mult_aux (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
+
+quotient_def
+  "(op *) :: int \<Rightarrow> int \<Rightarrow> int" 
+as 
+  "mult_aux"
+
+quotient_def 
+  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" 
+as 
+  "\<lambda>(x, y) (u, v). (x+v \<le> u+(y::nat))"
+
+definition
+  less_int_def: "z < (w::int) \<equiv> (z \<le> w & z \<noteq> w)"
+
+definition
+  diff_int_def:  "z - (w::int) \<equiv> z + (-w)"
+
+instance ..
+
+end
+
+subsection{*Construction of the Integers*}
+
+abbreviation
+  "uminus_aux \<equiv> \<lambda>(x, y). (y::nat, x::nat)"
+
+lemma zminus_zminus_aux:
+  "uminus_aux (uminus_aux z) = z"
+  by (cases z) (simp)
+
+lemma [quot_respect]:
+  shows "(intrel ===> intrel) uminus_aux uminus_aux"
+  by simp
+  
+lemma zminus_zminus: 
+  shows "- (- z) = (z::int)"
+apply(lifting zminus_zminus_aux)
+apply(injection)
+apply(rule quot_respect)
+apply(rule quot_respect)
+done
+(* PROBLEM *)
+
+lemma zminus_0_aux:
+  shows "uminus_aux (0, 0) = (0, 0::nat)"
+by simp
+
+lemma zminus_0: "- 0 = (0::int)"
+apply(lifting zminus_0_aux)
+apply(injection)
+apply(rule quot_respect)
+done
+(* PROBLEM *)
+
+subsection{*Integer Addition*}
+
+definition
+  "add_aux \<equiv> \<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"
+
+lemma zminus_zadd_distrib_aux:
+  shows "uminus_aux (add_aux z w) = add_aux (uminus_aux z) (uminus_aux w)"
+by (cases z, cases w)
+   (auto simp add: add_aux_def)
+
+lemma [quot_respect]:
+  shows "(intrel ===> intrel ===> intrel) 
+            (\<lambda>(x, y) (u, v). (x + u, y + (v::nat)))  (\<lambda>(x, y) (u, v). (x + u, y + (v::nat)))"
+by simp
+
+lemma zminus_zadd_distrib: 
+  shows "- (z + w) = (- z) + (- w::int)"
+apply(lifting zminus_zadd_distrib_aux[simplified add_aux_def])
+apply(injection)
+apply(rule quot_respect)+
+done
+(* PROBLEM *)
+
+lemma zadd_commute_aux:
+  shows "add_aux z w = add_aux w z"
+by (cases z, cases w)
+   (simp add: add_aux_def)
+
+lemma zadd_commute: 
+  shows "(z::int) + w = w + z"
+apply(lifting zadd_commute_aux[simplified add_aux_def])
+apply(injection)
+apply(rule quot_respect)+
+done
+(* PROBLEM *)
+
+lemma zadd_assoc_aux:
+  shows "add_aux (add_aux z1 z2) z3 = add_aux z1 (add_aux z2 z3)"
+by (cases z1, cases z2, cases z3) (simp add: add_aux_def)
+
+lemma zadd_assoc: "((z1::int) + z2) + z3 = z1 + (z2 + z3)"
+apply(lifting zadd_assoc_aux[simplified add_aux_def])
+apply(injection)
+apply(rule quot_respect)+
+done
+(* PROBLEM *)
+
+lemma zadd_0_aux:
+  fixes z::"nat \<times> nat"
+  shows "add_aux (0, 0) z = z"
+by (simp add: add_aux_def)
+
+
+(*also for the instance declaration int :: plus_ac0*)
+lemma zadd_0: "(0::int) + z = z"
+apply(lifting zadd_0_aux[simplified add_aux_def])
+apply(injection)
+apply(rule quot_respect)+
+done
+
+lemma zadd_zminus_inverse_aux:
+  shows "intrel (add_aux (uminus_aux z) z) (0, 0)"
+by (cases z) (simp add: add_aux_def)
+
+lemma zadd_zminus_inverse2: "(- z) + z = (0::int)"
+apply(lifting zadd_zminus_inverse_aux[simplified add_aux_def])
+apply(injection)
+apply(rule quot_respect)+
+done
+
+subsection{*Integer Multiplication*}
+
+lemma zmult_zminus_aux:
+  shows "mult_aux (uminus_aux z) w = uminus_aux (mult_aux z w)"
+apply(cases z, cases w)
+apply(simp)
+done
+
+lemma mult_aux_fst:
+  assumes a: "intrel x z"
+  shows "intrel (mult_aux x y) (mult_aux z y)"
+using a
+apply(cases x, cases y, cases z)
+apply(auto simp add: mult_aux.simps intrel.simps)
+apply(rename_tac u v w x y z)
+apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
+apply(simp add: mult_ac)
+apply(simp add: add_mult_distrib [symmetric])
+done
+
+lemma mult_aux_snd:
+  assumes a: "intrel x z"
+  shows "intrel (mult_aux y x) (mult_aux y z)"
+using a
+apply(cases x, cases y, cases z)
+apply(auto simp add: mult_aux.simps intrel.simps)
+apply(rename_tac u v w x y z)
+apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
+apply(simp add: mult_ac)
+apply(simp add: add_mult_distrib [symmetric])
+done
+
+lemma [quot_respect]:
+  shows "(intrel ===> intrel ===> intrel) mult_aux mult_aux"
+apply(simp only: fun_rel.simps)
+apply(rule allI | rule impI)+
+apply(rule equivp_transp[OF int_equivp])
+apply(rule mult_aux_fst)
+apply(assumption)
+apply(rule mult_aux_snd)
+apply(assumption)
+done
+
+lemma zmult_zminus: "(- z) * w = - (z * (w::int))"
+apply(lifting zmult_zminus_aux)
+apply(injection)
+apply(rule quot_respect)
+apply(rule quot_respect)
+done
+
+lemma zmult_commute_aux: 
+  shows "mult_aux z w = mult_aux w z"
+apply(cases z, cases w)
+apply(simp add: add_ac mult_ac)
+done
+
+lemma zmult_commute: "(z::int) * w = w * z"
+by (lifting zmult_commute_aux)
+
+lemma zmult_assoc_aux:
+  shows "mult_aux (mult_aux z1 z2) z3 = mult_aux z1 (mult_aux z2 z3)"
+apply(cases z1, cases z2, cases z3)
+apply(simp add: add_mult_distrib2 mult_ac)
+done
+
+lemma zmult_assoc: "((z1::int) * z2) * z3 = z1 * (z2 * z3)"
+by (lifting zmult_assoc_aux)
+
+lemma zadd_mult_distrib_aux:
+  shows "mult_aux (add_aux z1 z2) w = add_aux (mult_aux z1 w) (mult_aux z2 w)"
+apply(cases z1, cases z2, cases w)
+apply(simp add: add_mult_distrib2 mult_ac add_aux_def)
+done
+
+lemma zadd_zmult_distrib: "((z1::int) + z2) * w = (z1 * w) + (z2 * w)"
+apply(lifting zadd_mult_distrib_aux[simplified add_aux_def])
+apply(injection)
+apply(rule quot_respect)+
+done
+
+lemma zadd_zmult_distrib2: "(w::int) * (z1 + z2) = (w * z1) + (w * z2)"
+by (simp add: zmult_commute [of w] zadd_zmult_distrib)
+
+lemma zdiff_zmult_distrib: "((z1::int) - z2) * w = (z1 * w) - (z2 * w)"
+by (simp add: diff_int_def zadd_zmult_distrib zmult_zminus)
+
+lemma zdiff_zmult_distrib2: "(w::int) * (z1 - z2) = (w * z1) - (w * z2)"
+by (simp add: zmult_commute [of w] zdiff_zmult_distrib)
+
+lemmas int_distrib =
+  zadd_zmult_distrib zadd_zmult_distrib2
+  zdiff_zmult_distrib zdiff_zmult_distrib2
+
+lemma zmult_1_aux:
+  shows "mult_aux (1, 0) z = z"
+apply(cases z)
+apply(auto)
+done
+
+lemma zmult_1: "(1::int) * z = z"
+apply(lifting zmult_1_aux)
+done
+
+lemma zmult_1_right: "z * (1::int) = z"
+by (rule trans [OF zmult_commute zmult_1])
+
+lemma zero_not_one:
+  shows "(0, 0) \<noteq> (1::nat, 0::nat)"
+by simp
+
+text{*The Integers Form A Ring*}
+instance int :: comm_ring_1
+proof
+  fix i j k :: int
+  show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc)
+  show "i + j = j + i" by (simp add: zadd_commute)
+  show "0 + i = i" by (rule zadd_0)
+  show "- i + i = 0" by (rule zadd_zminus_inverse2)
+  show "i - j = i + (-j)" by (simp add: diff_int_def)
+  show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)
+  show "i * j = j * i" by (rule zmult_commute)
+  show "1 * i = i" by (rule zmult_1) 
+  show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
+  show "0 \<noteq> (1::int)" 
+    by (lifting zero_not_one) (auto) (* PROBLEM? regularize failed *)
+qed
+
+
+subsection{*The @{text "\<le>"} Ordering*}
+
+abbreviation
+  "le_aux \<equiv> \<lambda>(x, y) (u, v). (x+v \<le> u+(y::nat))"
+
+lemma zle_refl_aux:
+  "le_aux w w"
+apply(cases w)
+apply(simp)
+done
+
+lemma [quot_respect]:
+  shows "(intrel ===> intrel ===> op =) le_aux le_aux"
+by auto
+
+lemma zle_refl: "w \<le> (w::int)"
+apply(lifting zle_refl_aux)
+apply(injection)
+apply(rule quot_respect)
+done
+(* PROBLEM *)
+
+lemma zle_trans_aux:
+  shows "\<lbrakk>le_aux i j; le_aux j k\<rbrakk> \<Longrightarrow> le_aux i k"
+apply(cases i, cases j, cases k)
+apply(auto)
+done
+
+lemma zle_trans: "\<lbrakk>i \<le> j; j \<le> k\<rbrakk> \<Longrightarrow> i \<le> (k::int)"
+apply(lifting zle_trans_aux)
+apply(injection)
+apply(rule quot_respect)+
+done
+(* PROBLEM *)
+
+lemma zle_anti_sym_aux:
+  shows "\<lbrakk>le_aux z w; le_aux w z\<rbrakk> \<Longrightarrow> intrel z w"
+apply(cases z, cases w)
+apply(auto)
+done
+
+lemma zle_anti_sym: "\<lbrakk>z \<le> w; w \<le> z\<rbrakk> \<Longrightarrow> z = (w::int)"
+apply(lifting zle_anti_sym_aux)
+apply(injection)
+apply(rule quot_respect)+
+done
+(* PROBLEM *)
+
+(* Axiom 'order_less_le' of class 'order': *)
+lemma zless_le: "((w::int) < z) = (w \<le> z & w \<noteq> z)"
+by (simp add: less_int_def)
+
+instance int :: order
+apply(intro_classes)
+apply(auto intro: zle_refl zle_trans zle_anti_sym zless_le simp add: less_int_def)
+done
+
+(* Axiom 'linorder_linear' of class 'linorder': *)
+
+lemma zle_linear_aux:
+  "le_aux z w \<or> le_aux w z"
+apply(cases w, cases z)
+apply(auto)
+done
+
+
+lemma zle_linear: "(z::int) \<le> w \<or> w \<le> z"
+apply(lifting zle_linear_aux)
+apply(injection)
+apply(rule quot_respect)+
+done
+
+instance int :: linorder
+proof qed (rule zle_linear)
+
+lemma zadd_left_mono_aux:
+  shows "le_aux i j \<Longrightarrow> le_aux (add_aux k i) (add_aux k j)"
+apply(cases k)
+apply(auto simp add: add_aux_def)
+done
+
+lemma zadd_left_mono: "i \<le> j \<Longrightarrow> k + i \<le> k + (j::int)"
+apply(lifting zadd_left_mono_aux[simplified add_aux_def])
+apply(injection)
+apply(rule quot_respect)+
+done
+(* PROBLEM *)
+
+
+
+subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*}
+
+(* PROBLEM: this has to be a definition, not an abbreviation *)
+(* otherwise the lemma nat_le_eq_zle cannot be lifted        *)
+fun
+  nat_aux
+where
+  "nat_aux (x, y) =  x - (y::nat)"
+
+quotient_def
+  "nat2::int\<Rightarrow>nat"
+as
+  "nat_aux"
+
+abbreviation
+  "less_aux x y \<equiv> (le_aux x y \<and> \<not>(x = y))"
+
+lemma nat_le_eq_zle_aux:
+  shows "less_aux (0, 0) w \<or> le_aux (0, 0) z \<Longrightarrow> (nat_aux w \<le> nat_aux z) = (le_aux w z)"
+apply(auto)
+sorry
+
+lemma [quot_respect]:
+  shows "(intrel ===> op =) nat_aux nat_aux"
+apply(auto)
+done
+
+lemma nat_le_eq_zle: "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)"
+unfolding less_int_def
+apply(lifting nat_le_eq_zle_aux)
+apply(injection)
+apply(simp_all only: quot_respect)
+done
+(* PROBLEM *)
+
+end