# HG changeset patch
# User huffman
# Date 1313847343 25200
# Node ID e5294bcf58a46f0390ac0b7f1f3e54d93844d9a3
# Parent  8321948340ea589ab38f937586dbbb97030f1c48# Parent  6325ea1c5dfd5349c48117db142863f8c9a76194
merged

diff -r 8321948340ea -r e5294bcf58a4 NEWS
--- a/NEWS	Sat Aug 20 06:34:51 2011 -0700
+++ b/NEWS	Sat Aug 20 06:35:43 2011 -0700
@@ -70,7 +70,8 @@
 generalized theorems INF_cong and SUP_cong.  New type classes for complete
 boolean algebras and complete linear orders.  Lemmas Inf_less_iff,
 less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder.
-Changed proposition of lemmas Inf_fun_def, Sup_fun_def, Inf_apply, Sup_apply.
+Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def, Sup_fun_def,
+Inf_apply, Sup_apply.
 Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary,
 INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter,
 INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, UNION_eq_Union_image,
diff -r 8321948340ea -r e5294bcf58a4 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Sat Aug 20 06:34:51 2011 -0700
+++ b/src/HOL/Complete_Lattice.thy	Sat Aug 20 06:35:43 2011 -0700
@@ -414,8 +414,7 @@
   apply (simp_all only: INF_foundation_dual SUP_foundation_dual inf_Sup sup_Inf)
   done
 
-subclass distrib_lattice proof -- {* Question: is it sufficient to include @{class distrib_lattice}
-  and prove @{text inf_Sup} and @{text sup_Inf} from that? *}
+subclass distrib_lattice proof
   fix a b c
   from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" .
   then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def Inf_insert)
@@ -556,13 +555,13 @@
 begin
 
 definition
-  "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"
+  [simp]: "\<Sqinter>A \<longleftrightarrow> False \<notin> A"
 
 definition
-  "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
+  [simp]: "\<Squnion>A \<longleftrightarrow> True \<in> A"
 
 instance proof
-qed (auto simp add: Inf_bool_def Sup_bool_def)
+qed (auto intro: bool_induct)
 
 end
 
@@ -572,7 +571,7 @@
   fix A :: "'a set"
   fix P :: "'a \<Rightarrow> bool"
   show "(\<Sqinter>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P x)"
-    by (auto simp add: Ball_def INF_def Inf_bool_def)
+    by (auto simp add: INF_def)
 qed
 
 lemma SUP_bool_eq [simp]:
@@ -581,11 +580,11 @@
   fix A :: "'a set"
   fix P :: "'a \<Rightarrow> bool"
   show "(\<Squnion>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>A. P x)"
-    by (auto simp add: Bex_def SUP_def Sup_bool_def)
+    by (auto simp add: SUP_def)
 qed
 
 instance bool :: complete_boolean_algebra proof
-qed (auto simp add: Inf_bool_def Sup_bool_def)
+qed (auto intro: bool_induct)
 
 instantiation "fun" :: (type, complete_lattice) complete_lattice
 begin
@@ -638,7 +637,7 @@
   have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"
     by auto
   then show "x \<in> \<Inter>A \<longleftrightarrow> x \<in> {x. \<forall>B \<in> A. x \<in> B}"
-    by (simp add: Inf_fun_def Inf_bool_def) (simp add: mem_def)
+    by (simp add: Inf_fun_def) (simp add: mem_def)
 qed
 
 lemma Inter_iff [simp,no_atp]: "A \<in> \<Inter>C \<longleftrightarrow> (\<forall>X\<in>C. A \<in> X)"
@@ -821,7 +820,7 @@
   have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)"
     by auto
   then show "x \<in> \<Union>A \<longleftrightarrow> x \<in> {x. \<exists>B\<in>A. x \<in> B}"
-    by (simp add: Sup_fun_def Sup_bool_def) (simp add: mem_def)
+    by (simp add: Sup_fun_def) (simp add: mem_def)
 qed
 
 lemma Union_iff [simp, no_atp]:
diff -r 8321948340ea -r e5294bcf58a4 src/HOL/Library/More_Set.thy
--- a/src/HOL/Library/More_Set.thy	Sat Aug 20 06:34:51 2011 -0700
+++ b/src/HOL/Library/More_Set.thy	Sat Aug 20 06:35:43 2011 -0700
@@ -50,7 +50,7 @@
 
 lemma remove_set_compl:
   "remove x (- set xs) = - set (List.insert x xs)"
-  by (auto simp del: mem_def simp add: remove_def List.insert_def)
+  by (auto simp add: remove_def List.insert_def)
 
 lemma image_set:
   "image f (set xs) = set (map f xs)"
diff -r 8321948340ea -r e5294bcf58a4 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Sat Aug 20 06:34:51 2011 -0700
+++ b/src/HOL/Main.thy	Sat Aug 20 06:35:43 2011 -0700
@@ -11,4 +11,17 @@
 
 text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
 
+text {* Compatibility layer -- to be dropped *}
+
+lemma Inf_bool_def:
+  "Inf A \<longleftrightarrow> (\<forall>x\<in>A. x)"
+  by (auto intro: bool_induct)
+
+lemma Sup_bool_def:
+  "Sup A \<longleftrightarrow> (\<exists>x\<in>A. x)"
+  by auto
+
+declare Complete_Lattice.Inf_bool_def [simp del]
+declare Complete_Lattice.Sup_bool_def [simp del]
+
 end
