diff -r 6f6ee78c7357 -r ba7e81531c6d Quot/Examples/LarryInt.thy
--- a/Quot/Examples/LarryInt.thy	Fri Jan 01 11:30:00 2010 +0100
+++ b/Quot/Examples/LarryInt.thy	Fri Jan 01 23:59:32 2010 +0100
@@ -76,18 +76,18 @@
   shows "(intrel ===> intrel) uminus_raw uminus_raw"
   by (simp add: uminus_raw_def)
   
-lemma zminus_zminus: 
-  shows "- (- z) = (z::int)"
-apply(lifting zminus_zminus_raw)
-done
+lemma zminus_zminus:
+  fixes z::"int"
+  shows "- (- z) = z"
+  by(lifting zminus_zminus_raw)
 
 lemma zminus_0_raw:
   shows "uminus_raw (0, 0) = (0, 0::nat)"
-by (simp add: uminus_raw_def)
+  by (simp add: uminus_raw_def)
 
-lemma zminus_0: "- 0 = (0::int)"
-apply(lifting zminus_0_raw)
-done
+lemma zminus_0: 
+  shows "- 0 = (0::int)"
+  by (lifting zminus_0_raw)
 
 subsection{*Integer Addition*}
 
@@ -101,9 +101,9 @@
 by (simp add: add_raw_def)
 
 lemma zminus_zadd_distrib: 
-  shows "- (z + w) = (- z) + (- w::int)"
-apply(lifting zminus_zadd_distrib_raw)
-done
+  fixes z w::"int"
+  shows "- (z + w) = (- z) + (- w)"
+  by(lifting zminus_zadd_distrib_raw)
 
 lemma zadd_commute_raw:
   shows "add_raw z w = add_raw w z"
@@ -111,43 +111,45 @@
    (simp add: add_raw_def)
 
 lemma zadd_commute:
+  fixes z w::"int"
   shows "(z::int) + w = w + z"
-apply(lifting zadd_commute_raw)
-done
+  by (lifting zadd_commute_raw)
 
 lemma zadd_assoc_raw:
   shows "add_raw (add_raw z1 z2) z3 = add_raw z1 (add_raw z2 z3)"
-by (cases z1, cases z2, cases z3) (simp add: add_raw_def)
+  by (cases z1, cases z2, cases z3) (simp add: add_raw_def)
 
-lemma zadd_assoc: "((z1::int) + z2) + z3 = z1 + (z2 + z3)"
-apply(lifting zadd_assoc_raw)
-done
+lemma zadd_assoc: 
+  fixes z1 z2 z3::"int"
+  shows "(z1 + z2) + z3 = z1 + (z2 + z3)"
+  by (lifting zadd_assoc_raw)
 
 lemma zadd_0_raw:
-  fixes z::"nat \<times> nat"
   shows "add_raw (0, 0) z = z"
-by (simp add: add_raw_def)
+  by (simp add: add_raw_def)
 
 
-(*also for the instance declaration int :: plus_ac0*)
-lemma zadd_0: "(0::int) + z = z"
-apply(lifting zadd_0_raw)
-done
+text {*also for the instance declaration int :: plus_ac0*}
+lemma zadd_0: 
+  fixes z::"int"
+  shows "0 + z = z"
+  by (lifting zadd_0_raw)
 
 lemma zadd_zminus_inverse_raw:
   shows "intrel (add_raw (uminus_raw z) z) (0, 0)"
-by (cases z) (simp add: add_raw_def uminus_raw_def)
+  by (cases z) (simp add: add_raw_def uminus_raw_def)
 
-lemma zadd_zminus_inverse2: "(- z) + z = (0::int)"
-apply(lifting zadd_zminus_inverse_raw)
-done
+lemma zadd_zminus_inverse2: 
+  fixes z::"int"
+  shows "(- z) + z = 0"
+  by (lifting zadd_zminus_inverse_raw)
 
 subsection{*Integer Multiplication*}
 
 lemma zmult_zminus_raw:
   shows "mult_raw (uminus_raw z) w = uminus_raw (mult_raw z w)"
 apply(cases z, cases w)
-apply(simp add:uminus_raw_def)
+apply(simp add: uminus_raw_def)
 done
 
 lemma mult_raw_fst:
