1.1 --- a/NEWS	Thu Aug 18 13:37:41 2011 +0200
     1.2 +++ b/NEWS	Sat Aug 20 09:42:34 2011 +0200
     1.3 @@ -70,7 +70,8 @@
     1.4  generalized theorems INF_cong and SUP_cong.  New type classes for complete
     1.5  boolean algebras and complete linear orders.  Lemmas Inf_less_iff,
     1.6  less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder.
     1.7 -Changed proposition of lemmas Inf_fun_def, Sup_fun_def, Inf_apply, Sup_apply.
     1.8 +Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def, Sup_fun_def,
     1.9 +Inf_apply, Sup_apply.
    1.10  Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary,
    1.11  INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter,
    1.12  INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, UNION_eq_Union_image,

     2.1 --- a/src/HOL/Complete_Lattice.thy	Thu Aug 18 13:37:41 2011 +0200
     2.2 +++ b/src/HOL/Complete_Lattice.thy	Sat Aug 20 09:42:34 2011 +0200
     2.3 @@ -414,8 +414,7 @@
     2.4    apply (simp_all only: INF_foundation_dual SUP_foundation_dual inf_Sup sup_Inf)
     2.5    done
     2.6  
     2.7 -subclass distrib_lattice proof -- {* Question: is it sufficient to include @{class distrib_lattice}
     2.8 -  and prove @{text inf_Sup} and @{text sup_Inf} from that? *}
     2.9 +subclass distrib_lattice proof
    2.10    fix a b c
    2.11    from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" .
    2.12    then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def Inf_insert)
    2.13 @@ -556,13 +555,13 @@
    2.14  begin
    2.15  
    2.16  definition
    2.17 -  "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"
    2.18 +  [simp]: "\<Sqinter>A \<longleftrightarrow> False \<notin> A"
    2.19  
    2.20  definition
    2.21 -  "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
    2.22 +  [simp]: "\<Squnion>A \<longleftrightarrow> True \<in> A"
    2.23  
    2.24  instance proof
    2.25 -qed (auto simp add: Inf_bool_def Sup_bool_def)
    2.26 +qed (auto intro: bool_induct)
    2.27  
    2.28  end
    2.29  
    2.30 @@ -572,7 +571,7 @@
    2.31    fix A :: "'a set"
    2.32    fix P :: "'a \<Rightarrow> bool"
    2.33    show "(\<Sqinter>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P x)"
    2.34 -    by (auto simp add: Ball_def INF_def Inf_bool_def)
    2.35 +    by (auto simp add: INF_def)
    2.36  qed
    2.37  
    2.38  lemma SUP_bool_eq [simp]:
    2.39 @@ -581,11 +580,11 @@
    2.40    fix A :: "'a set"
    2.41    fix P :: "'a \<Rightarrow> bool"
    2.42    show "(\<Squnion>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>A. P x)"
    2.43 -    by (auto simp add: Bex_def SUP_def Sup_bool_def)
    2.44 +    by (auto simp add: SUP_def)
    2.45  qed
    2.46  
    2.47  instance bool :: complete_boolean_algebra proof
    2.48 -qed (auto simp add: Inf_bool_def Sup_bool_def)
    2.49 +qed (auto intro: bool_induct)
    2.50  
    2.51  instantiation "fun" :: (type, complete_lattice) complete_lattice
    2.52  begin
    2.53 @@ -638,7 +637,7 @@
    2.54    have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"
    2.55      by auto
    2.56    then show "x \<in> \<Inter>A \<longleftrightarrow> x \<in> {x. \<forall>B \<in> A. x \<in> B}"
    2.57 -    by (simp add: Inf_fun_def Inf_bool_def) (simp add: mem_def)
    2.58 +    by (simp add: Inf_fun_def) (simp add: mem_def)
    2.59  qed
    2.60  
    2.61  lemma Inter_iff [simp,no_atp]: "A \<in> \<Inter>C \<longleftrightarrow> (\<forall>X\<in>C. A \<in> X)"
    2.62 @@ -821,7 +820,7 @@
    2.63    have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)"
    2.64      by auto
    2.65    then show "x \<in> \<Union>A \<longleftrightarrow> x \<in> {x. \<exists>B\<in>A. x \<in> B}"
    2.66 -    by (simp add: Sup_fun_def Sup_bool_def) (simp add: mem_def)
    2.67 +    by (simp add: Sup_fun_def) (simp add: mem_def)
    2.68  qed
    2.69  
    2.70  lemma Union_iff [simp, no_atp]:

     3.1 --- a/src/HOL/Library/More_Set.thy	Thu Aug 18 13:37:41 2011 +0200
     3.2 +++ b/src/HOL/Library/More_Set.thy	Sat Aug 20 09:42:34 2011 +0200
     3.3 @@ -50,7 +50,7 @@
     3.4  
     3.5  lemma remove_set_compl:
     3.6    "remove x (- set xs) = - set (List.insert x xs)"
     3.7 -  by (auto simp del: mem_def simp add: remove_def List.insert_def)
     3.8 +  by (auto simp add: remove_def List.insert_def)
     3.9  
    3.10  lemma image_set:
    3.11    "image f (set xs) = set (map f xs)"

     4.1 --- a/src/HOL/Main.thy	Thu Aug 18 13:37:41 2011 +0200
     4.2 +++ b/src/HOL/Main.thy	Sat Aug 20 09:42:34 2011 +0200
     4.3 @@ -11,4 +11,17 @@
     4.4  
     4.5  text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
     4.6  
     4.7 +text {* Compatibility layer -- to be dropped *}
     4.8 +
     4.9 +lemma Inf_bool_def:
    4.10 +  "Inf A \<longleftrightarrow> (\<forall>x\<in>A. x)"
    4.11 +  by (auto intro: bool_induct)
    4.12 +
    4.13 +lemma Sup_bool_def:
    4.14 +  "Sup A \<longleftrightarrow> (\<exists>x\<in>A. x)"
    4.15 +  by auto
    4.16 +
    4.17 +declare Complete_Lattice.Inf_bool_def [simp del]
    4.18 +declare Complete_Lattice.Sup_bool_def [simp del]
    4.19 +
    4.20  end

     5.1 --- a/src/HOL/Nat.thy	Thu Aug 18 13:37:41 2011 +0200
     5.2 +++ b/src/HOL/Nat.thy	Sat Aug 20 09:42:34 2011 +0200
     5.3 @@ -22,10 +22,7 @@
     5.4  
     5.5  typedecl ind
     5.6  
     5.7 -axiomatization
     5.8 -  Zero_Rep :: ind and
     5.9 -  Suc_Rep :: "ind => ind"
    5.10 -where
    5.11 +axiomatization Zero_Rep :: ind and Suc_Rep :: "ind => ind" where
    5.12    -- {* the axiom of infinity in 2 parts *}
    5.13    Suc_Rep_inject:       "Suc_Rep x = Suc_Rep y ==> x = y" and
    5.14    Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
    5.15 @@ -34,10 +31,9 @@
    5.16  
    5.17  text {* Type definition *}
    5.18  
    5.19 -inductive Nat :: "ind \<Rightarrow> bool"
    5.20 -where
    5.21 -    Zero_RepI: "Nat Zero_Rep"
    5.22 -  | Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
    5.23 +inductive Nat :: "ind \<Rightarrow> bool" where
    5.24 +  Zero_RepI: "Nat Zero_Rep"
    5.25 +| Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
    5.26  
    5.27  typedef (open Nat) nat = "{n. Nat n}"
    5.28    using Nat.Zero_RepI by auto
    5.29 @@ -142,10 +138,9 @@
    5.30  instantiation nat :: "{minus, comm_monoid_add}"
    5.31  begin
    5.32  
    5.33 -primrec plus_nat
    5.34 -where
    5.35 +primrec plus_nat where
    5.36    add_0:      "0 + n = (n\<Colon>nat)"
    5.37 -  | add_Suc:  "Suc m + n = Suc (m + n)"
    5.38 +| add_Suc:  "Suc m + n = Suc (m + n)"
    5.39  
    5.40  lemma add_0_right [simp]: "m + 0 = (m::nat)"
    5.41    by (induct m) simp_all
    5.42 @@ -158,8 +153,7 @@
    5.43  lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
    5.44    by simp
    5.45  
    5.46 -primrec minus_nat
    5.47 -where
    5.48 +primrec minus_nat where
    5.49    diff_0 [code]: "m - 0 = (m\<Colon>nat)"
    5.50  | diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
    5.51  
    5.52 @@ -188,10 +182,9 @@
    5.53  definition
    5.54    One_nat_def [simp]: "1 = Suc 0"
    5.55  
    5.56 -primrec times_nat
    5.57 -where
    5.58 +primrec times_nat where
    5.59    mult_0:     "0 * n = (0\<Colon>nat)"
    5.60 -  | mult_Suc: "Suc m * n = n + (m * n)"
    5.61 +| mult_Suc: "Suc m * n = n + (m * n)"
    5.62  
    5.63  lemma mult_0_right [simp]: "(m::nat) * 0 = 0"
    5.64    by (induct m) simp_all
    5.65 @@ -364,7 +357,7 @@
    5.66  
    5.67  primrec less_eq_nat where
    5.68    "(0\<Colon>nat) \<le> n \<longleftrightarrow> True"
    5.69 -  | "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)"
    5.70 +| "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)"
    5.71  
    5.72  declare less_eq_nat.simps [simp del]
    5.73  lemma [code]: "(0\<Colon>nat) \<le> n \<longleftrightarrow> True" by (simp add: less_eq_nat.simps)
    5.74 @@ -1200,8 +1193,8 @@
    5.75  begin
    5.76  
    5.77  primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
    5.78 -    "funpow 0 f = id"
    5.79 -  | "funpow (Suc n) f = f o funpow n f"
    5.80 +  "funpow 0 f = id"
    5.81 +| "funpow (Suc n) f = f o funpow n f"
    5.82  
    5.83  end
    5.84  
    5.85 @@ -1267,7 +1260,7 @@
    5.86  
    5.87  primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
    5.88    "of_nat_aux inc 0 i = i"
    5.89 -  | "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- {* tail recursive *}
    5.90 +| "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- {* tail recursive *}
    5.91  
    5.92  lemma of_nat_code:
    5.93    "of_nat n = of_nat_aux (\<lambda>i. i + 1) n 0"

     6.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Thu Aug 18 13:37:41 2011 +0200
     6.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Sat Aug 20 09:42:34 2011 +0200
     6.3 @@ -159,7 +159,7 @@
     6.4  by (rule Rep_Nat_inverse)
     6.5  
     6.6  lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})"
     6.7 -nitpick [card = 1, unary_ints, max_potential = 0, expect = none]
     6.8 +(*nitpick [card = 1, unary_ints, max_potential = 0, expect = none] (?)*)
     6.9  by (rule Zero_int_def_raw)
    6.10  
    6.11  lemma "Abs_list (Rep_list a) = a"