# HG changeset patch # User haftmann # Date 1324738390 -3600 # Node ID b6d0cff57d9682f9b3e84bc310431b52339d3ccb # Parent 562e99c3d3166d364f8819918184a1ced315db46 adjusted to set/pred distinction by means of type constructor `set` diff -r 562e99c3d316 -r b6d0cff57d96 src/HOL/Library/Cset.thy --- 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 \ 'a \ bool" where "member A x \ x \ 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 \ x \ A" by (simp add: member_def) @@ -38,7 +34,7 @@ lemma set_eq_iff: "A = B \ 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 \ Cset.empty | Predicate.Insert x P \ Cset.insert x (of_pred P) | Predicate.Join P xq \ 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 \ 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 (\x. x \ 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 = \" - 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 diff -r 562e99c3d316 -r b6d0cff57d96 src/HOL/Library/Predicate_Compile_Alternative_Defs.thy --- 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 \ \ 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) == ((\x. Q x \ (\ P x)) \ (\ 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) = ((\x. A x \ B x) \ (\x. B x \ A x))" -by (fastforce simp add: mem_def) + "A = B \ (\x. A x \ B x) \ (\x. B x \ 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 diff -r 562e99c3d316 -r b6d0cff57d96 src/HOL/Library/Quotient_Set.thy --- 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 \) = op \" -using Quotient_abs_rep[OF assms] -by(simp add: fun_eq_iff mem_def) - -lemma mem_rsp[quot_respect]: - "(R ===> (R ===> op =) ===> op =) (op \) (op \)" - 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 \ = op \" 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 \ op \" by (intro fun_relI) (simp add: set_rel_def) diff -r 562e99c3d316 -r b6d0cff57d96 src/HOL/Metis_Examples/Message.thy --- 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\ parts G; G \ parts H |] ==> X\ parts H" by (blast dest: parts_mono) -lemma parts_cut: "[|Y\ parts (insert X G); X\ parts H|] ==> Y\ parts(G \ H)" -by (metis Un_insert_left Un_insert_right insert_absorb mem_def parts_Un parts_idem sup1CI) +(*lemma parts_cut: "[|Y\ parts (insert X G); X\ parts H|] ==> Y\ parts(G \ 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\ G ==> parts(insert X H) \ parts G \ parts H" +lemma parts_insert_subset_Un: "X \ G ==> parts(insert X H) \ parts G \ parts H" proof - assume "X \ G" - hence "G X" by (metis mem_def) - hence "\x\<^isub>1. G \ x\<^isub>1 \ x\<^isub>1 X" by (metis predicate1D) - hence "\x\<^isub>1. (G \ x\<^isub>1) X" by (metis Un_upper1) - hence "\x\<^isub>1. X \ G \ x\<^isub>1" by (metis mem_def) + hence "\x\<^isub>1. G \ x\<^isub>1 \ X \ x\<^isub>1 " by auto + hence "\x\<^isub>1. X \ G \ x\<^isub>1" by (metis Un_upper1) hence "insert X H \ G \ H" by (metis Un_upper2 insert_subset) hence "parts (insert X H) \ parts (G \ H)" by (metis parts_mono) thus "parts (insert X H) \ parts G \ parts H" by (metis parts_Un) @@ -716,10 +715,10 @@ by (metis analz_idem analz_synth) have F2: "\x\<^isub>1. parts x\<^isub>1 \ 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 \ synth (analz H)" using A1 by metis have "\x\<^isub>2 x\<^isub>1\msg set. x\<^isub>1 \ sup x\<^isub>1 x\<^isub>2" by (metis inf_sup_ord(3)) hence F4: "\x\<^isub>1. analz x\<^isub>1 \ analz (synth x\<^isub>1)" by (metis analz_synth) - have F5: "X \ synth (analz H)" using F3 by (metis mem_def) + have F5: "X \ synth (analz H)" using F3 by metis have "\x\<^isub>1. analz x\<^isub>1 \ synth (analz x\<^isub>1) \ analz (synth (analz x\<^isub>1)) = synth (analz x\<^isub>1)" using F1 by (metis subset_Un_eq) @@ -741,7 +740,7 @@ ==> Z \ synth (analz H) \ 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 \ synth (analz G) ==> diff -r 562e99c3d316 -r b6d0cff57d96 src/HOL/Metis_Examples/Proxies.thy --- 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 \ 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) \ y \ 0" definition "C (y::int) \ y \ 1" @@ -49,7 +49,7 @@ lemma int_le_0_imp_le_1: "x \ (0::int) \ x \ 1" by linarith -lemma "B \ C" +lemma "B \ 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 (\ (id (\ a))) \ id a" sledgehammer [type_enc = erased, expect = some] (id_apply) diff -r 562e99c3d316 -r b6d0cff57d96 src/HOL/Metis_Examples/Tarski.thy --- 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 \ 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) \ r \ x \ A} cl \ A" using A1 by metis next assume A1: "H = {x. (x, f x) \ r \ x \ A}" - have F1: "\v. (\R. R \ v) = v" by (metis Collect_mem_eq Collect_def) - have F2: "\w u. (\R. u R \ w R) = u \ w" - by (metis Collect_conj_eq Collect_def) - have F3: "\x v. (\R. v R \ x) = v -` x" by (metis vimage_def Collect_def) + have F1: "\v. {R. R \ v} = v" by (metis Collect_mem_eq) + have F2: "\w u. {R. R \ u \ R \ w} = u \ w" + by (metis Collect_conj_eq Collect_mem_eq) + have F3: "\x v. {R. v R \ x} = v -` x" by (metis vimage_def) hence F4: "A \ (\R. (R, f R)) -` r = H" using A1 by auto - hence F5: "(f (lub H cl), lub H cl) \ r" - by (metis F1 F3 F2 Int_commute flubH_le_lubH Collect_def) + hence F5: "(f (lub H cl), lub H cl) \ r" + by (metis A1 flubH_le_lubH) have F6: "(lub H cl, f (lub H cl)) \ 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)) \ r \ 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) \ r \ x \ A} \ f (lub {x. (x, f x) \ r \ x \ A} cl) = lub {x. (x, f x) \ r \ x \ A} cl" - by (metis F4 F2 F3 F1 Collect_def Int_commute) + by metis qed lemma (in CLF) (*lubH_is_fixp:*) diff -r 562e99c3d316 -r b6d0cff57d96 src/HOL/Metis_Examples/Trans_Closure.thy --- 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: "\y. f b = Intg y \ y \ x" assume A3: "(a, b) \ R\<^sup>*" assume A4: "(b, c) \ R\<^sup>*" - have "(R\<^sup>*) (a, b)" using A3 by (metis mem_def) - hence F1: "(a, b) \ R\<^sup>*" by (metis mem_def) have "b \ c" using A1 A2 by metis hence "\x\<^isub>1. (b, x\<^isub>1) \ R" using A4 by (metis converse_rtranclE) - thus "\c. (b, c) \ R \ (a, c) \ R\<^sup>*" using F1 by (metis transitive_closure_trans(6)) + thus "\c. (b, c) \ R \ (a, c) \ R\<^sup>*" using A3 by (metis transitive_closure_trans(6)) qed lemma "\f c = Intg x; \y. f b = Intg y \ y \ x; (a, b) \ R\<^sup>*; (b, c) \ R\<^sup>*\ diff -r 562e99c3d316 -r b6d0cff57d96 src/HOL/MicroJava/BV/BVExample.thy --- 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 (\(ss, w). \ is_empty w) + "iter f step ss w = while (\(ss, w). \ More_Set.is_empty w) (\(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 \ 's \ bool) \ (nat \ 's \ (nat \ 's) list) \ 's list \ 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 diff -r 562e99c3d316 -r b6d0cff57d96 src/HOL/MicroJava/J/TypeRel.thy --- 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 \ i \ o \ bool, i \ i \ i \ bool) subcls1p . -declare subcls1_def[unfolded Collect_def, code_pred_def] + +declare subcls1_def [code_pred_def] + code_pred (modes: i \ i \ o \ bool, i \ i \ i \ bool) [inductify] @@ -92,14 +96,16 @@ . definition subcls' where "subcls' G = (subcls1p G)^**" + code_pred (modes: i \ i \ i \ bool, i \ i \ o \ bool) [inductify] subcls' -. + . + lemma subcls_conv_subcls' [code_unfold]: - "(subcls1 G)^* = (\(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 (\(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 (\(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 diff -r 562e99c3d316 -r b6d0cff57d96 src/HOL/Nitpick.thy --- 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 \ \x. P = {x}" +"Ex1 P \ \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>* \ (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 \ trancl (split r) (a, b)" -by (simp add: trancl_def Collect_def mem_def) +"tranclp r a b \ (a, b) \ trancl {(x, y). r x y}" +by (simp add: trancl_def) definition prod :: "'a set \ 'b set \ ('a \ 'b) set" where "prod A B = {(a, b). a \ A \ b \ B}" @@ -98,8 +98,8 @@ *} lemma The_psimp [nitpick_psimp, no_atp]: -"P = {x} \ The P = x" -by (subgoal_tac "{x} = (\y. y = x)") (auto simp: mem_def) + "P = (op =) x \ The P = x" + by auto lemma Eps_psimp [nitpick_psimp, no_atp]: "\P x; \ P y; Eps P = y\ \ Eps P = x" diff -r 562e99c3d316 -r b6d0cff57d96 src/HOL/Nitpick_Examples/Core_Nits.thy --- 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\4, expect = none] by auto -lemma "Id (a, a)" +lemma "(a, a) \ Id" nitpick [card = 1\50, expect = none] -by (auto simp: Id_def Collect_def) +by (auto simp: Id_def) -lemma "Id ((a\'a, b\'a), (a, b))" +lemma "((a\'a, b\'a), (a, b)) \ Id" nitpick [card = 1\10, expect = none] -by (auto simp: Id_def Collect_def) +by (auto simp: Id_def) -lemma "UNIV (x\'a\'a)" +lemma "(x\'a\'a) \ UNIV" nitpick [card = 1\50, expect = none] sorry @@ -539,13 +539,13 @@ nitpick [expect = none] by auto -lemma "I = (\x. x) \ Id = (\x. Id (I x))" +lemma "I = (\x. x) \ Id = {x. I x \ Id}" nitpick [expect = none] by auto -lemma "{} = (\x. False)" +lemma "{} = {x. False}" nitpick [expect = none] -by (metis Collect_def empty_def) +by (metis empty_def) lemma "x \ {}" nitpick [expect = genuine] @@ -571,33 +571,23 @@ nitpick [expect = none] by auto -lemma "UNIV = (\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 \ UNIV \ True" nitpick [expect = none] -by (simp only: UNIV_def Collect_def) +by (simp only: UNIV_def mem_Collect_eq) lemma "x \ UNIV" nitpick [expect = genuine] oops -lemma "op \ = (\x P. P x)" -nitpick [expect = none] -apply (rule ext) -apply (rule ext) -by (simp add: mem_def) - lemma "I = (\x. x) \ op \ = (\x. (op \ (I x)))" nitpick [expect = none] apply (rule ext) apply (rule ext) -by (simp add: mem_def) - -lemma "P x = (x \ P)" -nitpick [expect = none] -by (simp add: mem_def) +by simp lemma "insert = (\x y. insert x (y \ y))" nitpick [expect = none] @@ -753,7 +743,7 @@ nitpick [expect = genuine] oops -lemma "(P\nat set) (Eps P)" +lemma "Eps (\x. x \ P) \ (P\nat set)" nitpick [expect = genuine] oops @@ -761,15 +751,15 @@ nitpick [expect = genuine] oops -lemma "\ (P\nat set) (Eps P)" +lemma "\ (P \ nat \ bool) (Eps P)" nitpick [expect = genuine] oops -lemma "P \ {} \ P (Eps P)" +lemma "P \ bot \ P (Eps P)" nitpick [expect = none] sorry -lemma "(P\nat set) \ {} \ P (Eps P)" +lemma "(P \ nat \ bool) \ bot \ P (Eps P)" nitpick [expect = none] sorry @@ -777,7 +767,7 @@ nitpick [expect = genuine] oops -lemma "(P\nat set) (The P)" +lemma "(P \ nat \ bool) (The P)" nitpick [expect = genuine] oops @@ -785,7 +775,7 @@ nitpick [expect = genuine] oops -lemma "\ (P\nat set) (The P)" +lemma "\ (P \ nat \ bool) (The P)" nitpick [expect = genuine] oops @@ -805,11 +795,11 @@ nitpick [expect = genuine] oops -lemma "P = {x} \ P (The P)" +lemma "P = {x} \ (THE x. x \ P) \ P" nitpick [expect = none] oops -lemma "P = {x\nat} \ P (The P)" +lemma "P = {x\nat} \ (THE x. x \ P) \ P" nitpick [expect = none] oops @@ -819,23 +809,23 @@ nitpick [expect = genuine] oops -lemma "(Q\nat set) (Eps Q)" +lemma "(Q \ nat \ bool) (Eps Q)" nitpick [expect = none] (* unfortunate *) oops -lemma "\ Q (Eps Q)" +lemma "\ (Q \ nat \ bool) (Eps Q)" nitpick [expect = genuine] oops -lemma "\ (Q\nat set) (Eps Q)" +lemma "\ (Q \ nat \ bool) (Eps Q)" nitpick [expect = genuine] oops -lemma "(Q\'a set) \ {} \ (Q\'a set) (Eps Q)" +lemma "(Q \ 'a \ bool) \ bot \ Q (Eps Q)" nitpick [expect = none] sorry -lemma "(Q\nat set) \ {} \ (Q\nat set) (Eps Q)" +lemma "(Q \ nat \ bool) \ top \ Q (Eps Q)" nitpick [expect = none] sorry @@ -843,7 +833,7 @@ nitpick [expect = genuine] oops -lemma "(Q\nat set) (The Q)" +lemma "(Q \ nat \ bool) (The Q)" nitpick [expect = genuine] oops @@ -851,7 +841,7 @@ nitpick [expect = genuine] oops -lemma "\ (Q\nat set) (The Q)" +lemma "\ (Q \ nat \ bool) (The Q)" nitpick [expect = genuine] oops @@ -871,11 +861,11 @@ nitpick [expect = genuine] oops -lemma "Q = {x\'a} \ (Q\'a set) (The Q)" +lemma "Q = {x\'a} \ (The Q) \ (Q\'a set)" nitpick [expect = none] sorry -lemma "Q = {x\nat} \ (Q\nat set) (The Q)" +lemma "Q = {x\nat} \ (The Q) \ (Q\nat set)" nitpick [expect = none] sorry diff -r 562e99c3d316 -r b6d0cff57d96 src/HOL/Nitpick_Examples/Induct_Nits.thy --- 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 \ bool" where "q2 n \ 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 \ q4 \ {}" +lemma "inf p3 q4 \ bot" nitpick [expect = potential] nitpick [non_wf, expect = potential] sorry -lemma "q3 \ p4 \ {}" +lemma "inf q3 p4 \ bot" nitpick [expect = potential] nitpick [non_wf, expect = potential] sorry -lemma "p3 \ q4 \ UNIV" +lemma "sup p3 q4 \ top" nitpick [expect = potential] nitpick [non_wf, expect = potential] sorry -lemma "q3 \ p4 \ UNIV" +lemma "sup q3 p4 \ top" nitpick [expect = potential] nitpick [non_wf, expect = potential] sorry diff -r 562e99c3d316 -r b6d0cff57d96 src/HOL/Nitpick_Examples/Manual_Nits.thy --- 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\nat) \ nats x" -lemma "nats = {0, 1, 2, 3, 4}" +lemma "nats = (\n. n \ {0, 1, 2, 3, 4})" nitpick [card nat = 10, show_consts, expect = genuine] oops diff -r 562e99c3d316 -r b6d0cff57d96 src/HOL/Nitpick_Examples/Mini_Nits.thy --- 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} \ {a, b}"} *} ML {* none 5 @{prop "{}\<^sup>+ = {}"} *} ML {* none 5 @{prop "UNIV\<^sup>+ = UNIV"} *} -ML {* none 5 @{prop "(UNIV\'a \ 'b \ bool) - {} = UNIV"} *} -ML {* none 5 @{prop "{} - (UNIV\'a \ 'b \ bool) = {}"} *} +ML {* none 5 @{prop "(UNIV \ ('a \ 'b) set) - {} = UNIV"} *} +ML {* none 5 @{prop "{} - (UNIV \ ('a \ '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 \ c \ {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *} -ML {* none 5 @{prop "A \ B = (\x. A x \ B x)"} *} -ML {* none 5 @{prop "A \ B = (\x. A x \ B x)"} *} +ML {* none 5 @{prop "A \ B = {x. x \ A \ x \ B}"} *} +ML {* none 5 @{prop "A \ B = {x. x \ A \