@@ -185,9 +187,10 @@
 apply(assumption)
 done
 
-lemma zmult_zminus: "(- z) * w = - (z * (w::int))"
-apply(lifting zmult_zminus_raw)
-done
+lemma zmult_zminus: 
+  fixes z w::"int"
+  shows "(- z) * w = - (z * w)"
+  by (lifting zmult_zminus_raw)
 
 lemma zmult_commute_raw: 
   shows "mult_raw z w = mult_raw w z"
@@ -195,8 +198,10 @@
 apply(simp add: add_ac mult_ac)
 done
 
-lemma zmult_commute: "(z::int) * w = w * z"
-by (lifting zmult_commute_raw)
+lemma zmult_commute: 
+  fixes z w::"int"
+  shows "z * w = w * z"
+  by (lifting zmult_commute_raw)
 
 lemma zmult_assoc_raw:
   shows "mult_raw (mult_raw z1 z2) z3 = mult_raw z1 (mult_raw z2 z3)"
@@ -204,8 +209,10 @@
 apply(simp add: add_mult_distrib2 mult_ac)
 done
 
-lemma zmult_assoc: "((z1::int) * z2) * z3 = z1 * (z2 * z3)"
-by (lifting zmult_assoc_raw)
+lemma zmult_assoc: 
+  fixes z1 z2 z3::"int"
+  shows "(z1 * z2) * z3 = z1 * (z2 * z3)"
+  by (lifting zmult_assoc_raw)
 
 lemma zadd_mult_distrib_raw:
   shows "mult_raw (add_raw z1 z2) w = add_raw (mult_raw z1 w) (mult_raw z2 w)"
@@ -213,18 +220,25 @@
 apply(simp add: add_mult_distrib2 mult_ac add_raw_def)
 done
 
-lemma zadd_zmult_distrib: "((z1::int) + z2) * w = (z1 * w) + (z2 * w)"
-apply(lifting zadd_mult_distrib_raw)
-done
+lemma zadd_zmult_distrib: 
+  fixes z1 z2 w::"int"
+  shows "(z1 + z2) * w = (z1 * w) + (z2 * w)"
+  by(lifting zadd_mult_distrib_raw)
+
+lemma zadd_zmult_distrib2: 
+  fixes w z1 z2::"int"
+  shows "w * (z1 + z2) = (w * z1) + (w * z2)"
+  by (simp add: zmult_commute [of w] zadd_zmult_distrib)
 
-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: 
+  fixes w z1 z2::"int"
+  shows "(z1 - z2) * w = (z1 * w) - (z2 * w)"
+  by (simp add: diff_int_def zadd_zmult_distrib zmult_zminus)
 
-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)
+lemma zdiff_zmult_distrib2: 
+  fixes w z1 z2::"int"
+  shows "w * (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
@@ -232,20 +246,21 @@
 
 lemma zmult_1_raw:
   shows "mult_raw (1, 0) z = z"
-apply(cases z)
-apply(auto)
-done
+  by (cases z) (auto)
 
-lemma zmult_1: "(1::int) * z = z"
-apply(lifting zmult_1_raw)
-done
+lemma zmult_1:
+  fixes z::"int"
+  shows "1 * z = z"
+  by (lifting zmult_1_raw)
 
-lemma zmult_1_right: "z * (1::int) = z"
-by (rule trans [OF zmult_commute zmult_1])
+lemma zmult_1_right: 
+  fixes z::"int"
+  shows "z * 1 = z"
+  by (rule trans [OF zmult_commute zmult_1])
 
 lemma zero_not_one:
   shows "\<not>(intrel (0, 0) (1::nat, 0::nat))"
-by auto
+  by auto
 
 text{*The Integers Form A Ring*}
 instance int :: comm_ring_1
@@ -267,29 +282,29 @@
 subsection{*The @{text "\<le>"} Ordering*}
 
 lemma zle_refl_raw:
-  "le_raw w w"
-apply(cases w)
-apply(simp add: le_raw_def)
-done
+  shows "le_raw w w"
+  by (cases w) (simp add: le_raw_def)
 
 lemma [quot_respect]:
   shows "(intrel ===> intrel ===> op =) le_raw le_raw"
