adjusted to set/pred distinction by means of type constructor `set`
authorhaftmann
Sat Dec 24 15:53:10 2011 +0100 (2011-12-24)
changeset 45970b6d0cff57d96
parent 45969 562e99c3d316
child 45971 b27e93132603
adjusted to set/pred distinction by means of type constructor `set`
src/HOL/Library/Cset.thy
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
src/HOL/Library/Quotient_Set.thy
src/HOL/Metis_Examples/Message.thy
src/HOL/Metis_Examples/Proxies.thy
src/HOL/Metis_Examples/Tarski.thy
src/HOL/Metis_Examples/Trans_Closure.thy
src/HOL/MicroJava/BV/BVExample.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/Nitpick.thy
src/HOL/Nitpick_Examples/Core_Nits.thy
src/HOL/Nitpick_Examples/Induct_Nits.thy
src/HOL/Nitpick_Examples/Manual_Nits.thy
src/HOL/Nitpick_Examples/Mini_Nits.thy
src/HOL/Nitpick_Examples/Typedef_Nits.thy
src/HOL/Predicate.thy
src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
src/HOL/Predicate_Compile_Examples/Examples.thy
src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
src/HOL/Quotient_Examples/Lift_Set.thy
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Library/Cset.thy	Sat Dec 24 15:53:10 2011 +0100
     1.2 +++ b/src/HOL/Library/Cset.thy	Sat Dec 24 15:53:10 2011 +0100
     1.3 @@ -24,10 +24,6 @@
     1.4  definition member :: "'a Cset.set \<Rightarrow> 'a \<Rightarrow> bool" where
     1.5    "member A x \<longleftrightarrow> x \<in> set_of A"
     1.6  
     1.7 -lemma member_set_of:
     1.8 -  "set_of = member"
     1.9 -  by (rule ext)+ (simp add: member_def mem_def)
    1.10 -
    1.11  lemma member_Set [simp]:
    1.12    "member (Set A) x \<longleftrightarrow> x \<in> A"
    1.13    by (simp add: member_def)
    1.14 @@ -38,7 +34,7 @@
    1.15  
    1.16  lemma set_eq_iff:
    1.17    "A = B \<longleftrightarrow> member A = member B"
    1.18 -  by (auto simp add: fun_eq_iff set_of_inject [symmetric] member_def mem_def)
    1.19 +  by (auto simp add: fun_eq_iff set_of_inject [symmetric] member_def)
    1.20  hide_fact (open) set_eq_iff
    1.21  
    1.22  lemma set_eqI:
    1.23 @@ -76,7 +72,7 @@
    1.24    [simp]: "A - B = Set (set_of A - set_of B)"
    1.25  
    1.26  instance proof
    1.27 -qed (auto intro!: Cset.set_eqI simp add: member_def mem_def)
    1.28 +qed (auto intro!: Cset.set_eqI simp add: member_def)
    1.29  
    1.30  end
    1.31  
    1.32 @@ -364,19 +360,13 @@
    1.33       Predicate.Empty \<Rightarrow> Cset.empty
    1.34     | Predicate.Insert x P \<Rightarrow> Cset.insert x (of_pred P)
    1.35     | Predicate.Join P xq \<Rightarrow> sup (of_pred P) (of_seq xq))"
    1.36 -  apply (auto split: seq.split simp add: Predicate.Seq_def of_pred_def Cset.set_eq_iff sup_apply eval_member [symmetric] member_def [symmetric] Collect_def mem_def member_set_of)
    1.37 -  apply (unfold Set.insert_def Collect_def sup_apply member_set_of)
    1.38 -  apply simp_all
    1.39 -  done
    1.40 +  by (auto split: seq.split simp add: Predicate.Seq_def of_pred_def Cset.set_eq_iff sup_apply eval_member [symmetric] member_def [symmetric])
    1.41  
    1.42  lemma of_seq_code [code]:
    1.43    "of_seq Predicate.Empty = Cset.empty"
    1.44    "of_seq (Predicate.Insert x P) = Cset.insert x (of_pred P)"
    1.45    "of_seq (Predicate.Join P xq) = sup (of_pred P) (of_seq xq)"
    1.46 -  apply (auto simp add: of_seq_def of_pred_def Cset.set_eq_iff mem_def Collect_def)
    1.47 -  apply (unfold Set.insert_def Collect_def sup_apply member_set_of)
    1.48 -  apply simp_all
    1.49 -  done
    1.50 +  by (auto simp add: of_seq_def of_pred_def Cset.set_eq_iff)
    1.51  
    1.52  lemma bind_set:
    1.53    "Cset.bind (Cset.set xs) f = fold (sup \<circ> f) xs (Cset.set [])"
    1.54 @@ -387,9 +377,9 @@
    1.55    "pred_of_cset (Cset.set xs) = foldr sup (List.map Predicate.single xs) bot"
    1.56  proof -
    1.57    have "pred_of_cset (Cset.set xs) = Predicate.Pred (\<lambda>x. x \<in> set xs)"
    1.58 -    by (simp add: Cset.pred_of_cset_def member_set)
    1.59 +    by (simp add: Cset.pred_of_cset_def)
    1.60    moreover have "foldr sup (List.map Predicate.single xs) bot = \<dots>"
    1.61 -    by (induct xs) (auto simp add: bot_pred_def intro: pred_eqI, simp add: mem_def)
    1.62 +    by (induct xs) (auto simp add: bot_pred_def intro: pred_eqI)
    1.63    ultimately show ?thesis by simp
    1.64  qed
    1.65  hide_fact (open) pred_of_cset_set
     2.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Sat Dec 24 15:53:10 2011 +0100
     2.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Sat Dec 24 15:53:10 2011 +0100
     2.3 @@ -12,7 +12,7 @@
     2.4  declare le_bool_def_raw[code_pred_inline]
     2.5  
     2.6  lemma min_bool_eq [code_pred_inline]: "(min :: bool => bool => bool) == (op &)"
     2.7 -by (rule eq_reflection) (auto simp add: fun_eq_iff min_def le_bool_def)
     2.8 +by (rule eq_reflection) (auto simp add: fun_eq_iff min_def)
     2.9  
    2.10  lemma [code_pred_inline]: 
    2.11    "((A::bool) ~= (B::bool)) = ((A & ~ B) | (B & ~ A))"
    2.12 @@ -31,11 +31,7 @@
    2.13  
    2.14  section {* Set operations *}
    2.15  
    2.16 -declare Collect_def[code_pred_inline]
    2.17 -declare mem_def[code_pred_inline]
    2.18 -
    2.19  declare eq_reflection[OF empty_def, code_pred_inline]
    2.20 -declare insert_code[code_pred_def]
    2.21  
    2.22  declare subset_iff[code_pred_inline]
    2.23  
    2.24 @@ -45,15 +41,16 @@
    2.25  
    2.26  lemma Diff[code_pred_inline]:
    2.27    "(A - B) = (%x. A x \<and> \<not> B x)"
    2.28 -by (auto simp add: mem_def)
    2.29 +  by (simp add: fun_eq_iff minus_apply)
    2.30  
    2.31  lemma subset_eq[code_pred_inline]:
    2.32    "(P :: 'a => bool) < (Q :: 'a => bool) == ((\<exists>x. Q x \<and> (\<not> P x)) \<and> (\<forall> x. P x --> Q x))"
    2.33 -by (rule eq_reflection) (fastforce simp add: mem_def)
    2.34 +  by (rule eq_reflection) (auto simp add: less_fun_def le_fun_def)
    2.35  
    2.36  lemma set_equality[code_pred_inline]:
    2.37 -  "(A = B) = ((\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x))"
    2.38 -by (fastforce simp add: mem_def)
    2.39 +  "A = B \<longleftrightarrow> (\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x)"
    2.40 +  by (auto simp add: fun_eq_iff)
    2.41 +
    2.42  
    2.43  section {* Setup for Numerals *}
    2.44  
    2.45 @@ -197,30 +194,6 @@
    2.46  declare size_list_simps[code_pred_def]
    2.47  declare size_list_def[symmetric, code_pred_inline]
    2.48  
    2.49 -subsection {* Alternative rules for set *}
    2.50 -
    2.51 -lemma set_ConsI1 [code_pred_intro]:
    2.52 -  "set (x # xs) x"
    2.53 -unfolding mem_def[symmetric, of _ x]
    2.54 -by auto
    2.55 -
    2.56 -lemma set_ConsI2 [code_pred_intro]:
    2.57 -  "set xs x ==> set (x' # xs) x" 
    2.58 -unfolding mem_def[symmetric, of _ x]
    2.59 -by auto
    2.60 -
    2.61 -code_pred [skip_proof] set
    2.62 -proof -
    2.63 -  case set
    2.64 -  from this show thesis
    2.65 -    apply (case_tac xb)
    2.66 -    apply auto
    2.67 -    unfolding mem_def[symmetric, of _ xc]
    2.68 -    apply auto
    2.69 -    unfolding mem_def
    2.70 -    apply fastforce
    2.71 -    done
    2.72 -qed
    2.73  
    2.74  subsection {* Alternative rules for list_all2 *}
    2.75  
    2.76 @@ -259,5 +232,4 @@
    2.77  lemma less_nat_k_0 [code_pred_simp]: "less_nat k 0 == False"
    2.78  unfolding less_nat[symmetric] by auto
    2.79  
    2.80 -
    2.81  end
    2.82 \ No newline at end of file
     3.1 --- a/src/HOL/Library/Quotient_Set.thy	Sat Dec 24 15:53:10 2011 +0100
     3.2 +++ b/src/HOL/Library/Quotient_Set.thy	Sat Dec 24 15:53:10 2011 +0100
     3.3 @@ -76,20 +76,10 @@
     3.4  
     3.5  lemma mem_prs[quot_preserve]:
     3.6    assumes "Quotient R Abs Rep"
     3.7 -  shows "(Rep ---> (Abs ---> id) ---> id) (op \<in>) = op \<in>"
     3.8 -using Quotient_abs_rep[OF assms]
     3.9 -by(simp add: fun_eq_iff mem_def)
    3.10 -
    3.11 -lemma mem_rsp[quot_respect]:
    3.12 -  "(R ===> (R ===> op =) ===> op =) (op \<in>) (op \<in>)"
    3.13 -  by (auto simp add: fun_eq_iff mem_def intro!: fun_relI elim: fun_relE)
    3.14 -
    3.15 -lemma mem_prs2:
    3.16 -  assumes "Quotient R Abs Rep"
    3.17    shows "(Rep ---> op -` Abs ---> id) op \<in> = op \<in>"
    3.18    by (simp add: fun_eq_iff Quotient_abs_rep[OF assms])
    3.19  
    3.20 -lemma mem_rsp2:
    3.21 +lemma mem_rsp[quot_respect]:
    3.22    shows "(R ===> set_rel R ===> op =) op \<in> op \<in>"
    3.23    by (intro fun_relI) (simp add: set_rel_def)
    3.24  
     4.1 --- a/src/HOL/Metis_Examples/Message.thy	Sat Dec 24 15:53:10 2011 +0100
     4.2 +++ b/src/HOL/Metis_Examples/Message.thy	Sat Dec 24 15:53:10 2011 +0100
     4.3 @@ -245,8 +245,9 @@
     4.4  lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
     4.5  by (blast dest: parts_mono)
     4.6  
     4.7 -lemma parts_cut: "[|Y\<in> parts (insert X G);  X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
     4.8 -by (metis Un_insert_left Un_insert_right insert_absorb mem_def parts_Un parts_idem sup1CI)
     4.9 +(*lemma parts_cut: "[|Y\<in> parts (insert X G);  X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
    4.10 +by (metis UnI2 insert_subset le_supE parts_Un_subset1 parts_increasing parts_trans subsetD)
    4.11 +by (metis Un_insert_left Un_insert_right insert_absorb parts_Un parts_idem sup1CI)*)
    4.12  
    4.13  
    4.14  subsubsection{*Rewrite rules for pulling out atomic messages *}
    4.15 @@ -677,8 +678,8 @@
    4.16  apply (rule subsetI)
    4.17  apply (erule analz.induct)
    4.18  apply (metis UnCI UnE Un_commute analz.Inj)
    4.19 -apply (metis MPair_synth UnCI UnE Un_commute analz.Fst analz.Inj mem_def)
    4.20 -apply (metis MPair_synth UnCI UnE Un_commute analz.Inj analz.Snd mem_def)
    4.21 +apply (metis MPair_synth UnCI UnE Un_commute analz.Fst analz.Inj)
    4.22 +apply (metis MPair_synth UnCI UnE Un_commute analz.Inj analz.Snd)
    4.23  apply (blast intro: analz.Decrypt)
    4.24  apply blast
    4.25  done
    4.26 @@ -695,13 +696,11 @@
    4.27  
    4.28  subsubsection{*For reasoning about the Fake rule in traces *}
    4.29  
    4.30 -lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
    4.31 +lemma parts_insert_subset_Un: "X \<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
    4.32  proof -
    4.33    assume "X \<in> G"
    4.34 -  hence "G X" by (metis mem_def)
    4.35 -  hence "\<forall>x\<^isub>1. G \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 X" by (metis predicate1D)
    4.36 -  hence "\<forall>x\<^isub>1. (G \<union> x\<^isub>1) X" by (metis Un_upper1)
    4.37 -  hence "\<forall>x\<^isub>1. X \<in> G \<union> x\<^isub>1" by (metis mem_def)
    4.38 +  hence "\<forall>x\<^isub>1. G \<subseteq> x\<^isub>1 \<longrightarrow> X \<in> x\<^isub>1 " by auto
    4.39 +  hence "\<forall>x\<^isub>1. X \<in> G \<union> x\<^isub>1" by (metis Un_upper1)
    4.40    hence "insert X H \<subseteq> G \<union> H" by (metis Un_upper2 insert_subset)
    4.41    hence "parts (insert X H) \<subseteq> parts (G \<union> H)" by (metis parts_mono)
    4.42    thus "parts (insert X H) \<subseteq> parts G \<union> parts H" by (metis parts_Un)
    4.43 @@ -716,10 +715,10 @@
    4.44      by (metis analz_idem analz_synth)
    4.45    have F2: "\<forall>x\<^isub>1. parts x\<^isub>1 \<union> synth (analz x\<^isub>1) = parts (synth (analz x\<^isub>1))"
    4.46      by (metis parts_analz parts_synth)
    4.47 -  have F3: "synth (analz H) X" using A1 by (metis mem_def)
    4.48 +  have F3: "X \<in> synth (analz H)" using A1 by metis
    4.49    have "\<forall>x\<^isub>2 x\<^isub>1\<Colon>msg set. x\<^isub>1 \<le> sup x\<^isub>1 x\<^isub>2" by (metis inf_sup_ord(3))
    4.50    hence F4: "\<forall>x\<^isub>1. analz x\<^isub>1 \<subseteq> analz (synth x\<^isub>1)" by (metis analz_synth)
    4.51 -  have F5: "X \<in> synth (analz H)" using F3 by (metis mem_def)
    4.52 +  have F5: "X \<in> synth (analz H)" using F3 by metis
    4.53    have "\<forall>x\<^isub>1. analz x\<^isub>1 \<subseteq> synth (analz x\<^isub>1)
    4.54           \<longrightarrow> analz (synth (analz x\<^isub>1)) = synth (analz x\<^isub>1)"
    4.55      using F1 by (metis subset_Un_eq)
    4.56 @@ -741,7 +740,7 @@
    4.57        ==> Z \<in>  synth (analz H) \<union> parts H"
    4.58  by (blast dest: Fake_parts_insert [THEN subsetD, dest])
    4.59  
    4.60 -declare analz_mono [intro] synth_mono [intro]
    4.61 +declare synth_mono [intro]
    4.62  
    4.63  lemma Fake_analz_insert:
    4.64       "X \<in> synth (analz G) ==>
     5.1 --- a/src/HOL/Metis_Examples/Proxies.thy	Sat Dec 24 15:53:10 2011 +0100
     5.2 +++ b/src/HOL/Metis_Examples/Proxies.thy	Sat Dec 24 15:53:10 2011 +0100
     5.3 @@ -41,7 +41,7 @@
     5.4  
     5.5  lemma "xs \<in> A"
     5.6  sledgehammer [expect = some]
     5.7 -by (metis_exhaust A_def Collect_def mem_def)
     5.8 +by (metis_exhaust A_def mem_Collect_eq)
     5.9  
    5.10  definition "B (y::int) \<equiv> y \<le> 0"
    5.11  definition "C (y::int) \<equiv> y \<le> 1"
    5.12 @@ -49,7 +49,7 @@
    5.13  lemma int_le_0_imp_le_1: "x \<le> (0::int) \<Longrightarrow> x \<le> 1"
    5.14  by linarith
    5.15  
    5.16 -lemma "B \<subseteq> C"
    5.17 +lemma "B \<le> C"
    5.18  sledgehammer [type_enc = poly_args, max_relevant = 100, expect = some]
    5.19  by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)
    5.20  
    5.21 @@ -151,7 +151,7 @@
    5.22  sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
    5.23  sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
    5.24  sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
    5.25 -by (metis_exhaust id_apply)
    5.26 +by metis_exhaust
    5.27  
    5.28  lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
    5.29  sledgehammer [type_enc = erased, expect = some] (id_apply)
     6.1 --- a/src/HOL/Metis_Examples/Tarski.thy	Sat Dec 24 15:53:10 2011 +0100
     6.2 +++ b/src/HOL/Metis_Examples/Tarski.thy	Sat Dec 24 15:53:10 2011 +0100
     6.3 @@ -196,8 +196,7 @@
     6.4  
     6.5  lemma (in PO) dualPO: "dual cl \<in> PartialOrder"
     6.6  apply (insert cl_po)
     6.7 -apply (simp add: PartialOrder_def dual_def refl_on_converse
     6.8 -                 trans_converse antisym_converse)
     6.9 +apply (simp add: PartialOrder_def dual_def)
    6.10  done
    6.11  
    6.12  lemma Rdual:
    6.13 @@ -519,22 +518,22 @@
    6.14    thus "lub {x. (x, f x) \<in> r \<and> x \<in> A} cl \<in> A" using A1 by metis
    6.15  next
    6.16    assume A1: "H = {x. (x, f x) \<in> r \<and> x \<in> A}"
    6.17 -  have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
    6.18 -  have F2: "\<forall>w u. (\<lambda>R. u R \<and> w R) = u \<inter> w"
    6.19 -    by (metis Collect_conj_eq Collect_def)
    6.20 -  have F3: "\<forall>x v. (\<lambda>R. v R \<in> x) = v -` x" by (metis vimage_def Collect_def)
    6.21 +  have F1: "\<forall>v. {R. R \<in> v} = v" by (metis Collect_mem_eq)
    6.22 +  have F2: "\<forall>w u. {R. R \<in> u \<and> R \<in> w} = u \<inter> w"
    6.23 +    by (metis Collect_conj_eq Collect_mem_eq)
    6.24 +  have F3: "\<forall>x v. {R. v R \<in> x} = v -` x" by (metis vimage_def)
    6.25    hence F4: "A \<inter> (\<lambda>R. (R, f R)) -` r = H" using A1 by auto
    6.26 -  hence F5: "(f (lub H cl), lub H cl) \<in> r"
    6.27 -    by (metis F1 F3 F2 Int_commute flubH_le_lubH Collect_def)
    6.28 +  hence F5: "(f (lub H cl), lub H cl) \<in> r" 
    6.29 +    by (metis A1 flubH_le_lubH)
    6.30    have F6: "(lub H cl, f (lub H cl)) \<in> r"
    6.31 -    by (metis F1 F3 F2 F4 Int_commute lubH_le_flubH Collect_def)
    6.32 +    by (metis A1 lubH_le_flubH)
    6.33    have "(lub H cl, f (lub H cl)) \<in> r \<longrightarrow> f (lub H cl) = lub H cl"
    6.34      using F5 by (metis antisymE)
    6.35    hence "f (lub H cl) = lub H cl" using F6 by metis
    6.36    thus "H = {x. (x, f x) \<in> r \<and> x \<in> A}
    6.37          \<Longrightarrow> f (lub {x. (x, f x) \<in> r \<and> x \<in> A} cl) =
    6.38             lub {x. (x, f x) \<in> r \<and> x \<in> A} cl"
    6.39 -    by (metis F4 F2 F3 F1 Collect_def Int_commute)
    6.40 +    by metis
    6.41  qed
    6.42  
    6.43  lemma (in CLF) (*lubH_is_fixp:*)
     7.1 --- a/src/HOL/Metis_Examples/Trans_Closure.thy	Sat Dec 24 15:53:10 2011 +0100
     7.2 +++ b/src/HOL/Metis_Examples/Trans_Closure.thy	Sat Dec 24 15:53:10 2011 +0100
     7.3 @@ -50,11 +50,9 @@
     7.4    assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
     7.5    assume A3: "(a, b) \<in> R\<^sup>*"
     7.6    assume A4: "(b, c) \<in> R\<^sup>*"
     7.7 -  have "(R\<^sup>*) (a, b)" using A3 by (metis mem_def)
     7.8 -  hence F1: "(a, b) \<in> R\<^sup>*" by (metis mem_def)
     7.9    have "b \<noteq> c" using A1 A2 by metis
    7.10    hence "\<exists>x\<^isub>1. (b, x\<^isub>1) \<in> R" using A4 by (metis converse_rtranclE)
    7.11 -  thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F1 by (metis transitive_closure_trans(6))
    7.12 +  thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using A3 by (metis transitive_closure_trans(6))
    7.13  qed
    7.14  
    7.15  lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b, c) \<in> R\<^sup>*\<rbrakk>
     8.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Sat Dec 24 15:53:10 2011 +0100
     8.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Sat Dec 24 15:53:10 2011 +0100
     8.3 @@ -452,7 +452,7 @@
     8.4  qed
     8.5  
     8.6  lemma [code]:
     8.7 -  "iter f step ss w = while (\<lambda>(ss, w). \<not> is_empty w)
     8.8 +  "iter f step ss w = while (\<lambda>(ss, w). \<not> More_Set.is_empty w)
     8.9      (\<lambda>(ss, w).
    8.10          let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p}))
    8.11      (ss, w)"
    8.12 @@ -478,12 +478,8 @@
    8.13    #> Code.add_signature_cmd ("unstables", "('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list) \<Rightarrow> 's list \<Rightarrow> nat set") 
    8.14  *}
    8.15  
    8.16 -definition [code del]: "mem2 = op :"
    8.17 -lemma [code]: "mem2 x A = A x"
    8.18 -  by(simp add: mem2_def mem_def)
    8.19 -
    8.20 -lemmas [folded mem2_def, code] =
    8.21 -  JType.sup_def[unfolded exec_lub_def]
    8.22 +lemmas [code] =
    8.23 +  JType.sup_def [unfolded exec_lub_def]
    8.24    wf_class_code
    8.25    widen.equation
    8.26    match_exception_entry_def
     9.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Sat Dec 24 15:53:10 2011 +0100
     9.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Sat Dec 24 15:53:10 2011 +0100
     9.3 @@ -4,7 +4,9 @@
     9.4  
     9.5  header {* \isaheader{Relations between Java Types} *}
     9.6  
     9.7 -theory TypeRel imports Decl "~~/src/HOL/Library/Wfrec" begin
     9.8 +theory TypeRel
     9.9 +imports Decl "~~/src/HOL/Library/Wfrec"
    9.10 +begin
    9.11  
    9.12  -- "direct subclass, cf. 8.1.3"
    9.13  
    9.14 @@ -84,7 +86,9 @@
    9.15    (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool)
    9.16    subcls1p 
    9.17    .
    9.18 -declare subcls1_def[unfolded Collect_def, code_pred_def]
    9.19 +
    9.20 +declare subcls1_def [code_pred_def]
    9.21 +
    9.22  code_pred 
    9.23    (modes: i \<Rightarrow> i \<times> o \<Rightarrow> bool, i \<Rightarrow> i \<times> i \<Rightarrow> bool)
    9.24    [inductify]
    9.25 @@ -92,14 +96,16 @@
    9.26    .
    9.27  
    9.28  definition subcls' where "subcls' G = (subcls1p G)^**"
    9.29 +
    9.30  code_pred
    9.31    (modes: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool)
    9.32    [inductify]
    9.33    subcls'
    9.34 -.
    9.35 +  .
    9.36 +
    9.37  lemma subcls_conv_subcls' [code_unfold]:
    9.38 -  "(subcls1 G)^* = (\<lambda>(C, D). subcls' G C D)"
    9.39 -by(simp add: subcls'_def subcls1_def rtrancl_def)(simp add: Collect_def)
    9.40 +  "(subcls1 G)^* = {(C, D). subcls' G C D}"
    9.41 +by(simp add: subcls'_def subcls1_def rtrancl_def)
    9.42  
    9.43  lemma class_rec_code [code]:
    9.44    "class_rec G C t f = 
    9.45 @@ -190,7 +196,7 @@
    9.46    map_of (map (\<lambda>(s,m). (s,(C,m))) ms)"
    9.47  apply (unfold method_def)
    9.48  apply (simp split del: split_if)
    9.49 -apply (erule (1) class_rec_lemma [THEN trans]);
    9.50 +apply (erule (1) class_rec_lemma [THEN trans])
    9.51  apply auto
    9.52  done
    9.53  
    9.54 @@ -204,7 +210,7 @@
    9.55    map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))"
    9.56  apply (unfold fields_def)
    9.57  apply (simp split del: split_if)
    9.58 -apply (erule (1) class_rec_lemma [THEN trans]);
    9.59 +apply (erule (1) class_rec_lemma [THEN trans])
    9.60  apply auto
    9.61  done
    9.62  
    10.1 --- a/src/HOL/Nitpick.thy	Sat Dec 24 15:53:10 2011 +0100
    10.2 +++ b/src/HOL/Nitpick.thy	Sat Dec 24 15:53:10 2011 +0100
    10.3 @@ -50,7 +50,7 @@
    10.4  *}
    10.5  
    10.6  lemma Ex1_unfold [nitpick_unfold, no_atp]:
    10.7 -"Ex1 P \<equiv> \<exists>x. P = {x}"
    10.8 +"Ex1 P \<equiv> \<exists>x. {x. P x} = {x}"
    10.9  apply (rule eq_reflection)
   10.10  apply (simp add: Ex1_def set_eq_iff)
   10.11  apply (rule iffI)
   10.12 @@ -60,7 +60,7 @@
   10.13   apply (rule allI)
   10.14   apply (rename_tac y)
   10.15   apply (erule_tac x = y in allE)
   10.16 -by (auto simp: mem_def)
   10.17 +by auto
   10.18  
   10.19  lemma rtrancl_unfold [nitpick_unfold, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
   10.20    by (simp only: rtrancl_trancl_reflcl)
   10.21 @@ -70,8 +70,8 @@
   10.22  by (rule eq_reflection) (auto dest: rtranclpD)
   10.23  
   10.24  lemma tranclp_unfold [nitpick_unfold, no_atp]:
   10.25 -"tranclp r a b \<equiv> trancl (split r) (a, b)"
   10.26 -by (simp add: trancl_def Collect_def mem_def)
   10.27 +"tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
   10.28 +by (simp add: trancl_def)
   10.29  
   10.30  definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
   10.31  "prod A B = {(a, b). a \<in> A \<and> b \<in> B}"
   10.32 @@ -98,8 +98,8 @@
   10.33  *}
   10.34  
   10.35  lemma The_psimp [nitpick_psimp, no_atp]:
   10.36 -"P = {x} \<Longrightarrow> The P = x"
   10.37 -by (subgoal_tac "{x} = (\<lambda>y. y = x)") (auto simp: mem_def)
   10.38 +  "P = (op =) x \<Longrightarrow> The P = x"
   10.39 +  by auto
   10.40  
   10.41  lemma Eps_psimp [nitpick_psimp, no_atp]:
   10.42  "\<lbrakk>P x; \<not> P y; Eps P = y\<rbrakk> \<Longrightarrow> Eps P = x"
    11.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Sat Dec 24 15:53:10 2011 +0100
    11.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Sat Dec 24 15:53:10 2011 +0100
    11.3 @@ -75,15 +75,15 @@
    11.4  nitpick [card = 1\<emdash>4, expect = none]
    11.5  by auto
    11.6  
    11.7 -lemma "Id (a, a)"
    11.8 +lemma "(a, a) \<in> Id"
    11.9  nitpick [card = 1\<emdash>50, expect = none]
   11.10 -by (auto simp: Id_def Collect_def)
   11.11 +by (auto simp: Id_def)
   11.12  
   11.13 -lemma "Id ((a\<Colon>'a, b\<Colon>'a), (a, b))"
   11.14 +lemma "((a\<Colon>'a, b\<Colon>'a), (a, b)) \<in> Id"
   11.15  nitpick [card = 1\<emdash>10, expect = none]
   11.16 -by (auto simp: Id_def Collect_def)
   11.17 +by (auto simp: Id_def)
   11.18  
   11.19 -lemma "UNIV (x\<Colon>'a\<times>'a)"
   11.20 +lemma "(x\<Colon>'a\<times>'a) \<in> UNIV"
   11.21  nitpick [card = 1\<emdash>50, expect = none]
   11.22  sorry
   11.23  
   11.24 @@ -539,13 +539,13 @@
   11.25  nitpick [expect = none]
   11.26  by auto
   11.27  
   11.28 -lemma "I = (\<lambda>x. x) \<Longrightarrow> Id = (\<lambda>x. Id (I x))"
   11.29 +lemma "I = (\<lambda>x. x) \<Longrightarrow> Id = {x. I x \<in> Id}"
   11.30  nitpick [expect = none]
   11.31  by auto
   11.32  
   11.33 -lemma "{} = (\<lambda>x. False)"
   11.34 +lemma "{} = {x. False}"
   11.35  nitpick [expect = none]
   11.36 -by (metis Collect_def empty_def)
   11.37 +by (metis empty_def)
   11.38  
   11.39  lemma "x \<in> {}"
   11.40  nitpick [expect = genuine]
   11.41 @@ -571,33 +571,23 @@
   11.42  nitpick [expect = none]
   11.43  by auto
   11.44  
   11.45 -lemma "UNIV = (\<lambda>x. True)"
   11.46 +lemma "UNIV = {x. True}"
   11.47  nitpick [expect = none]
   11.48 -by (simp only: UNIV_def Collect_def)
   11.49 +by (simp only: UNIV_def)
   11.50  
   11.51 -lemma "UNIV x = True"
   11.52 +lemma "x \<in> UNIV \<longleftrightarrow> True"
   11.53  nitpick [expect = none]
   11.54 -by (simp only: UNIV_def Collect_def)
   11.55 +by (simp only: UNIV_def mem_Collect_eq)
   11.56  
   11.57  lemma "x \<notin> UNIV"
   11.58  nitpick [expect = genuine]
   11.59  oops
   11.60  
   11.61 -lemma "op \<in> = (\<lambda>x P. P x)"
   11.62 -nitpick [expect = none]
   11.63 -apply (rule ext)
   11.64 -apply (rule ext)
   11.65 -by (simp add: mem_def)
   11.66 -
   11.67  lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<in> = (\<lambda>x. (op \<in> (I x)))"
   11.68  nitpick [expect = none]
   11.69  apply (rule ext)
   11.70  apply (rule ext)
   11.71 -by (simp add: mem_def)
   11.72 -
   11.73 -lemma "P x = (x \<in> P)"
   11.74 -nitpick [expect = none]
   11.75 -by (simp add: mem_def)
   11.76 +by simp
   11.77  
   11.78  lemma "insert = (\<lambda>x y. insert x (y \<union> y))"
   11.79  nitpick [expect = none]
   11.80 @@ -753,7 +743,7 @@
   11.81  nitpick [expect = genuine]
   11.82  oops
   11.83  
   11.84 -lemma "(P\<Colon>nat set) (Eps P)"
   11.85 +lemma "Eps (\<lambda>x. x \<in> P) \<in> (P\<Colon>nat set)"
   11.86  nitpick [expect = genuine]
   11.87  oops
   11.88  
   11.89 @@ -761,15 +751,15 @@
   11.90  nitpick [expect = genuine]
   11.91  oops
   11.92  
   11.93 -lemma "\<not> (P\<Colon>nat set) (Eps P)"
   11.94 +lemma "\<not> (P \<Colon> nat \<Rightarrow> bool) (Eps P)"
   11.95  nitpick [expect = genuine]
   11.96  oops
   11.97  
   11.98 -lemma "P \<noteq> {} \<Longrightarrow> P (Eps P)"
   11.99 +lemma "P \<noteq> bot \<Longrightarrow> P (Eps P)"
  11.100  nitpick [expect = none]
  11.101  sorry
  11.102  
  11.103 -lemma "(P\<Colon>nat set) \<noteq> {} \<Longrightarrow> P (Eps P)"
  11.104 +lemma "(P \<Colon> nat \<Rightarrow> bool) \<noteq> bot \<Longrightarrow> P (Eps P)"
  11.105  nitpick [expect = none]
  11.106  sorry
  11.107  
  11.108 @@ -777,7 +767,7 @@
  11.109  nitpick [expect = genuine]
  11.110  oops
  11.111  
  11.112 -lemma "(P\<Colon>nat set) (The P)"
  11.113 +lemma "(P \<Colon> nat \<Rightarrow> bool) (The P)"
  11.114  nitpick [expect = genuine]
  11.115  oops
  11.116  
  11.117 @@ -785,7 +775,7 @@
  11.118  nitpick [expect = genuine]
  11.119  oops
  11.120  
  11.121 -lemma "\<not> (P\<Colon>nat set) (The P)"
  11.122 +lemma "\<not> (P \<Colon> nat \<Rightarrow> bool) (The P)"
  11.123  nitpick [expect = genuine]
  11.124  oops
  11.125  
  11.126 @@ -805,11 +795,11 @@
  11.127  nitpick [expect = genuine]
  11.128  oops
  11.129  
  11.130 -lemma "P = {x} \<Longrightarrow> P (The P)"
  11.131 +lemma "P = {x} \<Longrightarrow> (THE x. x \<in> P) \<in> P"
  11.132  nitpick [expect = none]
  11.133  oops
  11.134  
  11.135 -lemma "P = {x\<Colon>nat} \<Longrightarrow> P (The P)"
  11.136 +lemma "P = {x\<Colon>nat} \<Longrightarrow> (THE x. x \<in> P) \<in> P"
  11.137  nitpick [expect = none]
  11.138  oops
  11.139  
  11.140 @@ -819,23 +809,23 @@
  11.141  nitpick [expect = genuine]
  11.142  oops
  11.143  
  11.144 -lemma "(Q\<Colon>nat set) (Eps Q)"
  11.145 +lemma "(Q \<Colon> nat \<Rightarrow> bool) (Eps Q)"
  11.146  nitpick [expect = none] (* unfortunate *)
  11.147  oops
  11.148  
  11.149 -lemma "\<not> Q (Eps Q)"
  11.150 +lemma "\<not> (Q \<Colon> nat \<Rightarrow> bool) (Eps Q)"
  11.151  nitpick [expect = genuine]
  11.152  oops
  11.153  
  11.154 -lemma "\<not> (Q\<Colon>nat set) (Eps Q)"
  11.155 +lemma "\<not> (Q \<Colon> nat \<Rightarrow> bool) (Eps Q)"
  11.156  nitpick [expect = genuine]
  11.157  oops
  11.158  
  11.159 -lemma "(Q\<Colon>'a set) \<noteq> {} \<Longrightarrow> (Q\<Colon>'a set) (Eps Q)"
  11.160 +lemma "(Q \<Colon> 'a \<Rightarrow> bool) \<noteq> bot \<Longrightarrow> Q (Eps Q)"
  11.161  nitpick [expect = none]
  11.162  sorry
  11.163  
  11.164 -lemma "(Q\<Colon>nat set) \<noteq> {} \<Longrightarrow> (Q\<Colon>nat set) (Eps Q)"
  11.165 +lemma "(Q \<Colon> nat \<Rightarrow> bool) \<noteq> top \<Longrightarrow> Q (Eps Q)"
  11.166  nitpick [expect = none]
  11.167  sorry
  11.168  
  11.169 @@ -843,7 +833,7 @@
  11.170  nitpick [expect = genuine]
  11.171  oops
  11.172  
  11.173 -lemma "(Q\<Colon>nat set) (The Q)"
  11.174 +lemma "(Q \<Colon> nat \<Rightarrow> bool) (The Q)"
  11.175  nitpick [expect = genuine]
  11.176  oops
  11.177  
  11.178 @@ -851,7 +841,7 @@
  11.179  nitpick [expect = genuine]
  11.180  oops
  11.181  
  11.182 -lemma "\<not> (Q\<Colon>nat set) (The Q)"
  11.183 +lemma "\<not> (Q \<Colon> nat \<Rightarrow> bool) (The Q)"
  11.184  nitpick [expect = genuine]
  11.185  oops
  11.186  
  11.187 @@ -871,11 +861,11 @@
  11.188  nitpick [expect = genuine]
  11.189  oops
  11.190  
  11.191 -lemma "Q = {x\<Colon>'a} \<Longrightarrow> (Q\<Colon>'a set) (The Q)"
  11.192 +lemma "Q = {x\<Colon>'a} \<Longrightarrow> (The Q) \<in> (Q\<Colon>'a set)"
  11.193  nitpick [expect = none]
  11.194  sorry
  11.195  
  11.196 -lemma "Q = {x\<Colon>nat} \<Longrightarrow> (Q\<Colon>nat set) (The Q)"
  11.197 +lemma "Q = {x\<Colon>nat} \<Longrightarrow> (The Q) \<in> (Q\<Colon>nat set)"
  11.198  nitpick [expect = none]
  11.199  sorry
  11.200  
    12.1 --- a/src/HOL/Nitpick_Examples/Induct_Nits.thy	Sat Dec 24 15:53:10 2011 +0100
    12.2 +++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy	Sat Dec 24 15:53:10 2011 +0100
    12.3 @@ -54,23 +54,23 @@
    12.4  coinductive q2 :: "nat \<Rightarrow> bool" where
    12.5  "q2 n \<Longrightarrow> q2 n"
    12.6  
    12.7 -lemma "p2 = {}"
    12.8 +lemma "p2 = bot"
    12.9  nitpick [expect = none]
   12.10  nitpick [dont_star_linear_preds, expect = none]
   12.11  sorry
   12.12  
   12.13 -lemma "q2 = {}"
   12.14 +lemma "q2 = bot"
   12.15  nitpick [expect = genuine]
   12.16  nitpick [dont_star_linear_preds, expect = genuine]
   12.17  nitpick [wf, expect = quasi_genuine]
   12.18  oops
   12.19  
   12.20 -lemma "p2 = UNIV"
   12.21 +lemma "p2 = top"
   12.22  nitpick [expect = genuine]
   12.23  nitpick [dont_star_linear_preds, expect = genuine]
   12.24  oops
   12.25  
   12.26 -lemma "q2 = UNIV"
   12.27 +lemma "q2 = top"
   12.28  nitpick [expect = none]
   12.29  nitpick [dont_star_linear_preds, expect = none]
   12.30  nitpick [wf, expect = quasi_genuine]
   12.31 @@ -123,32 +123,32 @@
   12.32  nitpick [non_wf, expect = none]
   12.33  sorry
   12.34  
   12.35 -lemma "p3 = UNIV - p4"
   12.36 +lemma "p3 = top - p4"
   12.37  nitpick [expect = none]
   12.38  nitpick [non_wf, expect = none]
   12.39  sorry
   12.40  
   12.41 -lemma "q3 = UNIV - q4"
   12.42 +lemma "q3 = top - q4"
   12.43  nitpick [expect = none]
   12.44  nitpick [non_wf, expect = none]
   12.45  sorry
   12.46  
   12.47 -lemma "p3 \<inter> q4 \<noteq> {}"
   12.48 +lemma "inf p3 q4 \<noteq> bot"
   12.49  nitpick [expect = potential]
   12.50  nitpick [non_wf, expect = potential]
   12.51  sorry
   12.52  
   12.53 -lemma "q3 \<inter> p4 \<noteq> {}"
   12.54 +lemma "inf q3 p4 \<noteq> bot"
   12.55  nitpick [expect = potential]
   12.56  nitpick [non_wf, expect = potential]
   12.57  sorry
   12.58  
   12.59 -lemma "p3 \<union> q4 \<noteq> UNIV"
   12.60 +lemma "sup p3 q4 \<noteq> top"
   12.61  nitpick [expect = potential]
   12.62  nitpick [non_wf, expect = potential]
   12.63  sorry
   12.64  
   12.65 -lemma "q3 \<union> p4 \<noteq> UNIV"
   12.66 +lemma "sup q3 p4 \<noteq> top"
   12.67  nitpick [expect = potential]
   12.68  nitpick [non_wf, expect = potential]
   12.69  sorry
    13.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Sat Dec 24 15:53:10 2011 +0100
    13.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Sat Dec 24 15:53:10 2011 +0100
    13.3 @@ -179,7 +179,7 @@
    13.4  coinductive nats where
    13.5  "nats (x\<Colon>nat) \<Longrightarrow> nats x"
    13.6  
    13.7 -lemma "nats = {0, 1, 2, 3, 4}"
    13.8 +lemma "nats = (\<lambda>n. n \<in> {0, 1, 2, 3, 4})"
    13.9  nitpick [card nat = 10, show_consts, expect = genuine]
   13.10  oops
   13.11  
    14.1 --- a/src/HOL/Nitpick_Examples/Mini_Nits.thy	Sat Dec 24 15:53:10 2011 +0100
    14.2 +++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy	Sat Dec 24 15:53:10 2011 +0100
    14.3 @@ -68,13 +68,13 @@
    14.4  ML {* genuine 1 @{prop "{a} \<noteq> {a, b}"} *}
    14.5  ML {* none 5 @{prop "{}\<^sup>+ = {}"} *}
    14.6  ML {* none 5 @{prop "UNIV\<^sup>+ = UNIV"} *}
    14.7 -ML {* none 5 @{prop "(UNIV\<Colon>'a \<times> 'b \<Rightarrow> bool) - {} = UNIV"} *}
    14.8 -ML {* none 5 @{prop "{} - (UNIV\<Colon>'a \<times> 'b \<Rightarrow> bool) = {}"} *}
    14.9 +ML {* none 5 @{prop "(UNIV \<Colon> ('a \<times> 'b) set) - {} = UNIV"} *}
   14.10 +ML {* none 5 @{prop "{} - (UNIV \<Colon> ('a \<times> 'b) set) = {}"} *}
   14.11  ML {* none 1 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
   14.12  ML {* genuine 2 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
   14.13  ML {* none 5 @{prop "a \<noteq> c \<Longrightarrow> {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
   14.14 -ML {* none 5 @{prop "A \<union> B = (\<lambda>x. A x \<or> B x)"} *}
   14.15 -ML {* none 5 @{prop "A \<inter> B = (\<lambda>x. A x \<and> B x)"} *}
   14.16 +ML {* none 5 @{prop "A \<union> B = {x. x \<in> A \<or> x \<in> B}"} *}
   14.17 +ML {* none 5 @{prop "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"} *}
   14.18  ML {* none 5 @{prop "A - B = (\<lambda>x. A x \<and> \<not> B x)"} *}
   14.19  ML {* none 5 @{prop "\<exists>a b. (a, b) = (b, a)"} *}
   14.20  ML {* genuine 2 @{prop "(a, b) = (b, a)"} *}
    15.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Sat Dec 24 15:53:10 2011 +0100
    15.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Sat Dec 24 15:53:10 2011 +0100
    15.3 @@ -52,7 +52,8 @@
    15.4  nitpick [card = 2, expect = none]
    15.5  oops
    15.6  
    15.7 -definition "bounded = {n\<Colon>nat. finite (UNIV\<Colon>'a \<Rightarrow> bool) \<longrightarrow> n < card (UNIV\<Colon>'a \<Rightarrow> bool)}"
    15.8 +definition "bounded = {n\<Colon>nat. finite (UNIV \<Colon> 'a set) \<longrightarrow> n < card (UNIV \<Colon> 'a set)}"
    15.9 +
   15.10  typedef (open) 'a bounded = "bounded(TYPE('a))"
   15.11  unfolding bounded_def
   15.12  apply (rule_tac x = 0 in exI)
    16.1 --- a/src/HOL/Predicate.thy	Sat Dec 24 15:53:10 2011 +0100
    16.2 +++ b/src/HOL/Predicate.thy	Sat Dec 24 15:53:10 2011 +0100
    16.3 @@ -74,19 +74,19 @@
    16.4  subsubsection {* Equality *}
    16.5  
    16.6  lemma pred_equals_eq: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)"
    16.7 -  by (simp add: set_eq_iff fun_eq_iff mem_def)
    16.8 +  by (simp add: set_eq_iff fun_eq_iff)
    16.9  
   16.10  lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R = S)"
   16.11 -  by (simp add: set_eq_iff fun_eq_iff mem_def)
   16.12 +  by (simp add: set_eq_iff fun_eq_iff)
   16.13  
   16.14  
   16.15  subsubsection {* Order relation *}
   16.16  
   16.17  lemma pred_subset_eq: "((\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
   16.18 -  by (simp add: subset_iff le_fun_def mem_def)
   16.19 +  by (simp add: subset_iff le_fun_def)
   16.20  
   16.21  lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) \<le> (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
   16.22 -  by (simp add: subset_iff le_fun_def mem_def)
   16.23 +  by (simp add: subset_iff le_fun_def)
   16.24  
   16.25  
   16.26  subsubsection {* Top and bottom elements *}
   16.27 @@ -137,10 +137,10 @@
   16.28    by (simp add: inf_fun_def)
   16.29  
   16.30  lemma inf_Int_eq: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
   16.31 -  by (simp add: inf_fun_def mem_def)
   16.32 +  by (simp add: inf_fun_def)
   16.33  
   16.34  lemma inf_Int_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<sqinter> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
   16.35 -  by (simp add: inf_fun_def mem_def)
   16.36 +  by (simp add: inf_fun_def)
   16.37  
   16.38  
   16.39  subsubsection {* Binary union *}
   16.40 @@ -175,10 +175,10 @@
   16.41    by (auto simp add: sup_fun_def)
   16.42  
   16.43  lemma sup_Un_eq: "(\<lambda>x. x \<in> R) \<squnion> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
   16.44 -  by (simp add: sup_fun_def mem_def)
   16.45 +  by (simp add: sup_fun_def)
   16.46  
   16.47  lemma sup_Un_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<squnion> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
   16.48 -  by (simp add: sup_fun_def mem_def)
   16.49 +  by (simp add: sup_fun_def)
   16.50  
   16.51  
   16.52  subsubsection {* Intersections of families *}
   16.53 @@ -578,8 +578,8 @@
   16.54  lemma not_bot:
   16.55    assumes "A \<noteq> \<bottom>"
   16.56    obtains x where "eval A x"
   16.57 -  using assms by (cases A) (auto simp add: bot_pred_def, simp add: mem_def)
   16.58 -  
   16.59 +  using assms by (cases A) (auto simp add: bot_pred_def)
   16.60 +
   16.61  
   16.62  subsubsection {* Emptiness check and definite choice *}
   16.63  
   16.64 @@ -1017,14 +1017,6 @@
   16.65  end;
   16.66  *}
   16.67  
   16.68 -lemma eval_mem [simp]:
   16.69 -  "x \<in> eval P \<longleftrightarrow> eval P x"
   16.70 -  by (simp add: mem_def)
   16.71 -
   16.72 -lemma eq_mem [simp]:
   16.73 -  "x \<in> (op =) y \<longleftrightarrow> x = y"
   16.74 -  by (auto simp add: mem_def)
   16.75 -
   16.76  no_notation
   16.77    bot ("\<bottom>") and
   16.78    top ("\<top>") and
    17.1 --- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Sat Dec 24 15:53:10 2011 +0100
    17.2 +++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Sat Dec 24 15:53:10 2011 +0100
    17.3 @@ -1,9 +1,9 @@
    17.4  theory Context_Free_Grammar_Example
    17.5  imports "~~/src/HOL/Library/Code_Prolog"
    17.6  begin
    17.7 -
    17.8 +(*
    17.9  declare mem_def[code_pred_inline]
   17.10 -
   17.11 +*)
   17.12  
   17.13  subsection {* Alternative rules for length *}
   17.14  
   17.15 @@ -32,7 +32,7 @@
   17.16  | "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
   17.17  
   17.18  lemma
   17.19 -  "w \<in> S\<^isub>1 \<Longrightarrow> w = []"
   17.20 +  "S\<^isub>1p w \<Longrightarrow> w = []"
   17.21  quickcheck[tester = prolog, iterations=1, expect = counterexample]
   17.22  oops
   17.23  
   17.24 @@ -60,13 +60,13 @@
   17.25    {ensure_groundness = true,
   17.26    limit_globally = NONE,
   17.27    limited_types = [],
   17.28 -  limited_predicates = [(["s1", "a1", "b1"], 2)],
   17.29 -  replacing = [(("s1", "limited_s1"), "quickcheck")],
   17.30 +  limited_predicates = [(["s1p", "a1p", "b1p"], 2)],
   17.31 +  replacing = [(("s1p", "limited_s1p"), "quickcheck")],
   17.32    manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
   17.33  
   17.34  
   17.35  theorem S\<^isub>1_sound:
   17.36 -"w \<in> S\<^isub>1 \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   17.37 +"S\<^isub>1p w \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   17.38  quickcheck[tester = prolog, iterations=1, expect = counterexample]
   17.39  oops
   17.40  
   17.41 @@ -84,13 +84,13 @@
   17.42    {ensure_groundness = true,
   17.43    limit_globally = NONE,
   17.44    limited_types = [],
   17.45 -  limited_predicates = [(["s2", "a2", "b2"], 3)],
   17.46 -  replacing = [(("s2", "limited_s2"), "quickcheck")],
   17.47 +  limited_predicates = [(["s2p", "a2p", "b2p"], 3)],
   17.48 +  replacing = [(("s2p", "limited_s2p"), "quickcheck")],
   17.49    manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
   17.50  
   17.51  
   17.52  theorem S\<^isub>2_sound:
   17.53 -"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   17.54 +  "S\<^isub>2p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   17.55  quickcheck[tester = prolog, iterations=1, expect = counterexample]
   17.56  oops
   17.57  
   17.58 @@ -107,12 +107,12 @@
   17.59    {ensure_groundness = true,
   17.60    limit_globally = NONE,
   17.61    limited_types = [],
   17.62 -  limited_predicates = [(["s3", "a3", "b3"], 6)],
   17.63 -  replacing = [(("s3", "limited_s3"), "quickcheck")],
   17.64 +  limited_predicates = [(["s3p", "a3p", "b3p"], 6)],
   17.65 +  replacing = [(("s3p", "limited_s3p"), "quickcheck")],
   17.66    manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
   17.67  
   17.68  lemma S\<^isub>3_sound:
   17.69 -"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   17.70 +  "S\<^isub>3p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   17.71  quickcheck[tester = prolog, iterations=1, size=1, expect = no_counterexample]
   17.72  oops
   17.73  
   17.74 @@ -149,13 +149,13 @@
   17.75    {ensure_groundness = true,
   17.76    limit_globally = NONE,
   17.77    limited_types = [],
   17.78 -  limited_predicates = [(["s4", "a4", "b4"], 6)],
   17.79 -  replacing = [(("s4", "limited_s4"), "quickcheck")],
   17.80 +  limited_predicates = [(["s4p", "a4p", "b4p"], 6)],
   17.81 +  replacing = [(("s4p", "limited_s4p"), "quickcheck")],
   17.82    manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
   17.83  
   17.84  
   17.85  theorem S\<^isub>4_sound:
   17.86 -"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   17.87 +  "S\<^isub>4p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   17.88  quickcheck[tester = prolog, size=1, iterations=1, expect = no_counterexample]
   17.89  oops
   17.90  
    18.1 --- a/src/HOL/Predicate_Compile_Examples/Examples.thy	Sat Dec 24 15:53:10 2011 +0100
    18.2 +++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Sat Dec 24 15:53:10 2011 +0100
    18.3 @@ -29,28 +29,44 @@
    18.4                           (s1 @ rhs @ s2) = rsl \<and>
    18.5                           (rule lhs rhs) \<in> fst g }"
    18.6  
    18.7 +definition derivesp :: "(('nts, 'ts) rule => bool) * 'nts => ('nts, 'ts) symbol list => ('nts, 'ts) symbol list => bool"
    18.8 +where
    18.9 +  "derivesp g = (\<lambda> lhs rhs. (lhs, rhs) \<in> derives (Collect (fst g), snd g))"
   18.10 + 
   18.11 +lemma [code_pred_def]:
   18.12 +  "derivesp g = (\<lambda> lsl rsl. \<exists>s1 s2 lhs rhs. 
   18.13 +                         (s1 @ [NTS lhs] @ s2 = lsl) \<and>
   18.14 +                         (s1 @ rhs @ s2) = rsl \<and>
   18.15 +                         (fst g) (rule lhs rhs))"
   18.16 +unfolding derivesp_def derives_def by auto
   18.17 +
   18.18  abbreviation "example_grammar == 
   18.19  ({ rule ''S'' [NTS ''A'', NTS ''B''],
   18.20     rule ''S'' [TS ''a''],
   18.21    rule ''A'' [TS ''b'']}, ''S'')"
   18.22  
   18.23 -
   18.24 -code_pred [inductify, skip_proof] derives .
   18.25 +definition "example_rules == 
   18.26 +(%x. x = rule ''S'' [NTS ''A'', NTS ''B''] \<or>
   18.27 +   x = rule ''S'' [TS ''a''] \<or>
   18.28 +  x = rule ''A'' [TS ''b''])"
   18.29  
   18.30 -thm derives.equation
   18.31  
   18.32 -definition "test = { rhs. derives example_grammar ([NTS ''S''], rhs) }"
   18.33 +code_pred [inductify, skip_proof] derivesp .
   18.34 +
   18.35 +thm derivesp.equation
   18.36  
   18.37 -code_pred (modes: o \<Rightarrow> bool) [inductify] test .
   18.38 -thm test.equation
   18.39 +definition "testp = (% rhs. derivesp (example_rules, ''S'') [NTS ''S''] rhs)"
   18.40  
   18.41 -values "{rhs. test rhs}"
   18.42 +code_pred (modes: o \<Rightarrow> bool) [inductify] testp .
   18.43 +thm testp.equation
   18.44  
   18.45 -declare rtrancl.intros(1)[code_pred_def] converse_rtrancl_into_rtrancl[code_pred_def]
   18.46 +values "{rhs. testp rhs}"
   18.47 +
   18.48 +declare rtranclp.intros(1)[code_pred_def] converse_rtranclp_into_rtranclp[code_pred_def]
   18.49  
   18.50 -code_pred [inductify] rtrancl .
   18.51 +code_pred [inductify] rtranclp .
   18.52  
   18.53 -definition "test2 = { rhs. ([NTS ''S''],rhs) \<in> (derives example_grammar)^*  }"
   18.54 +definition "test2 = (\<lambda> rhs. rtranclp (derivesp (example_rules, ''S'')) [NTS ''S''] rhs)"
   18.55  
   18.56  code_pred [inductify, skip_proof] test2 .
   18.57  
    19.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Sat Dec 24 15:53:10 2011 +0100
    19.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Sat Dec 24 15:53:10 2011 +0100
    19.3 @@ -6,12 +6,68 @@
    19.4  begin
    19.5  
    19.6  declare Let_def[code_pred_inline]
    19.7 -
    19.8 +(*
    19.9 +thm hotel_def
   19.10  lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
   19.11  by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
   19.12  
   19.13  lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
   19.14  by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
   19.15 +*)
   19.16 +
   19.17 +definition issuedp :: "event list => key => bool"
   19.18 +where
   19.19 +  "issuedp evs k = (k \<in> issued evs)"
   19.20 +
   19.21 +lemma [code_pred_def]:
   19.22 +  "issuedp [] Key0 = True"
   19.23 +  "issuedp (e # s) k = (issuedp s k \<or> (case e of Check_in g r (k1, k2) => k = k2 | _ => False))"
   19.24 +unfolding issuedp_def issued.simps initk_def
   19.25 +by (auto split: event.split)
   19.26 +
   19.27 +definition cardsp
   19.28 +where
   19.29 + "cardsp s g k = (k \<in> cards s g)"
   19.30 +
   19.31 +lemma [code_pred_def]:
   19.32 +  "cardsp [] g k = False"
   19.33 +  "cardsp (e # s) g k = (let C = cardsp s g in case e of Check_in g' r c => if g' = g then k = c \<or> C k else C k | _ => C k)"
   19.34 +unfolding cardsp_def_raw cards.simps by (auto simp add: Let_def split: event.split)
   19.35 +
   19.36 +definition
   19.37 +  "isinp evs r g = (g \<in> isin evs r)"
   19.38 +
   19.39 +lemma [code_pred_def]:
   19.40 +  "isinp [] r g = False"
   19.41 +  "isinp (e # s) r g =
   19.42 +  (let G = isinp s r
   19.43 +   in case e of Check_in g' r c => G g
   19.44 +    | Enter g' r' c => if r' = r then g = g' \<or> G g else G g
   19.45 +    | Exit g' r' => if r' = r then ((g \<noteq> g') \<and> G g) else G g)"
   19.46 +unfolding isinp_def_raw isin.simps by (auto simp add: Let_def split: event.split)
   19.47 +
   19.48 +declare hotel.simps(1)[code_pred_def]
   19.49 +lemma [code_pred_def]:
   19.50 +"hotel (e # s) =
   19.51 +  (hotel s & (case e of Check_in g r (k, k') => k = currk s r & \<not> issuedp s k'
   19.52 +  | Enter g r (k, k') => cardsp s g (k, k') & (roomk s r = k \<or> roomk s r = k')
   19.53 +  | Exit g r => isinp s r g))"
   19.54 +unfolding hotel.simps issuedp_def cardsp_def isinp_def
   19.55 +by (auto split: event.split)
   19.56 +
   19.57 +declare List.member_rec[code_pred_def]
   19.58 +
   19.59 +lemma [code_pred_def]: "no_Check_in s r = (~ (EX g c. List.member s (Check_in g r c)))"
   19.60 +unfolding no_Check_in_def member_def by auto
   19.61 +
   19.62 +lemma [code_pred_def]: "feels_safe s r =
   19.63 +(EX s\<^isub>1 s\<^isub>2 s\<^isub>3 g c c'.
   19.64 +    s =
   19.65 +    s\<^isub>3 @
   19.66 +    [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 &
   19.67 +    no_Check_in (s\<^isub>3 @ s\<^isub>2) r &
   19.68 +    (\<not> (\<exists> g'. isinp (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r g')))"
   19.69 +unfolding feels_safe_def isinp_def by auto
   19.70  
   19.71  setup {* Code_Prolog.map_code_options (K
   19.72    {ensure_groundness = true,
   19.73 @@ -25,8 +81,7 @@
   19.74  
   19.75  setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
   19.76  
   19.77 -lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
   19.78 -quickcheck[tester = random, iterations = 10000, report]
   19.79 +lemma "\<lbrakk> hotel s; isinp s r g \<rbrakk> \<Longrightarrow> owns s r = Some g"
   19.80  quickcheck[tester = prolog, iterations = 1, expect = counterexample]
   19.81  oops
   19.82  
   19.83 @@ -41,7 +96,7 @@
   19.84     manual_reorder = []}) *}
   19.85  
   19.86  lemma
   19.87 -  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   19.88 +  "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
   19.89  quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
   19.90  oops
   19.91  
   19.92 @@ -54,52 +109,18 @@
   19.93     manual_reorder = []}) *}
   19.94  
   19.95  lemma
   19.96 -  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   19.97 -quickcheck[tester = prolog, iterations = 1, expect = counterexample]
   19.98 -oops
   19.99 -
  19.100 -section {* Simulating a global depth limit manually by limiting all predicates *}
  19.101 -
  19.102 -setup {*
  19.103 -  Code_Prolog.map_code_options (K
  19.104 -  {ensure_groundness = true,
  19.105 -  limit_globally = NONE,
  19.106 -  limited_types = [],
  19.107 -  limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
  19.108 -    "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 12)],
  19.109 -  replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
  19.110 -  manual_reorder = []})
  19.111 -*}
  19.112 -
  19.113 -lemma
  19.114 -  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
  19.115 -quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
  19.116 -oops
  19.117 -
  19.118 -setup {*
  19.119 -  Code_Prolog.map_code_options (K
  19.120 -  {ensure_groundness = true,
  19.121 -  limit_globally = NONE,
  19.122 -  limited_types = [],
  19.123 -  limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
  19.124 -    "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 13)],
  19.125 -  replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
  19.126 -  manual_reorder = []})
  19.127 -*}
  19.128 -
  19.129 -lemma
  19.130 -  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
  19.131 +  "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
  19.132  quickcheck[tester = prolog, iterations = 1, expect = counterexample]
  19.133  oops
  19.134  
  19.135  section {* Using a global limit for limiting the execution *} 
  19.136  
  19.137 -text {* A global depth limit of 13 does not suffice to find the counterexample. *}
  19.138 +text {* A global depth limit of 10 does not suffice to find the counterexample. *}
  19.139  
  19.140  setup {*
  19.141    Code_Prolog.map_code_options (K
  19.142    {ensure_groundness = true,
  19.143 -  limit_globally = SOME 13,
  19.144 +  limit_globally = SOME 10,
  19.145    limited_types = [],
  19.146    limited_predicates = [],
  19.147    replacing = [],
  19.148 @@ -107,16 +128,16 @@
  19.149  *}
  19.150  
  19.151  lemma
  19.152 -  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
  19.153 +  "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
  19.154  quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
  19.155  oops
  19.156  
  19.157 -text {* But a global depth limit of 14 does. *}
  19.158 +text {* But a global depth limit of 11 does. *}
  19.159  
  19.160  setup {*
  19.161    Code_Prolog.map_code_options (K
  19.162    {ensure_groundness = true,
  19.163 -  limit_globally = SOME 14,
  19.164 +  limit_globally = SOME 11,
  19.165    limited_types = [],
  19.166    limited_predicates = [],
  19.167    replacing = [],
  19.168 @@ -124,7 +145,7 @@
  19.169  *}
  19.170  
  19.171  lemma
  19.172 -  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
  19.173 +  "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
  19.174  quickcheck[tester = prolog, iterations = 1, expect = counterexample]
  19.175  oops
  19.176  
    20.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Sat Dec 24 15:53:10 2011 +0100
    20.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Sat Dec 24 15:53:10 2011 +0100
    20.3 @@ -38,14 +38,14 @@
    20.4  values [expected "{()}" random_dseq 1, 1, 2] "{x. True'}"
    20.5  values [expected "{()}" random_dseq 1, 1, 3] "{x. True'}"
    20.6  
    20.7 -inductive EmptySet :: "'a \<Rightarrow> bool"
    20.8 +inductive EmptyPred :: "'a \<Rightarrow> bool"
    20.9  
   20.10 -code_pred (expected_modes: o => bool, i => bool) EmptySet .
   20.11 +code_pred (expected_modes: o => bool, i => bool) EmptyPred .
   20.12  
   20.13 -definition EmptySet' :: "'a \<Rightarrow> bool"
   20.14 -where "EmptySet' = {}"
   20.15 +definition EmptyPred' :: "'a \<Rightarrow> bool"
   20.16 +where "EmptyPred' = (\<lambda> x. False)"
   20.17  
   20.18 -code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' .
   20.19 +code_pred (expected_modes: o => bool, i => bool) [inductify] EmptyPred' .
   20.20  
   20.21  inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
   20.22  
   20.23 @@ -296,7 +296,7 @@
   20.24  lemma zerozero'_eq: "zerozero' x == zerozero x"
   20.25  proof -
   20.26    have "zerozero' = zerozero"
   20.27 -    apply (auto simp add: mem_def)
   20.28 +    apply (auto simp add: fun_eq_iff)
   20.29      apply (cases rule: zerozero'.cases)
   20.30      apply (auto simp add: equals_def intro: zerozero.intros)
   20.31      apply (cases rule: zerozero.cases)
   20.32 @@ -313,10 +313,21 @@
   20.33  
   20.34  code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' .
   20.35  
   20.36 -subsection {* Sets and Numerals *}
   20.37 +subsection {* Sets *}
   20.38 +(*
   20.39 +inductive_set EmptySet :: "'a set"
   20.40 +
   20.41 +code_pred (expected_modes: o => bool, i => bool) EmptySet .
   20.42 +
   20.43 +definition EmptySet' :: "'a set"
   20.44 +where "EmptySet' = {}"
   20.45 +
   20.46 +code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' .
   20.47 +*)
   20.48 +subsection {* Numerals *}
   20.49  
   20.50  definition
   20.51 -  "one_or_two = {Suc 0, (Suc (Suc 0))}"
   20.52 +  "one_or_two = (%x. x = Suc 0 \<or> ( x = Suc (Suc 0)))"
   20.53  
   20.54  code_pred [inductify] one_or_two .
   20.55  
   20.56 @@ -337,7 +348,7 @@
   20.57  values "{x. one_or_two' x}"
   20.58  
   20.59  definition one_or_two'':
   20.60 -  "one_or_two'' == {1, (2::nat)}"
   20.61 +  "one_or_two'' == (%x. x = 1 \<or> x = (2::nat))"
   20.62  
   20.63  code_pred [inductify] one_or_two'' .
   20.64  thm one_or_two''.equation
   20.65 @@ -847,7 +858,10 @@
   20.66  thm Min.equation
   20.67  
   20.68  subsection {* Lexicographic order *}
   20.69 +text {* This example requires to handle the differences of sets and predicates in the predicate compiler,
   20.70 +or to have a copy of all definitions on predicates due to the set-predicate distinction. *}
   20.71  
   20.72 +(*
   20.73  declare lexord_def[code_pred_def]
   20.74  code_pred [inductify] lexord .
   20.75  code_pred [random_dseq inductify] lexord .
   20.76 @@ -889,6 +903,7 @@
   20.77  
   20.78  values [random_dseq 4, 4, 6] 100 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
   20.79  *)
   20.80 +
   20.81  inductive has_length
   20.82  where
   20.83    "has_length [] 0"
   20.84 @@ -956,7 +971,7 @@
   20.85  thm lists.intros
   20.86  code_pred [inductify] lists .
   20.87  thm lists.equation
   20.88 -
   20.89 +*)
   20.90  subsection {* AVL Tree *}
   20.91  
   20.92  datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
   20.93 @@ -990,16 +1005,16 @@
   20.94  | "is_ord (MKT n l r h) =
   20.95   ((\<forall>n' \<in> set_of l. n' < n) \<and> (\<forall>n' \<in> set_of r. n < n') \<and> is_ord l \<and> is_ord r)"
   20.96  
   20.97 +(* 
   20.98  code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] set_of .
   20.99  thm set_of.equation
  20.100  
  20.101  code_pred (expected_modes: i => bool) [inductify] is_ord .
  20.102  thm is_ord_aux.equation
  20.103  thm is_ord.equation
  20.104 -
  20.105 +*)
  20.106  subsection {* Definitions about Relations *}
  20.107 -
  20.108 -term "converse"
  20.109 +(*
  20.110  code_pred (modes:
  20.111    (i * i => bool) => i * i => bool,
  20.112    (i * o => bool) => o * i => bool,
  20.113 @@ -1059,10 +1074,10 @@
  20.114  thm inv_image_def
  20.115  code_pred [inductify] inv_image .
  20.116  thm inv_image.equation
  20.117 -
  20.118 +*)
  20.119  subsection {* Inverting list functions *}
  20.120  
  20.121 -code_pred [inductify] size_list .
  20.122 +code_pred [inductify, skip_proof] size_list .
  20.123  code_pred [new_random_dseq inductify] size_list .
  20.124  thm size_listP.equation
  20.125  thm size_listP.new_random_dseq_equation
  20.126 @@ -1115,11 +1130,12 @@
  20.127  thm zipP.equation
  20.128  
  20.129  code_pred [inductify, skip_proof] upt .
  20.130 +(*
  20.131  code_pred [inductify, skip_proof] remdups .
  20.132  thm remdupsP.equation
  20.133  code_pred [dseq inductify] remdups .
  20.134  values [dseq 4] 5 "{xs. remdupsP xs [1, (2::int)]}"
  20.135 -
  20.136 +*)
  20.137  code_pred [inductify, skip_proof] remove1 .
  20.138  thm remove1P.equation
  20.139  values "{xs. remove1P 1 xs [2, (3::int)]}"
  20.140 @@ -1129,9 +1145,10 @@
  20.141  code_pred [dseq inductify] removeAll .
  20.142  
  20.143  values [dseq 4] 10 "{xs. removeAllP 1 xs [(2::nat)]}"
  20.144 -
  20.145 +(*
  20.146  code_pred [inductify] distinct .
  20.147  thm distinct.equation
  20.148 +*)
  20.149  code_pred [inductify, skip_proof] replicate .
  20.150  thm replicateP.equation
  20.151  values 5 "{(n, xs). replicateP n (0::int) xs}"
    21.1 --- a/src/HOL/Quotient_Examples/Lift_Set.thy	Sat Dec 24 15:53:10 2011 +0100
    21.2 +++ b/src/HOL/Quotient_Examples/Lift_Set.thy	Sat Dec 24 15:53:10 2011 +0100
    21.3 @@ -8,9 +8,9 @@
    21.4  imports Main
    21.5  begin
    21.6  
    21.7 -definition set where "set = (UNIV :: ('a => bool) => bool)"
    21.8 +definition set where "set = (UNIV :: ('a \<Rightarrow> bool) set)"
    21.9  
   21.10 -typedef (open) 'a set = "set :: 'a set set"
   21.11 +typedef (open) 'a set = "set :: ('a \<Rightarrow> bool) set"
   21.12    morphisms member Set
   21.13    unfolding set_def by auto
   21.14  
   21.15 @@ -37,15 +37,19 @@
   21.16  text {* Now, we can employ quotient_definition to lift definitions. *}
   21.17  
   21.18  quotient_definition empty where "empty :: 'a set"
   21.19 -is "Set.empty"
   21.20 +is "bot :: 'a \<Rightarrow> bool"
   21.21  
   21.22  term "Lift_Set.empty"
   21.23  thm Lift_Set.empty_def
   21.24  
   21.25 +definition insertp :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
   21.26 +  "insertp x P y \<longleftrightarrow> y = x \<or> P y"
   21.27 +
   21.28  quotient_definition insert where "insert :: 'a => 'a set => 'a set"
   21.29 -is "Set.insert"
   21.30 +is insertp
   21.31  
   21.32  term "Lift_Set.insert"
   21.33  thm Lift_Set.insert_def
   21.34  
   21.35  end
   21.36 +
    22.1 --- a/src/HOL/Wellfounded.thy	Sat Dec 24 15:53:10 2011 +0100
    22.2 +++ b/src/HOL/Wellfounded.thy	Sat Dec 24 15:53:10 2011 +0100
    22.3 @@ -298,8 +298,10 @@
    22.4  
    22.5  lemma wfP_SUP:
    22.6    "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow> wfP (SUPR UNIV r)"
    22.7 -  by (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred SUP_UN_eq2])
    22.8 -    (simp_all add: Collect_def)
    22.9 +  apply (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred SUP_UN_eq2])
   22.10 +  apply (simp_all add: inf_set_def)
   22.11 +  apply auto
   22.12 +  done
   22.13  
   22.14  lemma wf_Union: 
   22.15   "[| ALL r:R. wf r;