diff -r 8321948340ea -r e5294bcf58a4 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sat Aug 20 06:34:51 2011 -0700
+++ b/src/HOL/Nat.thy	Sat Aug 20 06:35:43 2011 -0700
@@ -22,10 +22,7 @@
 
 typedecl ind
 
-axiomatization
-  Zero_Rep :: ind and
-  Suc_Rep :: "ind => ind"
-where
+axiomatization Zero_Rep :: ind and Suc_Rep :: "ind => ind" where
   -- {* the axiom of infinity in 2 parts *}
   Suc_Rep_inject:       "Suc_Rep x = Suc_Rep y ==> x = y" and
   Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
@@ -34,10 +31,9 @@
 
 text {* Type definition *}
 
-inductive Nat :: "ind \<Rightarrow> bool"
-where
-    Zero_RepI: "Nat Zero_Rep"
-  | Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
+inductive Nat :: "ind \<Rightarrow> bool" where
+  Zero_RepI: "Nat Zero_Rep"
+| Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
 
 typedef (open Nat) nat = "{n. Nat n}"
   using Nat.Zero_RepI by auto
@@ -142,10 +138,9 @@
 instantiation nat :: "{minus, comm_monoid_add}"
 begin
 
-primrec plus_nat
-where
+primrec plus_nat where
   add_0:      "0 + n = (n\<Colon>nat)"
-  | add_Suc:  "Suc m + n = Suc (m + n)"
+| add_Suc:  "Suc m + n = Suc (m + n)"
 
 lemma add_0_right [simp]: "m + 0 = (m::nat)"
   by (induct m) simp_all
@@ -158,8 +153,7 @@
 lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
   by simp
 
-primrec minus_nat
-where
+primrec minus_nat where
   diff_0 [code]: "m - 0 = (m\<Colon>nat)"
 | diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
 
@@ -188,10 +182,9 @@
 definition
   One_nat_def [simp]: "1 = Suc 0"
 
-primrec times_nat
-where
+primrec times_nat where
   mult_0:     "0 * n = (0\<Colon>nat)"
-  | mult_Suc: "Suc m * n = n + (m * n)"
+| mult_Suc: "Suc m * n = n + (m * n)"
 
 lemma mult_0_right [simp]: "(m::nat) * 0 = 0"
   by (induct m) simp_all
@@ -364,7 +357,7 @@
 
 primrec less_eq_nat where
   "(0\<Colon>nat) \<le> n \<longleftrightarrow> True"
-  | "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)"
+| "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)"
 
 declare less_eq_nat.simps [simp del]
 lemma [code]: "(0\<Colon>nat) \<le> n \<longleftrightarrow> True" by (simp add: less_eq_nat.simps)
@@ -1200,8 +1193,8 @@
 begin
 
 primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
-    "funpow 0 f = id"
-  | "funpow (Suc n) f = f o funpow n f"
+  "funpow 0 f = id"
+| "funpow (Suc n) f = f o funpow n f"
 
 end
 
@@ -1267,7 +1260,7 @@
 
 primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
   "of_nat_aux inc 0 i = i"
-  | "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- {* tail recursive *}
+| "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- {* tail recursive *}
 
 lemma of_nat_code:
   "of_nat n = of_nat_aux (\<lambda>i. i + 1) n 0"
diff -r 8321948340ea -r e5294bcf58a4 src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Sat Aug 20 06:34:51 2011 -0700
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Sat Aug 20 06:35:43 2011 -0700
@@ -159,7 +159,7 @@
 by (rule Rep_Nat_inverse)
 
 lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})"
-nitpick [card = 1, unary_ints, max_potential = 0, expect = none]
+(*nitpick [card = 1, unary_ints, max_potential = 0, expect = none] (?)*)
 by (rule Zero_int_def_raw)
 
 lemma "Abs_list (Rep_list a) = a"
diff -r 8321948340ea -r e5294bcf58a4 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Aug 20 06:34:51 2011 -0700
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Aug 20 06:35:43 2011 -0700
@@ -251,7 +251,7 @@
           (if contains_existentials then pnf_narrowing_engine else narrowing_engine)
         val _ = File.write main_file main
         val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
-        val cmd = "exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
+        val cmd = "exec \"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables " ^
           (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
           " -o " ^ executable ^ ";"
         val (result, compilation_time) =
diff -r 8321948340ea -r e5294bcf58a4 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Sat Aug 20 06:34:51 2011 -0700
+++ b/src/Tools/Code/code_haskell.ML	Sat Aug 20 06:35:43 2011 -0700
@@ -453,7 +453,7 @@
     (target, { serializer = serializer, literals = literals,
       check = { env_var = "ISABELLE_GHC", make_destination = I,
         make_command = fn module_name =>
-          "\"$ISABELLE_GHC\" -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^
+          "\"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables -odir build -hidir build -stubdir build -e \"\" " ^
             module_name ^ ".hs" } })
   #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
       brackify_infix (1, R) fxy (