-by (auto) (simp_all add: le_raw_def)
+  by (auto) (simp_all add: le_raw_def)
 
-lemma zle_refl: "w \<le> (w::int)"
-apply(lifting zle_refl_raw)
-done
+lemma zle_refl: 
+  fixes w::"int"
+  shows "w \<le> w"
+  by (lifting zle_refl_raw)
+
 
 lemma zle_trans_raw:
   shows "\<lbrakk>le_raw i j; le_raw j k\<rbrakk> \<Longrightarrow> le_raw i k"
 apply(cases i, cases j, cases k)
-apply(auto)
-apply(simp add:le_raw_def)
+apply(auto simp add: le_raw_def)
 done
 
-lemma zle_trans: "\<lbrakk>i \<le> j; j \<le> k\<rbrakk> \<Longrightarrow> i \<le> (k::int)"
-apply(lifting zle_trans_raw)
-done
+lemma zle_trans: 
+  fixes i j k::"int"
+  shows "\<lbrakk>i \<le> j; j \<le> k\<rbrakk> \<Longrightarrow> i \<le> k"
+  by (lifting zle_trans_raw)
 
 lemma zle_anti_sym_raw:
   shows "\<lbrakk>le_raw z w; le_raw w z\<rbrakk> \<Longrightarrow> intrel z w"
@@ -297,34 +312,43 @@
 apply(auto iff: le_raw_def)
 done
 
-lemma zle_anti_sym: "\<lbrakk>z \<le> w; w \<le> z\<rbrakk> \<Longrightarrow> z = (w::int)"
-apply(lifting zle_anti_sym_raw)
-done
+lemma zle_anti_sym: 
+  fixes z w::"int"
+  shows "\<lbrakk>z \<le> w; w \<le> z\<rbrakk> \<Longrightarrow> z = w"
+  by (lifting zle_anti_sym_raw)
+
 
 (* 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)
+lemma zless_le: 
+  fixes w z::"int"
+  shows "(w < 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)
+apply (default)
+apply(auto simp add: zless_le zle_anti_sym)[1]
+apply(rule zle_refl)
+apply(erule zle_trans, assumption)
+apply(erule zle_anti_sym, assumption)
 done
 
 (* Axiom 'linorder_linear' of class 'linorder': *)
 
 lemma zle_linear_raw:
-  "le_raw z w \<or> le_raw w z"
+  shows "le_raw z w \<or> le_raw w z"
 apply(cases w, cases z)
 apply(auto iff: le_raw_def)
 done
 
-
-lemma zle_linear: "(z::int) \<le> w \<or> w \<le> z"
-apply(lifting zle_linear_raw)
-done
+lemma zle_linear: 
+  fixes z w::"int"
+  shows "z \<le> w \<or> w \<le> z"
+  by (lifting zle_linear_raw)
 
 instance int :: linorder
-proof qed (rule zle_linear)
+apply(default)
+apply(rule zle_linear)
+done
 
 lemma zadd_left_mono_raw:
   shows "le_raw i j \<Longrightarrow> le_raw (add_raw k i) (add_raw k j)"
@@ -332,10 +356,10 @@
 apply(auto simp add: add_raw_def le_raw_def)
 done
 
-lemma zadd_left_mono: "i \<le> j \<Longrightarrow> k + i \<le> k + (j::int)"
-apply(lifting zadd_left_mono_raw)
-done
-
+lemma zadd_left_mono: 
+  fixes i j::"int"
+  shows "i \<le> j \<Longrightarrow> k + i \<le> k + j"
+  by (lifting zadd_left_mono_raw)
 
 
 subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*}
@@ -344,7 +368,7 @@
   "nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
 
 quotient_definition
-  "nat2::int\<Rightarrow>nat"
+  "nat2::int \<Rightarrow> nat"
 as
   "nat_raw"
 
@@ -358,12 +382,12 @@
 
 lemma [quot_respect]:
   shows "(intrel ===> op =) nat_raw nat_raw"
-apply(auto iff: nat_raw_def)
-done
+  by (auto iff: nat_raw_def)
 
-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_raw)
-done
+lemma nat_le_eq_zle: 
+  fixes w z::"int"
+  shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)"
+  unfolding less_int_def
+  by (lifting nat_le_eq_zle_raw)
 
 end