# HG changeset patch # User wenzelm # Date 1546550359 -3600 # Node ID e65314985426a22f1800061f45f4cd57a8f1e8ae # Parent e15f053a42d88c991bfe2eff81dc1a1fe03c80bd isabelle update_inner_syntax_cartouches; diff -r e15f053a42d8 -r e65314985426 src/FOL/FOL.thy --- a/src/FOL/FOL.thy Thu Jan 03 21:48:05 2019 +0100 +++ b/src/FOL/FOL.thy Thu Jan 03 22:19:19 2019 +0100 @@ -17,18 +17,18 @@ subsection \The classical axiom\ axiomatization where - classical: "(\ P \ P) \ P" + classical: \(\ P \ P) \ P\ subsection \Lemmas and proof tools\ -lemma ccontr: "(\ P \ False) \ P" +lemma ccontr: \(\ P \ False) \ P\ by (erule FalseE [THEN classical]) subsubsection \Classical introduction rules for \\\ and \\\\ -lemma disjCI: "(\ Q \ P) \ P \ Q" +lemma disjCI: \(\ Q \ P) \ P \ Q\ apply (rule classical) apply (assumption | erule meta_mp | rule disjI1 notI)+ apply (erule notE disjI2)+ @@ -36,31 +36,31 @@ text \Introduction rule involving only \\\\ lemma ex_classical: - assumes r: "\ (\x. P(x)) \ P(a)" - shows "\x. P(x)" + assumes r: \\ (\x. P(x)) \ P(a)\ + shows \\x. P(x)\ apply (rule classical) apply (rule exI, erule r) done text \Version of above, simplifying \\\\ to \\\\.\ lemma exCI: - assumes r: "\x. \ P(x) \ P(a)" - shows "\x. P(x)" + assumes r: \\x. \ P(x) \ P(a)\ + shows \\x. P(x)\ apply (rule ex_classical) apply (rule notI [THEN allI, THEN r]) apply (erule notE) apply (erule exI) done -lemma excluded_middle: "\ P \ P" +lemma excluded_middle: \\ P \ P\ apply (rule disjCI) apply assumption done lemma case_split [case_names True False]: - assumes r1: "P \ Q" - and r2: "\ P \ Q" - shows Q + assumes r1: \P \ Q\ + and r2: \\ P \ Q\ + shows \Q\ apply (rule excluded_middle [THEN disjE]) apply (erule r2) apply (erule r1) @@ -81,10 +81,10 @@ text \Classical implies (\\\) elimination.\ lemma impCE: - assumes major: "P \ Q" - and r1: "\ P \ R" - and r2: "Q \ R" - shows R + assumes major: \P \ Q\ + and r1: \\ P \ R\ + and r2: \Q \ R\ + shows \R\ apply (rule excluded_middle [THEN disjE]) apply (erule r1) apply (rule r2) @@ -96,10 +96,10 @@ Can't install as default: would break old proofs. \ lemma impCE': - assumes major: "P \ Q" - and r1: "Q \ R" - and r2: "\ P \ R" - shows R + assumes major: \P \ Q\ + and r1: \Q \ R\ + and r2: \\ P \ R\ + shows \R\ apply (rule excluded_middle [THEN disjE]) apply (erule r2) apply (rule r1) @@ -107,13 +107,13 @@ done text \Double negation law.\ -lemma notnotD: "\ \ P \ P" +lemma notnotD: \\ \ P \ P\ apply (rule classical) apply (erule notE) apply assumption done -lemma contrapos2: "\Q; \ P \ \ Q\ \ P" +lemma contrapos2: \\Q; \ P \ \ Q\ \ P\ apply (rule classical) apply (drule (1) meta_mp) apply (erule (1) notE) @@ -127,10 +127,10 @@ \\ P \ \ Q\ and \P \ Q\. \ lemma iffCE: - assumes major: "P \ Q" - and r1: "\P; Q\ \ R" - and r2: "\\ P; \ Q\ \ R" - shows R + assumes major: \P \ Q\ + and r1: \\P; Q\ \ R\ + and r2: \\\ P; \ Q\ \ R\ + shows \R\ apply (rule major [unfolded iff_def, THEN conjE]) apply (elim impCE) apply (erule (1) r2) @@ -141,32 +141,32 @@ (*Better for fast_tac: needs no quantifier duplication!*) lemma alt_ex1E: - assumes major: "\! x. P(x)" - and r: "\x. \P(x); \y y'. P(y) \ P(y') \ y = y'\ \ R" - shows R + assumes major: \\! x. P(x)\ + and r: \\x. \P(x); \y y'. P(y) \ P(y') \ y = y'\ \ R\ + shows \R\ using major proof (rule ex1E) fix x - assume * : "\y. P(y) \ y = x" - assume "P(x)" - then show R + assume * : \\y. P(y) \ y = x\ + assume \P(x)\ + then show \R\ proof (rule r) { fix y y' - assume "P(y)" and "P(y')" - with * have "x = y" and "x = y'" + assume \P(y)\ and \P(y')\ + with * have \x = y\ and \x = y'\ by - (tactic "IntPr.fast_tac @{context} 1")+ - then have "y = y'" by (rule subst) + then have \y = y'\ by (rule subst) } note r' = this - show "\y y'. P(y) \ P(y') \ y = y'" + show \\y y'. P(y) \ P(y') \ y = y'\ by (intro strip, elim conjE) (rule r') qed qed -lemma imp_elim: "P \ Q \ (\ R \ P) \ (Q \ R) \ R" +lemma imp_elim: \P \ Q \ (\ R \ P) \ (Q \ R) \ R\ by (rule classical) iprover -lemma swap: "\ P \ (\ R \ P) \ R" +lemma swap: \\ P \ (\ R \ P) \ R\ by (rule classical) iprover @@ -214,32 +214,32 @@ \ -lemma ex1_functional: "\\! z. P(a,z); P(a,b); P(a,c)\ \ b = c" +lemma ex1_functional: \\\! z. P(a,z); P(a,b); P(a,c)\ \ b = c\ by blast text \Elimination of \True\ from assumptions:\ -lemma True_implies_equals: "(True \ PROP P) \ PROP P" +lemma True_implies_equals: \(True \ PROP P) \ PROP P\ proof - assume "True \ PROP P" - from this and TrueI show "PROP P" . + assume \True \ PROP P\ + from this and TrueI show \PROP P\ . next - assume "PROP P" - then show "PROP P" . + assume \PROP P\ + then show \PROP P\ . qed -lemma uncurry: "P \ Q \ R \ P \ Q \ R" +lemma uncurry: \P \ Q \ R \ P \ Q \ R\ by blast -lemma iff_allI: "(\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))" +lemma iff_allI: \(\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))\ by blast -lemma iff_exI: "(\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))" +lemma iff_exI: \(\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))\ by blast -lemma all_comm: "(\x y. P(x,y)) \ (\y x. P(x,y))" +lemma all_comm: \(\x y. P(x,y)) \ (\y x. P(x,y))\ by blast -lemma ex_comm: "(\x y. P(x,y)) \ (\y x. P(x,y))" +lemma ex_comm: \(\x y. P(x,y)) \ (\y x. P(x,y))\ by blast @@ -251,7 +251,7 @@ false cases boil down to the same thing. \ -lemma cases_simp: "(P \ Q) \ (\ P \ Q) \ Q" +lemma cases_simp: \(P \ Q) \ (\ P \ Q) \ Q\ by blast @@ -267,32 +267,32 @@ text \Existential miniscoping.\ lemma int_ex_simps: - "\P Q. (\x. P(x) \ Q) \ (\x. P(x)) \ Q" - "\P Q. (\x. P \ Q(x)) \ P \ (\x. Q(x))" - "\P Q. (\x. P(x) \ Q) \ (\x. P(x)) \ Q" - "\P Q. (\x. P \ Q(x)) \ P \ (\x. Q(x))" + \\P Q. (\x. P(x) \ Q) \ (\x. P(x)) \ Q\ + \\P Q. (\x. P \ Q(x)) \ P \ (\x. Q(x))\ + \\P Q. (\x. P(x) \ Q) \ (\x. P(x)) \ Q\ + \\P Q. (\x. P \ Q(x)) \ P \ (\x. Q(x))\ by iprover+ text \Classical rules.\ lemma cla_ex_simps: - "\P Q. (\x. P(x) \ Q) \ (\x. P(x)) \ Q" - "\P Q. (\x. P \ Q(x)) \ P \ (\x. Q(x))" + \\P Q. (\x. P(x) \ Q) \ (\x. P(x)) \ Q\ + \\P Q. (\x. P \ Q(x)) \ P \ (\x. Q(x))\ by blast+ lemmas ex_simps = int_ex_simps cla_ex_simps text \Universal miniscoping.\ lemma int_all_simps: - "\P Q. (\x. P(x) \ Q) \ (\x. P(x)) \ Q" - "\P Q. (\x. P \ Q(x)) \ P \ (\x. Q(x))" - "\P Q. (\x. P(x) \ Q) \ (\ x. P(x)) \ Q" - "\P Q. (\x. P \ Q(x)) \ P \ (\x. Q(x))" + \\P Q. (\x. P(x) \ Q) \ (\x. P(x)) \ Q\ + \\P Q. (\x. P \ Q(x)) \ P \ (\x. Q(x))\ + \\P Q. (\x. P(x) \ Q) \ (\ x. P(x)) \ Q\ + \\P Q. (\x. P \ Q(x)) \ P \ (\x. Q(x))\ by iprover+ text \Classical rules.\ lemma cla_all_simps: - "\P Q. (\x. P(x) \ Q) \ (\x. P(x)) \ Q" - "\P Q. (\x. P \ Q(x)) \ P \ (\x. Q(x))" + \\P Q. (\x. P(x) \ Q) \ (\x. P(x)) \ Q\ + \\P Q. (\x. P \ Q(x)) \ P \ (\x. Q(x))\ by blast+ lemmas all_simps = int_all_simps cla_all_simps @@ -300,16 +300,16 @@ subsubsection \Named rewrite rules proved for IFOL\ -lemma imp_disj1: "(P \ Q) \ R \ (P \ Q \ R)" by blast -lemma imp_disj2: "Q \ (P \ R) \ (P \ Q \ R)" by blast +lemma imp_disj1: \(P \ Q) \ R \ (P \ Q \ R)\ by blast +lemma imp_disj2: \Q \ (P \ R) \ (P \ Q \ R)\ by blast -lemma de_Morgan_conj: "(\ (P \ Q)) \ (\ P \ \ Q)" by blast +lemma de_Morgan_conj: \(\ (P \ Q)) \ (\ P \ \ Q)\ by blast -lemma not_imp: "\ (P \ Q) \ (P \ \ Q)" by blast -lemma not_iff: "\ (P \ Q) \ (P \ \ Q)" by blast +lemma not_imp: \\ (P \ Q) \ (P \ \ Q)\ by blast +lemma not_iff: \\ (P \ Q) \ (P \ \ Q)\ by blast -lemma not_all: "(\ (\x. P(x))) \ (\x. \ P(x))" by blast -lemma imp_all: "((\x. P(x)) \ Q) \ (\x. P(x) \ Q)" by blast +lemma not_all: \(\ (\x. P(x))) \ (\x. \ P(x))\ by blast +lemma imp_all: \((\x. P(x)) \ Q) \ (\x. P(x) \ Q)\ by blast lemmas meta_simps = @@ -320,15 +320,15 @@ refl [THEN P_iff_T] conj_simps disj_simps not_simps imp_simps iff_simps quant_simps -lemma notFalseI: "\ False" by iprover +lemma notFalseI: \\ False\ by iprover lemma cla_simps_misc: - "\ (P \ Q) \ \ P \ \ Q" - "P \ \ P" - "\ P \ P" - "\ \ P \ P" - "(\ P \ P) \ P" - "(\ P \ \ Q) \ (P \ Q)" by blast+ + \\ (P \ Q) \ \ P \ \ Q\ + \P \ \ P\ + \\ P \ P\ + \\ \ P \ P\ + \(\ P \ P) \ P\ + \(\ P \ \ Q) \ (P \ Q)\ by blast+ lemmas cla_simps = de_Morgan_conj de_Morgan_disj imp_disj1 imp_disj2 @@ -337,8 +337,8 @@ ML_file "simpdata.ML" -simproc_setup defined_Ex ("\x. P(x)") = \fn _ => Quantifier1.rearrange_ex\ -simproc_setup defined_All ("\x. P(x)") = \fn _ => Quantifier1.rearrange_all\ +simproc_setup defined_Ex (\\x. P(x)\) = \fn _ => Quantifier1.rearrange_ex\ +simproc_setup defined_All (\\x. P(x)\) = \fn _ => Quantifier1.rearrange_all\ ML \ (*intuitionistic simprules only*) @@ -366,35 +366,35 @@ subsection \Other simple lemmas\ -lemma [simp]: "((P \ R) \ (Q \ R)) \ ((P \ Q) \ R)" +lemma [simp]: \((P \ R) \ (Q \ R)) \ ((P \ Q) \ R)\ by blast -lemma [simp]: "((P \ Q) \ (P \ R)) \ (P \ (Q \ R))" +lemma [simp]: \((P \ Q) \ (P \ R)) \ (P \ (Q \ R))\ by blast -lemma not_disj_iff_imp: "\ P \ Q \ (P \ Q)" +lemma not_disj_iff_imp: \\ P \ Q \ (P \ Q)\ by blast subsubsection \Monotonicity of implications\ -lemma conj_mono: "\P1 \ Q1; P2 \ Q2\ \ (P1 \ P2) \ (Q1 \ Q2)" +lemma conj_mono: \\P1 \ Q1; P2 \ Q2\ \ (P1 \ P2) \ (Q1 \ Q2)\ by fast (*or (IntPr.fast_tac 1)*) -lemma disj_mono: "\P1 \ Q1; P2 \ Q2\ \ (P1 \ P2) \ (Q1 \ Q2)" +lemma disj_mono: \\P1 \ Q1; P2 \ Q2\ \ (P1 \ P2) \ (Q1 \ Q2)\ by fast (*or (IntPr.fast_tac 1)*) -lemma imp_mono: "\Q1 \ P1; P2 \ Q2\ \ (P1 \ P2) \ (Q1 \ Q2)" +lemma imp_mono: \\Q1 \ P1; P2 \ Q2\ \ (P1 \ P2) \ (Q1 \ Q2)\ by fast (*or (IntPr.fast_tac 1)*) -lemma imp_refl: "P \ P" +lemma imp_refl: \P \ P\ by (rule impI) text \The quantifier monotonicity rules are also intuitionistically valid.\ -lemma ex_mono: "(\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))" +lemma ex_mono: \(\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))\ by blast -lemma all_mono: "(\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))" +lemma all_mono: \(\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))\ by blast @@ -405,21 +405,21 @@ context begin -qualified definition "induct_forall(P) \ \x. P(x)" -qualified definition "induct_implies(A, B) \ A \ B" -qualified definition "induct_equal(x, y) \ x = y" -qualified definition "induct_conj(A, B) \ A \ B" +qualified definition \induct_forall(P) \ \x. P(x)\ +qualified definition \induct_implies(A, B) \ A \ B\ +qualified definition \induct_equal(x, y) \ x = y\ +qualified definition \induct_conj(A, B) \ A \ B\ -lemma induct_forall_eq: "(\x. P(x)) \ Trueprop(induct_forall(\x. P(x)))" +lemma induct_forall_eq: \(\x. P(x)) \ Trueprop(induct_forall(\x. P(x)))\ unfolding atomize_all induct_forall_def . -lemma induct_implies_eq: "(A \ B) \ Trueprop(induct_implies(A, B))" +lemma induct_implies_eq: \(A \ B) \ Trueprop(induct_implies(A, B))\ unfolding atomize_imp induct_implies_def . -lemma induct_equal_eq: "(x \ y) \ Trueprop(induct_equal(x, y))" +lemma induct_equal_eq: \(x \ y) \ Trueprop(induct_equal(x, y))\ unfolding atomize_eq induct_equal_def . -lemma induct_conj_eq: "(A &&& B) \ Trueprop(induct_conj(A, B))" +lemma induct_conj_eq: \(A &&& B) \ Trueprop(induct_conj(A, B))\ unfolding atomize_conj induct_conj_def . lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq diff -r e15f053a42d8 -r e65314985426 src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Thu Jan 03 21:48:05 2019 +0100 +++ b/src/FOL/IFOL.thy Thu Jan 03 22:19:19 2019 +0100 @@ -26,76 +26,76 @@ setup Pure_Thy.old_appl_syntax_setup class "term" -default_sort "term" +default_sort \term\ typedecl o judgment - Trueprop :: "o \ prop" (\(_)\ 5) + Trueprop :: \o \ prop\ (\(_)\ 5) subsubsection \Equality\ axiomatization - eq :: "['a, 'a] \ o" (infixl \=\ 50) + eq :: \['a, 'a] \ o\ (infixl \=\ 50) where - refl: "a = a" and - subst: "a = b \ P(a) \ P(b)" + refl: \a = a\ and + subst: \a = b \ P(a) \ P(b)\ subsubsection \Propositional logic\ axiomatization - False :: o and - conj :: "[o, o] => o" (infixr \\\ 35) and - disj :: "[o, o] => o" (infixr \\\ 30) and - imp :: "[o, o] => o" (infixr \\\ 25) + False :: \o\ and + conj :: \[o, o] => o\ (infixr \\\ 35) and + disj :: \[o, o] => o\ (infixr \\\ 30) and + imp :: \[o, o] => o\ (infixr \\\ 25) where - conjI: "\P; Q\ \ P \ Q" and - conjunct1: "P \ Q \ P" and - conjunct2: "P \ Q \ Q" and + conjI: \\P; Q\ \ P \ Q\ and + conjunct1: \P \ Q \ P\ and + conjunct2: \P \ Q \ Q\ and - disjI1: "P \ P \ Q" and - disjI2: "Q \ P \ Q" and - disjE: "\P \ Q; P \ R; Q \ R\ \ R" and + disjI1: \P \ P \ Q\ and + disjI2: \Q \ P \ Q\ and + disjE: \\P \ Q; P \ R; Q \ R\ \ R\ and - impI: "(P \ Q) \ P \ Q" and - mp: "\P \ Q; P\ \ Q" and + impI: \(P \ Q) \ P \ Q\ and + mp: \\P \ Q; P\ \ Q\ and - FalseE: "False \ P" + FalseE: \False \ P\ subsubsection \Quantifiers\ axiomatization - All :: "('a \ o) \ o" (binder \\\ 10) and - Ex :: "('a \ o) \ o" (binder \\\ 10) + All :: \('a \ o) \ o\ (binder \\\ 10) and + Ex :: \('a \ o) \ o\ (binder \\\ 10) where - allI: "(\x. P(x)) \ (\x. P(x))" and - spec: "(\x. P(x)) \ P(x)" and - exI: "P(x) \ (\x. P(x))" and - exE: "\\x. P(x); \x. P(x) \ R\ \ R" + allI: \(\x. P(x)) \ (\x. P(x))\ and + spec: \(\x. P(x)) \ P(x)\ and + exI: \P(x) \ (\x. P(x))\ and + exE: \\\x. P(x); \x. P(x) \ R\ \ R\ subsubsection \Definitions\ -definition "True \ False \ False" +definition \True \ False \ False\ definition Not (\\ _\ [40] 40) - where not_def: "\ P \ P \ False" + where not_def: \\ P \ P \ False\ definition iff (infixr \\\ 25) - where "P \ Q \ (P \ Q) \ (Q \ P)" + where \P \ Q \ (P \ Q) \ (Q \ P)\ -definition Ex1 :: "('a \ o) \ o" (binder \\!\ 10) - where ex1_def: "\!x. P(x) \ \x. P(x) \ (\y. P(y) \ y = x)" +definition Ex1 :: \('a \ o) \ o\ (binder \\!\ 10) + where ex1_def: \\!x. P(x) \ \x. P(x) \ (\y. P(y) \ y = x)\ axiomatization where \ \Reflection, admissible\ - eq_reflection: "(x = y) \ (x \ y)" and - iff_reflection: "(P \ Q) \ (P \ Q)" + eq_reflection: \(x = y) \ (x \ y)\ and + iff_reflection: \(P \ Q) \ (P \ Q)\ -abbreviation not_equal :: "['a, 'a] \ o" (infixl \\\ 50) - where "x \ y \ \ (x = y)" +abbreviation not_equal :: \['a, 'a] \ o\ (infixl \\\ 50) + where \x \ y \ \ (x = y)\ subsubsection \Old-style ASCII syntax\ @@ -116,44 +116,44 @@ lemmas strip = impI allI -lemma TrueI: True +lemma TrueI: \True\ unfolding True_def by (rule impI) subsubsection \Sequent-style elimination rules for \\\ \\\ and \\\\ lemma conjE: - assumes major: "P \ Q" - and r: "\P; Q\ \ R" - shows R + assumes major: \P \ Q\ + and r: \\P; Q\ \ R\ + shows \R\ apply (rule r) apply (rule major [THEN conjunct1]) apply (rule major [THEN conjunct2]) done lemma impE: - assumes major: "P \ Q" - and P - and r: "Q \ R" - shows R + assumes major: \P \ Q\ + and \P\ + and r: \Q \ R\ + shows \R\ apply (rule r) apply (rule major [THEN mp]) apply (rule \P\) done lemma allE: - assumes major: "\x. P(x)" - and r: "P(x) \ R" - shows R + assumes major: \\x. P(x)\ + and r: \P(x) \ R\ + shows \R\ apply (rule r) apply (rule major [THEN spec]) done text \Duplicates the quantifier; for use with @{ML eresolve_tac}.\ lemma all_dupE: - assumes major: "\x. P(x)" - and r: "\P(x); \x. P(x)\ \ R" - shows R + assumes major: \\x. P(x)\ + and r: \\P(x); \x. P(x)\ \ R\ + shows \R\ apply (rule r) apply (rule major [THEN spec]) apply (rule major) @@ -162,20 +162,20 @@ subsubsection \Negation rules, which translate between \\ P\ and \P \ False\\ -lemma notI: "(P \ False) \ \ P" +lemma notI: \(P \ False) \ \ P\ unfolding not_def by (erule impI) -lemma notE: "\\ P; P\ \ R" +lemma notE: \\\ P; P\ \ R\ unfolding not_def by (erule mp [THEN FalseE]) -lemma rev_notE: "\P; \ P\ \ R" +lemma rev_notE: \\P; \ P\ \ R\ by (erule notE) text \This is useful with the special implication rules for each kind of \P\.\ lemma not_to_imp: - assumes "\ P" - and r: "P \ False \ Q" - shows Q + assumes \\ P\ + and r: \P \ False \ Q\ + shows \Q\ apply (rule r) apply (rule impI) apply (erule notE [OF \\ P\]) @@ -185,14 +185,14 @@ For substitution into an assumption \P\, reduce \Q\ to \P \ Q\, substitute into this implication, then apply \impI\ to move \P\ back into the assumptions. \ -lemma rev_mp: "\P; P \ Q\ \ Q" +lemma rev_mp: \\P; P \ Q\ \ Q\ by (erule mp) text \Contrapositive of an inference rule.\ lemma contrapos: - assumes major: "\ Q" - and minor: "P \ Q" - shows "\ P" + assumes major: \\ Q\ + and minor: \P \ Q\ + shows \\ P\ apply (rule major [THEN notE, THEN notI]) apply (erule minor) done @@ -214,7 +214,7 @@ subsection \If-and-only-if\ -lemma iffI: "\P \ Q; Q \ P\ \ P \ Q" +lemma iffI: \\P \ Q; Q \ P\ \ P \ Q\ apply (unfold iff_def) apply (rule conjI) apply (erule impI) @@ -222,9 +222,9 @@ done lemma iffE: - assumes major: "P \ Q" - and r: "P \ Q \ Q \ P \ R" - shows R + assumes major: \P \ Q\ + and r: \P \ Q \ Q \ P \ R\ + shows \R\ apply (insert major, unfold iff_def) apply (erule conjE) apply (erule r) @@ -234,38 +234,38 @@ subsubsection \Destruct rules for \\\ similar to Modus Ponens\ -lemma iffD1: "\P \ Q; P\ \ Q" +lemma iffD1: \\P \ Q; P\ \ Q\ apply (unfold iff_def) apply (erule conjunct1 [THEN mp]) apply assumption done -lemma iffD2: "\P \ Q; Q\ \ P" +lemma iffD2: \\P \ Q; Q\ \ P\ apply (unfold iff_def) apply (erule conjunct2 [THEN mp]) apply assumption done -lemma rev_iffD1: "\P; P \ Q\ \ Q" +lemma rev_iffD1: \\P; P \ Q\ \ Q\ apply (erule iffD1) apply assumption done -lemma rev_iffD2: "\Q; P \ Q\ \ P" +lemma rev_iffD2: \\Q; P \ Q\ \ P\ apply (erule iffD2) apply assumption done -lemma iff_refl: "P \ P" +lemma iff_refl: \P \ P\ by (rule iffI) -lemma iff_sym: "Q \ P \ P \ Q" +lemma iff_sym: \Q \ P \ P \ Q\ apply (erule iffE) apply (rule iffI) apply (assumption | erule mp)+ done -lemma iff_trans: "\P \ Q; Q \ R\ \ P \ R" +lemma iff_trans: \\P \ Q; Q \ R\ \ P \ R\ apply (rule iffI) apply (assumption | erule iffE | erule (1) notE impE)+ done @@ -282,20 +282,20 @@ do NOT mean the same thing. The parser treats \\!x y.P(x,y)\ as sequential. \ -lemma ex1I: "P(a) \ (\x. P(x) \ x = a) \ \!x. P(x)" +lemma ex1I: \P(a) \ (\x. P(x) \ x = a) \ \!x. P(x)\ apply (unfold ex1_def) apply (assumption | rule exI conjI allI impI)+ done text \Sometimes easier to use: the premises have no shared variables. Safe!\ -lemma ex_ex1I: "\x. P(x) \ (\x y. \P(x); P(y)\ \ x = y) \ \!x. P(x)" +lemma ex_ex1I: \\x. P(x) \ (\x y. \P(x); P(y)\ \ x = y) \ \!x. P(x)\ apply (erule exE) apply (rule ex1I) apply assumption apply assumption done -lemma ex1E: "\! x. P(x) \ (\x. \P(x); \y. P(y) \ y = x\ \ R) \ R" +lemma ex1E: \\! x. P(x) \ (\x. \P(x); \y. P(y) \ y = x\ \ R) \ R\ apply (unfold ex1_def) apply (assumption | erule exE conjE)+ done @@ -315,77 +315,77 @@ (fn prems => fn ctxt => SIMPLE_METHOD' (iff_tac ctxt prems))\ lemma conj_cong: - assumes "P \ P'" - and "P' \ Q \ Q'" - shows "(P \ Q) \ (P' \ Q')" + assumes \P \ P'\ + and \P' \ Q \ Q'\ + shows \(P \ Q) \ (P' \ Q')\ apply (insert assms) apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+ done text \Reversed congruence rule! Used in ZF/Order.\ lemma conj_cong2: - assumes "P \ P'" - and "P' \ Q \ Q'" - shows "(Q \ P) \ (Q' \ P')" + assumes \P \ P'\ + and \P' \ Q \ Q'\ + shows \(Q \ P) \ (Q' \ P')\ apply (insert assms) apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+ done lemma disj_cong: - assumes "P \ P'" and "Q \ Q'" - shows "(P \ Q) \ (P' \ Q')" + assumes \P \ P'\ and \Q \ Q'\ + shows \(P \ Q) \ (P' \ Q')\ apply (insert assms) apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | erule (1) notE impE)+ done lemma imp_cong: - assumes "P \ P'" - and "P' \ Q \ Q'" - shows "(P \ Q) \ (P' \ Q')" + assumes \P \ P'\ + and \P' \ Q \ Q'\ + shows \(P \ Q) \ (P' \ Q')\ apply (insert assms) apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE | iff assms)+ done -lemma iff_cong: "\P \ P'; Q \ Q'\ \ (P \ Q) \ (P' \ Q')" +lemma iff_cong: \\P \ P'; Q \ Q'\ \ (P \ Q) \ (P' \ Q')\ apply (erule iffE | assumption | rule iffI | erule (1) notE impE)+ done -lemma not_cong: "P \ P' \ \ P \ \ P'" +lemma not_cong: \P \ P' \ \ P \ \ P'\ apply (assumption | rule iffI notI | erule (1) notE impE | erule iffE notE)+ done lemma all_cong: - assumes "\x. P(x) \ Q(x)" - shows "(\x. P(x)) \ (\x. Q(x))" + assumes \\x. P(x) \ Q(x)\ + shows \(\x. P(x)) \ (\x. Q(x))\ apply (assumption | rule iffI allI | erule (1) notE impE | erule allE | iff assms)+ done lemma ex_cong: - assumes "\x. P(x) \ Q(x)" - shows "(\x. P(x)) \ (\x. Q(x))" + assumes \\x. P(x) \ Q(x)\ + shows \(\x. P(x)) \ (\x. Q(x))\ apply (erule exE | assumption | rule iffI exI | erule (1) notE impE | iff assms)+ done lemma ex1_cong: - assumes "\x. P(x) \ Q(x)" - shows "(\!x. P(x)) \ (\!x. Q(x))" + assumes \\x. P(x) \ Q(x)\ + shows \(\!x. P(x)) \ (\!x. Q(x))\ apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE | iff assms)+ done subsection \Equality rules\ -lemma sym: "a = b \ b = a" +lemma sym: \a = b \ b = a\ apply (erule subst) apply (rule refl) done -lemma trans: "\a = b; b = c\ \ a = c" +lemma trans: \\a = b; b = c\ \ a = c\ apply (erule subst, assumption) done -lemma not_sym: "b \ a \ a \ b" +lemma not_sym: \b \ a \ a \ b\ apply (erule contrapos) apply (erule sym) done @@ -395,28 +395,28 @@ the first for definitions of formulae and the second for terms. \ -lemma def_imp_iff: "(A \ B) \ A \ B" +lemma def_imp_iff: \(A \ B) \ A \ B\ apply unfold apply (rule iff_refl) done -lemma meta_eq_to_obj_eq: "(A \ B) \ A = B" +lemma meta_eq_to_obj_eq: \(A \ B) \ A = B\ apply unfold apply (rule refl) done -lemma meta_eq_to_iff: "x \ y \ x \ y" +lemma meta_eq_to_iff: \x \ y \ x \ y\ by unfold (rule iff_refl) text \Substitution.\ -lemma ssubst: "\b = a; P(a)\ \ P(b)" +lemma ssubst: \\b = a; P(a)\ \ P(b)\ apply (drule sym) apply (erule (1) subst) done text \A special case of \ex1E\ that would otherwise need quantifier expansion.\ -lemma ex1_equalsE: "\\!x. P(x); P(a); P(b)\ \ a = b" +lemma ex1_equalsE: \\\!x. P(x); P(a); P(b)\ \ a = b\ apply (erule ex1E) apply (rule trans) apply (rule_tac [2] sym) @@ -426,17 +426,17 @@ subsubsection \Polymorphic congruence rules\ -lemma subst_context: "a = b \ t(a) = t(b)" +lemma subst_context: \a = b \ t(a) = t(b)\ apply (erule ssubst) apply (rule refl) done -lemma subst_context2: "\a = b; c = d\ \ t(a,c) = t(b,d)" +lemma subst_context2: \\a = b; c = d\ \ t(a,c) = t(b,d)\ apply (erule ssubst)+ apply (rule refl) done -lemma subst_context3: "\a = b; c = d; e = f\ \ t(a,c,e) = t(b,d,f)" +lemma subst_context3: \\a = b; c = d; e = f\ \ t(a,c,e) = t(b,d,f)\ apply (erule ssubst)+ apply (rule refl) done @@ -449,7 +449,7 @@ | | c = d \ -lemma box_equals: "\a = b; a = c; b = d\ \ c = d" +lemma box_equals: \\a = b; a = c; b = d\ \ c = d\ apply (rule trans) apply (rule trans) apply (rule sym) @@ -457,7 +457,7 @@ done text \Dual of \box_equals\: for proving equalities backwards.\ -lemma simp_equals: "\a = c; b = d; c = d\ \ a = b" +lemma simp_equals: \\a = c; b = d; c = d\ \ a = b\ apply (rule trans) apply (rule trans) apply assumption+ @@ -467,13 +467,13 @@ subsubsection \Congruence rules for predicate letters\ -lemma pred1_cong: "a = a' \ P(a) \ P(a')" +lemma pred1_cong: \a = a' \ P(a) \ P(a')\ apply (rule iffI) apply (erule (1) subst) apply (erule (1) ssubst) done -lemma pred2_cong: "\a = a'; b = b'\ \ P(a,b) \ P(a',b')" +lemma pred2_cong: \\a = a'; b = b'\ \ P(a,b) \ P(a',b')\ apply (rule iffI) apply (erule subst)+ apply assumption @@ -481,7 +481,7 @@ apply assumption done -lemma pred3_cong: "\a = a'; b = b'; c = c'\ \ P(a,b,c) \ P(a',b',c')" +lemma pred3_cong: \\a = a'; b = b'; c = c'\ \ P(a,b,c) \ P(a',b',c')\ apply (rule iffI) apply (erule subst)+ apply assumption @@ -490,7 +490,7 @@ done text \Special case for the equality predicate!\ -lemma eq_cong: "\a = a'; b = b'\ \ a = b \ a' = b'" +lemma eq_cong: \\a = a'; b = b'\ \ a = b \ a' = b'\ apply (erule (1) pred2_cong) done @@ -507,29 +507,29 @@ \ lemma conj_impE: - assumes major: "(P \ Q) \ S" - and r: "P \ (Q \ S) \ R" - shows R + assumes major: \(P \ Q) \ S\ + and r: \P \ (Q \ S) \ R\ + shows \R\ by (assumption | rule conjI impI major [THEN mp] r)+ lemma disj_impE: - assumes major: "(P \ Q) \ S" - and r: "\P \ S; Q \ S\ \ R" - shows R + assumes major: \(P \ Q) \ S\ + and r: \\P \ S; Q \ S\ \ R\ + shows \R\ by (assumption | rule disjI1 disjI2 impI major [THEN mp] r)+ text \Simplifies the implication. Classical version is stronger. Still UNSAFE since Q must be provable -- backtracking needed.\ lemma imp_impE: - assumes major: "(P \ Q) \ S" - and r1: "\P; Q \ S\ \ Q" - and r2: "S \ R" - shows R + assumes major: \(P \ Q) \ S\ + and r1: \\P; Q \ S\ \ Q\ + and r2: \S \ R\ + shows \R\ by (assumption | rule impI major [THEN mp] r1 r2)+ text \Simplifies the implication. Classical version is stronger. Still UNSAFE since ~P must be provable -- backtracking needed.\ -lemma not_impE: "\ P \ S \ (P \ False) \ (S \ R) \ R" +lemma not_impE: \\ P \ S \ (P \ False) \ (S \ R) \ R\ apply (drule mp) apply (rule notI) apply assumption @@ -538,21 +538,21 @@ text \Simplifies the implication. UNSAFE.\ lemma iff_impE: - assumes major: "(P \ Q) \ S" - and r1: "\P; Q \ S\ \ Q" - and r2: "\Q; P \ S\ \ P" - and r3: "S \ R" - shows R + assumes major: \(P \ Q) \ S\ + and r1: \\P; Q \ S\ \ Q\ + and r2: \\Q; P \ S\ \ P\ + and r3: \S \ R\ + shows \R\ apply (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+ done text \What if \(\x. \ \ P(x)) \ \ \ (\x. P(x))\ is an assumption? UNSAFE.\ lemma all_impE: - assumes major: "(\x. P(x)) \ S" - and r1: "\x. P(x)" - and r2: "S \ R" - shows R + assumes major: \(\x. P(x)) \ S\ + and r1: \\x. P(x)\ + and r2: \S \ R\ + shows \R\ apply (rule allI impI major [THEN mp] r1 r2)+ done @@ -560,14 +560,14 @@ Unsafe: \\x. P(x)) \ S\ is equivalent to \\x. P(x) \ S\.\ lemma ex_impE: - assumes major: "(\x. P(x)) \ S" - and r: "P(x) \ S \ R" - shows R + assumes major: \(\x. P(x)) \ S\ + and r: \P(x) \ S \ R\ + shows \R\ apply (assumption | rule exI impI major [THEN mp] r)+ done text \Courtesy of Krzysztof Grabczewski.\ -lemma disj_imp_disj: "P \ Q \ (P \ R) \ (Q \ S) \ R \ S" +lemma disj_imp_disj: \P \ Q \ (P \ R) \ (Q \ S) \ R \ S\ apply (erule disjE) apply (rule disjI1) apply assumption apply (rule disjI2) apply assumption @@ -584,7 +584,7 @@ ML_file "fologic.ML" -lemma thin_refl: "\x = x; PROP W\ \ PROP W" . +lemma thin_refl: \\x = x; PROP W\ \ PROP W\ . ML \ structure Hypsubst = Hypsubst @@ -611,32 +611,32 @@ setup \Intuitionistic.method_setup @{binding iprover}\ lemma impE': - assumes 1: "P \ Q" - and 2: "Q \ R" - and 3: "P \ Q \ P" - shows R + assumes 1: \P \ Q\ + and 2: \Q \ R\ + and 3: \P \ Q \ P\ + shows \R\ proof - - from 3 and 1 have P . - with 1 have Q by (rule impE) - with 2 show R . + from 3 and 1 have \P\ . + with 1 have \Q\ by (rule impE) + with 2 show \R\ . qed lemma allE': - assumes 1: "\x. P(x)" - and 2: "P(x) \ \x. P(x) \ Q" - shows Q + assumes 1: \\x. P(x)\ + and 2: \P(x) \ \x. P(x) \ Q\ + shows \Q\ proof - - from 1 have "P(x)" by (rule spec) - from this and 1 show Q by (rule 2) + from 1 have \P(x)\ by (rule spec) + from this and 1 show \Q\ by (rule 2) qed lemma notE': - assumes 1: "\ P" - and 2: "\ P \ P" - shows R + assumes 1: \\ P\ + and 2: \\ P \ P\ + shows \R\ proof - - from 2 and 1 have P . - with 1 show R by (rule notE) + from 2 and 1 have \P\ . + with 1 show \R\ by (rule notE) qed lemmas [Pure.elim!] = disjE iffE FalseE conjE exE @@ -650,14 +650,14 @@ \ -lemma iff_not_sym: "\ (Q \ P) \ \ (P \ Q)" +lemma iff_not_sym: \\ (Q \ P) \ \ (P \ Q)\ by iprover lemmas [sym] = sym iff_sym not_sym iff_not_sym and [Pure.elim?] = iffD1 iffD2 impE -lemma eq_commute: "a = b \ b = a" +lemma eq_commute: \a = b \ b = a\ apply (rule iffI) apply (erule sym)+ done @@ -665,56 +665,56 @@ subsection \Atomizing meta-level rules\ -lemma atomize_all [atomize]: "(\x. P(x)) \ Trueprop (\x. P(x))" +lemma atomize_all [atomize]: \(\x. P(x)) \ Trueprop (\x. P(x))\ proof - assume "\x. P(x)" - then show "\x. P(x)" .. + assume \\x. P(x)\ + then show \\x. P(x)\ .. next - assume "\x. P(x)" - then show "\x. P(x)" .. + assume \\x. P(x)\ + then show \\x. P(x)\ .. qed -lemma atomize_imp [atomize]: "(A \ B) \ Trueprop (A \ B)" +lemma atomize_imp [atomize]: \(A \ B) \ Trueprop (A \ B)\ proof - assume "A \ B" - then show "A \ B" .. + assume \A \ B\ + then show \A \ B\ .. next - assume "A \ B" and A - then show B by (rule mp) + assume \A \ B\ and \A\ + then show \B\ by (rule mp) qed -lemma atomize_eq [atomize]: "(x \ y) \ Trueprop (x = y)" +lemma atomize_eq [atomize]: \(x \ y) \ Trueprop (x = y)\ proof - assume "x \ y" - show "x = y" unfolding \x \ y\ by (rule refl) + assume \x \ y\ + show \x = y\ unfolding \x \ y\ by (rule refl) next - assume "x = y" - then show "x \ y" by (rule eq_reflection) + assume \x = y\ + then show \x \ y\ by (rule eq_reflection) qed -lemma atomize_iff [atomize]: "(A \ B) \ Trueprop (A \ B)" +lemma atomize_iff [atomize]: \(A \ B) \ Trueprop (A \ B)\ proof - assume "A \ B" - show "A \ B" unfolding \A \ B\ by (rule iff_refl) + assume \A \ B\ + show \A \ B\ unfolding \A \ B\ by (rule iff_refl) next - assume "A \ B" - then show "A \ B" by (rule iff_reflection) + assume \A \ B\ + then show \A \ B\ by (rule iff_reflection) qed -lemma atomize_conj [atomize]: "(A &&& B) \ Trueprop (A \ B)" +lemma atomize_conj [atomize]: \(A &&& B) \ Trueprop (A \ B)\ proof - assume conj: "A &&& B" - show "A \ B" + assume conj: \A &&& B\ + show \A \ B\ proof (rule conjI) - from conj show A by (rule conjunctionD1) - from conj show B by (rule conjunctionD2) + from conj show \A\ by (rule conjunctionD1) + from conj show \B\ by (rule conjunctionD2) qed next - assume conj: "A \ B" - show "A &&& B" + assume conj: \A \ B\ + show \A &&& B\ proof - - from conj show A .. - from conj show B .. + from conj show \A\ .. + from conj show \B\ .. qed qed @@ -724,24 +724,24 @@ subsection \Atomizing elimination rules\ -lemma atomize_exL[atomize_elim]: "(\x. P(x) \ Q) \ ((\x. P(x)) \ Q)" +lemma atomize_exL[atomize_elim]: \(\x. P(x) \ Q) \ ((\x. P(x)) \ Q)\ by rule iprover+ -lemma atomize_conjL[atomize_elim]: "(A \ B \ C) \ (A \ B \ C)" +lemma atomize_conjL[atomize_elim]: \(A \ B \ C) \ (A \ B \ C)\ by rule iprover+ -lemma atomize_disjL[atomize_elim]: "((A \ C) \ (B \ C) \ C) \ ((A \ B \ C) \ C)" +lemma atomize_disjL[atomize_elim]: \((A \ C) \ (B \ C) \ C) \ ((A \ B \ C) \ C)\ by rule iprover+ -lemma atomize_elimL[atomize_elim]: "(\B. (A \ B) \ B) \ Trueprop(A)" .. +lemma atomize_elimL[atomize_elim]: \(\B. (A \ B) \ B) \ Trueprop(A)\ .. subsection \Calculational rules\ -lemma forw_subst: "a = b \ P(b) \ P(a)" +lemma forw_subst: \a = b \ P(b) \ P(a)\ by (rule ssubst) -lemma back_subst: "P(a) \ a = b \ P(b)" +lemma back_subst: \P(a) \ a = b \ P(b)\ by (rule subst) text \ @@ -760,22 +760,22 @@ nonterminal letbinds and letbind -definition Let :: "['a::{}, 'a => 'b] \ ('b::{})" - where "Let(s, f) \ f(s)" +definition Let :: \['a::{}, 'a => 'b] \ ('b::{})\ + where \Let(s, f) \ f(s)\ syntax - "_bind" :: "[pttrn, 'a] => letbind" (\(2_ =/ _)\ 10) - "" :: "letbind => letbinds" (\_\) - "_binds" :: "[letbind, letbinds] => letbinds" (\_;/ _\) - "_Let" :: "[letbinds, 'a] => 'a" (\(let (_)/ in (_))\ 10) + "_bind" :: \[pttrn, 'a] => letbind\ (\(2_ =/ _)\ 10) + "" :: \letbind => letbinds\ (\_\) + "_binds" :: \[letbind, letbinds] => letbinds\ (\_;/ _\) + "_Let" :: \[letbinds, 'a] => 'a\ (\(let (_)/ in (_))\ 10) translations "_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))" "let x = a in e" == "CONST Let(a, \x. e)" lemma LetI: - assumes "\x. x = t \ P(u(x))" - shows "P(let x = t in u(x))" + assumes \\x. x = t \ P(u(x))\ + shows \P(let x = t in u(x))\ apply (unfold Let_def) apply (rule refl [THEN assms]) done @@ -784,113 +784,113 @@ subsection \Intuitionistic simplification rules\ lemma conj_simps: - "P \ True \ P" - "True \ P \ P" - "P \ False \ False" - "False \ P \ False" - "P \ P \ P" - "P \ P \ Q \ P \ Q" - "P \ \ P \ False" - "\ P \ P \ False" - "(P \ Q) \ R \ P \ (Q \ R)" + \P \ True \ P\ + \True \ P \ P\ + \P \ False \ False\ + \False \ P \ False\ + \P \ P \ P\ + \P \ P \ Q \ P \ Q\ + \P \ \ P \ False\ + \\ P \ P \ False\ + \(P \ Q) \ R \ P \ (Q \ R)\ by iprover+ lemma disj_simps: - "P \ True \ True" - "True \ P \ True" - "P \ False \ P" - "False \ P \ P" - "P \ P \ P" - "P \ P \ Q \ P \ Q" - "(P \ Q) \ R \ P \ (Q \ R)" + \P \ True \ True\ + \True \ P \ True\ + \P \ False \ P\ + \False \ P \ P\ + \P \ P \ P\ + \P \ P \ Q \ P \ Q\ + \(P \ Q) \ R \ P \ (Q \ R)\ by iprover+ lemma not_simps: - "\ (P \ Q) \ \ P \ \ Q" - "\ False \ True" - "\ True \ False" + \\ (P \ Q) \ \ P \ \ Q\ + \\ False \ True\ + \\ True \ False\ by iprover+ lemma imp_simps: - "(P \ False) \ \ P" - "(P \ True) \ True" - "(False \ P) \ True" - "(True \ P) \ P" - "(P \ P) \ True" - "(P \ \ P) \ \ P" + \(P \ False) \ \ P\ + \(P \ True) \ True\ + \(False \ P) \ True\ + \(True \ P) \ P\ + \(P \ P) \ True\ + \(P \ \ P) \ \ P\ by iprover+ lemma iff_simps: - "(True \ P) \ P" - "(P \ True) \ P" - "(P \ P) \ True" - "(False \ P) \ \ P" - "(P \ False) \ \ P" + \(True \ P) \ P\ + \(P \ True) \ P\ + \(P \ P) \ True\ + \(False \ P) \ \ P\ + \(P \ False) \ \ P\ by iprover+ text \The \x = t\ versions are needed for the simplification procedures.\ lemma quant_simps: - "\P. (\x. P) \ P" - "(\x. x = t \ P(x)) \ P(t)" - "(\x. t = x \ P(x)) \ P(t)" - "\P. (\x. P) \ P" - "\x. x = t" - "\x. t = x" - "(\x. x = t \ P(x)) \ P(t)" - "(\x. t = x \ P(x)) \ P(t)" + \\P. (\x. P) \ P\ + \(\x. x = t \ P(x)) \ P(t)\ + \(\x. t = x \ P(x)) \ P(t)\ + \\P. (\x. P) \ P\ + \\x. x = t\ + \\x. t = x\ + \(\x. x = t \ P(x)) \ P(t)\ + \(\x. t = x \ P(x)) \ P(t)\ by iprover+ text \These are NOT supplied by default!\ lemma distrib_simps: - "P \ (Q \ R) \ P \ Q \ P \ R" - "(Q \ R) \ P \ Q \ P \ R \ P" - "(P \ Q \ R) \ (P \ R) \ (Q \ R)" + \P \ (Q \ R) \ P \ Q \ P \ R\ + \(Q \ R) \ P \ Q \ P \ R \ P\ + \(P \ Q \ R) \ (P \ R) \ (Q \ R)\ by iprover+ subsubsection \Conversion into rewrite rules\ -lemma P_iff_F: "\ P \ (P \ False)" +lemma P_iff_F: \\ P \ (P \ False)\ by iprover -lemma iff_reflection_F: "\ P \ (P \ False)" +lemma iff_reflection_F: \\ P \ (P \ False)\ by (rule P_iff_F [THEN iff_reflection]) -lemma P_iff_T: "P \ (P \ True)" +lemma P_iff_T: \P \ (P \ True)\ by iprover -lemma iff_reflection_T: "P \ (P \ True)" +lemma iff_reflection_T: \P \ (P \ True)\ by (rule P_iff_T [THEN iff_reflection]) subsubsection \More rewrite rules\ -lemma conj_commute: "P \ Q \ Q \ P" by iprover -lemma conj_left_commute: "P \ (Q \ R) \ Q \ (P \ R)" by iprover +lemma conj_commute: \P \ Q \ Q \ P\ by iprover +lemma conj_left_commute: \P \ (Q \ R) \ Q \ (P \ R)\ by iprover lemmas conj_comms = conj_commute conj_left_commute -lemma disj_commute: "P \ Q \ Q \ P" by iprover -lemma disj_left_commute: "P \ (Q \ R) \ Q \ (P \ R)" by iprover +lemma disj_commute: \P \ Q \ Q \ P\ by iprover +lemma disj_left_commute: \P \ (Q \ R) \ Q \ (P \ R)\ by iprover lemmas disj_comms = disj_commute disj_left_commute -lemma conj_disj_distribL: "P \ (Q \ R) \ (P \ Q \ P \ R)" by iprover -lemma conj_disj_distribR: "(P \ Q) \ R \ (P \ R \ Q \ R)" by iprover +lemma conj_disj_distribL: \P \ (Q \ R) \ (P \ Q \ P \ R)\ by iprover +lemma conj_disj_distribR: \(P \ Q) \ R \ (P \ R \ Q \ R)\ by iprover -lemma disj_conj_distribL: "P \ (Q \ R) \ (P \ Q) \ (P \ R)" by iprover -lemma disj_conj_distribR: "(P \ Q) \ R \ (P \ R) \ (Q \ R)" by iprover +lemma disj_conj_distribL: \P \ (Q \ R) \ (P \ Q) \ (P \ R)\ by iprover +lemma disj_conj_distribR: \(P \ Q) \ R \ (P \ R) \ (Q \ R)\ by iprover -lemma imp_conj_distrib: "(P \ (Q \ R)) \ (P \ Q) \ (P \ R)" by iprover -lemma imp_conj: "((P \ Q) \ R) \ (P \ (Q \ R))" by iprover -lemma imp_disj: "(P \ Q \ R) \ (P \ R) \ (Q \ R)" by iprover +lemma imp_conj_distrib: \(P \ (Q \ R)) \ (P \ Q) \ (P \ R)\ by iprover +lemma imp_conj: \((P \ Q) \ R) \ (P \ (Q \ R))\ by iprover +lemma imp_disj: \(P \ Q \ R) \ (P \ R) \ (Q \ R)\ by iprover -lemma de_Morgan_disj: "(\ (P \ Q)) \ (\ P \ \ Q)" by iprover +lemma de_Morgan_disj: \(\ (P \ Q)) \ (\ P \ \ Q)\ by iprover -lemma not_ex: "(\ (\x. P(x))) \ (\x. \ P(x))" by iprover -lemma imp_ex: "((\x. P(x)) \ Q) \ (\x. P(x) \ Q)" by iprover +lemma not_ex: \(\ (\x. P(x))) \ (\x. \ P(x))\ by iprover +lemma imp_ex: \((\x. P(x)) \ Q) \ (\x. P(x) \ Q)\ by iprover -lemma ex_disj_distrib: "(\x. P(x) \ Q(x)) \ ((\x. P(x)) \ (\x. Q(x)))" +lemma ex_disj_distrib: \(\x. P(x) \ Q(x)) \ ((\x. P(x)) \ (\x. Q(x)))\ by iprover -lemma all_conj_distrib: "(\x. P(x) \ Q(x)) \ ((\x. P(x)) \ (\x. Q(x)))" +lemma all_conj_distrib: \(\x. P(x) \ Q(x)) \ ((\x. P(x)) \ (\x. Q(x)))\ by iprover end diff -r e15f053a42d8 -r e65314985426 src/FOL/ex/Classical.thy --- a/src/FOL/ex/Classical.thy Thu Jan 03 21:48:05 2019 +0100 +++ b/src/FOL/ex/Classical.thy Thu Jan 03 22:19:19 2019 +0100 @@ -9,16 +9,16 @@ imports FOL begin -lemma "(P \ Q \ R) \ (P \ Q) \ (P \ R)" +lemma \(P \ Q \ R) \ (P \ Q) \ (P \ R)\ by blast subsubsection \If and only if\ -lemma "(P \ Q) \ (Q \ P)" +lemma \(P \ Q) \ (Q \ P)\ by blast -lemma "\ (P \ \ P)" +lemma \\ (P \ \ P)\ by blast @@ -37,91 +37,91 @@ \ text\1\ -lemma "(P \ Q) \ (\ Q \ \ P)" +lemma \(P \ Q) \ (\ Q \ \ P)\ by blast text\2\ -lemma "\ \ P \ P" +lemma \\ \ P \ P\ by blast text\3\ -lemma "\ (P \ Q) \ (Q \ P)" +lemma \\ (P \ Q) \ (Q \ P)\ by blast text\4\ -lemma "(\ P \ Q) \ (\ Q \ P)" +lemma \(\ P \ Q) \ (\ Q \ P)\ by blast text\5\ -lemma "((P \ Q) \ (P \ R)) \ (P \ (Q \ R))" +lemma \((P \ Q) \ (P \ R)) \ (P \ (Q \ R))\ by blast text\6\ -lemma "P \ \ P" +lemma \P \ \ P\ by blast text\7\ -lemma "P \ \ \ \ P" +lemma \P \ \ \ \ P\ by blast text\8. Peirce's law\ -lemma "((P \ Q) \ P) \ P" +lemma \((P \ Q) \ P) \ P\ by blast text\9\ -lemma "((P \ Q) \ (\ P \ Q) \ (P \ \ Q)) \ \ (\ P \ \ Q)" +lemma \((P \ Q) \ (\ P \ Q) \ (P \ \ Q)) \ \ (\ P \ \ Q)\ by blast text\10\ -lemma "(Q \ R) \ (R \ P \ Q) \ (P \ Q \ R) \ (P \ Q)" +lemma \(Q \ R) \ (R \ P \ Q) \ (P \ Q \ R) \ (P \ Q)\ by blast text\11. Proved in each direction (incorrectly, says Pelletier!!)\ -lemma "P \ P" +lemma \P \ P\ by blast text\12. "Dijkstra's law"\ -lemma "((P \ Q) \ R) \ (P \ (Q \ R))" +lemma \((P \ Q) \ R) \ (P \ (Q \ R))\ by blast text\13. Distributive law\ -lemma "P \ (Q \ R) \ (P \ Q) \ (P \ R)" +lemma \P \ (Q \ R) \ (P \ Q) \ (P \ R)\ by blast text\14\ -lemma "(P \ Q) \ ((Q \ \ P) \ (\ Q \ P))" +lemma \(P \ Q) \ ((Q \ \ P) \ (\ Q \ P))\ by blast text\15\ -lemma "(P \ Q) \ (\ P \ Q)" +lemma \(P \ Q) \ (\ P \ Q)\ by blast text\16\ -lemma "(P \ Q) \ (Q \ P)" +lemma \(P \ Q) \ (Q \ P)\ by blast text\17\ -lemma "((P \ (Q \ R)) \ S) \ ((\ P \ Q \ S) \ (\ P \ \ R \ S))" +lemma \((P \ (Q \ R)) \ S) \ ((\ P \ Q \ S) \ (\ P \ \ R \ S))\ by blast subsection \Classical Logic: examples with quantifiers\ -lemma "(\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))" +lemma \(\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))\ by blast -lemma "(\x. P \ Q(x)) \ (P \ (\x. Q(x)))" +lemma \(\x. P \ Q(x)) \ (P \ (\x. Q(x)))\ by blast -lemma "(\x. P(x) \ Q) \ (\x. P(x)) \ Q" +lemma \(\x. P(x) \ Q) \ (\x. P(x)) \ Q\ by blast -lemma "(\x. P(x)) \ Q \ (\x. P(x) \ Q)" +lemma \(\x. P(x)) \ Q \ (\x. P(x) \ Q)\ by blast text\Discussed in Avron, Gentzen-Type Systems, Resolution and Tableaux, JAR 10 (265-281), 1993. Proof is trivial!\ -lemma "\ ((\x. \ P(x)) \ ((\x. P(x)) \ (\x. P(x) \ Q(x))) \ \ (\x. P(x)))" +lemma \\ ((\x. \ P(x)) \ ((\x. P(x)) \ (\x. P(x) \ Q(x))) \ \ (\x. P(x)))\ by blast @@ -129,195 +129,195 @@ text\Theorem B of Peter Andrews, Theorem Proving via General Matings, JACM 28 (1981).\ -lemma "(\x. \y. P(x) \ P(y)) \ ((\x. P(x)) \ (\y. P(y)))" +lemma \(\x. \y. P(x) \ P(y)) \ ((\x. P(x)) \ (\y. P(y)))\ by blast text\Needs multiple instantiation of ALL.\ -lemma "(\x. P(x) \ P(f(x))) \ P(d) \ P(f(f(f(d))))" +lemma \(\x. P(x) \ P(f(x))) \ P(d) \ P(f(f(f(d))))\ by blast text\Needs double instantiation of the quantifier\ -lemma "\x. P(x) \ P(a) \ P(b)" +lemma \\x. P(x) \ P(a) \ P(b)\ by blast -lemma "\z. P(z) \ (\x. P(x))" +lemma \\z. P(z) \ (\x. P(x))\ by blast -lemma "\x. (\y. P(y)) \ P(x)" +lemma \\x. (\y. P(y)) \ P(x)\ by blast text\V. Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 1--23. NOT PROVED.\ lemma - "\x x'. \y. \z z'. + \\x x'. \y. \z z'. (\ P(y,y) \ P(x,x) \ \ S(z,x)) \ (S(x,y) \ \ S(y,z) \ Q(z',z')) \ - (Q(x',y) \ \ Q(y,z') \ S(x',x'))" + (Q(x',y) \ \ Q(y,z') \ S(x',x'))\ oops subsection \Hard examples with quantifiers\ text\18\ -lemma "\y. \x. P(y) \ P(x)" +lemma \\y. \x. P(y) \ P(x)\ by blast text\19\ -lemma "\x. \y z. (P(y) \ Q(z)) \ (P(x) \ Q(x))" +lemma \\x. \y z. (P(y) \ Q(z)) \ (P(x) \ Q(x))\ by blast text\20\ -lemma "(\x y. \z. \w. (P(x) \ Q(y) \ R(z) \ S(w))) - \ (\x y. P(x) \ Q(y)) \ (\z. R(z))" +lemma \(\x y. \z. \w. (P(x) \ Q(y) \ R(z) \ S(w))) + \ (\x y. P(x) \ Q(y)) \ (\z. R(z))\ by blast text\21\ -lemma "(\x. P \ Q(x)) \ (\x. Q(x) \ P) \ (\x. P \ Q(x))" +lemma \(\x. P \ Q(x)) \ (\x. Q(x) \ P) \ (\x. P \ Q(x))\ by blast text\22\ -lemma "(\x. P \ Q(x)) \ (P \ (\x. Q(x)))" +lemma \(\x. P \ Q(x)) \ (P \ (\x. Q(x)))\ by blast text\23\ -lemma "(\x. P \ Q(x)) \ (P \ (\x. Q(x)))" +lemma \(\x. P \ Q(x)) \ (P \ (\x. Q(x)))\ by blast text\24\ lemma - "\ (\x. S(x) \ Q(x)) \ (\x. P(x) \ Q(x) \ R(x)) \ + \\ (\x. S(x) \ Q(x)) \ (\x. P(x) \ Q(x) \ R(x)) \ (\ (\x. P(x)) \ (\x. Q(x))) \ (\x. Q(x) \ R(x) \ S(x)) - \ (\x. P(x) \ R(x))" + \ (\x. P(x) \ R(x))\ by blast text\25\ lemma - "(\x. P(x)) \ + \(\x. P(x)) \ (\x. L(x) \ \ (M(x) \ R(x))) \ (\x. P(x) \ (M(x) \ L(x))) \ ((\x. P(x) \ Q(x)) \ (\x. P(x) \ R(x))) - \ (\x. Q(x) \ P(x))" + \ (\x. Q(x) \ P(x))\ by blast text\26\ lemma - "((\x. p(x)) \ (\x. q(x))) \ + \((\x. p(x)) \ (\x. q(x))) \ (\x. \y. p(x) \ q(y) \ (r(x) \ s(y))) - \ ((\x. p(x) \ r(x)) \ (\x. q(x) \ s(x)))" + \ ((\x. p(x) \ r(x)) \ (\x. q(x) \ s(x)))\ by blast text\27\ lemma - "(\x. P(x) \ \ Q(x)) \ + \(\x. P(x) \ \ Q(x)) \ (\x. P(x) \ R(x)) \ (\x. M(x) \ L(x) \ P(x)) \ ((\x. R(x) \ \ Q(x)) \ (\x. L(x) \ \ R(x))) - \ (\x. M(x) \ \ L(x))" + \ (\x. M(x) \ \ L(x))\ by blast text\28. AMENDED\ lemma - "(\x. P(x) \ (\x. Q(x))) \ + \(\x. P(x) \ (\x. Q(x))) \ ((\x. Q(x) \ R(x)) \ (\x. Q(x) \ S(x))) \ ((\x. S(x)) \ (\x. L(x) \ M(x))) - \ (\x. P(x) \ L(x) \ M(x))" + \ (\x. P(x) \ L(x) \ M(x))\ by blast text\29. Essentially the same as Principia Mathematica *11.71\ lemma - "(\x. P(x)) \ (\y. Q(y)) + \(\x. P(x)) \ (\y. Q(y)) \ ((\x. P(x) \ R(x)) \ (\y. Q(y) \ S(y)) \ - (\x y. P(x) \ Q(y) \ R(x) \ S(y)))" + (\x y. P(x) \ Q(y) \ R(x) \ S(y)))\ by blast text\30\ lemma - "(\x. P(x) \ Q(x) \ \ R(x)) \ + \(\x. P(x) \ Q(x) \ \ R(x)) \ (\x. (Q(x) \ \ S(x)) \ P(x) \ R(x)) - \ (\x. S(x))" + \ (\x. S(x))\ by blast text\31\ lemma - "\ (\x. P(x) \ (Q(x) \ R(x))) \ + \\ (\x. P(x) \ (Q(x) \ R(x))) \ (\x. L(x) \ P(x)) \ (\x. \ R(x) \ M(x)) - \ (\x. L(x) \ M(x))" + \ (\x. L(x) \ M(x))\ by blast text\32\ lemma - "(\x. P(x) \ (Q(x) \ R(x)) \ S(x)) \ + \(\x. P(x) \ (Q(x) \ R(x)) \ S(x)) \ (\x. S(x) \ R(x) \ L(x)) \ (\x. M(x) \ R(x)) - \ (\x. P(x) \ M(x) \ L(x))" + \ (\x. P(x) \ M(x) \ L(x))\ by blast text\33\ lemma - "(\x. P(a) \ (P(x) \ P(b)) \ P(c)) \ - (\x. (\ P(a) \ P(x) \ P(c)) \ (\ P(a) \ \ P(b) \ P(c)))" + \(\x. P(a) \ (P(x) \ P(b)) \ P(c)) \ + (\x. (\ P(a) \ P(x) \ P(c)) \ (\ P(a) \ \ P(b) \ P(c)))\ by blast text\34. AMENDED (TWICE!!). Andrews's challenge.\ lemma - "((\x. \y. p(x) \ p(y)) \ ((\x. q(x)) \ (\y. p(y)))) \ - ((\x. \y. q(x) \ q(y)) \ ((\x. p(x)) \ (\y. q(y))))" + \((\x. \y. p(x) \ p(y)) \ ((\x. q(x)) \ (\y. p(y)))) \ + ((\x. \y. q(x) \ q(y)) \ ((\x. p(x)) \ (\y. q(y))))\ by blast text\35\ -lemma "\x y. P(x,y) \ (\u v. P(u,v))" +lemma \\x y. P(x,y) \ (\u v. P(u,v))\ by blast text\36\ lemma - "(\x. \y. J(x,y)) \ + \(\x. \y. J(x,y)) \ (\x. \y. G(x,y)) \ (\x y. J(x,y) \ G(x,y) \ (\z. J(y,z) \ G(y,z) \ H(x,z))) - \ (\x. \y. H(x,y))" + \ (\x. \y. H(x,y))\ by blast text\37\ lemma - "(\z. \w. \x. \y. + \(\z. \w. \x. \y. (P(x,z) \ P(y,w)) \ P(y,z) \ (P(y,w) \ (\u. Q(u,w)))) \ (\x z. \ P(x,z) \ (\y. Q(y,z))) \ ((\x y. Q(x,y)) \ (\x. R(x,x))) - \ (\x. \y. R(x,y))" + \ (\x. \y. R(x,y))\ by blast text\38\ lemma - "(\x. p(a) \ (p(x) \ (\y. p(y) \ r(x,y))) \ + \(\x. p(a) \ (p(x) \ (\y. p(y) \ r(x,y))) \ (\z. \w. p(z) \ r(x,w) \ r(w,z))) \ (\x. (\ p(a) \ p(x) \ (\z. \w. p(z) \ r(x,w) \ r(w,z))) \ (\ p(a) \ \ (\y. p(y) \ r(x,y)) \ - (\z. \w. p(z) \ r(x,w) \ r(w,z))))" + (\z. \w. p(z) \ r(x,w) \ r(w,z))))\ by blast text\39\ -lemma "\ (\x. \y. F(y,x) \ \ F(y,y))" +lemma \\ (\x. \y. F(y,x) \ \ F(y,y))\ by blast text\40. AMENDED\ lemma - "(\y. \x. F(x,y) \ F(x,x)) \ - \ (\x. \y. \z. F(z,y) \ \ F(z,x))" + \(\y. \x. F(x,y) \ F(x,x)) \ + \ (\x. \y. \z. F(z,y) \ \ F(z,x))\ by blast text\41\ lemma - "(\z. \y. \x. f(x,y) \ f(x,z) \ \ f(x,x)) - \ \ (\z. \x. f(x,z))" + \(\z. \y. \x. f(x,y) \ f(x,z) \ \ f(x,x)) + \ \ (\z. \x. f(x,z))\ by blast text\42\ -lemma "\ (\y. \x. p(x,y) \ \ (\z. p(x,z) \ p(z,x)))" +lemma \\ (\y. \x. p(x,y) \ \ (\z. p(x,z) \ p(z,x)))\ by blast text\43\ lemma - "(\x. \y. q(x,y) \ (\z. p(z,x) \ p(z,y))) - \ (\x. \y. q(x,y) \ q(y,x))" + \(\x. \y. q(x,y) \ (\z. p(z,x) \ p(z,y))) + \ (\x. \y. q(x,y) \ q(y,x))\ by blast text \ @@ -328,69 +328,69 @@ text\44\ lemma - "(\x. f(x) \ (\y. g(y) \ h(x,y) \ (\y. g(y) \ \ h(x,y)))) \ + \(\x. f(x) \ (\y. g(y) \ h(x,y) \ (\y. g(y) \ \ h(x,y)))) \ (\x. j(x) \ (\y. g(y) \ h(x,y))) - \ (\x. j(x) \ \ f(x))" + \ (\x. j(x) \ \ f(x))\ by blast text\45\ lemma - "(\x. f(x) \ (\y. g(y) \ h(x,y) \ j(x,y)) + \(\x. f(x) \ (\y. g(y) \ h(x,y) \ j(x,y)) \ (\y. g(y) \ h(x,y) \ k(y))) \ \ (\y. l(y) \ k(y)) \ (\x. f(x) \ (\y. h(x,y) \ l(y)) \ (\y. g(y) \ h(x,y) \ j(x,y))) - \ (\x. f(x) \ \ (\y. g(y) \ h(x,y)))" + \ (\x. f(x) \ \ (\y. g(y) \ h(x,y)))\ by blast text\46\ lemma - "(\x. f(x) \ (\y. f(y) \ h(y,x) \ g(y)) \ g(x)) \ + \(\x. f(x) \ (\y. f(y) \ h(y,x) \ g(y)) \ g(x)) \ ((\x. f(x) \ \ g(x)) \ (\x. f(x) \ \ g(x) \ (\y. f(y) \ \ g(y) \ j(x,y)))) \ (\x y. f(x) \ f(y) \ h(x,y) \ \ j(y,x)) - \ (\x. f(x) \ g(x))" + \ (\x. f(x) \ g(x))\ by blast subsection \Problems (mainly) involving equality or functions\ text\48\ -lemma "(a = b \ c = d) \ (a = c \ b = d) \ a = d \ b = c" +lemma \(a = b \ c = d) \ (a = c \ b = d) \ a = d \ b = c\ by blast text\49. NOT PROVED AUTOMATICALLY. Hard because it involves substitution for Vars; the type constraint ensures that x,y,z have the same type as a,b,u.\ lemma - "(\x y::'a. \z. z = x \ z = y) \ P(a) \ P(b) \ a \ b \ (\u::'a. P(u))" + \(\x y::'a. \z. z = x \ z = y) \ P(a) \ P(b) \ a \ b \ (\u::'a. P(u))\ apply safe - apply (rule_tac x = a in allE, assumption) - apply (rule_tac x = b in allE, assumption) + apply (rule_tac x = \a\ in allE, assumption) + apply (rule_tac x = \b\ in allE, assumption) apply fast \ \blast's treatment of equality can't do it\ done text\50. (What has this to do with equality?)\ -lemma "(\x. P(a,x) \ (\y. P(x,y))) \ (\x. \y. P(x,y))" +lemma \(\x. P(a,x) \ (\y. P(x,y))) \ (\x. \y. P(x,y))\ by blast text\51\ lemma - "(\z w. \x y. P(x,y) \ (x = z \ y = w)) \ - (\z. \x. \w. (\y. P(x,y) \ y=w) \ x = z)" + \(\z w. \x y. P(x,y) \ (x = z \ y = w)) \ + (\z. \x. \w. (\y. P(x,y) \ y=w) \ x = z)\ by blast text\52\ text\Almost the same as 51.\ lemma - "(\z w. \x y. P(x,y) \ (x = z \ y = w)) \ - (\w. \y. \z. (\x. P(x,y) \ x = z) \ y = w)" + \(\z w. \x y. P(x,y) \ (x = z \ y = w)) \ + (\w. \y. \z. (\x. P(x,y) \ x = z) \ y = w)\ by blast text\55\ text\Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988). fast DISCOVERS who killed Agatha.\ schematic_goal - "lives(agatha) \ lives(butler) \ lives(charles) \ + \lives(agatha) \ lives(butler) \ lives(charles) \ (killed(agatha,agatha) \ killed(butler,agatha) \ killed(charles,agatha)) \ (\x y. killed(x,y) \ hates(x,y) \ \ richer(x,y)) \ (\x. hates(agatha,x) \ \ hates(charles,x)) \ @@ -398,60 +398,60 @@ (\x. lives(x) \ \ richer(x,agatha) \ hates(butler,x)) \ (\x. hates(agatha,x) \ hates(butler,x)) \ (\x. \ hates(x,agatha) \ \ hates(x,butler) \ \ hates(x,charles)) \ - killed(?who,agatha)" + killed(?who,agatha)\ by fast \ \MUCH faster than blast\ text\56\ -lemma "(\x. (\y. P(y) \ x = f(y)) \ P(x)) \ (\x. P(x) \ P(f(x)))" +lemma \(\x. (\y. P(y) \ x = f(y)) \ P(x)) \ (\x. P(x) \ P(f(x)))\ by blast text\57\ lemma - "P(f(a,b), f(b,c)) \ P(f(b,c), f(a,c)) \ - (\x y z. P(x,y) \ P(y,z) \ P(x,z)) \ P(f(a,b), f(a,c))" + \P(f(a,b), f(b,c)) \ P(f(b,c), f(a,c)) \ + (\x y z. P(x,y) \ P(y,z) \ P(x,z)) \ P(f(a,b), f(a,c))\ by blast text\58 NOT PROVED AUTOMATICALLY\ -lemma "(\x y. f(x) = g(y)) \ (\x y. f(f(x)) = f(g(y)))" +lemma \(\x y. f(x) = g(y)) \ (\x y. f(f(x)) = f(g(y)))\ by (slow elim: subst_context) text\59\ -lemma "(\x. P(x) \ \ P(f(x))) \ (\x. P(x) \ \ P(f(x)))" +lemma \(\x. P(x) \ \ P(f(x))) \ (\x. P(x) \ \ P(f(x)))\ by blast text\60\ -lemma "\x. P(x,f(x)) \ (\y. (\z. P(z,y) \ P(z,f(x))) \ P(x,y))" +lemma \\x. P(x,f(x)) \ (\y. (\z. P(z,y) \ P(z,f(x))) \ P(x,y))\ by blast text\62 as corrected in JAR 18 (1997), page 135\ lemma - "(\x. p(a) \ (p(x) \ p(f(x))) \ p(f(f(x)))) \ + \(\x. p(a) \ (p(x) \ p(f(x))) \ p(f(f(x)))) \ (\x. (\ p(a) \ p(x) \ p(f(f(x)))) \ - (\ p(a) \ \ p(f(x)) \ p(f(f(x)))))" + (\ p(a) \ \ p(f(x)) \ p(f(f(x)))))\ by blast text \From Davis, Obvious Logical Inferences, IJCAI-81, 530-531 fast indeed copes!\ lemma - "(\x. F(x) \ \ G(x) \ (\y. H(x,y) \ J(y))) \ + \(\x. F(x) \ \ G(x) \ (\y. H(x,y) \ J(y))) \ (\x. K(x) \ F(x) \ (\y. H(x,y) \ K(y))) \ - (\x. K(x) \ \ G(x)) \ (\x. K(x) \ J(x))" + (\x. K(x) \ \ G(x)) \ (\x. K(x) \ J(x))\ by fast text \From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393. It does seem obvious!\ lemma - "(\x. F(x) \ \ G(x) \ (\y. H(x,y) \ J(y))) \ + \(\x. F(x) \ \ G(x) \ (\y. H(x,y) \ J(y))) \ (\x. K(x) \ F(x) \ (\y. H(x,y) \ K(y))) \ - (\x. K(x) \ \ G(x)) \ (\x. K(x) \ \ G(x))" + (\x. K(x) \ \ G(x)) \ (\x. K(x) \ \ G(x))\ by fast text \Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.) author U. Egly.\ lemma - "((\x. A(x) \ (\y. C(y) \ (\z. D(x,y,z)))) \ + \((\x. A(x) \ (\y. C(y) \ (\z. D(x,y,z)))) \ (\w. C(w) \ (\y. C(y) \ (\z. D(w,y,z))))) \ (\w. C(w) \ (\u. C(u) \ (\v. D(w,u,v))) \ @@ -466,7 +466,7 @@ (\v. C(v) \ (\y. ((C(y) \ Q(w,y,y)) \ OO(w,g) \ \ P(v,y)) \ ((C(y) \ Q(w,y,y)) \ OO(w,b) \ P(v,y) \ OO(v,b))))) - \ \ (\x. A(x) \ (\y. C(y) \ (\z. D(x,y,z))))" + \ \ (\x. A(x) \ (\y. C(y) \ (\z. D(x,y,z))))\ by (blast 12) \ \Needed because the search for depths below 12 is very slow.\ @@ -476,7 +476,7 @@ p. 105. \ lemma - "((\x. A(x) \ (\y. C(y) \ (\z. D(x,y,z)))) \ + \((\x. A(x) \ (\y. C(y) \ (\z. D(x,y,z)))) \ (\w. C(w) \ (\y. C(y) \ (\z. D(w,y,z))))) \ (\w. C(w) \ (\u. C(u) \ (\v. D(w,u,v))) \ @@ -495,23 +495,23 @@ \ (\u. C(u) \ (\y. (C(y) \ P(y,y) \ \ P(u,y)) \ (C(y) \ \ P(y,y) \ P(u,y) \ OO(u,b))))) - \ \ (\x. A(x) \ (\y. C(y) \ (\z. D(x,y,z))))" + \ \ (\x. A(x) \ (\y. C(y) \ (\z. D(x,y,z))))\ by blast text \Challenge found on info-hol.\ -lemma "\x. \v w. \y z. P(x) \ Q(y) \ (P(v) \ R(w)) \ (R(z) \ Q(v))" +lemma \\x. \v w. \y z. P(x) \ Q(y) \ (P(v) \ R(w)) \ (R(z) \ Q(v))\ by blast text \ Attributed to Lewis Carroll by S. G. Pulman. The first or last assumption can be deleted.\ lemma - "(\x. honest(x) \ industrious(x) \ healthy(x)) \ + \(\x. honest(x) \ industrious(x) \ healthy(x)) \ \ (\x. grocer(x) \ healthy(x)) \ (\x. industrious(x) \ grocer(x) \ honest(x)) \ (\x. cyclist(x) \ industrious(x)) \ (\x. \ healthy(x) \ cyclist(x) \ \ honest(x)) - \ (\x. grocer(x) \ \ cyclist(x))" + \ (\x. grocer(x) \ \ cyclist(x))\ by blast diff -r e15f053a42d8 -r e65314985426 src/FOL/ex/Foundation.thy --- a/src/FOL/ex/Foundation.thy Thu Jan 03 21:48:05 2019 +0100 +++ b/src/FOL/ex/Foundation.thy Thu Jan 03 22:19:19 2019 +0100 @@ -9,7 +9,7 @@ imports IFOL begin -lemma "A \ B \ (C \ A \ C)" +lemma \A \ B \ (C \ A \ C)\ apply (rule impI) apply (rule impI) apply (rule conjI) @@ -20,9 +20,9 @@ text \A form of conj-elimination\ lemma - assumes "A \ B" - and "A \ B \ C" - shows C + assumes \A \ B\ + and \A \ B \ C\ + shows \C\ apply (rule assms) apply (rule conjunct1) apply (rule assms) @@ -31,26 +31,26 @@ done lemma - assumes "\A. \ \ A \ A" - shows "B \ \ B" + assumes \\A. \ \ A \ A\ + shows \B \ \ B\ apply (rule assms) apply (rule notI) -apply (rule_tac P = "\ B" in notE) +apply (rule_tac P = \\ B\ in notE) apply (rule_tac [2] notI) -apply (rule_tac [2] P = "B \ \ B" in notE) +apply (rule_tac [2] P = \B \ \ B\ in notE) prefer 2 apply assumption apply (rule_tac [2] disjI1) prefer 2 apply assumption apply (rule notI) -apply (rule_tac P = "B \ \ B" in notE) +apply (rule_tac P = \B \ \ B\ in notE) apply assumption apply (rule disjI2) apply assumption done lemma - assumes "\A. \ \ A \ A" - shows "B \ \ B" + assumes \\A. \ \ A \ A\ + shows \B \ \ B\ apply (rule assms) apply (rule notI) apply (rule notE) @@ -64,14 +64,14 @@ lemma - assumes "A \ \ A" - and "\ \ A" - shows A + assumes \A \ \ A\ + and \\ \ A\ + shows \A\ apply (rule disjE) apply (rule assms) apply assumption apply (rule FalseE) -apply (rule_tac P = "\ A" in notE) +apply (rule_tac P = \\ A\ in notE) apply (rule assms) apply assumption done @@ -80,27 +80,27 @@ subsection "Examples with quantifiers" lemma - assumes "\z. G(z)" - shows "\z. G(z) \ H(z)" + assumes \\z. G(z)\ + shows \\z. G(z) \ H(z)\ apply (rule allI) apply (rule disjI1) apply (rule assms [THEN spec]) done -lemma "\x. \y. x = y" +lemma \\x. \y. x = y\ apply (rule allI) apply (rule exI) apply (rule refl) done -lemma "\y. \x. x = y" +lemma \\y. \x. x = y\ apply (rule exI) apply (rule allI) apply (rule refl)? oops text \Parallel lifting example.\ -lemma "\u. \x. \v. \y. \w. P(u,x,v,y,w)" +lemma \\u. \x. \v. \y. \w. P(u,x,v,y,w)\ apply (rule exI allI) apply (rule exI allI) apply (rule exI allI) @@ -109,8 +109,8 @@ oops lemma - assumes "(\z. F(z)) \ B" - shows "\z. F(z) \ B" + assumes \(\z. F(z)) \ B\ + shows \\z. F(z) \ B\ apply (rule conjE) apply (rule assms) apply (rule exE) @@ -122,7 +122,7 @@ done text \A bigger demonstration of quantifiers -- not in the paper.\ -lemma "(\y. \x. Q(x,y)) \ (\x. \y. Q(x,y))" +lemma \(\y. \x. Q(x,y)) \ (\x. \y. Q(x,y))\ apply (rule impI) apply (rule allI) apply (rule exE, assumption) diff -r e15f053a42d8 -r e65314985426 src/FOL/ex/If.thy --- a/src/FOL/ex/If.thy Thu Jan 03 21:48:05 2019 +0100 +++ b/src/FOL/ex/If.thy Thu Jan 03 22:19:19 2019 +0100 @@ -9,16 +9,16 @@ imports FOL begin -definition "if" :: "[o,o,o]=>o" - where "if(P,Q,R) \ P \ Q \ \ P \ R" +definition "if" :: \[o,o,o]=>o\ + where \if(P,Q,R) \ P \ Q \ \ P \ R\ -lemma ifI: "\P \ Q; \ P \ R\ \ if(P,Q,R)" +lemma ifI: \\P \ Q; \ P \ R\ \ if(P,Q,R)\ unfolding if_def by blast -lemma ifE: "\if(P,Q,R); \P; Q\ \ S; \\ P; R\ \ S\ \ S" +lemma ifE: \\if(P,Q,R); \P; Q\ \ S; \\ P; R\ \ S\ \ S\ unfolding if_def by blast -lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) \ if(Q, if(P,A,C), if(P,B,D))" +lemma if_commute: \if(P, if(Q,A,B), if(Q,C,D)) \ if(Q, if(P,A,C), if(P,B,D))\ apply (rule iffI) apply (erule ifE) apply (erule ifE) @@ -30,27 +30,27 @@ declare ifI [intro!] declare ifE [elim!] -lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) \ if(Q, if(P,A,C), if(P,B,D))" +lemma if_commute: \if(P, if(Q,A,B), if(Q,C,D)) \ if(Q, if(P,A,C), if(P,B,D))\ by blast -lemma "if(if(P,Q,R), A, B) \ if(P, if(Q,A,B), if(R,A,B))" +lemma \if(if(P,Q,R), A, B) \ if(P, if(Q,A,B), if(R,A,B))\ by blast text\Trying again from the beginning in order to prove from the definitions\ -lemma "if(if(P,Q,R), A, B) \ if(P, if(Q,A,B), if(R,A,B))" +lemma \if(if(P,Q,R), A, B) \ if(P, if(Q,A,B), if(R,A,B))\ unfolding if_def by blast text \An invalid formula. High-level rules permit a simpler diagnosis.\ -lemma "if(if(P,Q,R), A, B) \ if(P, if(Q,A,B), if(R,B,A))" +lemma \if(if(P,Q,R), A, B) \ if(P, if(Q,A,B), if(R,B,A))\ apply auto \ \The next step will fail unless subgoals remain\ apply (tactic all_tac) oops text \Trying again from the beginning in order to prove from the definitions.\ -lemma "if(if(P,Q,R), A, B) \ if(P, if(Q,A,B), if(R,B,A))" +lemma \if(if(P,Q,R), A, B) \ if(P, if(Q,A,B), if(R,B,A))\ unfolding if_def apply auto \ \The next step will fail unless subgoals remain\ diff -r e15f053a42d8 -r e65314985426 src/FOL/ex/Intro.thy --- a/src/FOL/ex/Intro.thy Thu Jan 03 21:48:05 2019 +0100 +++ b/src/FOL/ex/Intro.thy Thu Jan 03 22:19:19 2019 +0100 @@ -13,7 +13,7 @@ subsubsection \Some simple backward proofs\ -lemma mythm: "P \ P \ P" +lemma mythm: \P \ P \ P\ apply (rule impI) apply (rule disjE) prefer 3 apply (assumption) @@ -21,7 +21,7 @@ apply assumption done -lemma "(P \ Q) \ R \ (P \ R)" +lemma \(P \ Q) \ R \ (P \ R)\ apply (rule impI) apply (erule disjE) apply (drule conjunct1) @@ -31,7 +31,7 @@ done text \Correct version, delaying use of \spec\ until last.\ -lemma "(\x y. P(x,y)) \ (\z w. P(w,z))" +lemma \(\x y. P(x,y)) \ (\z w. P(w,z))\ apply (rule impI) apply (rule allI) apply (rule allI) @@ -43,12 +43,12 @@ subsubsection \Demonstration of \fast\\ -lemma "(\y. \x. J(y,x) \ \ J(x,x)) \ \ (\x. \y. \z. J(z,y) \ \ J(z,x))" +lemma \(\y. \x. J(y,x) \ \ J(x,x)) \ \ (\x. \y. \z. J(z,y) \ \ J(z,x))\ apply fast done -lemma "\x. P(x,f(x)) \ (\y. (\z. P(z,y) \ P(z,f(x))) \ P(x,y))" +lemma \\x. P(x,f(x)) \ (\y. (\z. P(z,y) \ P(z,f(x))) \ P(x,y))\ apply fast done @@ -56,9 +56,9 @@ subsubsection \Derivation of conjunction elimination rule\ lemma - assumes major: "P \ Q" - and minor: "\P; Q\ \ R" - shows R + assumes major: \P \ Q\ + and minor: \\P; Q\ \ R\ + shows \R\ apply (rule minor) apply (rule major [THEN conjunct1]) apply (rule major [THEN conjunct2]) @@ -70,8 +70,8 @@ text \Derivation of negation introduction\ lemma - assumes "P \ False" - shows "\ P" + assumes \P \ False\ + shows \\ P\ apply (unfold not_def) apply (rule impI) apply (rule assms) @@ -79,9 +79,9 @@ done lemma - assumes major: "\ P" - and minor: P - shows R + assumes major: \\ P\ + and minor: \P\ + shows \R\ apply (rule FalseE) apply (rule mp) apply (rule major [unfolded not_def]) @@ -90,9 +90,9 @@ text \Alternative proof of the result above\ lemma - assumes major: "\ P" - and minor: P - shows R + assumes major: \\ P\ + and minor: \P\ + shows \R\ apply (rule minor [THEN major [unfolded not_def, THEN mp, THEN FalseE]]) done diff -r e15f053a42d8 -r e65314985426 src/FOL/ex/Intuitionistic.thy --- a/src/FOL/ex/Intuitionistic.thy Thu Jan 03 21:48:05 2019 +0100 +++ b/src/FOL/ex/Intuitionistic.thy Thu Jan 03 22:19:19 2019 +0100 @@ -36,56 +36,56 @@ intuitionistically provable. Finally, if $P$ is a negation then $\neg\neg P$ is intuitionstically equivalent to $P$. [Andy Pitts]\ -lemma "\ \ (P \ Q) \ \ \ P \ \ \ Q" +lemma \\ \ (P \ Q) \ \ \ P \ \ \ Q\ by (tactic \IntPr.fast_tac @{context} 1\) -lemma "\ \ ((\ P \ Q) \ (\ P \ \ Q) \ P)" +lemma \\ \ ((\ P \ Q) \ (\ P \ \ Q) \ P)\ by (tactic \IntPr.fast_tac @{context} 1\) text \Double-negation does NOT distribute over disjunction.\ -lemma "\ \ (P \ Q) \ (\ \ P \ \ \ Q)" +lemma \\ \ (P \ Q) \ (\ \ P \ \ \ Q)\ by (tactic \IntPr.fast_tac @{context} 1\) -lemma "\ \ \ P \ \ P" +lemma \\ \ \ P \ \ P\ by (tactic \IntPr.fast_tac @{context} 1\) -lemma "\ \ ((P \ Q \ R) \ (P \ Q) \ (P \ R))" +lemma \\ \ ((P \ Q \ R) \ (P \ Q) \ (P \ R))\ by (tactic \IntPr.fast_tac @{context} 1\) -lemma "(P \ Q) \ (Q \ P)" +lemma \(P \ Q) \ (Q \ P)\ by (tactic \IntPr.fast_tac @{context} 1\) -lemma "((P \ (Q \ (Q \ R))) \ R) \ R" +lemma \((P \ (Q \ (Q \ R))) \ R) \ R\ by (tactic \IntPr.fast_tac @{context} 1\) lemma - "(((G \ A) \ J) \ D \ E) \ (((H \ B) \ I) \ C \ J) + \(((G \ A) \ J) \ D \ E) \ (((H \ B) \ I) \ C \ J) \ (A \ H) \ F \ G \ (((C \ B) \ I) \ D) \ (A \ C) - \ (((F \ A) \ B) \ I) \ E" + \ (((F \ A) \ B) \ I) \ E\ by (tactic \IntPr.fast_tac @{context} 1\) subsection \Lemmas for the propositional double-negation translation\ -lemma "P \ \ \ P" +lemma \P \ \ \ P\ by (tactic \IntPr.fast_tac @{context} 1\) -lemma "\ \ (\ \ P \ P)" +lemma \\ \ (\ \ P \ P)\ by (tactic \IntPr.fast_tac @{context} 1\) -lemma "\ \ P \ \ \ (P \ Q) \ \ \ Q" +lemma \\ \ P \ \ \ (P \ Q) \ \ \ Q\ by (tactic \IntPr.fast_tac @{context} 1\) text \The following are classically but not constructively valid. The attempt to prove them terminates quickly!\ -lemma "((P \ Q) \ P) \ P" +lemma \((P \ Q) \ P) \ P\ apply (tactic \IntPr.fast_tac @{context} 1\)? apply (rule asm_rl) \ \Checks that subgoals remain: proof failed.\ oops -lemma "(P \ Q \ R) \ (P \ R) \ (Q \ R)" +lemma \(P \ Q \ R) \ (P \ R) \ (Q \ R)\ apply (tactic \IntPr.fast_tac @{context} 1\)? apply (rule asm_rl) \ \Checks that subgoals remain: proof failed.\ oops @@ -95,19 +95,19 @@ text \de Bruijn formula with three predicates\ lemma - "((P \ Q) \ P \ Q \ R) \ + \((P \ Q) \ P \ Q \ R) \ ((Q \ R) \ P \ Q \ R) \ - ((R \ P) \ P \ Q \ R) \ P \ Q \ R" + ((R \ P) \ P \ Q \ R) \ P \ Q \ R\ by (tactic \IntPr.fast_tac @{context} 1\) text \de Bruijn formula with five predicates\ lemma - "((P \ Q) \ P \ Q \ R \ S \ T) \ + \((P \ Q) \ P \ Q \ R \ S \ T) \ ((Q \ R) \ P \ Q \ R \ S \ T) \ ((R \ S) \ P \ Q \ R \ S \ T) \ ((S \ T) \ P \ Q \ R \ S \ T) \ - ((T \ P) \ P \ Q \ R \ S \ T) \ P \ Q \ R \ S \ T" + ((T \ P) \ P \ Q \ R \ S \ T) \ P \ Q \ R \ S \ T\ by (tactic \IntPr.fast_tac @{context} 1\) @@ -119,98 +119,98 @@ text\Problem 1.1\ lemma - "(\x. \y. \z. p(x) \ q(y) \ r(z)) \ - (\z. \y. \x. p(x) \ q(y) \ r(z))" + \(\x. \y. \z. p(x) \ q(y) \ r(z)) \ + (\z. \y. \x. p(x) \ q(y) \ r(z))\ by (tactic \IntPr.best_dup_tac @{context} 1\) \ \SLOW\ text\Problem 3.1\ -lemma "\ (\x. \y. mem(y,x) \ \ mem(x,x))" +lemma \\ (\x. \y. mem(y,x) \ \ mem(x,x))\ by (tactic \IntPr.fast_tac @{context} 1\) text\Problem 4.1: hopeless!\ lemma - "(\x. p(x) \ p(h(x)) \ p(g(x))) \ (\x. p(x)) \ (\x. \ p(h(x))) - \ (\x. p(g(g(g(g(g(x)))))))" + \(\x. p(x) \ p(h(x)) \ p(g(x))) \ (\x. p(x)) \ (\x. \ p(h(x))) + \ (\x. p(g(g(g(g(g(x)))))))\ oops subsection \Intuitionistic FOL: propositional problems based on Pelletier.\ text\\\\\1\ -lemma "\ \ ((P \ Q) \ (\ Q \ \ P))" +lemma \\ \ ((P \ Q) \ (\ Q \ \ P))\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\2\ -lemma "\ \ (\ \ P \ P)" +lemma \\ \ (\ \ P \ P)\ by (tactic \IntPr.fast_tac @{context} 1\) text\3\ -lemma "\ (P \ Q) \ (Q \ P)" +lemma \\ (P \ Q) \ (Q \ P)\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\4\ -lemma "\ \ ((\ P \ Q) \ (\ Q \ P))" +lemma \\ \ ((\ P \ Q) \ (\ Q \ P))\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\5\ -lemma "\ \ ((P \ Q \ P \ R) \ P \ (Q \ R))" +lemma \\ \ ((P \ Q \ P \ R) \ P \ (Q \ R))\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\6\ -lemma "\ \ (P \ \ P)" +lemma \\ \ (P \ \ P)\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\7\ -lemma "\ \ (P \ \ \ \ P)" +lemma \\ \ (P \ \ \ \ P)\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\8. Peirce's law\ -lemma "\ \ (((P \ Q) \ P) \ P)" +lemma \\ \ (((P \ Q) \ P) \ P)\ by (tactic \IntPr.fast_tac @{context} 1\) text\9\ -lemma "((P \ Q) \ (\ P \ Q) \ (P \ \ Q)) \ \ (\ P \ \ Q)" +lemma \((P \ Q) \ (\ P \ Q) \ (P \ \ Q)) \ \ (\ P \ \ Q)\ by (tactic \IntPr.fast_tac @{context} 1\) text\10\ -lemma "(Q \ R) \ (R \ P \ Q) \ (P \ (Q \ R)) \ (P \ Q)" +lemma \(Q \ R) \ (R \ P \ Q) \ (P \ (Q \ R)) \ (P \ Q)\ by (tactic \IntPr.fast_tac @{context} 1\) subsection\11. Proved in each direction (incorrectly, says Pelletier!!)\ -lemma "P \ P" +lemma \P \ P\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\12. Dijkstra's law\ -lemma "\ \ (((P \ Q) \ R) \ (P \ (Q \ R)))" +lemma \\ \ (((P \ Q) \ R) \ (P \ (Q \ R)))\ by (tactic \IntPr.fast_tac @{context} 1\) -lemma "((P \ Q) \ R) \ \ \ (P \ (Q \ R))" +lemma \((P \ Q) \ R) \ \ \ (P \ (Q \ R))\ by (tactic \IntPr.fast_tac @{context} 1\) text\13. Distributive law\ -lemma "P \ (Q \ R) \ (P \ Q) \ (P \ R)" +lemma \P \ (Q \ R) \ (P \ Q) \ (P \ R)\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\14\ -lemma "\ \ ((P \ Q) \ ((Q \ \ P) \ (\ Q \ P)))" +lemma \\ \ ((P \ Q) \ ((Q \ \ P) \ (\ Q \ P)))\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\15\ -lemma "\ \ ((P \ Q) \ (\ P \ Q))" +lemma \\ \ ((P \ Q) \ (\ P \ Q))\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\16\ -lemma "\ \ ((P \ Q) \ (Q \ P))" +lemma \\ \ ((P \ Q) \ (Q \ P))\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\17\ -lemma "\ \ (((P \ (Q \ R)) \ S) \ ((\ P \ Q \ S) \ (\ P \ \ R \ S)))" +lemma \\ \ (((P \ (Q \ R)) \ S) \ ((\ P \ Q \ S) \ (\ P \ \ R \ S)))\ by (tactic \IntPr.fast_tac @{context} 1\) text \Dijkstra's ``Golden Rule''\ -lemma "(P \ Q) \ P \ Q \ (P \ Q)" +lemma \(P \ Q) \ P \ Q \ (P \ Q)\ by (tactic \IntPr.fast_tac @{context} 1\) @@ -218,47 +218,47 @@ subsection \The converse is classical in the following implications \dots\ -lemma "(\x. P(x) \ Q) \ (\x. P(x)) \ Q" +lemma \(\x. P(x) \ Q) \ (\x. P(x)) \ Q\ by (tactic \IntPr.fast_tac @{context} 1\) -lemma "((\x. P(x)) \ Q) \ \ (\x. P(x) \ \ Q)" +lemma \((\x. P(x)) \ Q) \ \ (\x. P(x) \ \ Q)\ by (tactic \IntPr.fast_tac @{context} 1\) -lemma "((\x. \ P(x)) \ Q) \ \ (\x. \ (P(x) \ Q))" +lemma \((\x. \ P(x)) \ Q) \ \ (\x. \ (P(x) \ Q))\ by (tactic \IntPr.fast_tac @{context} 1\) -lemma "(\x. P(x)) \ Q \ (\x. P(x) \ Q)" +lemma \(\x. P(x)) \ Q \ (\x. P(x) \ Q)\ by (tactic \IntPr.fast_tac @{context} 1\) -lemma "(\x. P \ Q(x)) \ (P \ (\x. Q(x)))" +lemma \(\x. P \ Q(x)) \ (P \ (\x. Q(x)))\ by (tactic \IntPr.fast_tac @{context} 1\) subsection \The following are not constructively valid!\ text \The attempt to prove them terminates quickly!\ -lemma "((\x. P(x)) \ Q) \ (\x. P(x) \ Q)" +lemma \((\x. P(x)) \ Q) \ (\x. P(x) \ Q)\ apply (tactic \IntPr.fast_tac @{context} 1\)? apply (rule asm_rl) \ \Checks that subgoals remain: proof failed.\ oops -lemma "(P \ (\x. Q(x))) \ (\x. P \ Q(x))" +lemma \(P \ (\x. Q(x))) \ (\x. P \ Q(x))\ apply (tactic \IntPr.fast_tac @{context} 1\)? apply (rule asm_rl) \ \Checks that subgoals remain: proof failed.\ oops -lemma "(\x. P(x) \ Q) \ ((\x. P(x)) \ Q)" +lemma \(\x. P(x) \ Q) \ ((\x. P(x)) \ Q)\ apply (tactic \IntPr.fast_tac @{context} 1\)? apply (rule asm_rl) \ \Checks that subgoals remain: proof failed.\ oops -lemma "(\x. \ \ P(x)) \ \ \ (\x. P(x))" +lemma \(\x. \ \ P(x)) \ \ \ (\x. P(x))\ apply (tactic \IntPr.fast_tac @{context} 1\)? apply (rule asm_rl) \ \Checks that subgoals remain: proof failed.\ oops text \Classically but not intuitionistically valid. Proved by a bug in 1986!\ -lemma "\x. Q(x) \ (\x. Q(x))" +lemma \\x. Q(x) \ (\x. Q(x))\ apply (tactic \IntPr.fast_tac @{context} 1\)? apply (rule asm_rl) \ \Checks that subgoals remain: proof failed.\ oops @@ -272,36 +272,36 @@ \ text\\\\\18\ -lemma "\ \ (\y. \x. P(y) \ P(x))" +lemma \\ \ (\y. \x. P(y) \ P(x))\ oops \ \NOT PROVED\ text\\\\\19\ -lemma "\ \ (\x. \y z. (P(y) \ Q(z)) \ (P(x) \ Q(x)))" +lemma \\ \ (\x. \y z. (P(y) \ Q(z)) \ (P(x) \ Q(x)))\ oops \ \NOT PROVED\ text\20\ lemma - "(\x y. \z. \w. (P(x) \ Q(y) \ R(z) \ S(w))) - \ (\x y. P(x) \ Q(y)) \ (\z. R(z))" + \(\x y. \z. \w. (P(x) \ Q(y) \ R(z) \ S(w))) + \ (\x y. P(x) \ Q(y)) \ (\z. R(z))\ by (tactic \IntPr.fast_tac @{context} 1\) text\21\ -lemma "(\x. P \ Q(x)) \ (\x. Q(x) \ P) \ \ \ (\x. P \ Q(x))" +lemma \(\x. P \ Q(x)) \ (\x. Q(x) \ P) \ \ \ (\x. P \ Q(x))\ oops \ \NOT PROVED; needs quantifier duplication\ text\22\ -lemma "(\x. P \ Q(x)) \ (P \ (\x. Q(x)))" +lemma \(\x. P \ Q(x)) \ (P \ (\x. Q(x)))\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\23\ -lemma "\ \ ((\x. P \ Q(x)) \ (P \ (\x. Q(x))))" +lemma \\ \ ((\x. P \ Q(x)) \ (P \ (\x. Q(x))))\ by (tactic \IntPr.fast_tac @{context} 1\) text\24\ lemma - "\ (\x. S(x) \ Q(x)) \ (\x. P(x) \ Q(x) \ R(x)) \ + \\ (\x. S(x) \ Q(x)) \ (\x. P(x) \ Q(x) \ R(x)) \ (\ (\x. P(x)) \ (\x. Q(x))) \ (\x. Q(x) \ R(x) \ S(x)) - \ \ \ (\x. P(x) \ R(x))" + \ \ \ (\x. P(x) \ R(x))\ text \ Not clear why \fast_tac\, \best_tac\, \ASTAR\ and \ITER_DEEPEN\ all take forever. @@ -314,139 +314,139 @@ text\25\ lemma - "(\x. P(x)) \ + \(\x. P(x)) \ (\x. L(x) \ \ (M(x) \ R(x))) \ (\x. P(x) \ (M(x) \ L(x))) \ ((\x. P(x) \ Q(x)) \ (\x. P(x) \ R(x))) - \ (\x. Q(x) \ P(x))" + \ (\x. Q(x) \ P(x))\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\26\ lemma - "(\ \ (\x. p(x)) \ \ \ (\x. q(x))) \ + \(\ \ (\x. p(x)) \ \ \ (\x. q(x))) \ (\x. \y. p(x) \ q(y) \ (r(x) \ s(y))) - \ ((\x. p(x) \ r(x)) \ (\x. q(x) \ s(x)))" + \ ((\x. p(x) \ r(x)) \ (\x. q(x) \ s(x)))\ oops \ \NOT PROVED\ text\27\ lemma - "(\x. P(x) \ \ Q(x)) \ + \(\x. P(x) \ \ Q(x)) \ (\x. P(x) \ R(x)) \ (\x. M(x) \ L(x) \ P(x)) \ ((\x. R(x) \ \ Q(x)) \ (\x. L(x) \ \ R(x))) - \ (\x. M(x) \ \ L(x))" + \ (\x. M(x) \ \ L(x))\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\28. AMENDED\ lemma - "(\x. P(x) \ (\x. Q(x))) \ + \(\x. P(x) \ (\x. Q(x))) \ (\ \ (\x. Q(x) \ R(x)) \ (\x. Q(x) \ S(x))) \ (\ \ (\x. S(x)) \ (\x. L(x) \ M(x))) - \ (\x. P(x) \ L(x) \ M(x))" + \ (\x. P(x) \ L(x) \ M(x))\ by (tactic \IntPr.fast_tac @{context} 1\) text\29. Essentially the same as Principia Mathematica *11.71\ lemma - "(\x. P(x)) \ (\y. Q(y)) + \(\x. P(x)) \ (\y. Q(y)) \ ((\x. P(x) \ R(x)) \ (\y. Q(y) \ S(y)) \ - (\x y. P(x) \ Q(y) \ R(x) \ S(y)))" + (\x y. P(x) \ Q(y) \ R(x) \ S(y)))\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\30\ lemma - "(\x. (P(x) \ Q(x)) \ \ R(x)) \ + \(\x. (P(x) \ Q(x)) \ \ R(x)) \ (\x. (Q(x) \ \ S(x)) \ P(x) \ R(x)) - \ (\x. \ \ S(x))" + \ (\x. \ \ S(x))\ by (tactic \IntPr.fast_tac @{context} 1\) text\31\ lemma - "\ (\x. P(x) \ (Q(x) \ R(x))) \ + \\ (\x. P(x) \ (Q(x) \ R(x))) \ (\x. L(x) \ P(x)) \ (\x. \ R(x) \ M(x)) - \ (\x. L(x) \ M(x))" + \ (\x. L(x) \ M(x))\ by (tactic \IntPr.fast_tac @{context} 1\) text\32\ lemma - "(\x. P(x) \ (Q(x) \ R(x)) \ S(x)) \ + \(\x. P(x) \ (Q(x) \ R(x)) \ S(x)) \ (\x. S(x) \ R(x) \ L(x)) \ (\x. M(x) \ R(x)) - \ (\x. P(x) \ M(x) \ L(x))" + \ (\x. P(x) \ M(x) \ L(x))\ by (tactic \IntPr.fast_tac @{context} 1\) text\\\\\33\ lemma - "(\x. \ \ (P(a) \ (P(x) \ P(b)) \ P(c))) \ - (\x. \ \ ((\ P(a) \ P(x) \ P(c)) \ (\ P(a) \ \ P(b) \ P(c))))" + \(\x. \ \ (P(a) \ (P(x) \ P(b)) \ P(c))) \ + (\x. \ \ ((\ P(a) \ P(x) \ P(c)) \ (\ P(a) \ \ P(b) \ P(c))))\ apply (tactic \IntPr.best_tac @{context} 1\) done text\36\ lemma - "(\x. \y. J(x,y)) \ + \(\x. \y. J(x,y)) \ (\x. \y. G(x,y)) \ (\x y. J(x,y) \ G(x,y) \ (\z. J(y,z) \ G(y,z) \ H(x,z))) - \ (\x. \y. H(x,y))" + \ (\x. \y. H(x,y))\ by (tactic \IntPr.fast_tac @{context} 1\) text\37\ lemma - "(\z. \w. \x. \y. + \(\z. \w. \x. \y. \ \ (P(x,z) \ P(y,w)) \ P(y,z) \ (P(y,w) \ (\u. Q(u,w)))) \ (\x z. \ P(x,z) \ (\y. Q(y,z))) \ (\ \ (\x y. Q(x,y)) \ (\x. R(x,x))) - \ \ \ (\x. \y. R(x,y))" + \ \ \ (\x. \y. R(x,y))\ oops \ \NOT PROVED\ text\39\ -lemma "\ (\x. \y. F(y,x) \ \ F(y,y))" +lemma \\ (\x. \y. F(y,x) \ \ F(y,y))\ by (tactic \IntPr.fast_tac @{context} 1\) text\40. AMENDED\ lemma - "(\y. \x. F(x,y) \ F(x,x)) \ - \ (\x. \y. \z. F(z,y) \ \ F(z,x))" + \(\y. \x. F(x,y) \ F(x,x)) \ + \ (\x. \y. \z. F(z,y) \ \ F(z,x))\ by (tactic \IntPr.fast_tac @{context} 1\) text\44\ lemma - "(\x. f(x) \ + \(\x. f(x) \ (\y. g(y) \ h(x,y) \ (\y. g(y) \ \ h(x,y)))) \ (\x. j(x) \ (\y. g(y) \ h(x,y))) - \ (\x. j(x) \ \ f(x))" + \ (\x. j(x) \ \ f(x))\ by (tactic \IntPr.fast_tac @{context} 1\) text\48\ -lemma "(a = b \ c = d) \ (a = c \ b = d) \ a = d \ b = c" +lemma \(a = b \ c = d) \ (a = c \ b = d) \ a = d \ b = c\ by (tactic \IntPr.fast_tac @{context} 1\) text\51\ lemma - "(\z w. \x y. P(x,y) \ (x = z \ y = w)) \ - (\z. \x. \w. (\y. P(x,y) \ y = w) \ x = z)" + \(\z w. \x y. P(x,y) \ (x = z \ y = w)) \ + (\z. \x. \w. (\y. P(x,y) \ y = w) \ x = z)\ by (tactic \IntPr.fast_tac @{context} 1\) text\52\ text \Almost the same as 51.\ lemma - "(\z w. \x y. P(x,y) \ (x = z \ y = w)) \ - (\w. \y. \z. (\x. P(x,y) \ x = z) \ y = w)" + \(\z w. \x y. P(x,y) \ (x = z \ y = w)) \ + (\w. \y. \z. (\x. P(x,y) \ x = z) \ y = w)\ by (tactic \IntPr.fast_tac @{context} 1\) text\56\ -lemma "(\x. (\y. P(y) \ x = f(y)) \ P(x)) \ (\x. P(x) \ P(f(x)))" +lemma \(\x. (\y. P(y) \ x = f(y)) \ P(x)) \ (\x. P(x) \ P(f(x)))\ by (tactic \IntPr.fast_tac @{context} 1\) text\57\ lemma - "P(f(a,b), f(b,c)) \ P(f(b,c), f(a,c)) \ - (\x y z. P(x,y) \ P(y,z) \ P(x,z)) \ P(f(a,b), f(a,c))" + \P(f(a,b), f(b,c)) \ P(f(b,c), f(a,c)) \ + (\x y z. P(x,y) \ P(y,z) \ P(x,z)) \ P(f(a,b), f(a,c))\ by (tactic \IntPr.fast_tac @{context} 1\) text\60\ -lemma "\x. P(x,f(x)) \ (\y. (\z. P(z,y) \ P(z,f(x))) \ P(x,y))" +lemma \\x. P(x,f(x)) \ (\y. (\z. P(z,y) \ P(z,f(x))) \ P(x,y))\ by (tactic \IntPr.fast_tac @{context} 1\) end diff -r e15f053a42d8 -r e65314985426 src/FOL/ex/Locale_Test/Locale_Test.thy --- a/src/FOL/ex/Locale_Test/Locale_Test.thy Thu Jan 03 21:48:05 2019 +0100 +++ b/src/FOL/ex/Locale_Test/Locale_Test.thy Thu Jan 03 22:19:19 2019 +0100 @@ -16,9 +16,9 @@ lemmas less_mixin_thy_merge2 = le'.less_def end -lemma "gless(x, y) \ gle(x, y) \ x \ y" (* mixin from first interpretation applied *) +lemma \gless(x, y) \ gle(x, y) \ x \ y\ (* mixin from first interpretation applied *) by (rule le1.less_mixin_thy_merge1) -lemma "gless'(x, y) \ gle'(x, y) \ x \ y" (* mixin from second interpretation applied *) +lemma \gless'(x, y) \ gle'(x, y) \ x \ y\ (* mixin from second interpretation applied *) by (rule le1.less_mixin_thy_merge2) end diff -r e15f053a42d8 -r e65314985426 src/FOL/ex/Locale_Test/Locale_Test1.thy --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Thu Jan 03 21:48:05 2019 +0100 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Thu Jan 03 22:19:19 2019 +0100 @@ -9,24 +9,24 @@ begin typedecl int -instance int :: "term" .. +instance int :: \term\ .. -consts plus :: "int => int => int" (infixl \+\ 60) - zero :: int (\0\) - minus :: "int => int" (\- _\) +consts plus :: \int => int => int\ (infixl \+\ 60) + zero :: \int\ (\0\) + minus :: \int => int\ (\- _\) axiomatization where - int_assoc: "(x + y::int) + z = x + (y + z)" and - int_zero: "0 + x = x" and - int_minus: "(-x) + x = 0" and - int_minus2: "-(-x) = x" + int_assoc: \(x + y::int) + z = x + (y + z)\ and + int_zero: \0 + x = x\ and + int_minus: \(-x) + x = 0\ and + int_minus2: \-(-x) = x\ section \Inference of parameter types\ locale param1 = fixes p print_locale! param1 -locale param2 = fixes p :: 'b +locale param2 = fixes p :: \'b\ print_locale! param2 (* @@ -37,7 +37,7 @@ locale param3 = fixes p (infix \..\ 50) print_locale! param3 -locale param4 = fixes p :: "'a => 'a => 'a" (infix \..\ 50) +locale param4 = fixes p :: \'a => 'a => 'a\ (infix \..\ 50) print_locale! param4 @@ -45,13 +45,13 @@ locale constraint1 = fixes prod (infixl \**\ 65) - assumes l_id: "x ** y = x" - assumes assoc: "(x ** y) ** z = x ** (y ** z)" + assumes l_id: \x ** y = x\ + assumes assoc: \(x ** y) ** z = x ** (y ** z)\ print_locale! constraint1 locale constraint2 = fixes p and q - assumes "p = q" + assumes \p = q\ print_locale! constraint2 @@ -59,35 +59,35 @@ locale semi = fixes prod (infixl \**\ 65) - assumes assoc: "(x ** y) ** z = x ** (y ** z)" + assumes assoc: \(x ** y) ** z = x ** (y ** z)\ print_locale! semi thm semi_def locale lgrp = semi + fixes one and inv - assumes lone: "one ** x = x" - and linv: "inv(x) ** x = one" + assumes lone: \one ** x = x\ + and linv: \inv(x) ** x = one\ print_locale! lgrp thm lgrp_def lgrp_axioms_def -locale add_lgrp = semi "(++)" for sum (infixl \++\ 60) + +locale add_lgrp = semi \(++)\ for sum (infixl \++\ 60) + fixes zero and neg - assumes lzero: "zero ++ x = x" - and lneg: "neg(x) ++ x = zero" + assumes lzero: \zero ++ x = x\ + and lneg: \neg(x) ++ x = zero\ print_locale! add_lgrp thm add_lgrp_def add_lgrp_axioms_def -locale rev_lgrp = semi "%x y. y ++ x" for sum (infixl \++\ 60) +locale rev_lgrp = semi \%x y. y ++ x\ for sum (infixl \++\ 60) print_locale! rev_lgrp thm rev_lgrp_def -locale hom = f: semi f + g: semi g for f and g +locale hom = f: semi \f\ + g: semi \g\ for f and g print_locale! hom thm hom_def -locale perturbation = semi + d: semi "%x y. delta(x) ** delta(y)" for delta +locale perturbation = semi + d: semi \%x y. delta(x) ** delta(y)\ for delta print_locale! perturbation thm perturbation_def -locale pert_hom = d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2 +locale pert_hom = d1: perturbation \f\ \d1\ + d2: perturbation \f\ \d2\ for f d1 d2 print_locale! pert_hom thm pert_hom_def text \Alternative expression, obtaining nicer names in \semi f\.\ -locale pert_hom' = semi f + d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2 +locale pert_hom' = semi \f\ + d1: perturbation \f\ \d1\ + d2: perturbation \f\ \d2\ for f d1 d2 print_locale! pert_hom' thm pert_hom'_def @@ -96,32 +96,32 @@ locale logic = fixes land (infixl \&&\ 55) and lnot (\-- _\ [60] 60) - assumes assoc: "(x && y) && z = x && (y && z)" - and notnot: "-- (-- x) = x" + assumes assoc: \(x && y) && z = x && (y && z)\ + and notnot: \-- (-- x) = x\ begin definition lor (infixl \||\ 50) where - "x || y = --(-- x && -- y)" + \x || y = --(-- x && -- y)\ end print_locale! logic -locale use_decl = l: logic + semi "(||)" +locale use_decl = l: logic + semi \(||)\ print_locale! use_decl thm use_decl_def locale extra_type = - fixes a :: 'a - and P :: "'a => 'b => o" + fixes a :: \'a\ + and P :: \'a => 'b => o\ begin -definition test :: "'a => o" - where "test(x) \ (\b. P(x, b))" +definition test :: \'a => o\ + where \test(x) \ (\b. P(x, b))\ end -term extra_type.test thm extra_type.test_def +term \extra_type.test\ thm extra_type.test_def -interpretation var?: extra_type "0" "%x y. x = 0" . +interpretation var?: extra_type \0\ \%x y. x = 0\ . thm var.test_def @@ -143,12 +143,12 @@ declare [[show_hyps]] locale "syntax" = - fixes p1 :: "'a => 'b" - and p2 :: "'b => o" + fixes p1 :: \'a => 'b\ + and p2 :: \'b => o\ begin -definition d1 :: "'a => o" (\D1'(_')\) where "d1(x) \ \ p2(p1(x))" -definition d2 :: "'b => o" (\D2'(_')\) where "d2(x) \ \ p2(x)" +definition d1 :: \'a => o\ (\D1'(_')\) where \d1(x) \ \ p2(p1(x))\ +definition d2 :: \'b => o\ (\D2'(_')\) where \d2(x) \ \ p2(x)\ thm d1_def d2_def @@ -156,7 +156,7 @@ thm syntax.d1_def syntax.d2_def -locale syntax' = "syntax" p1 p2 for p1 :: "'a => 'a" and p2 :: "'a => o" +locale syntax' = "syntax" \p1\ \p2\ for p1 :: \'a => 'a\ and p2 :: \'a => o\ begin thm d1_def d2_def (* should print as "D1(?x) <-> ..." and "D2(?x) <-> ..." *) @@ -168,7 +168,7 @@ end -locale syntax'' = "syntax" p3 p2 for p3 :: "'a => 'b" and p2 :: "'b => o" +locale syntax'' = "syntax" \p3\ \p2\ for p3 :: \'a => 'b\ and p2 :: \'b => o\ begin thm d1_def d2_def @@ -194,14 +194,14 @@ fixes land (infixl \&&\ 55) and lor (infixl \||\ 50) and lnot (\-- _\ [60] 60) - assumes assoc: "(x && y) && z = x && (y && z)" - and notnot: "-- (-- x) = x" - defines "x || y == --(-- x && -- y)" + assumes assoc: \(x && y) && z = x && (y && z)\ + and notnot: \-- (-- x) = x\ + defines \x || y == --(-- x && -- y)\ begin thm lor_def -lemma "x || y = --(-- x && --y)" +lemma \x || y = --(-- x && --y)\ by (unfold lor_def) (rule refl) end @@ -211,7 +211,7 @@ locale logic_def2 = logic_def begin -lemma "x || y = --(-- x && --y)" +lemma \x || y = --(-- x && --y)\ by (unfold lor_def) (rule refl) end @@ -222,56 +222,56 @@ (* A somewhat arcane homomorphism example *) definition semi_hom where - "semi_hom(prod, sum, h) \ (\x y. h(prod(x, y)) = sum(h(x), h(y)))" + \semi_hom(prod, sum, h) \ (\x y. h(prod(x, y)) = sum(h(x), h(y)))\ lemma semi_hom_mult: - "semi_hom(prod, sum, h) \ h(prod(x, y)) = sum(h(x), h(y))" + \semi_hom(prod, sum, h) \ h(prod(x, y)) = sum(h(x), h(y))\ by (simp add: semi_hom_def) -locale semi_hom_loc = prod: semi prod + sum: semi sum +locale semi_hom_loc = prod: semi \prod\ + sum: semi \sum\ for prod and sum and h + - assumes semi_homh: "semi_hom(prod, sum, h)" + assumes semi_homh: \semi_hom(prod, sum, h)\ notes semi_hom_mult = semi_hom_mult [OF semi_homh] thm semi_hom_loc.semi_hom_mult (* unspecified, attribute not applied in backgroud theory !!! *) -lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))" +lemma (in semi_hom_loc) \h(prod(x, y)) = sum(h(x), h(y))\ by (rule semi_hom_mult) (* Referring to facts from within a context specification *) lemma - assumes x: "P \ P" + assumes x: \P \ P\ notes y = x - shows True .. + shows \True\ .. section \Theorem statements\ lemma (in lgrp) lcancel: - "x ** y = x ** z \ y = z" + \x ** y = x ** z \ y = z\ proof - assume "x ** y = x ** z" - then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc) - then show "y = z" by (simp add: lone linv) + assume \x ** y = x ** z\ + then have \inv(x) ** x ** y = inv(x) ** x ** z\ by (simp add: assoc) + then show \y = z\ by (simp add: lone linv) qed simp print_locale! lgrp locale rgrp = semi + fixes one and inv - assumes rone: "x ** one = x" - and rinv: "x ** inv(x) = one" + assumes rone: \x ** one = x\ + and rinv: \x ** inv(x) = one\ begin lemma rcancel: - "y ** x = z ** x \ y = z" + \y ** x = z ** x \ y = z\ proof - assume "y ** x = z ** x" - then have "y ** (x ** inv(x)) = z ** (x ** inv(x))" + assume \y ** x = z ** x\ + then have \y ** (x ** inv(x)) = z ** (x ** inv(x))\ by (simp add: assoc [symmetric]) - then show "y = z" by (simp add: rone rinv) + then show \y = z\ by (simp add: rone rinv) qed simp end @@ -281,18 +281,18 @@ subsection \Patterns\ lemma (in rgrp) - assumes "y ** x = z ** x" (is ?a) - shows "y = z" (is ?t) + assumes \y ** x = z ** x\ (is \?a\) + shows \y = z\ (is \?t\) proof - txt \Weird proof involving patterns from context element and conclusion.\ { - assume ?a - then have "y ** (x ** inv(x)) = z ** (x ** inv(x))" + assume \?a\ + then have \y ** (x ** inv(x)) = z ** (x ** inv(x))\ by (simp add: assoc [symmetric]) - then have ?t by (simp add: rone rinv) + then have \?t\ by (simp add: rone rinv) } note x = this - show ?t by (rule x [OF \?a\]) + show \?t\ by (rule x [OF \?a\]) qed @@ -303,15 +303,15 @@ proof unfold_locales { fix x - have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone) - then show "x ** one = x" by (simp add: assoc lcancel) + have \inv(x) ** x ** one = inv(x) ** x\ by (simp add: linv lone) + then show \x ** one = x\ by (simp add: assoc lcancel) } note rone = this { fix x - have "inv(x) ** x ** inv(x) = inv(x) ** one" + have \inv(x) ** x ** inv(x) = inv(x) ** one\ by (simp add: linv lone rone) - then show "x ** inv(x) = one" by (simp add: assoc lcancel) + then show \x ** inv(x) = one\ by (simp add: assoc lcancel) } qed @@ -322,7 +322,7 @@ (* use of derived theorem *) lemma (in lgrp) - "y ** x = z ** x \ y = z" + \y ** x = z ** x \ y = z\ apply (rule rcancel) done @@ -332,15 +332,15 @@ proof unfold_locales { fix x - have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone) - then show "one ** x = x" by (simp add: assoc [symmetric] rcancel) + have \one ** (x ** inv(x)) = x ** inv(x)\ by (simp add: rinv rone) + then show \one ** x = x\ by (simp add: assoc [symmetric] rcancel) } note lone = this { fix x - have "inv(x) ** (x ** inv(x)) = one ** inv(x)" + have \inv(x) ** (x ** inv(x)) = one ** inv(x)\ by (simp add: rinv lone rone) - then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel) + then show \inv(x) ** x = one\ by (simp add: assoc [symmetric] rcancel) } qed @@ -353,30 +353,30 @@ (* Duality *) locale order = - fixes less :: "'a => 'a => o" (infix \<<\ 50) - assumes refl: "x << x" - and trans: "[| x << y; y << z |] ==> x << z" + fixes less :: \'a => 'a => o\ (infix \<<\ 50) + assumes refl: \x << x\ + and trans: \[| x << y; y << z |] ==> x << z\ -sublocale order < dual: order "%x y. y << x" +sublocale order < dual: order \%x y. y << x\ apply unfold_locales apply (rule refl) apply (blast intro: trans) done print_locale! order (* Only two instances of order. *) locale order' = - fixes less :: "'a => 'a => o" (infix \<<\ 50) - assumes refl: "x << x" - and trans: "[| x << y; y << z |] ==> x << z" + fixes less :: \'a => 'a => o\ (infix \<<\ 50) + assumes refl: \x << x\ + and trans: \[| x << y; y << z |] ==> x << z\ locale order_with_def = order' begin -definition greater :: "'a => 'a => o" (infix \>>\ 50) where - "x >> y \ y << x" +definition greater :: \'a => 'a => o\ (infix \>>\ 50) where + \x >> y \ y << x\ end -sublocale order_with_def < dual: order' "(>>)" +sublocale order_with_def < dual: order' \(>>)\ apply unfold_locales unfolding greater_def apply (rule refl) apply (blast intro: trans) @@ -392,17 +392,17 @@ locale A5 = fixes A and B and C and D and E - assumes eq: "A \ B \ C \ D \ E" + assumes eq: \A \ B \ C \ D \ E\ -sublocale A5 < 1: A5 _ _ D E C +sublocale A5 < 1: A5 _ _ \D\ \E\ \C\ print_facts using eq apply (blast intro: A5.intro) done -sublocale A5 < 2: A5 C _ E _ A +sublocale A5 < 2: A5 \C\ _ \E\ _ \A\ print_facts using eq apply (blast intro: A5.intro) done -sublocale A5 < 3: A5 B C A _ _ +sublocale A5 < 3: A5 \B\ \C\ \A\ _ _ print_facts using eq apply (blast intro: A5.intro) done @@ -414,25 +414,25 @@ (* Free arguments of instance *) locale trivial = - fixes P and Q :: o - assumes Q: "P \ P \ Q" + fixes P and Q :: \o\ + assumes Q: \P \ P \ Q\ begin -lemma Q_triv: "Q" using Q by fast +lemma Q_triv: \Q\ using Q by fast end -sublocale trivial < x: trivial x _ +sublocale trivial < x: trivial \x\ _ apply unfold_locales using Q by fast print_locale! trivial context trivial begin -thm x.Q [where ?x = True] +thm x.Q [where ?x = \True\] end -sublocale trivial < y: trivial Q Q +sublocale trivial < y: trivial \Q\ \Q\ by unfold_locales (* Succeeds since previous interpretation is more general. *) @@ -441,13 +441,13 @@ subsection \Sublocale, then interpretation in theory\ -interpretation int?: lgrp "(+)" "0" "minus" +interpretation int?: lgrp \(+)\ \0\ \minus\ proof unfold_locales qed (rule int_assoc int_zero int_minus)+ thm int.assoc int.semi_axioms -interpretation int2?: semi "(+)" +interpretation int2?: semi \(+)\ by unfold_locales (* subsumed, thm int2.assoc not generated *) ML \(Global_Theory.get_thms @{theory} "int2.assoc"; @@ -460,18 +460,18 @@ subsection \Interpretation in theory, then sublocale\ -interpretation fol: logic "(+)" "minus" +interpretation fol: logic \(+)\ \minus\ by unfold_locales (rule int_assoc int_minus2)+ locale logic2 = fixes land (infixl \&&\ 55) and lnot (\-- _\ [60] 60) - assumes assoc: "(x && y) && z = x && (y && z)" - and notnot: "-- (-- x) = x" + assumes assoc: \(x && y) && z = x && (y && z)\ + and notnot: \-- (-- x) = x\ begin definition lor (infixl \||\ 50) where - "x || y = --(-- x && -- y)" + \x || y = --(-- x && -- y)\ end @@ -497,59 +497,59 @@ locale logic_o = fixes land (infixl \&&\ 55) and lnot (\-- _\ [60] 60) - assumes assoc_o: "(x && y) && z \ x && (y && z)" - and notnot_o: "-- (-- x) \ x" + assumes assoc_o: \(x && y) && z \ x && (y && z)\ + and notnot_o: \-- (-- x) \ x\ begin definition lor_o (infixl \||\ 50) where - "x || y \ --(-- x && -- y)" + \x || y \ --(-- x && -- y)\ end -interpretation x: logic_o "(\)" "Not" - rewrites bool_logic_o: "x.lor_o(x, y) \ x \ y" +interpretation x: logic_o \(\)\ \Not\ + rewrites bool_logic_o: \x.lor_o(x, y) \ x \ y\ proof - - show bool_logic_o: "PROP logic_o((\), Not)" by unfold_locales fast+ - show "logic_o.lor_o((\), Not, x, y) \ x \ y" + show bool_logic_o: \PROP logic_o((\), Not)\ by unfold_locales fast+ + show \logic_o.lor_o((\), Not, x, y) \ x \ y\ by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast qed thm x.lor_o_def bool_logic_o -lemma lor_triv: "z \ z" .. +lemma lor_triv: \z \ z\ .. -lemma (in logic_o) lor_triv: "x || y \ x || y" by fast +lemma (in logic_o) lor_triv: \x || y \ x || y\ by fast -thm lor_triv [where z = True] (* Check strict prefix. *) +thm lor_triv [where z = \True\] (* Check strict prefix. *) x.lor_triv subsection \Rewrite morphisms in expressions\ -interpretation y: logic_o "(\)" "Not" rewrites bool_logic_o2: "logic_o.lor_o((\), Not, x, y) \ x \ y" +interpretation y: logic_o \(\)\ \Not\ rewrites bool_logic_o2: \logic_o.lor_o((\), Not, x, y) \ x \ y\ proof - - show bool_logic_o: "PROP logic_o((\), Not)" by unfold_locales fast+ - show "logic_o.lor_o((\), Not, x, y) \ x \ y" unfolding logic_o.lor_o_def [OF bool_logic_o] by fast + show bool_logic_o: \PROP logic_o((\), Not)\ by unfold_locales fast+ + show \logic_o.lor_o((\), Not, x, y) \ x \ y\ unfolding logic_o.lor_o_def [OF bool_logic_o] by fast qed subsection \Inheritance of rewrite morphisms\ locale reflexive = - fixes le :: "'a => 'a => o" (infix \\\ 50) - assumes refl: "x \ x" + fixes le :: \'a => 'a => o\ (infix \\\ 50) + assumes refl: \x \ x\ begin -definition less (infix \\\ 50) where "x \ y \ x \ y \ x \ y" +definition less (infix \\\ 50) where \x \ y \ x \ y \ x \ y\ end axiomatization - gle :: "'a => 'a => o" and gless :: "'a => 'a => o" and - gle' :: "'a => 'a => o" and gless' :: "'a => 'a => o" + gle :: \'a => 'a => o\ and gless :: \'a => 'a => o\ and + gle' :: \'a => 'a => o\ and gless' :: \'a => 'a => o\ where - grefl: "gle(x, x)" and gless_def: "gless(x, y) \ gle(x, y) \ x \ y" and - grefl': "gle'(x, x)" and gless'_def: "gless'(x, y) \ gle'(x, y) \ x \ y" + grefl: \gle(x, x)\ and gless_def: \gless(x, y) \ gle(x, y) \ x \ y\ and + grefl': \gle'(x, x)\ and gless'_def: \gless'(x, y) \ gle'(x, y) \ x \ y\ text \Setup\ @@ -558,11 +558,11 @@ lemmas less_thm = less_def end -interpretation le: mixin gle rewrites "reflexive.less(gle, x, y) \ gless(x, y)" +interpretation le: mixin \gle\ rewrites \reflexive.less(gle, x, y) \ gless(x, y)\ proof - - show "mixin(gle)" by unfold_locales (rule grefl) + show \mixin(gle)\ by unfold_locales (rule grefl) note reflexive = this[unfolded mixin_def] - show "reflexive.less(gle, x, y) \ gless(x, y)" + show \reflexive.less(gle, x, y) \ gless(x, y)\ by (simp add: reflexive.less_def[OF reflexive] gless_def) qed @@ -573,11 +573,11 @@ lemmas less_thm2 = less_def end -interpretation le: mixin2 gle +interpretation le: mixin2 \gle\ by unfold_locales thm le.less_thm2 (* rewrite morphism applied *) -lemma "gless(x, y) \ gle(x, y) \ x \ y" +lemma \gless(x, y) \ gle(x, y) \ x \ y\ by (rule le.less_thm2) text \Rewrite morphism does not leak to a side branch.\ @@ -587,11 +587,11 @@ lemmas less_thm3 = less_def end -interpretation le: mixin3 gle +interpretation le: mixin3 \gle\ by unfold_locales thm le.less_thm3 (* rewrite morphism not applied *) -lemma "reflexive.less(gle, x, y) \ gle(x, y) \ x \ y" by (rule le.less_thm3) +lemma \reflexive.less(gle, x, y) \ gle(x, y) \ x \ y\ by (rule le.less_thm3) text \Rewrite morphism only available in original context\ @@ -599,12 +599,12 @@ locale mixin4_mixin = mixin4_base -interpretation le: mixin4_mixin gle - rewrites "reflexive.less(gle, x, y) \ gless(x, y)" +interpretation le: mixin4_mixin \gle\ + rewrites \reflexive.less(gle, x, y) \ gless(x, y)\ proof - - show "mixin4_mixin(gle)" by unfold_locales (rule grefl) + show \mixin4_mixin(gle)\ by unfold_locales (rule grefl) note reflexive = this[unfolded mixin4_mixin_def mixin4_base_def mixin_def] - show "reflexive.less(gle, x, y) \ gless(x, y)" + show \reflexive.less(gle, x, y) \ gless(x, y)\ by (simp add: reflexive.less_def[OF reflexive] gless_def) qed @@ -613,16 +613,16 @@ lemmas less_thm4 = less_def end -locale mixin4_combined = le1?: mixin4_mixin le' + le2?: mixin4_copy le for le' le +locale mixin4_combined = le1?: mixin4_mixin \le'\ + le2?: mixin4_copy \le\ for le' le begin lemmas less_thm4' = less_def end -interpretation le4: mixin4_combined gle' gle +interpretation le4: mixin4_combined \gle'\ \gle\ by unfold_locales (rule grefl') thm le4.less_thm4' (* rewrite morphism not applied *) -lemma "reflexive.less(gle, x, y) \ gle(x, y) \ x \ y" +lemma \reflexive.less(gle, x, y) \ gle(x, y) \ x \ y\ by (rule le4.less_thm4') text \Inherited rewrite morphism applied to new theorem\ @@ -631,22 +631,22 @@ locale mixin5_inherited = mixin5_base -interpretation le5: mixin5_base gle - rewrites "reflexive.less(gle, x, y) \ gless(x, y)" +interpretation le5: mixin5_base \gle\ + rewrites \reflexive.less(gle, x, y) \ gless(x, y)\ proof - - show "mixin5_base(gle)" by unfold_locales + show \mixin5_base(gle)\ by unfold_locales note reflexive = this[unfolded mixin5_base_def mixin_def] - show "reflexive.less(gle, x, y) \ gless(x, y)" + show \reflexive.less(gle, x, y) \ gless(x, y)\ by (simp add: reflexive.less_def[OF reflexive] gless_def) qed -interpretation le5: mixin5_inherited gle +interpretation le5: mixin5_inherited \gle\ by unfold_locales lemmas (in mixin5_inherited) less_thm5 = less_def thm le5.less_thm5 (* rewrite morphism applied *) -lemma "gless(x, y) \ gle(x, y) \ x \ y" +lemma \gless(x, y) \ gle(x, y) \ x \ y\ by (rule le5.less_thm5) text \Rewrite morphism pushed down to existing inherited locale\ @@ -655,23 +655,23 @@ locale mixin6_inherited = mixin5_base -interpretation le6: mixin6_base gle +interpretation le6: mixin6_base \gle\ by unfold_locales -interpretation le6: mixin6_inherited gle +interpretation le6: mixin6_inherited \gle\ by unfold_locales -interpretation le6: mixin6_base gle - rewrites "reflexive.less(gle, x, y) \ gless(x, y)" +interpretation le6: mixin6_base \gle\ + rewrites \reflexive.less(gle, x, y) \ gless(x, y)\ proof - - show "mixin6_base(gle)" by unfold_locales + show \mixin6_base(gle)\ by unfold_locales note reflexive = this[unfolded mixin6_base_def mixin_def] - show "reflexive.less(gle, x, y) \ gless(x, y)" + show \reflexive.less(gle, x, y) \ gless(x, y)\ by (simp add: reflexive.less_def[OF reflexive] gless_def) qed lemmas (in mixin6_inherited) less_thm6 = less_def thm le6.less_thm6 (* mixin applied *) -lemma "gless(x, y) \ gle(x, y) \ x \ y" +lemma \gless(x, y) \ gle(x, y) \ x \ y\ by (rule le6.less_thm6) text \Existing rewrite morphism inherited through sublocale relation\ @@ -680,22 +680,22 @@ locale mixin7_inherited = reflexive -interpretation le7: mixin7_base gle - rewrites "reflexive.less(gle, x, y) \ gless(x, y)" +interpretation le7: mixin7_base \gle\ + rewrites \reflexive.less(gle, x, y) \ gless(x, y)\ proof - - show "mixin7_base(gle)" by unfold_locales + show \mixin7_base(gle)\ by unfold_locales note reflexive = this[unfolded mixin7_base_def mixin_def] - show "reflexive.less(gle, x, y) \ gless(x, y)" + show \reflexive.less(gle, x, y) \ gless(x, y)\ by (simp add: reflexive.less_def[OF reflexive] gless_def) qed -interpretation le7: mixin7_inherited gle +interpretation le7: mixin7_inherited \gle\ by unfold_locales lemmas (in mixin7_inherited) less_thm7 = less_def thm le7.less_thm7 (* before, rewrite morphism not applied *) -lemma "reflexive.less(gle, x, y) \ gle(x, y) \ x \ y" +lemma \reflexive.less(gle, x, y) \ gle(x, y) \ x \ y\ by (rule le7.less_thm7) sublocale mixin7_inherited < mixin7_base @@ -704,13 +704,13 @@ lemmas (in mixin7_inherited) less_thm7b = less_def thm le7.less_thm7b (* after, mixin applied *) -lemma "gless(x, y) \ gle(x, y) \ x \ y" +lemma \gless(x, y) \ gle(x, y) \ x \ y\ by (rule le7.less_thm7b) text \This locale will be interpreted in later theories.\ -locale mixin_thy_merge = le: reflexive le + le': reflexive le' for le le' +locale mixin_thy_merge = le: reflexive \le\ + le': reflexive \le'\ for le le' subsection \Rewrite morphisms in sublocale\ @@ -720,37 +720,37 @@ selection operator.\ axiomatization glob_one and glob_inv - where glob_lone: "prod(glob_one(prod), x) = x" - and glob_linv: "prod(glob_inv(prod, x), x) = glob_one(prod)" + where glob_lone: \prod(glob_one(prod), x) = x\ + and glob_linv: \prod(glob_inv(prod, x), x) = glob_one(prod)\ locale dgrp = semi begin -definition one where "one = glob_one(prod)" +definition one where \one = glob_one(prod)\ -lemma lone: "one ** x = x" +lemma lone: \one ** x = x\ unfolding one_def by (rule glob_lone) -definition inv where "inv(x) = glob_inv(prod, x)" +definition inv where \inv(x) = glob_inv(prod, x)\ -lemma linv: "inv(x) ** x = one" +lemma linv: \inv(x) ** x = one\ unfolding one_def inv_def by (rule glob_linv) end sublocale lgrp < def?: dgrp - rewrites one_equation: "dgrp.one(prod) = one" and inv_equation: "dgrp.inv(prod, x) = inv(x)" + rewrites one_equation: \dgrp.one(prod) = one\ and inv_equation: \dgrp.inv(prod, x) = inv(x)\ proof - - show "dgrp(prod)" by unfold_locales + show \dgrp(prod)\ by unfold_locales from this interpret d: dgrp . \ \Unit\ - have "dgrp.one(prod) = glob_one(prod)" by (rule d.one_def) - also have "... = glob_one(prod) ** one" by (simp add: rone) - also have "... = one" by (simp add: glob_lone) - finally show "dgrp.one(prod) = one" . + have \dgrp.one(prod) = glob_one(prod)\ by (rule d.one_def) + also have \... = glob_one(prod) ** one\ by (simp add: rone) + also have \... = one\ by (simp add: glob_lone) + finally show \dgrp.one(prod) = one\ . \ \Inverse\ - then have "dgrp.inv(prod, x) ** x = inv(x) ** x" by (simp add: glob_linv d.linv linv) - then show "dgrp.inv(prod, x) = inv(x)" by (simp add: rcancel) + then have \dgrp.inv(prod, x) ** x = inv(x) ** x\ by (simp add: glob_linv d.linv linv) + then show \dgrp.inv(prod, x) = inv(x)\ by (simp add: rcancel) qed print_locale! lgrp @@ -760,35 +760,35 @@ text \Equations stored in target\ -lemma "dgrp.one(prod) = one" by (rule one_equation) -lemma "dgrp.inv(prod, x) = inv(x)" by (rule inv_equation) +lemma \dgrp.one(prod) = one\ by (rule one_equation) +lemma \dgrp.inv(prod, x) = inv(x)\ by (rule inv_equation) text \Rewrite morphisms applied\ -lemma "one = glob_one(prod)" by (rule one_def) -lemma "inv(x) = glob_inv(prod, x)" by (rule inv_def) +lemma \one = glob_one(prod)\ by (rule one_def) +lemma \inv(x) = glob_inv(prod, x)\ by (rule inv_def) end text \Interpreted versions\ -lemma "0 = glob_one ((+))" by (rule int.def.one_def) -lemma "- x = glob_inv((+), x)" by (rule int.def.inv_def) +lemma \0 = glob_one ((+))\ by (rule int.def.one_def) +lemma \- x = glob_inv((+), x)\ by (rule int.def.inv_def) text \Roundup applies rewrite morphisms at declaration level in DFS tree\ -locale roundup = fixes x assumes true: "x \ True" +locale roundup = fixes x assumes true: \x \ True\ -sublocale roundup \ sub: roundup x rewrites "x \ True \ True" +sublocale roundup \ sub: roundup \x\ rewrites \x \ True \ True\ apply unfold_locales apply (simp add: true) done -lemma (in roundup) "True \ True \ True" by (rule sub.true) +lemma (in roundup) \True \ True \ True\ by (rule sub.true) section \Interpretation in named contexts\ locale container begin -interpretation "private": roundup True by unfold_locales rule +interpretation "private": roundup \True\ by unfold_locales rule lemmas true_copy = private.true end @@ -806,39 +806,39 @@ notepad begin - interpret "local": lgrp "(+)" "0" "minus" + interpret "local": lgrp \(+)\ \0\ \minus\ by unfold_locales (* subsumed *) { - fix zero :: int - assume "!!x. zero + x = x" "!!x. (-x) + x = zero" - then interpret local_fixed: lgrp "(+)" zero "minus" + fix zero :: \int\ + assume \!!x. zero + x = x\ \!!x. (-x) + x = zero\ + then interpret local_fixed: lgrp \(+)\ \zero\ \minus\ by unfold_locales thm local_fixed.lone - print_dependencies! lgrp "(+)" 0 minus + lgrp "(+)" zero minus + print_dependencies! lgrp \(+)\ \0\ \minus\ + lgrp \(+)\ \zero\ \minus\ } - assume "!!x zero. zero + x = x" "!!x zero. (-x) + x = zero" - then interpret local_free: lgrp "(+)" zero "minus" for zero + assume \!!x zero. zero + x = x\ \!!x zero. (-x) + x = zero\ + then interpret local_free: lgrp \(+)\ \zero\ \minus\ for zero by unfold_locales - thm local_free.lone [where ?zero = 0] + thm local_free.lone [where ?zero = \0\] end notepad begin { fix pand and pnot and por - assume passoc: "\x y z. pand(pand(x, y), z) \ pand(x, pand(y, z))" - and pnotnot: "\x. pnot(pnot(x)) \ x" - and por_def: "\x y. por(x, y) \ pnot(pand(pnot(x), pnot(y)))" - interpret loc: logic_o pand pnot - rewrites por_eq: "\x y. logic_o.lor_o(pand, pnot, x, y) \ por(x, y)" (* FIXME *) + assume passoc: \\x y z. pand(pand(x, y), z) \ pand(x, pand(y, z))\ + and pnotnot: \\x. pnot(pnot(x)) \ x\ + and por_def: \\x y. por(x, y) \ pnot(pand(pnot(x), pnot(y)))\ + interpret loc: logic_o \pand\ \pnot\ + rewrites por_eq: \\x y. logic_o.lor_o(pand, pnot, x, y) \ por(x, y)\ (* FIXME *) proof - - show logic_o: "PROP logic_o(pand, pnot)" using passoc pnotnot by unfold_locales + show logic_o: \PROP logic_o(pand, pnot)\ using passoc pnotnot by unfold_locales fix x y - show "logic_o.lor_o(pand, pnot, x, y) \ por(x, y)" + show \logic_o.lor_o(pand, pnot, x, y) \ por(x, y)\ by (unfold logic_o.lor_o_def [OF logic_o]) (rule por_def [symmetric]) qed print_interps logic_o - have "\x y. por(x, y) \ pnot(pand(pnot(x), pnot(y)))" by (rule loc.lor_o_def) + have \\x y. por(x, y) \ pnot(pand(pnot(x), pnot(y)))\ by (rule loc.lor_o_def) } end diff -r e15f053a42d8 -r e65314985426 src/FOL/ex/Locale_Test/Locale_Test2.thy --- a/src/FOL/ex/Locale_Test/Locale_Test2.thy Thu Jan 03 21:48:05 2019 +0100 +++ b/src/FOL/ex/Locale_Test/Locale_Test2.thy Thu Jan 03 22:19:19 2019 +0100 @@ -8,12 +8,12 @@ imports Locale_Test1 begin -interpretation le1: mixin_thy_merge gle gle' - rewrites "reflexive.less(gle, x, y) \ gless(x, y)" +interpretation le1: mixin_thy_merge \gle\ \gle'\ + rewrites \reflexive.less(gle, x, y) \ gless(x, y)\ proof - - show "mixin_thy_merge(gle, gle')" by unfold_locales + show \mixin_thy_merge(gle, gle')\ by unfold_locales note reflexive = this[unfolded mixin_thy_merge_def, THEN conjunct1] - show "reflexive.less(gle, x, y) \ gless(x, y)" + show \reflexive.less(gle, x, y) \ gless(x, y)\ by (simp add: reflexive.less_def[OF reflexive] gless_def) qed diff -r e15f053a42d8 -r e65314985426 src/FOL/ex/Locale_Test/Locale_Test3.thy --- a/src/FOL/ex/Locale_Test/Locale_Test3.thy Thu Jan 03 21:48:05 2019 +0100 +++ b/src/FOL/ex/Locale_Test/Locale_Test3.thy Thu Jan 03 22:19:19 2019 +0100 @@ -8,12 +8,12 @@ imports Locale_Test1 begin -interpretation le2: mixin_thy_merge gle gle' - rewrites "reflexive.less(gle', x, y) \ gless'(x, y)" +interpretation le2: mixin_thy_merge \gle\ \gle'\ + rewrites \reflexive.less(gle', x, y) \ gless'(x, y)\ proof - - show "mixin_thy_merge(gle, gle')" by unfold_locales + show \mixin_thy_merge(gle, gle')\ by unfold_locales note reflexive = this[unfolded mixin_thy_merge_def, THEN conjunct2] - show "reflexive.less(gle', x, y) \ gless'(x, y)" + show \reflexive.less(gle', x, y) \ gless'(x, y)\ by (simp add: reflexive.less_def[OF reflexive] gless'_def) qed diff -r e15f053a42d8 -r e65314985426 src/FOL/ex/Miniscope.thy --- a/src/FOL/ex/Miniscope.thy Thu Jan 03 21:48:05 2019 +0100 +++ b/src/FOL/ex/Miniscope.thy Thu Jan 03 22:19:19 2019 +0100 @@ -18,14 +18,14 @@ subsubsection \de Morgan laws\ lemma demorgans1: - "\ (P \ Q) \ \ P \ \ Q" - "\ (P \ Q) \ \ P \ \ Q" - "\ \ P \ P" + \\ (P \ Q) \ \ P \ \ Q\ + \\ (P \ Q) \ \ P \ \ Q\ + \\ \ P \ P\ by blast+ lemma demorgans2: - "\P. \ (\x. P(x)) \ (\x. \ P(x))" - "\P. \ (\x. P(x)) \ (\x. \ P(x))" + \\P. \ (\x. P(x)) \ (\x. \ P(x))\ + \\P. \ (\x. P(x)) \ (\x. \ P(x))\ by blast+ lemmas demorgans = demorgans1 demorgans2 @@ -33,10 +33,10 @@ (*** Removal of --> and <-> (positive and negative occurrences) ***) (*Last one is important for computing a compact CNF*) lemma nnf_simps: - "(P \ Q) \ (\ P \ Q)" - "\ (P \ Q) \ (P \ \ Q)" - "(P \ Q) \ (\ P \ Q) \ (\ Q \ P)" - "\ (P \ Q) \ (P \ Q) \ (\ P \ \ Q)" + \(P \ Q) \ (\ P \ Q)\ + \\ (P \ Q) \ (P \ \ Q)\ + \(P \ Q) \ (\ P \ Q) \ (\ Q \ P)\ + \\ (P \ Q) \ (P \ Q) \ (\ P \ \ Q)\ by blast+ @@ -45,24 +45,24 @@ subsubsection \Pushing in the existential quantifiers\ lemma ex_simps: - "(\x. P) \ P" - "\P Q. (\x. P(x) \ Q) \ (\x. P(x)) \ Q" - "\P Q. (\x. P \ Q(x)) \ P \ (\x. Q(x))" - "\P Q. (\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))" - "\P Q. (\x. P(x) \ Q) \ (\x. P(x)) \ Q" - "\P Q. (\x. P \ Q(x)) \ P \ (\x. Q(x))" + \(\x. P) \ P\ + \\P Q. (\x. P(x) \ Q) \ (\x. P(x)) \ Q\ + \\P Q. (\x. P \ Q(x)) \ P \ (\x. Q(x))\ + \\P Q. (\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))\ + \\P Q. (\x. P(x) \ Q) \ (\x. P(x)) \ Q\ + \\P Q. (\x. P \ Q(x)) \ P \ (\x. Q(x))\ by blast+ subsubsection \Pushing in the universal quantifiers\ lemma all_simps: - "(\x. P) \ P" - "\P Q. (\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))" - "\P Q. (\x. P(x) \ Q) \ (\x. P(x)) \ Q" - "\P Q. (\x. P \ Q(x)) \ P \ (\x. Q(x))" - "\P Q. (\x. P(x) \ Q) \ (\x. P(x)) \ Q" - "\P Q. (\x. P \ Q(x)) \ P \ (\x. Q(x))" + \(\x. P) \ P\ + \\P Q. (\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))\ + \\P Q. (\x. P(x) \ Q) \ (\x. P(x)) \ Q\ + \\P Q. (\x. P \ Q(x)) \ P \ (\x. Q(x))\ + \\P Q. (\x. P(x) \ Q) \ (\x. P(x)) \ Q\ + \\P Q. (\x. P \ Q(x)) \ P \ (\x. Q(x))\ by blast+ lemmas mini_simps = demorgans nnf_simps ex_simps all_simps diff -r e15f053a42d8 -r e65314985426 src/FOL/ex/Nat.thy --- a/src/FOL/ex/Nat.thy Thu Jan 03 21:48:05 2019 +0100 +++ b/src/FOL/ex/Nat.thy Thu Jan 03 22:19:19 2019 +0100 @@ -10,27 +10,27 @@ begin typedecl nat -instance nat :: "term" .. +instance nat :: \term\ .. axiomatization - Zero :: nat (\0\) and - Suc :: "nat => nat" and - rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a" + Zero :: \nat\ (\0\) and + Suc :: \nat => nat\ and + rec :: \[nat, 'a, [nat, 'a] => 'a] => 'a\ where - induct: "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)" and - Suc_inject: "Suc(m)=Suc(n) ==> m=n" and - Suc_neq_0: "Suc(m)=0 ==> R" and - rec_0: "rec(0,a,f) = a" and - rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m,a,f))" + induct: \[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)\ and + Suc_inject: \Suc(m)=Suc(n) ==> m=n\ and + Suc_neq_0: \Suc(m)=0 ==> R\ and + rec_0: \rec(0,a,f) = a\ and + rec_Suc: \rec(Suc(m), a, f) = f(m, rec(m,a,f))\ -definition add :: "[nat, nat] => nat" (infixl \+\ 60) - where "m + n == rec(m, n, %x y. Suc(y))" +definition add :: \[nat, nat] => nat\ (infixl \+\ 60) + where \m + n == rec(m, n, %x y. Suc(y))\ subsection \Proofs about the natural numbers\ -lemma Suc_n_not_n: "Suc(k) \ k" -apply (rule_tac n = k in induct) +lemma Suc_n_not_n: \Suc(k) \ k\ +apply (rule_tac n = \k\ in induct) apply (rule notI) apply (erule Suc_neq_0) apply (rule notI) @@ -38,7 +38,7 @@ apply (erule Suc_inject) done -lemma "(k+m)+n = k+(m+n)" +lemma \(k+m)+n = k+(m+n)\ apply (rule induct) back back @@ -48,37 +48,37 @@ back oops -lemma add_0 [simp]: "0+n = n" +lemma add_0 [simp]: \0+n = n\ apply (unfold add_def) apply (rule rec_0) done -lemma add_Suc [simp]: "Suc(m)+n = Suc(m+n)" +lemma add_Suc [simp]: \Suc(m)+n = Suc(m+n)\ apply (unfold add_def) apply (rule rec_Suc) done -lemma add_assoc: "(k+m)+n = k+(m+n)" -apply (rule_tac n = k in induct) +lemma add_assoc: \(k+m)+n = k+(m+n)\ +apply (rule_tac n = \k\ in induct) apply simp apply simp done -lemma add_0_right: "m+0 = m" -apply (rule_tac n = m in induct) +lemma add_0_right: \m+0 = m\ +apply (rule_tac n = \m\ in induct) apply simp apply simp done -lemma add_Suc_right: "m+Suc(n) = Suc(m+n)" -apply (rule_tac n = m in induct) +lemma add_Suc_right: \m+Suc(n) = Suc(m+n)\ +apply (rule_tac n = \m\ in induct) apply simp_all done lemma - assumes prem: "!!n. f(Suc(n)) = Suc(f(n))" - shows "f(i+j) = i+f(j)" -apply (rule_tac n = i in induct) + assumes prem: \!!n. f(Suc(n)) = Suc(f(n))\ + shows \f(i+j) = i+f(j)\ +apply (rule_tac n = \i\ in induct) apply simp apply (simp add: prem) done diff -r e15f053a42d8 -r e65314985426 src/FOL/ex/Nat_Class.thy --- a/src/FOL/ex/Nat_Class.thy Thu Jan 03 21:48:05 2019 +0100 +++ b/src/FOL/ex/Nat_Class.thy Thu Jan 03 22:19:19 2019 +0100 @@ -16,21 +16,21 @@ \ class nat = - fixes Zero :: 'a (\0\) - and Suc :: "'a \ 'a" - and rec :: "'a \ 'a \ ('a \ 'a \ 'a) \ 'a" - assumes induct: "P(0) \ (\x. P(x) \ P(Suc(x))) \ P(n)" - and Suc_inject: "Suc(m) = Suc(n) \ m = n" - and Suc_neq_Zero: "Suc(m) = 0 \ R" - and rec_Zero: "rec(0, a, f) = a" - and rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))" + fixes Zero :: \'a\ (\0\) + and Suc :: \'a \ 'a\ + and rec :: \'a \ 'a \ ('a \ 'a \ 'a) \ 'a\ + assumes induct: \P(0) \ (\x. P(x) \ P(Suc(x))) \ P(n)\ + and Suc_inject: \Suc(m) = Suc(n) \ m = n\ + and Suc_neq_Zero: \Suc(m) = 0 \ R\ + and rec_Zero: \rec(0, a, f) = a\ + and rec_Suc: \rec(Suc(m), a, f) = f(m, rec(m, a, f))\ begin -definition add :: "'a \ 'a \ 'a" (infixl \+\ 60) - where "m + n = rec(m, n, \x y. Suc(y))" +definition add :: \'a \ 'a \ 'a\ (infixl \+\ 60) + where \m + n = rec(m, n, \x y. Suc(y))\ -lemma Suc_n_not_n: "Suc(k) \ (k::'a)" - apply (rule_tac n = k in induct) +lemma Suc_n_not_n: \Suc(k) \ (k::'a)\ + apply (rule_tac n = \k\ in induct) apply (rule notI) apply (erule Suc_neq_Zero) apply (rule notI) @@ -38,7 +38,7 @@ apply (erule Suc_inject) done -lemma "(k + m) + n = k + (m + n)" +lemma \(k + m) + n = k + (m + n)\ apply (rule induct) back back @@ -47,37 +47,37 @@ back oops -lemma add_Zero [simp]: "0 + n = n" +lemma add_Zero [simp]: \0 + n = n\ apply (unfold add_def) apply (rule rec_Zero) done -lemma add_Suc [simp]: "Suc(m) + n = Suc(m + n)" +lemma add_Suc [simp]: \Suc(m) + n = Suc(m + n)\ apply (unfold add_def) apply (rule rec_Suc) done -lemma add_assoc: "(k + m) + n = k + (m + n)" - apply (rule_tac n = k in induct) +lemma add_assoc: \(k + m) + n = k + (m + n)\ + apply (rule_tac n = \k\ in induct) apply simp apply simp done -lemma add_Zero_right: "m + 0 = m" - apply (rule_tac n = m in induct) +lemma add_Zero_right: \m + 0 = m\ + apply (rule_tac n = \m\ in induct) apply simp apply simp done -lemma add_Suc_right: "m + Suc(n) = Suc(m + n)" - apply (rule_tac n = m in induct) +lemma add_Suc_right: \m + Suc(n) = Suc(m + n)\ + apply (rule_tac n = \m\ in induct) apply simp_all done lemma - assumes prem: "\n. f(Suc(n)) = Suc(f(n))" - shows "f(i + j) = i + f(j)" - apply (rule_tac n = i in induct) + assumes prem: \\n. f(Suc(n)) = Suc(f(n))\ + shows \f(i + j) = i + f(j)\ + apply (rule_tac n = \i\ in induct) apply simp apply (simp add: prem) done diff -r e15f053a42d8 -r e65314985426 src/FOL/ex/Natural_Numbers.thy --- a/src/FOL/ex/Natural_Numbers.thy Thu Jan 03 21:48:05 2019 +0100 +++ b/src/FOL/ex/Natural_Numbers.thy Thu Jan 03 22:19:19 2019 +0100 @@ -14,59 +14,59 @@ \ typedecl nat -instance nat :: "term" .. +instance nat :: \term\ .. axiomatization - Zero :: nat (\0\) and - Suc :: "nat => nat" and - rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a" + Zero :: \nat\ (\0\) and + Suc :: \nat => nat\ and + rec :: \[nat, 'a, [nat, 'a] => 'a] => 'a\ where induct [case_names 0 Suc, induct type: nat]: - "P(0) ==> (!!x. P(x) ==> P(Suc(x))) ==> P(n)" and - Suc_inject: "Suc(m) = Suc(n) ==> m = n" and - Suc_neq_0: "Suc(m) = 0 ==> R" and - rec_0: "rec(0, a, f) = a" and - rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))" + \P(0) ==> (!!x. P(x) ==> P(Suc(x))) ==> P(n)\ and + Suc_inject: \Suc(m) = Suc(n) ==> m = n\ and + Suc_neq_0: \Suc(m) = 0 ==> R\ and + rec_0: \rec(0, a, f) = a\ and + rec_Suc: \rec(Suc(m), a, f) = f(m, rec(m, a, f))\ -lemma Suc_n_not_n: "Suc(k) \ k" -proof (induct k) - show "Suc(0) \ 0" +lemma Suc_n_not_n: \Suc(k) \ k\ +proof (induct \k\) + show \Suc(0) \ 0\ proof - assume "Suc(0) = 0" - then show False by (rule Suc_neq_0) + assume \Suc(0) = 0\ + then show \False\ by (rule Suc_neq_0) qed next - fix n assume hyp: "Suc(n) \ n" - show "Suc(Suc(n)) \ Suc(n)" + fix n assume hyp: \Suc(n) \ n\ + show \Suc(Suc(n)) \ Suc(n)\ proof - assume "Suc(Suc(n)) = Suc(n)" - then have "Suc(n) = n" by (rule Suc_inject) - with hyp show False by contradiction + assume \Suc(Suc(n)) = Suc(n)\ + then have \Suc(n) = n\ by (rule Suc_inject) + with hyp show \False\ by contradiction qed qed -definition add :: "nat => nat => nat" (infixl \+\ 60) - where "m + n = rec(m, n, \x y. Suc(y))" +definition add :: \nat => nat => nat\ (infixl \+\ 60) + where \m + n = rec(m, n, \x y. Suc(y))\ -lemma add_0 [simp]: "0 + n = n" +lemma add_0 [simp]: \0 + n = n\ unfolding add_def by (rule rec_0) -lemma add_Suc [simp]: "Suc(m) + n = Suc(m + n)" +lemma add_Suc [simp]: \Suc(m) + n = Suc(m + n)\ unfolding add_def by (rule rec_Suc) -lemma add_assoc: "(k + m) + n = k + (m + n)" - by (induct k) simp_all +lemma add_assoc: \(k + m) + n = k + (m + n)\ + by (induct \k\) simp_all -lemma add_0_right: "m + 0 = m" - by (induct m) simp_all +lemma add_0_right: \m + 0 = m\ + by (induct \m\) simp_all -lemma add_Suc_right: "m + Suc(n) = Suc(m + n)" - by (induct m) simp_all +lemma add_Suc_right: \m + Suc(n) = Suc(m + n)\ + by (induct \m\) simp_all lemma - assumes "!!n. f(Suc(n)) = Suc(f(n))" - shows "f(i + j) = i + f(j)" - using assms by (induct i) simp_all + assumes \!!n. f(Suc(n)) = Suc(f(n))\ + shows \f(i + j) = i + f(j)\ + using assms by (induct \i\) simp_all end diff -r e15f053a42d8 -r e65314985426 src/FOL/ex/Prolog.thy --- a/src/FOL/ex/Prolog.thy Thu Jan 03 21:48:05 2019 +0100 +++ b/src/FOL/ex/Prolog.thy Thu Jan 03 22:19:19 2019 +0100 @@ -10,31 +10,31 @@ begin typedecl 'a list -instance list :: ("term") "term" .. +instance list :: (\term\) \term\ .. axiomatization - Nil :: "'a list" and - Cons :: "['a, 'a list]=> 'a list" (infixr \:\ 60) and - app :: "['a list, 'a list, 'a list] => o" and - rev :: "['a list, 'a list] => o" + Nil :: \'a list\ and + Cons :: \['a, 'a list]=> 'a list\ (infixr \:\ 60) and + app :: \['a list, 'a list, 'a list] => o\ and + rev :: \['a list, 'a list] => o\ where - appNil: "app(Nil,ys,ys)" and - appCons: "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)" and - revNil: "rev(Nil,Nil)" and - revCons: "[| rev(xs,ys); app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)" + appNil: \app(Nil,ys,ys)\ and + appCons: \app(xs,ys,zs) ==> app(x:xs, ys, x:zs)\ and + revNil: \rev(Nil,Nil)\ and + revCons: \[| rev(xs,ys); app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)\ -schematic_goal "app(a:b:c:Nil, d:e:Nil, ?x)" +schematic_goal \app(a:b:c:Nil, d:e:Nil, ?x)\ apply (rule appNil appCons) apply (rule appNil appCons) apply (rule appNil appCons) apply (rule appNil appCons) done -schematic_goal "app(?x, c:d:Nil, a:b:c:d:Nil)" +schematic_goal \app(?x, c:d:Nil, a:b:c:d:Nil)\ apply (rule appNil appCons)+ done -schematic_goal "app(?x, ?y, a:b:c:d:Nil)" +schematic_goal \app(?x, ?y, a:b:c:d:Nil)\ apply (rule appNil appCons)+ back back @@ -47,15 +47,15 @@ lemmas rules = appNil appCons revNil revCons -schematic_goal "rev(a:b:c:d:Nil, ?x)" +schematic_goal \rev(a:b:c:d:Nil, ?x)\ apply (rule rules)+ done -schematic_goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)" +schematic_goal \rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)\ apply (rule rules)+ done -schematic_goal "rev(?x, a:b:c:Nil)" +schematic_goal \rev(?x, a:b:c:Nil)\ apply (rule rules)+ \ \does not solve it directly!\ back back @@ -67,23 +67,23 @@ DEPTH_FIRST (has_fewer_prems 1) (resolve_tac ctxt @{thms rules} 1) \ -schematic_goal "rev(?x, a:b:c:Nil)" +schematic_goal \rev(?x, a:b:c:Nil)\ apply (tactic \prolog_tac @{context}\) done -schematic_goal "rev(a:?x:c:?y:Nil, d:?z:b:?u)" +schematic_goal \rev(a:?x:c:?y:Nil, d:?z:b:?u)\ apply (tactic \prolog_tac @{context}\) done (*rev([a..p], ?w) requires 153 inferences *) -schematic_goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)" +schematic_goal \rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)\ apply (tactic \ DEPTH_SOLVE (resolve_tac @{context} ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1)\) done (*?x has 16, ?y has 32; rev(?y,?w) requires 561 (rather large) inferences total inferences = 2 + 1 + 17 + 561 = 581*) -schematic_goal "a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x \ app(?x,?x,?y) \ rev(?y,?w)" +schematic_goal \a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x \ app(?x,?x,?y) \ rev(?y,?w)\ apply (tactic \ DEPTH_SOLVE (resolve_tac @{context} ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1)\) done diff -r e15f053a42d8 -r e65314985426 src/FOL/ex/Propositional_Cla.thy --- a/src/FOL/ex/Propositional_Cla.thy Thu Jan 03 21:48:05 2019 +0100 +++ b/src/FOL/ex/Propositional_Cla.thy Thu Jan 03 22:19:19 2019 +0100 @@ -11,110 +11,110 @@ text \commutative laws of \\\ and \\\\ -lemma "P \ Q \ Q \ P" +lemma \P \ Q \ Q \ P\ by (tactic "IntPr.fast_tac @{context} 1") -lemma "P \ Q \ Q \ P" +lemma \P \ Q \ Q \ P\ by fast text \associative laws of \\\ and \\\\ -lemma "(P \ Q) \ R \ P \ (Q \ R)" +lemma \(P \ Q) \ R \ P \ (Q \ R)\ by fast -lemma "(P \ Q) \ R \ P \ (Q \ R)" +lemma \(P \ Q) \ R \ P \ (Q \ R)\ by fast text \distributive laws of \\\ and \\\\ -lemma "(P \ Q) \ R \ (P \ R) \ (Q \ R)" +lemma \(P \ Q) \ R \ (P \ R) \ (Q \ R)\ by fast -lemma "(P \ R) \ (Q \ R) \ (P \ Q) \ R" +lemma \(P \ R) \ (Q \ R) \ (P \ Q) \ R\ by fast -lemma "(P \ Q) \ R \ (P \ R) \ (Q \ R)" +lemma \(P \ Q) \ R \ (P \ R) \ (Q \ R)\ by fast -lemma "(P \ R) \ (Q \ R) \ (P \ Q) \ R" +lemma \(P \ R) \ (Q \ R) \ (P \ Q) \ R\ by fast text \Laws involving implication\ -lemma "(P \ R) \ (Q \ R) \ (P \ Q \ R)" +lemma \(P \ R) \ (Q \ R) \ (P \ Q \ R)\ by fast -lemma "(P \ Q \ R) \ (P \ (Q \ R))" +lemma \(P \ Q \ R) \ (P \ (Q \ R))\ by fast -lemma "((P \ R) \ R) \ ((Q \ R) \ R) \ (P \ Q \ R) \ R" +lemma \((P \ R) \ R) \ ((Q \ R) \ R) \ (P \ Q \ R) \ R\ by fast -lemma "\ (P \ R) \ \ (Q \ R) \ \ (P \ Q \ R)" +lemma \\ (P \ R) \ \ (Q \ R) \ \ (P \ Q \ R)\ by fast -lemma "(P \ Q \ R) \ (P \ Q) \ (P \ R)" +lemma \(P \ Q \ R) \ (P \ Q) \ (P \ R)\ by fast text \Propositions-as-types\ \ \The combinator K\ -lemma "P \ (Q \ P)" +lemma \P \ (Q \ P)\ by fast \ \The combinator S\ -lemma "(P \ Q \ R) \ (P \ Q) \ (P \ R)" +lemma \(P \ Q \ R) \ (P \ Q) \ (P \ R)\ by fast \ \Converse is classical\ -lemma "(P \ Q) \ (P \ R) \ (P \ Q \ R)" +lemma \(P \ Q) \ (P \ R) \ (P \ Q \ R)\ by fast -lemma "(P \ Q) \ (\ Q \ \ P)" +lemma \(P \ Q) \ (\ Q \ \ P)\ by fast text \Schwichtenberg's examples (via T. Nipkow)\ -lemma stab_imp: "(((Q \ R) \ R) \ Q) \ (((P \ Q) \ R) \ R) \ P \ Q" +lemma stab_imp: \(((Q \ R) \ R) \ Q) \ (((P \ Q) \ R) \ R) \ P \ Q\ by fast lemma stab_to_peirce: - "(((P \ R) \ R) \ P) \ (((Q \ R) \ R) \ Q) - \ ((P \ Q) \ P) \ P" + \(((P \ R) \ R) \ P) \ (((Q \ R) \ R) \ Q) + \ ((P \ Q) \ P) \ P\ by fast lemma peirce_imp1: - "(((Q \ R) \ Q) \ Q) - \ (((P \ Q) \ R) \ P \ Q) \ P \ Q" + \(((Q \ R) \ Q) \ Q) + \ (((P \ Q) \ R) \ P \ Q) \ P \ Q\ by fast -lemma peirce_imp2: "(((P \ R) \ P) \ P) \ ((P \ Q \ R) \ P) \ P" +lemma peirce_imp2: \(((P \ R) \ P) \ P) \ ((P \ Q \ R) \ P) \ P\ by fast -lemma mints: "((((P \ Q) \ P) \ P) \ Q) \ Q" +lemma mints: \((((P \ Q) \ P) \ P) \ Q) \ Q\ by fast -lemma mints_solovev: "(P \ (Q \ R) \ Q) \ ((P \ Q) \ R) \ R" +lemma mints_solovev: \(P \ (Q \ R) \ Q) \ ((P \ Q) \ R) \ R\ by fast lemma tatsuta: - "(((P7 \ P1) \ P10) \ P4 \ P5) + \(((P7 \ P1) \ P10) \ P4 \ P5) \ (((P8 \ P2) \ P9) \ P3 \ P10) \ (P1 \ P8) \ P6 \ P7 \ (((P3 \ P2) \ P9) \ P4) - \ (P1 \ P3) \ (((P6 \ P1) \ P2) \ P9) \ P5" + \ (P1 \ P3) \ (((P6 \ P1) \ P2) \ P9) \ P5\ by fast lemma tatsuta1: - "(((P8 \ P2) \ P9) \ P3 \ P10) + \(((P8 \ P2) \ P9) \ P3 \ P10) \ (((P3 \ P2) \ P9) \ P4) \ (((P6 \ P1) \ P2) \ P9) \ (((P7 \ P1) \ P10) \ P4 \ P5) - \ (P1 \ P3) \ (P1 \ P8) \ P6 \ P7 \ P5" + \ (P1 \ P3) \ (P1 \ P8) \ P6 \ P7 \ P5\ by fast end diff -r e15f053a42d8 -r e65314985426 src/FOL/ex/Propositional_Int.thy --- a/src/FOL/ex/Propositional_Int.thy Thu Jan 03 21:48:05 2019 +0100 +++ b/src/FOL/ex/Propositional_Int.thy Thu Jan 03 22:19:19 2019 +0100 @@ -11,110 +11,110 @@ text \commutative laws of \\\ and \\\\ -lemma "P \ Q \ Q \ P" +lemma \P \ Q \ Q \ P\ by (tactic "IntPr.fast_tac @{context} 1") -lemma "P \ Q \ Q \ P" +lemma \P \ Q \ Q \ P\ by (tactic "IntPr.fast_tac @{context} 1") text \associative laws of \\\ and \\\\ -lemma "(P \ Q) \ R \ P \ (Q \ R)" +lemma \(P \ Q) \ R \ P \ (Q \ R)\ by (tactic "IntPr.fast_tac @{context} 1") -lemma "(P \ Q) \ R \ P \ (Q \ R)" +lemma \(P \ Q) \ R \ P \ (Q \ R)\ by (tactic "IntPr.fast_tac @{context} 1") text \distributive laws of \\\ and \\\\ -lemma "(P \ Q) \ R \ (P \ R) \ (Q \ R)" +lemma \(P \ Q) \ R \ (P \ R) \ (Q \ R)\ by (tactic "IntPr.fast_tac @{context} 1") -lemma "(P \ R) \ (Q \ R) \ (P \ Q) \ R" +lemma \(P \ R) \ (Q \ R) \ (P \ Q) \ R\ by (tactic "IntPr.fast_tac @{context} 1") -lemma "(P \ Q) \ R \ (P \ R) \ (Q \ R)" +lemma \(P \ Q) \ R \ (P \ R) \ (Q \ R)\ by (tactic "IntPr.fast_tac @{context} 1") -lemma "(P \ R) \ (Q \ R) \ (P \ Q) \ R" +lemma \(P \ R) \ (Q \ R) \ (P \ Q) \ R\ by (tactic "IntPr.fast_tac @{context} 1") text \Laws involving implication\ -lemma "(P \ R) \ (Q \ R) \ (P \ Q \ R)" +lemma \(P \ R) \ (Q \ R) \ (P \ Q \ R)\ by (tactic "IntPr.fast_tac @{context} 1") -lemma "(P \ Q \ R) \ (P \ (Q \ R))" +lemma \(P \ Q \ R) \ (P \ (Q \ R))\ by (tactic "IntPr.fast_tac @{context} 1") -lemma "((P \ R) \ R) \ ((Q \ R) \ R) \ (P \ Q \ R) \ R" +lemma \((P \ R) \ R) \ ((Q \ R) \ R) \ (P \ Q \ R) \ R\ by (tactic "IntPr.fast_tac @{context} 1") -lemma "\ (P \ R) \ \ (Q \ R) \ \ (P \ Q \ R)" +lemma \\ (P \ R) \ \ (Q \ R) \ \ (P \ Q \ R)\ by (tactic "IntPr.fast_tac @{context} 1") -lemma "(P \ Q \ R) \ (P \ Q) \ (P \ R)" +lemma \(P \ Q \ R) \ (P \ Q) \ (P \ R)\ by (tactic "IntPr.fast_tac @{context} 1") text \Propositions-as-types\ \ \The combinator K\ -lemma "P \ (Q \ P)" +lemma \P \ (Q \ P)\ by (tactic "IntPr.fast_tac @{context} 1") \ \The combinator S\ -lemma "(P \ Q \ R) \ (P \ Q) \ (P \ R)" +lemma \(P \ Q \ R) \ (P \ Q) \ (P \ R)\ by (tactic "IntPr.fast_tac @{context} 1") \ \Converse is classical\ -lemma "(P \ Q) \ (P \ R) \ (P \ Q \ R)" +lemma \(P \ Q) \ (P \ R) \ (P \ Q \ R)\ by (tactic "IntPr.fast_tac @{context} 1") -lemma "(P \ Q) \ (\ Q \ \ P)" +lemma \(P \ Q) \ (\ Q \ \ P)\ by (tactic "IntPr.fast_tac @{context} 1") text \Schwichtenberg's examples (via T. Nipkow)\ -lemma stab_imp: "(((Q \ R) \ R) \ Q) \ (((P \ Q) \ R) \ R) \ P \ Q" +lemma stab_imp: \(((Q \ R) \ R) \ Q) \ (((P \ Q) \ R) \ R) \ P \ Q\ by (tactic "IntPr.fast_tac @{context} 1") lemma stab_to_peirce: - "(((P \ R) \ R) \ P) \ (((Q \ R) \ R) \ Q) - \ ((P \ Q) \ P) \ P" + \(((P \ R) \ R) \ P) \ (((Q \ R) \ R) \ Q) + \ ((P \ Q) \ P) \ P\ by (tactic "IntPr.fast_tac @{context} 1") lemma peirce_imp1: - "(((Q \ R) \ Q) \ Q) - \ (((P \ Q) \ R) \ P \ Q) \ P \ Q" + \(((Q \ R) \ Q) \ Q) + \ (((P \ Q) \ R) \ P \ Q) \ P \ Q\ by (tactic "IntPr.fast_tac @{context} 1") -lemma peirce_imp2: "(((P \ R) \ P) \ P) \ ((P \ Q \ R) \ P) \ P" +lemma peirce_imp2: \(((P \ R) \ P) \ P) \ ((P \ Q \ R) \ P) \ P\ by (tactic "IntPr.fast_tac @{context} 1") -lemma mints: "((((P \ Q) \ P) \ P) \ Q) \ Q" +lemma mints: \((((P \ Q) \ P) \ P) \ Q) \ Q\ by (tactic "IntPr.fast_tac @{context} 1") -lemma mints_solovev: "(P \ (Q \ R) \ Q) \ ((P \ Q) \ R) \ R" +lemma mints_solovev: \(P \ (Q \ R) \ Q) \ ((P \ Q) \ R) \ R\ by (tactic "IntPr.fast_tac @{context} 1") lemma tatsuta: - "(((P7 \ P1) \ P10) \ P4 \ P5) + \(((P7 \ P1) \ P10) \ P4 \ P5) \ (((P8 \ P2) \ P9) \ P3 \ P10) \ (P1 \ P8) \ P6 \ P7 \ (((P3 \ P2) \ P9) \ P4) - \ (P1 \ P3) \ (((P6 \ P1) \ P2) \ P9) \ P5" + \ (P1 \ P3) \ (((P6 \ P1) \ P2) \ P9) \ P5\ by (tactic "IntPr.fast_tac @{context} 1") lemma tatsuta1: - "(((P8 \ P2) \ P9) \ P3 \ P10) + \(((P8 \ P2) \ P9) \ P3 \ P10) \ (((P3 \ P2) \ P9) \ P4) \ (((P6 \ P1) \ P2) \ P9) \ (((P7 \ P1) \ P10) \ P4 \ P5) - \ (P1 \ P3) \ (P1 \ P8) \ P6 \ P7 \ P5" + \ (P1 \ P3) \ (P1 \ P8) \ P6 \ P7 \ P5\ by (tactic "IntPr.fast_tac @{context} 1") end diff -r e15f053a42d8 -r e65314985426 src/FOL/ex/Quantifiers_Cla.thy --- a/src/FOL/ex/Quantifiers_Cla.thy Thu Jan 03 21:48:05 2019 +0100 +++ b/src/FOL/ex/Quantifiers_Cla.thy Thu Jan 03 22:19:19 2019 +0100 @@ -9,92 +9,92 @@ imports FOL begin -lemma "(\x y. P(x,y)) \ (\y x. P(x,y))" +lemma \(\x y. P(x,y)) \ (\y x. P(x,y))\ by fast -lemma "(\x y. P(x,y)) \ (\y x. P(x,y))" +lemma \(\x y. P(x,y)) \ (\y x. P(x,y))\ by fast text \Converse is false.\ -lemma "(\x. P(x)) \ (\x. Q(x)) \ (\x. P(x) \ Q(x))" +lemma \(\x. P(x)) \ (\x. Q(x)) \ (\x. P(x) \ Q(x))\ by fast -lemma "(\x. P \ Q(x)) \ (P \ (\x. Q(x)))" +lemma \(\x. P \ Q(x)) \ (P \ (\x. Q(x)))\ by fast -lemma "(\x. P(x) \ Q) \ ((\x. P(x)) \ Q)" +lemma \(\x. P(x) \ Q) \ ((\x. P(x)) \ Q)\ by fast text \Some harder ones.\ -lemma "(\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))" +lemma \(\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))\ by fast \ \Converse is false.\ -lemma "(\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))" +lemma \(\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))\ by fast text \Basic test of quantifier reasoning.\ \ \TRUE\ -lemma "(\y. \x. Q(x,y)) \ (\x. \y. Q(x,y))" +lemma \(\y. \x. Q(x,y)) \ (\x. \y. Q(x,y))\ by fast -lemma "(\x. Q(x)) \ (\x. Q(x))" +lemma \(\x. Q(x)) \ (\x. Q(x))\ by fast text \The following should fail, as they are false!\ -lemma "(\x. \y. Q(x,y)) \ (\y. \x. Q(x,y))" +lemma \(\x. \y. Q(x,y)) \ (\y. \x. Q(x,y))\ apply fast? oops -lemma "(\x. Q(x)) \ (\x. Q(x))" +lemma \(\x. Q(x)) \ (\x. Q(x))\ apply fast? oops -schematic_goal "P(?a) \ (\x. P(x))" +schematic_goal \P(?a) \ (\x. P(x))\ apply fast? oops -schematic_goal "(P(?a) \ (\x. Q(x))) \ (\x. P(x) \ Q(x))" +schematic_goal \(P(?a) \ (\x. Q(x))) \ (\x. P(x) \ Q(x))\ apply fast? oops text \Back to things that are provable \dots\ -lemma "(\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))" +lemma \(\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))\ by fast text \An example of why \exI\ should be delayed as long as possible.\ -lemma "(P \ (\x. Q(x))) \ P \ (\x. Q(x))" +lemma \(P \ (\x. Q(x))) \ P \ (\x. Q(x))\ by fast -schematic_goal "(\x. P(x) \ Q(f(x))) \ (\x. Q(x) \ R(g(x))) \ P(d) \ R(?a)" +schematic_goal \(\x. P(x) \ Q(f(x))) \ (\x. Q(x) \ R(g(x))) \ P(d) \ R(?a)\ by fast -lemma "(\x. Q(x)) \ (\x. Q(x))" +lemma \(\x. Q(x)) \ (\x. Q(x))\ by fast text \Some slow ones\ text \Principia Mathematica *11.53\ -lemma "(\x y. P(x) \ Q(y)) \ ((\x. P(x)) \ (\y. Q(y)))" +lemma \(\x y. P(x) \ Q(y)) \ ((\x. P(x)) \ (\y. Q(y)))\ by fast (*Principia Mathematica *11.55 *) -lemma "(\x y. P(x) \ Q(x,y)) \ (\x. P(x) \ (\y. Q(x,y)))" +lemma \(\x y. P(x) \ Q(x,y)) \ (\x. P(x) \ (\y. Q(x,y)))\ by fast (*Principia Mathematica *11.61 *) -lemma "(\y. \x. P(x) \ Q(x,y)) \ (\x. P(x) \ (\y. Q(x,y)))" +lemma \(\y. \x. P(x) \ Q(x,y)) \ (\x. P(x) \ (\y. Q(x,y)))\ by fast end diff -r e15f053a42d8 -r e65314985426 src/FOL/ex/Quantifiers_Int.thy --- a/src/FOL/ex/Quantifiers_Int.thy Thu Jan 03 21:48:05 2019 +0100 +++ b/src/FOL/ex/Quantifiers_Int.thy Thu Jan 03 22:19:19 2019 +0100 @@ -9,92 +9,92 @@ imports IFOL begin -lemma "(\x y. P(x,y)) \ (\y x. P(x,y))" +lemma \(\x y. P(x,y)) \ (\y x. P(x,y))\ by (tactic "IntPr.fast_tac @{context} 1") -lemma "(\x y. P(x,y)) \ (\y x. P(x,y))" +lemma \(\x y. P(x,y)) \ (\y x. P(x,y))\ by (tactic "IntPr.fast_tac @{context} 1") \ \Converse is false\ -lemma "(\x. P(x)) \ (\x. Q(x)) \ (\x. P(x) \ Q(x))" +lemma \(\x. P(x)) \ (\x. Q(x)) \ (\x. P(x) \ Q(x))\ by (tactic "IntPr.fast_tac @{context} 1") -lemma "(\x. P \ Q(x)) \ (P \ (\x. Q(x)))" +lemma \(\x. P \ Q(x)) \ (P \ (\x. Q(x)))\ by (tactic "IntPr.fast_tac @{context} 1") -lemma "(\x. P(x) \ Q) \ ((\x. P(x)) \ Q)" +lemma \(\x. P(x) \ Q) \ ((\x. P(x)) \ Q)\ by (tactic "IntPr.fast_tac @{context} 1") text \Some harder ones\ -lemma "(\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))" +lemma \(\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))\ by (tactic "IntPr.fast_tac @{context} 1") \ \Converse is false\ -lemma "(\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))" +lemma \(\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))\ by (tactic "IntPr.fast_tac @{context} 1") text \Basic test of quantifier reasoning\ \ \TRUE\ -lemma "(\y. \x. Q(x,y)) \ (\x. \y. Q(x,y))" +lemma \(\y. \x. Q(x,y)) \ (\x. \y. Q(x,y))\ by (tactic "IntPr.fast_tac @{context} 1") -lemma "(\x. Q(x)) \ (\x. Q(x))" +lemma \(\x. Q(x)) \ (\x. Q(x))\ by (tactic "IntPr.fast_tac @{context} 1") text \The following should fail, as they are false!\ -lemma "(\x. \y. Q(x,y)) \ (\y. \x. Q(x,y))" +lemma \(\x. \y. Q(x,y)) \ (\y. \x. Q(x,y))\ apply (tactic "IntPr.fast_tac @{context} 1")? oops -lemma "(\x. Q(x)) \ (\x. Q(x))" +lemma \(\x. Q(x)) \ (\x. Q(x))\ apply (tactic "IntPr.fast_tac @{context} 1")? oops -schematic_goal "P(?a) \ (\x. P(x))" +schematic_goal \P(?a) \ (\x. P(x))\ apply (tactic "IntPr.fast_tac @{context} 1")? oops -schematic_goal "(P(?a) \ (\x. Q(x))) \ (\x. P(x) \ Q(x))" +schematic_goal \(P(?a) \ (\x. Q(x))) \ (\x. P(x) \ Q(x))\ apply (tactic "IntPr.fast_tac @{context} 1")? oops text \Back to things that are provable \dots\ -lemma "(\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))" +lemma \(\x. P(x) \ Q(x)) \ (\x. P(x)) \ (\x. Q(x))\ by (tactic "IntPr.fast_tac @{context} 1") \ \An example of why exI should be delayed as long as possible\ -lemma "(P \ (\x. Q(x))) \ P \ (\x. Q(x))" +lemma \(P \ (\x. Q(x))) \ P \ (\x. Q(x))\ by (tactic "IntPr.fast_tac @{context} 1") -schematic_goal "(\x. P(x) \ Q(f(x))) \ (\x. Q(x) \ R(g(x))) \ P(d) \ R(?a)" +schematic_goal \(\x. P(x) \ Q(f(x))) \ (\x. Q(x) \ R(g(x))) \ P(d) \ R(?a)\ by (tactic "IntPr.fast_tac @{context} 1") -lemma "(\x. Q(x)) \ (\x. Q(x))" +lemma \(\x. Q(x)) \ (\x. Q(x))\ by (tactic "IntPr.fast_tac @{context} 1") text \Some slow ones\ \ \Principia Mathematica *11.53\ -lemma "(\x y. P(x) \ Q(y)) \ ((\x. P(x)) \ (\y. Q(y)))" +lemma \(\x y. P(x) \ Q(y)) \ ((\x. P(x)) \ (\y. Q(y)))\ by (tactic "IntPr.fast_tac @{context} 1") (*Principia Mathematica *11.55 *) -lemma "(\x y. P(x) \ Q(x,y)) \ (\x. P(x) \ (\y. Q(x,y)))" +lemma \(\x y. P(x) \ Q(x,y)) \ (\x. P(x) \ (\y. Q(x,y)))\ by (tactic "IntPr.fast_tac @{context} 1") (*Principia Mathematica *11.61 *) -lemma "(\y. \x. P(x) \ Q(x,y)) \ (\x. P(x) \ (\y. Q(x,y)))" +lemma \(\y. \x. P(x) \ Q(x,y)) \ (\x. P(x) \ (\y. Q(x,y)))\ by (tactic "IntPr.fast_tac @{context} 1") end diff -r e15f053a42d8 -r e65314985426 src/Tools/induct.ML --- a/src/Tools/induct.ML Thu Jan 03 21:48:05 2019 +0100 +++ b/src/Tools/induct.ML Thu Jan 03 22:19:19 2019 +0100 @@ -172,7 +172,7 @@ val rearrange_eqs_simproc = Simplifier.make_simproc @{context} "rearrange_eqs" - {lhss = [@{term "Pure.all (t :: 'a::{} \ prop)"}], + {lhss = [@{term \Pure.all (t :: 'a::{} \ prop)\}], proc = fn _ => fn ctxt => fn ct => mk_swap_rrule ctxt ct};