--- a/src/HOL/Library/Cset.thy Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Library/Cset.thy Sat Dec 24 15:53:10 2011 +0100
@@ -24,10 +24,6 @@
definition member :: "'a Cset.set \<Rightarrow> 'a \<Rightarrow> bool" where
"member A x \<longleftrightarrow> x \<in> set_of A"
-lemma member_set_of:
- "set_of = member"
- by (rule ext)+ (simp add: member_def mem_def)
-
lemma member_Set [simp]:
"member (Set A) x \<longleftrightarrow> x \<in> A"
by (simp add: member_def)
@@ -38,7 +34,7 @@
lemma set_eq_iff:
"A = B \<longleftrightarrow> member A = member B"
- by (auto simp add: fun_eq_iff set_of_inject [symmetric] member_def mem_def)
+ by (auto simp add: fun_eq_iff set_of_inject [symmetric] member_def)
hide_fact (open) set_eq_iff
lemma set_eqI:
@@ -76,7 +72,7 @@
[simp]: "A - B = Set (set_of A - set_of B)"
instance proof
-qed (auto intro!: Cset.set_eqI simp add: member_def mem_def)
+qed (auto intro!: Cset.set_eqI simp add: member_def)
end
@@ -364,19 +360,13 @@
Predicate.Empty \<Rightarrow> Cset.empty
| Predicate.Insert x P \<Rightarrow> Cset.insert x (of_pred P)
| Predicate.Join P xq \<Rightarrow> sup (of_pred P) (of_seq xq))"
- 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)
- apply (unfold Set.insert_def Collect_def sup_apply member_set_of)
- apply simp_all
- done
+ 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])
lemma of_seq_code [code]:
"of_seq Predicate.Empty = Cset.empty"
"of_seq (Predicate.Insert x P) = Cset.insert x (of_pred P)"
"of_seq (Predicate.Join P xq) = sup (of_pred P) (of_seq xq)"
- apply (auto simp add: of_seq_def of_pred_def Cset.set_eq_iff mem_def Collect_def)
- apply (unfold Set.insert_def Collect_def sup_apply member_set_of)
- apply simp_all
- done
+ by (auto simp add: of_seq_def of_pred_def Cset.set_eq_iff)
lemma bind_set:
"Cset.bind (Cset.set xs) f = fold (sup \<circ> f) xs (Cset.set [])"
@@ -387,9 +377,9 @@
"pred_of_cset (Cset.set xs) = foldr sup (List.map Predicate.single xs) bot"
proof -
have "pred_of_cset (Cset.set xs) = Predicate.Pred (\<lambda>x. x \<in> set xs)"
- by (simp add: Cset.pred_of_cset_def member_set)
+ by (simp add: Cset.pred_of_cset_def)
moreover have "foldr sup (List.map Predicate.single xs) bot = \<dots>"
- by (induct xs) (auto simp add: bot_pred_def intro: pred_eqI, simp add: mem_def)
+ by (induct xs) (auto simp add: bot_pred_def intro: pred_eqI)
ultimately show ?thesis by simp
qed
hide_fact (open) pred_of_cset_set
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Sat Dec 24 15:53:10 2011 +0100
@@ -12,7 +12,7 @@
declare le_bool_def_raw[code_pred_inline]
lemma min_bool_eq [code_pred_inline]: "(min :: bool => bool => bool) == (op &)"
-by (rule eq_reflection) (auto simp add: fun_eq_iff min_def le_bool_def)
+by (rule eq_reflection) (auto simp add: fun_eq_iff min_def)
lemma [code_pred_inline]:
"((A::bool) ~= (B::bool)) = ((A & ~ B) | (B & ~ A))"
@@ -31,11 +31,7 @@
section {* Set operations *}
-declare Collect_def[code_pred_inline]
-declare mem_def[code_pred_inline]
-
declare eq_reflection[OF empty_def, code_pred_inline]
-declare insert_code[code_pred_def]
declare subset_iff[code_pred_inline]
@@ -45,15 +41,16 @@
lemma Diff[code_pred_inline]:
"(A - B) = (%x. A x \<and> \<not> B x)"
-by (auto simp add: mem_def)
+ by (simp add: fun_eq_iff minus_apply)
lemma subset_eq[code_pred_inline]:
"(P :: 'a => bool) < (Q :: 'a => bool) == ((\<exists>x. Q x \<and> (\<not> P x)) \<and> (\<forall> x. P x --> Q x))"
-by (rule eq_reflection) (fastforce simp add: mem_def)
+ by (rule eq_reflection) (auto simp add: less_fun_def le_fun_def)
lemma set_equality[code_pred_inline]:
- "(A = B) = ((\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x))"
-by (fastforce simp add: mem_def)
+ "A = B \<longleftrightarrow> (\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x)"
+ by (auto simp add: fun_eq_iff)
+
section {* Setup for Numerals *}
@@ -197,30 +194,6 @@
declare size_list_simps[code_pred_def]
declare size_list_def[symmetric, code_pred_inline]
-subsection {* Alternative rules for set *}
-
-lemma set_ConsI1 [code_pred_intro]:
- "set (x # xs) x"
-unfolding mem_def[symmetric, of _ x]
-by auto
-
-lemma set_ConsI2 [code_pred_intro]:
- "set xs x ==> set (x' # xs) x"
-unfolding mem_def[symmetric, of _ x]
-by auto
-
-code_pred [skip_proof] set
-proof -
- case set
- from this show thesis
- apply (case_tac xb)
- apply auto
- unfolding mem_def[symmetric, of _ xc]
- apply auto
- unfolding mem_def
- apply fastforce
- done
-qed
subsection {* Alternative rules for list_all2 *}
@@ -259,5 +232,4 @@
lemma less_nat_k_0 [code_pred_simp]: "less_nat k 0 == False"
unfolding less_nat[symmetric] by auto
-
end
\ No newline at end of file
--- a/src/HOL/Library/Quotient_Set.thy Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Library/Quotient_Set.thy Sat Dec 24 15:53:10 2011 +0100
@@ -76,20 +76,10 @@
lemma mem_prs[quot_preserve]:
assumes "Quotient R Abs Rep"
- shows "(Rep ---> (Abs ---> id) ---> id) (op \<in>) = op \<in>"
-using Quotient_abs_rep[OF assms]
-by(simp add: fun_eq_iff mem_def)
-
-lemma mem_rsp[quot_respect]:
- "(R ===> (R ===> op =) ===> op =) (op \<in>) (op \<in>)"
- by (auto simp add: fun_eq_iff mem_def intro!: fun_relI elim: fun_relE)
-
-lemma mem_prs2:
- assumes "Quotient R Abs Rep"
shows "(Rep ---> op -` Abs ---> id) op \<in> = op \<in>"
by (simp add: fun_eq_iff Quotient_abs_rep[OF assms])
-lemma mem_rsp2:
+lemma mem_rsp[quot_respect]:
shows "(R ===> set_rel R ===> op =) op \<in> op \<in>"
by (intro fun_relI) (simp add: set_rel_def)
--- a/src/HOL/Metis_Examples/Message.thy Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Metis_Examples/Message.thy Sat Dec 24 15:53:10 2011 +0100
@@ -245,8 +245,9 @@
lemma parts_trans: "[| X\<in> parts G; G \<subseteq> parts H |] ==> X\<in> parts H"
by (blast dest: parts_mono)
-lemma parts_cut: "[|Y\<in> parts (insert X G); X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
-by (metis Un_insert_left Un_insert_right insert_absorb mem_def parts_Un parts_idem sup1CI)
+(*lemma parts_cut: "[|Y\<in> parts (insert X G); X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
+by (metis UnI2 insert_subset le_supE parts_Un_subset1 parts_increasing parts_trans subsetD)
+by (metis Un_insert_left Un_insert_right insert_absorb parts_Un parts_idem sup1CI)*)
subsubsection{*Rewrite rules for pulling out atomic messages *}
@@ -677,8 +678,8 @@
apply (rule subsetI)
apply (erule analz.induct)
apply (metis UnCI UnE Un_commute analz.Inj)
-apply (metis MPair_synth UnCI UnE Un_commute analz.Fst analz.Inj mem_def)
-apply (metis MPair_synth UnCI UnE Un_commute analz.Inj analz.Snd mem_def)
+apply (metis MPair_synth UnCI UnE Un_commute analz.Fst analz.Inj)
+apply (metis MPair_synth UnCI UnE Un_commute analz.Inj analz.Snd)
apply (blast intro: analz.Decrypt)
apply blast
done
@@ -695,13 +696,11 @@
subsubsection{*For reasoning about the Fake rule in traces *}
-lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
+lemma parts_insert_subset_Un: "X \<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
proof -
assume "X \<in> G"
- hence "G X" by (metis mem_def)
- hence "\<forall>x\<^isub>1. G \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 X" by (metis predicate1D)
- hence "\<forall>x\<^isub>1. (G \<union> x\<^isub>1) X" by (metis Un_upper1)
- hence "\<forall>x\<^isub>1. X \<in> G \<union> x\<^isub>1" by (metis mem_def)
+ hence "\<forall>x\<^isub>1. G \<subseteq> x\<^isub>1 \<longrightarrow> X \<in> x\<^isub>1 " by auto
+ hence "\<forall>x\<^isub>1. X \<in> G \<union> x\<^isub>1" by (metis Un_upper1)
hence "insert X H \<subseteq> G \<union> H" by (metis Un_upper2 insert_subset)
hence "parts (insert X H) \<subseteq> parts (G \<union> H)" by (metis parts_mono)
thus "parts (insert X H) \<subseteq> parts G \<union> parts H" by (metis parts_Un)
@@ -716,10 +715,10 @@
by (metis analz_idem analz_synth)
have F2: "\<forall>x\<^isub>1. parts x\<^isub>1 \<union> synth (analz x\<^isub>1) = parts (synth (analz x\<^isub>1))"
by (metis parts_analz parts_synth)
- have F3: "synth (analz H) X" using A1 by (metis mem_def)
+ have F3: "X \<in> synth (analz H)" using A1 by metis
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))
hence F4: "\<forall>x\<^isub>1. analz x\<^isub>1 \<subseteq> analz (synth x\<^isub>1)" by (metis analz_synth)
- have F5: "X \<in> synth (analz H)" using F3 by (metis mem_def)
+ have F5: "X \<in> synth (analz H)" using F3 by metis
have "\<forall>x\<^isub>1. analz x\<^isub>1 \<subseteq> synth (analz x\<^isub>1)
\<longrightarrow> analz (synth (analz x\<^isub>1)) = synth (analz x\<^isub>1)"
using F1 by (metis subset_Un_eq)
@@ -741,7 +740,7 @@
==> Z \<in> synth (analz H) \<union> parts H"
by (blast dest: Fake_parts_insert [THEN subsetD, dest])
-declare analz_mono [intro] synth_mono [intro]
+declare synth_mono [intro]
lemma Fake_analz_insert:
"X \<in> synth (analz G) ==>
--- a/src/HOL/Metis_Examples/Proxies.thy Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Metis_Examples/Proxies.thy Sat Dec 24 15:53:10 2011 +0100
@@ -41,7 +41,7 @@
lemma "xs \<in> A"
sledgehammer [expect = some]
-by (metis_exhaust A_def Collect_def mem_def)
+by (metis_exhaust A_def mem_Collect_eq)
definition "B (y::int) \<equiv> y \<le> 0"
definition "C (y::int) \<equiv> y \<le> 1"
@@ -49,7 +49,7 @@
lemma int_le_0_imp_le_1: "x \<le> (0::int) \<Longrightarrow> x \<le> 1"
by linarith
-lemma "B \<subseteq> C"
+lemma "B \<le> C"
sledgehammer [type_enc = poly_args, max_relevant = 100, expect = some]
by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)
@@ -151,7 +151,7 @@
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
-by (metis_exhaust id_apply)
+by metis_exhaust
lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
sledgehammer [type_enc = erased, expect = some] (id_apply)
--- a/src/HOL/Metis_Examples/Tarski.thy Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Metis_Examples/Tarski.thy Sat Dec 24 15:53:10 2011 +0100
@@ -196,8 +196,7 @@
lemma (in PO) dualPO: "dual cl \<in> PartialOrder"
apply (insert cl_po)
-apply (simp add: PartialOrder_def dual_def refl_on_converse
- trans_converse antisym_converse)
+apply (simp add: PartialOrder_def dual_def)
done
lemma Rdual:
@@ -519,22 +518,22 @@
thus "lub {x. (x, f x) \<in> r \<and> x \<in> A} cl \<in> A" using A1 by metis
next
assume A1: "H = {x. (x, f x) \<in> r \<and> x \<in> A}"
- have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
- have F2: "\<forall>w u. (\<lambda>R. u R \<and> w R) = u \<inter> w"
- by (metis Collect_conj_eq Collect_def)
- have F3: "\<forall>x v. (\<lambda>R. v R \<in> x) = v -` x" by (metis vimage_def Collect_def)
+ have F1: "\<forall>v. {R. R \<in> v} = v" by (metis Collect_mem_eq)
+ have F2: "\<forall>w u. {R. R \<in> u \<and> R \<in> w} = u \<inter> w"
+ by (metis Collect_conj_eq Collect_mem_eq)
+ have F3: "\<forall>x v. {R. v R \<in> x} = v -` x" by (metis vimage_def)
hence F4: "A \<inter> (\<lambda>R. (R, f R)) -` r = H" using A1 by auto
- hence F5: "(f (lub H cl), lub H cl) \<in> r"
- by (metis F1 F3 F2 Int_commute flubH_le_lubH Collect_def)
+ hence F5: "(f (lub H cl), lub H cl) \<in> r"
+ by (metis A1 flubH_le_lubH)
have F6: "(lub H cl, f (lub H cl)) \<in> r"
- by (metis F1 F3 F2 F4 Int_commute lubH_le_flubH Collect_def)
+ by (metis A1 lubH_le_flubH)
have "(lub H cl, f (lub H cl)) \<in> r \<longrightarrow> f (lub H cl) = lub H cl"
using F5 by (metis antisymE)
hence "f (lub H cl) = lub H cl" using F6 by metis
thus "H = {x. (x, f x) \<in> r \<and> x \<in> A}
\<Longrightarrow> f (lub {x. (x, f x) \<in> r \<and> x \<in> A} cl) =
lub {x. (x, f x) \<in> r \<and> x \<in> A} cl"
- by (metis F4 F2 F3 F1 Collect_def Int_commute)
+ by metis
qed
lemma (in CLF) (*lubH_is_fixp:*)
--- a/src/HOL/Metis_Examples/Trans_Closure.thy Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Metis_Examples/Trans_Closure.thy Sat Dec 24 15:53:10 2011 +0100
@@ -50,11 +50,9 @@
assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
assume A3: "(a, b) \<in> R\<^sup>*"
assume A4: "(b, c) \<in> R\<^sup>*"
- have "(R\<^sup>*) (a, b)" using A3 by (metis mem_def)
- hence F1: "(a, b) \<in> R\<^sup>*" by (metis mem_def)
have "b \<noteq> c" using A1 A2 by metis
hence "\<exists>x\<^isub>1. (b, x\<^isub>1) \<in> R" using A4 by (metis converse_rtranclE)
- thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F1 by (metis transitive_closure_trans(6))
+ thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using A3 by (metis transitive_closure_trans(6))
qed
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>
--- a/src/HOL/MicroJava/BV/BVExample.thy Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy Sat Dec 24 15:53:10 2011 +0100
@@ -452,7 +452,7 @@
qed
lemma [code]:
- "iter f step ss w = while (\<lambda>(ss, w). \<not> is_empty w)
+ "iter f step ss w = while (\<lambda>(ss, w). \<not> More_Set.is_empty w)
(\<lambda>(ss, w).
let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p}))
(ss, w)"
@@ -478,12 +478,8 @@
#> 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")
*}
-definition [code del]: "mem2 = op :"
-lemma [code]: "mem2 x A = A x"
- by(simp add: mem2_def mem_def)
-
-lemmas [folded mem2_def, code] =
- JType.sup_def[unfolded exec_lub_def]
+lemmas [code] =
+ JType.sup_def [unfolded exec_lub_def]
wf_class_code
widen.equation
match_exception_entry_def
--- a/src/HOL/MicroJava/J/TypeRel.thy Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy Sat Dec 24 15:53:10 2011 +0100
@@ -4,7 +4,9 @@
header {* \isaheader{Relations between Java Types} *}
-theory TypeRel imports Decl "~~/src/HOL/Library/Wfrec" begin
+theory TypeRel
+imports Decl "~~/src/HOL/Library/Wfrec"
+begin
-- "direct subclass, cf. 8.1.3"
@@ -84,7 +86,9 @@
(modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool)
subcls1p
.
-declare subcls1_def[unfolded Collect_def, code_pred_def]
+
+declare subcls1_def [code_pred_def]
+
code_pred
(modes: i \<Rightarrow> i \<times> o \<Rightarrow> bool, i \<Rightarrow> i \<times> i \<Rightarrow> bool)
[inductify]
@@ -92,14 +96,16 @@
.
definition subcls' where "subcls' G = (subcls1p G)^**"
+
code_pred
(modes: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool)
[inductify]
subcls'
-.
+ .
+
lemma subcls_conv_subcls' [code_unfold]:
- "(subcls1 G)^* = (\<lambda>(C, D). subcls' G C D)"
-by(simp add: subcls'_def subcls1_def rtrancl_def)(simp add: Collect_def)
+ "(subcls1 G)^* = {(C, D). subcls' G C D}"
+by(simp add: subcls'_def subcls1_def rtrancl_def)
lemma class_rec_code [code]:
"class_rec G C t f =
@@ -190,7 +196,7 @@
map_of (map (\<lambda>(s,m). (s,(C,m))) ms)"
apply (unfold method_def)
apply (simp split del: split_if)
-apply (erule (1) class_rec_lemma [THEN trans]);
+apply (erule (1) class_rec_lemma [THEN trans])
apply auto
done
@@ -204,7 +210,7 @@
map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))"
apply (unfold fields_def)
apply (simp split del: split_if)
-apply (erule (1) class_rec_lemma [THEN trans]);
+apply (erule (1) class_rec_lemma [THEN trans])
apply auto
done
--- a/src/HOL/Nitpick.thy Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Nitpick.thy Sat Dec 24 15:53:10 2011 +0100
@@ -50,7 +50,7 @@
*}
lemma Ex1_unfold [nitpick_unfold, no_atp]:
-"Ex1 P \<equiv> \<exists>x. P = {x}"
+"Ex1 P \<equiv> \<exists>x. {x. P x} = {x}"
apply (rule eq_reflection)
apply (simp add: Ex1_def set_eq_iff)
apply (rule iffI)
@@ -60,7 +60,7 @@
apply (rule allI)
apply (rename_tac y)
apply (erule_tac x = y in allE)
-by (auto simp: mem_def)
+by auto
lemma rtrancl_unfold [nitpick_unfold, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
by (simp only: rtrancl_trancl_reflcl)
@@ -70,8 +70,8 @@
by (rule eq_reflection) (auto dest: rtranclpD)
lemma tranclp_unfold [nitpick_unfold, no_atp]:
-"tranclp r a b \<equiv> trancl (split r) (a, b)"
-by (simp add: trancl_def Collect_def mem_def)
+"tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
+by (simp add: trancl_def)
definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
"prod A B = {(a, b). a \<in> A \<and> b \<in> B}"
@@ -98,8 +98,8 @@
*}
lemma The_psimp [nitpick_psimp, no_atp]:
-"P = {x} \<Longrightarrow> The P = x"
-by (subgoal_tac "{x} = (\<lambda>y. y = x)") (auto simp: mem_def)
+ "P = (op =) x \<Longrightarrow> The P = x"
+ by auto
lemma Eps_psimp [nitpick_psimp, no_atp]:
"\<lbrakk>P x; \<not> P y; Eps P = y\<rbrakk> \<Longrightarrow> Eps P = x"
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Sat Dec 24 15:53:10 2011 +0100
@@ -75,15 +75,15 @@
nitpick [card = 1\<emdash>4, expect = none]
by auto
-lemma "Id (a, a)"
+lemma "(a, a) \<in> Id"
nitpick [card = 1\<emdash>50, expect = none]
-by (auto simp: Id_def Collect_def)
+by (auto simp: Id_def)
-lemma "Id ((a\<Colon>'a, b\<Colon>'a), (a, b))"
+lemma "((a\<Colon>'a, b\<Colon>'a), (a, b)) \<in> Id"
nitpick [card = 1\<emdash>10, expect = none]
-by (auto simp: Id_def Collect_def)
+by (auto simp: Id_def)
-lemma "UNIV (x\<Colon>'a\<times>'a)"
+lemma "(x\<Colon>'a\<times>'a) \<in> UNIV"
nitpick [card = 1\<emdash>50, expect = none]
sorry
@@ -539,13 +539,13 @@
nitpick [expect = none]
by auto
-lemma "I = (\<lambda>x. x) \<Longrightarrow> Id = (\<lambda>x. Id (I x))"
+lemma "I = (\<lambda>x. x) \<Longrightarrow> Id = {x. I x \<in> Id}"
nitpick [expect = none]
by auto
-lemma "{} = (\<lambda>x. False)"
+lemma "{} = {x. False}"
nitpick [expect = none]
-by (metis Collect_def empty_def)
+by (metis empty_def)
lemma "x \<in> {}"
nitpick [expect = genuine]
@@ -571,33 +571,23 @@
nitpick [expect = none]
by auto
-lemma "UNIV = (\<lambda>x. True)"
+lemma "UNIV = {x. True}"
nitpick [expect = none]
-by (simp only: UNIV_def Collect_def)
+by (simp only: UNIV_def)
-lemma "UNIV x = True"
+lemma "x \<in> UNIV \<longleftrightarrow> True"
nitpick [expect = none]
-by (simp only: UNIV_def Collect_def)
+by (simp only: UNIV_def mem_Collect_eq)
lemma "x \<notin> UNIV"
nitpick [expect = genuine]
oops
-lemma "op \<in> = (\<lambda>x P. P x)"
-nitpick [expect = none]
-apply (rule ext)
-apply (rule ext)
-by (simp add: mem_def)
-
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<in> = (\<lambda>x. (op \<in> (I x)))"
nitpick [expect = none]
apply (rule ext)
apply (rule ext)
-by (simp add: mem_def)
-
-lemma "P x = (x \<in> P)"
-nitpick [expect = none]
-by (simp add: mem_def)
+by simp
lemma "insert = (\<lambda>x y. insert x (y \<union> y))"
nitpick [expect = none]
@@ -753,7 +743,7 @@
nitpick [expect = genuine]
oops
-lemma "(P\<Colon>nat set) (Eps P)"
+lemma "Eps (\<lambda>x. x \<in> P) \<in> (P\<Colon>nat set)"
nitpick [expect = genuine]
oops
@@ -761,15 +751,15 @@
nitpick [expect = genuine]
oops
-lemma "\<not> (P\<Colon>nat set) (Eps P)"
+lemma "\<not> (P \<Colon> nat \<Rightarrow> bool) (Eps P)"
nitpick [expect = genuine]
oops
-lemma "P \<noteq> {} \<Longrightarrow> P (Eps P)"
+lemma "P \<noteq> bot \<Longrightarrow> P (Eps P)"
nitpick [expect = none]
sorry
-lemma "(P\<Colon>nat set) \<noteq> {} \<Longrightarrow> P (Eps P)"
+lemma "(P \<Colon> nat \<Rightarrow> bool) \<noteq> bot \<Longrightarrow> P (Eps P)"
nitpick [expect = none]
sorry
@@ -777,7 +767,7 @@
nitpick [expect = genuine]
oops
-lemma "(P\<Colon>nat set) (The P)"
+lemma "(P \<Colon> nat \<Rightarrow> bool) (The P)"
nitpick [expect = genuine]
oops
@@ -785,7 +775,7 @@
nitpick [expect = genuine]
oops
-lemma "\<not> (P\<Colon>nat set) (The P)"
+lemma "\<not> (P \<Colon> nat \<Rightarrow> bool) (The P)"
nitpick [expect = genuine]
oops
@@ -805,11 +795,11 @@
nitpick [expect = genuine]
oops
-lemma "P = {x} \<Longrightarrow> P (The P)"
+lemma "P = {x} \<Longrightarrow> (THE x. x \<in> P) \<in> P"
nitpick [expect = none]
oops
-lemma "P = {x\<Colon>nat} \<Longrightarrow> P (The P)"
+lemma "P = {x\<Colon>nat} \<Longrightarrow> (THE x. x \<in> P) \<in> P"
nitpick [expect = none]
oops
@@ -819,23 +809,23 @@
nitpick [expect = genuine]
oops
-lemma "(Q\<Colon>nat set) (Eps Q)"
+lemma "(Q \<Colon> nat \<Rightarrow> bool) (Eps Q)"
nitpick [expect = none] (* unfortunate *)
oops
-lemma "\<not> Q (Eps Q)"
+lemma "\<not> (Q \<Colon> nat \<Rightarrow> bool) (Eps Q)"
nitpick [expect = genuine]
oops
-lemma "\<not> (Q\<Colon>nat set) (Eps Q)"
+lemma "\<not> (Q \<Colon> nat \<Rightarrow> bool) (Eps Q)"
nitpick [expect = genuine]
oops
-lemma "(Q\<Colon>'a set) \<noteq> {} \<Longrightarrow> (Q\<Colon>'a set) (Eps Q)"
+lemma "(Q \<Colon> 'a \<Rightarrow> bool) \<noteq> bot \<Longrightarrow> Q (Eps Q)"
nitpick [expect = none]
sorry
-lemma "(Q\<Colon>nat set) \<noteq> {} \<Longrightarrow> (Q\<Colon>nat set) (Eps Q)"
+lemma "(Q \<Colon> nat \<Rightarrow> bool) \<noteq> top \<Longrightarrow> Q (Eps Q)"
nitpick [expect = none]
sorry
@@ -843,7 +833,7 @@
nitpick [expect = genuine]
oops
-lemma "(Q\<Colon>nat set) (The Q)"
+lemma "(Q \<Colon> nat \<Rightarrow> bool) (The Q)"
nitpick [expect = genuine]
oops
@@ -851,7 +841,7 @@
nitpick [expect = genuine]
oops
-lemma "\<not> (Q\<Colon>nat set) (The Q)"
+lemma "\<not> (Q \<Colon> nat \<Rightarrow> bool) (The Q)"
nitpick [expect = genuine]
oops
@@ -871,11 +861,11 @@
nitpick [expect = genuine]
oops
-lemma "Q = {x\<Colon>'a} \<Longrightarrow> (Q\<Colon>'a set) (The Q)"
+lemma "Q = {x\<Colon>'a} \<Longrightarrow> (The Q) \<in> (Q\<Colon>'a set)"
nitpick [expect = none]
sorry
-lemma "Q = {x\<Colon>nat} \<Longrightarrow> (Q\<Colon>nat set) (The Q)"
+lemma "Q = {x\<Colon>nat} \<Longrightarrow> (The Q) \<in> (Q\<Colon>nat set)"
nitpick [expect = none]
sorry
--- a/src/HOL/Nitpick_Examples/Induct_Nits.thy Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy Sat Dec 24 15:53:10 2011 +0100
@@ -54,23 +54,23 @@
coinductive q2 :: "nat \<Rightarrow> bool" where
"q2 n \<Longrightarrow> q2 n"
-lemma "p2 = {}"
+lemma "p2 = bot"
nitpick [expect = none]
nitpick [dont_star_linear_preds, expect = none]
sorry
-lemma "q2 = {}"
+lemma "q2 = bot"
nitpick [expect = genuine]
nitpick [dont_star_linear_preds, expect = genuine]
nitpick [wf, expect = quasi_genuine]
oops
-lemma "p2 = UNIV"
+lemma "p2 = top"
nitpick [expect = genuine]
nitpick [dont_star_linear_preds, expect = genuine]
oops
-lemma "q2 = UNIV"
+lemma "q2 = top"
nitpick [expect = none]
nitpick [dont_star_linear_preds, expect = none]
nitpick [wf, expect = quasi_genuine]
@@ -123,32 +123,32 @@
nitpick [non_wf, expect = none]
sorry
-lemma "p3 = UNIV - p4"
+lemma "p3 = top - p4"
nitpick [expect = none]
nitpick [non_wf, expect = none]
sorry
-lemma "q3 = UNIV - q4"
+lemma "q3 = top - q4"
nitpick [expect = none]
nitpick [non_wf, expect = none]
sorry
-lemma "p3 \<inter> q4 \<noteq> {}"
+lemma "inf p3 q4 \<noteq> bot"
nitpick [expect = potential]
nitpick [non_wf, expect = potential]
sorry
-lemma "q3 \<inter> p4 \<noteq> {}"
+lemma "inf q3 p4 \<noteq> bot"
nitpick [expect = potential]
nitpick [non_wf, expect = potential]
sorry
-lemma "p3 \<union> q4 \<noteq> UNIV"
+lemma "sup p3 q4 \<noteq> top"
nitpick [expect = potential]
nitpick [non_wf, expect = potential]
sorry
-lemma "q3 \<union> p4 \<noteq> UNIV"
+lemma "sup q3 p4 \<noteq> top"
nitpick [expect = potential]
nitpick [non_wf, expect = potential]
sorry
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Sat Dec 24 15:53:10 2011 +0100
@@ -179,7 +179,7 @@
coinductive nats where
"nats (x\<Colon>nat) \<Longrightarrow> nats x"
-lemma "nats = {0, 1, 2, 3, 4}"
+lemma "nats = (\<lambda>n. n \<in> {0, 1, 2, 3, 4})"
nitpick [card nat = 10, show_consts, expect = genuine]
oops
--- a/src/HOL/Nitpick_Examples/Mini_Nits.thy Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy Sat Dec 24 15:53:10 2011 +0100
@@ -68,13 +68,13 @@
ML {* genuine 1 @{prop "{a} \<noteq> {a, b}"} *}
ML {* none 5 @{prop "{}\<^sup>+ = {}"} *}
ML {* none 5 @{prop "UNIV\<^sup>+ = UNIV"} *}
-ML {* none 5 @{prop "(UNIV\<Colon>'a \<times> 'b \<Rightarrow> bool) - {} = UNIV"} *}
-ML {* none 5 @{prop "{} - (UNIV\<Colon>'a \<times> 'b \<Rightarrow> bool) = {}"} *}
+ML {* none 5 @{prop "(UNIV \<Colon> ('a \<times> 'b) set) - {} = UNIV"} *}
+ML {* none 5 @{prop "{} - (UNIV \<Colon> ('a \<times> 'b) set) = {}"} *}
ML {* none 1 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
ML {* genuine 2 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
ML {* none 5 @{prop "a \<noteq> c \<Longrightarrow> {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
-ML {* none 5 @{prop "A \<union> B = (\<lambda>x. A x \<or> B x)"} *}
-ML {* none 5 @{prop "A \<inter> B = (\<lambda>x. A x \<and> B x)"} *}
+ML {* none 5 @{prop "A \<union> B = {x. x \<in> A \<or> x \<in> B}"} *}
+ML {* none 5 @{prop "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"} *}
ML {* none 5 @{prop "A - B = (\<lambda>x. A x \<and> \<not> B x)"} *}
ML {* none 5 @{prop "\<exists>a b. (a, b) = (b, a)"} *}
ML {* genuine 2 @{prop "(a, b) = (b, a)"} *}
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Sat Dec 24 15:53:10 2011 +0100
@@ -52,7 +52,8 @@
nitpick [card = 2, expect = none]
oops
-definition "bounded = {n\<Colon>nat. finite (UNIV\<Colon>'a \<Rightarrow> bool) \<longrightarrow> n < card (UNIV\<Colon>'a \<Rightarrow> bool)}"
+definition "bounded = {n\<Colon>nat. finite (UNIV \<Colon> 'a set) \<longrightarrow> n < card (UNIV \<Colon> 'a set)}"
+
typedef (open) 'a bounded = "bounded(TYPE('a))"
unfolding bounded_def
apply (rule_tac x = 0 in exI)
--- a/src/HOL/Predicate.thy Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Predicate.thy Sat Dec 24 15:53:10 2011 +0100
@@ -74,19 +74,19 @@
subsubsection {* Equality *}
lemma pred_equals_eq: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)"
- by (simp add: set_eq_iff fun_eq_iff mem_def)
+ by (simp add: set_eq_iff fun_eq_iff)
lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R = S)"
- by (simp add: set_eq_iff fun_eq_iff mem_def)
+ by (simp add: set_eq_iff fun_eq_iff)
subsubsection {* Order relation *}
lemma pred_subset_eq: "((\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
- by (simp add: subset_iff le_fun_def mem_def)
+ by (simp add: subset_iff le_fun_def)
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)"
- by (simp add: subset_iff le_fun_def mem_def)
+ by (simp add: subset_iff le_fun_def)
subsubsection {* Top and bottom elements *}
@@ -137,10 +137,10 @@
by (simp add: inf_fun_def)
lemma inf_Int_eq: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
- by (simp add: inf_fun_def mem_def)
+ by (simp add: inf_fun_def)
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)"
- by (simp add: inf_fun_def mem_def)
+ by (simp add: inf_fun_def)
subsubsection {* Binary union *}
@@ -175,10 +175,10 @@
by (auto simp add: sup_fun_def)
lemma sup_Un_eq: "(\<lambda>x. x \<in> R) \<squnion> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
- by (simp add: sup_fun_def mem_def)
+ by (simp add: sup_fun_def)
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)"
- by (simp add: sup_fun_def mem_def)
+ by (simp add: sup_fun_def)
subsubsection {* Intersections of families *}
@@ -578,8 +578,8 @@
lemma not_bot:
assumes "A \<noteq> \<bottom>"
obtains x where "eval A x"
- using assms by (cases A) (auto simp add: bot_pred_def, simp add: mem_def)
-
+ using assms by (cases A) (auto simp add: bot_pred_def)
+
subsubsection {* Emptiness check and definite choice *}
@@ -1017,14 +1017,6 @@
end;
*}
-lemma eval_mem [simp]:
- "x \<in> eval P \<longleftrightarrow> eval P x"
- by (simp add: mem_def)
-
-lemma eq_mem [simp]:
- "x \<in> (op =) y \<longleftrightarrow> x = y"
- by (auto simp add: mem_def)
-
no_notation
bot ("\<bottom>") and
top ("\<top>") and
--- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Sat Dec 24 15:53:10 2011 +0100
@@ -1,9 +1,9 @@
theory Context_Free_Grammar_Example
imports "~~/src/HOL/Library/Code_Prolog"
begin
-
+(*
declare mem_def[code_pred_inline]
-
+*)
subsection {* Alternative rules for length *}
@@ -32,7 +32,7 @@
| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
lemma
- "w \<in> S\<^isub>1 \<Longrightarrow> w = []"
+ "S\<^isub>1p w \<Longrightarrow> w = []"
quickcheck[tester = prolog, iterations=1, expect = counterexample]
oops
@@ -60,13 +60,13 @@
{ensure_groundness = true,
limit_globally = NONE,
limited_types = [],
- limited_predicates = [(["s1", "a1", "b1"], 2)],
- replacing = [(("s1", "limited_s1"), "quickcheck")],
+ limited_predicates = [(["s1p", "a1p", "b1p"], 2)],
+ replacing = [(("s1p", "limited_s1p"), "quickcheck")],
manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
theorem S\<^isub>1_sound:
-"w \<in> S\<^isub>1 \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+"S\<^isub>1p w \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
quickcheck[tester = prolog, iterations=1, expect = counterexample]
oops
@@ -84,13 +84,13 @@
{ensure_groundness = true,
limit_globally = NONE,
limited_types = [],
- limited_predicates = [(["s2", "a2", "b2"], 3)],
- replacing = [(("s2", "limited_s2"), "quickcheck")],
+ limited_predicates = [(["s2p", "a2p", "b2p"], 3)],
+ replacing = [(("s2p", "limited_s2p"), "quickcheck")],
manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
theorem S\<^isub>2_sound:
-"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+ "S\<^isub>2p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
quickcheck[tester = prolog, iterations=1, expect = counterexample]
oops
@@ -107,12 +107,12 @@
{ensure_groundness = true,
limit_globally = NONE,
limited_types = [],
- limited_predicates = [(["s3", "a3", "b3"], 6)],
- replacing = [(("s3", "limited_s3"), "quickcheck")],
+ limited_predicates = [(["s3p", "a3p", "b3p"], 6)],
+ replacing = [(("s3p", "limited_s3p"), "quickcheck")],
manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
lemma S\<^isub>3_sound:
-"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+ "S\<^isub>3p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
quickcheck[tester = prolog, iterations=1, size=1, expect = no_counterexample]
oops
@@ -149,13 +149,13 @@
{ensure_groundness = true,
limit_globally = NONE,
limited_types = [],
- limited_predicates = [(["s4", "a4", "b4"], 6)],
- replacing = [(("s4", "limited_s4"), "quickcheck")],
+ limited_predicates = [(["s4p", "a4p", "b4p"], 6)],
+ replacing = [(("s4p", "limited_s4p"), "quickcheck")],
manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
theorem S\<^isub>4_sound:
-"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+ "S\<^isub>4p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
quickcheck[tester = prolog, size=1, iterations=1, expect = no_counterexample]
oops
--- a/src/HOL/Predicate_Compile_Examples/Examples.thy Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Examples.thy Sat Dec 24 15:53:10 2011 +0100
@@ -29,28 +29,44 @@
(s1 @ rhs @ s2) = rsl \<and>
(rule lhs rhs) \<in> fst g }"
+definition derivesp :: "(('nts, 'ts) rule => bool) * 'nts => ('nts, 'ts) symbol list => ('nts, 'ts) symbol list => bool"
+where
+ "derivesp g = (\<lambda> lhs rhs. (lhs, rhs) \<in> derives (Collect (fst g), snd g))"
+
+lemma [code_pred_def]:
+ "derivesp g = (\<lambda> lsl rsl. \<exists>s1 s2 lhs rhs.
+ (s1 @ [NTS lhs] @ s2 = lsl) \<and>
+ (s1 @ rhs @ s2) = rsl \<and>
+ (fst g) (rule lhs rhs))"
+unfolding derivesp_def derives_def by auto
+
abbreviation "example_grammar ==
({ rule ''S'' [NTS ''A'', NTS ''B''],
rule ''S'' [TS ''a''],
rule ''A'' [TS ''b'']}, ''S'')"
-
-code_pred [inductify, skip_proof] derives .
+definition "example_rules ==
+(%x. x = rule ''S'' [NTS ''A'', NTS ''B''] \<or>
+ x = rule ''S'' [TS ''a''] \<or>
+ x = rule ''A'' [TS ''b''])"
-thm derives.equation
-definition "test = { rhs. derives example_grammar ([NTS ''S''], rhs) }"
+code_pred [inductify, skip_proof] derivesp .
+
+thm derivesp.equation
-code_pred (modes: o \<Rightarrow> bool) [inductify] test .
-thm test.equation
+definition "testp = (% rhs. derivesp (example_rules, ''S'') [NTS ''S''] rhs)"
-values "{rhs. test rhs}"
+code_pred (modes: o \<Rightarrow> bool) [inductify] testp .
+thm testp.equation
-declare rtrancl.intros(1)[code_pred_def] converse_rtrancl_into_rtrancl[code_pred_def]
+values "{rhs. testp rhs}"
+
+declare rtranclp.intros(1)[code_pred_def] converse_rtranclp_into_rtranclp[code_pred_def]
-code_pred [inductify] rtrancl .
+code_pred [inductify] rtranclp .
-definition "test2 = { rhs. ([NTS ''S''],rhs) \<in> (derives example_grammar)^* }"
+definition "test2 = (\<lambda> rhs. rtranclp (derivesp (example_rules, ''S'')) [NTS ''S''] rhs)"
code_pred [inductify, skip_proof] test2 .
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy Sat Dec 24 15:53:10 2011 +0100
@@ -6,12 +6,68 @@
begin
declare Let_def[code_pred_inline]
-
+(*
+thm hotel_def
lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
+*)
+
+definition issuedp :: "event list => key => bool"
+where
+ "issuedp evs k = (k \<in> issued evs)"
+
+lemma [code_pred_def]:
+ "issuedp [] Key0 = True"
+ "issuedp (e # s) k = (issuedp s k \<or> (case e of Check_in g r (k1, k2) => k = k2 | _ => False))"
+unfolding issuedp_def issued.simps initk_def
+by (auto split: event.split)
+
+definition cardsp
+where
+ "cardsp s g k = (k \<in> cards s g)"
+
+lemma [code_pred_def]:
+ "cardsp [] g k = False"
+ "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)"
+unfolding cardsp_def_raw cards.simps by (auto simp add: Let_def split: event.split)
+
+definition
+ "isinp evs r g = (g \<in> isin evs r)"
+
+lemma [code_pred_def]:
+ "isinp [] r g = False"
+ "isinp (e # s) r g =
+ (let G = isinp s r
+ in case e of Check_in g' r c => G g
+ | Enter g' r' c => if r' = r then g = g' \<or> G g else G g
+ | Exit g' r' => if r' = r then ((g \<noteq> g') \<and> G g) else G g)"
+unfolding isinp_def_raw isin.simps by (auto simp add: Let_def split: event.split)
+
+declare hotel.simps(1)[code_pred_def]
+lemma [code_pred_def]:
+"hotel (e # s) =
+ (hotel s & (case e of Check_in g r (k, k') => k = currk s r & \<not> issuedp s k'
+ | Enter g r (k, k') => cardsp s g (k, k') & (roomk s r = k \<or> roomk s r = k')
+ | Exit g r => isinp s r g))"
+unfolding hotel.simps issuedp_def cardsp_def isinp_def
+by (auto split: event.split)
+
+declare List.member_rec[code_pred_def]
+
+lemma [code_pred_def]: "no_Check_in s r = (~ (EX g c. List.member s (Check_in g r c)))"
+unfolding no_Check_in_def member_def by auto
+
+lemma [code_pred_def]: "feels_safe s r =
+(EX s\<^isub>1 s\<^isub>2 s\<^isub>3 g c c'.
+ s =
+ s\<^isub>3 @
+ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 &
+ no_Check_in (s\<^isub>3 @ s\<^isub>2) r &
+ (\<not> (\<exists> g'. isinp (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r g')))"
+unfolding feels_safe_def isinp_def by auto
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
@@ -25,8 +81,7 @@
setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
-lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
-quickcheck[tester = random, iterations = 10000, report]
+lemma "\<lbrakk> hotel s; isinp s r g \<rbrakk> \<Longrightarrow> owns s r = Some g"
quickcheck[tester = prolog, iterations = 1, expect = counterexample]
oops
@@ -41,7 +96,7 @@
manual_reorder = []}) *}
lemma
- "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+ "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
oops
@@ -54,52 +109,18 @@
manual_reorder = []}) *}
lemma
- "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[tester = prolog, iterations = 1, expect = counterexample]
-oops
-
-section {* Simulating a global depth limit manually by limiting all predicates *}
-
-setup {*
- Code_Prolog.map_code_options (K
- {ensure_groundness = true,
- limit_globally = NONE,
- limited_types = [],
- limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
- "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 12)],
- replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
- manual_reorder = []})
-*}
-
-lemma
- "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
-oops
-
-setup {*
- Code_Prolog.map_code_options (K
- {ensure_groundness = true,
- limit_globally = NONE,
- limited_types = [],
- limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
- "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 13)],
- replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
- manual_reorder = []})
-*}
-
-lemma
- "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+ "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
quickcheck[tester = prolog, iterations = 1, expect = counterexample]
oops
section {* Using a global limit for limiting the execution *}
-text {* A global depth limit of 13 does not suffice to find the counterexample. *}
+text {* A global depth limit of 10 does not suffice to find the counterexample. *}
setup {*
Code_Prolog.map_code_options (K
{ensure_groundness = true,
- limit_globally = SOME 13,
+ limit_globally = SOME 10,
limited_types = [],
limited_predicates = [],
replacing = [],
@@ -107,16 +128,16 @@
*}
lemma
- "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+ "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
oops
-text {* But a global depth limit of 14 does. *}
+text {* But a global depth limit of 11 does. *}
setup {*
Code_Prolog.map_code_options (K
{ensure_groundness = true,
- limit_globally = SOME 14,
+ limit_globally = SOME 11,
limited_types = [],
limited_predicates = [],
replacing = [],
@@ -124,7 +145,7 @@
*}
lemma
- "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+ "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
quickcheck[tester = prolog, iterations = 1, expect = counterexample]
oops
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Sat Dec 24 15:53:10 2011 +0100
@@ -38,14 +38,14 @@
values [expected "{()}" random_dseq 1, 1, 2] "{x. True'}"
values [expected "{()}" random_dseq 1, 1, 3] "{x. True'}"
-inductive EmptySet :: "'a \<Rightarrow> bool"
+inductive EmptyPred :: "'a \<Rightarrow> bool"
-code_pred (expected_modes: o => bool, i => bool) EmptySet .
+code_pred (expected_modes: o => bool, i => bool) EmptyPred .
-definition EmptySet' :: "'a \<Rightarrow> bool"
-where "EmptySet' = {}"
+definition EmptyPred' :: "'a \<Rightarrow> bool"
+where "EmptyPred' = (\<lambda> x. False)"
-code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' .
+code_pred (expected_modes: o => bool, i => bool) [inductify] EmptyPred' .
inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
@@ -296,7 +296,7 @@
lemma zerozero'_eq: "zerozero' x == zerozero x"
proof -
have "zerozero' = zerozero"
- apply (auto simp add: mem_def)
+ apply (auto simp add: fun_eq_iff)
apply (cases rule: zerozero'.cases)
apply (auto simp add: equals_def intro: zerozero.intros)
apply (cases rule: zerozero.cases)
@@ -313,10 +313,21 @@
code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' .
-subsection {* Sets and Numerals *}
+subsection {* Sets *}
+(*
+inductive_set EmptySet :: "'a set"
+
+code_pred (expected_modes: o => bool, i => bool) EmptySet .
+
+definition EmptySet' :: "'a set"
+where "EmptySet' = {}"
+
+code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' .
+*)
+subsection {* Numerals *}
definition
- "one_or_two = {Suc 0, (Suc (Suc 0))}"
+ "one_or_two = (%x. x = Suc 0 \<or> ( x = Suc (Suc 0)))"
code_pred [inductify] one_or_two .
@@ -337,7 +348,7 @@
values "{x. one_or_two' x}"
definition one_or_two'':
- "one_or_two'' == {1, (2::nat)}"
+ "one_or_two'' == (%x. x = 1 \<or> x = (2::nat))"
code_pred [inductify] one_or_two'' .
thm one_or_two''.equation
@@ -847,7 +858,10 @@
thm Min.equation
subsection {* Lexicographic order *}
+text {* This example requires to handle the differences of sets and predicates in the predicate compiler,
+or to have a copy of all definitions on predicates due to the set-predicate distinction. *}
+(*
declare lexord_def[code_pred_def]
code_pred [inductify] lexord .
code_pred [random_dseq inductify] lexord .
@@ -889,6 +903,7 @@
values [random_dseq 4, 4, 6] 100 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
*)
+
inductive has_length
where
"has_length [] 0"
@@ -956,7 +971,7 @@
thm lists.intros
code_pred [inductify] lists .
thm lists.equation
-
+*)
subsection {* AVL Tree *}
datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
@@ -990,16 +1005,16 @@
| "is_ord (MKT n l r h) =
((\<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)"
+(*
code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] set_of .
thm set_of.equation
code_pred (expected_modes: i => bool) [inductify] is_ord .
thm is_ord_aux.equation
thm is_ord.equation
-
+*)
subsection {* Definitions about Relations *}
-
-term "converse"
+(*
code_pred (modes:
(i * i => bool) => i * i => bool,
(i * o => bool) => o * i => bool,
@@ -1059,10 +1074,10 @@
thm inv_image_def
code_pred [inductify] inv_image .
thm inv_image.equation
-
+*)
subsection {* Inverting list functions *}
-code_pred [inductify] size_list .
+code_pred [inductify, skip_proof] size_list .
code_pred [new_random_dseq inductify] size_list .
thm size_listP.equation
thm size_listP.new_random_dseq_equation
@@ -1115,11 +1130,12 @@
thm zipP.equation
code_pred [inductify, skip_proof] upt .
+(*
code_pred [inductify, skip_proof] remdups .
thm remdupsP.equation
code_pred [dseq inductify] remdups .
values [dseq 4] 5 "{xs. remdupsP xs [1, (2::int)]}"
-
+*)
code_pred [inductify, skip_proof] remove1 .
thm remove1P.equation
values "{xs. remove1P 1 xs [2, (3::int)]}"
@@ -1129,9 +1145,10 @@
code_pred [dseq inductify] removeAll .
values [dseq 4] 10 "{xs. removeAllP 1 xs [(2::nat)]}"
-
+(*
code_pred [inductify] distinct .
thm distinct.equation
+*)
code_pred [inductify, skip_proof] replicate .
thm replicateP.equation
values 5 "{(n, xs). replicateP n (0::int) xs}"
--- a/src/HOL/Quotient_Examples/Lift_Set.thy Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Quotient_Examples/Lift_Set.thy Sat Dec 24 15:53:10 2011 +0100
@@ -8,9 +8,9 @@
imports Main
begin
-definition set where "set = (UNIV :: ('a => bool) => bool)"
+definition set where "set = (UNIV :: ('a \<Rightarrow> bool) set)"
-typedef (open) 'a set = "set :: 'a set set"
+typedef (open) 'a set = "set :: ('a \<Rightarrow> bool) set"
morphisms member Set
unfolding set_def by auto
@@ -37,15 +37,19 @@
text {* Now, we can employ quotient_definition to lift definitions. *}
quotient_definition empty where "empty :: 'a set"
-is "Set.empty"
+is "bot :: 'a \<Rightarrow> bool"
term "Lift_Set.empty"
thm Lift_Set.empty_def
+definition insertp :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
+ "insertp x P y \<longleftrightarrow> y = x \<or> P y"
+
quotient_definition insert where "insert :: 'a => 'a set => 'a set"
-is "Set.insert"
+is insertp
term "Lift_Set.insert"
thm Lift_Set.insert_def
end
+
--- a/src/HOL/Wellfounded.thy Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Wellfounded.thy Sat Dec 24 15:53:10 2011 +0100
@@ -298,8 +298,10 @@
lemma wfP_SUP:
"\<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)"
- by (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred SUP_UN_eq2])
- (simp_all add: Collect_def)
+ apply (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred SUP_UN_eq2])
+ apply (simp_all add: inf_set_def)
+ apply auto
+ done
lemma wf_Union:
"[| ALL r:R. wf r;