# HG changeset patch # User wenzelm # Date 1511726912 -3600 # Node ID 1393c2340eec2eeff8b2859dee02e02d295392b4 # Parent 0ec94bb9cec4e68c4c6c6be0fd861f19cf39e5ec more symbols; diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Algebra/AbelCoset.thy --- a/src/HOL/Algebra/AbelCoset.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Algebra/AbelCoset.thy Sun Nov 26 21:08:32 2017 +0100 @@ -290,7 +290,7 @@ text\Alternative characterization of normal subgroups\ lemma (in abelian_group) a_normal_inv_iff: "(N \ \carrier = carrier G, mult = add G, one = zero G\) = - (subgroup N \carrier = carrier G, mult = add G, one = zero G\ & (\x \ carrier G. \h \ N. x \ h \ (\ x) \ N))" + (subgroup N \carrier = carrier G, mult = add G, one = zero G\ \ (\x \ carrier G. \h \ N. x \ h \ (\ x) \ N))" (is "_ = ?rhs") by (rule group.normal_inv_iff [OF a_group, folded a_inv_def, simplified monoid_record_simps]) diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Algebra/Bij.thy --- a/src/HOL/Algebra/Bij.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Algebra/Bij.thy Sun Nov 26 21:08:32 2017 +0100 @@ -67,7 +67,7 @@ shows "\h \ Bij S; g \ S \ S \ S; x \ S; y \ S\ \ inv_into S h (g x y) = g (inv_into S h x) (inv_into S h y)" apply (simp add: Bij_def bij_betw_def) -apply (subgoal_tac "\x'\S. \y'\S. x = h x' & y = h y'", clarify) +apply (subgoal_tac "\x'\S. \y'\S. x = h x' \ y = h y'", clarify) apply (simp add: eq [symmetric] inv_f_f funcset_mem [THEN funcset_mem], blast) done diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Algebra/Complete_Lattice.thy --- a/src/HOL/Algebra/Complete_Lattice.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Algebra/Complete_Lattice.thy Sun Nov 26 21:08:32 2017 +0100 @@ -14,9 +14,9 @@ locale weak_complete_lattice = weak_partial_order + assumes sup_exists: - "[| A \ carrier L |] ==> EX s. least L s (Upper L A)" + "[| A \ carrier L |] ==> \s. least L s (Upper L A)" and inf_exists: - "[| A \ carrier L |] ==> EX i. greatest L i (Lower L A)" + "[| A \ carrier L |] ==> \i. greatest L i (Lower L A)" sublocale weak_complete_lattice \ weak_lattice proof @@ -32,9 +32,9 @@ lemma (in weak_partial_order) weak_complete_latticeI: assumes sup_exists: - "!!A. [| A \ carrier L |] ==> EX s. least L s (Upper L A)" + "!!A. [| A \ carrier L |] ==> \s. least L s (Upper L A)" and inf_exists: - "!!A. [| A \ carrier L |] ==> EX i. greatest L i (Lower L A)" + "!!A. [| A \ carrier L |] ==> \i. greatest L i (Lower L A)" shows "weak_complete_lattice L" by standard (auto intro: sup_exists inf_exists) @@ -111,9 +111,9 @@ qed theorem (in weak_partial_order) weak_complete_lattice_criterion1: - assumes top_exists: "EX g. greatest L g (carrier L)" + assumes top_exists: "\g. greatest L g (carrier L)" and inf_exists: - "!!A. [| A \ carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)" + "\A. [| A \ carrier L; A \ {} |] ==> \i. greatest L i (Lower L A)" shows "weak_complete_lattice L" proof (rule weak_complete_latticeI) from top_exists obtain top where top: "greatest L top (carrier L)" .. @@ -121,7 +121,7 @@ assume L: "A \ carrier L" let ?B = "Upper L A" from L top have "top \ ?B" by (fast intro!: Upper_memI intro: greatest_le) - then have B_non_empty: "?B ~= {}" by fast + then have B_non_empty: "?B \ {}" by fast have B_L: "?B \ carrier L" by simp from inf_exists [OF B_L B_non_empty] obtain b where b_inf_B: "greatest L b (Lower L ?B)" .. @@ -139,11 +139,11 @@ apply (rule L) apply (rule greatest_closed [OF b_inf_B]) done - then show "EX s. least L s (Upper L A)" .. + then show "\s. least L s (Upper L A)" .. next fix A assume L: "A \ carrier L" - show "EX i. greatest L i (Lower L A)" + show "\i. greatest L i (Lower L A)" proof (cases "A = {}") case True then show ?thesis by (simp add: top_exists) @@ -547,9 +547,9 @@ locale complete_lattice = partial_order + assumes sup_exists: - "[| A \ carrier L |] ==> EX s. least L s (Upper L A)" + "[| A \ carrier L |] ==> \s. least L s (Upper L A)" and inf_exists: - "[| A \ carrier L |] ==> EX i. greatest L i (Lower L A)" + "[| A \ carrier L |] ==> \i. greatest L i (Lower L A)" sublocale complete_lattice \ lattice proof @@ -578,16 +578,16 @@ lemma (in partial_order) complete_latticeI: assumes sup_exists: - "!!A. [| A \ carrier L |] ==> EX s. least L s (Upper L A)" + "!!A. [| A \ carrier L |] ==> \s. least L s (Upper L A)" and inf_exists: - "!!A. [| A \ carrier L |] ==> EX i. greatest L i (Lower L A)" + "!!A. [| A \ carrier L |] ==> \i. greatest L i (Lower L A)" shows "complete_lattice L" by standard (auto intro: sup_exists inf_exists) theorem (in partial_order) complete_lattice_criterion1: - assumes top_exists: "EX g. greatest L g (carrier L)" + assumes top_exists: "\g. greatest L g (carrier L)" and inf_exists: - "!!A. [| A \ carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)" + "!!A. [| A \ carrier L; A \ {} |] ==> \i. greatest L i (Lower L A)" shows "complete_lattice L" proof (rule complete_latticeI) from top_exists obtain top where top: "greatest L top (carrier L)" .. @@ -595,7 +595,7 @@ assume L: "A \ carrier L" let ?B = "Upper L A" from L top have "top \ ?B" by (fast intro!: Upper_memI intro: greatest_le) - then have B_non_empty: "?B ~= {}" by fast + then have B_non_empty: "?B \ {}" by fast have B_L: "?B \ carrier L" by simp from inf_exists [OF B_L B_non_empty] obtain b where b_inf_B: "greatest L b (Lower L ?B)" .. @@ -613,11 +613,11 @@ apply (rule L) apply (rule greatest_closed [OF b_inf_B]) done - then show "EX s. least L s (Upper L A)" .. + then show "\s. least L s (Upper L A)" .. next fix A assume L: "A \ carrier L" - show "EX i. greatest L i (Lower L A)" + show "\i. greatest L i (Lower L A)" proof (cases "A = {}") case True then show ?thesis by (simp add: top_exists) @@ -1181,7 +1181,7 @@ assume "B \ carrier ?L" then have "least ?L (\ B) (Upper ?L B)" by (fastforce intro!: least_UpperI simp: Upper_def) - then show "EX s. least ?L s (Upper ?L B)" .. + then show "\s. least ?L s (Upper ?L B)" .. next fix B assume "B \ carrier ?L" @@ -1189,7 +1189,7 @@ txt \@{term "\ B"} is not the infimum of @{term B}: @{term "\ {} = UNIV"} which is in general bigger than @{term "A"}! \ by (fastforce intro!: greatest_LowerI simp: Lower_def) - then show "EX i. greatest ?L i (Lower ?L B)" .. + then show "\i. greatest ?L i (Lower ?L B)" .. qed text \Another example, that of the lattice of subgroups of a group, diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Algebra/Congruence.thy --- a/src/HOL/Algebra/Congruence.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Algebra/Congruence.thy Sun Nov 26 21:08:32 2017 +0100 @@ -52,15 +52,15 @@ abbreviation not_eq :: "_ \ 'a \ 'a \ bool" (infixl ".\\" 50) - where "x .\\<^bsub>S\<^esub> y == ~(x .=\<^bsub>S\<^esub> y)" + where "x .\\<^bsub>S\<^esub> y \ \(x .=\<^bsub>S\<^esub> y)" abbreviation not_elem :: "_ \ 'a \ 'a set \ bool" (infixl ".\\" 50) - where "x .\\<^bsub>S\<^esub> A == ~(x .\\<^bsub>S\<^esub> A)" + where "x .\\<^bsub>S\<^esub> A \ \(x .\\<^bsub>S\<^esub> A)" abbreviation set_not_eq :: "_ \ 'a set \ 'a set \ bool" (infixl "{.\}\" 50) - where "A {.\}\<^bsub>S\<^esub> B == ~(A {.=}\<^bsub>S\<^esub> B)" + where "A {.\}\<^bsub>S\<^esub> B \ \(A {.=}\<^bsub>S\<^esub> B)" locale equivalence = fixes S (structure) diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Algebra/Coset.thy --- a/src/HOL/Algebra/Coset.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Algebra/Coset.thy Sun Nov 26 21:08:32 2017 +0100 @@ -410,7 +410,7 @@ text\Alternative characterization of normal subgroups\ lemma (in group) normal_inv_iff: "(N \ G) = - (subgroup N G & (\x \ carrier G. \h \ N. x \ h \ (inv x) \ N))" + (subgroup N G \ (\x \ carrier G. \h \ N. x \ h \ (inv x) \ N))" (is "_ = ?rhs") proof assume N: "N \ G" @@ -476,7 +476,7 @@ assume "\h\H. y = x \ h" and x: "x \ carrier G" and sb: "subgroup H G" - then obtain h' where h': "h' \ H & x \ h' = y" by blast + then obtain h' where h': "h' \ H \ x \ h' = y" by blast show "\h\H. x = y \ h" proof show "x = y \ inv h'" using h' x sb @@ -593,7 +593,7 @@ definition r_congruent :: "[('a,'b)monoid_scheme, 'a set] \ ('a*'a)set" ("rcong\ _") - where "rcong\<^bsub>G\<^esub> H = {(x,y). x \ carrier G & y \ carrier G & inv\<^bsub>G\<^esub> x \\<^bsub>G\<^esub> y \ H}" + where "rcong\<^bsub>G\<^esub> H = {(x,y). x \ carrier G \ y \ carrier G \ inv\<^bsub>G\<^esub> x \\<^bsub>G\<^esub> y \ H}" lemma (in subgroup) equiv_rcong: @@ -784,7 +784,7 @@ lemma (in group) inj_on_f: "\H \ carrier G; a \ carrier G\ \ inj_on (\y. y \ inv a) (H #> a)" apply (rule inj_onI) -apply (subgoal_tac "x \ carrier G & y \ carrier G") +apply (subgoal_tac "x \ carrier G \ y \ carrier G") prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD]) apply (simp add: subsetD) done @@ -898,7 +898,7 @@ definition kernel :: "('a, 'm) monoid_scheme \ ('b, 'n) monoid_scheme \ ('a \ 'b) \ 'a set" \\the kernel of a homomorphism\ - where "kernel G H h = {x. x \ carrier G & h x = \\<^bsub>H\<^esub>}" + where "kernel G H h = {x. x \ carrier G \ h x = \\<^bsub>H\<^esub>}" lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G" apply (rule subgroup.intro) diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Algebra/FiniteProduct.thy --- a/src/HOL/Algebra/FiniteProduct.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Algebra/FiniteProduct.thy Sun Nov 26 21:08:32 2017 +0100 @@ -48,7 +48,7 @@ lemma finite_imp_foldSetD: "[| finite A; e \ D; !!x y. [| x \ A; y \ D |] ==> f x y \ D |] ==> - EX x. (A, x) \ foldSetD D f e" + \x. (A, x) \ foldSetD D f e" proof (induct set: finite) case empty then show ?case by auto next @@ -89,7 +89,7 @@ by (induct set: foldSetD) auto lemma (in LCD) finite_imp_foldSetD: - "[| finite A; A \ B; e \ D |] ==> EX x. (A, x) \ foldSetD D f e" + "[| finite A; A \ B; e \ D |] ==> \x. (A, x) \ foldSetD D f e" proof (induct set: finite) case empty then show ?case by auto next @@ -102,8 +102,8 @@ qed lemma (in LCD) foldSetD_determ_aux: - "e \ D ==> \A x. A \ B & card A < n --> (A, x) \ foldSetD D f e --> - (\y. (A, y) \ foldSetD D f e --> y = x)" + "e \ D \ \A x. A \ B \ card A < n \ (A, x) \ foldSetD D f e \ + (\y. (A, y) \ foldSetD D f e \ y = x)" apply (induct n) apply (auto simp add: less_Suc_eq) (* slow *) apply (erule foldSetD.cases) @@ -120,7 +120,7 @@ prefer 2 apply (blast elim!: equalityE) apply blast txt \case @{prop "xa \ xb"}.\ - apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb \ Aa & xa \ Ab") + apply (subgoal_tac "Aa - {xb} = Ab - {xa} \ xb \ Aa \ xa \ Ab") prefer 2 apply (blast elim!: equalityE) apply clarify apply (subgoal_tac "Aa = insert xb Ab - {xa}") @@ -166,9 +166,9 @@ by (unfold foldD_def) blast lemma (in LCD) foldD_insert_aux: - "[| x ~: A; x \ B; e \ D; A \ B |] ==> + "[| x \ A; x \ B; e \ D; A \ B |] ==> ((insert x A, v) \ foldSetD D f e) = - (EX y. (A, y) \ foldSetD D f e & v = f x y)" + (\y. (A, y) \ foldSetD D f e \ v = f x y)" apply auto apply (rule_tac A1 = A in finite_imp_foldSetD [THEN exE]) apply (fastforce dest: foldSetD_imp_finite) @@ -291,7 +291,7 @@ finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b" where "finprod G f A = (if finite A - then foldD (carrier G) (mult G o f) \\<^bsub>G\<^esub> A + then foldD (carrier G) (mult G \ f) \\<^bsub>G\<^esub> A else \\<^bsub>G\<^esub>)" syntax @@ -360,7 +360,7 @@ by fast lemma funcset_Un_left [iff]: - "(f \ A Un B \ C) = (f \ A \ C & f \ B \ C)" + "(f \ A Un B \ C) = (f \ A \ C \ f \ B \ C)" by fast lemma finprod_Un_Int: diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Algebra/Group.thy --- a/src/HOL/Algebra/Group.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Algebra/Group.thy Sun Nov 26 21:08:32 2017 +0100 @@ -22,12 +22,12 @@ definition m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" ("inv\ _" [81] 80) - where "inv\<^bsub>G\<^esub> x = (THE y. y \ carrier G & x \\<^bsub>G\<^esub> y = \\<^bsub>G\<^esub> & y \\<^bsub>G\<^esub> x = \\<^bsub>G\<^esub>)" + where "inv\<^bsub>G\<^esub> x = (THE y. y \ carrier G \ x \\<^bsub>G\<^esub> y = \\<^bsub>G\<^esub> \ y \\<^bsub>G\<^esub> x = \\<^bsub>G\<^esub>)" definition Units :: "_ => 'a set" \\The set of invertible elements\ - where "Units G = {y. y \ carrier G & (\x \ carrier G. x \\<^bsub>G\<^esub> y = \\<^bsub>G\<^esub> & y \\<^bsub>G\<^esub> x = \\<^bsub>G\<^esub>)}" + where "Units G = {y. y \ carrier G \ (\x \ carrier G. x \\<^bsub>G\<^esub> y = \\<^bsub>G\<^esub> \ y \\<^bsub>G\<^esub> x = \\<^bsub>G\<^esub>)}" consts pow :: "[('a, 'm) monoid_scheme, 'a, 'b::semiring_1] => 'a" (infixr "'(^')\" 75) @@ -277,7 +277,7 @@ with x xG show "x \ \ = x" by simp qed have inv_ex: - "!!x. x \ carrier G ==> \y \ carrier G. y \ x = \ & x \ y = \" + "\x. x \ carrier G \ \y \ carrier G. y \ x = \ \ x \ y = \" proof - fix x assume x: "x \ carrier G" @@ -287,10 +287,10 @@ by (simp add: m_assoc [symmetric] l_inv r_one) with x y have r_inv: "x \ y = \" by simp - from x y show "\y \ carrier G. y \ x = \ & x \ y = \" + from x y show "\y \ carrier G. y \ x = \ \ x \ y = \" by (fast intro: l_inv r_inv) qed - then have carrier_subset_Units: "carrier G <= Units G" + then have carrier_subset_Units: "carrier G \ Units G" by (unfold Units_def) fast show ?thesis by standard (auto simp: r_one m_assoc carrier_subset_Units) @@ -305,9 +305,9 @@ lemma (in group) Units_eq [simp]: "Units G = carrier G" proof - show "Units G <= carrier G" by fast + show "Units G \ carrier G" by fast next - show "carrier G <= Units G" by (rule Units) + show "carrier G \ Units G" by (rule Units) qed lemma (in group) inv_closed [intro, simp]: @@ -510,13 +510,13 @@ monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp] lemma subgroup_nonempty: - "~ subgroup {} G" + "\ subgroup {} G" by (blast dest: subgroup.one_closed) lemma (in subgroup) finite_imp_card_positive: "finite (carrier G) ==> 0 < card H" proof (rule classical) - assume "finite (carrier G)" and a: "~ 0 < card H" + assume "finite (carrier G)" and a: "\ 0 < card H" then have "finite H" by (blast intro: finite_subset [OF subset]) with is_subgroup a have "subgroup {} G" by simp with subgroup_nonempty show ?thesis by contradiction @@ -591,7 +591,7 @@ definition hom :: "_ => _ => ('a => 'b) set" where "hom G H = - {h. h \ carrier G \ carrier H & + {h. h \ carrier G \ carrier H \ (\x \ carrier G. \y \ carrier G. h (x \\<^bsub>G\<^esub> y) = h x \\<^bsub>H\<^esub> h y)}" lemma (in group) hom_compose: @@ -600,9 +600,9 @@ definition iso :: "_ => _ => ('a => 'b) set" (infixr "\" 60) - where "G \ H = {h. h \ hom G H & bij_betw h (carrier G) (carrier H)}" + where "G \ H = {h. h \ hom G H \ bij_betw h (carrier G) (carrier H)}" -lemma iso_refl: "(%x. x) \ G \ G" +lemma iso_refl: "(\x. x) \ G \ G" by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) lemma (in group) iso_sym: @@ -798,15 +798,15 @@ done theorem (in group) subgroups_Inter: - assumes subgr: "(!!H. H \ A ==> subgroup H G)" - and not_empty: "A ~= {}" + assumes subgr: "(\H. H \ A \ subgroup H G)" + and not_empty: "A \ {}" shows "subgroup (\A) G" proof (rule subgroupI) from subgr [THEN subgroup.subset] and not_empty show "\A \ carrier G" by blast next from subgr [THEN subgroup.one_closed] - show "\A ~= {}" by blast + show "\A \ {}" by blast next fix x assume "x \ \A" with subgr [THEN subgroup.m_inv_closed] @@ -828,7 +828,7 @@ then show "\G. greatest ?L G (carrier ?L)" .. next fix A - assume L: "A \ carrier ?L" and non_empty: "A ~= {}" + assume L: "A \ carrier ?L" and non_empty: "A \ {}" then have Int_subgroup: "subgroup (\A) G" by (fastforce intro: subgroups_Inter) have "greatest ?L (\A) (Lower ?L A)" (is "greatest _ ?Int _") diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Algebra/IntRing.thy --- a/src/HOL/Algebra/IntRing.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Algebra/IntRing.thy Sun Nov 26 21:08:32 2017 +0100 @@ -166,7 +166,7 @@ "x \ UNIV \ True" "A \ UNIV \ True" "(\x \ UNIV. P x) \ (\x. P x)" - "(EX x : UNIV. P x) \ (EX x. P x)" + "(\x \ UNIV. P x) \ (\x. P x)" "(True \ Q) \ Q" "(True \ PROP R) \ PROP R" by simp_all @@ -247,7 +247,7 @@ then show "(\x. a = x * p) \ (\x. b = x * p)" by (metis dvd_def mult.commute) next - assume "UNIV = {uu. EX x. uu = x * p}" + assume "UNIV = {uu. \x. uu = x * p}" then obtain x where "1 = x * p" by best then have "\p * x\ = 1" by (simp add: mult.commute) then show False using prime diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Algebra/Lattice.thy --- a/src/HOL/Algebra/Lattice.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Algebra/Lattice.thy Sun Nov 26 21:08:32 2017 +0100 @@ -98,11 +98,11 @@ locale weak_upper_semilattice = weak_partial_order + assumes sup_of_two_exists: - "[| x \ carrier L; y \ carrier L |] ==> EX s. least L s (Upper L {x, y})" + "[| x \ carrier L; y \ carrier L |] ==> \s. least L s (Upper L {x, y})" locale weak_lower_semilattice = weak_partial_order + assumes inf_of_two_exists: - "[| x \ carrier L; y \ carrier L |] ==> EX s. greatest L s (Lower L {x, y})" + "[| x \ carrier L; y \ carrier L |] ==> \s. greatest L s (Lower L {x, y})" locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice @@ -250,7 +250,7 @@ qed lemma (in weak_upper_semilattice) finite_sup_least: - "[| finite A; A \ carrier L; A ~= {} |] ==> least L (\A) (Upper L A)" + "[| finite A; A \ carrier L; A \ {} |] ==> least L (\A) (Upper L A)" proof (induct set: finite) case empty then show ?case by simp @@ -284,7 +284,7 @@ qed lemma (in weak_upper_semilattice) finite_sup_closed [simp]: - "[| finite A; A \ carrier L; A ~= {} |] ==> \A \ carrier L" + "[| finite A; A \ carrier L; A \ {} |] ==> \A \ carrier L" proof (induct set: finite) case empty then show ?case by simp next @@ -495,7 +495,7 @@ qed lemma (in weak_lower_semilattice) finite_inf_greatest: - "[| finite A; A \ carrier L; A ~= {} |] ==> greatest L (\A) (Lower L A)" + "[| finite A; A \ carrier L; A \ {} |] ==> greatest L (\A) (Lower L A)" proof (induct set: finite) case empty then show ?case by simp next @@ -528,7 +528,7 @@ qed lemma (in weak_lower_semilattice) finite_inf_closed [simp]: - "[| finite A; A \ carrier L; A ~= {} |] ==> \A \ carrier L" + "[| finite A; A \ carrier L; A \ {} |] ==> \A \ carrier L" proof (induct set: finite) case empty then show ?case by simp next @@ -611,7 +611,7 @@ proof fix x y assume L: "x \ carrier L" "y \ carrier L" - show "EX s. least L s (Upper L {x, y})" + show "\s. least L s (Upper L {x, y})" proof - note total L moreover @@ -631,7 +631,7 @@ next fix x y assume L: "x \ carrier L" "y \ carrier L" - show "EX i. greatest L i (Lower L {x, y})" + show "\i. greatest L i (Lower L {x, y})" proof - note total L moreover @@ -687,14 +687,14 @@ locale upper_semilattice = partial_order + assumes sup_of_two_exists: - "[| x \ carrier L; y \ carrier L |] ==> EX s. least L s (Upper L {x, y})" + "[| x \ carrier L; y \ carrier L |] ==> \s. least L s (Upper L {x, y})" sublocale upper_semilattice \ weak?: weak_upper_semilattice by unfold_locales (rule sup_of_two_exists) locale lower_semilattice = partial_order + assumes inf_of_two_exists: - "[| x \ carrier L; y \ carrier L |] ==> EX s. greatest L s (Lower L {x, y})" + "[| x \ carrier L; y \ carrier L |] ==> \s. greatest L s (Lower L {x, y})" sublocale lower_semilattice \ weak?: weak_lower_semilattice by unfold_locales (rule inf_of_two_exists) diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Algebra/Order.thy --- a/src/HOL/Algebra/Order.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Algebra/Order.thy Sun Nov 26 21:08:32 2017 +0100 @@ -42,7 +42,7 @@ definition lless :: "[_, 'a, 'a] => bool" (infixl "\\" 50) - where "x \\<^bsub>L\<^esub> y \ x \\<^bsub>L\<^esub> y & x .\\<^bsub>L\<^esub> y" + where "x \\<^bsub>L\<^esub> y \ x \\<^bsub>L\<^esub> y \ x .\\<^bsub>L\<^esub> y" subsubsection \The order relation\ @@ -65,7 +65,7 @@ lemma weak_llessI: fixes R (structure) - assumes "x \ y" and "~(x .= y)" + assumes "x \ y" and "\(x .= y)" shows "x \ y" using assms unfolding lless_def by simp @@ -137,11 +137,11 @@ definition Upper :: "[_, 'a set] => 'a set" - where "Upper L A = {u. (ALL x. x \ A \ carrier L --> x \\<^bsub>L\<^esub> u)} \ carrier L" + where "Upper L A = {u. (\x. x \ A \ carrier L \ x \\<^bsub>L\<^esub> u)} \ carrier L" definition Lower :: "[_, 'a set] => 'a set" - where "Lower L A = {l. (ALL x. x \ A \ carrier L --> l \\<^bsub>L\<^esub> x)} \ carrier L" + where "Lower L A = {l. (\x. x \ A \ carrier L \ l \\<^bsub>L\<^esub> x)} \ carrier L" lemma Upper_closed [intro!, simp]: "Upper L A \ carrier L" @@ -320,11 +320,11 @@ definition least :: "[_, 'a, 'a set] => bool" - where "least L l A \ A \ carrier L & l \ A & (ALL x : A. l \\<^bsub>L\<^esub> x)" + where "least L l A \ A \ carrier L \ l \ A \ (\x\A. l \\<^bsub>L\<^esub> x)" definition greatest :: "[_, 'a, 'a set] => bool" - where "greatest L g A \ A \ carrier L & g \ A & (ALL x : A. x \\<^bsub>L\<^esub> g)" + where "greatest L g A \ A \ carrier L \ g \ A \ (\x\A. x \\<^bsub>L\<^esub> g)" text (in weak_partial_order) \Could weaken these to @{term "l \ carrier L \ l .\ A"} and @{term "g \ carrier L \ g .\ A"}.\ @@ -601,7 +601,7 @@ using weak_le_antisym unfolding eq_is_equal . lemma lless_eq: - "x \ y \ x \ y & x \ y" + "x \ y \ x \ y \ x \ y" unfolding lless_def by (simp add: eq_is_equal) lemma set_eq_is_eq: "A {.=} B \ A = B" diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Algebra/Ring.thy --- a/src/HOL/Algebra/Ring.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Algebra/Ring.thy Sun Nov 26 21:08:32 2017 +0100 @@ -238,9 +238,9 @@ locale cring = ring + comm_monoid R locale "domain" = cring + - assumes one_not_zero [simp]: "\ ~= \" + assumes one_not_zero [simp]: "\ \ \" and integral: "[| a \ b = \; a \ carrier R; b \ carrier R |] ==> - a = \ | b = \" + a = \ \ b = \" locale field = "domain" + assumes field_Units: "Units R = carrier R - {\}" @@ -427,7 +427,7 @@ a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus lemma (in semiring) nat_pow_zero: - "(n::nat) ~= 0 ==> \ (^) n = \" + "(n::nat) \ 0 \ \ (^) n = \" by (induct n) simp_all context semiring begin @@ -469,7 +469,7 @@ fixes R (structure) and S (structure) assumes "ring R" "cring S" assumes RS: "a \ carrier R" "b \ carrier R" "c \ carrier S" "d \ carrier S" - shows "a \ \ (a \ \ b) = b & c \\<^bsub>S\<^esub> d = d \\<^bsub>S\<^esub> c" + shows "a \ \ (a \ \ b) = b \ c \\<^bsub>S\<^esub> d = d \\<^bsub>S\<^esub> c" proof - interpret ring R by fact interpret cring S by fact @@ -513,27 +513,27 @@ context "domain" begin lemma zero_not_one [simp]: - "\ ~= \" + "\ \ \" by (rule not_sym) simp lemma integral_iff: (* not by default a simp rule! *) - "[| a \ carrier R; b \ carrier R |] ==> (a \ b = \) = (a = \ | b = \)" + "[| a \ carrier R; b \ carrier R |] ==> (a \ b = \) = (a = \ \ b = \)" proof assume "a \ carrier R" "b \ carrier R" "a \ b = \" - then show "a = \ | b = \" by (simp add: integral) + then show "a = \ \ b = \" by (simp add: integral) next - assume "a \ carrier R" "b \ carrier R" "a = \ | b = \" + assume "a \ carrier R" "b \ carrier R" "a = \ \ b = \" then show "a \ b = \" by auto qed lemma m_lcancel: - assumes prem: "a ~= \" + assumes prem: "a \ \" and R: "a \ carrier R" "b \ carrier R" "c \ carrier R" shows "(a \ b = a \ c) = (b = c)" proof assume eq: "a \ b = a \ c" with R have "a \ (b \ c) = \" by algebra - with R have "a = \ | (b \ c) = \" by (simp add: integral_iff) + with R have "a = \ \ (b \ c) = \" by (simp add: integral_iff) with prem and R have "b \ c = \" by auto with R have "b = b \ (b \ c)" by algebra also from R have "b \ (b \ c) = c" by algebra @@ -543,7 +543,7 @@ qed lemma m_rcancel: - assumes prem: "a ~= \" + assumes prem: "a \ \" and R: "a \ carrier R" "b \ carrier R" "c \ carrier R" shows conc: "(b \ a = c \ a) = (b = c)" proof - @@ -609,9 +609,9 @@ definition ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set" where "ring_hom R S = - {h. h \ carrier R \ carrier S & - (ALL x y. x \ carrier R & y \ carrier R --> - h (x \\<^bsub>R\<^esub> y) = h x \\<^bsub>S\<^esub> h y & h (x \\<^bsub>R\<^esub> y) = h x \\<^bsub>S\<^esub> h y) & + {h. h \ carrier R \ carrier S \ + (\x y. x \ carrier R \ y \ carrier R \ + h (x \\<^bsub>R\<^esub> y) = h x \\<^bsub>S\<^esub> h y \ h (x \\<^bsub>R\<^esub> y) = h x \\<^bsub>S\<^esub> h y) \ h \\<^bsub>R\<^esub> = \\<^bsub>S\<^esub>}" lemma ring_hom_memI: @@ -675,13 +675,13 @@ qed lemma (in ring_hom_cring) hom_finsum [simp]: - "f \ A \ carrier R ==> - h (finsum R f A) = finsum S (h o f) A" + "f \ A \ carrier R \ + h (finsum R f A) = finsum S (h \ f) A" by (induct A rule: infinite_finite_induct, auto simp: Pi_def) lemma (in ring_hom_cring) hom_finprod: - "f \ A \ carrier R ==> - h (finprod R f A) = finprod S (h o f) A" + "f \ A \ carrier R \ + h (finprod R f A) = finprod S (h \ f) A" by (induct A rule: infinite_finite_induct, auto simp: Pi_def) declare ring_hom_cring.hom_finprod [simp] diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Algebra/UnivPoly.thy --- a/src/HOL/Algebra/UnivPoly.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Algebra/UnivPoly.thy Sun Nov 26 21:08:32 2017 +0100 @@ -42,7 +42,7 @@ lemma bound_below: assumes bound: "bound z m f" and nonzero: "f n \ z" shows "n \ m" proof (rule classical) - assume "~ ?thesis" + assume "\ ?thesis" then have "m < n" by arith with bound have "f n = z" .. with nonzero show ?thesis by contradiction @@ -54,7 +54,7 @@ definition up :: "('a, 'm) ring_scheme => (nat => 'a) set" - where "up R = {f. f \ UNIV \ carrier R & (EX n. bound \\<^bsub>R\<^esub> n f)}" + where "up R = {f. f \ UNIV \ carrier R \ (\n. bound \\<^bsub>R\<^esub> n f)}" definition UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring" where "UP R = \ @@ -72,7 +72,7 @@ \ lemma mem_upI [intro]: - "[| !!n. f n \ carrier R; EX n. bound (zero R) n f |] ==> f \ up R" + "[| \n. f n \ carrier R; \n. bound (zero R) n f |] ==> f \ up R" by (simp add: up_def Pi_def) lemma mem_upD [dest]: @@ -82,7 +82,7 @@ context ring begin -lemma bound_upD [dest]: "f \ up R ==> EX n. bound \ n f" by (simp add: up_def) +lemma bound_upD [dest]: "f \ up R \ \n. bound \ n f" by (simp add: up_def) lemma up_one_closed: "(\n. if n = 0 then \ else \) \ up R" using up_def by force @@ -97,7 +97,7 @@ by auto next assume UP: "p \ up R" "q \ up R" - show "EX n. bound \ n (\i. p i \ q i)" + show "\n. bound \ n (\i. p i \ q i)" proof - from UP obtain n where boundn: "bound \ n p" by fast from UP obtain m where boundm: "bound \ m q" by fast @@ -117,7 +117,7 @@ assume R: "p \ up R" then obtain n where "bound \ n p" by auto then have "bound \ n (\i. \ p i)" by auto - then show "EX n. bound \ n (\i. \ p i)" by auto + then show "\n. bound \ n (\i. \ p i)" by auto qed auto lemma up_minus_closed: @@ -135,7 +135,7 @@ by (simp add: mem_upD funcsetI) next assume UP: "p \ up R" "q \ up R" - show "EX n. bound \ n (\n. \i \ {..n}. p i \ q (n-i))" + show "\n. bound \ n (\n. \i \ {..n}. p i \ q (n-i))" proof - from UP obtain n where boundn: "bound \ n p" by fast from UP obtain m where boundm: "bound \ m q" by fast @@ -751,33 +751,33 @@ qed lemma deg_belowI: - assumes non_zero: "n ~= 0 ==> coeff P p n ~= \" + assumes non_zero: "n \ 0 \ coeff P p n \ \" and R: "p \ carrier P" - shows "n <= deg R p" + shows "n \ deg R p" \ \Logically, this is a slightly stronger version of @{thm [source] deg_aboveD}\ proof (cases "n=0") case True then show ?thesis by simp next - case False then have "coeff P p n ~= \" by (rule non_zero) - then have "~ deg R p < n" by (fast dest: deg_aboveD intro: R) + case False then have "coeff P p n \ \" by (rule non_zero) + then have "\ deg R p < n" by (fast dest: deg_aboveD intro: R) then show ?thesis by arith qed lemma lcoeff_nonzero_deg: - assumes deg: "deg R p ~= 0" and R: "p \ carrier P" - shows "coeff P p (deg R p) ~= \" + assumes deg: "deg R p \ 0" and R: "p \ carrier P" + shows "coeff P p (deg R p) \ \" proof - - from R obtain m where "deg R p <= m" and m_coeff: "coeff P p m ~= \" + from R obtain m where "deg R p \ m" and m_coeff: "coeff P p m \ \" proof - - have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)" + have minus: "\(n::nat) m. n \ 0 \ (n - Suc 0 < m) = (n \ m)" by arith from deg have "deg R p - 1 < (LEAST n. bound \ n (coeff P p))" by (unfold deg_def P_def) simp - then have "~ bound \ (deg R p - 1) (coeff P p)" by (rule not_less_Least) - then have "EX m. deg R p - 1 < m & coeff P p m ~= \" + then have "\ bound \ (deg R p - 1) (coeff P p)" by (rule not_less_Least) + then have "\m. deg R p - 1 < m \ coeff P p m \ \" by (unfold bound_def) fast - then have "EX m. deg R p <= m & coeff P p m ~= \" by (simp add: deg minus) + then have "\m. deg R p \ m \ coeff P p m \ \" by (simp add: deg minus) then show ?thesis by (auto intro: that) qed with deg_belowI R have "deg R p = m" by fastforce @@ -785,24 +785,24 @@ qed lemma lcoeff_nonzero_nonzero: - assumes deg: "deg R p = 0" and nonzero: "p ~= \\<^bsub>P\<^esub>" and R: "p \ carrier P" - shows "coeff P p 0 ~= \" + assumes deg: "deg R p = 0" and nonzero: "p \ \\<^bsub>P\<^esub>" and R: "p \ carrier P" + shows "coeff P p 0 \ \" proof - - have "EX m. coeff P p m ~= \" + have "\m. coeff P p m \ \" proof (rule classical) - assume "~ ?thesis" + assume "\ ?thesis" with R have "p = \\<^bsub>P\<^esub>" by (auto intro: up_eqI) with nonzero show ?thesis by contradiction qed - then obtain m where coeff: "coeff P p m ~= \" .. - from this and R have "m <= deg R p" by (rule deg_belowI) + then obtain m where coeff: "coeff P p m \ \" .. + from this and R have "m \ deg R p" by (rule deg_belowI) then have "m = 0" by (simp add: deg) with coeff show ?thesis by simp qed lemma lcoeff_nonzero: - assumes neq: "p ~= \\<^bsub>P\<^esub>" and R: "p \ carrier P" - shows "coeff P p (deg R p) ~= \" + assumes neq: "p \ \\<^bsub>P\<^esub>" and R: "p \ carrier P" + shows "coeff P p (deg R p) \ \" proof (cases "deg R p = 0") case True with neq R show ?thesis by (simp add: lcoeff_nonzero_nonzero) next @@ -810,55 +810,55 @@ qed lemma deg_eqI: - "[| !!m. n < m ==> coeff P p m = \; - !!n. n ~= 0 ==> coeff P p n ~= \; p \ carrier P |] ==> deg R p = n" + "[| \m. n < m \ coeff P p m = \; + \n. n \ 0 \ coeff P p n \ \; p \ carrier P |] ==> deg R p = n" by (fast intro: le_antisym deg_aboveI deg_belowI) text \Degree and polynomial operations\ lemma deg_add [simp]: "p \ carrier P \ q \ carrier P \ - deg R (p \\<^bsub>P\<^esub> q) <= max (deg R p) (deg R q)" + deg R (p \\<^bsub>P\<^esub> q) \ max (deg R p) (deg R q)" by(rule deg_aboveI)(simp_all add: deg_aboveD) lemma deg_monom_le: - "a \ carrier R ==> deg R (monom P a n) <= n" + "a \ carrier R \ deg R (monom P a n) \ n" by (intro deg_aboveI) simp_all lemma deg_monom [simp]: - "[| a ~= \; a \ carrier R |] ==> deg R (monom P a n) = n" + "[| a \ \; a \ carrier R |] ==> deg R (monom P a n) = n" by (fastforce intro: le_antisym deg_aboveI deg_belowI) lemma deg_const [simp]: assumes R: "a \ carrier R" shows "deg R (monom P a 0) = 0" proof (rule le_antisym) - show "deg R (monom P a 0) <= 0" by (rule deg_aboveI) (simp_all add: R) + show "deg R (monom P a 0) \ 0" by (rule deg_aboveI) (simp_all add: R) next - show "0 <= deg R (monom P a 0)" by (rule deg_belowI) (simp_all add: R) + show "0 \ deg R (monom P a 0)" by (rule deg_belowI) (simp_all add: R) qed lemma deg_zero [simp]: "deg R \\<^bsub>P\<^esub> = 0" proof (rule le_antisym) - show "deg R \\<^bsub>P\<^esub> <= 0" by (rule deg_aboveI) simp_all + show "deg R \\<^bsub>P\<^esub> \ 0" by (rule deg_aboveI) simp_all next - show "0 <= deg R \\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all + show "0 \ deg R \\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all qed lemma deg_one [simp]: "deg R \\<^bsub>P\<^esub> = 0" proof (rule le_antisym) - show "deg R \\<^bsub>P\<^esub> <= 0" by (rule deg_aboveI) simp_all + show "deg R \\<^bsub>P\<^esub> \ 0" by (rule deg_aboveI) simp_all next - show "0 <= deg R \\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all + show "0 \ deg R \\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all qed lemma deg_uminus [simp]: assumes R: "p \ carrier P" shows "deg R (\\<^bsub>P\<^esub> p) = deg R p" proof (rule le_antisym) - show "deg R (\\<^bsub>P\<^esub> p) <= deg R p" by (simp add: deg_aboveI deg_aboveD R) + show "deg R (\\<^bsub>P\<^esub> p) \ deg R p" by (simp add: deg_aboveI deg_aboveD R) next - show "deg R p <= deg R (\\<^bsub>P\<^esub> p)" + show "deg R p \ deg R (\\<^bsub>P\<^esub> p)" by (simp add: deg_belowI lcoeff_nonzero_deg inj_on_eq_iff [OF R.a_inv_inj, of _ "\", simplified] R) qed @@ -868,7 +868,7 @@ lemma deg_smult_ring [simp]: "[| a \ carrier R; p \ carrier P |] ==> - deg R (a \\<^bsub>P\<^esub> p) <= (if a = \ then 0 else deg R p)" + deg R (a \\<^bsub>P\<^esub> p) \ (if a = \ then 0 else deg R p)" by (cases "a = \") (simp add: deg_aboveI deg_aboveD)+ end @@ -880,10 +880,10 @@ assumes R: "a \ carrier R" "p \ carrier P" shows "deg R (a \\<^bsub>P\<^esub> p) = (if a = \ then 0 else deg R p)" proof (rule le_antisym) - show "deg R (a \\<^bsub>P\<^esub> p) <= (if a = \ then 0 else deg R p)" + show "deg R (a \\<^bsub>P\<^esub> p) \ (if a = \ then 0 else deg R p)" using R by (rule deg_smult_ring) next - show "(if a = \ then 0 else deg R p) <= deg R (a \\<^bsub>P\<^esub> p)" + show "(if a = \ then 0 else deg R p) \ deg R (a \\<^bsub>P\<^esub> p)" proof (cases "a = \") qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff R) qed @@ -895,7 +895,7 @@ lemma deg_mult_ring: assumes R: "p \ carrier P" "q \ carrier P" - shows "deg R (p \\<^bsub>P\<^esub> q) <= deg R p + deg R q" + shows "deg R (p \\<^bsub>P\<^esub> q) \ deg R p + deg R q" proof (rule deg_aboveI) fix m assume boundm: "deg R p + deg R q < m" @@ -919,16 +919,16 @@ begin lemma deg_mult [simp]: - "[| p ~= \\<^bsub>P\<^esub>; q ~= \\<^bsub>P\<^esub>; p \ carrier P; q \ carrier P |] ==> + "[| p \ \\<^bsub>P\<^esub>; q \ \\<^bsub>P\<^esub>; p \ carrier P; q \ carrier P |] ==> deg R (p \\<^bsub>P\<^esub> q) = deg R p + deg R q" proof (rule le_antisym) assume "p \ carrier P" " q \ carrier P" - then show "deg R (p \\<^bsub>P\<^esub> q) <= deg R p + deg R q" by (rule deg_mult_ring) + then show "deg R (p \\<^bsub>P\<^esub> q) \ deg R p + deg R q" by (rule deg_mult_ring) next let ?s = "(\i. coeff P p i \ coeff P q (deg R p + deg R q - i))" - assume R: "p \ carrier P" "q \ carrier P" and nz: "p ~= \\<^bsub>P\<^esub>" "q ~= \\<^bsub>P\<^esub>" + assume R: "p \ carrier P" "q \ carrier P" and nz: "p \ \\<^bsub>P\<^esub>" "q \ \\<^bsub>P\<^esub>" have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith - show "deg R p + deg R q <= deg R (p \\<^bsub>P\<^esub> q)" + show "deg R p + deg R q \ deg R (p \\<^bsub>P\<^esub> q)" proof (rule deg_belowI, simp add: R) have "(\i \ {.. deg R p + deg R q}. ?s i) = (\i \ {..< deg R p} \ {deg R p .. deg R p + deg R q}. ?s i)" @@ -942,7 +942,7 @@ by (simp cong: R.finsum_cong add: deg_aboveD R Pi_def) finally have "(\i \ {.. deg R p + deg R q}. ?s i) = coeff P p (deg R p) \ coeff P q (deg R q)" . - with nz show "(\i \ {.. deg R p + deg R q}. ?s i) ~= \" + with nz show "(\i \ {.. deg R p + deg R q}. ?s i) \ \" by (simp add: integral_iff lcoeff_nonzero R) qed (simp add: R) qed @@ -969,7 +969,7 @@ from R have RR: "!!i. (if i = k then coeff P p i else \) \ carrier R" by simp show "coeff P (\\<^bsub>P\<^esub> i \ {..deg R p}. ?s i) k = coeff P p k" - proof (cases "k <= deg R p") + proof (cases "k \ deg R p") case True hence "coeff P (\\<^bsub>P\<^esub> i \ {..deg R p}. ?s i) k = coeff P (\\<^bsub>P\<^esub> i \ {..k} \ {k<..deg R p}. ?s i) k" @@ -1017,9 +1017,9 @@ lemma domainI: assumes cring: "cring R" - and one_not_zero: "one R ~= zero R" - and integral: "!!a b. [| mult R a b = zero R; a \ carrier R; - b \ carrier R |] ==> a = zero R | b = zero R" + and one_not_zero: "one R \ zero R" + and integral: "\a b. [| mult R a b = zero R; a \ carrier R; + b \ carrier R |] ==> a = zero R \ b = zero R" shows "domain R" by (auto intro!: domain.intro domain_axioms.intro cring.axioms assms del: disjCI) @@ -1028,7 +1028,7 @@ begin lemma UP_one_not_zero: - "\\<^bsub>P\<^esub> ~= \\<^bsub>P\<^esub>" + "\\<^bsub>P\<^esub> \ \\<^bsub>P\<^esub>" proof assume "\\<^bsub>P\<^esub> = \\<^bsub>P\<^esub>" hence "coeff P \\<^bsub>P\<^esub> 0 = (coeff P \\<^bsub>P\<^esub> 0)" by simp @@ -1037,17 +1037,17 @@ qed lemma UP_integral: - "[| p \\<^bsub>P\<^esub> q = \\<^bsub>P\<^esub>; p \ carrier P; q \ carrier P |] ==> p = \\<^bsub>P\<^esub> | q = \\<^bsub>P\<^esub>" + "[| p \\<^bsub>P\<^esub> q = \\<^bsub>P\<^esub>; p \ carrier P; q \ carrier P |] ==> p = \\<^bsub>P\<^esub> \ q = \\<^bsub>P\<^esub>" proof - fix p q assume pq: "p \\<^bsub>P\<^esub> q = \\<^bsub>P\<^esub>" and R: "p \ carrier P" "q \ carrier P" - show "p = \\<^bsub>P\<^esub> | q = \\<^bsub>P\<^esub>" + show "p = \\<^bsub>P\<^esub> \ q = \\<^bsub>P\<^esub>" proof (rule classical) - assume c: "~ (p = \\<^bsub>P\<^esub> | q = \\<^bsub>P\<^esub>)" + assume c: "\ (p = \\<^bsub>P\<^esub> \ q = \\<^bsub>P\<^esub>)" with R have "deg R p + deg R q = deg R (p \\<^bsub>P\<^esub> q)" by simp also from pq have "... = 0" by simp finally have "deg R p + deg R q = 0" . - then have f1: "deg R p = 0 & deg R q = 0" by simp + then have f1: "deg R p = 0 \ deg R q = 0" by simp from f1 R have "p = (\\<^bsub>P\<^esub> i \ {..0}. monom P (coeff P p i) i)" by (simp only: up_repr_le) also from R have "... = monom P (coeff P p 0) 0" by simp @@ -1059,9 +1059,9 @@ from R have "coeff P p 0 \ coeff P q 0 = coeff P (p \\<^bsub>P\<^esub> q) 0" by simp also from pq have "... = \" by simp finally have "coeff P p 0 \ coeff P q 0 = \" . - with R have "coeff P p 0 = \ | coeff P q 0 = \" + with R have "coeff P p 0 = \ \ coeff P q 0 = \" by (simp add: R.integral_iff) - with p q show "p = \\<^bsub>P\<^esub> | q = \\<^bsub>P\<^esub>" by fastforce + with p q show "p = \\<^bsub>P\<^esub> \ q = \\<^bsub>P\<^esub>" by fastforce qed qed @@ -1206,8 +1206,8 @@ maybe it is not that necessary.\ lemma (in ring_hom_ring) hom_finsum [simp]: - "f \ A \ carrier R ==> - h (finsum R f A) = finsum S (h o f) A" + "f \ A \ carrier R \ + h (finsum R f A) = finsum S (h \ f) A" by (induct A rule: infinite_finite_induct, auto simp: Pi_def) context UP_pre_univ_prop @@ -1429,9 +1429,9 @@ theorem UP_universal_property: assumes S: "s \ carrier S" - shows "\!Phi. Phi \ ring_hom P S \ extensional (carrier P) & - Phi (monom P \ 1) = s & - (ALL r : carrier R. Phi (monom P r 0) = h r)" + shows "\!Phi. Phi \ ring_hom P S \ extensional (carrier P) \ + Phi (monom P \ 1) = s \ + (\r \ carrier R. Phi (monom P r 0) = h r)" using S eval_monom1 apply (auto intro: eval_ring_hom eval_const eval_extensional) apply (rule extensionalityI) @@ -1550,14 +1550,14 @@ lemma long_div_theorem: assumes g_in_P [simp]: "g \ carrier P" and f_in_P [simp]: "f \ carrier P" and g_not_zero: "g \ \\<^bsub>P\<^esub>" - shows "\ q r (k::nat). (q \ carrier P) \ (r \ carrier P) \ (lcoeff g)(^)\<^bsub>R\<^esub>k \\<^bsub>P\<^esub> f = g \\<^bsub>P\<^esub> q \\<^bsub>P\<^esub> r \ (r = \\<^bsub>P\<^esub> | deg R r < deg R g)" + shows "\q r (k::nat). (q \ carrier P) \ (r \ carrier P) \ (lcoeff g)(^)\<^bsub>R\<^esub>k \\<^bsub>P\<^esub> f = g \\<^bsub>P\<^esub> q \\<^bsub>P\<^esub> r \ (r = \\<^bsub>P\<^esub> \ deg R r < deg R g)" using f_in_P proof (induct "deg R f" arbitrary: "f" rule: nat_less_induct) case (1 f) note f_in_P [simp] = "1.prems" let ?pred = "(\ q r (k::nat). (q \ carrier P) \ (r \ carrier P) - \ (lcoeff g)(^)\<^bsub>R\<^esub>k \\<^bsub>P\<^esub> f = g \\<^bsub>P\<^esub> q \\<^bsub>P\<^esub> r \ (r = \\<^bsub>P\<^esub> | deg R r < deg R g))" + \ (lcoeff g)(^)\<^bsub>R\<^esub>k \\<^bsub>P\<^esub> f = g \\<^bsub>P\<^esub> q \\<^bsub>P\<^esub> r \ (r = \\<^bsub>P\<^esub> \ deg R r < deg R g))" let ?lg = "lcoeff g" and ?lf = "lcoeff f" show ?case proof (cases "deg R f < deg R g") diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/BNF_Cardinal_Order_Relation.thy --- a/src/HOL/BNF_Cardinal_Order_Relation.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Sun Nov 26 21:08:32 2017 +0100 @@ -387,8 +387,8 @@ lemma card_of_image: "|f ` A| <=o |A|" proof(cases "A = {}", simp add: card_of_empty) - assume "A ~= {}" - hence "f ` A ~= {}" by auto + assume "A \ {}" + hence "f ` A \ {}" by auto thus "|f ` A| \o |A|" using card_of_ordLeq2[of "f ` A" A] by auto qed @@ -886,7 +886,7 @@ moreover have "under r a \ Field r" using under_Field . ultimately have "under r a < Field r" by blast - then obtain b where 1: "b : Field r \ ~ (b,a) : r" + then obtain b where 1: "b \ Field r \ \ (b,a) \ r" unfolding under_def by blast moreover have ba: "b \ a" using 1 r unfolding card_order_on_def well_order_on_def @@ -1100,7 +1100,7 @@ using 3 infinite_imp_bij_betw2[of "?Inl ` A"] by auto moreover have "?A' = A <+> B" using Case1 by blast ultimately have "bij_betw g (?Inl ` A) (A <+> B)" by simp - hence "bij_betw (g o ?Inl) A (A <+> B)" + hence "bij_betw (g \ ?Inl) A (A <+> B)" using 2 by (auto simp add: bij_betw_trans) thus ?thesis using card_of_ordIso ordIso_symmetric by blast next @@ -1510,11 +1510,11 @@ definition regularCard where "regularCard r \ - ALL K. K \ Field r \ cofinal K r \ |K| =o r" + \K. K \ Field r \ cofinal K r \ |K| =o r" definition relChain where "relChain r As \ - ALL i j. (i,j) \ r \ As i \ As j" + \i j. (i,j) \ r \ As i \ As j" lemma regularCard_UNION: assumes r: "Card_order r" "regularCard r" @@ -1523,17 +1523,17 @@ and cardB: "|B| As i" proof- - let ?phi = "%b j. j : Field r \ b : As j" - have "ALL b : B. EX j. ?phi b j" using Bsub by blast + let ?phi = "\b j. j \ Field r \ b \ As j" + have "\b\B. \j. ?phi b j" using Bsub by blast then obtain f where f: "!! b. b : B \ ?phi b (f b)" using bchoice[of B ?phi] by blast let ?K = "f ` B" - {assume 1: "!! i. i : Field r \ ~ B \ As i" + {assume 1: "\i. i \ Field r \ \ B \ As i" have 2: "cofinal ?K r" unfolding cofinal_def proof auto fix i assume i: "i : Field r" with 1 obtain b where b: "b : B \ b \ As i" by blast - hence "i \ f b \ ~ (f b,i) : r" + hence "i \ f b \ \ (f b,i) \ r" using As f unfolding relChain_def by auto hence "i \ f b \ (i, f b) : r" using r unfolding card_order_on_def well_order_on_def linear_order_on_def diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/BNF_Composition.thy --- a/src/HOL/BNF_Composition.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/BNF_Composition.thy Sun Nov 26 21:08:32 2017 +0100 @@ -18,13 +18,13 @@ lemma ssubst_mem: "\t = s; s \ X\ \ t \ X" by simp -lemma empty_natural: "(\_. {}) o f = image g o (\_. {})" +lemma empty_natural: "(\_. {}) \ f = image g \ (\_. {})" by (rule ext) simp -lemma Union_natural: "Union o image (image f) = image f o Union" +lemma Union_natural: "Union \ image (image f) = image f \ Union" by (rule ext) (auto simp only: comp_apply) -lemma in_Union_o_assoc: "x \ (Union o gset o gmap) A \ x \ (Union o (gset o gmap)) A" +lemma in_Union_o_assoc: "x \ (Union \ gset \ gmap) A \ x \ (Union \ (gset \ gmap)) A" by (unfold comp_assoc) lemma comp_single_set_bd: @@ -66,7 +66,7 @@ lemma Union_image_empty: "A \ \(f ` {}) = A" by simp -lemma image_o_collect: "collect ((\f. image g o f) ` F) = image g o collect F" +lemma image_o_collect: "collect ((\f. image g \ f) ` F) = image g \ collect F" by (rule ext) (auto simp add: collect_def) lemma conj_subset_def: "A \ {x. P x \ Q x} = (A \ {x. P x} \ A \ {x. Q x})" @@ -91,19 +91,19 @@ vimage2p f g R OO vimage2p g h S \ vimage2p f h T" unfolding vimage2p_def by auto -lemma type_copy_map_cong0: "M (g x) = N (h x) \ (f o M o g) x = (f o N o h) x" +lemma type_copy_map_cong0: "M (g x) = N (h x) \ (f \ M \ g) x = (f \ N \ h) x" by auto -lemma type_copy_set_bd: "(\y. |S y| \o bd) \ |(S o Rep) x| \o bd" +lemma type_copy_set_bd: "(\y. |S y| \o bd) \ |(S \ Rep) x| \o bd" by auto lemma vimage2p_cong: "R = S \ vimage2p f g R = vimage2p f g S" by simp -lemma Ball_comp_iff: "(\x. Ball (A x) f) o g = (\x. Ball ((A o g) x) f)" +lemma Ball_comp_iff: "(\x. Ball (A x) f) \ g = (\x. Ball ((A \ g) x) f)" unfolding o_def by auto -lemma conj_comp_iff: "(\x. P x \ Q x) o g = (\x. (P o g) x \ (Q o g) x)" +lemma conj_comp_iff: "(\x. P x \ Q x) \ g = (\x. (P \ g) x \ (Q \ g) x)" unfolding o_def by auto context @@ -111,26 +111,26 @@ assumes type_copy: "type_definition Rep Abs UNIV" begin -lemma type_copy_map_id0: "M = id \ Abs o M o Rep = id" +lemma type_copy_map_id0: "M = id \ Abs \ M \ Rep = id" using type_definition.Rep_inverse[OF type_copy] by auto -lemma type_copy_map_comp0: "M = M1 o M2 \ f o M o g = (f o M1 o Rep) o (Abs o M2 o g)" +lemma type_copy_map_comp0: "M = M1 \ M2 \ f \ M \ g = (f \ M1 \ Rep) \ (Abs \ M2 \ g)" using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto -lemma type_copy_set_map0: "S o M = image f o S' \ (S o Rep) o (Abs o M o g) = image f o (S' o g)" +lemma type_copy_set_map0: "S \ M = image f \ S' \ (S \ Rep) \ (Abs \ M \ g) = image f \ (S' \ g)" using type_definition.Abs_inverse[OF type_copy UNIV_I] by (auto simp: o_def fun_eq_iff) -lemma type_copy_wit: "x \ (S o Rep) (Abs y) \ x \ S y" +lemma type_copy_wit: "x \ (S \ Rep) (Abs y) \ x \ S y" using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto lemma type_copy_vimage2p_Grp_Rep: "vimage2p f Rep (Grp (Collect P) h) = - Grp (Collect (\x. P (f x))) (Abs o h o f)" + Grp (Collect (\x. P (f x))) (Abs \ h \ f)" unfolding vimage2p_def Grp_def fun_eq_iff by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I] type_definition.Rep_inverse[OF type_copy] dest: sym) lemma type_copy_vimage2p_Grp_Abs: - "\h. vimage2p g Abs (Grp (Collect P) h) = Grp (Collect (\x. P (g x))) (Rep o h o g)" + "\h. vimage2p g Abs (Grp (Collect P) h) = Grp (Collect (\x. P (g x))) (Rep \ h \ g)" unfolding vimage2p_def Grp_def fun_eq_iff by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I] type_definition.Rep_inverse[OF type_copy] dest: sym) diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/BNF_Def.thy --- a/src/HOL/BNF_Def.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/BNF_Def.thy Sun Nov 26 21:08:32 2017 +0100 @@ -180,7 +180,7 @@ lemma case_sum_o_inj: "case_sum f g \ Inl = f" "case_sum f g \ Inr = g" by auto -lemma map_sum_o_inj: "map_sum f g o Inl = Inl o f" "map_sum f g o Inr = Inr o g" +lemma map_sum_o_inj: "map_sum f g \ Inl = Inl \ f" "map_sum f g \ Inr = Inr \ g" by auto lemma card_order_csum_cone_cexp_def: @@ -262,11 +262,11 @@ lemma eq_onp_True: "eq_onp (\_. True) = (op =)" unfolding eq_onp_def by simp -lemma Ball_image_comp: "Ball (f ` A) g = Ball A (g o f)" +lemma Ball_image_comp: "Ball (f ` A) g = Ball A (g \ f)" by auto lemma rel_fun_Collect_case_prodD: - "rel_fun A B f g \ X \ Collect (case_prod A) \ x \ X \ B ((f o fst) x) ((g o snd) x)" + "rel_fun A B f g \ X \ Collect (case_prod A) \ x \ X \ B ((f \ fst) x) ((g \ snd) x)" unfolding rel_fun_def by auto lemma eq_onp_mono_iff: "eq_onp P \ eq_onp Q \ P \ Q" diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/BNF_Fixpoint_Base.thy --- a/src/HOL/BNF_Fixpoint_Base.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/BNF_Fixpoint_Base.thy Sun Nov 26 21:08:32 2017 +0100 @@ -46,7 +46,7 @@ fix b have "b = f (g b)" using fg unfolding fun_eq_iff by simp - thus "EX a. b = f a" by blast + thus "\a. b = f a" by blast qed lemma case_sum_step: @@ -248,27 +248,27 @@ lemma snd_convol': "snd (\f, g\ x) = g x" using snd_convol unfolding convol_def by simp -lemma convol_expand_snd: "fst o f = g \ \g, snd o f\ = f" +lemma convol_expand_snd: "fst \ f = g \ \g, snd \ f\ = f" unfolding convol_def by auto lemma convol_expand_snd': - assumes "(fst o f = g)" - shows "h = snd o f \ \g, h\ = f" + assumes "(fst \ f = g)" + shows "h = snd \ f \ \g, h\ = f" proof - - from assms have *: "\g, snd o f\ = f" by (rule convol_expand_snd) - then have "h = snd o f \ h = snd o \g, snd o f\" by simp - moreover have "\ \ h = snd o f" by (simp add: snd_convol) + from assms have *: "\g, snd \ f\ = f" by (rule convol_expand_snd) + then have "h = snd \ f \ h = snd \ \g, snd \ f\" by simp + moreover have "\ \ h = snd \ f" by (simp add: snd_convol) moreover have "\ \ \g, h\ = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff) ultimately show ?thesis by simp qed -lemma case_sum_expand_Inr_pointfree: "f o Inl = g \ case_sum g (f o Inr) = f" +lemma case_sum_expand_Inr_pointfree: "f \ Inl = g \ case_sum g (f \ Inr) = f" by (auto split: sum.splits) -lemma case_sum_expand_Inr': "f o Inl = g \ h = f o Inr \ case_sum g h = f" +lemma case_sum_expand_Inr': "f \ Inl = g \ h = f \ Inr \ case_sum g h = f" by (rule iffI) (auto simp add: fun_eq_iff split: sum.splits) -lemma case_sum_expand_Inr: "f o Inl = g \ f x = case_sum g (f o Inr) x" +lemma case_sum_expand_Inr: "f \ Inl = g \ f x = case_sum g (f \ Inr) x" by (auto split: sum.splits) lemma id_transfer: "rel_fun A A id id" diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/BNF_Greatest_Fixpoint.thy --- a/src/HOL/BNF_Greatest_Fixpoint.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy Sun Nov 26 21:08:32 2017 +0100 @@ -36,7 +36,7 @@ lemma equiv_proj: assumes e: "equiv A R" and m: "z \ R" - shows "(proj R o fst) z = (proj R o snd) z" + shows "(proj R \ fst) z = (proj R \ snd) z" proof - from m have z: "(fst z, snd z) \ R" by auto with e have "\x. (fst z, x) \ R \ (snd z, x) \ R" "\x. (snd z, x) \ R \ (fst z, x) \ R" @@ -139,10 +139,10 @@ lemma fst_diag_id: "(fst \ (\x. (x, x))) z = id z" by simp lemma snd_diag_id: "(snd \ (\x. (x, x))) z = id z" by simp -lemma fst_diag_fst: "fst o ((\x. (x, x)) o fst) = fst" by auto -lemma snd_diag_fst: "snd o ((\x. (x, x)) o fst) = fst" by auto -lemma fst_diag_snd: "fst o ((\x. (x, x)) o snd) = snd" by auto -lemma snd_diag_snd: "snd o ((\x. (x, x)) o snd) = snd" by auto +lemma fst_diag_fst: "fst \ ((\x. (x, x)) \ fst) = fst" by auto +lemma snd_diag_fst: "snd \ ((\x. (x, x)) \ fst) = fst" by auto +lemma fst_diag_snd: "fst \ ((\x. (x, x)) \ snd) = snd" by auto +lemma snd_diag_snd: "snd \ ((\x. (x, x)) \ snd) = snd" by auto definition Succ where "Succ Kl kl = {k . kl @ [k] \ Kl}" definition Shift where "Shift Kl k = {kl. k # kl \ Kl}" diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/BNF_Least_Fixpoint.thy --- a/src/HOL/BNF_Least_Fixpoint.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/BNF_Least_Fixpoint.thy Sun Nov 26 21:08:32 2017 +0100 @@ -54,7 +54,7 @@ unfolding bij_betw_def inj_on_def by blast lemma surj_fun_eq: - assumes surj_on: "f ` X = UNIV" and eq_on: "\x \ X. (g1 o f) x = (g2 o f) x" + assumes surj_on: "f ` X = UNIV" and eq_on: "\x \ X. (g1 \ f) x = (g2 \ f) x" shows "g1 = g2" proof (rule ext) fix y diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/BNF_Wellorder_Constructions.thy --- a/src/HOL/BNF_Wellorder_Constructions.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/BNF_Wellorder_Constructions.thy Sun Nov 26 21:08:32 2017 +0100 @@ -368,7 +368,7 @@ where 1: "Well_order r \ Well_order r' \ Well_order r''" and "embed r r' f" and "embed r' r'' f'" using * ** unfolding ordLeq_def by blast - hence "embed r r'' (f' o f)" + hence "embed r r'' (f' \ f)" using comp_embed[of r r' f r'' f'] by auto thus "r \o r''" unfolding ordLeq_def using 1 by auto qed @@ -389,7 +389,7 @@ where 1: "Well_order r \ Well_order r' \ Well_order r''" and "iso r r' f" and 3: "iso r' r'' f'" using * ** unfolding ordIso_def by auto - hence "iso r r'' (f' o f)" + hence "iso r r'' (f' \ f)" using comp_iso[of r r' f r'' f'] by auto thus "r =o r''" unfolding ordIso_def using 1 by auto qed @@ -691,10 +691,10 @@ ultimately have "f23 ` (f12 ` ?A1) < f23 ` ?A2" by (simp add: inj_on_strict_subset) moreover - {have "embed r1 r3 (f23 o f12)" + {have "embed r1 r3 (f23 \ f12)" using 1 EMB23 0 by (auto simp add: comp_embed) hence "\a \ ?A1. f23(f12 a) = f13 a" - using EMB13 0 embed_unique[of r1 r3 "f23 o f12" f13] by auto + using EMB13 0 embed_unique[of r1 r3 "f23 \ f12" f13] by auto hence "f23 ` (f12 ` ?A1) = f13 ` ?A1" by force } ultimately diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/BNF_Wellorder_Embedding.thy --- a/src/HOL/BNF_Wellorder_Embedding.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/BNF_Wellorder_Embedding.thy Sun Nov 26 21:08:32 2017 +0100 @@ -128,7 +128,7 @@ lemma comp_embed: assumes WELL: "Well_order r" and EMB: "embed r r' f" and EMB': "embed r' r'' f'" -shows "embed r r'' (f' o f)" +shows "embed r r'' (f' \ f)" proof(unfold embed_def, auto) fix a assume *: "a \ Field r" hence "bij_betw f (under r a) (under r' (f a))" @@ -147,7 +147,7 @@ lemma comp_iso: assumes WELL: "Well_order r" and EMB: "iso r r' f" and EMB': "iso r' r'' f'" -shows "iso r r'' (f' o f)" +shows "iso r r'' (f' \ f)" using assms unfolding iso_def by (auto simp add: comp_embed bij_betw_trans) @@ -672,25 +672,25 @@ have Well': "wo_rel r'" using WELL' unfolding wo_rel_def . (* Main proof *) obtain H where H_def: "H = - (\h a. if False \ (snd o h)`(underS r a) \ (fst o h)`(underS r a) \ Field r' - then (wo_rel.suc r' ((fst o h)`(underS r a)), True) + (\h a. if False \ (snd \ h)`(underS r a) \ (fst \ h)`(underS r a) \ Field r' + then (wo_rel.suc r' ((fst \ h)`(underS r a)), True) else (undefined, False))" by blast have Adm: "wo_rel.adm_wo r H" using Well proof(unfold wo_rel.adm_wo_def, clarify) fix h1::"'a \ 'a' * bool" and h2::"'a \ 'a' * bool" and x assume "\y\underS r x. h1 y = h2 y" - hence "\y\underS r x. (fst o h1) y = (fst o h2) y \ - (snd o h1) y = (snd o h2) y" by auto - hence "(fst o h1)`(underS r x) = (fst o h2)`(underS r x) \ - (snd o h1)`(underS r x) = (snd o h2)`(underS r x)" + hence "\y\underS r x. (fst \ h1) y = (fst \ h2) y \ + (snd \ h1) y = (snd \ h2) y" by auto + hence "(fst \ h1)`(underS r x) = (fst \ h2)`(underS r x) \ + (snd \ h1)`(underS r x) = (snd \ h2)`(underS r x)" by (auto simp add: image_def) thus "H h1 x = H h2 x" by (simp add: H_def del: not_False_in_image_Ball) qed (* More constant definitions: *) obtain h::"'a \ 'a' * bool" and f::"'a \ 'a'" and g::"'a \ bool" where h_def: "h = wo_rel.worec r H" and - f_def: "f = fst o h" and g_def: "g = snd o h" by blast + f_def: "f = fst \ h" and g_def: "g = snd \ h" by blast obtain test where test_def: "test = (\ a. False \ (g`(underS r a)) \ f`(underS r a) \ Field r')" by blast (* *) @@ -813,19 +813,19 @@ EMB: "embed r r' f" and EMB': "embed r' r f'" shows "(\a \ Field r. f'(f a) = a) \ (\a' \ Field r'. f(f' a') = a')" proof- - have "embed r r (f' o f)" using assms + have "embed r r (f' \ f)" using assms by(auto simp add: comp_embed) moreover have "embed r r id" using assms by (auto simp add: id_embed) ultimately have "\a \ Field r. f'(f a) = a" - using assms embed_unique[of r r "f' o f" id] id_def by auto + using assms embed_unique[of r r "f' \ f" id] id_def by auto moreover - {have "embed r' r' (f o f')" using assms + {have "embed r' r' (f \ f')" using assms by(auto simp add: comp_embed) moreover have "embed r' r' id" using assms by (auto simp add: id_embed) ultimately have "\a' \ Field r'. f(f' a') = a'" - using assms embed_unique[of r' r' "f o f'" id] id_def by auto + using assms embed_unique[of r' r' "f \ f'" id] id_def by auto } ultimately show ?thesis by blast qed @@ -836,11 +836,11 @@ shows "bij_betw f (Field r) (Field r')" proof- let ?A = "Field r" let ?A' = "Field r'" - have "embed r r (g o f) \ embed r' r' (f o g)" + have "embed r r (g \ f) \ embed r' r' (f \ g)" using assms by (auto simp add: comp_embed) hence 1: "(\a \ ?A. g(f a) = a) \ (\a' \ ?A'. f(g a') = a')" - using WELL id_embed[of r] embed_unique[of r r "g o f" id] - WELL' id_embed[of r'] embed_unique[of r' r' "f o g" id] + using WELL id_embed[of r] embed_unique[of r r "g \ f" id] + WELL' id_embed[of r'] embed_unique[of r' r' "f \ g" id] id_def by auto have 2: "(\a \ ?A. f a \ ?A') \ (\a' \ ?A'. g a' \ ?A)" using assms embed_Field[of r r' f] embed_Field[of r' r g] by blast @@ -883,9 +883,9 @@ lemma embedS_comp_embed: assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''" and EMB: "embedS r r' f" and EMB': "embed r' r'' f'" -shows "embedS r r'' (f' o f)" +shows "embedS r r'' (f' \ f)" proof- - let ?g = "(f' o f)" let ?h = "inv_into (Field r) ?g" + let ?g = "(f' \ f)" let ?h = "inv_into (Field r) ?g" have 1: "embed r r' f \ \ (bij_betw f (Field r) (Field r'))" using EMB by (auto simp add: embedS_def) hence 2: "embed r r'' ?g" @@ -894,7 +894,7 @@ {assume "bij_betw ?g (Field r) (Field r'')" hence "embed r'' r ?h" using 2 WELL by (auto simp add: inv_into_Field_embed_bij_betw) - hence "embed r' r (?h o f')" using WELL' EMB' + hence "embed r' r (?h \ f')" using WELL' EMB' by (auto simp add: comp_embed) hence "bij_betw f (Field r) (Field r')" using WELL WELL' 1 by (auto simp add: embed_bothWays_Field_bij_betw) @@ -906,9 +906,9 @@ lemma embed_comp_embedS: assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''" and EMB: "embed r r' f" and EMB': "embedS r' r'' f'" -shows "embedS r r'' (f' o f)" +shows "embedS r r'' (f' \ f)" proof- - let ?g = "(f' o f)" let ?h = "inv_into (Field r) ?g" + let ?g = "(f' \ f)" let ?h = "inv_into (Field r) ?g" have 1: "embed r' r'' f' \ \ (bij_betw f' (Field r') (Field r''))" using EMB' by (auto simp add: embedS_def) hence 2: "embed r r'' ?g" @@ -917,7 +917,7 @@ {assume "bij_betw ?g (Field r) (Field r'')" hence "embed r'' r ?h" using 2 WELL by (auto simp add: inv_into_Field_embed_bij_betw) - hence "embed r'' r' (f o ?h)" using WELL'' EMB + hence "embed r'' r' (f \ ?h)" using WELL'' EMB by (auto simp add: comp_embed) hence "bij_betw f' (Field r') (Field r'')" using WELL' WELL'' 1 by (auto simp add: embed_bothWays_Field_bij_betw) @@ -929,28 +929,28 @@ lemma embed_comp_iso: assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''" and EMB: "embed r r' f" and EMB': "iso r' r'' f'" -shows "embed r r'' (f' o f)" +shows "embed r r'' (f' \ f)" using assms unfolding iso_def by (auto simp add: comp_embed) lemma iso_comp_embed: assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''" and EMB: "iso r r' f" and EMB': "embed r' r'' f'" -shows "embed r r'' (f' o f)" +shows "embed r r'' (f' \ f)" using assms unfolding iso_def by (auto simp add: comp_embed) lemma embedS_comp_iso: assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''" and EMB: "embedS r r' f" and EMB': "iso r' r'' f'" -shows "embedS r r'' (f' o f)" +shows "embedS r r'' (f' \ f)" using assms unfolding iso_def by (auto simp add: embedS_comp_embed) lemma iso_comp_embedS: assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''" and EMB: "iso r r' f" and EMB': "embedS r' r'' f'" -shows "embedS r r'' (f' o f)" +shows "embedS r r'' (f' \ f)" using assms unfolding iso_def using embed_comp_embedS by (auto simp add: embed_comp_embedS) diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Basic_BNFs.thy --- a/src/HOL/Basic_BNFs.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Basic_BNFs.thy Sun Nov 26 21:08:32 2017 +0100 @@ -19,8 +19,8 @@ "s = Inr x \ x \ setr s" lemma sum_set_defs[code]: - "setl = (\x. case x of Inl z => {z} | _ => {})" - "setr = (\x. case x of Inr z => {z} | _ => {})" + "setl = (\x. case x of Inl z \ {z} | _ \ {})" + "setr = (\x. case x of Inr z \ {z} | _ \ {})" by (auto simp: fun_eq_iff intro: setl.intros setr.intros elim: setl.cases setr.cases split: sum.splits) lemma rel_sum_simps[code, simp]: @@ -52,7 +52,7 @@ show "map_sum id id = id" by (rule map_sum.id) next fix f1 :: "'o \ 's" and f2 :: "'p \ 't" and g1 :: "'s \ 'q" and g2 :: "'t \ 'r" - show "map_sum (g1 o f1) (g2 o f2) = map_sum g1 g2 o map_sum f1 f2" + show "map_sum (g1 \ f1) (g2 \ f2) = map_sum g1 g2 \ map_sum f1 f2" by (rule map_sum.comp[symmetric]) next fix x and f1 :: "'o \ 'q" and f2 :: "'p \ 'r" and g1 g2 @@ -66,11 +66,11 @@ qed next fix f1 :: "'o \ 'q" and f2 :: "'p \ 'r" - show "setl o map_sum f1 f2 = image f1 o setl" + show "setl \ map_sum f1 f2 = image f1 \ setl" by (rule ext, unfold o_apply) (simp add: sum_set_defs(1) split: sum.split) next fix f1 :: "'o \ 'q" and f2 :: "'p \ 'r" - show "setr o map_sum f1 f2 = image f2 o setr" + show "setr \ map_sum f1 f2 = image f2 \ setr" by (rule ext, unfold o_apply) (simp add: sum_set_defs(2) split: sum.split) next show "card_order natLeq" by (rule natLeq_card_order) @@ -149,7 +149,7 @@ show "map_prod id id = id" by (rule map_prod.id) next fix f1 f2 g1 g2 - show "map_prod (g1 o f1) (g2 o f2) = map_prod g1 g2 o map_prod f1 f2" + show "map_prod (g1 \ f1) (g2 \ f2) = map_prod g1 g2 \ map_prod f1 f2" by (rule map_prod.comp[symmetric]) next fix x f1 f2 g1 g2 @@ -157,11 +157,11 @@ thus "map_prod f1 f2 x = map_prod g1 g2 x" by (cases x) simp next fix f1 f2 - show "(\x. {fst x}) o map_prod f1 f2 = image f1 o (\x. {fst x})" + show "(\x. {fst x}) \ map_prod f1 f2 = image f1 \ (\x. {fst x})" by (rule ext, unfold o_apply) simp next fix f1 f2 - show "(\x. {snd x}) o map_prod f1 f2 = image f2 o (\x. {snd x})" + show "(\x. {snd x}) \ map_prod f1 f2 = image f2 \ (\x. {snd x})" by (rule ext, unfold o_apply) simp next show "card_order natLeq" by (rule natLeq_card_order) diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Computational_Algebra/Polynomial.thy --- a/src/HOL/Computational_Algebra/Polynomial.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Computational_Algebra/Polynomial.thy Sun Nov 26 21:08:32 2017 +0100 @@ -1094,7 +1094,7 @@ lemma poly_prod: "poly (\k\A. p k) x = (\k\A. poly (p k) x)" by (induct A rule: infinite_finite_induct) simp_all -lemma degree_prod_sum_le: "finite S \ degree (prod f S) \ sum (degree o f) S" +lemma degree_prod_sum_le: "finite S \ degree (prod f S) \ sum (degree \ f) S" proof (induct S rule: finite_induct) case empty then show ?case by simp diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Computational_Algebra/Primes.thy --- a/src/HOL/Computational_Algebra/Primes.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Computational_Algebra/Primes.thy Sun Nov 26 21:08:32 2017 +0100 @@ -271,7 +271,7 @@ subsubsection \Make prime naively executable\ lemma prime_nat_iff': - "prime (p :: nat) \ p > 1 \ (\n \ {2.. p > 1 \ (\n \ {2.. n dvd p)" proof safe assume "p > 1" and *: "\n\{2..n dvd p" show "prime p" unfolding prime_nat_iff @@ -286,7 +286,7 @@ qed (auto simp: prime_nat_iff) lemma prime_int_iff': - "prime (p :: int) \ p > 1 \ (\n \ {2.. p > 1 \ (\n \ {2.. n dvd p)" (is "?lhs = ?rhs") proof assume "?lhs" thus "?rhs" @@ -352,9 +352,9 @@ lemma primes_infinite: "\ (finite {(p::nat). prime p})" proof assume "finite {(p::nat). prime p}" - with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))" + with Max_ge have "(\b. (\x \ {(p::nat). prime p}. x \ b))" by auto - then obtain b where "ALL (x::nat). prime x \ x <= b" + then obtain b where "\(x::nat). prime x \ x \ b" by auto with bigger_prime [of b] show False by auto diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Conditionally_Complete_Lattices.thy --- a/src/HOL/Conditionally_Complete_Lattices.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Conditionally_Complete_Lattices.thy Sun Nov 26 21:08:32 2017 +0100 @@ -430,7 +430,7 @@ assumes "a < b" and "P a" and "\ P b" shows "\c. a \ c \ c \ b \ (\x. a \ x \ x < c \ P x) \ (\d. (\x. a \ x \ x < d \ P x) \ d \ c)" -proof (rule exI [where x = "Sup {d. \x. a \ x & x < d --> P x}"], auto) +proof (rule exI [where x = "Sup {d. \x. a \ x \ x < d \ P x}"], auto) show "a \ Sup {d. \c. a \ c \ c < d \ P c}" by (rule cSup_upper, auto simp: bdd_above_def) (metis \a < b\ \\ P b\ linear less_le) @@ -439,7 +439,7 @@ apply (rule cSup_least) apply auto apply (metis less_le_not_le) - apply (metis \a \~ P b\ linear less_le) + apply (metis \a \\ P b\ linear less_le) done next fix x @@ -454,7 +454,7 @@ assume 0: "\x. a \ x \ x < d \ P x" thus "d \ Sup {d. \c. a \ c \ c < d \ P c}" by (rule_tac cSup_upper, auto simp: bdd_above_def) - (metis \a \~ P b\ linear less_le) + (metis \a \\ P b\ linear less_le) qed end diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Divides.thy --- a/src/HOL/Divides.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Divides.thy Sun Nov 26 21:08:32 2017 +0100 @@ -673,7 +673,7 @@ "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)" by (fact div_add1_eq) -lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)" +lemma zmod_eq_0_iff: "(m mod d = 0) = (\q::int. m = d*q)" by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def) (* REVISIT: should this be generalized to all semiring_div types? *) @@ -769,20 +769,20 @@ text\The proofs of the two lemmas below are essentially identical\ lemma split_pos_lemma: - "0 - P(n div k :: int)(n mod k) = (\i j. 0\j & j P i j)" + "0 + P(n div k :: int)(n mod k) = (\i j. 0\j \ j n = k*i + j \ P i j)" by auto lemma split_neg_lemma: - "k<0 ==> - P(n div k :: int)(n mod k) = (\i j. k0 & n = k*i + j --> P i j)" + "k<0 \ + P(n div k :: int)(n mod k) = (\i j. k j\0 \ n = k*i + j \ P i j)" by auto lemma split_zdiv: "P(n div k :: int) = - ((k = 0 --> P 0) & - (0 (\i j. 0\j & j P i)) & - (k<0 --> (\i j. k0 & n = k*i + j --> P i)))" + ((k = 0 \ P 0) \ + (0 (\i j. 0\j \ j n = k*i + j \ P i)) \ + (k<0 \ (\i j. k j\0 \ n = k*i + j \ P i)))" apply (cases "k = 0") apply simp apply (simp only: linorder_neq_iff) @@ -792,9 +792,9 @@ lemma split_zmod: "P(n mod k :: int) = - ((k = 0 --> P n) & - (0 (\i j. 0\j & j P j)) & - (k<0 --> (\i j. k0 & n = k*i + j --> P j)))" + ((k = 0 \ P n) \ + (0 (\i j. 0\j \ j n = k*i + j \ P j)) \ + (k<0 \ (\i j. k j\0 \ n = k*i + j \ P j)))" apply (case_tac "k=0", simp) apply (simp only: linorder_neq_iff) apply (erule disjE) @@ -955,7 +955,7 @@ by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff) lemma nonneg1_imp_zdiv_pos_iff: - "(0::int) <= a \ (a div b > 0) = (a >= b & b>0)" + "(0::int) \ a \ (a div b > 0) = (a \ b \ b>0)" apply rule apply rule using div_pos_pos_trivial[of a b]apply arith diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Enum.thy --- a/src/HOL/Enum.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Enum.thy Sun Nov 26 21:08:32 2017 +0100 @@ -88,7 +88,7 @@ [code del]: "enum_the = The" lemma [code]: - "The P = (case filter P enum of [x] => x | _ => enum_the P)" + "The P = (case filter P enum of [x] \ x | _ \ enum_the P)" proof - { fix a @@ -212,16 +212,16 @@ then have "\ n. x : bacc r n" proof (induct x arbitrary: rule: acc.induct) case (accI x) - then have "\y. \ n. (y, x) \ r --> y : bacc r n" by simp + then have "\y. \ n. (y, x) \ r \ y \ bacc r n" by simp from choice[OF this] obtain n where n: "\y. (y, x) \ r \ y \ bacc r (n y)" .. - obtain n where "\y. (y, x) : r \ y : bacc r n" + obtain n where "\y. (y, x) \ r \ y \ bacc r n" proof - fix y assume y: "(y, x) : r" + fix y assume y: "(y, x) \ r" with n have "y : bacc r (n y)" by auto - moreover have "n y <= Max ((%(y, x). n y) ` r)" + moreover have "n y <= Max ((\(y, x). n y) ` r)" using y \finite r\ by (auto intro!: Max_ge) note bacc_mono[OF this, of r] - ultimately show "y : bacc r (Max ((%(y, x). n y) ` r))" by auto + ultimately show "y : bacc r (Max ((\(y, x). n y) ` r))" by auto qed then show ?case by (auto simp add: Let_def intro!: exI[of _ "Suc n"]) @@ -297,13 +297,13 @@ begin definition - "enum = map (\ys. the o map_of (zip (enum::'a list) ys)) (List.n_lists (length (enum::'a::enum list)) enum)" + "enum = map (\ys. the \ map_of (zip (enum::'a list) ys)) (List.n_lists (length (enum::'a::enum list)) enum)" definition - "enum_all P = all_n_lists (\bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))" + "enum_all P = all_n_lists (\bs. P (the \ map_of (zip enum bs))) (length (enum :: 'a list))" definition - "enum_ex P = ex_n_lists (\bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))" + "enum_ex P = ex_n_lists (\bs. P (the \ map_of (zip enum bs))) (length (enum :: 'a list))" instance proof show "UNIV = set (enum :: ('a \ 'b) list)" @@ -368,17 +368,17 @@ end lemma enum_fun_code [code]: "enum = (let enum_a = (enum :: 'a::{enum, equal} list) - in map (\ys. the o map_of (zip enum_a ys)) (List.n_lists (length enum_a) enum))" + in map (\ys. the \ map_of (zip enum_a ys)) (List.n_lists (length enum_a) enum))" by (simp add: enum_fun_def Let_def) lemma enum_all_fun_code [code]: "enum_all P = (let enum_a = (enum :: 'a::{enum, equal} list) - in all_n_lists (\bs. P (the o map_of (zip enum_a bs))) (length enum_a))" + in all_n_lists (\bs. P (the \ map_of (zip enum_a bs))) (length enum_a))" by (simp only: enum_all_fun_def Let_def) lemma enum_ex_fun_code [code]: "enum_ex P = (let enum_a = (enum :: 'a::{enum, equal} list) - in ex_n_lists (\bs. P (the o map_of (zip enum_a bs))) (length enum_a))" + in ex_n_lists (\bs. P (the \ map_of (zip enum_a bs))) (length enum_a))" by (simp only: enum_ex_fun_def Let_def) instantiation set :: (enum) enum diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Fields.thy --- a/src/HOL/Fields.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Fields.thy Sun Nov 26 21:08:32 2017 +0100 @@ -400,10 +400,10 @@ lemma inverse_mult_distrib [simp]: "inverse (a * b) = inverse a * inverse b" proof cases - assume "a \ 0 & b \ 0" + assume "a \ 0 \ b \ 0" thus ?thesis by (simp add: nonzero_inverse_mult_distrib ac_simps) next - assume "~ (a \ 0 & b \ 0)" + assume "\ (a \ 0 \ b \ 0)" thus ?thesis by force qed @@ -596,7 +596,7 @@ assumes invle: "inverse a \ inverse b" and apos: "0 < a" shows "b \ a" proof (rule classical) - assume "~ b \ a" + assume "\ b \ a" hence "a < b" by (simp add: linorder_not_le) hence bpos: "0 < b" by (blast intro: apos less_trans) hence "a * inverse a \ a * inverse b" @@ -649,9 +649,9 @@ assumes less: "a < b" and apos: "0 < a" shows "inverse b < inverse a" proof (rule ccontr) - assume "~ inverse b < inverse a" + assume "\ inverse b < inverse a" hence "inverse a \ inverse b" by simp - hence "~ (a < b)" + hence "\ (a < b)" by (simp add: not_less inverse_le_imp_le [OF _ apos]) thus False by (rule notE [OF _ less]) qed @@ -1142,19 +1142,19 @@ text\Simplify quotients that are compared with the value 1.\ lemma le_divide_eq_1: - "(1 \ b / a) = ((0 < a & a \ b) | (a < 0 & b \ a))" + "(1 \ b / a) = ((0 < a \ a \ b) \ (a < 0 \ b \ a))" by (auto simp add: le_divide_eq) lemma divide_le_eq_1: - "(b / a \ 1) = ((0 < a & b \ a) | (a < 0 & a \ b) | a=0)" + "(b / a \ 1) = ((0 < a \ b \ a) \ (a < 0 \ a \ b) \ a=0)" by (auto simp add: divide_le_eq) lemma less_divide_eq_1: - "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))" + "(1 < b / a) = ((0 < a \ a < b) \ (a < 0 \ b < a))" by (auto simp add: less_divide_eq) lemma divide_less_eq_1: - "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)" + "(b / a < 1) = ((0 < a \ b < a) \ (a < 0 \ a < b) \ a=0)" by (auto simp add: divide_less_eq) lemma divide_nonneg_nonneg [simp]: @@ -1208,11 +1208,11 @@ by (auto simp add: divide_less_eq) lemma eq_divide_eq_1 [simp]: - "(1 = b/a) = ((a \ 0 & a = b))" + "(1 = b/a) = ((a \ 0 \ a = b))" by (auto simp add: eq_divide_eq) lemma divide_eq_eq_1 [simp]: - "(b/a = 1) = ((a \ 0 & a = b))" + "(b/a = 1) = ((a \ 0 \ a = b))" by (auto simp add: divide_eq_eq) lemma abs_div_pos: "0 < y ==> @@ -1221,10 +1221,10 @@ apply (simp add: order_less_imp_le) done -lemma zero_le_divide_abs_iff [simp]: "(0 \ a / \b\) = (0 \ a | b = 0)" +lemma zero_le_divide_abs_iff [simp]: "(0 \ a / \b\) = (0 \ a \ b = 0)" by (auto simp: zero_le_divide_iff) -lemma divide_le_0_abs_iff [simp]: "(a / \b\ \ 0) = (a \ 0 | b = 0)" +lemma divide_le_0_abs_iff [simp]: "(a / \b\ \ 0) = (a \ 0 \ b = 0)" by (auto simp: divide_le_0_iff) lemma field_le_mult_one_interval: diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Groebner_Basis.thy Sun Nov 26 21:08:32 2017 +0100 @@ -19,8 +19,8 @@ by blast+ lemma dnf: - "(P & (Q | R)) = ((P&Q) | (P&R))" - "((Q | R) & P) = ((Q&P) | (R&P))" + "(P \ (Q \ R)) = ((P\Q) \ (P\R))" + "((Q \ R) \ P) = ((Q\P) \ (R\P))" "(P \ Q) = (Q \ P)" "(P \ Q) = (Q \ P)" by blast+ diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/HOL.thy Sun Nov 26 21:08:32 2017 +0100 @@ -1627,12 +1627,10 @@ subsection \Other simple lemmas and lemma duplicates\ -lemma all_cong: "(\x. Q x \ P x = P' x) \ - (ALL x. Q x \ P x) = (ALL x. Q x \ P' x)" +lemma all_cong: "(\x. Q x \ P x = P' x) \ (\x. Q x \ P x) = (\x. Q x \ P' x)" by auto -lemma ex_cong: "(\x. Q x \ P x = P' x) \ - (EX x. Q x \ P x) = (EX x. Q x \ P' x)" +lemma ex_cong: "(\x. Q x \ P x = P' x) \ (\x. Q x \ P x) = (\x. Q x \ P' x)" by auto lemma ex1_eq [iff]: "\!x. x = t" "\!x. t = x" diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Library/BNF_Corec.thy --- a/src/HOL/Library/BNF_Corec.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Library/BNF_Corec.thy Sun Nov 26 21:08:32 2017 +0100 @@ -31,17 +31,17 @@ unfolding BNF_Def.Grp_def by auto lemma sum_comp_cases: - assumes "f o Inl = g o Inl" and "f o Inr = g o Inr" + assumes "f \ Inl = g \ Inl" and "f \ Inr = g \ Inr" shows "f = g" proof (rule ext) fix a show "f a = g a" using assms unfolding comp_def fun_eq_iff by (cases a) auto qed -lemma case_sum_Inl_Inr_L: "case_sum (f o Inl) (f o Inr) = f" +lemma case_sum_Inl_Inr_L: "case_sum (f \ Inl) (f \ Inr) = f" by (metis case_sum_expand_Inr') -lemma eq_o_InrI: "\g o Inl = h; case_sum h f = g\ \ f = g o Inr" +lemma eq_o_InrI: "\g \ Inl = h; case_sum h f = g\ \ f = g \ Inr" by (auto simp: fun_eq_iff split: sum.splits) lemma id_bnf_o: "BNF_Composition.id_bnf \ f = f" @@ -63,7 +63,7 @@ subsection \Coinduction\ -lemma eq_comp_compI: "a o b = f o x \ x o c = id \ f = a o (b o c)" +lemma eq_comp_compI: "a \ b = f \ x \ x \ c = id \ f = a \ (b \ c)" unfolding fun_eq_iff by simp lemma self_bounded_weaken_left: "(a :: 'a :: semilattice_inf) \ inf a b \ a \ b" @@ -159,7 +159,7 @@ by (simp add: antisym cong_gen_cong gen_cong_minimal leq_gen_cong) lemma gen_cong_rho: - "\ = eval o f \ rel (gen_cong R) (f x) (f y) \ gen_cong R (\ x) (\ y)" + "\ = eval \ f \ rel (gen_cong R) (f x) (f y) \ gen_cong R (\ x) (\ y)" by (simp add: gen_cong_eval) lemma coinduction: assumes coind: "\R. R \ retr R \ R \ op =" @@ -181,7 +181,7 @@ fixes rel eval rel' eval' retr emb assumes base: "cong rel eval retr" and step: "cong rel' eval' retr" - and emb: "eval' o emb = eval" + and emb: "eval' \ emb = eval" and emb_transfer: "rel_fun (rel R) (rel' R) emb emb" begin diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Library/Cardinality.thy --- a/src/HOL/Library/Cardinality.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Library/Cardinality.thy Sun Nov 26 21:08:32 2017 +0100 @@ -92,7 +92,7 @@ unfolding bs[symmetric] distinct_card[OF distb] .. have ca: "CARD('a) = length as" unfolding as[symmetric] distinct_card[OF dista] .. - let ?xs = "map (\ys. the o map_of (zip as ys)) (List.n_lists (length as) bs)" + let ?xs = "map (\ys. the \ map_of (zip as ys)) (List.n_lists (length as) bs)" have "UNIV = set ?xs" proof(rule UNIV_eq_I) fix f :: "'a \ 'b" diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Library/DAList.thy --- a/src/HOL/Library/DAList.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Library/DAList.thy Sun Nov 26 21:08:32 2017 +0100 @@ -22,7 +22,7 @@ typedef ('key, 'value) alist = "{xs :: ('key \ 'value) list. (distinct \ map fst) xs}" morphisms impl_of Alist proof - show "[] \ {xs. (distinct o map fst) xs}" + show "[] \ {xs. (distinct \ map fst) xs}" by simp qed diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Library/Diagonal_Subsequence.thy --- a/src/HOL/Library/Diagonal_Subsequence.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Library/Diagonal_Subsequence.thy Sun Nov 26 21:08:32 2017 +0100 @@ -8,22 +8,22 @@ locale subseqs = fixes P::"nat\(nat\nat)\bool" - assumes ex_subseq: "\n s. strict_mono (s::nat\nat) \ \r'. strict_mono r' \ P n (s o r')" + assumes ex_subseq: "\n s. strict_mono (s::nat\nat) \ \r'. strict_mono r' \ P n (s \ r')" begin -definition reduce where "reduce s n = (SOME r'::nat\nat. strict_mono r' \ P n (s o r'))" +definition reduce where "reduce s n = (SOME r'::nat\nat. strict_mono r' \ P n (s \ r'))" lemma subseq_reduce[intro, simp]: "strict_mono s \ strict_mono (reduce s n)" unfolding reduce_def by (rule someI2_ex[OF ex_subseq]) auto lemma reduce_holds: - "strict_mono s \ P n (s o reduce s n)" + "strict_mono s \ P n (s \ reduce s n)" unfolding reduce_def by (rule someI2_ex[OF ex_subseq]) (auto simp: o_def) primrec seqseq :: "nat \ nat \ nat" where "seqseq 0 = id" -| "seqseq (Suc n) = seqseq n o reduce (seqseq n) n" +| "seqseq (Suc n) = seqseq n \ reduce (seqseq n) n" lemma subseq_seqseq[intro, simp]: "strict_mono (seqseq n)" proof (induct n) @@ -35,7 +35,7 @@ lemma seqseq_holds: "P n (seqseq (Suc n))" proof - - have "P n (seqseq n o reduce (seqseq n) n)" + have "P n (seqseq n \ reduce (seqseq n) n)" by (intro reduce_holds subseq_seqseq) thus ?thesis by simp qed @@ -57,14 +57,14 @@ primrec fold_reduce where "fold_reduce n 0 = id" -| "fold_reduce n (Suc k) = fold_reduce n k o reduce (seqseq (n + k)) (n + k)" +| "fold_reduce n (Suc k) = fold_reduce n k \ reduce (seqseq (n + k)) (n + k)" lemma subseq_fold_reduce[intro, simp]: "strict_mono (fold_reduce n k)" proof (induct k) case (Suc k) from strict_mono_o[OF this subseq_reduce] show ?case by (simp add: o_def) qed (simp add: strict_mono_def) -lemma ex_subseq_reduce_index: "seqseq (n + k) = seqseq n o fold_reduce n k" +lemma ex_subseq_reduce_index: "seqseq (n + k) = seqseq n \ fold_reduce n k" by (induct k) simp_all lemma seqseq_fold_reduce: "seqseq n = fold_reduce 0 n" @@ -73,20 +73,20 @@ lemma diagseq_fold_reduce: "diagseq n = fold_reduce 0 n n" using seqseq_fold_reduce by (simp add: diagseq_def) -lemma fold_reduce_add: "fold_reduce 0 (m + n) = fold_reduce 0 m o fold_reduce m n" +lemma fold_reduce_add: "fold_reduce 0 (m + n) = fold_reduce 0 m \ fold_reduce m n" by (induct n) simp_all -lemma diagseq_add: "diagseq (k + n) = (seqseq k o (fold_reduce k n)) (k + n)" +lemma diagseq_add: "diagseq (k + n) = (seqseq k \ (fold_reduce k n)) (k + n)" proof - have "diagseq (k + n) = fold_reduce 0 (k + n) (k + n)" by (simp add: diagseq_fold_reduce) - also have "\ = (seqseq k o fold_reduce k n) (k + n)" + also have "\ = (seqseq k \ fold_reduce k n) (k + n)" unfolding fold_reduce_add seqseq_fold_reduce .. finally show ?thesis . qed lemma diagseq_sub: - assumes "m \ n" shows "diagseq n = (seqseq m o (fold_reduce m (n - m))) n" + assumes "m \ n" shows "diagseq n = (seqseq m \ (fold_reduce m (n - m))) n" using diagseq_add[of m "n - m"] assms by simp lemma subseq_diagonal_rest: "strict_mono (\x. fold_reduce k x (k + x))" @@ -100,12 +100,12 @@ finally show "?lhs < \" . qed -lemma diagseq_seqseq: "diagseq o (op + k) = (seqseq k o (\x. fold_reduce k x (k + x)))" +lemma diagseq_seqseq: "diagseq \ (op + k) = (seqseq k \ (\x. fold_reduce k x (k + x)))" by (auto simp: o_def diagseq_add) lemma diagseq_holds: - assumes subseq_stable: "\r s n. strict_mono r \ P n s \ P n (s o r)" - shows "P k (diagseq o (op + (Suc k)))" + assumes subseq_stable: "\r s n. strict_mono r \ P n s \ P n (s \ r)" + shows "P k (diagseq \ (op + (Suc k)))" unfolding diagseq_seqseq by (intro subseq_stable subseq_diagonal_rest seqseq_holds) end diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Library/Extended.thy --- a/src/HOL/Library/Extended.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Library/Extended.thy Sun Nov 26 21:08:32 2017 +0100 @@ -23,7 +23,7 @@ case_of_simps less_eq_extended_case: less_eq_extended.simps definition less_extended :: "'a extended \ 'a extended \ bool" where -"((x::'a extended) < y) = (x \ y & \ y \ x)" +"((x::'a extended) < y) = (x \ y \ \ y \ x)" instance by intro_classes (auto simp: less_extended_def less_eq_extended_case split: extended.splits) diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Library/Extended_Nat.thy --- a/src/HOL/Library/Extended_Nat.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Library/Extended_Nat.thy Sun Nov 26 21:08:32 2017 +0100 @@ -602,9 +602,9 @@ by (induct n) auto lemma enat_less_induct: - assumes prem: "!!n. \m::enat. m < n --> P m ==> P n" shows "P n" + assumes prem: "\n. \m::enat. m < n \ P m \ P n" shows "P n" proof - - have P_enat: "!!k. P (enat k)" + have P_enat: "\k. P (enat k)" apply (rule nat_less_induct) apply (rule prem, clarify) apply (erule less_enatE, simp) diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Library/Extended_Real.thy Sun Nov 26 21:08:32 2017 +0100 @@ -1138,7 +1138,7 @@ } moreover { - assume "y = -\ | y = \" + assume "y = -\ \ y = \" then have ?thesis using assms[rule_format, of 1] by (cases x) auto } @@ -2845,7 +2845,7 @@ proof - { fix x - have "(real_of_ereal o ereal) x = id x" + have "(real_of_ereal \ ereal) x = id x" by auto } then show ?thesis diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Library/FSet.thy --- a/src/HOL/Library/FSet.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Library/FSet.thy Sun Nov 26 21:08:32 2017 +0100 @@ -510,7 +510,7 @@ by transfer auto lemma pfsubset_ffilter: - "(\x. x |\| A \ P x \ Q x) \ (x |\| A & \ P x & Q x) \ + "(\x. x |\| A \ P x \ Q x) \ (x |\| A \ \ P x \ Q x) \ ffilter P A |\| ffilter Q A" unfolding less_fset_def by (auto simp add: subset_ffilter eq_ffilter) diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Library/Old_Datatype.thy --- a/src/HOL/Library/Old_Datatype.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Library/Old_Datatype.thy Sun Nov 26 21:08:32 2017 +0100 @@ -15,7 +15,7 @@ subsection \The datatype universe\ -definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}" +definition "Node = {p. \f x k. p = (f :: nat => 'b + nat, x ::'a + nat) \ f k = Inr 0}" typedef ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set" morphisms Rep_Node Abs_Node @@ -44,9 +44,9 @@ (*Leaf nodes, with arbitrary or nat labels*) definition Leaf :: "'a => ('a, 'b) dtree" - where "Leaf == Atom o Inl" + where "Leaf == Atom \ Inl" definition Numb :: "nat => ('a, 'b) dtree" - where "Numb == Atom o Inr" + where "Numb == Atom \ Inr" (*Injections of the "disjoint sum"*) definition In0 :: "('a, 'b) dtree => ('a, 'b) dtree" @@ -56,13 +56,13 @@ (*Function spaces*) definition Lim :: "('b => ('a, 'b) dtree) => ('a, 'b) dtree" - where "Lim f == \{z. ? x. z = Push_Node (Inl x) ` (f x)}" + where "Lim f == \{z. \x. z = Push_Node (Inl x) ` (f x)}" (*the set of nodes with depth less than k*) definition ndepth :: "('a, 'b) node => nat" where "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)" definition ntrunc :: "[nat, ('a, 'b) dtree] => ('a, 'b) dtree" - where "ntrunc k N == {n. n:N & ndepth(n) ndepth(n) ('a, 'b) dtree set" @@ -72,10 +72,10 @@ (*the corresponding eliminators*) definition Split :: "[[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c" - where "Split c M == THE u. EX x y. M = Scons x y & u = c x y" + where "Split c M == THE u. \x y. M = Scons x y \ u = c x y" definition Case :: "[[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c" - where "Case c d M == THE u. (EX x . M = In0(x) & u = c(x)) | (EX y . M = In1(y) & u = d(y))" + where "Case c d M == THE u. (\x . M = In0(x) \ u = c(x)) \ (\y . M = In1(y) \ u = d(y))" (** equality for the "universe" **) @@ -207,7 +207,7 @@ "[| Scons M N = Scons M' N'; [| M=M'; N=N' |] ==> P |] ==> P" by (iprover dest: Scons_inject1 Scons_inject2) -lemma Scons_Scons_eq [iff]: "(Scons M N = Scons M' N') = (M=M' & N=N')" +lemma Scons_Scons_eq [iff]: "(Scons M N = Scons M' N') = (M=M' \ N=N')" by (blast elim!: Scons_inject) (*** Distinctness involving Leaf and Numb ***) @@ -241,7 +241,7 @@ by (simp add: ndepth_def Node_K0_I [THEN Abs_Node_inverse] Least_equality) lemma ndepth_Push_Node_aux: - "case_nat (Inr (Suc i)) f k = Inr 0 --> Suc(LEAST x. f x = Inr 0) <= k" + "case_nat (Inr (Suc i)) f k = Inr 0 \ Suc(LEAST x. f x = Inr 0) \ k" apply (induct_tac "k", auto) apply (erule Least_le) done @@ -385,7 +385,7 @@ done lemma ntrunc_o_equality: - "[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2" + "[| !!k. (ntrunc(k) \ h1) = (ntrunc(k) \ h2) |] ==> h1=h2" apply (rule ntrunc_equality [THEN ext]) apply (simp add: fun_eq_iff) done diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Library/Old_Recdef.thy --- a/src/HOL/Library/Old_Recdef.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Library/Old_Recdef.thy Sun Nov 26 21:08:32 2017 +0100 @@ -13,8 +13,8 @@ subsection \Lemmas for TFL\ -lemma tfl_wf_induct: "ALL R. wf R --> - (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))" +lemma tfl_wf_induct: "\R. wf R \ + (\P. (\x. (\y. (y,x)\R \ P y) \ P x) \ (\x. P x))" apply clarify apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast) done @@ -22,39 +22,39 @@ lemma tfl_cut_def: "cut f r x \ (\y. if (y,x) \ r then f y else undefined)" unfolding cut_def . -lemma tfl_cut_apply: "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)" +lemma tfl_cut_apply: "\f R. (x,a)\R \ (cut f R a)(x) = f(x)" apply clarify apply (rule cut_apply, assumption) done lemma tfl_wfrec: - "ALL M R f. (f=wfrec R M) --> wf R --> (ALL x. f x = M (cut f R x) x)" + "\M R f. (f=wfrec R M) \ wf R \ (\x. f x = M (cut f R x) x)" apply clarify apply (erule wfrec) done -lemma tfl_eq_True: "(x = True) --> x" +lemma tfl_eq_True: "(x = True) \ x" by blast -lemma tfl_rev_eq_mp: "(x = y) --> y --> x" +lemma tfl_rev_eq_mp: "(x = y) \ y \ x" by blast -lemma tfl_simp_thm: "(x --> y) --> (x = x') --> (x' --> y)" +lemma tfl_simp_thm: "(x \ y) \ (x = x') \ (x' \ y)" by blast -lemma tfl_P_imp_P_iff_True: "P ==> P = True" +lemma tfl_P_imp_P_iff_True: "P \ P = True" by blast -lemma tfl_imp_trans: "(A --> B) ==> (B --> C) ==> (A --> C)" +lemma tfl_imp_trans: "(A \ B) \ (B \ C) \ (A \ C)" by blast -lemma tfl_disj_assoc: "(a \ b) \ c == a \ (b \ c)" +lemma tfl_disj_assoc: "(a \ b) \ c \ a \ (b \ c)" by simp -lemma tfl_disjE: "P \ Q ==> P --> R ==> Q --> R ==> R" +lemma tfl_disjE: "P \ Q \ P \ R \ Q \ R \ R" by blast -lemma tfl_exE: "\x. P x ==> \x. P x --> Q ==> Q" +lemma tfl_exE: "\x. P x \ \x. P x \ Q \ Q" by blast ML_file "old_recdef.ML" diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Library/Option_ord.thy --- a/src/HOL/Library/Option_ord.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Library/Option_ord.thy Sun Nov 26 21:08:32 2017 +0100 @@ -101,12 +101,12 @@ fix z :: "'a option" assume H: "\x. (\y. y < x \ P y) \ P x" have "P None" by (rule H) simp - then have P_Some [case_names Some]: "P z" if "\x. z = Some x \ (P o Some) x" for z + then have P_Some [case_names Some]: "P z" if "\x. z = Some x \ (P \ Some) x" for z using \P None\ that by (cases z) simp_all show "P z" proof (cases z rule: P_Some) case (Some w) - show "(P o Some) w" + show "(P \ Some) w" proof (induct rule: less_induct) case (less x) have "P (Some x)" @@ -117,7 +117,7 @@ proof (cases y rule: P_Some) case (Some v) with \y < Some x\ have "v < x" by simp - with less show "(P o Some) v" . + with less show "(P \ Some) v" . qed qed then show ?case by simp diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Library/Predicate_Compile_Alternative_Defs.thy --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Sun Nov 26 21:08:32 2017 +0100 @@ -15,11 +15,11 @@ declare less_bool_def[abs_def, code_pred_inline] declare le_bool_def[abs_def, code_pred_inline] -lemma min_bool_eq [code_pred_inline]: "(min :: bool => bool => bool) == (op &)" +lemma min_bool_eq [code_pred_inline]: "(min :: bool => bool => bool) == (op \)" by (rule eq_reflection) (auto simp add: fun_eq_iff min_def) lemma [code_pred_inline]: - "((A::bool) ~= (B::bool)) = ((A & ~ B) | (B & ~ A))" + "((A::bool) \ (B::bool)) = ((A \ \ B) \ (B \ \ A))" by fast setup \Predicate_Compile_Data.ignore_consts [@{const_name Let}]\ @@ -45,7 +45,7 @@ by (simp add: fun_eq_iff) lemma subset_eq[code_pred_inline]: - "(P :: 'a => bool) < (Q :: 'a => bool) == ((\x. Q x \ (\ P x)) \ (\ x. P x --> Q x))" + "(P :: 'a \ bool) < (Q :: 'a \ bool) \ ((\x. Q x \ (\ P x)) \ (\x. P x \ Q x))" by (rule eq_reflection) (auto simp add: less_fun_def le_fun_def) lemma set_equality[code_pred_inline]: diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Library/Product_Order.thy --- a/src/HOL/Library/Product_Order.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Library/Product_Order.thy Sun Nov 26 21:08:32 2017 +0100 @@ -220,11 +220,11 @@ of two complete lattices:\ lemma INF_prod_alt_def: - "INFIMUM A f = (INFIMUM A (fst o f), INFIMUM A (snd o f))" + "INFIMUM A f = (INFIMUM A (fst \ f), INFIMUM A (snd \ f))" unfolding Inf_prod_def by simp lemma SUP_prod_alt_def: - "SUPREMUM A f = (SUPREMUM A (fst o f), SUPREMUM A (snd o f))" + "SUPREMUM A f = (SUPREMUM A (fst \ f), SUPREMUM A (snd \ f))" unfolding Sup_prod_def by simp diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Library/RBT_Set.thy --- a/src/HOL/Library/RBT_Set.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Library/RBT_Set.thy Sun Nov 26 21:08:32 2017 +0100 @@ -548,8 +548,8 @@ lemma subset_Coset_empty_Set_empty [code]: "Coset t1 \ Set t2 \ (case (RBT.impl_of t1, RBT.impl_of t2) of - (rbt.Empty, rbt.Empty) => False | - (_, _) => Code.abort (STR ''non_empty_trees'') (\_. Coset t1 \ Set t2))" + (rbt.Empty, rbt.Empty) \ False | + (_, _) \ Code.abort (STR ''non_empty_trees'') (\_. Coset t1 \ Set t2))" proof - have *: "\t. RBT.impl_of t = rbt.Empty \ t = RBT rbt.Empty" by (subst(asm) RBT_inverse[symmetric]) (auto simp: impl_of_inject) @@ -568,7 +568,7 @@ by (auto simp add: card.eq_fold intro: finite_fold_fold_keys comp_fun_commute_const) lemma sum_Set [code]: - "sum f (Set xs) = fold_keys (plus o f) xs 0" + "sum f (Set xs) = fold_keys (plus \ f) xs 0" proof - have "comp_fun_commute (\x. op + (f x))" by standard (auto simp: ac_simps) diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Library/Ramsey.thy --- a/src/HOL/Library/Ramsey.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Library/Ramsey.thy Sun Nov 26 21:08:32 2017 +0100 @@ -27,7 +27,7 @@ (is "\r\1. ?R m n r") proof (induct k \ "m + n" arbitrary: m n) case 0 - show ?case (is "EX r. ?Q r") + show ?case (is "\r. ?Q r") proof from 0 show "?Q 1" by (clarsimp simp: indep_def) (metis card.empty emptyE empty_subsetI) @@ -35,7 +35,7 @@ next case (Suc k) consider "m = 0 \ n = 0" | "m \ 0" "n \ 0" by auto - then show ?case (is "EX r. ?Q r") + then show ?case (is "\r. ?Q r") proof cases case 1 then have "?Q 1" diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Library/Stream.thy --- a/src/HOL/Library/Stream.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Library/Stream.thy Sun Nov 26 21:08:32 2017 +0100 @@ -251,7 +251,7 @@ lemma sdrop_while_sdrop_LEAST: assumes "\n. P (s !! n)" - shows "sdrop_while (Not o P) s = sdrop (LEAST n. P (s !! n)) s" + shows "sdrop_while (Not \ P) s = sdrop (LEAST n. P (s !! n)) s" proof - from assms obtain m where "P (s !! m)" "\n. P (s !! n) \ m \ n" and *: "(LEAST n. P (s !! n)) = m" by atomize_elim (auto intro: LeastI Least_le) @@ -266,8 +266,8 @@ qed primcorec sfilter where - "shd (sfilter P s) = shd (sdrop_while (Not o P) s)" -| "stl (sfilter P s) = sfilter P (stl (sdrop_while (Not o P) s))" + "shd (sfilter P s) = shd (sdrop_while (Not \ P) s)" +| "stl (sfilter P s) = sfilter P (stl (sdrop_while (Not \ P) s))" lemma sfilter_Stream: "sfilter P (x ## s) = (if P x then x ## sfilter P s else sfilter P s)" proof (cases "P x") diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Library/Sublist.thy --- a/src/HOL/Library/Sublist.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Library/Sublist.thy Sun Nov 26 21:08:32 2017 +0100 @@ -1018,7 +1018,7 @@ "subseq (xs @ zs) (ys @ zs) \ subseq xs ys" (is "?l = ?r") proof { fix xs' ys' xs ys zs :: "'a list" assume "subseq xs' ys'" - then have "xs' = xs @ zs & ys' = ys @ zs \ subseq xs ys" + then have "xs' = xs @ zs \ ys' = ys @ zs \ subseq xs ys" proof (induct arbitrary: xs ys zs) case list_emb_Nil show ?case by simp next diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Library/Sum_of_Squares/sum_of_squares.ML --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Sun Nov 26 21:08:32 2017 +0100 @@ -1018,8 +1018,8 @@ addsimps [@{thm power_divide}] val th = Thm.instantiate' [] [SOME d, SOME (Thm.dest_arg P)] - (if ord then @{lemma "(d=0 --> P) & (d>0 --> P) & (d<(0::real) --> P) ==> P" by auto} - else @{lemma "(d=0 --> P) & (d ~= (0::real) --> P) ==> P" by blast}) + (if ord then @{lemma "(d=0 \ P) \ (d>0 \ P) \ (d<(0::real) \ P) \ P" by auto} + else @{lemma "(d=0 \ P) \ (d \ (0::real) \ P) \ P" by blast}) in resolve_tac ctxt [th] i THEN Simplifier.asm_full_simp_tac simp_ctxt i end)); fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i); diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Library/While_Combinator.thy --- a/src/HOL/Library/While_Combinator.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Library/While_Combinator.thy Sun Nov 26 21:08:32 2017 +0100 @@ -12,8 +12,8 @@ subsection \Partial version\ definition while_option :: "('a \ bool) \ ('a \ 'a) \ 'a \ 'a option" where -"while_option b c s = (if (\k. ~ b ((c ^^ k) s)) - then Some ((c ^^ (LEAST k. ~ b ((c ^^ k) s))) s) +"while_option b c s = (if (\k. \ b ((c ^^ k) s)) + then Some ((c ^^ (LEAST k. \ b ((c ^^ k) s))) s) else None)" theorem while_option_unfold[code]: @@ -21,42 +21,42 @@ proof cases assume "b s" show ?thesis - proof (cases "\k. ~ b ((c ^^ k) s)") + proof (cases "\k. \ b ((c ^^ k) s)") case True - then obtain k where 1: "~ b ((c ^^ k) s)" .. + then obtain k where 1: "\ b ((c ^^ k) s)" .. with \b s\ obtain l where "k = Suc l" by (cases k) auto - with 1 have "~ b ((c ^^ l) (c s))" by (auto simp: funpow_swap1) - then have 2: "\l. ~ b ((c ^^ l) (c s))" .. + with 1 have "\ b ((c ^^ l) (c s))" by (auto simp: funpow_swap1) + then have 2: "\l. \ b ((c ^^ l) (c s))" .. from 1 - have "(LEAST k. ~ b ((c ^^ k) s)) = Suc (LEAST l. ~ b ((c ^^ Suc l) s))" + have "(LEAST k. \ b ((c ^^ k) s)) = Suc (LEAST l. \ b ((c ^^ Suc l) s))" by (rule Least_Suc) (simp add: \b s\) - also have "... = Suc (LEAST l. ~ b ((c ^^ l) (c s)))" + also have "... = Suc (LEAST l. \ b ((c ^^ l) (c s)))" by (simp add: funpow_swap1) finally show ?thesis using True 2 \b s\ by (simp add: funpow_swap1 while_option_def) next case False - then have "~ (\l. ~ b ((c ^^ Suc l) s))" by blast - then have "~ (\l. ~ b ((c ^^ l) (c s)))" + then have "\ (\l. \ b ((c ^^ Suc l) s))" by blast + then have "\ (\l. \ b ((c ^^ l) (c s)))" by (simp add: funpow_swap1) with False \b s\ show ?thesis by (simp add: while_option_def) qed next - assume [simp]: "~ b s" - have least: "(LEAST k. ~ b ((c ^^ k) s)) = 0" + assume [simp]: "\ b s" + have least: "(LEAST k. \ b ((c ^^ k) s)) = 0" by (rule Least_equality) auto moreover - have "\k. ~ b ((c ^^ k) s)" by (rule exI[of _ "0::nat"]) auto + have "\k. \ b ((c ^^ k) s)" by (rule exI[of _ "0::nat"]) auto ultimately show ?thesis unfolding while_option_def by auto qed lemma while_option_stop2: - "while_option b c s = Some t \ EX k. t = (c^^k) s \ \ b t" + "while_option b c s = Some t \ \k. t = (c^^k) s \ \ b t" apply(simp add: while_option_def split: if_splits) by (metis (lifting) LeastI_ex) -lemma while_option_stop: "while_option b c s = Some t \ ~ b t" +lemma while_option_stop: "while_option b c s = Some t \ \ b t" by(metis while_option_stop2) theorem while_option_rule: @@ -65,13 +65,13 @@ and init: "P s" shows "P t" proof - - define k where "k = (LEAST k. ~ b ((c ^^ k) s))" + define k where "k = (LEAST k. \ b ((c ^^ k) s))" from assms have t: "t = (c ^^ k) s" by (simp add: while_option_def k_def split: if_splits) have 1: "ALL i k" then have "P ((c ^^ i) s)" by (induct i) (auto simp: init step 1) } thus "P t" by (auto simp: t) qed @@ -243,8 +243,8 @@ theorem wf_while_option_Some: assumes "wf {(t, s). (P s \ b s) \ t = c s}" - and "!!s. P s \ b s \ P(c s)" and "P s" - shows "EX t. while_option b c s = Some t" + and "\s. P s \ b s \ P(c s)" and "P s" + shows "\t. while_option b c s = Some t" using assms(1,3) proof (induction s) case less thus ?case using assms(2) @@ -264,8 +264,8 @@ qed theorem measure_while_option_Some: fixes f :: "'s \ nat" -shows "(!!s. P s \ b s \ P(c s) \ f(c s) < f s) - \ P s \ EX t. while_option b c s = Some t" +shows "(\s. P s \ b s \ P(c s) \ f(c s) < f s) + \ P s \ \t. while_option b c s = Some t" by(blast intro: wf_while_option_Some[OF wf_if_measure, of P b f]) text\Kleene iteration starting from the empty set and assuming some finite diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Library/positivstellensatz.ML Sun Nov 26 21:08:32 2017 +0100 @@ -177,12 +177,12 @@ if exists (curry op aconv (Thm.concl_of tha)) (Thm.hyps_of thb) (* FIXME !? *) then Thm.equal_elim (Thm.symmetric (deduct_antisym_rule tha thb)) tha else thb; -val pth = @{lemma "(((x::real) < y) == (y - x > 0))" and "((x <= y) == (y - x >= 0))" and - "((x = y) == (x - y = 0))" and "((~(x < y)) == (x - y >= 0))" and - "((~(x <= y)) == (x - y > 0))" and "((~(x = y)) == (x - y > 0 | -(x - y) > 0))" +val pth = @{lemma "(((x::real) < y) \ (y - x > 0))" and "((x \ y) \ (y - x \ 0))" and + "((x = y) \ (x - y = 0))" and "((\(x < y)) \ (x - y \ 0))" and + "((\(x \ y)) \ (x - y > 0))" and "((\(x = y)) \ (x - y > 0 \ -(x - y) > 0))" by (atomize (full), auto simp add: less_diff_eq le_diff_eq not_less)}; -val pth_final = @{lemma "(~p ==> False) ==> p" by blast} +val pth_final = @{lemma "(\p \ False) \ p" by blast} val pth_add = @{lemma "(x = (0::real) ==> y = 0 ==> x + y = 0 )" and "( x = 0 ==> y >= 0 ==> x + y >= 0)" and "(x = 0 ==> y > 0 ==> x + y > 0)" and "(x >= 0 ==> y = 0 ==> x + y >= 0)" and @@ -204,8 +204,8 @@ val weak_dnf_simps = List.take (@{thms simp_thms}, 34) @ - @{lemma "((P & (Q | R)) = ((P&Q) | (P&R)))" and "((Q | R) & P) = ((Q&P) | (R&P))" and - "(P & Q) = (Q & P)" and "((P | Q) = (Q | P))" by blast+}; + @{lemma "((P \ (Q \ R)) = ((P\Q) \ (P\R)))" and "((Q \ R) \ P) = ((Q\P) \ (R\P))" and + "(P \ Q) = (Q \ P)" and "((P \ Q) = (Q \ P))" by blast+}; (* val nnfD_simps = @@ -214,65 +214,65 @@ "((~(P = Q)) = ((P & ~ Q) | (~P & Q)) )" and "((~ ~(P)) = P)" by blast+}; *) -val choice_iff = @{lemma "(ALL x. EX y. P x y) = (EX f. ALL x. P x (f x))" by metis}; +val choice_iff = @{lemma "(\x. \y. P x y) = (\f. \x. P x (f x))" by metis}; val prenex_simps = map (fn th => th RS sym) ([@{thm "all_conj_distrib"}, @{thm "ex_disj_distrib"}] @ @{thms "HOL.all_simps"(1-4)} @ @{thms "ex_simps"(1-4)}); val real_abs_thms1 = @{lemma - "((-1 * \x::real\ >= r) = (-1 * x >= r & 1 * x >= r))" and - "((-1 * \x\ + a >= r) = (a + -1 * x >= r & a + 1 * x >= r))" and - "((a + -1 * \x\ >= r) = (a + -1 * x >= r & a + 1 * x >= r))" and - "((a + -1 * \x\ + b >= r) = (a + -1 * x + b >= r & a + 1 * x + b >= r))" and - "((a + b + -1 * \x\ >= r) = (a + b + -1 * x >= r & a + b + 1 * x >= r))" and - "((a + b + -1 * \x\ + c >= r) = (a + b + -1 * x + c >= r & a + b + 1 * x + c >= r))" and - "((-1 * max x y >= r) = (-1 * x >= r & -1 * y >= r))" and - "((-1 * max x y + a >= r) = (a + -1 * x >= r & a + -1 * y >= r))" and - "((a + -1 * max x y >= r) = (a + -1 * x >= r & a + -1 * y >= r))" and - "((a + -1 * max x y + b >= r) = (a + -1 * x + b >= r & a + -1 * y + b >= r))" and - "((a + b + -1 * max x y >= r) = (a + b + -1 * x >= r & a + b + -1 * y >= r))" and - "((a + b + -1 * max x y + c >= r) = (a + b + -1 * x + c >= r & a + b + -1 * y + c >= r))" and - "((1 * min x y >= r) = (1 * x >= r & 1 * y >= r))" and - "((1 * min x y + a >= r) = (a + 1 * x >= r & a + 1 * y >= r))" and - "((a + 1 * min x y >= r) = (a + 1 * x >= r & a + 1 * y >= r))" and - "((a + 1 * min x y + b >= r) = (a + 1 * x + b >= r & a + 1 * y + b >= r))" and - "((a + b + 1 * min x y >= r) = (a + b + 1 * x >= r & a + b + 1 * y >= r))" and - "((a + b + 1 * min x y + c >= r) = (a + b + 1 * x + c >= r & a + b + 1 * y + c >= r))" and - "((min x y >= r) = (x >= r & y >= r))" and - "((min x y + a >= r) = (a + x >= r & a + y >= r))" and - "((a + min x y >= r) = (a + x >= r & a + y >= r))" and - "((a + min x y + b >= r) = (a + x + b >= r & a + y + b >= r))" and - "((a + b + min x y >= r) = (a + b + x >= r & a + b + y >= r))" and - "((a + b + min x y + c >= r) = (a + b + x + c >= r & a + b + y + c >= r))" and - "((-1 * \x\ > r) = (-1 * x > r & 1 * x > r))" and - "((-1 * \x\ + a > r) = (a + -1 * x > r & a + 1 * x > r))" and - "((a + -1 * \x\ > r) = (a + -1 * x > r & a + 1 * x > r))" and - "((a + -1 * \x\ + b > r) = (a + -1 * x + b > r & a + 1 * x + b > r))" and - "((a + b + -1 * \x\ > r) = (a + b + -1 * x > r & a + b + 1 * x > r))" and - "((a + b + -1 * \x\ + c > r) = (a + b + -1 * x + c > r & a + b + 1 * x + c > r))" and - "((-1 * max x y > r) = ((-1 * x > r) & -1 * y > r))" and - "((-1 * max x y + a > r) = (a + -1 * x > r & a + -1 * y > r))" and - "((a + -1 * max x y > r) = (a + -1 * x > r & a + -1 * y > r))" and - "((a + -1 * max x y + b > r) = (a + -1 * x + b > r & a + -1 * y + b > r))" and - "((a + b + -1 * max x y > r) = (a + b + -1 * x > r & a + b + -1 * y > r))" and - "((a + b + -1 * max x y + c > r) = (a + b + -1 * x + c > r & a + b + -1 * y + c > r))" and - "((min x y > r) = (x > r & y > r))" and - "((min x y + a > r) = (a + x > r & a + y > r))" and - "((a + min x y > r) = (a + x > r & a + y > r))" and - "((a + min x y + b > r) = (a + x + b > r & a + y + b > r))" and - "((a + b + min x y > r) = (a + b + x > r & a + b + y > r))" and - "((a + b + min x y + c > r) = (a + b + x + c > r & a + b + y + c > r))" + "((-1 * \x::real\ \ r) = (-1 * x \ r \ 1 * x \ r))" and + "((-1 * \x\ + a \ r) = (a + -1 * x \ r \ a + 1 * x \ r))" and + "((a + -1 * \x\ \ r) = (a + -1 * x \ r \ a + 1 * x \ r))" and + "((a + -1 * \x\ + b \ r) = (a + -1 * x + b \ r \ a + 1 * x + b \ r))" and + "((a + b + -1 * \x\ \ r) = (a + b + -1 * x \ r \ a + b + 1 * x \ r))" and + "((a + b + -1 * \x\ + c \ r) = (a + b + -1 * x + c \ r \ a + b + 1 * x + c \ r))" and + "((-1 * max x y \ r) = (-1 * x \ r \ -1 * y \ r))" and + "((-1 * max x y + a \ r) = (a + -1 * x \ r \ a + -1 * y \ r))" and + "((a + -1 * max x y \ r) = (a + -1 * x \ r \ a + -1 * y \ r))" and + "((a + -1 * max x y + b \ r) = (a + -1 * x + b \ r \ a + -1 * y + b \ r))" and + "((a + b + -1 * max x y \ r) = (a + b + -1 * x \ r \ a + b + -1 * y \ r))" and + "((a + b + -1 * max x y + c \ r) = (a + b + -1 * x + c \ r \ a + b + -1 * y + c \ r))" and + "((1 * min x y \ r) = (1 * x \ r \ 1 * y \ r))" and + "((1 * min x y + a \ r) = (a + 1 * x \ r \ a + 1 * y \ r))" and + "((a + 1 * min x y \ r) = (a + 1 * x \ r \ a + 1 * y \ r))" and + "((a + 1 * min x y + b \ r) = (a + 1 * x + b \ r \ a + 1 * y + b \ r))" and + "((a + b + 1 * min x y \ r) = (a + b + 1 * x \ r \ a + b + 1 * y \ r))" and + "((a + b + 1 * min x y + c \ r) = (a + b + 1 * x + c \ r \ a + b + 1 * y + c \ r))" and + "((min x y \ r) = (x \ r \ y \ r))" and + "((min x y + a \ r) = (a + x \ r \ a + y \ r))" and + "((a + min x y \ r) = (a + x \ r \ a + y \ r))" and + "((a + min x y + b \ r) = (a + x + b \ r \ a + y + b \ r))" and + "((a + b + min x y \ r) = (a + b + x \ r \ a + b + y \ r))" and + "((a + b + min x y + c \ r) = (a + b + x + c \ r \ a + b + y + c \ r))" and + "((-1 * \x\ > r) = (-1 * x > r \ 1 * x > r))" and + "((-1 * \x\ + a > r) = (a + -1 * x > r \ a + 1 * x > r))" and + "((a + -1 * \x\ > r) = (a + -1 * x > r \ a + 1 * x > r))" and + "((a + -1 * \x\ + b > r) = (a + -1 * x + b > r \ a + 1 * x + b > r))" and + "((a + b + -1 * \x\ > r) = (a + b + -1 * x > r \ a + b + 1 * x > r))" and + "((a + b + -1 * \x\ + c > r) = (a + b + -1 * x + c > r \ a + b + 1 * x + c > r))" and + "((-1 * max x y > r) = ((-1 * x > r) \ -1 * y > r))" and + "((-1 * max x y + a > r) = (a + -1 * x > r \ a + -1 * y > r))" and + "((a + -1 * max x y > r) = (a + -1 * x > r \ a + -1 * y > r))" and + "((a + -1 * max x y + b > r) = (a + -1 * x + b > r \ a + -1 * y + b > r))" and + "((a + b + -1 * max x y > r) = (a + b + -1 * x > r \ a + b + -1 * y > r))" and + "((a + b + -1 * max x y + c > r) = (a + b + -1 * x + c > r \ a + b + -1 * y + c > r))" and + "((min x y > r) = (x > r \ y > r))" and + "((min x y + a > r) = (a + x > r \ a + y > r))" and + "((a + min x y > r) = (a + x > r \ a + y > r))" and + "((a + min x y + b > r) = (a + x + b > r \ a + y + b > r))" and + "((a + b + min x y > r) = (a + b + x > r \ a + b + y > r))" and + "((a + b + min x y + c > r) = (a + b + x + c > r \ a + b + y + c > r))" by auto}; -val abs_split' = @{lemma "P \x::'a::linordered_idom\ == (x >= 0 & P x | x < 0 & P (-x))" +val abs_split' = @{lemma "P \x::'a::linordered_idom\ == (x \ 0 \ P x \ x < 0 \ P (-x))" by (atomize (full)) (auto split: abs_split)}; -val max_split = @{lemma "P (max x y) == ((x::'a::linorder) <= y & P y | x > y & P x)" - by (atomize (full)) (cases "x <= y", auto simp add: max_def)}; +val max_split = @{lemma "P (max x y) \ ((x::'a::linorder) \ y \ P y \ x > y \ P x)" + by (atomize (full)) (cases "x \ y", auto simp add: max_def)}; -val min_split = @{lemma "P (min x y) == ((x::'a::linorder) <= y & P x | x > y & P y)" - by (atomize (full)) (cases "x <= y", auto simp add: min_def)}; +val min_split = @{lemma "P (min x y) \ ((x::'a::linorder) \ y \ P x \ x > y \ P y)" + by (atomize (full)) (cases "x \ y", auto simp add: min_def)}; (* Miscellaneous *) diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Limited_Sequence.thy --- a/src/HOL/Limited_Sequence.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Limited_Sequence.thy Sun Nov 26 21:08:32 2017 +0100 @@ -171,8 +171,8 @@ definition neg_not_seq :: "unit pos_dseq \ unit neg_dseq" where "neg_not_seq x = (\i. case Lazy_Sequence.yield (x i) of - None => Lazy_Sequence.hb_single () - | Some ((), xq) => Lazy_Sequence.empty)" + None \ Lazy_Sequence.hb_single () + | Some ((), xq) \ Lazy_Sequence.empty)" ML \ diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Limits.thy --- a/src/HOL/Limits.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Limits.thy Sun Nov 26 21:08:32 2017 +0100 @@ -2365,7 +2365,7 @@ lemma uniformly_continuous_imp_Cauchy_continuous: fixes f :: "'a::metric_space \ 'b::metric_space" - shows "\uniformly_continuous_on S f; Cauchy \; \n. (\ n) \ S\ \ Cauchy(f o \)" + shows "\uniformly_continuous_on S f; Cauchy \; \n. (\ n) \ S\ \ Cauchy(f \ \)" by (simp add: uniformly_continuous_on_def Cauchy_def) meson lemma (in bounded_linear) isUCont: "isUCont f" diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/List.thy --- a/src/HOL/List.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/List.thy Sun Nov 26 21:08:32 2017 +0100 @@ -147,7 +147,7 @@ primrec zip :: "'a list \ 'b list \ ('a \ 'b) list" where "zip xs [] = []" | zip_Cons: "zip xs (y # ys) = - (case xs of [] => [] | z # zs => (z, y) # zip zs ys)" + (case xs of [] \ [] | z # zs \ (z, y) # zip zs ys)" \ \Warning: simpset does not contain this definition, but separate theorems for \xs = []\ and \xs = z # zs\\ @@ -182,7 +182,7 @@ "find P (x#xs) = (if P x then Some x else find P xs)" text \In the context of multisets, \count_list\ is equivalent to - @{term "count o mset"} and it it advisable to use the latter.\ + @{term "count \ mset"} and it it advisable to use the latter.\ primrec count_list :: "'a list \ 'a \ nat" where "count_list [] y = 0" | "count_list (x#xs) y = (if x=y then count_list xs y + 1 else count_list xs y)" @@ -190,9 +190,9 @@ definition "extract" :: "('a \ bool) \ 'a list \ ('a list * 'a * 'a list) option" where "extract P xs = - (case dropWhile (Not o P) xs of + (case dropWhile (Not \ P) xs of [] \ None | - y#ys \ Some(takeWhile (Not o P) xs, y, ys))" + y#ys \ Some(takeWhile (Not \ P) xs, y, ys))" hide_const (open) "extract" @@ -783,10 +783,10 @@ lemma neq_Nil_conv: "(xs \ []) = (\y ys. xs = y # ys)" by (induct xs) auto -lemma tl_Nil: "tl xs = [] \ xs = [] \ (EX x. xs = [x])" +lemma tl_Nil: "tl xs = [] \ xs = [] \ (\x. xs = [x])" by (cases xs) auto -lemma Nil_tl: "[] = tl xs \ xs = [] \ (EX x. xs = [x])" +lemma Nil_tl: "[] = tl xs \ xs = [] \ (\x. xs = [x])" by (cases xs) auto lemma length_induct: @@ -987,7 +987,7 @@ done lemma append_eq_append_conv2: "(xs @ ys = zs @ ts) = - (EX us. xs = zs @ us & us @ ys = ts | xs @ us = zs & ys = us@ ts)" + (\us. xs = zs @ us \ us @ ys = ts \ xs @ us = zs \ ys = us @ ts)" apply (induct xs arbitrary: ys zs ts) apply fastforce apply(case_tac zs) @@ -1019,7 +1019,7 @@ lemma hd_append2 [simp]: "xs \ [] ==> hd (xs @ ys) = hd xs" by (simp add: hd_append split: list.split) -lemma tl_append: "tl (xs @ ys) = (case xs of [] => tl ys | z#zs => zs @ ys)" +lemma tl_append: "tl (xs @ ys) = (case xs of [] \ tl ys | z#zs \ zs @ ys)" by (simp split: list.split) lemma tl_append2 [simp]: "xs \ [] ==> tl (xs @ ys) = tl xs @ ys" @@ -1027,11 +1027,11 @@ lemma Cons_eq_append_conv: "x#xs = ys@zs = - (ys = [] & x#xs = zs | (EX ys'. x#ys' = ys & xs = ys'@zs))" + (ys = [] \ x#xs = zs \ (\ys'. x#ys' = ys \ xs = ys'@zs))" by(cases ys) auto lemma append_eq_Cons_conv: "(ys@zs = x#xs) = - (ys = [] & zs = x#xs | (EX ys'. ys = x#ys' & ys'@zs = xs))" + (ys = [] \ zs = x#xs \ (\ys'. ys = x#ys' \ ys'@zs = xs))" by(cases ys) auto lemma longest_common_prefix: @@ -1112,7 +1112,7 @@ lemma map_tl: "map f (tl xs) = tl (map f xs)" by (cases xs) simp_all -lemma map_ext: "(!!x. x : set xs --> f x = g x) ==> map f xs = map g xs" +lemma map_ext: "(\x. x \ set xs \ f x = g x) ==> map f xs = map g xs" by (induct xs) simp_all lemma map_ident [simp]: "map (\x. x) = (\xs. xs)" @@ -1124,7 +1124,7 @@ lemma map_map [simp]: "map f (map g xs) = map (f \ g) xs" by (induct xs) auto -lemma map_comp_map[simp]: "((map f) o (map g)) = map(f o g)" +lemma map_comp_map[simp]: "((map f) \ (map g)) = map(f \ g)" by (rule ext) simp lemma rev_map: "rev (map f xs) = map f (rev xs)" @@ -1156,7 +1156,7 @@ declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!] lemma ex_map_conv: - "(EX xs. ys = map f xs) = (ALL y : set ys. EX x. y = f x)" + "(\xs. ys = map f xs) = (\y \ set ys. \x. y = f x)" by(induct ys, auto simp add: Cons_eq_map_conv) lemma map_eq_imp_length_eq: @@ -1380,7 +1380,7 @@ "(x : set xs) = (\ys zs. xs = ys @ x # zs \ x \ set zs)" by (auto dest!: split_list_last) -lemma split_list_prop: "\x \ set xs. P x \ \ys x zs. xs = ys @ x # zs & P x" +lemma split_list_prop: "\x \ set xs. P x \ \ys x zs. xs = ys @ x # zs \ P x" proof (induct xs) case Nil thus ?case by simp next @@ -1450,7 +1450,7 @@ by rule (erule split_list_last_prop, auto) -lemma finite_list: "finite A ==> EX xs. set xs = A" +lemma finite_list: "finite A \ \xs. set xs = A" by (erule finite_induct) (auto simp add: list.set(2)[symmetric] simp del: list.set(2)) lemma card_length: "card (set xs) \ length xs" @@ -1481,7 +1481,7 @@ by (induct xs) (auto simp add: le_SucI) lemma sum_length_filter_compl: - "length(filter P xs) + length(filter (%x. ~P x) xs) = length xs" + "length(filter P xs) + length(filter (\x. \P x) xs) = length xs" by(induct xs) simp_all lemma filter_True [simp]: "\x \ set xs. P x ==> filter P xs = xs" @@ -1500,18 +1500,18 @@ apply simp done -lemma filter_map: "filter P (map f xs) = map f (filter (P o f) xs)" +lemma filter_map: "filter P (map f xs) = map f (filter (P \ f) xs)" by (induct xs) simp_all lemma length_filter_map[simp]: - "length (filter P (map f xs)) = length(filter (P o f) xs)" + "length (filter P (map f xs)) = length(filter (P \ f) xs)" by (simp add:filter_map) lemma filter_is_subset [simp]: "set (filter P xs) \ set xs" by auto lemma length_filter_less: - "\ x : set xs; ~ P x \ \ length(filter P xs) < length xs" + "\ x \ set xs; \ P x \ \ length(filter P xs) < length xs" proof (induct xs) case Nil thus ?case by simp next @@ -1522,12 +1522,12 @@ qed lemma length_filter_conv_card: - "length(filter p xs) = card{i. i < length xs & p(xs!i)}" + "length(filter p xs) = card{i. i < length xs \ p(xs!i)}" proof (induct xs) case Nil thus ?case by simp next case (Cons x xs) - let ?S = "{i. i < length xs & p(xs!i)}" + let ?S = "{i. i < length xs \ p(xs!i)}" have fin: "finite ?S" by(fast intro: bounded_nat_set_is_finite) show ?case (is "?l = card ?S'") proof (cases) @@ -1621,7 +1621,7 @@ lemma partition_filter1: "fst (partition P xs) = filter P xs" by (induct xs) (auto simp add: Let_def split_def) -lemma partition_filter2: "snd (partition P xs) = filter (Not o P) xs" +lemma partition_filter2: "snd (partition P xs) = filter (Not \ P) xs" by (induct xs) (auto simp add: Let_def split_def) lemma partition_P: @@ -1643,7 +1643,7 @@ qed lemma partition_filter_conv[simp]: - "partition f xs = (filter f xs,filter (Not o f) xs)" + "partition f xs = (filter f xs,filter (Not \ f) xs)" unfolding partition_filter2[symmetric] unfolding partition_filter1[symmetric] by simp @@ -1784,7 +1784,7 @@ by (auto simp add: set_conv_nth) lemma all_set_conv_all_nth: - "(\x \ set xs. P x) = (\i. i < length xs --> P (xs ! i))" + "(\x \ set xs. P x) = (\i. i < length xs \ P (xs ! i))" by (auto simp add: set_conv_nth) lemma rev_nth: @@ -1808,18 +1808,18 @@ qed lemma Skolem_list_nth: - "(ALL iix. P i x) = (\xs. size xs = k \ (\ixs. ?P k xs)") proof(induct k) case 0 show ?case by simp next case (Suc k) - show ?case (is "?L = ?R" is "_ = (EX xs. ?P' xs)") + show ?case (is "?L = ?R" is "_ = (\xs. ?P' xs)") proof assume "?R" thus "?L" using Suc by auto next assume "?L" - with Suc obtain x xs where "?P k xs & P k x" by (metis less_Suc_eq) + with Suc obtain x xs where "?P k xs \ P k x" by (metis less_Suc_eq) hence "?P'(xs@[x])" by(simp add:nth_append less_Suc_eq) thus "?R" .. qed @@ -1967,7 +1967,7 @@ by (induct xs) (auto split: if_split_asm) lemma in_set_butlast_appendI: - "x : set (butlast xs) | x : set (butlast ys) ==> x : set (butlast (xs @ ys))" + "x \ set (butlast xs) \ x \ set (butlast ys) \ x \ set (butlast (xs @ ys))" by (auto dest: in_set_butlastD simp add: butlast_append) lemma last_drop[simp]: "n < length xs \ last (drop n xs) = last xs" @@ -2004,7 +2004,7 @@ by (induct xs) simp_all lemma snoc_eq_iff_butlast: - "xs @ [x] = ys \ (ys \ [] & butlast ys = xs & last ys = x)" + "xs @ [x] = ys \ (ys \ [] \ butlast ys = xs \ last ys = x)" by fastforce corollary longest_common_suffix: @@ -2036,7 +2036,7 @@ declare take_Cons [simp del] and drop_Cons [simp del] -lemma take_Suc: "xs ~= [] ==> take (Suc n) xs = hd xs # take n (tl xs)" +lemma take_Suc: "xs \ [] \ take (Suc n) xs = hd xs # take n (tl xs)" by(clarsimp simp add:neq_Nil_conv) lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)" @@ -2285,7 +2285,7 @@ by (induct xs) auto lemma takeWhile_append1 [simp]: - "[| x:set xs; ~P(x)|] ==> takeWhile P (xs @ ys) = takeWhile P xs" + "\x \ set xs; \P(x)\ \ takeWhile P (xs @ ys) = takeWhile P xs" by (induct xs) auto lemma takeWhile_append2 [simp]: @@ -2306,7 +2306,7 @@ by (induct xs) auto lemma dropWhile_append1 [simp]: - "[| x : set xs; ~P(x)|] ==> dropWhile P (xs @ ys) = (dropWhile P xs)@ys" + "\x \ set xs; \P(x)\ \ dropWhile P (xs @ ys) = (dropWhile P xs)@ys" by (induct xs) auto lemma dropWhile_append2 [simp]: @@ -2336,7 +2336,7 @@ by(induct xs, auto) lemma dropWhile_eq_Cons_conv: - "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys & \ P y)" + "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys \ \ P y)" by(induct xs, auto) lemma distinct_takeWhile[simp]: "distinct xs ==> distinct (takeWhile P xs)" @@ -2693,7 +2693,7 @@ lemma list_all2_append1: "list_all2 P (xs @ ys) zs = - (EX us vs. zs = us @ vs \ length us = length xs \ length vs = length ys \ + (\us vs. zs = us @ vs \ length us = length xs \ length vs = length ys \ list_all2 P xs us \ list_all2 P ys vs)" apply (simp add: list_all2_iff zip_append1) apply (rule iffI) @@ -2705,7 +2705,7 @@ lemma list_all2_append2: "list_all2 P xs (ys @ zs) = - (EX us vs. xs = us @ vs \ length us = length ys \ length vs = length zs \ + (\us vs. xs = us @ vs \ length us = length ys \ length vs = length zs \ list_all2 P us ys \ list_all2 P vs zs)" apply (simp add: list_all2_iff zip_append2) apply (rule iffI) @@ -2904,7 +2904,7 @@ lemma fold_append [simp]: "fold f (xs @ ys) = fold f ys \ fold f xs" by (induct xs) simp_all -lemma fold_map [code_unfold]: "fold g (map f xs) = fold (g o f) xs" +lemma fold_map [code_unfold]: "fold g (map f xs) = fold (g \ f) xs" by (induct xs) simp_all lemma fold_filter: @@ -3044,7 +3044,7 @@ lemma foldl_append [simp]: "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys" by (simp add: foldl_conv_fold) -lemma foldr_map [code_unfold]: "foldr g (map f xs) a = foldr (g o f) xs a" +lemma foldr_map [code_unfold]: "foldr g (map f xs) a = foldr (g \ f) xs a" by (simp add: foldr_conv_fold fold_map rev_map) lemma foldr_filter: @@ -3075,7 +3075,7 @@ by(induct j)simp_all lemma upt_eq_Cons_conv: - "([i.. i = x \ [i+1.. k <= length ys ==> - (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys" + "k \ length xs \ k \ length ys \ + (\i. i < k \ xs!i = ys!i) \ take k xs = take k ys" apply (atomize, induct k arbitrary: xs ys) apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib, clarify) txt \Both lists must be non-empty\ @@ -3294,7 +3294,7 @@ lemma remdups_id_iff_distinct [simp]: "remdups xs = xs \ distinct xs" by (metis distinct_remdups distinct_remdups_id) -lemma finite_distinct_list: "finite A \ EX xs. set xs = A & distinct xs" +lemma finite_distinct_list: "finite A \ \xs. set xs = A \ distinct xs" by (metis distinct_remdups finite_list set_remdups) lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])" @@ -3319,7 +3319,7 @@ by (induct xs) auto lemma distinct_map: - "distinct(map f xs) = (distinct xs & inj_on f (set xs))" + "distinct(map f xs) = (distinct xs \ inj_on f (set xs))" by (induct xs) auto lemma distinct_map_filter: @@ -3379,7 +3379,7 @@ sometimes it is useful.\ lemma distinct_conv_nth: -"distinct xs = (\i < size xs. \j < size xs. i \ j --> xs!i \ xs!j)" +"distinct xs = (\i < size xs. \j < size xs. i \ j \ xs!i \ xs!j)" apply (induct xs, simp, simp) apply (rule iffI, clarsimp) apply (case_tac i) @@ -3451,7 +3451,7 @@ lemma distinct_length_filter: "distinct xs \ length (filter P xs) = card ({x. P x} Int set xs)" by (induct xs) (auto) -lemma not_distinct_decomp: "~ distinct ws ==> EX xs ys zs y. ws = xs@[y]@ys@[y]@zs" +lemma not_distinct_decomp: "\ distinct ws \ \xs ys zs y. ws = xs@[y]@ys@[y]@zs" apply (induct n == "length ws" arbitrary:ws) apply simp apply(case_tac ws) apply simp apply (simp split:if_split_asm) @@ -3563,7 +3563,7 @@ by force lemma remdups_adj_altdef: "(remdups_adj xs = ys) \ - (\f::nat => nat. mono f & f ` {0 ..< size xs} = {0 ..< size ys} + (\f::nat => nat. mono f \ f ` {0 ..< size xs} = {0 ..< size ys} \ (\i < size xs. xs!i = ys!(f i)) \ (\i. i + 1 < size xs \ (xs!i = xs!(i+1) \ f i = f(i+1))))" (is "?L \ (\f. ?p f xs ys)") proof @@ -3645,7 +3645,7 @@ proof cases assume "x1 = x2" - let ?f' = "f o Suc" + let ?f' = "f \ Suc" have "remdups_adj (x1 # xs) = ys" proof (intro "3.hyps" exI conjI impI allI) @@ -4114,15 +4114,15 @@ lemma set_replicate_conv_if: "set (replicate n x) = (if n = 0 then {} else {x})" by auto -lemma in_set_replicate[simp]: "(x : set (replicate n y)) = (x = y & n \ 0)" +lemma in_set_replicate[simp]: "(x \ set (replicate n y)) = (x = y \ n \ 0)" by (simp add: set_replicate_conv_if) lemma Ball_set_replicate[simp]: - "(ALL x : set(replicate n a). P x) = (P a | n=0)" + "(\x \ set(replicate n a). P x) = (P a \ n=0)" by(simp add: set_replicate_conv_if) lemma Bex_set_replicate[simp]: - "(EX x : set(replicate n a). P x) = (P a & n\0)" + "(\x \ set(replicate n a). P x) = (P a \ n\0)" by(simp add: set_replicate_conv_if) lemma replicate_append_same: @@ -4144,7 +4144,7 @@ by (induct n) auto lemma replicate_eq_replicate[simp]: - "(replicate m x = replicate n y) \ (m=n & (m\0 \ x=y))" + "(replicate m x = replicate n y) \ (m=n \ (m\0 \ x=y))" apply(induct m arbitrary: n) apply simp apply(induct_tac n) @@ -4306,7 +4306,7 @@ by(simp add:rotate_def) lemma rotate_add: - "rotate (m+n) = rotate m o rotate n" + "rotate (m+n) = rotate m \ rotate n" by(simp add:rotate_def funpow_add) lemma rotate_rotate: "rotate m (rotate n xs) = rotate (m+n) xs" @@ -4469,7 +4469,7 @@ case Nil thus ?case by simp next case (Cons a xs) - then have "!x. x: set xs \ x \ a" by auto + then have "\x. x \ set xs \ x \ a" by auto with Cons show ?case by(simp add: nths_Cons cong:filter_cong) qed @@ -4809,7 +4809,7 @@ subsubsection \(In)finiteness\ lemma finite_maxlen: - "finite (M::'a list set) ==> EX n. ALL s:M. size s < n" + "finite (M::'a list set) \ \n. \s\M. size s < n" proof (induct rule: finite.induct) case emptyI show ?case by simp next @@ -4891,7 +4891,7 @@ from this show ?thesis by (rule card_lists_distinct_length_eq) qed -lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)" +lemma infinite_UNIV_listI: "\ finite(UNIV::'a list set)" apply (rule notI) apply (drule finite_maxlen) apply clarsimp @@ -4977,7 +4977,7 @@ by (cases xs) (simp_all add: sorted_Cons) lemma sorted_append: - "sorted (xs@ys) = (sorted xs & sorted ys & (\x \ set xs. \y \ set ys. x\y))" + "sorted (xs@ys) = (sorted xs \ sorted ys \ (\x \ set xs. \y \ set ys. x\y))" by (induct xs) (auto simp add:sorted_Cons) lemma sorted_nth_mono: @@ -5878,8 +5878,8 @@ by (unfold lenlex_def) blast lemma lenlex_conv: - "lenlex r = {(xs,ys). length xs < length ys | - length xs = length ys \ (xs, ys) : lex r}" + "lenlex r = {(xs,ys). length xs < length ys \ + length xs = length ys \ (xs, ys) \ lex r}" by (simp add: lenlex_def Id_on_def lex_prod_def inv_image_def) lemma Nil_notin_lex [iff]: "([], ys) \ lex r" @@ -5889,8 +5889,8 @@ by (simp add:lex_conv) lemma Cons_in_lex [simp]: - "((x # xs, y # ys) : lex r) = - ((x, y) : r \ length xs = length ys | x = y \ (xs, ys) : lex r)" + "((x # xs, y # ys) \ lex r) = + ((x, y) \ r \ length xs = length ys \ x = y \ (xs, ys) \ lex r)" apply (simp add: lex_conv) apply (rule iffI) prefer 2 apply (blast intro: Cons_eq_appendI, clarify) @@ -5944,7 +5944,7 @@ by (unfold lexord_def, induct_tac x, auto) lemma lexord_cons_cons[simp]: - "((a # x, b # y) \ lexord r) = ((a,b)\ r | (a = b & (x,y)\ lexord r))" + "((a # x, b # y) \ lexord r) = ((a,b)\ r \ (a = b \ (x,y)\ lexord r))" apply (unfold lexord_def, safe, simp_all) apply (case_tac u, simp, simp) apply (case_tac u, simp, clarsimp, blast, blast, clarsimp) @@ -5964,13 +5964,13 @@ by (induct x, auto) lemma lexord_append_leftD: - "\ (x @ u, x @ v) \ lexord r; (! a. (a,a) \ r) \ \ (u,v) \ lexord r" + "\ (x @ u, x @ v) \ lexord r; (\a. (a,a) \ r) \ \ (u,v) \ lexord r" by (erule rev_mp, induct_tac x, auto) lemma lexord_take_index_conv: - "((x,y) : lexord r) = + "((x,y) \ lexord r) = ((length x < length y \ take (length x) y = x) \ - (\i. i < min(length x)(length y) & take i x = take i y & (x!i,y!i) \ r))" + (\i. i < min(length x)(length y) \ take i x = take i y \ (x!i,y!i) \ r))" apply (unfold lexord_def Let_def, clarsimp) apply (rule_tac f = "(% a b. a \ b)" in arg_cong2) apply auto @@ -5992,7 +5992,7 @@ apply (induct_tac x, clarsimp) by (clarify, case_tac x, simp, force) -lemma lexord_irreflexive: "ALL x. (x,x) \ r \ (xs,xs) \ lexord r" +lemma lexord_irreflexive: "\x. (x,x) \ r \ (xs,xs) \ lexord r" by (induct xs) auto text\By Ren\'e Thiemann:\ @@ -6033,7 +6033,7 @@ lemma lexord_transI: "trans r \ trans (lexord r)" by (rule transI, drule lexord_trans, blast) -lemma lexord_linear: "(! a b. (a,b)\ r | a = b | (b,a) \ r) \ (x,y) : lexord r | x = y | (y,x) : lexord r" +lemma lexord_linear: "(\a b. (a,b)\ r \ a = b \ (b,a) \ r) \ (x,y) \ lexord r \ x = y \ (y,x) \ lexord r" apply (rule_tac x = y in spec) apply (induct_tac x, rule allI) apply (case_tac x, simp, simp) @@ -6427,8 +6427,8 @@ lemma listrel_eq_len: "(xs, ys) \ listrel r \ length xs = length ys" by(induct rule: listrel.induct) auto -lemma listrel_iff_zip [code_unfold]: "(xs,ys) : listrel r \ - length xs = length ys & (\(x,y) \ set(zip xs ys). (x,y) \ r)" (is "?L \ ?R") +lemma listrel_iff_zip [code_unfold]: "(xs,ys) \ listrel r \ + length xs = length ys \ (\(x,y) \ set(zip xs ys). (x,y) \ r)" (is "?L \ ?R") proof assume ?L thus ?R by induct (auto intro: listrel_eq_len) next @@ -6437,8 +6437,8 @@ by (induct rule: list_induct2) (auto intro: listrel.intros) qed -lemma listrel_iff_nth: "(xs,ys) : listrel r \ - length xs = length ys & (\n < length xs. (xs!n, ys!n) \ r)" (is "?L \ ?R") +lemma listrel_iff_nth: "(xs,ys) \ listrel r \ + length xs = length ys \ (\n < length xs. (xs!n, ys!n) \ r)" (is "?L \ ?R") by (auto simp add: all_set_conv_all_nth listrel_iff_zip) @@ -6579,7 +6579,7 @@ "x \ set xs \ y \ f x \ y \ size_list f xs" by (induct xs) auto -lemma size_list_map[simp]: "size_list f (map g xs) = size_list (f o g) xs" +lemma size_list_map[simp]: "size_list f (map g xs) = size_list (f \ g) xs" by (induct xs) auto lemma size_list_append[simp]: "size_list f (xs @ ys) = size_list f xs + size_list f ys" @@ -6757,7 +6757,7 @@ lemma [code]: "lexordp r xs [] = False" "lexordp r [] (y#ys) = True" - "lexordp r (x # xs) (y # ys) = (r x y | (x = y & lexordp r xs ys))" + "lexordp r (x # xs) (y # ys) = (r x y \ (x = y \ lexordp r xs ys))" unfolding lexordp_def by auto text \Bounded quantification and summation over nats.\ diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/MacLaurin.thy --- a/src/HOL/MacLaurin.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/MacLaurin.thy Sun Nov 26 21:08:32 2017 +0100 @@ -209,7 +209,7 @@ fixes n :: nat and h :: real shows "h < 0 \ n > 0 \ diff 0 = f \ - (\m t. m < n & h \ t & t \ 0 --> DERIV (diff m) t :> diff (Suc m) t) \ + (\m t. m < n \ h \ t \ t \ 0 \ DERIV (diff m) t :> diff (Suc m) t) \ (\t. h < t \ t < 0 \ f h = (\mVersion for Sine Function\ -lemma mod_exhaust_less_4: "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = 3" +lemma mod_exhaust_less_4: "m mod 4 = 0 \ m mod 4 = 1 \ m mod 4 = 2 \ m mod 4 = 3" for m :: nat by auto diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Map.thy --- a/src/HOL/Map.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Map.thy Sun Nov 26 21:08:32 2017 +0100 @@ -258,11 +258,11 @@ subsection \@{const map_option} related\ -lemma map_option_o_empty [simp]: "map_option f o empty = empty" +lemma map_option_o_empty [simp]: "map_option f \ empty = empty" by (rule ext) simp lemma map_option_o_map_upd [simp]: - "map_option f o m(a\b) = (map_option f o m)(a\f b)" + "map_option f \ m(a\b) = (map_option f \ m)(a\f b)" by (rule ext) simp @@ -299,7 +299,7 @@ by (rule ext) (simp add: map_add_def split: option.split) lemma map_add_Some_iff: - "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)" + "((m ++ n) k = Some x) = (n k = Some x \ n k = None \ m k = Some x)" by (simp add: map_add_def split: option.split) lemma map_add_SomeD [dest!]: @@ -309,7 +309,7 @@ lemma map_add_find_right [simp]: "n k = Some xx \ (m ++ n) k = Some xx" by (subst map_add_Some_iff) fast -lemma map_add_None [iff]: "((m ++ n) k = None) = (n k = None & m k = None)" +lemma map_add_None [iff]: "((m ++ n) k = None) = (n k = None \ m k = None)" by (simp add: map_add_def split: option.split) lemma map_add_upd[simp]: "f ++ g(x\y) = (f ++ g)(x\y)" diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Meson.thy --- a/src/HOL/Meson.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Meson.thy Sun Nov 26 21:08:32 2017 +0100 @@ -15,21 +15,21 @@ text \de Morgan laws\ -lemma not_conjD: "~(P&Q) ==> ~P | ~Q" - and not_disjD: "~(P|Q) ==> ~P & ~Q" - and not_notD: "~~P ==> P" - and not_allD: "!!P. ~(\x. P(x)) ==> \x. ~P(x)" - and not_exD: "!!P. ~(\x. P(x)) ==> \x. ~P(x)" +lemma not_conjD: "\(P\Q) \ \P \ \Q" + and not_disjD: "\(P\Q) \ \P \ \Q" + and not_notD: "\\P \ P" + and not_allD: "\P. \(\x. P(x)) \ \x. \P(x)" + and not_exD: "\P. \(\x. P(x)) \ \x. \P(x)" by fast+ text \Removal of \\\ and \\\ (positive and negative occurrences)\ -lemma imp_to_disjD: "P-->Q ==> ~P | Q" - and not_impD: "~(P-->Q) ==> P & ~Q" - and iff_to_disjD: "P=Q ==> (~P | Q) & (~Q | P)" - and not_iffD: "~(P=Q) ==> (P | Q) & (~P | ~Q)" - \ \Much more efficient than @{prop "(P & ~Q) | (Q & ~P)"} for computing CNF\ - and not_refl_disj_D: "x ~= x | P ==> P" +lemma imp_to_disjD: "P\Q \ \P \ Q" + and not_impD: "\(P\Q) \ P \ \Q" + and iff_to_disjD: "P=Q \ (\P \ Q) \ (\Q \ P)" + and not_iffD: "\(P=Q) \ (P \ Q) \ (\P \ \Q)" + \ \Much more efficient than @{prop "(P \ \Q) \ (Q \ \P)"} for computing CNF\ + and not_refl_disj_D: "x \ x \ P \ P" by fast+ @@ -37,24 +37,24 @@ text \Conjunction\ -lemma conj_exD1: "!!P Q. (\x. P(x)) & Q ==> \x. P(x) & Q" - and conj_exD2: "!!P Q. P & (\x. Q(x)) ==> \x. P & Q(x)" +lemma conj_exD1: "\P Q. (\x. P(x)) \ Q \ \x. P(x) \ Q" + and conj_exD2: "\P Q. P \ (\x. Q(x)) \ \x. P \ Q(x)" by fast+ text \Disjunction\ -lemma disj_exD: "!!P Q. (\x. P(x)) | (\x. Q(x)) ==> \x. P(x) | Q(x)" +lemma disj_exD: "\P Q. (\x. P(x)) \ (\x. Q(x)) \ \x. P(x) \ Q(x)" \ \DO NOT USE with forall-Skolemization: makes fewer schematic variables!!\ \ \With ex-Skolemization, makes fewer Skolem constants\ - and disj_exD1: "!!P Q. (\x. P(x)) | Q ==> \x. P(x) | Q" - and disj_exD2: "!!P Q. P | (\x. Q(x)) ==> \x. P | Q(x)" + and disj_exD1: "\P Q. (\x. P(x)) \ Q \ \x. P(x) \ Q" + and disj_exD2: "\P Q. P \ (\x. Q(x)) \ \x. P \ Q(x)" by fast+ -lemma disj_assoc: "(P|Q)|R ==> P|(Q|R)" - and disj_comm: "P|Q ==> Q|P" - and disj_FalseD1: "False|P ==> P" - and disj_FalseD2: "P|False ==> P" +lemma disj_assoc: "(P\Q)\R \ P\(Q\R)" + and disj_comm: "P\Q \ Q\P" + and disj_FalseD1: "False\P \ P" + and disj_FalseD2: "P\False \ P" by fast+ @@ -63,15 +63,15 @@ text\Inserts negated disjunct after removing the negation; P is a literal. Model elimination requires assuming the negation of every attempted subgoal, hence the negated disjuncts.\ -lemma make_neg_rule: "~P|Q ==> ((~P==>P) ==> Q)" +lemma make_neg_rule: "\P\Q \ ((\P\P) \ Q)" by blast text\Version for Plaisted's "Postive refinement" of the Meson procedure\ -lemma make_refined_neg_rule: "~P|Q ==> (P ==> Q)" +lemma make_refined_neg_rule: "\P\Q \ (P \ Q)" by blast text\@{term P} should be a literal\ -lemma make_pos_rule: "P|Q ==> ((P==>~P) ==> Q)" +lemma make_pos_rule: "P\Q \ ((P\\P) \ Q)" by blast text\Versions of \make_neg_rule\ and \make_pos_rule\ that don't @@ -79,15 +79,15 @@ lemmas make_neg_rule' = make_refined_neg_rule -lemma make_pos_rule': "[|P|Q; ~P|] ==> Q" +lemma make_pos_rule': "\P\Q; \P\ \ Q" by blast text\Generation of a goal clause -- put away the final literal\ -lemma make_neg_goal: "~P ==> ((~P==>P) ==> False)" +lemma make_neg_goal: "\P \ ((\P\P) \ False)" by blast -lemma make_pos_goal: "P ==> ((P==>~P) ==> False)" +lemma make_pos_goal: "P \ ((P\\P) \ False)" by blast @@ -97,18 +97,17 @@ (*NOTE: could handle conjunctions (faster?) by nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *) -lemma conj_forward: "[| P'&Q'; P' ==> P; Q' ==> Q |] ==> P&Q" +lemma conj_forward: "\P'\Q'; P' \ P; Q' \ Q \ \ P\Q" by blast -lemma disj_forward: "[| P'|Q'; P' ==> P; Q' ==> Q |] ==> P|Q" +lemma disj_forward: "\P'\Q'; P' \ P; Q' \ Q \ \ P\Q" by blast -lemma imp_forward: "[| P' \ Q'; P ==> P'; Q' ==> Q |] ==> P \ Q" +lemma imp_forward: "\P' \ Q'; P \ P'; Q' \ Q \ \ P \ Q" by blast (*Version of @{text disj_forward} for removal of duplicate literals*) -lemma disj_forward2: - "[| P'|Q'; P' ==> P; [| Q'; P==>False |] ==> Q |] ==> P|Q" +lemma disj_forward2: "\ P'\Q'; P' \ P; \Q'; P\False\ \ Q\ \ P\Q" apply blast done diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Nat.thy --- a/src/HOL/Nat.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Nat.thy Sun Nov 26 21:08:32 2017 +0100 @@ -360,10 +360,10 @@ for m n :: nat by (cases m) simp_all -lemma add_is_1: "m + n = Suc 0 \ m = Suc 0 \ n = 0 | m = 0 \ n = Suc 0" +lemma add_is_1: "m + n = Suc 0 \ m = Suc 0 \ n = 0 \ m = 0 \ n = Suc 0" by (cases m) simp_all -lemma one_is_add: "Suc 0 = m + n \ m = Suc 0 \ n = 0 | m = 0 \ n = Suc 0" +lemma one_is_add: "Suc 0 = m + n \ m = Suc 0 \ n = 0 \ m = 0 \ n = Suc 0" by (rule trans, rule eq_commute, rule add_is_1) lemma add_eq_self_zero: "m + n = m \ n = 0" @@ -735,7 +735,7 @@ for m n :: nat unfolding less_le .. -lemma nat_le_linear: "m \ n | n \ m" +lemma nat_le_linear: "m \ n \ n \ m" for m n :: nat by (rule linear) diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Nitpick.thy Sun Nov 26 21:08:32 2017 +0100 @@ -150,10 +150,10 @@ "one_frac \ Abs_Frac (1, 1)" definition num :: "'a \ int" where - "num \ fst o Rep_Frac" + "num \ fst \ Rep_Frac" definition denom :: "'a \ int" where - "denom \ snd o Rep_Frac" + "denom \ snd \ Rep_Frac" function norm_frac :: "int \ int \ int \ int" where "norm_frac a b = diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Nonstandard_Analysis/HTranscendental.thy --- a/src/HOL/Nonstandard_Analysis/HTranscendental.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Nonstandard_Analysis/HTranscendental.thy Sun Nov 26 21:08:32 2017 +0100 @@ -370,7 +370,7 @@ done lemma starfun_exp_HInfinite_Infinitesimal_disj: - "x \ HInfinite ==> ( *f* exp) x \ HInfinite | ( *f* exp) (x::hypreal) \ Infinitesimal" + "x \ HInfinite \ ( *f* exp) x \ HInfinite \ ( *f* exp) (x::hypreal) \ Infinitesimal" apply (insert linorder_linear [of x 0]) apply (auto intro: starfun_exp_HInfinite starfun_exp_Infinitesimal) done diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Nonstandard_Analysis/HyperNat.thy --- a/src/HOL/Nonstandard_Analysis/HyperNat.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Nonstandard_Analysis/HyperNat.thy Sun Nov 26 21:08:32 2017 +0100 @@ -154,7 +154,7 @@ lemma hypnat_of_nat_Suc [simp]: "hypnat_of_nat (Suc n) = hypnat_of_nat n + 1" by transfer simp -lemma of_nat_eq_add [rule_format]: "\d::hypnat. of_nat m = of_nat n + d --> d \ range of_nat" +lemma of_nat_eq_add [rule_format]: "\d::hypnat. of_nat m = of_nat n + d \ d \ range of_nat" apply (induct n) apply (auto simp add: add.assoc) apply (case_tac x) diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Nonstandard_Analysis/NSCA.thy --- a/src/HOL/Nonstandard_Analysis/NSCA.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Nonstandard_Analysis/NSCA.thy Sun Nov 26 21:08:32 2017 +0100 @@ -16,7 +16,7 @@ definition \\standard part map\ stc :: "hcomplex => hcomplex" where - "stc x = (SOME r. x \ HFinite & r:SComplex & r \ x)" + "stc x = (SOME r. x \ HFinite \ r\SComplex \ r \ x)" subsection\Closure Laws for SComplex, the Standard Complex Numbers\ @@ -63,7 +63,7 @@ lemma SComplex_SReal_dense: "[| x \ SComplex; y \ SComplex; hcmod x < hcmod y - |] ==> \r \ Reals. hcmod x< r & r < hcmod y" + |] ==> \r \ Reals. hcmod x< r \ r < hcmod y" apply (auto intro: SReal_dense simp add: SReal_hcmod_SComplex) done @@ -350,7 +350,7 @@ apply (simp add: Standard_HComplex st_SReal [unfolded Reals_eq_Standard]) done -lemma stc_part_Ex1: "x:HFinite ==> \!t. t \ SComplex & x \ t" +lemma stc_part_Ex1: "x\HFinite \ \!t. t \ SComplex \ x \ t" apply (drule stc_part_Ex, safe) apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym) apply (auto intro!: approx_unique_complex) diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Nonstandard_Analysis/NatStar.thy --- a/src/HOL/Nonstandard_Analysis/NatStar.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Nonstandard_Analysis/NatStar.thy Sun Nov 26 21:08:32 2017 +0100 @@ -143,9 +143,9 @@ by transfer (rule refl) lemma starfunNat_inverse_real_of_nat_Infinitesimal [simp]: - "N \ HNatInfinite \ ( *f* (%x. inverse (real x))) N \ Infinitesimal" + "N \ HNatInfinite \ ( *f* (\x. inverse (real x))) N \ Infinitesimal" apply (rule_tac f1 = inverse in starfun_o2 [THEN subst]) - apply (subgoal_tac "hypreal_of_hypnat N ~= 0") + apply (subgoal_tac "hypreal_of_hypnat N \ 0") apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat) done diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Number_Theory/Euler_Criterion.thy --- a/src/HOL/Number_Theory/Euler_Criterion.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Number_Theory/Euler_Criterion.thy Sun Nov 26 21:08:32 2017 +0100 @@ -78,7 +78,7 @@ private lemma P_lemma: assumes "x \ S1" shows "\! y. P x y" proof - - have "~ p dvd x" using assms zdvd_not_zless S1_def by auto + have "\ p dvd x" using assms zdvd_not_zless S1_def by auto hence co_xp: "coprime x p" using p_prime prime_imp_coprime_int[of p x] by (simp add: ac_simps) then obtain y' where y': "[x * y' = 1] (mod p)" using cong_solve_coprime_int by blast @@ -110,11 +110,11 @@ private lemma f_lemma_1: assumes "x \ S1" shows "f x = f (f_1 x)" using f_def f_1_lemma_2[of x] assms by auto -private lemma l1: assumes "~ QuadRes p a" "x \ S1" +private lemma l1: assumes "\ QuadRes p a" "x \ S1" shows "x \ f_1 x" using f_1_lemma_1[of x] assms unfolding P_def QuadRes_def power2_eq_square by fastforce -private lemma l2: assumes "~ QuadRes p a" "x \ S1" +private lemma l2: assumes "\ QuadRes p a" "x \ S1" shows "[\ (f x) = a] (mod p)" using assms l1 f_1_lemma_1 P_def f_def by auto @@ -165,7 +165,7 @@ by simp blast qed -private lemma l11: assumes "~ QuadRes p a" +private lemma l11: assumes "\ QuadRes p a" shows "card S2 = (p - 1) div 2" proof - have "sum card S2 = 2 * card S2" @@ -175,11 +175,11 @@ ultimately show ?thesis by linarith qed -private lemma l12: assumes "~ QuadRes p a" +private lemma l12: assumes "\ QuadRes p a" shows "[prod Prod S2 = a ^ ((p - 1) div 2)] (mod p)" using assms l2 l10 l11 unfolding S2_def by blast -private lemma E_2: assumes "~ QuadRes p a" +private lemma E_2: assumes "\ QuadRes p a" shows "[a ^ ((p - 1) div 2) = -1] (mod p)" using l9 l12 cong_trans cong_sym assms by blast lemma euler_criterion_aux: "[(Legendre a p) = a ^ ((p - 1) div 2)] (mod p)" diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Number_Theory/Gauss.thy --- a/src/HOL/Number_Theory/Gauss.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Number_Theory/Gauss.thy Sun Nov 26 21:08:32 2017 +0100 @@ -323,8 +323,8 @@ done then have "\x \ E. [(p-x) mod p = - x](mod p)" by (metis cong_def minus_mod_self1 mod_mod_trivial) - then have "[prod ((\x. x mod p) o (op - p)) E = prod (uminus) E](mod p)" - using finite_E p_ge_2 cong_prod [of E "(\x. x mod p) o (op - p)" uminus p] + then have "[prod ((\x. x mod p) \ (op - p)) E = prod (uminus) E](mod p)" + using finite_E p_ge_2 cong_prod [of E "(\x. x mod p) \ (op - p)" uminus p] by auto then have two: "[prod id F = prod (uminus) E](mod p)" by (metis FE cong_cong_mod_int cong_refl cong_prod minus_mod_self1) diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Number_Theory/Pocklington.thy --- a/src/HOL/Number_Theory/Pocklington.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Number_Theory/Pocklington.thy Sun Nov 26 21:08:32 2017 +0100 @@ -212,7 +212,7 @@ from lucas_coprime_lemma[OF n01(3) an1] cong_imp_coprime_nat an1 have an: "coprime a n" "coprime (a ^ (n - 1)) n" using \n \ 2\ by simp_all - have False if H0: "\m. 0 < m \ m < n - 1 \ [a ^ m = 1] (mod n)" (is "EX m. ?P m") + have False if H0: "\m. 0 < m \ m < n - 1 \ [a ^ m = 1] (mod n)" (is "\m. ?P m") proof - from H0[unfolded nat_exists_least_iff[of ?P]] obtain m where m: "0 < m" "m < n - 1" "[a ^ m = 1] (mod n)" "\k ?P k" diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Number_Theory/Residues.thy --- a/src/HOL/Number_Theory/Residues.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Number_Theory/Residues.thy Sun Nov 26 21:08:32 2017 +0100 @@ -296,7 +296,7 @@ fixes a m :: nat assumes "coprime a m" shows "[a ^ totient m = 1] (mod m)" -proof (cases "m = 0 | m = 1") +proof (cases "m = 0 \ m = 1") case True then show ?thesis by auto next diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Numeral_Simprocs.thy --- a/src/HOL/Numeral_Simprocs.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Numeral_Simprocs.thy Sun Nov 26 21:08:32 2017 +0100 @@ -77,7 +77,7 @@ by auto lemma nat_mult_dvd_cancel_disj[simp]: - "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))" + "(k*m) dvd (k*n) = (k=0 \ m dvd (n::nat))" by (auto simp: dvd_eq_mod_eq_0 mod_mult_mult1) lemma nat_mult_dvd_cancel1: "0 < k \ (k*m) dvd (k*n::nat) = (m dvd n)" diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Option.thy --- a/src/HOL/Option.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Option.thy Sun Nov 26 21:08:32 2017 +0100 @@ -109,7 +109,7 @@ by (simp add: map_option_case split: option.split) lemma map_option_o_case_sum [simp]: - "map_option f o case_sum g h = case_sum (map_option f o g) (map_option f o h)" + "map_option f \ case_sum g h = case_sum (map_option f \ g) (map_option f \ h)" by (rule o_case_sum) lemma map_option_cong: "x = y \ (\a. y = Some a \ f a = g a) \ map_option f x = map_option g y" diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Orderings.thy Sun Nov 26 21:08:32 2017 +0100 @@ -389,7 +389,7 @@ done lemma not_less_iff_gr_or_eq: - "\(x < y) \ (x > y | x = y)" + "\(x < y) \ (x > y \ x = y)" apply(simp add:not_less le_less) apply blast done @@ -745,14 +745,14 @@ "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10) translations - "ALL x "ALL x. x < y \ P" - "EX x "EX x. x < y \ P" - "ALL x<=y. P" => "ALL x. x <= y \ P" - "EX x<=y. P" => "EX x. x <= y \ P" - "ALL x>y. P" => "ALL x. x > y \ P" - "EX x>y. P" => "EX x. x > y \ P" - "ALL x>=y. P" => "ALL x. x >= y \ P" - "EX x>=y. P" => "EX x. x >= y \ P" + "\x "\x. x < y \ P" + "\x "\x. x < y \ P" + "\x\y. P" \ "\x. x \ y \ P" + "\x\y. P" \ "\x. x \ y \ P" + "\x>y. P" \ "\x. x > y \ P" + "\x>y. P" \ "\x. x > y \ P" + "\x\y. P" \ "\x. x \ y \ P" + "\x\y. P" \ "\x. x \ y \ P" print_translation \ let @@ -1001,22 +1001,22 @@ a >= b >= c ... in Isar proofs.\ lemma xt1 [no_atp]: - "a = b ==> b > c ==> a > c" - "a > b ==> b = c ==> a > c" - "a = b ==> b >= c ==> a >= c" - "a >= b ==> b = c ==> a >= c" - "(x::'a::order) >= y ==> y >= x ==> x = y" - "(x::'a::order) >= y ==> y >= z ==> x >= z" - "(x::'a::order) > y ==> y >= z ==> x > z" - "(x::'a::order) >= y ==> y > z ==> x > z" - "(a::'a::order) > b ==> b > a ==> P" - "(x::'a::order) > y ==> y > z ==> x > z" - "(a::'a::order) >= b ==> a ~= b ==> a > b" - "(a::'a::order) ~= b ==> a >= b ==> a > b" - "a = f b ==> b > c ==> (!!x y. x > y ==> f x > f y) ==> a > f c" - "a > b ==> f b = c ==> (!!x y. x > y ==> f x > f y) ==> f a > c" - "a = f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c" - "a >= b ==> f b = c ==> (!! x y. x >= y ==> f x >= f y) ==> f a >= c" + "a = b \ b > c \ a > c" + "a > b \ b = c \ a > c" + "a = b \ b \ c \ a \ c" + "a \ b \ b = c \ a \ c" + "(x::'a::order) \ y \ y \ x \ x = y" + "(x::'a::order) \ y \ y \ z \ x \ z" + "(x::'a::order) > y \ y \ z \ x > z" + "(x::'a::order) \ y \ y > z \ x > z" + "(a::'a::order) > b \ b > a \ P" + "(x::'a::order) > y \ y > z \ x > z" + "(a::'a::order) \ b \ a \ b \ a > b" + "(a::'a::order) \ b \ a \ b \ a > b" + "a = f b \ b > c \ (\x y. x > y \ f x > f y) \ a > f c" + "a > b \ f b = c \ (\x y. x > y \ f x > f y) \ f a > c" + "a = f b \ b \ c \ (\x y. x \ y \ f x \ f y) \ a \ f c" + "a \ b \ f b = c \ (\x y. x \ y \ f x \ f y) \ f a \ c" by auto lemma xt2 [no_atp]: diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Partial_Function.thy --- a/src/HOL/Partial_Function.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Partial_Function.thy Sun Nov 26 21:08:32 2017 +0100 @@ -340,7 +340,7 @@ lemma admissible_image: assumes pfun: "partial_function_definitions le lub" - assumes adm: "ccpo.admissible lub le (P o g)" + assumes adm: "ccpo.admissible lub le (P \ g)" assumes inj: "\x y. f x = f y \ x = y" assumes inv: "\x. f (g x) = x" shows "ccpo.admissible (img_lub f g lub) (img_ord f le) P" @@ -350,10 +350,10 @@ by (auto simp: img_ord_def intro: chainI dest: chainD) assume "A \ {}" assume P_A: "\x\A. P x" - have "(P o g) (lub (f ` A))" using adm ch' + have "(P \ g) (lub (f ` A))" using adm ch' proof (rule ccpo.admissibleD) fix x assume "x \ f ` A" - with P_A show "(P o g) x" by (auto simp: inj[OF inv]) + with P_A show "(P \ g) x" by (auto simp: inj[OF inv]) qed(simp add: \A \ {}\) thus "P (img_lub f g lub A)" unfolding img_lub_def by simp qed diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Predicate.thy Sun Nov 26 21:08:32 2017 +0100 @@ -383,7 +383,7 @@ by (rule unit_pred_cases) (auto elim: botE intro: singleI) definition map :: "('a \ 'b) \ 'a pred \ 'b pred" where - "map f P = P \ (single o f)" + "map f P = P \ (single \ f)" lemma eval_map [simp]: "eval (map f P) = (\x\{x. eval P x}. (\y. f x = y))" diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Presburger.thy Sun Nov 26 21:08:32 2017 +0100 @@ -180,8 +180,8 @@ subsubsection\First some trivial facts about periodic sets or predicates\ lemma periodic_finite_ex: - assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)" - shows "(EX x. P x) = (EX j : {1..d}. P j)" + assumes dpos: "(0::int) < d" and modd: "\x k. P x = P(x - k*d)" + shows "(\x. P x) = (\j \ {1..d}. P j)" (is "?LHS = ?RHS") proof assume ?LHS @@ -219,7 +219,7 @@ lemma decr_mult_lemma: assumes dpos: "(0::int) < d" and minus: "\x. P x \ P(x - d)" and knneg: "0 <= k" - shows "ALL x. P x \ P(x - k*d)" + shows "\x. P x \ P(x - k*d)" using knneg proof (induct rule:int_ge_induct) case base thus ?case by simp @@ -235,25 +235,25 @@ lemma minusinfinity: assumes dpos: "0 < d" and - P1eqP1: "ALL x k. P1 x = P1(x - k*d)" and ePeqP1: "EX z::int. ALL x. x < z \ (P x = P1 x)" - shows "(EX x. P1 x) \ (EX x. P x)" + P1eqP1: "\x k. P1 x = P1(x - k*d)" and ePeqP1: "\z::int. \x. x < z \ (P x = P1 x)" + shows "(\x. P1 x) \ (\x. P x)" proof - assume eP1: "EX x. P1 x" + assume eP1: "\x. P1 x" then obtain x where P1: "P1 x" .. - from ePeqP1 obtain z where P1eqP: "ALL x. x < z \ (P x = P1 x)" .. + from ePeqP1 obtain z where P1eqP: "\x. x < z \ (P x = P1 x)" .. let ?w = "x - (\x - z\ + 1) * d" from dpos have w: "?w < z" by(rule decr_lemma) have "P1 x = P1 ?w" using P1eqP1 by blast also have "\ = P(?w)" using w P1eqP by blast finally have "P ?w" using P1 by blast - thus "EX x. P x" .. + thus "\x. P x" .. qed lemma cpmi: assumes dp: "0 < D" and p1:"\z. \ x< z. P x = P' x" - and nb:"\x.(\ j\ {1..D}. \(b::int) \ B. x \ b+j) --> P (x) --> P (x - D)" + and nb:"\x.(\ j\ {1..D}. \(b::int) \ B. x \ b+j) \ P (x) \ P (x - D)" and pd: "\ x k. P' x = P' (x-k*D)" - shows "(\x. P x) = ((\ j\ {1..D} . P' j) | (\ j \ {1..D}.\ b\ B. P (b+j)))" + shows "(\x. P x) = ((\j \ {1..D} . P' j) \ (\j \ {1..D}. \ b \ B. P (b+j)))" (is "?L = (?R1 \ ?R2)") proof- {assume "?R2" hence "?L" by blast} @@ -263,11 +263,11 @@ { fix x assume P: "P x" and H: "\ ?R2" {fix y assume "\ (\j\{1..D}. \b\B. P (b + j))" and P: "P y" - hence "~(EX (j::int) : {1..D}. EX (b::int) : B. y = b+j)" by auto + hence "\(\(j::int) \ {1..D}. \(b::int) \ B. y = b+j)" by auto with nb P have "P (y - D)" by auto } - hence "ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D)" by blast + hence "\x. \(\(j::int) \ {1..D}. \(b::int) \ B. P(b+j)) \ P (x) \ P (x - D)" by blast with H P have th: " \x. P x \ P (x - D)" by auto - from p1 obtain z where z: "ALL x. x < z --> (P x = P' x)" by blast + from p1 obtain z where z: "\x. x < z \ (P x = P' x)" by blast let ?y = "x - (\x - z\ + 1)*D" have zp: "0 <= (\x - z\ + 1)" by arith from dp have yz: "?y < z" using decr_lemma[OF dp] by simp @@ -284,7 +284,7 @@ P1eqP1: "\x k. P' x = P'(x - k*d)" and ePeqP1: "\ z. \ x>z. P x = P' x" shows "(\ x. P' x) \ (\ x. P x)" proof - assume eP1: "EX x. P' x" + assume eP1: "\x. P' x" then obtain x where P1: "P' x" .. from ePeqP1 obtain z where P1eqP: "\x>z. P x = P' x" .. let ?w' = "x + (\x - z\ + 1) * d" @@ -294,12 +294,12 @@ hence "P' x = P' ?w" using P1eqP1 by blast also have "\ = P(?w)" using w P1eqP by blast finally have "P ?w" using P1 by blast - thus "EX x. P x" .. + thus "\x. P x" .. qed lemma incr_mult_lemma: - assumes dpos: "(0::int) < d" and plus: "ALL x::int. P x \ P(x + d)" and knneg: "0 <= k" - shows "ALL x. P x \ P(x + k*d)" + assumes dpos: "(0::int) < d" and plus: "\x::int. P x \ P(x + d)" and knneg: "0 <= k" + shows "\x. P x \ P(x + k*d)" using knneg proof (induct rule:int_ge_induct) case base thus ?case by simp @@ -315,9 +315,9 @@ lemma cppi: assumes dp: "0 < D" and p1:"\z. \ x> z. P x = P' x" - and nb:"\x.(\ j\ {1..D}. \(b::int) \ A. x \ b - j) --> P (x) --> P (x + D)" + and nb:"\x.(\ j\ {1..D}. \(b::int) \ A. x \ b - j) \ P (x) \ P (x + D)" and pd: "\ x k. P' x= P' (x-k*D)" - shows "(\x. P x) = ((\ j\ {1..D} . P' j) | (\ j \ {1..D}.\ b\ A. P (b - j)))" (is "?L = (?R1 \ ?R2)") + shows "(\x. P x) = ((\j \ {1..D} . P' j) \ (\ j \ {1..D}. \ b\ A. P (b - j)))" (is "?L = (?R1 \ ?R2)") proof- {assume "?R2" hence "?L" by blast} moreover @@ -326,11 +326,11 @@ { fix x assume P: "P x" and H: "\ ?R2" {fix y assume "\ (\j\{1..D}. \b\A. P (b - j))" and P: "P y" - hence "~(EX (j::int) : {1..D}. EX (b::int) : A. y = b - j)" by auto + hence "\(\(j::int) \ {1..D}. \(b::int) \ A. y = b - j)" by auto with nb P have "P (y + D)" by auto } - hence "ALL x.~(EX (j::int) : {1..D}. EX (b::int) : A. P(b-j)) --> P (x) --> P (x + D)" by blast + hence "\x. \(\(j::int) \ {1..D}. \(b::int) \ A. P(b-j)) \ P (x) \ P (x + D)" by blast with H P have th: " \x. P x \ P (x + D)" by auto - from p1 obtain z where z: "ALL x. x > z --> (P x = P' x)" by blast + from p1 obtain z where z: "\x. x > z \ (P x = P' x)" by blast let ?y = "x + (\x - z\ + 1)*D" have zp: "0 <= (\x - z\ + 1)" by arith from dp have yz: "?y > z" using incr_lemma[OF dp] by simp diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Quickcheck_Exhaustive.thy --- a/src/HOL/Quickcheck_Exhaustive.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Quickcheck_Exhaustive.thy Sun Nov 26 21:08:32 2017 +0100 @@ -336,7 +336,7 @@ enum = (Enum.enum :: 'a list) in check_all_n_lists - (\(ys, yst). f (the o map_of (zip enum ys), mk_term yst)) + (\(ys, yst). f (the \ map_of (zip enum ys), mk_term yst)) (natural_of_nat (length enum)))" definition enum_term_of_fun :: "('a \ 'b) itself \ unit \ term list" diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Quickcheck_Narrowing.thy --- a/src/HOL/Quickcheck_Narrowing.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Quickcheck_Narrowing.thy Sun Nov 26 21:08:32 2017 +0100 @@ -52,7 +52,7 @@ primrec map_cons :: "('a => 'b) => 'a narrowing_cons => 'b narrowing_cons" where - "map_cons f (Narrowing_cons ty cs) = Narrowing_cons ty (map (\c. f o c) cs)" + "map_cons f (Narrowing_cons ty cs) = Narrowing_cons ty (map (\c. f \ c) cs)" subsubsection \From narrowing's deep representation of terms to @{theory Code_Evaluation}'s terms\ @@ -111,8 +111,8 @@ definition sum :: "'a narrowing => 'a narrowing => 'a narrowing" where "sum a b d = - (case a d of Narrowing_cons (Narrowing_sum_of_products ssa) ca => - case b d of Narrowing_cons (Narrowing_sum_of_products ssb) cb => + (case a d of Narrowing_cons (Narrowing_sum_of_products ssa) ca \ + case b d of Narrowing_cons (Narrowing_sum_of_products ssb) cb \ Narrowing_cons (Narrowing_sum_of_products (ssa @ ssb)) (ca @ cb))" lemma [fundef_cong]: @@ -146,11 +146,11 @@ (* FIXME: hard-wired maximal depth of 100 here *) definition exists :: "('a :: {narrowing, partial_term_of} => property) => property" where - "exists f = (case narrowing (100 :: integer) of Narrowing_cons ty cs => Existential ty (\ t. f (conv cs t)) (partial_term_of (TYPE('a))))" + "exists f = (case narrowing (100 :: integer) of Narrowing_cons ty cs \ Existential ty (\ t. f (conv cs t)) (partial_term_of (TYPE('a))))" definition "all" :: "('a :: {narrowing, partial_term_of} => property) => property" where - "all f = (case narrowing (100 :: integer) of Narrowing_cons ty cs => Universal ty (\t. f (conv cs t)) (partial_term_of (TYPE('a))))" + "all f = (case narrowing (100 :: integer) of Narrowing_cons ty cs \ Universal ty (\t. f (conv cs t)) (partial_term_of (TYPE('a))))" subsubsection \class \is_testable\\ diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Quotient.thy Sun Nov 26 21:08:32 2017 +0100 @@ -107,7 +107,7 @@ by (metis Quotient3_rep_reflp Quotient3_symp Quotient3_transp part_equivpI) lemma abs_o_rep: - "Abs o Rep = id" + "Abs \ Rep = id" unfolding fun_eq_iff by (simp add: Quotient3_abs_rep) @@ -280,25 +280,25 @@ (* Next four lemmas are unused *) lemma all_reg: - assumes a: "!x :: 'a. (P x --> Q x)" + assumes a: "\x :: 'a. (P x \ Q x)" and b: "All P" shows "All Q" using a b by fast lemma ex_reg: - assumes a: "!x :: 'a. (P x --> Q x)" + assumes a: "\x :: 'a. (P x \ Q x)" and b: "Ex P" shows "Ex Q" using a b by fast lemma ball_reg: - assumes a: "!x :: 'a. (x \ R --> P x --> Q x)" + assumes a: "\x :: 'a. (x \ R \ P x \ Q x)" and b: "Ball R P" shows "Ball R Q" using a b by fast lemma bex_reg: - assumes a: "!x :: 'a. (x \ R --> P x --> Q x)" + assumes a: "\x :: 'a. (x \ R \ P x \ Q x)" and b: "Bex R P" shows "Bex R Q" using a b by fast diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Random_Pred.thy --- a/src/HOL/Random_Pred.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Random_Pred.thy Sun Nov 26 21:08:32 2017 +0100 @@ -59,10 +59,10 @@ in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))" definition Random :: "(Random.seed \ ('a \ (unit \ term)) \ Random.seed) \ 'a random_pred" - where "Random g = scomp g (Pair o (Predicate.single o fst))" + where "Random g = scomp g (Pair \ (Predicate.single \ fst))" definition map :: "('a \ 'b) \ 'a random_pred \ 'b random_pred" - where "map f P = bind P (single o f)" + where "map f P = bind P (single \ f)" hide_const (open) iter' iter empty single bind union if_randompred iterate_upto not_randompred Random map diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Random_Sequence.thy --- a/src/HOL/Random_Sequence.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Random_Sequence.thy Sun Nov 26 21:08:32 2017 +0100 @@ -42,7 +42,7 @@ definition map :: "('a => 'b) => 'a random_dseq => 'b random_dseq" where - "map f P = bind P (single o f)" + "map f P = bind P (single \ f)" fun Random :: "(natural \ Random.seed \ (('a \ (unit \ term)) \ Random.seed)) \ 'a random_dseq" where @@ -82,7 +82,7 @@ definition pos_map :: "('a => 'b) => 'a pos_random_dseq => 'b pos_random_dseq" where - "pos_map f P = pos_bind P (pos_single o f)" + "pos_map f P = pos_bind P (pos_single \ f)" fun iter :: "(Random.seed \ ('a \ (unit \ term)) \ Random.seed) \ natural \ Random.seed \ 'a Lazy_Sequence.lazy_sequence" @@ -132,7 +132,7 @@ definition neg_map :: "('a => 'b) => 'a neg_random_dseq => 'b neg_random_dseq" where - "neg_map f P = neg_bind P (neg_single o f)" + "neg_map f P = neg_bind P (neg_single \ f)" definition pos_not_random_dseq :: "unit neg_random_dseq => unit pos_random_dseq" where diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Record.thy --- a/src/HOL/Record.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Record.thy Sun Nov 26 21:08:32 2017 +0100 @@ -224,70 +224,70 @@ lemmas simps = Let_def repr_inv abst_inv repr_inj abst_inj lemma iso_tuple_access_update_fst_fst: - "f o h g = j o f \ - (f o iso_tuple_fst isom) o (iso_tuple_fst_update isom o h) g = - j o (f o iso_tuple_fst isom)" + "f \ h g = j \ f \ + (f \ iso_tuple_fst isom) \ (iso_tuple_fst_update isom \ h) g = + j \ (f \ iso_tuple_fst isom)" by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_fst_def simps fun_eq_iff) lemma iso_tuple_access_update_snd_snd: - "f o h g = j o f \ - (f o iso_tuple_snd isom) o (iso_tuple_snd_update isom o h) g = - j o (f o iso_tuple_snd isom)" + "f \ h g = j \ f \ + (f \ iso_tuple_snd isom) \ (iso_tuple_snd_update isom \ h) g = + j \ (f \ iso_tuple_snd isom)" by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_snd_def simps fun_eq_iff) lemma iso_tuple_access_update_fst_snd: - "(f o iso_tuple_fst isom) o (iso_tuple_snd_update isom o h) g = - id o (f o iso_tuple_fst isom)" + "(f \ iso_tuple_fst isom) \ (iso_tuple_snd_update isom \ h) g = + id \ (f \ iso_tuple_fst isom)" by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_fst_def simps fun_eq_iff) lemma iso_tuple_access_update_snd_fst: - "(f o iso_tuple_snd isom) o (iso_tuple_fst_update isom o h) g = - id o (f o iso_tuple_snd isom)" + "(f \ iso_tuple_snd isom) \ (iso_tuple_fst_update isom \ h) g = + id \ (f \ iso_tuple_snd isom)" by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_def simps fun_eq_iff) lemma iso_tuple_update_swap_fst_fst: - "h f o j g = j g o h f \ - (iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g = - (iso_tuple_fst_update isom o j) g o (iso_tuple_fst_update isom o h) f" + "h f \ j g = j g \ h f \ + (iso_tuple_fst_update isom \ h) f \ (iso_tuple_fst_update isom \ j) g = + (iso_tuple_fst_update isom \ j) g \ (iso_tuple_fst_update isom \ h) f" by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose fun_eq_iff) lemma iso_tuple_update_swap_snd_snd: - "h f o j g = j g o h f \ - (iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g = - (iso_tuple_snd_update isom o j) g o (iso_tuple_snd_update isom o h) f" + "h f \ j g = j g \ h f \ + (iso_tuple_snd_update isom \ h) f \ (iso_tuple_snd_update isom \ j) g = + (iso_tuple_snd_update isom \ j) g \ (iso_tuple_snd_update isom \ h) f" by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose fun_eq_iff) lemma iso_tuple_update_swap_fst_snd: - "(iso_tuple_snd_update isom o h) f o (iso_tuple_fst_update isom o j) g = - (iso_tuple_fst_update isom o j) g o (iso_tuple_snd_update isom o h) f" + "(iso_tuple_snd_update isom \ h) f \ (iso_tuple_fst_update isom \ j) g = + (iso_tuple_fst_update isom \ j) g \ (iso_tuple_snd_update isom \ h) f" by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def simps fun_eq_iff) lemma iso_tuple_update_swap_snd_fst: - "(iso_tuple_fst_update isom o h) f o (iso_tuple_snd_update isom o j) g = - (iso_tuple_snd_update isom o j) g o (iso_tuple_fst_update isom o h) f" + "(iso_tuple_fst_update isom \ h) f \ (iso_tuple_snd_update isom \ j) g = + (iso_tuple_snd_update isom \ j) g \ (iso_tuple_fst_update isom \ h) f" by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def simps fun_eq_iff) lemma iso_tuple_update_compose_fst_fst: - "h f o j g = k (f o g) \ - (iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g = - (iso_tuple_fst_update isom o k) (f o g)" + "h f \ j g = k (f \ g) \ + (iso_tuple_fst_update isom \ h) f \ (iso_tuple_fst_update isom \ j) g = + (iso_tuple_fst_update isom \ k) (f \ g)" by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose fun_eq_iff) lemma iso_tuple_update_compose_snd_snd: - "h f o j g = k (f o g) \ - (iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g = - (iso_tuple_snd_update isom o k) (f o g)" + "h f \ j g = k (f \ g) \ + (iso_tuple_snd_update isom \ h) f \ (iso_tuple_snd_update isom \ j) g = + (iso_tuple_snd_update isom \ k) (f \ g)" by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose fun_eq_iff) lemma iso_tuple_surjective_proof_assist_step: - "iso_tuple_surjective_proof_assist v a (iso_tuple_fst isom o f) \ - iso_tuple_surjective_proof_assist v b (iso_tuple_snd isom o f) \ + "iso_tuple_surjective_proof_assist v a (iso_tuple_fst isom \ f) \ + iso_tuple_surjective_proof_assist v b (iso_tuple_snd isom \ f) \ iso_tuple_surjective_proof_assist v (iso_tuple_cons isom a b) f" by (clarsimp simp: iso_tuple_surjective_proof_assist_def simps iso_tuple_fst_def iso_tuple_snd_def iso_tuple_cons_def) @@ -295,7 +295,7 @@ lemma iso_tuple_fst_update_accessor_cong_assist: assumes "iso_tuple_update_accessor_cong_assist f g" shows "iso_tuple_update_accessor_cong_assist - (iso_tuple_fst_update isom o f) (g o iso_tuple_fst isom)" + (iso_tuple_fst_update isom \ f) (g \ iso_tuple_fst isom)" proof - from assms have "f id = id" by (rule iso_tuple_update_accessor_cong_assist_id) @@ -307,7 +307,7 @@ lemma iso_tuple_snd_update_accessor_cong_assist: assumes "iso_tuple_update_accessor_cong_assist f g" shows "iso_tuple_update_accessor_cong_assist - (iso_tuple_snd_update isom o f) (g o iso_tuple_snd isom)" + (iso_tuple_snd_update isom \ f) (g \ iso_tuple_snd isom)" proof - from assms have "f id = id" by (rule iso_tuple_update_accessor_cong_assist_id) @@ -319,7 +319,7 @@ lemma iso_tuple_fst_update_accessor_eq_assist: assumes "iso_tuple_update_accessor_eq_assist f g a u a' v" shows "iso_tuple_update_accessor_eq_assist - (iso_tuple_fst_update isom o f) (g o iso_tuple_fst isom) + (iso_tuple_fst_update isom \ f) (g \ iso_tuple_fst isom) (iso_tuple_cons isom a b) u (iso_tuple_cons isom a' b) v" proof - from assms have "f id = id" @@ -334,7 +334,7 @@ lemma iso_tuple_snd_update_accessor_eq_assist: assumes "iso_tuple_update_accessor_eq_assist f g b u b' v" shows "iso_tuple_update_accessor_eq_assist - (iso_tuple_snd_update isom o f) (g o iso_tuple_snd isom) + (iso_tuple_snd_update isom \ f) (g \ iso_tuple_snd isom) (iso_tuple_cons isom a b) u (iso_tuple_cons isom a b') v" proof - from assms have "f id = id" diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/SMT.thy --- a/src/HOL/SMT.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/SMT.thy Sun Nov 26 21:08:32 2017 +0100 @@ -371,7 +371,7 @@ by auto lemma [z3_rule]: - "((P = Q) \ R) = (R | (Q = (\ P)))" + "((P = Q) \ R) = (R \ (Q = (\ P)))" by auto lemma [z3_rule]: diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Set.thy --- a/src/HOL/Set.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Set.thy Sun Nov 26 21:08:32 2017 +0100 @@ -837,7 +837,7 @@ lemma subset_Diff_insert: "A \ B - insert x C \ A \ B - C \ x \ A" by blast -lemma doubleton_eq_iff: "{a, b} = {c, d} \ a = c \ b = d \ a = d & b = c" +lemma doubleton_eq_iff: "{a, b} = {c, d} \ a = c \ b = d \ a = d \ b = c" by (blast elim: equalityE) lemma Un_singleton_iff: "A \ B = {x} \ A = {} \ B = {x} \ A = {x} \ B = {} \ A = {x} \ B = {x}" @@ -1584,7 +1584,7 @@ "\A P Q. (\x\A. P \ Q x) \ (P \ (\x\A. Q x))" "\P. (\x\{}. P x) \ False" "\P. (\x\UNIV. P x) \ (\x. P x)" - "\a B P. (\x\insert a B. P x) \ (P a | (\x\B. P x))" + "\a B P. (\x\insert a B. P x) \ (P a \ (\x\B. P x))" "\P Q. (\x\Collect Q. P x) \ (\x. Q x \ P x)" "\A P f. (\x\f`A. P x) \ (\x\A. P (f x))" "\A P. (\(\x\A. P x)) \ (\x\A. \ P x)" diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Set_Interval.thy Sun Nov 26 21:08:32 2017 +0100 @@ -196,19 +196,19 @@ begin lemma greaterThanLessThan_iff [simp]: - "(i : {l<.. {l<.. i < u)" by (simp add: greaterThanLessThan_def) lemma atLeastLessThan_iff [simp]: - "(i : {l.. {l.. i \ i < u)" by (simp add: atLeastLessThan_def) lemma greaterThanAtMost_iff [simp]: - "(i : {l<..u}) = (l < i & i <= u)" + "(i \ {l<..u}) = (l < i \ i \ u)" by (simp add: greaterThanAtMost_def) lemma atLeastAtMost_iff [simp]: - "(i : {l..u}) = (l <= i & i <= u)" + "(i \ {l..u}) = (l \ i \ i \ u)" by (simp add: atLeastAtMost_def) text \The above four lemmas could be declared as iffs. Unfortunately this @@ -234,11 +234,11 @@ by(auto simp: atLeastAtMost_def atLeast_def atMost_def) lemma atLeastatMost_empty_iff[simp]: - "{a..b} = {} \ (~ a <= b)" + "{a..b} = {} \ (\ a \ b)" by auto (blast intro: order_trans) lemma atLeastatMost_empty_iff2[simp]: - "{} = {a..b} \ (~ a <= b)" + "{} = {a..b} \ (\ a \ b)" by auto (blast intro: order_trans) lemma atLeastLessThan_empty[simp]: @@ -246,20 +246,20 @@ by(auto simp: atLeastLessThan_def) lemma atLeastLessThan_empty_iff[simp]: - "{a.. (~ a < b)" + "{a.. (\ a < b)" by auto (blast intro: le_less_trans) lemma atLeastLessThan_empty_iff2[simp]: - "{} = {a.. (~ a < b)" + "{} = {a.. (\ a < b)" by auto (blast intro: le_less_trans) lemma greaterThanAtMost_empty[simp]: "l \ k ==> {k<..l} = {}" by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def) -lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \ ~ k < l" +lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \ \ k < l" by auto (blast intro: less_le_trans) -lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \ ~ k < l" +lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \ \ k < l" by auto (blast intro: less_le_trans) lemma greaterThanLessThan_empty[simp]:"l \ k ==> {k<.. {a .. b} = {a}" by simp lemma atLeastatMost_subset_iff[simp]: - "{a..b} <= {c..d} \ (~ a <= b) | c <= a & b <= d" + "{a..b} \ {c..d} \ (\ a \ b) \ c \ a \ b \ d" unfolding atLeastAtMost_def atLeast_def atMost_def by (blast intro: order_trans) lemma atLeastatMost_psubset_iff: "{a..b} < {c..d} \ - ((~ a <= b) | c <= a & b <= d & (c < a | b < d)) & c <= d" + ((\ a \ b) \ c \ a \ b \ d \ (c < a \ b < d)) \ c \ d" by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans) lemma Icc_eq_Icc[simp]: @@ -294,11 +294,11 @@ qed simp lemma Icc_subset_Ici_iff[simp]: - "{l..h} \ {l'..} = (~ l\h \ l\l')" + "{l..h} \ {l'..} = (\ l\h \ l\l')" by(auto simp: subset_eq intro: order_trans) lemma Icc_subset_Iic_iff[simp]: - "{l..h} \ {..h'} = (~ l\h \ h\h')" + "{l..h} \ {..h'} = (\ l\h \ h\h')" by(auto simp: subset_eq intro: order_trans) lemma not_Ici_eq_empty[simp]: "{l..} \ {}" @@ -462,7 +462,7 @@ end lemma (in linorder) atLeastLessThan_subset_iff: - "{a.. b <= a | c<=a & b<=d" + "{a.. {c.. b \ a \ c\a \ b\d" apply (auto simp:subset_eq Ball_def) apply(frule_tac x=a in spec) apply(erule_tac x=d in allE) @@ -1092,7 +1092,7 @@ text \A set of natural numbers is finite iff it is bounded.\ lemma finite_nat_set_iff_bounded: - "finite(N::nat set) = (EX m. ALL n:N. nm. \n\N. n?F\, simplified less_Suc_eq_le[symmetric]] by blast @@ -1101,7 +1101,7 @@ qed lemma finite_nat_set_iff_bounded_le: - "finite(N::nat set) = (EX m. ALL n:N. n<=m)" + "finite(N::nat set) = (\m. \n\N. n<=m)" apply(simp add:finite_nat_set_iff_bounded) apply(blast dest:less_imp_le_nat le_imp_less_Suc) done @@ -1177,8 +1177,8 @@ proof fix x assume "x : ?B" then obtain i where i: "i : {k..n+k}" "x : M(i)" by auto - hence "i-k\n & x : M((i-k)+k)" by auto - thus "x : ?A" by blast + hence "i-k\n \ x \ M((i-k)+k)" by auto + thus "x \ ?A" by blast qed qed @@ -1263,7 +1263,7 @@ by (blast dest: ex_bij_betw_nat_finite bij_betw_inv) lemma finite_same_card_bij: - "finite A \ finite B \ card A = card B \ EX h. bij_betw h A B" + "finite A \ finite B \ card A = card B \ \h. bij_betw h A B" apply(drule ex_bij_betw_finite_nat) apply(drule ex_bij_betw_nat_finite) apply(auto intro!:bij_betw_trans) @@ -1282,7 +1282,7 @@ using assms ex_bij_betw_finite_nat by blast moreover obtain g where "bij_betw g {0 ..< card B} B" using assms ex_bij_betw_nat_finite by blast - ultimately have "bij_betw (g o f) A B" + ultimately have "bij_betw (g \ f) A B" by (auto simp: bij_betw_trans) thus "(\f. bij_betw f A B)" by blast qed (auto simp: bij_betw_same_card) @@ -1297,11 +1297,11 @@ moreover obtain g where "inj_on g {0 ..< card B}" and 3: "g ` {0 ..< card B} = B" using FIN' ex_bij_betw_nat_finite unfolding bij_betw_def by force ultimately have "inj_on g (f ` A)" using subset_inj_on[of g _ "f ` A"] * by force - hence "inj_on (g o f) A" using 1 comp_inj_on by blast + hence "inj_on (g \ f) A" using 1 comp_inj_on by blast moreover {have "{0 ..< card A} \ {0 ..< card B}" using * by force with 2 have "f ` A \ {0 ..< card B}" by blast - hence "(g o f) ` A \ B" unfolding comp_def using 3 by force + hence "(g \ f) ` A \ B" unfolding comp_def using 3 by force } ultimately show "(\f. inj_on f A \ f ` A \ B)" by blast qed (insert assms, auto) @@ -1541,7 +1541,7 @@ subsubsection \Some Subset Conditions\ lemma ivl_subset [simp]: - "({i.. {m.. i | m \ i & j \ (n::'a::linorder))" + "({i.. {m.. i \ m \ i \ j \ (n::'a::linorder))" apply(auto simp:linorder_not_le) apply(rule ccontr) apply(insert linorder_le_less_linear[of i n]) @@ -1809,7 +1809,7 @@ by (induct n, auto simp add: algebra_simps not_le le_Suc_eq) lemma sum_nat_group: "(\m 0 < k", auto) apply (induct "n") apply (simp_all add: sum_add_nat_ivl add.commute atLeast0LessThan[symmetric]) done diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/String.thy --- a/src/HOL/String.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/String.thy Sun Nov 26 21:08:32 2017 +0100 @@ -359,7 +359,7 @@ subsection \Dedicated conversion for generated computations\ definition char_of_num :: "num \ char" - where "char_of_num = char_of_nat o nat_of_num" + where "char_of_num = char_of_nat \ nat_of_num" lemma [code_computation_unfold]: "Char = char_of_num" diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Sun Nov 26 21:08:32 2017 +0100 @@ -1598,7 +1598,7 @@ (** Helper facts **) -val not_ffalse = @{lemma "~ fFalse" by (unfold fFalse_def) fast} +val not_ffalse = @{lemma "\ fFalse" by (unfold fFalse_def) fast} val ftrue = @{lemma "fTrue" by (unfold fTrue_def) fast} (* The Boolean indicates that a fairly sound type encoding is needed. *) @@ -1624,13 +1624,13 @@ fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]} |> map (pair Non_Rec_Def)), (("fconj", false), - @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q" by (unfold fconj_def) fast+} + @{lemma "\ P \ \ Q \ fconj P Q" "\ fconj P Q \ P" "\ fconj P Q \ Q" by (unfold fconj_def) fast+} |> map (pair General)), (("fdisj", false), - @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q" by (unfold fdisj_def) fast+} + @{lemma "\ P \ fdisj P Q" "\ Q \ fdisj P Q" "\ fdisj P Q \ P \ Q" by (unfold fdisj_def) fast+} |> map (pair General)), (("fimplies", false), - @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q" + @{lemma "P \ fimplies P Q" "\ Q \ fimplies P Q" "\ fimplies P Q \ \ P \ Q" by (unfold fimplies_def) fast+} |> map (pair General)), (("fequal", true), @@ -1642,8 +1642,8 @@ |> map (pair General)), (* Partial characterization of "fAll" and "fEx". A complete characterization would require the axiom of choice for replay with Metis. *) - (("fAll", false), [(General, @{lemma "~ fAll P | P x" by (auto simp: fAll_def)})]), - (("fEx", false), [(General, @{lemma "~ P x | fEx P" by (auto simp: fEx_def)})])] + (("fAll", false), [(General, @{lemma "\ fAll P \ P x" by (auto simp: fAll_def)})]), + (("fEx", false), [(General, @{lemma "\ P x \ fEx P" by (auto simp: fEx_def)})])] |> map (apsnd (map (apsnd zero_var_indexes))) val completish_helper_table = diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Nov 26 21:08:32 2017 +0100 @@ -285,10 +285,10 @@ else if s = tptp_and then HOLogic.conj else if s = tptp_implies then HOLogic.imp else if s = tptp_iff orelse s = tptp_equal then HOLogic.eq_const dummyT - else if s = tptp_not_iff orelse s = tptp_not_equal then @{term "%P Q. Q ~= P"} - else if s = tptp_if then @{term "%P Q. Q --> P"} - else if s = tptp_not_and then @{term "%P Q. ~ (P & Q)"} - else if s = tptp_not_or then @{term "%P Q. ~ (P | Q)"} + else if s = tptp_not_iff orelse s = tptp_not_equal then @{term "\P Q. Q \ P"} + else if s = tptp_if then @{term "\P Q. Q \ P"} + else if s = tptp_not_and then @{term "\P Q. \ (P \ Q)"} + else if s = tptp_not_or then @{term "\P Q. \ (P \ Q)"} else if s = tptp_not then HOLogic.Not else if s = tptp_ho_forall then HOLogic.all_const dummyT else if s = tptp_ho_exists then HOLogic.exists_const dummyT diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Tools/Argo/argo_real.ML --- a/src/HOL/Tools/Argo/argo_real.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Tools/Argo/argo_real.ML Sun Nov 26 21:08:32 2017 +0100 @@ -241,8 +241,8 @@ by (simp add: max_def)} val abs_thm = mk_rewr @{lemma "abs (x::real) = (if 0 <= x then x else -x)" by simp} val sub_eq_thm = mk_rewr @{lemma "((x::real) = y) = (x - y = 0)" by simp} -val eq_le_thm = mk_rewr @{lemma "((x::real) = y) = ((x <= y) & (y <= x))" by (rule order_eq_iff)} -val add_le_thm = mk_rewr @{lemma "((x::real) <= y) = (x + n <= y + n)" by simp} +val eq_le_thm = mk_rewr @{lemma "((x::real) = y) = ((x \ y) \ (y \ x))" by (rule order_eq_iff)} +val add_le_thm = mk_rewr @{lemma "((x::real) \ y) = (x + n \ y + n)" by simp} val add_lt_thm = mk_rewr @{lemma "((x::real) < y) = (x + n < y + n)" by simp} val sub_le_thm = mk_rewr @{lemma "((x::real) <= y) = (x - y <= 0)" by simp} val sub_lt_thm = mk_rewr @{lemma "((x::real) < y) = (x - y < 0)" by simp} @@ -250,8 +250,8 @@ val neg_mul_le_thm = mk_rewr @{lemma "n < 0 ==> ((x::real) <= y) = (n * y <= n * x)" by simp} val pos_mul_lt_thm = mk_rewr @{lemma "0 < n ==> ((x::real) < y) = (n * x < n * y)" by simp} val neg_mul_lt_thm = mk_rewr @{lemma "n < 0 ==> ((x::real) < y) = (n * y < n * x)" by simp} -val not_le_thm = mk_rewr @{lemma "(~((x::real) <= y)) = (y < x)" by auto} -val not_lt_thm = mk_rewr @{lemma "(~((x::real) < y)) = (y <= x)" by auto} +val not_le_thm = mk_rewr @{lemma "(\((x::real) \ y)) = (y < x)" by auto} +val not_lt_thm = mk_rewr @{lemma "(\((x::real) < y)) = (y \ x)" by auto} fun replay_rewr _ Argo_Proof.Rewr_Neg = Conv.rewr_conv neg_thm | replay_rewr ctxt (Argo_Proof.Rewr_Add ps) = add_conv ctxt ps diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Tools/Argo/argo_tactic.ML --- a/src/HOL/Tools/Argo/argo_tactic.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Tools/Argo/argo_tactic.ML Sun Nov 26 21:08:32 2017 +0100 @@ -325,12 +325,12 @@ fun taut_or1_term i ts = [mk_nary HOLogic.mk_disj ts, HOLogic.mk_not (nth ts i)] fun taut_or2_term ts = HOLogic.mk_not (mk_nary HOLogic.mk_disj ts) :: ts -val iff_1_taut = @{lemma "P = Q | P | Q" by fast} -val iff_2_taut = @{lemma "P = Q | (~P) | (~Q)" by fast} -val iff_3_taut = @{lemma "~(P = Q) | (~P) | Q" by fast} -val iff_4_taut = @{lemma "~(P = Q) | P | (~Q)" by fast} -val ite_then_taut = @{lemma "~P | (if P then t else u) = t" by auto} -val ite_else_taut = @{lemma "P | (if P then t else u) = u" by auto} +val iff_1_taut = @{lemma "P = Q \ P \ Q" by fast} +val iff_2_taut = @{lemma "P = Q \ (\P) \ (\Q)" by fast} +val iff_3_taut = @{lemma "\(P = Q) \ (\P) \ Q" by fast} +val iff_4_taut = @{lemma "\(P = Q) \ P \ (\Q)" by fast} +val ite_then_taut = @{lemma "\P \ (if P then t else u) = t" by auto} +val ite_else_taut = @{lemma "P \ (if P then t else u) = u" by auto} fun taut_rule_of ctxt (Argo_Proof.Taut_And_1 n) = with_frees ctxt n taut_and1_term | taut_rule_of ctxt (Argo_Proof.Taut_And_2 (i, n)) = with_frees ctxt n (taut_and2_term i) @@ -364,8 +364,8 @@ if i > 1 then (Conv.rewr_conv rule then_conv Conv.arg_conv (not_nary_conv rule (i - 1))) ct else Conv.all_conv ct -val flatten_and_thm = @{lemma "(P1 & P2) & P3 == P1 & P2 & P3" by simp} -val flatten_or_thm = @{lemma "(P1 | P2) | P3 == P1 | P2 | P3" by simp} +val flatten_and_thm = @{lemma "(P1 \ P2) \ P3 \ P1 \ P2 \ P3" by simp} +val flatten_or_thm = @{lemma "(P1 \ P2) \ P3 \ P1 \ P2 \ P3" by simp} fun flatten_conv cv rule ct = ( Conv.try_conv (Conv.arg_conv cv) then_conv @@ -384,14 +384,14 @@ fun explode rule1 rule2 thm = explode rule1 rule2 (thm RS rule1) @ explode rule1 rule2 (thm RS rule2) handle THM _ => [thm] val explode_conj = explode @{thm conjunct1} @{thm conjunct2} -val explode_ndis = explode @{lemma "~(P | Q) ==> ~P" by auto} @{lemma "~(P | Q) ==> ~Q" by auto} +val explode_ndis = explode @{lemma "\(P \ Q) \ \P" by auto} @{lemma "\(P \ Q) \ \Q" by auto} fun pick_false i thms = nth thms i fun pick_dual rule (i1, i2) thms = rule OF [nth thms i1, nth thms i2] handle THM _ => rule OF [nth thms i2, nth thms i1] -val pick_dual_conj = pick_dual @{lemma "~P ==> P ==> False" by auto} -val pick_dual_ndis = pick_dual @{lemma "~P ==> P ==> ~True" by auto} +val pick_dual_conj = pick_dual @{lemma "\P \ P \ False" by auto} +val pick_dual_ndis = pick_dual @{lemma "\P \ P \ \True" by auto} fun join thm0 rule is thms = let @@ -399,13 +399,13 @@ val thms' = fold (fn i => cons (if 0 <= i andalso i < l then nth thms i else thm0)) is [] in fold (fn thm => fn thm' => discharge2 thm thm' rule) (tl thms') (hd thms') end -val join_conj = join @{lemma "True" by auto} @{lemma "P ==> Q ==> P & Q" by auto} -val join_ndis = join @{lemma "~False" by auto} @{lemma "~P ==> ~Q ==> ~(P | Q)" by auto} +val join_conj = join @{lemma "True" by auto} @{lemma "P \ Q \ P \ Q" by auto} +val join_ndis = join @{lemma "\False" by auto} @{lemma "\P \ \Q \ \(P \ Q)" by auto} -val false_thm = @{lemma "False ==> P" by auto} -val ntrue_thm = @{lemma "~True ==> P" by auto} -val iff_conj_thm = @{lemma "(P ==> Q) ==> (Q ==> P) ==> P = Q" by auto} -val iff_ndis_thm = @{lemma "(~P ==> ~Q) ==> (~Q ==> ~P) ==> P = Q" by auto} +val false_thm = @{lemma "False \ P" by auto} +val ntrue_thm = @{lemma "\True \ P" by auto} +val iff_conj_thm = @{lemma "(P \ Q) \ (Q \ P) \ P = Q" by auto} +val iff_ndis_thm = @{lemma "(\P \ \Q) \ (\Q \ \P) \ P = Q" by auto} fun iff_intro rule lf rf ct = let @@ -421,21 +421,21 @@ val sort_conj = sort_nary with_conj join_conj explode_conj val sort_ndis = sort_nary with_ndis join_ndis explode_ndis -val not_true_thm = mk_rewr @{lemma "(~True) = False" by auto} -val not_false_thm = mk_rewr @{lemma "(~False) = True" by auto} -val not_not_thm = mk_rewr @{lemma "(~~P) = P" by auto} -val not_and_thm = mk_rewr @{lemma "(~(P & Q)) = (~P | ~Q)" by auto} -val not_or_thm = mk_rewr @{lemma "(~(P | Q)) = (~P & ~Q)" by auto} +val not_true_thm = mk_rewr @{lemma "(\True) = False" by auto} +val not_false_thm = mk_rewr @{lemma "(\False) = True" by auto} +val not_not_thm = mk_rewr @{lemma "(\\P) = P" by auto} +val not_and_thm = mk_rewr @{lemma "(\(P \ Q)) = (\P \ \Q)" by auto} +val not_or_thm = mk_rewr @{lemma "(\(P \ Q)) = (\P \ \Q)" by auto} val not_iff_thms = map mk_rewr - @{lemma "(~((~P) = Q)) = (P = Q)" "(~(P = (~Q))) = (P = Q)" "(~(P = Q)) = ((~P) = Q)" by auto} + @{lemma "(\((\P) = Q)) = (P = Q)" "(\(P = (\Q))) = (P = Q)" "(\(P = Q)) = ((\P) = Q)" by auto} val iff_true_thms = map mk_rewr @{lemma "(True = P) = P" "(P = True) = P" by auto} -val iff_false_thms = map mk_rewr @{lemma "(False = P) = (~P)" "(P = False) = (~P)" by auto} -val iff_not_not_thm = mk_rewr @{lemma "((~P) = (~Q)) = (P = Q)" by auto} +val iff_false_thms = map mk_rewr @{lemma "(False = P) = (\P)" "(P = False) = (\P)" by auto} +val iff_not_not_thm = mk_rewr @{lemma "((\P) = (\Q)) = (P = Q)" by auto} val iff_refl_thm = mk_rewr @{lemma "(P = P) = True" by auto} val iff_symm_thm = mk_rewr @{lemma "(P = Q) = (Q = P)" by auto} -val iff_dual_thms = map mk_rewr @{lemma "(P = (~P)) = False" "((~P) = P) = False" by auto} -val imp_thm = mk_rewr @{lemma "(P --> Q) = (~P | Q)" by auto} -val ite_prop_thm = mk_rewr @{lemma "(If P Q R) = ((~P | Q) & (P | R) & (Q | R))" by auto} +val iff_dual_thms = map mk_rewr @{lemma "(P = (\P)) = False" "((\P) = P) = False" by auto} +val imp_thm = mk_rewr @{lemma "(P \ Q) = (\P \ Q)" by auto} +val ite_prop_thm = mk_rewr @{lemma "(If P Q R) = ((\P \ Q) \ (P \ R) \ (Q \ R))" by auto} val ite_true_thm = mk_rewr @{lemma "(If True t u) = t" by auto} val ite_false_thm = mk_rewr @{lemma "(If False t u) = u" by auto} val ite_eq_thm = mk_rewr @{lemma "(If P t t) = t" by auto} @@ -494,8 +494,8 @@ (* proof replay for clauses *) -val prep_clause_rule = @{lemma "P ==> ~P ==> False" by fast} -val extract_lit_rule = @{lemma "(~(P | Q) ==> False) ==> ~P ==> ~Q ==> False" by fast} +val prep_clause_rule = @{lemma "P \ \P \ False" by fast} +val extract_lit_rule = @{lemma "(\(P \ Q) \ False) \ \P \ \Q \ False" by fast} fun add_lit i thm lits = let val ct = Thm.cprem_of thm 1 @@ -518,7 +518,7 @@ (* proof replay for unit resolution *) -val unit_rule = @{lemma "(P ==> False) ==> (~P ==> False) ==> False" by fast} +val unit_rule = @{lemma "(P \ False) \ (\P \ False) \ False" by fast} val unit_rule_var = Thm.dest_arg (Thm.dest_arg1 (Thm.cprem_of unit_rule 1)) val bogus_ct = @{cterm HOL.True} @@ -538,7 +538,7 @@ (* proof replay for hypothesis *) -val dneg_rule = @{lemma "~~P ==> P" by auto} +val dneg_rule = @{lemma "\\P \ P" by auto} fun replay_hyp i ct = if i < 0 then (Thm.assume ct, [(~i, ct)]) @@ -562,7 +562,7 @@ (* proof replay for symmetry *) -val symm_rules = @{lemma "a = b ==> b = a" "~(a = b) ==> ~(b = a)" by simp_all} +val symm_rules = @{lemma "a = b ==> b = a" "\(a = b) \ \(b = a)" by simp_all} fun replay_symm thm = hd (discharges thm symm_rules) @@ -570,9 +570,9 @@ (* proof replay for transitivity *) val trans_rules = @{lemma - "~(a = b) ==> b = c ==> ~(a = c)" - "a = b ==> ~(b = c) ==> ~(a = c)" - "a = b ==> b = c ==> a = c" + "\(a = b) \ b = c \ \(a = c)" + "a = b \ \(b = c) \ \(a = c)" + "a = b \ b = c ==> a = c" by simp_all} fun replay_trans thm1 thm2 = hd (discharges thm2 (discharges thm1 trans_rules)) @@ -585,8 +585,8 @@ (* proof replay for substitution *) -val subst_rule1 = @{lemma "~(p a) ==> p = q ==> a = b ==> ~(q b)" by simp} -val subst_rule2 = @{lemma "p a ==> p = q ==> a = b ==> q b" by simp} +val subst_rule1 = @{lemma "\(p a) \ p = q \ a = b \ \(q b)" by simp} +val subst_rule2 = @{lemma "p a \ p = q \ a = b \ q b" by simp} fun replay_subst thm1 thm2 thm3 = subst_rule1 OF [thm1, thm2, thm3] handle THM _ => subst_rule2 OF [thm1, thm2, thm3] @@ -596,8 +596,8 @@ structure Thm_Cache = Table(type key = Argo_Proof.proof_id val ord = Argo_Proof.proof_id_ord) -val unclausify_rule1 = @{lemma "(~P ==> False) ==> P" by auto} -val unclausify_rule2 = @{lemma "(P ==> False) ==> ~P" by auto} +val unclausify_rule1 = @{lemma "(\P \ False) \ P" by auto} +val unclausify_rule2 = @{lemma "(P \ False) \ \P" by auto} fun unclausify (thm, lits) ls = (case (Thm.prop_of thm, lits) of diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Tools/BNF/bnf_comp.ML --- a/src/HOL/Tools/BNF/bnf_comp.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Sun Nov 26 21:08:32 2017 +0100 @@ -932,7 +932,7 @@ rtac ctxt refl) 1; fun pred_set_tac ctxt = HEADGOAL (EVERY' - [rtac ctxt (pred_set_of_bnf bnf RS @{thm arg_cong[of _ _ "\f. f o _"]} RS trans), + [rtac ctxt (pred_set_of_bnf bnf RS @{thm arg_cong[of _ _ "\f. f \ _"]} RS trans), SELECT_GOAL (unfold_thms_tac ctxt (@{thms Ball_comp_iff conj_comp_iff})), rtac ctxt refl]); val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML Sun Nov 26 21:08:32 2017 +0100 @@ -69,8 +69,8 @@ unfold_thms_tac ctxt xtor_un_fold_defs THEN HEADGOAL (REPEAT_DETERM o FIRST' [hyp_subst_tac_thin true ctxt, rtac ctxt refl, rtac ctxt conjI, - rtac ctxt @{thm arg_cong2[of _ _ _ _ "op o", OF refl]}, - rtac ctxt @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]}, + rtac ctxt @{thm arg_cong2[of _ _ _ _ "op \", OF refl]}, + rtac ctxt @{thm arg_cong2[of _ _ _ _ "op \", OF _ refl]}, resolve_tac ctxt map_arg_congs, resolve_tac ctxt fp_un_fold_uniques THEN_ALL_NEW case_fp fp (K all_tac) (rtac ctxt sym), SELECT_GOAL (CHANGED (unfold_thms_tac ctxt (flat [simp_thms, map_thms, map_defs, diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Sun Nov 26 21:08:32 2017 +0100 @@ -517,7 +517,7 @@ val (tfrees, _) = BNF_Util.mk_TFrees n @{context}; val T = mk_tupleT_balanced tfrees; in - @{thm asm_rl[of "ALL x. P x --> Q x" for P Q]} + @{thm asm_rl[of "\x. P x \ Q x" for P Q]} |> Thm.instantiate' [SOME (Thm.ctyp_of @{context} T)] [] |> Raw_Simplifier.rewrite_goals_rule @{context} @{thms split_paired_All[THEN eq_reflection]} |> (fn thm => impI RS funpow n (fn th => allI RS th) thm) diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Sun Nov 26 21:08:32 2017 +0100 @@ -1629,7 +1629,7 @@ val theta = (funs ~~ @{map 2} mk_fun_insts Ts funs) @ (algs ~~ map (Thm.cterm_of lthy) dtors); val dtor_unfold_dtors = (dtor_unfold_unique_thm OF - map (fn thm => mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]}) + map (fn thm => mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "op \", OF _ refl]}) @{thm trans[OF id_o o_id[symmetric]]}) map_id0s) |> split_conj_thm |> map mk_sym; in diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Tools/BNF/bnf_gfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Sun Nov 26 21:08:32 2017 +0100 @@ -807,10 +807,10 @@ EVERY' (map2 (fn map_thm => fn map_comp0 => EVERY' (map (rtac ctxt) [@{thm comp_assoc[symmetric]} RS trans, - @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_thm, refl] RS trans, + @{thm arg_cong2[of _ _ _ _ "op \"]} OF [map_thm, refl] RS trans, @{thm comp_assoc[symmetric]} RS sym RS trans, map_thm RS arg_cong RS trans, @{thm comp_assoc[symmetric]} RS trans, - @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl]])) + @{thm arg_cong2[of _ _ _ _ "op \"]} OF [map_comp0 RS sym, refl]])) maps map_comp0s)] 1; fun mk_mcong_tac ctxt m coinduct_tac map_comps dtor_maps map_cong0s set_map0ss set_Jsetss diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Sun Nov 26 21:08:32 2017 +0100 @@ -1279,7 +1279,7 @@ (funs ~~ @{map 2} mk_fun_insts Ts funs) @ (algs ~~ map (Thm.cterm_of lthy) ctors); val ctor_fold_ctors = (ctor_fold_unique_thm OF map (fn thm => mk_trans @{thm id_o} (mk_sym (thm RS - @{thm trans[OF arg_cong2[of _ _ _ _ "op o", OF refl] o_id]}))) map_id0s) + @{thm trans[OF arg_cong2[of _ _ _ _ "op \", OF refl] o_id]}))) map_id0s) |> split_conj_thm |> map mk_sym; in infer_instantiate lthy theta ctor_fold_unique_thm diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Tools/BNF/bnf_lift.ML --- a/src/HOL/Tools/BNF/bnf_lift.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Tools/BNF/bnf_lift.ML Sun Nov 26 21:08:32 2017 +0100 @@ -310,7 +310,7 @@ fun pred_set_tac ctxt = HEADGOAL (EVERY' - [rtac ctxt (pred_set_of_bnf bnf RS @{thm arg_cong[of _ _ "\f. f o _"]} RS trans), + [rtac ctxt (pred_set_of_bnf bnf RS @{thm arg_cong[of _ _ "\f. f \ _"]} RS trans), SELECT_GOAL (unfold_thms_tac ctxt (@{thms Ball_comp_iff conj_comp_iff})), rtac ctxt refl]); diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Tools/Meson/meson.ML Sun Nov 26 21:08:32 2017 +0100 @@ -770,8 +770,8 @@ (*Rules to convert the head literal into a negated assumption. If the head literal is already negated, then using notEfalse instead of notEfalse' prevents a double negation.*) -val notEfalse = @{lemma "~ P ==> P ==> False" by (rule notE)}; -val notEfalse' = @{lemma "P ==> ~ P ==> False" by (rule notE)}; +val notEfalse = @{lemma "\ P \ P \ False" by (rule notE)}; +val notEfalse' = @{lemma "P \ \ P \ False" by (rule notE)}; fun negated_asm_of_head th = th RS notEfalse handle THM _ => th RS notEfalse'; diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Sun Nov 26 21:08:32 2017 +0100 @@ -292,7 +292,7 @@ fun ss_only ths ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps ths val cheat_choice = - @{prop "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)"} + @{prop "\x. \y. Q x y \ \f. \x. Q x (f x)"} |> Logic.varify_global |> Skip_Proof.make_thm @{theory} diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Sun Nov 26 21:08:32 2017 +0100 @@ -99,7 +99,7 @@ (* INFERENCE RULE: ASSUME *) -val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)} +val EXCLUDED_MIDDLE = @{lemma "P \ \ P \ False" by (rule notE)} fun inst_excluded_middle ctxt i_atom = let @@ -256,7 +256,7 @@ don't use this trick in general because it makes the proof object uglier than necessary. FIXME. *) fun negate_head ctxt th = - if exists (fn t => t aconv @{prop "~ False"}) (Thm.prems_of th) then + if exists (fn t => t aconv @{prop "\ False"}) (Thm.prems_of th) then (th RS @{thm select_FalseI}) |> fold (rewrite_rule ctxt o single) @{thms not_atomize_select atomize_not_select} else @@ -298,7 +298,7 @@ (* INFERENCE RULE: REFL *) -val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp} +val REFL_THM = Thm.incr_indexes 2 @{lemma "t \ t \ False" by simp} val refl_x = Thm.cterm_of @{context} (Var (hd (Term.add_vars (Thm.prop_of REFL_THM) []))); val refl_idx = 1 + Thm.maxidx_of REFL_THM; @@ -312,8 +312,8 @@ (* INFERENCE RULE: EQUALITY *) -val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp} -val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp} +val subst_em = @{lemma "s = t \ P s \ \ P t \ False" by simp} +val ssubst_em = @{lemma "s = t \ P t \ \ P s \ False" by simp} fun equality_inference ctxt type_enc concealed sym_tab (pos, atom) fp fr = let val thy = Proof_Context.theory_of ctxt diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Tools/Old_Datatype/old_datatype.ML --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Sun Nov 26 21:08:32 2017 +0100 @@ -47,7 +47,7 @@ val Sumr_inject = @{thm Sumr_inject}; val datatype_injI = - @{lemma "(!!x. ALL y. f x = f y --> x = y) ==> inj f" by (simp add: inj_on_def)}; + @{lemma "(\x. \y. f x = f y \ x = y) \ inj f" by (simp add: inj_on_def)}; (** proof of characteristic theorems **) diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sun Nov 26 21:08:32 2017 +0100 @@ -142,7 +142,7 @@ map_filter (fn th => if Thm.no_prems th then SOME (OF1 @{thm equivp_reflp} th) else NONE handle THM _ => NONE) (rev (Named_Theorems.get ctxt @{named_theorems quot_equiv})) -val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)} +val eq_imp_rel = @{lemma "equivp R \ a = b \ R a b" by (simp add: equivp_reflp)} fun eq_imp_rel_get ctxt = map (OF1 eq_imp_rel) (rev (Named_Theorems.get ctxt @{named_theorems quot_equiv})) @@ -569,10 +569,10 @@ the Quot_True premise in 2nd records the lifted theorem *) val procedure_thm = - @{lemma "[|A; - A --> B; - Quot_True D ==> B = C; - C = D|] ==> D" + @{lemma "\A; + A \ B; + Quot_True D \ B = C; + C = D\ \ D" by (simp add: Quot_True_def)} (* in case of partial equivalence relations, this form of the diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Tools/SMT/conj_disj_perm.ML --- a/src/HOL/Tools/SMT/conj_disj_perm.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Tools/SMT/conj_disj_perm.ML Sun Nov 26 21:08:32 2017 +0100 @@ -20,8 +20,8 @@ fun add_lit thm = Termtab.update (HOLogic.dest_Trueprop (Thm.prop_of thm), thm) -val ndisj1_rule = @{lemma "~(P | Q) ==> ~P" by auto} -val ndisj2_rule = @{lemma "~(P | Q) ==> ~Q" by auto} +val ndisj1_rule = @{lemma "\(P \ Q) \ \P" by auto} +val ndisj2_rule = @{lemma "\(P \ Q) \ \Q" by auto} fun explode_thm thm = (case HOLogic.dest_Trueprop (Thm.prop_of thm) of @@ -33,7 +33,7 @@ and explode_conj_thm rule1 rule2 thm lits = explode_thm (thm RS rule1) (explode_thm (thm RS rule2) (add_lit thm lits)) -val not_false_rule = @{lemma "~False" by auto} +val not_false_rule = @{lemma "\False" by auto} fun explode thm = explode_thm thm (add_lit not_false_rule (add_lit @{thm TrueI} Termtab.empty)) fun find_dual_lit lits (@{const HOL.Not} $ t, thm) = Termtab.lookup lits t |> Option.map (pair thm) @@ -41,8 +41,8 @@ fun find_dual_lits lits = Termtab.get_first (find_dual_lit lits) lits -val not_not_rule = @{lemma "P ==> ~~P" by auto} -val ndisj_rule = @{lemma "~P ==> ~Q ==> ~(P | Q)" by auto} +val not_not_rule = @{lemma "P \ \\P" by auto} +val ndisj_rule = @{lemma "\P \ \Q \ \(P \ Q)" by auto} fun join lits t = (case Termtab.lookup lits t of @@ -63,8 +63,8 @@ val thm2 = prove_conj_disj_imp crhs clhs in eq_from_impls thm1 thm2 end -val not_not_false_rule = @{lemma "~~False ==> P" by auto} -val not_true_rule = @{lemma "~True ==> P" by auto} +val not_not_false_rule = @{lemma "\\False \ P" by auto} +val not_true_rule = @{lemma "\True \ P" by auto} fun prove_any_imp ct = (case Thm.term_of ct of @@ -94,7 +94,7 @@ val thm2 = if to_right then prove_any_imp crhs else prove_contradiction_imp crhs in eq_from_impls thm1 thm2 end -val contrapos_rule = @{lemma "(~P) = (~Q) ==> P = Q" by auto} +val contrapos_rule = @{lemma "(\P) = (\Q) \ P = Q" by auto} fun contrapos prove cp = contrapos_rule OF [prove (apply2 (Thm.apply @{cterm HOL.Not}) cp)] datatype kind = True | False | Conj | Disj | Other diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Tools/SMT/z3_replay.ML --- a/src/HOL/Tools/SMT/z3_replay.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Tools/SMT/z3_replay.ML Sun Nov 26 21:08:32 2017 +0100 @@ -83,7 +83,7 @@ fun rewrite_conv _ [] = Conv.all_conv | rewrite_conv ctxt eqs = Simplifier.full_rewrite (empty_simpset ctxt addsimps eqs) - val rewrite_true_rule = @{lemma "True == ~ False" by simp} + val rewrite_true_rule = @{lemma "True \ \ False" by simp} val prep_rules = [@{thm Let_def}, remove_trigger, remove_fun_app, rewrite_true_rule] fun rewrite _ [] = I @@ -142,8 +142,8 @@ (* |- (EX x. P x) = P c |- ~ (ALL x. P x) = ~ P c *) local val sk_rules = @{lemma - "c = (SOME x. P x) ==> (EX x. P x) = P c" - "c = (SOME x. ~ P x) ==> (~ (ALL x. P x)) = (~ P c)" + "c = (SOME x. P x) \ (\x. P x) = P c" + "c = (SOME x. \ P x) \ (\ (\x. P x)) = (\ P c)" by (metis someI_ex)+} in @@ -155,12 +155,12 @@ end -val true_thm = @{lemma "~False" by simp} +val true_thm = @{lemma "\False" by simp} fun make_discharge_rules rules = rules @ [@{thm allI}, @{thm refl}, @{thm reflexive}, true_thm] val intro_def_rules = @{lemma - "(~ P | P) & (P | ~ P)" - "(P | ~ P) & (~ P | P)" + "(\ P \ P) \ (P \ \ P)" + "(P \ \ P) \ (\ P \ P)" by fast+} fun discharge_assms_tac ctxt rules = diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Tools/SMT/z3_replay_methods.ML --- a/src/HOL/Tools/SMT/z3_replay_methods.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Tools/SMT/z3_replay_methods.ML Sun Nov 26 21:08:32 2017 +0100 @@ -319,8 +319,8 @@ end val cong_dest_rules = @{lemma - "(~ P | Q) & (P | ~ Q) ==> P = Q" - "(P | ~ Q) & (~ P | Q) ==> P = Q" + "(\ P \ Q) \ (P \ \ Q) \ P = Q" + "(P \ \ Q) \ (\ P \ Q) \ P = Q" by fast+} fun cong_full_core_tac ctxt = @@ -342,10 +342,10 @@ (* quantifier introduction *) val quant_intro_rules = @{lemma - "(!!x. P x = Q x) ==> (ALL x. P x) = (ALL x. Q x)" - "(!!x. P x = Q x) ==> (EX x. P x) = (EX x. Q x)" - "(!!x. (~ P x) = Q x) ==> (~ (EX x. P x)) = (ALL x. Q x)" - "(!!x. (~ P x) = Q x) ==> (~ (ALL x. P x)) = (EX x. Q x)" + "(\x. P x = Q x) ==> (\x. P x) = (\x. Q x)" + "(\x. P x = Q x) ==> (\x. P x) = (\x. Q x)" + "(!!x. (\ P x) = Q x) \ (\(\x. P x)) = (\x. Q x)" + "(\x. (\ P x) = Q x) ==> (\(\x. P x)) = (\x. Q x)" by fast+} fun quant_intro ctxt [thm] t = @@ -476,8 +476,8 @@ (* elimination of unused bound variables *) -val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast} -val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast} +val elim_all = @{lemma "P = Q \ (\x. P) = Q" by fast} +val elim_ex = @{lemma "P = Q \ (\x. P) = Q" by fast} fun elim_unused_tac ctxt i st = ( match_tac ctxt [@{thm refl}] @@ -496,7 +496,7 @@ (* quantifier instantiation *) -val quant_inst_rule = @{lemma "~P x | Q ==> ~(ALL x. P x) | Q" by fast} +val quant_inst_rule = @{lemma "\P x \ Q ==> \(\x. P x) \ Q" by fast} fun quant_inst ctxt _ t = prove ctxt t (fn _ => REPEAT_ALL_NEW (resolve_tac ctxt [quant_inst_rule]) @@ -507,8 +507,8 @@ exception LEMMA of unit -val intro_hyp_rule1 = @{lemma "(~P ==> Q) ==> P | Q" by fast} -val intro_hyp_rule2 = @{lemma "(P ==> Q) ==> ~P | Q" by fast} +val intro_hyp_rule1 = @{lemma "(\P \ Q) \ P \ Q" by fast} +val intro_hyp_rule2 = @{lemma "(P \ Q) \ \P \ Q" by fast} fun norm_lemma thm = (thm COMP_INCR intro_hyp_rule1) @@ -568,7 +568,7 @@ (* iff-false *) -val iff_false_rule = @{lemma "~P ==> P = False" by fast} +val iff_false_rule = @{lemma "\P \ P = False" by fast} fun iff_false _ [thm] _ = thm RS iff_false_rule | iff_false ctxt thms t = replay_rule_error ctxt Z3_Proof.Iff_False thms t diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Tools/cnf.ML --- a/src/HOL/Tools/cnf.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Tools/cnf.ML Sun Nov 26 21:08:32 2017 +0100 @@ -63,15 +63,15 @@ val conj_cong = @{lemma "[| P = P'; Q = Q' |] ==> (P \ Q) = (P' \ Q')" by auto}; val disj_cong = @{lemma "[| P = P'; Q = Q' |] ==> (P \ Q) = (P' \ Q')" by auto}; -val make_nnf_imp = @{lemma "[| (~P) = P'; Q = Q' |] ==> (P \ Q) = (P' \ Q')" by auto}; -val make_nnf_iff = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (P = Q) = ((P' \ NQ) \ (NP \ Q'))" by auto}; -val make_nnf_not_false = @{lemma "(~False) = True" by auto}; -val make_nnf_not_true = @{lemma "(~True) = False" by auto}; -val make_nnf_not_conj = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P \ Q)) = (P' \ Q')" by auto}; -val make_nnf_not_disj = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P \ Q)) = (P' \ Q')" by auto}; -val make_nnf_not_imp = @{lemma "[| P = P'; (~Q) = Q' |] ==> (~(P \ Q)) = (P' \ Q')" by auto}; -val make_nnf_not_iff = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (~(P = Q)) = ((P' \ Q') \ (NP \ NQ))" by auto}; -val make_nnf_not_not = @{lemma "P = P' ==> (~~P) = P'" by auto}; +val make_nnf_imp = @{lemma "[| (\P) = P'; Q = Q' |] ==> (P \ Q) = (P' \ Q')" by auto}; +val make_nnf_iff = @{lemma "[| P = P'; (\P) = NP; Q = Q'; (\Q) = NQ |] ==> (P = Q) = ((P' \ NQ) \ (NP \ Q'))" by auto}; +val make_nnf_not_false = @{lemma "(\False) = True" by auto}; +val make_nnf_not_true = @{lemma "(\True) = False" by auto}; +val make_nnf_not_conj = @{lemma "[| (\P) = P'; (\Q) = Q' |] ==> (\(P \ Q)) = (P' \ Q')" by auto}; +val make_nnf_not_disj = @{lemma "[| (\P) = P'; (\Q) = Q' |] ==> (\(P \ Q)) = (P' \ Q')" by auto}; +val make_nnf_not_imp = @{lemma "[| P = P'; (\Q) = Q' |] ==> (\(P \ Q)) = (P' \ Q')" by auto}; +val make_nnf_not_iff = @{lemma "[| P = P'; (\P) = NP; Q = Q'; (\Q) = NQ |] ==> (\(P = Q)) = ((P' \ Q') \ (NP \ NQ))" by auto}; +val make_nnf_not_not = @{lemma "P = P' ==> (\\P) = P'" by auto}; val simp_TF_conj_True_l = @{lemma "[| P = True; Q = Q' |] ==> (P \ Q) = Q'" by auto}; val simp_TF_conj_True_r = @{lemma "[| P = P'; Q = True |] ==> (P \ Q) = P'" by auto}; @@ -85,10 +85,10 @@ val make_cnf_disj_conj_l = @{lemma "[| (P \ R) = PR; (Q \ R) = QR |] ==> ((P \ Q) \ R) = (PR \ QR)" by auto}; val make_cnf_disj_conj_r = @{lemma "[| (P \ Q) = PQ; (P \ R) = PR |] ==> (P \ (Q \ R)) = (PQ \ PR)" by auto}; -val make_cnfx_disj_ex_l = @{lemma "((EX (x::bool). P x) \ Q) = (EX x. P x \ Q)" by auto}; -val make_cnfx_disj_ex_r = @{lemma "(P \ (EX (x::bool). Q x)) = (EX x. P \ Q x)" by auto}; -val make_cnfx_newlit = @{lemma "(P \ Q) = (EX x. (P \ x) \ (Q \ ~x))" by auto}; -val make_cnfx_ex_cong = @{lemma "(ALL (x::bool). P x = Q x) \ (EX x. P x) = (EX x. Q x)" by auto}; +val make_cnfx_disj_ex_l = @{lemma "((\(x::bool). P x) \ Q) = (\x. P x \ Q)" by auto}; +val make_cnfx_disj_ex_r = @{lemma "(P \ (\(x::bool). Q x)) = (\x. P \ Q x)" by auto}; +val make_cnfx_newlit = @{lemma "(P \ Q) = (\x. (P \ x) \ (Q \ \x))" by auto}; +val make_cnfx_ex_cong = @{lemma "(\(x::bool). P x = Q x) \ (\x. P x) = (\x. Q x)" by auto}; val weakening_thm = @{lemma "[| P; Q |] ==> Q" by auto}; diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Tools/inductive.ML Sun Nov 26 21:08:32 2017 +0100 @@ -108,9 +108,9 @@ val simp_thms1 = map mk_meta_eq - @{lemma "(~ True) = False" "(~ False) = True" - "(True --> P) = P" "(False --> P) = True" - "(P & True) = P" "(True & P) = P" + @{lemma "(\ True) = False" "(\ False) = True" + "(True \ P) = P" "(False \ P) = True" + "(P \ True) = P" "(True \ P) = P" by (fact simp_thms)+}; val simp_thms2 = @@ -420,7 +420,7 @@ (mono RS (fp_def RS (if coind then @{thm def_gfp_unfold} else @{thm def_lfp_unfold}))); - val rules = [refl, TrueI, @{lemma "~ False" by (rule notI)}, exI, conjI]; + val rules = [refl, TrueI, @{lemma "\ False" by (rule notI)}, exI, conjI]; val intrs = map_index (fn (i, intr) => Goal.prove_sorry ctxt [] [] intr (fn _ => EVERY @@ -451,7 +451,7 @@ val intrs = map dest_intr intr_ts ~~ intr_names; val rules1 = [disjE, exE, FalseE]; - val rules2 = [conjE, FalseE, @{lemma "~ True ==> R" by (rule notE [OF _ TrueI])}]; + val rules2 = [conjE, FalseE, @{lemma "\ True \ R" by (rule notE [OF _ TrueI])}]; fun prove_elim c = let diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Tools/rewrite_hol_proof.ML --- a/src/HOL/Tools/rewrite_hol_proof.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Tools/rewrite_hol_proof.ML Sun Nov 26 21:08:32 2017 +0100 @@ -118,7 +118,7 @@ "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %% \ \ (HOL.refl % TYPE('T3) % x1 %% prfT3) %% \ \ (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') == \ - \ (exE % TYPE('a) % P % EX x. Q x %% prfa %% prf' %% \ + \ (exE % TYPE('a) % P % \x. Q x %% prfa %% prf' %% \ \ (Lam x H : P x. \ \ exI % TYPE('a) % Q % x %% prfa %% \ \ (iffD1 % P x % Q x %% (prf % x) %% H)))", @@ -126,95 +126,95 @@ "(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %% \ \ (HOL.refl % TYPE('T3) % x1 %% prfT3) %% \ \ (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') == \ - \ (exE % TYPE('a) % Q % EX x. P x %% prfa %% prf' %% \ + \ (exE % TYPE('a) % Q % \x. P x %% prfa %% prf' %% \ \ (Lam x H : Q x. \ \ exI % TYPE('a) % P % x %% prfa %% \ \ (iffD2 % P x % Q x %% (prf % x) %% H)))", - (* & *) + (* \ *) - "(iffD1 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ - \ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% prfT3 %% prfT4 %% \ - \ (HOL.refl % TYPE('T5) % op & %% prfT5) %% prf1) %% prf2) %% prf3) == \ + "(iffD1 % A \ C % B \ D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ + \ (cong % TYPE('T3) % TYPE('T4) % op \ % op \ % A % B %% prfT3 %% prfT4 %% \ + \ (HOL.refl % TYPE('T5) % op \ %% prfT5) %% prf1) %% prf2) %% prf3) == \ \ (conjI % B % D %% \ \ (iffD1 % A % B %% prf1 %% (conjunct1 % A % C %% prf3)) %% \ \ (iffD1 % C % D %% prf2 %% (conjunct2 % A % C %% prf3)))", - "(iffD2 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ - \ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% prfT3 %% prfT4 %% \ - \ (HOL.refl % TYPE('T5) % op & %% prfT5) %% prf1) %% prf2) %% prf3) == \ + "(iffD2 % A \ C % B \ D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ + \ (cong % TYPE('T3) % TYPE('T4) % op \ % op \ % A % B %% prfT3 %% prfT4 %% \ + \ (HOL.refl % TYPE('T5) % op \ %% prfT5) %% prf1) %% prf2) %% prf3) == \ \ (conjI % A % C %% \ \ (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %% \ \ (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))", - "(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% prfb %% prfb %% \ - \ (HOL.refl % TYPE(bool=>bool) % op & A %% prfbb)) == \ - \ (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% prfb %% prfb %% \ + "(cong % TYPE(bool) % TYPE(bool) % op \ A % op \ A % B % C %% prfb %% prfb %% \ + \ (HOL.refl % TYPE(bool=>bool) % op \ A %% prfbb)) == \ + \ (cong % TYPE(bool) % TYPE(bool) % op \ A % op \ A % B % C %% prfb %% prfb %% \ \ (cong % TYPE(bool) % TYPE(bool=>bool) % \ - \ (op & :: bool=>bool=>bool) % (op & :: bool=>bool=>bool) % A % A %% \ + \ (op \ :: bool=>bool=>bool) % (op \ :: bool=>bool=>bool) % A % A %% \ \ prfb %% prfbb %% \ - \ (HOL.refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool) %% \ + \ (HOL.refl % TYPE(bool=>bool=>bool) % (op \ :: bool=>bool=>bool) %% \ \ (OfClass type_class % TYPE(bool=>bool=>bool))) %% \ \ (HOL.refl % TYPE(bool) % A %% prfb)))", - (* | *) + (* \ *) - "(iffD1 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ - \ (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% prfT3 %% prfT4 %% \ - \ (HOL.refl % TYPE('T5) % op | %% prfT5) %% prf1) %% prf2) %% prf3) == \ - \ (disjE % A % C % B | D %% prf3 %% \ + "(iffD1 % A \ C % B \ D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ + \ (cong % TYPE('T3) % TYPE('T4) % op \ % op \ % A % B %% prfT3 %% prfT4 %% \ + \ (HOL.refl % TYPE('T5) % op \ %% prfT5) %% prf1) %% prf2) %% prf3) == \ + \ (disjE % A % C % B \ D %% prf3 %% \ \ (Lam H : A. disjI1 % B % D %% (iffD1 % A % B %% prf1 %% H)) %% \ \ (Lam H : C. disjI2 % D % B %% (iffD1 % C % D %% prf2 %% H)))", - "(iffD2 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ - \ (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% prfT3 %% prfT4 %% \ - \ (HOL.refl % TYPE('T5) % op | %% prfT5) %% prf1) %% prf2) %% prf3) == \ - \ (disjE % B % D % A | C %% prf3 %% \ + "(iffD2 % A \ C % B \ D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ + \ (cong % TYPE('T3) % TYPE('T4) % op \ % op \ % A % B %% prfT3 %% prfT4 %% \ + \ (HOL.refl % TYPE('T5) % op \ %% prfT5) %% prf1) %% prf2) %% prf3) == \ + \ (disjE % B % D % A \ C %% prf3 %% \ \ (Lam H : B. disjI1 % A % C %% (iffD2 % A % B %% prf1 %% H)) %% \ \ (Lam H : D. disjI2 % C % A %% (iffD2 % C % D %% prf2 %% H)))", - "(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% prfb %% prfb %% \ - \ (HOL.refl % TYPE(bool=>bool) % op | A %% prfbb)) == \ - \ (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% prfb %% prfb %% \ + "(cong % TYPE(bool) % TYPE(bool) % op \ A % op \ A % B % C %% prfb %% prfb %% \ + \ (HOL.refl % TYPE(bool=>bool) % op \ A %% prfbb)) == \ + \ (cong % TYPE(bool) % TYPE(bool) % op \ A % op \ A % B % C %% prfb %% prfb %% \ \ (cong % TYPE(bool) % TYPE(bool=>bool) % \ - \ (op | :: bool=>bool=>bool) % (op | :: bool=>bool=>bool) % A % A %% \ + \ (op \ :: bool=>bool=>bool) % (op \ :: bool=>bool=>bool) % A % A %% \ \ prfb %% prfbb %% \ - \ (HOL.refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool) %% \ + \ (HOL.refl % TYPE(bool=>bool=>bool) % (op \ :: bool=>bool=>bool) %% \ \ (OfClass type_class % TYPE(bool=>bool=>bool))) %% \ \ (HOL.refl % TYPE(bool) % A %% prfb)))", - (* --> *) + (* \ *) - "(iffD1 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ - \ (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% prfT3 %% prfT4 %% \ - \ (HOL.refl % TYPE('T5) % op --> %% prfT5) %% prf1) %% prf2) %% prf3) == \ + "(iffD1 % A \ C % B \ D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ + \ (cong % TYPE('T3) % TYPE('T4) % op \ % op \ % A % B %% prfT3 %% prfT4 %% \ + \ (HOL.refl % TYPE('T5) % op \ %% prfT5) %% prf1) %% prf2) %% prf3) == \ \ (impI % B % D %% (Lam H: B. iffD1 % C % D %% prf2 %% \ \ (mp % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% H))))", - "(iffD2 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ - \ (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% prfT3 %% prfT4 %% \ - \ (HOL.refl % TYPE('T5) % op --> %% prfT5) %% prf1) %% prf2) %% prf3) == \ + "(iffD2 % A \ C % B \ D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ + \ (cong % TYPE('T3) % TYPE('T4) % op \ % op \ % A % B %% prfT3 %% prfT4 %% \ + \ (HOL.refl % TYPE('T5) % op \ %% prfT5) %% prf1) %% prf2) %% prf3) == \ \ (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %% \ \ (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))", - "(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% prfb %% prfb %% \ - \ (HOL.refl % TYPE(bool=>bool) % op --> A %% prfbb)) == \ - \ (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% prfb %% prfb %% \ + "(cong % TYPE(bool) % TYPE(bool) % op \ A % op \ A % B % C %% prfb %% prfb %% \ + \ (HOL.refl % TYPE(bool=>bool) % op \ A %% prfbb)) == \ + \ (cong % TYPE(bool) % TYPE(bool) % op \ A % op \ A % B % C %% prfb %% prfb %% \ \ (cong % TYPE(bool) % TYPE(bool=>bool) % \ - \ (op --> :: bool=>bool=>bool) % (op --> :: bool=>bool=>bool) % A % A %% \ + \ (op \ :: bool=>bool=>bool) % (op \ :: bool=>bool=>bool) % A % A %% \ \ prfb %% prfbb %% \ - \ (HOL.refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool) %% \ + \ (HOL.refl % TYPE(bool=>bool=>bool) % (op \ :: bool=>bool=>bool) %% \ \ (OfClass type_class % TYPE(bool=>bool=>bool))) %% \ \ (HOL.refl % TYPE(bool) % A %% prfb)))", - (* ~ *) + (* \ *) - "(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %% \ + "(iffD1 % \ P % \ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %% \ \ (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) == \ \ (notI % Q %% (Lam H: Q. \ \ notE % P % False %% prf2 %% (iffD2 % P % Q %% prf1 %% H)))", - "(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %% \ + "(iffD2 % \ P % \ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %% \ \ (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) == \ \ (notI % P %% (Lam H: P. \ \ notE % Q % False %% prf2 %% (iffD1 % P % Q %% prf1 %% H)))", diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Tools/sat.ML --- a/src/HOL/Tools/sat.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Tools/sat.ML Sun Nov 26 21:08:32 2017 +0100 @@ -71,7 +71,7 @@ val counter = Unsynchronized.ref 0; val resolution_thm = - @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)} + @{lemma "(P \ False) \ (\ P \ False) \ False" by (rule case_split)} (* ------------------------------------------------------------------------- *) (* lit_ord: an order on integers that considers their absolute values only, *) diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Transcendental.thy Sun Nov 26 21:08:32 2017 +0100 @@ -4367,7 +4367,7 @@ lemma sin_times_pi_eq_0: "sin (x * pi) = 0 \ x \ \" by (simp add: sin_zero_iff_int2) (metis Ints_cases Ints_of_int) -lemma cos_one_2pi: "cos x = 1 \ (\n::nat. x = n * 2 * pi) | (\n::nat. x = - (n * 2 * pi))" +lemma cos_one_2pi: "cos x = 1 \ (\n::nat. x = n * 2 * pi) \ (\n::nat. x = - (n * 2 * pi))" (is "?lhs = ?rhs") proof assume ?lhs