author | paulson <lp15@cam.ac.uk> |
Mon, 11 May 2020 11:15:41 +0100 | |
changeset 71827 | 5e315defb038 |
parent 71608 | 856c68ab6f13 |
child 71833 | ff6f3b09b8b4 |
permissions | -rw-r--r-- |
923 | 1 |
(* Title: HOL/HOL.thy |
11750 | 2 |
Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson |
3 |
*) |
|
923 | 4 |
|
60758 | 5 |
section \<open>The basis of Higher-Order Logic\<close> |
923 | 6 |
|
15131 | 7 |
theory HOL |
70853 | 8 |
imports Pure Tools.Code_Generator |
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46497
diff
changeset
|
9 |
keywords |
52432 | 10 |
"try" "solve_direct" "quickcheck" "print_coercions" "print_claset" |
11 |
"print_induct_rules" :: diag and |
|
47657
1ba213363d0c
moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
haftmann
parents:
46973
diff
changeset
|
12 |
"quickcheck_params" :: thy_decl |
15131 | 13 |
begin |
2260 | 14 |
|
69605 | 15 |
ML_file \<open>~~/src/Tools/misc_legacy.ML\<close> |
16 |
ML_file \<open>~~/src/Tools/try.ML\<close> |
|
17 |
ML_file \<open>~~/src/Tools/quickcheck.ML\<close> |
|
18 |
ML_file \<open>~~/src/Tools/solve_direct.ML\<close> |
|
19 |
ML_file \<open>~~/src/Tools/IsaPlanner/zipper.ML\<close> |
|
20 |
ML_file \<open>~~/src/Tools/IsaPlanner/isand.ML\<close> |
|
21 |
ML_file \<open>~~/src/Tools/IsaPlanner/rw_inst.ML\<close> |
|
22 |
ML_file \<open>~~/src/Provers/hypsubst.ML\<close> |
|
23 |
ML_file \<open>~~/src/Provers/splitter.ML\<close> |
|
24 |
ML_file \<open>~~/src/Provers/classical.ML\<close> |
|
25 |
ML_file \<open>~~/src/Provers/blast.ML\<close> |
|
26 |
ML_file \<open>~~/src/Provers/clasimp.ML\<close> |
|
27 |
ML_file \<open>~~/src/Tools/eqsubst.ML\<close> |
|
28 |
ML_file \<open>~~/src/Provers/quantifier1.ML\<close> |
|
29 |
ML_file \<open>~~/src/Tools/atomize_elim.ML\<close> |
|
30 |
ML_file \<open>~~/src/Tools/cong_tac.ML\<close> |
|
31 |
ML_file \<open>~~/src/Tools/intuitionistic.ML\<close> setup \<open>Intuitionistic.method_setup \<^binding>\<open>iprover\<close>\<close> |
|
32 |
ML_file \<open>~~/src/Tools/project_rule.ML\<close> |
|
33 |
ML_file \<open>~~/src/Tools/subtyping.ML\<close> |
|
34 |
ML_file \<open>~~/src/Tools/case_product.ML\<close> |
|
48891 | 35 |
|
30165
6ee87f67d9cd
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
30160
diff
changeset
|
36 |
|
67149 | 37 |
ML \<open>Plugin_Name.declare_setup \<^binding>\<open>extraction\<close>\<close> |
58659
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset
|
38 |
|
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset
|
39 |
ML \<open> |
67149 | 40 |
Plugin_Name.declare_setup \<^binding>\<open>quickcheck_random\<close>; |
41 |
Plugin_Name.declare_setup \<^binding>\<open>quickcheck_exhaustive\<close>; |
|
42 |
Plugin_Name.declare_setup \<^binding>\<open>quickcheck_bounded_forall\<close>; |
|
43 |
Plugin_Name.declare_setup \<^binding>\<open>quickcheck_full_exhaustive\<close>; |
|
44 |
Plugin_Name.declare_setup \<^binding>\<open>quickcheck_narrowing\<close>; |
|
58659
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset
|
45 |
\<close> |
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset
|
46 |
ML \<open> |
67149 | 47 |
Plugin_Name.define_setup \<^binding>\<open>quickcheck\<close> |
69593 | 48 |
[\<^plugin>\<open>quickcheck_exhaustive\<close>, |
49 |
\<^plugin>\<open>quickcheck_random\<close>, |
|
50 |
\<^plugin>\<open>quickcheck_bounded_forall\<close>, |
|
51 |
\<^plugin>\<open>quickcheck_full_exhaustive\<close>, |
|
52 |
\<^plugin>\<open>quickcheck_narrowing\<close>] |
|
58659
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset
|
53 |
\<close> |
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset
|
54 |
|
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset
|
55 |
|
60758 | 56 |
subsection \<open>Primitive logic\<close> |
11750 | 57 |
|
66893
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
58 |
text \<open> |
67299 | 59 |
The definition of the logic is based on Mike Gordon's technical report @{cite "Gordon-TR68"} that |
66893
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
60 |
describes the first implementation of HOL. However, there are a number of differences. |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
61 |
In particular, we start with the definite description operator and introduce Hilbert's \<open>\<epsilon>\<close> operator |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
62 |
only much later. Moreover, axiom \<open>(P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P) \<longrightarrow> (P = Q)\<close> is derived from the other |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
63 |
axioms. The fact that this axiom is derivable was first noticed by Bruno Barras (for Mike Gordon's |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
64 |
line of HOL systems) and later independently by Alexander Maletzky (for Isabelle/HOL). |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
65 |
\<close> |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
66 |
|
60758 | 67 |
subsubsection \<open>Core syntax\<close> |
2260 | 68 |
|
67149 | 69 |
setup \<open>Axclass.class_axiomatization (\<^binding>\<open>type\<close>, [])\<close> |
36452 | 70 |
default_sort type |
69593 | 71 |
setup \<open>Object_Logic.add_base_sort \<^sort>\<open>type\<close>\<close> |
25460
b80087af2274
interpretation of typedecls: instantiation to class type
haftmann
parents:
25388
diff
changeset
|
72 |
|
70879 | 73 |
setup \<open>Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc [])\<close> |
70849 | 74 |
|
55383 | 75 |
axiomatization where fun_arity: "OFCLASS('a \<Rightarrow> 'b, type_class)" |
76 |
instance "fun" :: (type, type) type by (rule fun_arity) |
|
77 |
||
78 |
axiomatization where itself_arity: "OFCLASS('a itself, type_class)" |
|
79 |
instance itself :: (type) type by (rule itself_arity) |
|
25460
b80087af2274
interpretation of typedecls: instantiation to class type
haftmann
parents:
25388
diff
changeset
|
80 |
|
7357 | 81 |
typedecl bool |
923 | 82 |
|
62151 | 83 |
judgment Trueprop :: "bool \<Rightarrow> prop" ("(_)" 5) |
84 |
||
85 |
axiomatization implies :: "[bool, bool] \<Rightarrow> bool" (infixr "\<longrightarrow>" 25) |
|
68973
a1e26440efb8
tuned "=" syntax declarations; made "~=" uniformly "infix"
nipkow
parents:
68072
diff
changeset
|
86 |
and eq :: "['a, 'a] \<Rightarrow> bool" |
62151 | 87 |
and The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" |
88 |
||
68973
a1e26440efb8
tuned "=" syntax declarations; made "~=" uniformly "infix"
nipkow
parents:
68072
diff
changeset
|
89 |
notation (input) |
a1e26440efb8
tuned "=" syntax declarations; made "~=" uniformly "infix"
nipkow
parents:
68072
diff
changeset
|
90 |
eq (infixl "=" 50) |
a1e26440efb8
tuned "=" syntax declarations; made "~=" uniformly "infix"
nipkow
parents:
68072
diff
changeset
|
91 |
notation (output) |
a1e26440efb8
tuned "=" syntax declarations; made "~=" uniformly "infix"
nipkow
parents:
68072
diff
changeset
|
92 |
eq (infix "=" 50) |
a1e26440efb8
tuned "=" syntax declarations; made "~=" uniformly "infix"
nipkow
parents:
68072
diff
changeset
|
93 |
|
a1e26440efb8
tuned "=" syntax declarations; made "~=" uniformly "infix"
nipkow
parents:
68072
diff
changeset
|
94 |
text \<open>The input syntax for \<open>eq\<close> is more permissive than the output syntax |
a1e26440efb8
tuned "=" syntax declarations; made "~=" uniformly "infix"
nipkow
parents:
68072
diff
changeset
|
95 |
because of the large amount of material that relies on infixl.\<close> |
923 | 96 |
|
62151 | 97 |
subsubsection \<open>Defined connectives and quantifiers\<close> |
98 |
||
99 |
definition True :: bool |
|
100 |
where "True \<equiv> ((\<lambda>x::bool. x) = (\<lambda>x. x))" |
|
101 |
||
102 |
definition All :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<forall>" 10) |
|
103 |
where "All P \<equiv> (P = (\<lambda>x. True))" |
|
46973 | 104 |
|
62151 | 105 |
definition Ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<exists>" 10) |
106 |
where "Ex P \<equiv> \<forall>Q. (\<forall>x. P x \<longrightarrow> Q) \<longrightarrow> Q" |
|
107 |
||
108 |
definition False :: bool |
|
109 |
where "False \<equiv> (\<forall>P. P)" |
|
110 |
||
111 |
definition Not :: "bool \<Rightarrow> bool" ("\<not> _" [40] 40) |
|
112 |
where not_def: "\<not> P \<equiv> P \<longrightarrow> False" |
|
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
113 |
|
62151 | 114 |
definition conj :: "[bool, bool] \<Rightarrow> bool" (infixr "\<and>" 35) |
115 |
where and_def: "P \<and> Q \<equiv> \<forall>R. (P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> R" |
|
38555 | 116 |
|
62151 | 117 |
definition disj :: "[bool, bool] \<Rightarrow> bool" (infixr "\<or>" 30) |
118 |
where or_def: "P \<or> Q \<equiv> \<forall>R. (P \<longrightarrow> R) \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> R" |
|
119 |
||
71827 | 120 |
definition Uniq :: "('a \<Rightarrow> bool) \<Rightarrow> bool" |
121 |
where "Uniq P \<equiv> (\<forall>x y. P x \<longrightarrow> P y \<longrightarrow> y = x)" |
|
122 |
||
63909 | 123 |
definition Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool" |
62151 | 124 |
where "Ex1 P \<equiv> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x)" |
923 | 125 |
|
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
126 |
|
60758 | 127 |
subsubsection \<open>Additional concrete syntax\<close> |
2260 | 128 |
|
71827 | 129 |
syntax (ASCII) "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(4?< _./ _)" [0, 10] 10) |
130 |
syntax "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(2\<exists>\<^sub>\<le>\<^sub>1 _./ _)" [0, 10] 10) |
|
131 |
translations "\<exists>\<^sub>\<le>\<^sub>1x. P" \<rightleftharpoons> "CONST Uniq (\<lambda>x. P)" |
|
132 |
||
133 |
print_translation \<open> |
|
134 |
[Syntax_Trans.preserve_binder_abs_tr' \<^const_syntax>\<open>Uniq\<close> \<^syntax_const>\<open>_Uniq\<close>] |
|
135 |
\<close> \<comment> \<open>to avoid eta-contraction of body\<close> |
|
136 |
||
137 |
||
63909 | 138 |
syntax (ASCII) |
139 |
"_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(3EX! _./ _)" [0, 10] 10) |
|
140 |
syntax (input) |
|
141 |
"_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(3?! _./ _)" [0, 10] 10) |
|
142 |
syntax "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>!_./ _)" [0, 10] 10) |
|
143 |
translations "\<exists>!x. P" \<rightleftharpoons> "CONST Ex1 (\<lambda>x. P)" |
|
144 |
||
145 |
print_translation \<open> |
|
69593 | 146 |
[Syntax_Trans.preserve_binder_abs_tr' \<^const_syntax>\<open>Ex1\<close> \<^syntax_const>\<open>_Ex1\<close>] |
63909 | 147 |
\<close> \<comment> \<open>to avoid eta-contraction of body\<close> |
148 |
||
149 |
||
63912
9f8325206465
clarified notation: iterated quantifier is negated as one chunk;
wenzelm
parents:
63909
diff
changeset
|
150 |
syntax |
9f8325206465
clarified notation: iterated quantifier is negated as one chunk;
wenzelm
parents:
63909
diff
changeset
|
151 |
"_Not_Ex" :: "idts \<Rightarrow> bool \<Rightarrow> bool" ("(3\<nexists>_./ _)" [0, 10] 10) |
9f8325206465
clarified notation: iterated quantifier is negated as one chunk;
wenzelm
parents:
63909
diff
changeset
|
152 |
"_Not_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(3\<nexists>!_./ _)" [0, 10] 10) |
9f8325206465
clarified notation: iterated quantifier is negated as one chunk;
wenzelm
parents:
63909
diff
changeset
|
153 |
translations |
9f8325206465
clarified notation: iterated quantifier is negated as one chunk;
wenzelm
parents:
63909
diff
changeset
|
154 |
"\<nexists>x. P" \<rightleftharpoons> "\<not> (\<exists>x. P)" |
9f8325206465
clarified notation: iterated quantifier is negated as one chunk;
wenzelm
parents:
63909
diff
changeset
|
155 |
"\<nexists>!x. P" \<rightleftharpoons> "\<not> (\<exists>!x. P)" |
62522 | 156 |
|
157 |
||
68973
a1e26440efb8
tuned "=" syntax declarations; made "~=" uniformly "infix"
nipkow
parents:
68072
diff
changeset
|
158 |
abbreviation not_equal :: "['a, 'a] \<Rightarrow> bool" (infix "\<noteq>" 50) |
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61941
diff
changeset
|
159 |
where "x \<noteq> y \<equiv> \<not> (x = y)" |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
160 |
|
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61941
diff
changeset
|
161 |
notation (ASCII) |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61941
diff
changeset
|
162 |
Not ("~ _" [40] 40) and |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61941
diff
changeset
|
163 |
conj (infixr "&" 35) and |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61941
diff
changeset
|
164 |
disj (infixr "|" 30) and |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61941
diff
changeset
|
165 |
implies (infixr "-->" 25) and |
68973
a1e26440efb8
tuned "=" syntax declarations; made "~=" uniformly "infix"
nipkow
parents:
68072
diff
changeset
|
166 |
not_equal (infix "~=" 50) |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
167 |
|
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
168 |
abbreviation (iff) |
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61941
diff
changeset
|
169 |
iff :: "[bool, bool] \<Rightarrow> bool" (infixr "\<longleftrightarrow>" 25) |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61941
diff
changeset
|
170 |
where "A \<longleftrightarrow> B \<equiv> A = B" |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
171 |
|
60759 | 172 |
syntax "_The" :: "[pttrn, bool] \<Rightarrow> 'a" ("(3THE _./ _)" [0, 10] 10) |
173 |
translations "THE x. P" \<rightleftharpoons> "CONST The (\<lambda>x. P)" |
|
60758 | 174 |
print_translation \<open> |
69593 | 175 |
[(\<^const_syntax>\<open>The\<close>, fn _ => fn [Abs abs] => |
46125
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
45654
diff
changeset
|
176 |
let val (x, t) = Syntax_Trans.atomic_abs_tr' abs |
69593 | 177 |
in Syntax.const \<^syntax_const>\<open>_The\<close> $ x $ t end)] |
61799 | 178 |
\<close> \<comment> \<open>To avoid eta-contraction of body\<close> |
923 | 179 |
|
46125
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
45654
diff
changeset
|
180 |
nonterminal letbinds and letbind |
923 | 181 |
syntax |
60759 | 182 |
"_bind" :: "[pttrn, 'a] \<Rightarrow> letbind" ("(2_ =/ _)" 10) |
183 |
"" :: "letbind \<Rightarrow> letbinds" ("_") |
|
184 |
"_binds" :: "[letbind, letbinds] \<Rightarrow> letbinds" ("_;/ _") |
|
185 |
"_Let" :: "[letbinds, 'a] \<Rightarrow> 'a" ("(let (_)/ in (_))" [0, 10] 10) |
|
923 | 186 |
|
46125
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
45654
diff
changeset
|
187 |
nonterminal case_syn and cases_syn |
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
45654
diff
changeset
|
188 |
syntax |
60759 | 189 |
"_case_syntax" :: "['a, cases_syn] \<Rightarrow> 'b" ("(case _ of/ _)" 10) |
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61941
diff
changeset
|
190 |
"_case1" :: "['a, 'b] \<Rightarrow> case_syn" ("(2_ \<Rightarrow>/ _)" 10) |
60759 | 191 |
"" :: "case_syn \<Rightarrow> cases_syn" ("_") |
192 |
"_case2" :: "[case_syn, cases_syn] \<Rightarrow> cases_syn" ("_/ | _") |
|
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61941
diff
changeset
|
193 |
syntax (ASCII) |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61941
diff
changeset
|
194 |
"_case1" :: "['a, 'b] \<Rightarrow> case_syn" ("(2_ =>/ _)" 10) |
13763
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset
|
195 |
|
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61941
diff
changeset
|
196 |
notation (ASCII) |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61941
diff
changeset
|
197 |
All (binder "ALL " 10) and |
63909 | 198 |
Ex (binder "EX " 10) |
2372 | 199 |
|
62521 | 200 |
notation (input) |
21524 | 201 |
All (binder "! " 10) and |
63909 | 202 |
Ex (binder "? " 10) |
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7220
diff
changeset
|
203 |
|
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7220
diff
changeset
|
204 |
|
60758 | 205 |
subsubsection \<open>Axioms and basic definitions\<close> |
2260 | 206 |
|
46973 | 207 |
axiomatization where |
208 |
refl: "t = (t::'a)" and |
|
209 |
subst: "s = t \<Longrightarrow> P s \<Longrightarrow> P t" and |
|
60759 | 210 |
ext: "(\<And>x::'a. (f x ::'b) = g x) \<Longrightarrow> (\<lambda>x. f x) = (\<lambda>x. g x)" |
61799 | 211 |
\<comment> \<open>Extensionality is built into the meta-logic, and this rule expresses |
15380 | 212 |
a related property. It is an eta-expanded version of the traditional |
60758 | 213 |
rule, and similar to the ABS rule of HOL\<close> and |
6289 | 214 |
|
11432
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
10489
diff
changeset
|
215 |
the_eq_trivial: "(THE x. x = a) = (a::'a)" |
923 | 216 |
|
46973 | 217 |
axiomatization where |
60759 | 218 |
impI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<longrightarrow> Q" and |
219 |
mp: "\<lbrakk>P \<longrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q" and |
|
15380 | 220 |
|
60759 | 221 |
True_or_False: "(P = True) \<or> (P = False)" |
15380 | 222 |
|
46973 | 223 |
definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10) |
60759 | 224 |
where "If P x y \<equiv> (THE z::'a. (P = True \<longrightarrow> z = x) \<and> (P = False \<longrightarrow> z = y))" |
923 | 225 |
|
46973 | 226 |
definition Let :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b" |
227 |
where "Let s f \<equiv> f s" |
|
38525 | 228 |
|
229 |
translations |
|
60759 | 230 |
"_Let (_binds b bs) e" \<rightleftharpoons> "_Let b (_Let bs e)" |
231 |
"let x = a in e" \<rightleftharpoons> "CONST Let a (\<lambda>x. e)" |
|
38525 | 232 |
|
46973 | 233 |
axiomatization undefined :: 'a |
22481
79c2724c36b5
added class "default" and expansion axioms for undefined
haftmann
parents:
22473
diff
changeset
|
234 |
|
46973 | 235 |
class default = fixes default :: 'a |
4868 | 236 |
|
11750 | 237 |
|
60758 | 238 |
subsection \<open>Fundamental rules\<close> |
20944 | 239 |
|
60758 | 240 |
subsubsection \<open>Equality\<close> |
20944 | 241 |
|
60759 | 242 |
lemma sym: "s = t \<Longrightarrow> t = s" |
18457 | 243 |
by (erule subst) (rule refl) |
15411 | 244 |
|
60759 | 245 |
lemma ssubst: "t = s \<Longrightarrow> P s \<Longrightarrow> P t" |
18457 | 246 |
by (drule sym) (erule subst) |
15411 | 247 |
|
60759 | 248 |
lemma trans: "\<lbrakk>r = s; s = t\<rbrakk> \<Longrightarrow> r = t" |
18457 | 249 |
by (erule subst) |
15411 | 250 |
|
60759 | 251 |
lemma trans_sym [Pure.elim?]: "r = s \<Longrightarrow> t = s \<Longrightarrow> r = t" |
40715
3ba17f07b23c
lemma trans_sym allows single-step "normalization" in Isar, e.g. via moreover/ultimately;
wenzelm
parents:
40582
diff
changeset
|
252 |
by (rule trans [OF _ sym]) |
3ba17f07b23c
lemma trans_sym allows single-step "normalization" in Isar, e.g. via moreover/ultimately;
wenzelm
parents:
40582
diff
changeset
|
253 |
|
58826 | 254 |
lemma meta_eq_to_obj_eq: |
63575 | 255 |
assumes "A \<equiv> B" |
20944 | 256 |
shows "A = B" |
63575 | 257 |
unfolding assms by (rule refl) |
15411 | 258 |
|
61799 | 259 |
text \<open>Useful with \<open>erule\<close> for proving equalities from known equalities.\<close> |
20944 | 260 |
(* a = b |
15411 | 261 |
| | |
262 |
c = d *) |
|
60759 | 263 |
lemma box_equals: "\<lbrakk>a = b; a = c; b = d\<rbrakk> \<Longrightarrow> c = d" |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
264 |
by (iprover intro: sym trans) |
15411 | 265 |
|
60758 | 266 |
text \<open>For calculational reasoning:\<close> |
15524
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset
|
267 |
|
60759 | 268 |
lemma forw_subst: "a = b \<Longrightarrow> P b \<Longrightarrow> P a" |
15524
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset
|
269 |
by (rule ssubst) |
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset
|
270 |
|
60759 | 271 |
lemma back_subst: "P a \<Longrightarrow> a = b \<Longrightarrow> P b" |
15524
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset
|
272 |
by (rule subst) |
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset
|
273 |
|
15411 | 274 |
|
60758 | 275 |
subsubsection \<open>Congruence rules for application\<close> |
15411 | 276 |
|
61799 | 277 |
text \<open>Similar to \<open>AP_THM\<close> in Gordon's HOL.\<close> |
60759 | 278 |
lemma fun_cong: "(f :: 'a \<Rightarrow> 'b) = g \<Longrightarrow> f x = g x" |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
279 |
by (iprover intro: refl elim: subst) |
15411 | 280 |
|
61799 | 281 |
text \<open>Similar to \<open>AP_TERM\<close> in Gordon's HOL and FOL's \<open>subst_context\<close>.\<close> |
60759 | 282 |
lemma arg_cong: "x = y \<Longrightarrow> f x = f y" |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
283 |
by (iprover intro: refl elim: subst) |
15411 | 284 |
|
60759 | 285 |
lemma arg_cong2: "\<lbrakk>a = b; c = d\<rbrakk> \<Longrightarrow> f a c = f b d" |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
286 |
by (iprover intro: refl elim: subst) |
15655 | 287 |
|
60759 | 288 |
lemma cong: "\<lbrakk>f = g; (x::'a) = y\<rbrakk> \<Longrightarrow> f x = g y" |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
289 |
by (iprover intro: refl elim: subst) |
15411 | 290 |
|
60758 | 291 |
ML \<open>fun cong_tac ctxt = Cong_Tac.cong_tac ctxt @{thm cong}\<close> |
15411 | 292 |
|
32733
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32668
diff
changeset
|
293 |
|
60758 | 294 |
subsubsection \<open>Equality of booleans -- iff\<close> |
15411 | 295 |
|
60759 | 296 |
lemma iffD2: "\<lbrakk>P = Q; Q\<rbrakk> \<Longrightarrow> P" |
18457 | 297 |
by (erule ssubst) |
15411 | 298 |
|
60759 | 299 |
lemma rev_iffD2: "\<lbrakk>Q; P = Q\<rbrakk> \<Longrightarrow> P" |
18457 | 300 |
by (erule iffD2) |
15411 | 301 |
|
21504 | 302 |
lemma iffD1: "Q = P \<Longrightarrow> Q \<Longrightarrow> P" |
303 |
by (drule sym) (rule iffD2) |
|
304 |
||
305 |
lemma rev_iffD1: "Q \<Longrightarrow> Q = P \<Longrightarrow> P" |
|
306 |
by (drule sym) (rule rev_iffD2) |
|
15411 | 307 |
|
308 |
lemma iffE: |
|
60759 | 309 |
assumes major: "P = Q" |
310 |
and minor: "\<lbrakk>P \<longrightarrow> Q; Q \<longrightarrow> P\<rbrakk> \<Longrightarrow> R" |
|
18457 | 311 |
shows R |
312 |
by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1]) |
|
15411 | 313 |
|
314 |
||
66893
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
315 |
subsubsection \<open>True (1)\<close> |
15411 | 316 |
|
63575 | 317 |
lemma TrueI: True |
21504 | 318 |
unfolding True_def by (rule refl) |
15411 | 319 |
|
60759 | 320 |
lemma eqTrueE: "P = True \<Longrightarrow> P" |
21504 | 321 |
by (erule iffD2) (rule TrueI) |
15411 | 322 |
|
323 |
||
66893
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
324 |
subsubsection \<open>Universal quantifier (1)\<close> |
15411 | 325 |
|
60759 | 326 |
lemma spec: "\<forall>x::'a. P x \<Longrightarrow> P x" |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
327 |
unfolding All_def by (iprover intro: eqTrueE fun_cong) |
15411 | 328 |
|
329 |
lemma allE: |
|
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
330 |
assumes major: "\<forall>x. P x" and minor: "P x \<Longrightarrow> R" |
21504 | 331 |
shows R |
332 |
by (iprover intro: minor major [THEN spec]) |
|
15411 | 333 |
|
334 |
lemma all_dupE: |
|
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
335 |
assumes major: "\<forall>x. P x" and minor: "\<lbrakk>P x; \<forall>x. P x\<rbrakk> \<Longrightarrow> R" |
21504 | 336 |
shows R |
337 |
by (iprover intro: minor major major [THEN spec]) |
|
15411 | 338 |
|
339 |
||
60758 | 340 |
subsubsection \<open>False\<close> |
21504 | 341 |
|
60758 | 342 |
text \<open> |
61799 | 343 |
Depends upon \<open>spec\<close>; it is impossible to do propositional |
21504 | 344 |
logic before quantifiers! |
60758 | 345 |
\<close> |
15411 | 346 |
|
60759 | 347 |
lemma FalseE: "False \<Longrightarrow> P" |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
348 |
unfolding False_def by (erule spec) |
15411 | 349 |
|
60759 | 350 |
lemma False_neq_True: "False = True \<Longrightarrow> P" |
21504 | 351 |
by (erule eqTrueE [THEN FalseE]) |
15411 | 352 |
|
353 |
||
60758 | 354 |
subsubsection \<open>Negation\<close> |
15411 | 355 |
|
356 |
lemma notI: |
|
60759 | 357 |
assumes "P \<Longrightarrow> False" |
358 |
shows "\<not> P" |
|
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
359 |
unfolding not_def by (iprover intro: impI assms) |
15411 | 360 |
|
60759 | 361 |
lemma False_not_True: "False \<noteq> True" |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
362 |
by (iprover intro: notI elim: False_neq_True) |
15411 | 363 |
|
60759 | 364 |
lemma True_not_False: "True \<noteq> False" |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
365 |
by (iprover intro: notI dest: sym elim: False_neq_True) |
15411 | 366 |
|
60759 | 367 |
lemma notE: "\<lbrakk>\<not> P; P\<rbrakk> \<Longrightarrow> R" |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
368 |
unfolding not_def |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
369 |
by (iprover intro: mp [THEN FalseE]) |
15411 | 370 |
|
371 |
||
60758 | 372 |
subsubsection \<open>Implication\<close> |
15411 | 373 |
|
374 |
lemma impE: |
|
60759 | 375 |
assumes "P \<longrightarrow> Q" P "Q \<Longrightarrow> R" |
376 |
shows R |
|
63575 | 377 |
by (iprover intro: assms mp) |
15411 | 378 |
|
63575 | 379 |
text \<open>Reduces \<open>Q\<close> to \<open>P \<longrightarrow> Q\<close>, allowing substitution in \<open>P\<close>.\<close> |
60759 | 380 |
lemma rev_mp: "\<lbrakk>P; P \<longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
381 |
by (rule mp) |
15411 | 382 |
|
383 |
lemma contrapos_nn: |
|
60759 | 384 |
assumes major: "\<not> Q" |
63575 | 385 |
and minor: "P \<Longrightarrow> Q" |
60759 | 386 |
shows "\<not> P" |
63575 | 387 |
by (iprover intro: notI minor major [THEN notE]) |
15411 | 388 |
|
63575 | 389 |
text \<open>Not used at all, but we already have the other 3 combinations.\<close> |
15411 | 390 |
lemma contrapos_pn: |
391 |
assumes major: "Q" |
|
63575 | 392 |
and minor: "P \<Longrightarrow> \<not> Q" |
60759 | 393 |
shows "\<not> P" |
63575 | 394 |
by (iprover intro: notI minor major notE) |
15411 | 395 |
|
60759 | 396 |
lemma not_sym: "t \<noteq> s \<Longrightarrow> s \<noteq> t" |
21250 | 397 |
by (erule contrapos_nn) (erule sym) |
398 |
||
60759 | 399 |
lemma eq_neq_eq_imp_neq: "\<lbrakk>x = a; a \<noteq> b; b = y\<rbrakk> \<Longrightarrow> x \<noteq> y" |
21250 | 400 |
by (erule subst, erule ssubst, assumption) |
15411 | 401 |
|
402 |
||
66893
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
403 |
subsubsection \<open>Disjunction (1)\<close> |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
404 |
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
405 |
lemma disjE: |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
406 |
assumes major: "P \<or> Q" |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
407 |
and minorP: "P \<Longrightarrow> R" |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
408 |
and minorQ: "Q \<Longrightarrow> R" |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
409 |
shows R |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
410 |
by (iprover intro: minorP minorQ impI |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
411 |
major [unfolded or_def, THEN spec, THEN mp, THEN mp]) |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
412 |
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
413 |
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
414 |
subsubsection \<open>Derivation of \<open>iffI\<close>\<close> |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
415 |
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
416 |
text \<open>In an intuitionistic version of HOL \<open>iffI\<close> needs to be an axiom.\<close> |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
417 |
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
418 |
lemma iffI: |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
419 |
assumes "P \<Longrightarrow> Q" and "Q \<Longrightarrow> P" |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
420 |
shows "P = Q" |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
421 |
proof (rule disjE[OF True_or_False[of P]]) |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
422 |
assume 1: "P = True" |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
423 |
note Q = assms(1)[OF eqTrueE[OF this]] |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
424 |
from 1 show ?thesis |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
425 |
proof (rule ssubst) |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
426 |
from True_or_False[of Q] show "True = Q" |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
427 |
proof (rule disjE) |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
428 |
assume "Q = True" |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
429 |
thus ?thesis by(rule sym) |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
430 |
next |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
431 |
assume "Q = False" |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
432 |
with Q have False by (rule rev_iffD1) |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
433 |
thus ?thesis by (rule FalseE) |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
434 |
qed |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
435 |
qed |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
436 |
next |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
437 |
assume 2: "P = False" |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
438 |
thus ?thesis |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
439 |
proof (rule ssubst) |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
440 |
from True_or_False[of Q] show "False = Q" |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
441 |
proof (rule disjE) |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
442 |
assume "Q = True" |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
443 |
from 2 assms(2)[OF eqTrueE[OF this]] have False by (rule iffD1) |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
444 |
thus ?thesis by (rule FalseE) |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
445 |
next |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
446 |
assume "Q = False" |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
447 |
thus ?thesis by(rule sym) |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
448 |
qed |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
449 |
qed |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
450 |
qed |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
451 |
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
452 |
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
453 |
subsubsection \<open>True (2)\<close> |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
454 |
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
455 |
lemma eqTrueI: "P \<Longrightarrow> P = True" |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
456 |
by (iprover intro: iffI TrueI) |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
457 |
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
458 |
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
459 |
subsubsection \<open>Universal quantifier (2)\<close> |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
460 |
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
461 |
lemma allI: |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
462 |
assumes "\<And>x::'a. P x" |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
463 |
shows "\<forall>x. P x" |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
464 |
unfolding All_def by (iprover intro: ext eqTrueI assms) |
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
465 |
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
466 |
|
60758 | 467 |
subsubsection \<open>Existential quantifier\<close> |
15411 | 468 |
|
60759 | 469 |
lemma exI: "P x \<Longrightarrow> \<exists>x::'a. P x" |
63575 | 470 |
unfolding Ex_def by (iprover intro: allI allE impI mp) |
15411 | 471 |
|
472 |
lemma exE: |
|
60759 | 473 |
assumes major: "\<exists>x::'a. P x" |
63575 | 474 |
and minor: "\<And>x. P x \<Longrightarrow> Q" |
15411 | 475 |
shows "Q" |
63575 | 476 |
by (rule major [unfolded Ex_def, THEN spec, THEN mp]) (iprover intro: impI [THEN allI] minor) |
15411 | 477 |
|
478 |
||
60758 | 479 |
subsubsection \<open>Conjunction\<close> |
15411 | 480 |
|
60759 | 481 |
lemma conjI: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q" |
63575 | 482 |
unfolding and_def by (iprover intro: impI [THEN allI] mp) |
15411 | 483 |
|
60759 | 484 |
lemma conjunct1: "\<lbrakk>P \<and> Q\<rbrakk> \<Longrightarrow> P" |
63575 | 485 |
unfolding and_def by (iprover intro: impI dest: spec mp) |
15411 | 486 |
|
60759 | 487 |
lemma conjunct2: "\<lbrakk>P \<and> Q\<rbrakk> \<Longrightarrow> Q" |
63575 | 488 |
unfolding and_def by (iprover intro: impI dest: spec mp) |
15411 | 489 |
|
490 |
lemma conjE: |
|
60759 | 491 |
assumes major: "P \<and> Q" |
63575 | 492 |
and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R" |
60759 | 493 |
shows R |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
494 |
proof (rule minor) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
495 |
show P by (rule major [THEN conjunct1]) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
496 |
show Q by (rule major [THEN conjunct2]) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
497 |
qed |
15411 | 498 |
|
499 |
lemma context_conjI: |
|
63575 | 500 |
assumes P "P \<Longrightarrow> Q" |
501 |
shows "P \<and> Q" |
|
502 |
by (iprover intro: conjI assms) |
|
15411 | 503 |
|
504 |
||
66893
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
66836
diff
changeset
|
505 |
subsubsection \<open>Disjunction (2)\<close> |
15411 | 506 |
|
60759 | 507 |
lemma disjI1: "P \<Longrightarrow> P \<or> Q" |
63575 | 508 |
unfolding or_def by (iprover intro: allI impI mp) |
15411 | 509 |
|
60759 | 510 |
lemma disjI2: "Q \<Longrightarrow> P \<or> Q" |
63575 | 511 |
unfolding or_def by (iprover intro: allI impI mp) |
15411 | 512 |
|
513 |
||
60758 | 514 |
subsubsection \<open>Classical logic\<close> |
15411 | 515 |
|
516 |
lemma classical: |
|
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
517 |
assumes "\<not> P \<Longrightarrow> P" |
60759 | 518 |
shows P |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
519 |
proof (rule True_or_False [THEN disjE]) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
520 |
show P if "P = True" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
521 |
using that by (iprover intro: eqTrueE) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
522 |
show P if "P = False" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
523 |
proof (intro notI assms) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
524 |
assume P |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
525 |
with that show False |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
526 |
by (iprover elim: subst) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
527 |
qed |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
528 |
qed |
15411 | 529 |
|
45607 | 530 |
lemmas ccontr = FalseE [THEN classical] |
15411 | 531 |
|
63575 | 532 |
text \<open>\<open>notE\<close> with premises exchanged; it discharges \<open>\<not> R\<close> so that it can be used to |
533 |
make elimination rules.\<close> |
|
15411 | 534 |
lemma rev_notE: |
60759 | 535 |
assumes premp: P |
63575 | 536 |
and premnot: "\<not> R \<Longrightarrow> \<not> P" |
60759 | 537 |
shows R |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
538 |
by (iprover intro: ccontr notE [OF premnot premp]) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
539 |
|
15411 | 540 |
|
63575 | 541 |
text \<open>Double negation law.\<close> |
60759 | 542 |
lemma notnotD: "\<not>\<not> P \<Longrightarrow> P" |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
543 |
by (iprover intro: ccontr notE ) |
15411 | 544 |
|
545 |
lemma contrapos_pp: |
|
60759 | 546 |
assumes p1: Q |
63575 | 547 |
and p2: "\<not> P \<Longrightarrow> \<not> Q" |
60759 | 548 |
shows P |
63575 | 549 |
by (iprover intro: classical p1 p2 notE) |
15411 | 550 |
|
551 |
||
60758 | 552 |
subsubsection \<open>Unique existence\<close> |
15411 | 553 |
|
71827 | 554 |
lemma Uniq_I [intro?]: |
555 |
assumes "\<And>x y. \<lbrakk>P x; P y\<rbrakk> \<Longrightarrow> y = x" |
|
556 |
shows "Uniq P" |
|
557 |
unfolding Uniq_def by (iprover intro: assms allI impI) |
|
558 |
||
559 |
lemma Uniq_D [dest?]: "\<lbrakk>Uniq P; P a; P b\<rbrakk> \<Longrightarrow> a=b" |
|
560 |
unfolding Uniq_def by (iprover dest: spec mp) |
|
561 |
||
15411 | 562 |
lemma ex1I: |
60759 | 563 |
assumes "P a" "\<And>x. P x \<Longrightarrow> x = a" |
564 |
shows "\<exists>!x. P x" |
|
63575 | 565 |
unfolding Ex1_def by (iprover intro: assms exI conjI allI impI) |
15411 | 566 |
|
63575 | 567 |
text \<open>Sometimes easier to use: the premises have no shared variables. Safe!\<close> |
15411 | 568 |
lemma ex_ex1I: |
60759 | 569 |
assumes ex_prem: "\<exists>x. P x" |
63575 | 570 |
and eq: "\<And>x y. \<lbrakk>P x; P y\<rbrakk> \<Longrightarrow> x = y" |
60759 | 571 |
shows "\<exists>!x. P x" |
63575 | 572 |
by (iprover intro: ex_prem [THEN exE] ex1I eq) |
15411 | 573 |
|
574 |
lemma ex1E: |
|
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
575 |
assumes major: "\<exists>!x. P x" and minor: "\<And>x. \<lbrakk>P x; \<forall>y. P y \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> R" |
60759 | 576 |
shows R |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
577 |
proof (rule major [unfolded Ex1_def, THEN exE]) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
578 |
show "\<And>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<Longrightarrow> R" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
579 |
by (iprover intro: minor elim: conjE) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
580 |
qed |
15411 | 581 |
|
60759 | 582 |
lemma ex1_implies_ex: "\<exists>!x. P x \<Longrightarrow> \<exists>x. P x" |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
583 |
by (iprover intro: exI elim: ex1E) |
15411 | 584 |
|
60758 | 585 |
subsubsection \<open>Classical intro rules for disjunction and existential quantifiers\<close> |
15411 | 586 |
|
587 |
lemma disjCI: |
|
63575 | 588 |
assumes "\<not> Q \<Longrightarrow> P" |
589 |
shows "P \<or> Q" |
|
590 |
by (rule classical) (iprover intro: assms disjI1 disjI2 notI elim: notE) |
|
15411 | 591 |
|
60759 | 592 |
lemma excluded_middle: "\<not> P \<or> P" |
63575 | 593 |
by (iprover intro: disjCI) |
15411 | 594 |
|
60758 | 595 |
text \<open> |
20944 | 596 |
case distinction as a natural deduction rule. |
63575 | 597 |
Note that \<open>\<not> P\<close> is the second case, not the first. |
60758 | 598 |
\<close> |
27126
3ede9103de8e
eliminated obsolete case_split_thm -- use case_split;
wenzelm
parents:
27107
diff
changeset
|
599 |
lemma case_split [case_names True False]: |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
600 |
assumes "P \<Longrightarrow> Q" "\<not> P \<Longrightarrow> Q" |
60759 | 601 |
shows Q |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
602 |
using excluded_middle [of P] |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
603 |
by (iprover intro: assms elim: disjE) |
27126
3ede9103de8e
eliminated obsolete case_split_thm -- use case_split;
wenzelm
parents:
27107
diff
changeset
|
604 |
|
63575 | 605 |
text \<open>Classical implies (\<open>\<longrightarrow>\<close>) elimination.\<close> |
15411 | 606 |
lemma impCE: |
60759 | 607 |
assumes major: "P \<longrightarrow> Q" |
63575 | 608 |
and minor: "\<not> P \<Longrightarrow> R" "Q \<Longrightarrow> R" |
60759 | 609 |
shows R |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
610 |
using excluded_middle [of P] |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
611 |
by (iprover intro: minor major [THEN mp] elim: disjE)+ |
15411 | 612 |
|
63575 | 613 |
text \<open> |
614 |
This version of \<open>\<longrightarrow>\<close> elimination works on \<open>Q\<close> before \<open>P\<close>. It works best for |
|
615 |
those cases in which \<open>P\<close> holds "almost everywhere". Can't install as |
|
616 |
default: would break old proofs. |
|
617 |
\<close> |
|
15411 | 618 |
lemma impCE': |
60759 | 619 |
assumes major: "P \<longrightarrow> Q" |
63575 | 620 |
and minor: "Q \<Longrightarrow> R" "\<not> P \<Longrightarrow> R" |
60759 | 621 |
shows R |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
622 |
using assms by (elim impCE) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
623 |
|
15411 | 624 |
|
63575 | 625 |
text \<open>Classical \<open>\<longleftrightarrow>\<close> elimination.\<close> |
15411 | 626 |
lemma iffCE: |
60759 | 627 |
assumes major: "P = Q" |
63575 | 628 |
and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R" "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R" |
60759 | 629 |
shows R |
63575 | 630 |
by (rule major [THEN iffE]) (iprover intro: minor elim: impCE notE) |
15411 | 631 |
|
632 |
lemma exCI: |
|
60759 | 633 |
assumes "\<forall>x. \<not> P x \<Longrightarrow> P a" |
634 |
shows "\<exists>x. P x" |
|
63575 | 635 |
by (rule ccontr) (iprover intro: assms exI allI notI notE [of "\<exists>x. P x"]) |
15411 | 636 |
|
637 |
||
60758 | 638 |
subsubsection \<open>Intuitionistic Reasoning\<close> |
12386 | 639 |
|
640 |
lemma impE': |
|
60759 | 641 |
assumes 1: "P \<longrightarrow> Q" |
642 |
and 2: "Q \<Longrightarrow> R" |
|
643 |
and 3: "P \<longrightarrow> Q \<Longrightarrow> P" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset
|
644 |
shows R |
12386 | 645 |
proof - |
646 |
from 3 and 1 have P . |
|
647 |
with 1 have Q by (rule impE) |
|
648 |
with 2 show R . |
|
649 |
qed |
|
650 |
||
651 |
lemma allE': |
|
60759 | 652 |
assumes 1: "\<forall>x. P x" |
653 |
and 2: "P x \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset
|
654 |
shows Q |
12386 | 655 |
proof - |
656 |
from 1 have "P x" by (rule spec) |
|
657 |
from this and 1 show Q by (rule 2) |
|
658 |
qed |
|
659 |
||
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset
|
660 |
lemma notE': |
60759 | 661 |
assumes 1: "\<not> P" |
662 |
and 2: "\<not> P \<Longrightarrow> P" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset
|
663 |
shows R |
12386 | 664 |
proof - |
665 |
from 2 and 1 have P . |
|
666 |
with 1 show R by (rule notE) |
|
667 |
qed |
|
668 |
||
60759 | 669 |
lemma TrueE: "True \<Longrightarrow> P \<Longrightarrow> P" . |
670 |
lemma notFalseE: "\<not> False \<Longrightarrow> P \<Longrightarrow> P" . |
|
22444
fb80fedd192d
added safe intro rules for removing "True" subgoals as well as "~ False" ones.
dixon
parents:
22377
diff
changeset
|
671 |
|
22467
c9357ef01168
TrueElim and notTrueElim tested and added as safe elim rules.
dixon
parents:
22445
diff
changeset
|
672 |
lemmas [Pure.elim!] = disjE iffE FalseE conjE exE TrueE notFalseE |
15801 | 673 |
and [Pure.intro!] = iffI conjI impI TrueI notI allI refl |
674 |
and [Pure.elim 2] = allE notE' impE' |
|
675 |
and [Pure.intro] = exI disjI2 disjI1 |
|
12386 | 676 |
|
677 |
lemmas [trans] = trans |
|
678 |
and [sym] = sym not_sym |
|
15801 | 679 |
and [Pure.elim?] = iffD1 iffD2 impE |
11750 | 680 |
|
11438
3d9222b80989
declare trans [trans] (*overridden in theory Calculation*);
wenzelm
parents:
11432
diff
changeset
|
681 |
|
60758 | 682 |
subsubsection \<open>Atomizing meta-level connectives\<close> |
11750 | 683 |
|
28513 | 684 |
axiomatization where |
63575 | 685 |
eq_reflection: "x = y \<Longrightarrow> x \<equiv> y" \<comment> \<open>admissible axiom\<close> |
28513 | 686 |
|
60759 | 687 |
lemma atomize_all [atomize]: "(\<And>x. P x) \<equiv> Trueprop (\<forall>x. P x)" |
12003 | 688 |
proof |
60759 | 689 |
assume "\<And>x. P x" |
690 |
then show "\<forall>x. P x" .. |
|
9488 | 691 |
next |
60759 | 692 |
assume "\<forall>x. P x" |
693 |
then show "\<And>x. P x" by (rule allE) |
|
9488 | 694 |
qed |
695 |
||
60759 | 696 |
lemma atomize_imp [atomize]: "(A \<Longrightarrow> B) \<equiv> Trueprop (A \<longrightarrow> B)" |
12003 | 697 |
proof |
60759 | 698 |
assume r: "A \<Longrightarrow> B" |
699 |
show "A \<longrightarrow> B" by (rule impI) (rule r) |
|
9488 | 700 |
next |
60759 | 701 |
assume "A \<longrightarrow> B" and A |
23553 | 702 |
then show B by (rule mp) |
9488 | 703 |
qed |
704 |
||
60759 | 705 |
lemma atomize_not: "(A \<Longrightarrow> False) \<equiv> Trueprop (\<not> A)" |
14749 | 706 |
proof |
60759 | 707 |
assume r: "A \<Longrightarrow> False" |
708 |
show "\<not> A" by (rule notI) (rule r) |
|
14749 | 709 |
next |
60759 | 710 |
assume "\<not> A" and A |
23553 | 711 |
then show False by (rule notE) |
14749 | 712 |
qed |
713 |
||
60759 | 714 |
lemma atomize_eq [atomize, code]: "(x \<equiv> y) \<equiv> Trueprop (x = y)" |
12003 | 715 |
proof |
60759 | 716 |
assume "x \<equiv> y" |
717 |
show "x = y" by (unfold \<open>x \<equiv> y\<close>) (rule refl) |
|
10432
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset
|
718 |
next |
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset
|
719 |
assume "x = y" |
60759 | 720 |
then show "x \<equiv> y" by (rule eq_reflection) |
10432
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset
|
721 |
qed |
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset
|
722 |
|
60759 | 723 |
lemma atomize_conj [atomize]: "(A &&& B) \<equiv> Trueprop (A \<and> B)" |
12003 | 724 |
proof |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28741
diff
changeset
|
725 |
assume conj: "A &&& B" |
60759 | 726 |
show "A \<and> B" |
19121 | 727 |
proof (rule conjI) |
728 |
from conj show A by (rule conjunctionD1) |
|
729 |
from conj show B by (rule conjunctionD2) |
|
730 |
qed |
|
11953 | 731 |
next |
60759 | 732 |
assume conj: "A \<and> B" |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28741
diff
changeset
|
733 |
show "A &&& B" |
19121 | 734 |
proof - |
735 |
from conj show A .. |
|
736 |
from conj show B .. |
|
11953 | 737 |
qed |
738 |
qed |
|
739 |
||
12386 | 740 |
lemmas [symmetric, rulify] = atomize_all atomize_imp |
18832 | 741 |
and [symmetric, defn] = atomize_all atomize_imp atomize_eq |
12386 | 742 |
|
11750 | 743 |
|
60758 | 744 |
subsubsection \<open>Atomizing elimination rules\<close> |
26580
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset
|
745 |
|
60759 | 746 |
lemma atomize_exL[atomize_elim]: "(\<And>x. P x \<Longrightarrow> Q) \<equiv> ((\<exists>x. P x) \<Longrightarrow> Q)" |
26580
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset
|
747 |
by rule iprover+ |
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset
|
748 |
|
60759 | 749 |
lemma atomize_conjL[atomize_elim]: "(A \<Longrightarrow> B \<Longrightarrow> C) \<equiv> (A \<and> B \<Longrightarrow> C)" |
26580
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset
|
750 |
by rule iprover+ |
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset
|
751 |
|
60759 | 752 |
lemma atomize_disjL[atomize_elim]: "((A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C) \<equiv> ((A \<or> B \<Longrightarrow> C) \<Longrightarrow> C)" |
26580
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset
|
753 |
by rule iprover+ |
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset
|
754 |
|
60759 | 755 |
lemma atomize_elimL[atomize_elim]: "(\<And>B. (A \<Longrightarrow> B) \<Longrightarrow> B) \<equiv> Trueprop A" .. |
26580
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset
|
756 |
|
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset
|
757 |
|
60758 | 758 |
subsection \<open>Package setup\<close> |
20944 | 759 |
|
69605 | 760 |
ML_file \<open>Tools/hologic.ML\<close> |
70847 | 761 |
ML_file \<open>Tools/rewrite_hol_proof.ML\<close> |
51314
eac4bb5adbf9
just one HOLogic.Trueprop_conv, with regular exception CTERM;
wenzelm
parents:
51304
diff
changeset
|
762 |
|
70879 | 763 |
setup \<open>Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc Rewrite_HOL_Proof.rews)\<close> |
70849 | 764 |
|
51314
eac4bb5adbf9
just one HOLogic.Trueprop_conv, with regular exception CTERM;
wenzelm
parents:
51304
diff
changeset
|
765 |
|
60758 | 766 |
subsubsection \<open>Sledgehammer setup\<close> |
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset
|
767 |
|
60758 | 768 |
text \<open> |
63575 | 769 |
Theorems blacklisted to Sledgehammer. These theorems typically produce clauses |
770 |
that are prolific (match too many equality or membership literals) and relate to |
|
771 |
seldom-used facts. Some duplicate other rules. |
|
60758 | 772 |
\<close> |
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset
|
773 |
|
57963 | 774 |
named_theorems no_atp "theorems that should be filtered out by Sledgehammer" |
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset
|
775 |
|
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset
|
776 |
|
60758 | 777 |
subsubsection \<open>Classical Reasoner setup\<close> |
9529 | 778 |
|
60759 | 779 |
lemma imp_elim: "P \<longrightarrow> Q \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R" |
26411 | 780 |
by (rule classical) iprover |
781 |
||
60759 | 782 |
lemma swap: "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R" |
26411 | 783 |
by (rule classical) iprover |
784 |
||
62958
b41c1cb5e251
Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents:
62913
diff
changeset
|
785 |
lemma thin_refl: "\<lbrakk>x = x; PROP W\<rbrakk> \<Longrightarrow> PROP W" . |
20944 | 786 |
|
60758 | 787 |
ML \<open> |
42799 | 788 |
structure Hypsubst = Hypsubst |
789 |
( |
|
21218 | 790 |
val dest_eq = HOLogic.dest_eq |
21151 | 791 |
val dest_Trueprop = HOLogic.dest_Trueprop |
792 |
val dest_imp = HOLogic.dest_imp |
|
26411 | 793 |
val eq_reflection = @{thm eq_reflection} |
794 |
val rev_eq_reflection = @{thm meta_eq_to_obj_eq} |
|
795 |
val imp_intr = @{thm impI} |
|
796 |
val rev_mp = @{thm rev_mp} |
|
797 |
val subst = @{thm subst} |
|
798 |
val sym = @{thm sym} |
|
22129 | 799 |
val thin_refl = @{thm thin_refl}; |
42799 | 800 |
); |
21671 | 801 |
open Hypsubst; |
21151 | 802 |
|
42799 | 803 |
structure Classical = Classical |
804 |
( |
|
26411 | 805 |
val imp_elim = @{thm imp_elim} |
806 |
val not_elim = @{thm notE} |
|
807 |
val swap = @{thm swap} |
|
808 |
val classical = @{thm classical} |
|
21151 | 809 |
val sizef = Drule.size_of_thm |
810 |
val hyp_subst_tacs = [Hypsubst.hyp_subst_tac] |
|
42799 | 811 |
); |
21151 | 812 |
|
58826 | 813 |
structure Basic_Classical: BASIC_CLASSICAL = Classical; |
33308
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
33185
diff
changeset
|
814 |
open Basic_Classical; |
60758 | 815 |
\<close> |
22129 | 816 |
|
60758 | 817 |
setup \<open> |
35389 | 818 |
(*prevent substitution on bool*) |
58826 | 819 |
let |
69593 | 820 |
fun non_bool_eq (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _])) = T <> \<^typ>\<open>bool\<close> |
58826 | 821 |
| non_bool_eq _ = false; |
822 |
fun hyp_subst_tac' ctxt = |
|
823 |
SUBGOAL (fn (goal, i) => |
|
824 |
if Term.exists_Const non_bool_eq goal |
|
825 |
then Hypsubst.hyp_subst_tac ctxt i |
|
826 |
else no_tac); |
|
827 |
in |
|
828 |
Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac' ctxt ORELSE' tac) |
|
829 |
end |
|
60758 | 830 |
\<close> |
21009 | 831 |
|
832 |
declare iffI [intro!] |
|
833 |
and notI [intro!] |
|
834 |
and impI [intro!] |
|
835 |
and disjCI [intro!] |
|
836 |
and conjI [intro!] |
|
837 |
and TrueI [intro!] |
|
838 |
and refl [intro!] |
|
839 |
||
840 |
declare iffCE [elim!] |
|
841 |
and FalseE [elim!] |
|
842 |
and impCE [elim!] |
|
843 |
and disjE [elim!] |
|
844 |
and conjE [elim!] |
|
845 |
||
846 |
declare ex_ex1I [intro!] |
|
847 |
and allI [intro!] |
|
848 |
and exI [intro] |
|
849 |
||
850 |
declare exE [elim!] |
|
851 |
allE [elim] |
|
852 |
||
69593 | 853 |
ML \<open>val HOL_cs = claset_of \<^context>\<close> |
19162 | 854 |
|
60759 | 855 |
lemma contrapos_np: "\<not> Q \<Longrightarrow> (\<not> P \<Longrightarrow> Q) \<Longrightarrow> P" |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
856 |
by (erule swap) |
10383 | 857 |
|
18689
a50587cd8414
prefer ex1I over ex_ex1I in single-step reasoning;
wenzelm
parents:
18595
diff
changeset
|
858 |
declare ex_ex1I [rule del, intro! 2] |
a50587cd8414
prefer ex1I over ex_ex1I in single-step reasoning;
wenzelm
parents:
18595
diff
changeset
|
859 |
and ex1I [intro] |
a50587cd8414
prefer ex1I over ex_ex1I in single-step reasoning;
wenzelm
parents:
18595
diff
changeset
|
860 |
|
41865
4e8483cc2cc5
declare ext [intro]: Extensionality now available by default
paulson
parents:
41827
diff
changeset
|
861 |
declare ext [intro] |
4e8483cc2cc5
declare ext [intro]: Extensionality now available by default
paulson
parents:
41827
diff
changeset
|
862 |
|
12386 | 863 |
lemmas [intro?] = ext |
864 |
and [elim?] = ex1_implies_ex |
|
11977 | 865 |
|
63575 | 866 |
text \<open>Better than \<open>ex1E\<close> for classical reasoner: needs no quantifier duplication!\<close> |
20973 | 867 |
lemma alt_ex1E [elim!]: |
20944 | 868 |
assumes major: "\<exists>!x. P x" |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
869 |
and minor: "\<And>x. \<lbrakk>P x; \<forall>y y'. P y \<and> P y' \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> R" |
20944 | 870 |
shows R |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
871 |
proof (rule ex1E [OF major minor]) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
872 |
show "\<forall>y y'. P y \<and> P y' \<longrightarrow> y = y'" if "P x" and \<section>: "\<forall>y. P y \<longrightarrow> y = x" for x |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
873 |
using \<open>P x\<close> \<section> \<section> by fast |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
874 |
qed assumption |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
875 |
|
71827 | 876 |
text \<open>And again using Uniq\<close> |
877 |
lemma alt_ex1E': |
|
878 |
assumes "\<exists>!x. P x" "\<And>x. \<lbrakk>P x; \<exists>\<^sub>\<le>\<^sub>1x. P x\<rbrakk> \<Longrightarrow> R" |
|
879 |
shows R |
|
880 |
using assms unfolding Uniq_def by fast |
|
881 |
||
882 |
lemma ex1_iff_ex_Uniq: "(\<exists>!x. P x) \<longleftrightarrow> (\<exists>x. P x) \<and> (\<exists>\<^sub>\<le>\<^sub>1x. P x)" |
|
883 |
unfolding Uniq_def by fast |
|
884 |
||
20944 | 885 |
|
60758 | 886 |
ML \<open> |
42477 | 887 |
structure Blast = Blast |
888 |
( |
|
889 |
structure Classical = Classical |
|
69597 | 890 |
val Trueprop_const = dest_Const \<^const>\<open>Trueprop\<close> |
69593 | 891 |
val equality_name = \<^const_name>\<open>HOL.eq\<close> |
892 |
val not_name = \<^const_name>\<open>Not\<close> |
|
42477 | 893 |
val notE = @{thm notE} |
894 |
val ccontr = @{thm ccontr} |
|
895 |
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac |
|
896 |
); |
|
897 |
val blast_tac = Blast.blast_tac; |
|
60758 | 898 |
\<close> |
20944 | 899 |
|
900 |
||
60758 | 901 |
subsubsection \<open>THE: definite description operator\<close> |
59504
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset
|
902 |
|
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset
|
903 |
lemma the_equality [intro]: |
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset
|
904 |
assumes "P a" |
63575 | 905 |
and "\<And>x. P x \<Longrightarrow> x = a" |
59504
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset
|
906 |
shows "(THE x. P x) = a" |
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset
|
907 |
by (blast intro: assms trans [OF arg_cong [where f=The] the_eq_trivial]) |
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset
|
908 |
|
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset
|
909 |
lemma theI: |
63575 | 910 |
assumes "P a" |
911 |
and "\<And>x. P x \<Longrightarrow> x = a" |
|
59504
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset
|
912 |
shows "P (THE x. P x)" |
63575 | 913 |
by (iprover intro: assms the_equality [THEN ssubst]) |
59504
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset
|
914 |
|
60759 | 915 |
lemma theI': "\<exists>!x. P x \<Longrightarrow> P (THE x. P x)" |
59504
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset
|
916 |
by (blast intro: theI) |
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset
|
917 |
|
63575 | 918 |
text \<open>Easier to apply than \<open>theI\<close>: only one occurrence of \<open>P\<close>.\<close> |
59504
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset
|
919 |
lemma theI2: |
60759 | 920 |
assumes "P a" "\<And>x. P x \<Longrightarrow> x = a" "\<And>x. P x \<Longrightarrow> Q x" |
59504
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset
|
921 |
shows "Q (THE x. P x)" |
63575 | 922 |
by (iprover intro: assms theI) |
59504
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset
|
923 |
|
63575 | 924 |
lemma the1I2: |
925 |
assumes "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x" |
|
926 |
shows "Q (THE x. P x)" |
|
927 |
by (iprover intro: assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)] elim: allE impE) |
|
59504
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset
|
928 |
|
60759 | 929 |
lemma the1_equality [elim?]: "\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> (THE x. P x) = a" |
59504
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset
|
930 |
by blast |
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset
|
931 |
|
71827 | 932 |
lemma the1_equality': "\<lbrakk>\<exists>\<^sub>\<le>\<^sub>1x. P x; P a\<rbrakk> \<Longrightarrow> (THE x. P x) = a" |
933 |
unfolding Uniq_def by blast |
|
934 |
||
60759 | 935 |
lemma the_sym_eq_trivial: "(THE y. x = y) = x" |
59504
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset
|
936 |
by blast |
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset
|
937 |
|
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset
|
938 |
|
60758 | 939 |
subsubsection \<open>Simplifier\<close> |
12281 | 940 |
|
60759 | 941 |
lemma eta_contract_eq: "(\<lambda>s. f s) = f" .. |
12281 | 942 |
|
943 |
lemma simp_thms: |
|
60759 | 944 |
shows not_not: "(\<not> \<not> P) = P" |
945 |
and Not_eq_iff: "((\<not> P) = (\<not> Q)) = (P = Q)" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset
|
946 |
and |
60759 | 947 |
"(P \<noteq> Q) = (P = (\<not> Q))" |
948 |
"(P \<or> \<not>P) = True" "(\<not> P \<or> P) = True" |
|
12281 | 949 |
"(x = x) = True" |
32068 | 950 |
and not_True_eq_False [code]: "(\<not> True) = False" |
951 |
and not_False_eq_True [code]: "(\<not> False) = True" |
|
20944 | 952 |
and |
60759 | 953 |
"(\<not> P) \<noteq> P" "P \<noteq> (\<not> P)" |
954 |
"(True = P) = P" |
|
20944 | 955 |
and eq_True: "(P = True) = P" |
60759 | 956 |
and "(False = P) = (\<not> P)" |
20944 | 957 |
and eq_False: "(P = False) = (\<not> P)" |
958 |
and |
|
60759 | 959 |
"(True \<longrightarrow> P) = P" "(False \<longrightarrow> P) = True" |
960 |
"(P \<longrightarrow> True) = True" "(P \<longrightarrow> P) = True" |
|
961 |
"(P \<longrightarrow> False) = (\<not> P)" "(P \<longrightarrow> \<not> P) = (\<not> P)" |
|
962 |
"(P \<and> True) = P" "(True \<and> P) = P" |
|
963 |
"(P \<and> False) = False" "(False \<and> P) = False" |
|
964 |
"(P \<and> P) = P" "(P \<and> (P \<and> Q)) = (P \<and> Q)" |
|
965 |
"(P \<and> \<not> P) = False" "(\<not> P \<and> P) = False" |
|
966 |
"(P \<or> True) = True" "(True \<or> P) = True" |
|
967 |
"(P \<or> False) = P" "(False \<or> P) = P" |
|
968 |
"(P \<or> P) = P" "(P \<or> (P \<or> Q)) = (P \<or> Q)" and |
|
969 |
"(\<forall>x. P) = P" "(\<exists>x. P) = P" "\<exists>x. x = t" "\<exists>x. t = x" |
|
31166
a90fe83f58ea
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents:
31156
diff
changeset
|
970 |
and |
60759 | 971 |
"\<And>P. (\<exists>x. x = t \<and> P x) = P t" |
972 |
"\<And>P. (\<exists>x. t = x \<and> P x) = P t" |
|
973 |
"\<And>P. (\<forall>x. x = t \<longrightarrow> P x) = P t" |
|
974 |
"\<And>P. (\<forall>x. t = x \<longrightarrow> P x) = P t" |
|
66109 | 975 |
"(\<forall>x. x \<noteq> t) = False" "(\<forall>x. t \<noteq> x) = False" |
17589 | 976 |
by (blast, blast, blast, blast, blast, iprover+) |
13421 | 977 |
|
63575 | 978 |
lemma disj_absorb: "A \<or> A \<longleftrightarrow> A" |
14201 | 979 |
by blast |
980 |
||
63575 | 981 |
lemma disj_left_absorb: "A \<or> (A \<or> B) \<longleftrightarrow> A \<or> B" |
14201 | 982 |
by blast |
983 |
||
63575 | 984 |
lemma conj_absorb: "A \<and> A \<longleftrightarrow> A" |
14201 | 985 |
by blast |
986 |
||
63575 | 987 |
lemma conj_left_absorb: "A \<and> (A \<and> B) \<longleftrightarrow> A \<and> B" |
14201 | 988 |
by blast |
989 |
||
12281 | 990 |
lemma eq_ac: |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56941
diff
changeset
|
991 |
shows eq_commute: "a = b \<longleftrightarrow> b = a" |
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56941
diff
changeset
|
992 |
and iff_left_commute: "(P \<longleftrightarrow> (Q \<longleftrightarrow> R)) \<longleftrightarrow> (Q \<longleftrightarrow> (P \<longleftrightarrow> R))" |
63575 | 993 |
and iff_assoc: "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))" |
994 |
by (iprover, blast+) |
|
995 |
||
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56941
diff
changeset
|
996 |
lemma neq_commute: "a \<noteq> b \<longleftrightarrow> b \<noteq> a" by iprover |
12281 | 997 |
|
998 |
lemma conj_comms: |
|
63575 | 999 |
shows conj_commute: "P \<and> Q \<longleftrightarrow> Q \<and> P" |
1000 |
and conj_left_commute: "P \<and> (Q \<and> R) \<longleftrightarrow> Q \<and> (P \<and> R)" by iprover+ |
|
1001 |
lemma conj_assoc: "(P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)" by iprover |
|
12281 | 1002 |
|
19174 | 1003 |
lemmas conj_ac = conj_commute conj_left_commute conj_assoc |
1004 |
||
12281 | 1005 |
lemma disj_comms: |
63575 | 1006 |
shows disj_commute: "P \<or> Q \<longleftrightarrow> Q \<or> P" |
1007 |
and disj_left_commute: "P \<or> (Q \<or> R) \<longleftrightarrow> Q \<or> (P \<or> R)" by iprover+ |
|
1008 |
lemma disj_assoc: "(P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)" by iprover |
|
12281 | 1009 |
|
19174 | 1010 |
lemmas disj_ac = disj_commute disj_left_commute disj_assoc |
1011 |
||
63575 | 1012 |
lemma conj_disj_distribL: "P \<and> (Q \<or> R) \<longleftrightarrow> P \<and> Q \<or> P \<and> R" by iprover |
1013 |
lemma conj_disj_distribR: "(P \<or> Q) \<and> R \<longleftrightarrow> P \<and> R \<or> Q \<and> R" by iprover |
|
12281 | 1014 |
|
63575 | 1015 |
lemma disj_conj_distribL: "P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)" by iprover |
1016 |
lemma disj_conj_distribR: "(P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)" by iprover |
|
12281 | 1017 |
|
60759 | 1018 |
lemma imp_conjR: "(P \<longrightarrow> (Q \<and> R)) = ((P \<longrightarrow> Q) \<and> (P \<longrightarrow> R))" by iprover |
1019 |
lemma imp_conjL: "((P \<and> Q) \<longrightarrow> R) = (P \<longrightarrow> (Q \<longrightarrow> R))" by iprover |
|
1020 |
lemma imp_disjL: "((P \<or> Q) \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))" by iprover |
|
12281 | 1021 |
|
61799 | 1022 |
text \<open>These two are specialized, but \<open>imp_disj_not1\<close> is useful in \<open>Auth/Yahalom\<close>.\<close> |
63575 | 1023 |
lemma imp_disj_not1: "(P \<longrightarrow> Q \<or> R) \<longleftrightarrow> (\<not> Q \<longrightarrow> P \<longrightarrow> R)" by blast |
1024 |
lemma imp_disj_not2: "(P \<longrightarrow> Q \<or> R) \<longleftrightarrow> (\<not> R \<longrightarrow> P \<longrightarrow> Q)" by blast |
|
12281 | 1025 |
|
63575 | 1026 |
lemma imp_disj1: "((P \<longrightarrow> Q) \<or> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast |
1027 |
lemma imp_disj2: "(Q \<or> (P \<longrightarrow> R)) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast |
|
12281 | 1028 |
|
63575 | 1029 |
lemma imp_cong: "(P = P') \<Longrightarrow> (P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<longrightarrow> Q) \<longleftrightarrow> (P' \<longrightarrow> Q'))" |
21151 | 1030 |
by iprover |
1031 |
||
63575 | 1032 |
lemma de_Morgan_disj: "\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q" by iprover |
1033 |
lemma de_Morgan_conj: "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q" by blast |
|
1034 |
lemma not_imp: "\<not> (P \<longrightarrow> Q) \<longleftrightarrow> P \<and> \<not> Q" by blast |
|
1035 |
lemma not_iff: "P \<noteq> Q \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)" by blast |
|
1036 |
lemma disj_not1: "\<not> P \<or> Q \<longleftrightarrow> (P \<longrightarrow> Q)" by blast |
|
1037 |
lemma disj_not2: "P \<or> \<not> Q \<longleftrightarrow> (Q \<longrightarrow> P)" by blast \<comment> \<open>changes orientation :-(\<close> |
|
1038 |
lemma imp_conv_disj: "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P) \<or> Q" by blast |
|
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62958
diff
changeset
|
1039 |
lemma disj_imp: "P \<or> Q \<longleftrightarrow> \<not> P \<longrightarrow> Q" by blast |
12281 | 1040 |
|
63575 | 1041 |
lemma iff_conv_conj_imp: "(P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)" by iprover |
12281 | 1042 |
|
1043 |
||
63575 | 1044 |
lemma cases_simp: "(P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q) \<longleftrightarrow> Q" |
62390 | 1045 |
\<comment> \<open>Avoids duplication of subgoals after \<open>if_split\<close>, when the true and false\<close> |
61799 | 1046 |
\<comment> \<open>cases boil down to the same thing.\<close> |
12281 | 1047 |
by blast |
1048 |
||
63575 | 1049 |
lemma not_all: "\<not> (\<forall>x. P x) \<longleftrightarrow> (\<exists>x. \<not> P x)" by blast |
1050 |
lemma imp_all: "((\<forall>x. P x) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P x \<longrightarrow> Q)" by blast |
|
1051 |
lemma not_ex: "\<not> (\<exists>x. P x) \<longleftrightarrow> (\<forall>x. \<not> P x)" by iprover |
|
1052 |
lemma imp_ex: "((\<exists>x. P x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q)" by iprover |
|
1053 |
lemma all_not_ex: "(\<forall>x. P x) \<longleftrightarrow> \<not> (\<exists>x. \<not> P x)" by blast |
|
12281 | 1054 |
|
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset
|
1055 |
declare All_def [no_atp] |
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24280
diff
changeset
|
1056 |
|
63575 | 1057 |
lemma ex_disj_distrib: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>x. P x) \<or> (\<exists>x. Q x)" by iprover |
1058 |
lemma all_conj_distrib: "(\<forall>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>x. P x) \<and> (\<forall>x. Q x)" by iprover |
|
12281 | 1059 |
|
60758 | 1060 |
text \<open> |
63575 | 1061 |
\<^medskip> The \<open>\<and>\<close> congruence rule: not included by default! |
60758 | 1062 |
May slow rewrite proofs down by as much as 50\%\<close> |
12281 | 1063 |
|
63575 | 1064 |
lemma conj_cong: "P = P' \<Longrightarrow> (P' \<Longrightarrow> Q = Q') \<Longrightarrow> (P \<and> Q) = (P' \<and> Q')" |
17589 | 1065 |
by iprover |
12281 | 1066 |
|
63575 | 1067 |
lemma rev_conj_cong: "Q = Q' \<Longrightarrow> (Q' \<Longrightarrow> P = P') \<Longrightarrow> (P \<and> Q) = (P' \<and> Q')" |
17589 | 1068 |
by iprover |
12281 | 1069 |
|
61799 | 1070 |
text \<open>The \<open>|\<close> congruence rule: not included by default!\<close> |
12281 | 1071 |
|
63575 | 1072 |
lemma disj_cong: "P = P' \<Longrightarrow> (\<not> P' \<Longrightarrow> Q = Q') \<Longrightarrow> (P \<or> Q) = (P' \<or> Q')" |
12281 | 1073 |
by blast |
1074 |
||
1075 |
||
63575 | 1076 |
text \<open>\<^medskip> if-then-else rules\<close> |
12281 | 1077 |
|
32068 | 1078 |
lemma if_True [code]: "(if True then x else y) = x" |
63575 | 1079 |
unfolding If_def by blast |
12281 | 1080 |
|
32068 | 1081 |
lemma if_False [code]: "(if False then x else y) = y" |
63575 | 1082 |
unfolding If_def by blast |
12281 | 1083 |
|
60759 | 1084 |
lemma if_P: "P \<Longrightarrow> (if P then x else y) = x" |
63575 | 1085 |
unfolding If_def by blast |
12281 | 1086 |
|
60759 | 1087 |
lemma if_not_P: "\<not> P \<Longrightarrow> (if P then x else y) = y" |
63575 | 1088 |
unfolding If_def by blast |
12281 | 1089 |
|
62390 | 1090 |
lemma if_split: "P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))" |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1091 |
proof (rule case_split [of Q]) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1092 |
show ?thesis if Q |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1093 |
using that by (simplesubst if_P) blast+ |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1094 |
show ?thesis if "\<not> Q" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1095 |
using that by (simplesubst if_not_P) blast+ |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1096 |
qed |
12281 | 1097 |
|
62390 | 1098 |
lemma if_split_asm: "P (if Q then x else y) = (\<not> ((Q \<and> \<not> P x) \<or> (\<not> Q \<and> \<not> P y)))" |
63575 | 1099 |
by (simplesubst if_split) blast |
12281 | 1100 |
|
62390 | 1101 |
lemmas if_splits [no_atp] = if_split if_split_asm |
12281 | 1102 |
|
1103 |
lemma if_cancel: "(if c then x else x) = x" |
|
63575 | 1104 |
by (simplesubst if_split) blast |
12281 | 1105 |
|
1106 |
lemma if_eq_cancel: "(if x = y then y else x) = x" |
|
63575 | 1107 |
by (simplesubst if_split) blast |
12281 | 1108 |
|
60759 | 1109 |
lemma if_bool_eq_conj: "(if P then Q else R) = ((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R))" |
61799 | 1110 |
\<comment> \<open>This form is useful for expanding \<open>if\<close>s on the RIGHT of the \<open>\<Longrightarrow>\<close> symbol.\<close> |
62390 | 1111 |
by (rule if_split) |
12281 | 1112 |
|
60759 | 1113 |
lemma if_bool_eq_disj: "(if P then Q else R) = ((P \<and> Q) \<or> (\<not> P \<and> R))" |
61799 | 1114 |
\<comment> \<open>And this form is useful for expanding \<open>if\<close>s on the LEFT.\<close> |
62390 | 1115 |
by (simplesubst if_split) blast |
12281 | 1116 |
|
63575 | 1117 |
lemma Eq_TrueI: "P \<Longrightarrow> P \<equiv> True" unfolding atomize_eq by iprover |
1118 |
lemma Eq_FalseI: "\<not> P \<Longrightarrow> P \<equiv> False" unfolding atomize_eq by iprover |
|
12281 | 1119 |
|
63575 | 1120 |
text \<open>\<^medskip> let rules for simproc\<close> |
15423 | 1121 |
|
60759 | 1122 |
lemma Let_folded: "f x \<equiv> g x \<Longrightarrow> Let x f \<equiv> Let x g" |
15423 | 1123 |
by (unfold Let_def) |
1124 |
||
60759 | 1125 |
lemma Let_unfold: "f x \<equiv> g \<Longrightarrow> Let x f \<equiv> g" |
15423 | 1126 |
by (unfold Let_def) |
1127 |
||
60758 | 1128 |
text \<open> |
16999 | 1129 |
The following copy of the implication operator is useful for |
1130 |
fine-tuning congruence rules. It instructs the simplifier to simplify |
|
1131 |
its premise. |
|
60758 | 1132 |
\<close> |
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
1133 |
|
63575 | 1134 |
definition simp_implies :: "prop \<Rightarrow> prop \<Rightarrow> prop" (infixr "=simp=>" 1) |
67399 | 1135 |
where "simp_implies \<equiv> (\<Longrightarrow>)" |
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
1136 |
|
18457 | 1137 |
lemma simp_impliesI: |
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
1138 |
assumes PQ: "(PROP P \<Longrightarrow> PROP Q)" |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
1139 |
shows "PROP P =simp=> PROP Q" |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1140 |
unfolding simp_implies_def |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1141 |
by (iprover intro: PQ) |
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
1142 |
|
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
1143 |
lemma simp_impliesE: |
25388 | 1144 |
assumes PQ: "PROP P =simp=> PROP Q" |
63575 | 1145 |
and P: "PROP P" |
1146 |
and QR: "PROP Q \<Longrightarrow> PROP R" |
|
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
1147 |
shows "PROP R" |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1148 |
by (iprover intro: QR P PQ [unfolded simp_implies_def]) |
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
1149 |
|
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
1150 |
lemma simp_implies_cong: |
60759 | 1151 |
assumes PP' :"PROP P \<equiv> PROP P'" |
63575 | 1152 |
and P'QQ': "PROP P' \<Longrightarrow> (PROP Q \<equiv> PROP Q')" |
60759 | 1153 |
shows "(PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q')" |
63575 | 1154 |
unfolding simp_implies_def |
1155 |
proof (rule equal_intr_rule) |
|
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
1156 |
assume PQ: "PROP P \<Longrightarrow> PROP Q" |
63575 | 1157 |
and P': "PROP P'" |
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
1158 |
from PP' [symmetric] and P' have "PROP P" |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
1159 |
by (rule equal_elim_rule1) |
23553 | 1160 |
then have "PROP Q" by (rule PQ) |
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
1161 |
with P'QQ' [OF P'] show "PROP Q'" by (rule equal_elim_rule1) |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
1162 |
next |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
1163 |
assume P'Q': "PROP P' \<Longrightarrow> PROP Q'" |
63575 | 1164 |
and P: "PROP P" |
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
1165 |
from PP' and P have P': "PROP P'" by (rule equal_elim_rule1) |
23553 | 1166 |
then have "PROP Q'" by (rule P'Q') |
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
1167 |
with P'QQ' [OF P', symmetric] show "PROP Q" |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
1168 |
by (rule equal_elim_rule1) |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
1169 |
qed |
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
berghofe
parents:
16587
diff
changeset
|
1170 |
|
20944 | 1171 |
lemma uncurry: |
1172 |
assumes "P \<longrightarrow> Q \<longrightarrow> R" |
|
1173 |
shows "P \<and> Q \<longrightarrow> R" |
|
23553 | 1174 |
using assms by blast |
20944 | 1175 |
|
1176 |
lemma iff_allI: |
|
1177 |
assumes "\<And>x. P x = Q x" |
|
1178 |
shows "(\<forall>x. P x) = (\<forall>x. Q x)" |
|
23553 | 1179 |
using assms by blast |
20944 | 1180 |
|
1181 |
lemma iff_exI: |
|
1182 |
assumes "\<And>x. P x = Q x" |
|
1183 |
shows "(\<exists>x. P x) = (\<exists>x. Q x)" |
|
23553 | 1184 |
using assms by blast |
20944 | 1185 |
|
63575 | 1186 |
lemma all_comm: "(\<forall>x y. P x y) = (\<forall>y x. P x y)" |
20944 | 1187 |
by blast |
1188 |
||
63575 | 1189 |
lemma ex_comm: "(\<exists>x y. P x y) = (\<exists>y x. P x y)" |
20944 | 1190 |
by blast |
1191 |
||
69605 | 1192 |
ML_file \<open>Tools/simpdata.ML\<close> |
60758 | 1193 |
ML \<open>open Simpdata\<close> |
42455 | 1194 |
|
60758 | 1195 |
setup \<open> |
58826 | 1196 |
map_theory_simpset (put_simpset HOL_basic_ss) #> |
1197 |
Simplifier.method_setup Splitter.split_modifiers |
|
60758 | 1198 |
\<close> |
42455 | 1199 |
|
71517 | 1200 |
simproc_setup defined_Ex ("\<exists>x. P x") = \<open>K Quantifier1.rearrange_ex\<close> |
1201 |
simproc_setup defined_All ("\<forall>x. P x") = \<open>K Quantifier1.rearrange_all\<close> |
|
21671 | 1202 |
|
61799 | 1203 |
text \<open>Simproc for proving \<open>(y = x) \<equiv> False\<close> from premise \<open>\<not> (x = y)\<close>:\<close> |
24035 | 1204 |
|
60758 | 1205 |
simproc_setup neq ("x = y") = \<open>fn _ => |
63575 | 1206 |
let |
1207 |
val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI}; |
|
1208 |
fun is_neq eq lhs rhs thm = |
|
1209 |
(case Thm.prop_of thm of |
|
1210 |
_ $ (Not $ (eq' $ l' $ r')) => |
|
1211 |
Not = HOLogic.Not andalso eq' = eq andalso |
|
1212 |
r' aconv lhs andalso l' aconv rhs |
|
1213 |
| _ => false); |
|
1214 |
fun proc ss ct = |
|
1215 |
(case Thm.term_of ct of |
|
1216 |
eq $ lhs $ rhs => |
|
1217 |
(case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of |
|
1218 |
SOME thm => SOME (thm RS neq_to_EQ_False) |
|
1219 |
| NONE => NONE) |
|
1220 |
| _ => NONE); |
|
69216
1a52baa70aed
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents:
68979
diff
changeset
|
1221 |
in proc end |
60758 | 1222 |
\<close> |
24035 | 1223 |
|
60758 | 1224 |
simproc_setup let_simp ("Let x f") = \<open> |
63575 | 1225 |
let |
1226 |
fun count_loose (Bound i) k = if i >= k then 1 else 0 |
|
1227 |
| count_loose (s $ t) k = count_loose s k + count_loose t k |
|
1228 |
| count_loose (Abs (_, _, t)) k = count_loose t (k + 1) |
|
1229 |
| count_loose _ _ = 0; |
|
69593 | 1230 |
fun is_trivial_let (Const (\<^const_name>\<open>Let\<close>, _) $ x $ t) = |
63575 | 1231 |
(case t of |
1232 |
Abs (_, _, t') => count_loose t' 0 <= 1 |
|
1233 |
| _ => true); |
|
1234 |
in |
|
1235 |
fn _ => fn ctxt => fn ct => |
|
1236 |
if is_trivial_let (Thm.term_of ct) |
|
1237 |
then SOME @{thm Let_def} (*no or one ocurrence of bound variable*) |
|
1238 |
else |
|
1239 |
let (*Norbert Schirmer's case*) |
|
1240 |
val t = Thm.term_of ct; |
|
70326 | 1241 |
val (t', ctxt') = yield_singleton (Variable.import_terms false) t ctxt; |
63575 | 1242 |
in |
1243 |
Option.map (hd o Variable.export ctxt' ctxt o single) |
|
69593 | 1244 |
(case t' of Const (\<^const_name>\<open>Let\<close>,_) $ x $ f => (* x and f are already in normal form *) |
63575 | 1245 |
if is_Free x orelse is_Bound x orelse is_Const x |
1246 |
then SOME @{thm Let_def} |
|
1247 |
else |
|
1248 |
let |
|
1249 |
val n = case f of (Abs (x, _, _)) => x | _ => "x"; |
|
1250 |
val cx = Thm.cterm_of ctxt x; |
|
1251 |
val xT = Thm.typ_of_cterm cx; |
|
1252 |
val cf = Thm.cterm_of ctxt f; |
|
1253 |
val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx); |
|
1254 |
val (_ $ _ $ g) = Thm.prop_of fx_g; |
|
1255 |
val g' = abstract_over (x, g); |
|
1256 |
val abs_g'= Abs (n, xT, g'); |
|
1257 |
in |
|
1258 |
if g aconv g' then |
|
1259 |
let |
|
1260 |
val rl = |
|
1261 |
infer_instantiate ctxt [(("f", 0), cf), (("x", 0), cx)] @{thm Let_unfold}; |
|
1262 |
in SOME (rl OF [fx_g]) end |
|
1263 |
else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g') |
|
1264 |
then NONE (*avoid identity conversion*) |
|
1265 |
else |
|
1266 |
let |
|
1267 |
val g'x = abs_g' $ x; |
|
1268 |
val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of ctxt g'x)); |
|
1269 |
val rl = |
|
1270 |
@{thm Let_folded} |> infer_instantiate ctxt |
|
1271 |
[(("f", 0), Thm.cterm_of ctxt f), |
|
1272 |
(("x", 0), cx), |
|
1273 |
(("g", 0), Thm.cterm_of ctxt abs_g')]; |
|
1274 |
in SOME (rl OF [Thm.transitive fx_g g_g'x]) end |
|
1275 |
end |
|
1276 |
| _ => NONE) |
|
1277 |
end |
|
1278 |
end |
|
1279 |
\<close> |
|
24035 | 1280 |
|
21151 | 1281 |
lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P" |
1282 |
proof |
|
23389 | 1283 |
assume "True \<Longrightarrow> PROP P" |
1284 |
from this [OF TrueI] show "PROP P" . |
|
21151 | 1285 |
next |
1286 |
assume "PROP P" |
|
23389 | 1287 |
then show "PROP P" . |
21151 | 1288 |
qed |
1289 |
||
59864 | 1290 |
lemma implies_True_equals: "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True" |
61169 | 1291 |
by standard (intro TrueI) |
59864 | 1292 |
|
1293 |
lemma False_implies_equals: "(False \<Longrightarrow> P) \<equiv> Trueprop True" |
|
61169 | 1294 |
by standard simp_all |
59864 | 1295 |
|
60183
4cd4c204578c
undid 6d7b7a037e8d because it does not help but slows simplification down by up to 5% (AODV)
nipkow
parents:
60169
diff
changeset
|
1296 |
(* This is not made a simp rule because it does not improve any proofs |
4cd4c204578c
undid 6d7b7a037e8d because it does not help but slows simplification down by up to 5% (AODV)
nipkow
parents:
60169
diff
changeset
|
1297 |
but slows some AFP entries down by 5% (cpu time). May 2015 *) |
63575 | 1298 |
lemma implies_False_swap: |
1299 |
"NO_MATCH (Trueprop False) P \<Longrightarrow> |
|
1300 |
(False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)" |
|
1301 |
by (rule swap_prems_eq) |
|
60169
5ef8ed685965
swap False to the right in assumptions to be eliminated at the right end
nipkow
parents:
60151
diff
changeset
|
1302 |
|
21151 | 1303 |
lemma ex_simps: |
60759 | 1304 |
"\<And>P Q. (\<exists>x. P x \<and> Q) = ((\<exists>x. P x) \<and> Q)" |
1305 |
"\<And>P Q. (\<exists>x. P \<and> Q x) = (P \<and> (\<exists>x. Q x))" |
|
1306 |
"\<And>P Q. (\<exists>x. P x \<or> Q) = ((\<exists>x. P x) \<or> Q)" |
|
1307 |
"\<And>P Q. (\<exists>x. P \<or> Q x) = (P \<or> (\<exists>x. Q x))" |
|
1308 |
"\<And>P Q. (\<exists>x. P x \<longrightarrow> Q) = ((\<forall>x. P x) \<longrightarrow> Q)" |
|
1309 |
"\<And>P Q. (\<exists>x. P \<longrightarrow> Q x) = (P \<longrightarrow> (\<exists>x. Q x))" |
|
61799 | 1310 |
\<comment> \<open>Miniscoping: pushing in existential quantifiers.\<close> |
21151 | 1311 |
by (iprover | blast)+ |
1312 |
||
1313 |
lemma all_simps: |
|
60759 | 1314 |
"\<And>P Q. (\<forall>x. P x \<and> Q) = ((\<forall>x. P x) \<and> Q)" |
1315 |
"\<And>P Q. (\<forall>x. P \<and> Q x) = (P \<and> (\<forall>x. Q x))" |
|
1316 |
"\<And>P Q. (\<forall>x. P x \<or> Q) = ((\<forall>x. P x) \<or> Q)" |
|
1317 |
"\<And>P Q. (\<forall>x. P \<or> Q x) = (P \<or> (\<forall>x. Q x))" |
|
1318 |
"\<And>P Q. (\<forall>x. P x \<longrightarrow> Q) = ((\<exists>x. P x) \<longrightarrow> Q)" |
|
1319 |
"\<And>P Q. (\<forall>x. P \<longrightarrow> Q x) = (P \<longrightarrow> (\<forall>x. Q x))" |
|
61799 | 1320 |
\<comment> \<open>Miniscoping: pushing in universal quantifiers.\<close> |
21151 | 1321 |
by (iprover | blast)+ |
15481 | 1322 |
|
21671 | 1323 |
lemmas [simp] = |
63575 | 1324 |
triv_forall_equality \<comment> \<open>prunes params\<close> |
1325 |
True_implies_equals implies_True_equals \<comment> \<open>prune \<open>True\<close> in asms\<close> |
|
1326 |
False_implies_equals \<comment> \<open>prune \<open>False\<close> in asms\<close> |
|
21671 | 1327 |
if_True |
1328 |
if_False |
|
1329 |
if_cancel |
|
1330 |
if_eq_cancel |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
67405
diff
changeset
|
1331 |
imp_disjL \<comment> \<open>In general it seems wrong to add distributive laws by default: they |
63575 | 1332 |
might cause exponential blow-up. But \<open>imp_disjL\<close> has been in for a while |
20973 | 1333 |
and cannot be removed without affecting existing proofs. Moreover, |
63575 | 1334 |
rewriting by \<open>(P \<or> Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))\<close> might be justified on the |
1335 |
grounds that it allows simplification of \<open>R\<close> in the two cases.\<close> |
|
21671 | 1336 |
conj_assoc |
1337 |
disj_assoc |
|
1338 |
de_Morgan_conj |
|
1339 |
de_Morgan_disj |
|
1340 |
imp_disj1 |
|
1341 |
imp_disj2 |
|
1342 |
not_imp |
|
1343 |
disj_not1 |
|
1344 |
not_all |
|
1345 |
not_ex |
|
1346 |
cases_simp |
|
1347 |
the_eq_trivial |
|
1348 |
the_sym_eq_trivial |
|
1349 |
ex_simps |
|
1350 |
all_simps |
|
1351 |
simp_thms |
|
1352 |
||
1353 |
lemmas [cong] = imp_cong simp_implies_cong |
|
62390 | 1354 |
lemmas [split] = if_split |
20973 | 1355 |
|
69593 | 1356 |
ML \<open>val HOL_ss = simpset_of \<^context>\<close> |
20973 | 1357 |
|
63575 | 1358 |
text \<open>Simplifies \<open>x\<close> assuming \<open>c\<close> and \<open>y\<close> assuming \<open>\<not> c\<close>.\<close> |
20944 | 1359 |
lemma if_cong: |
1360 |
assumes "b = c" |
|
63575 | 1361 |
and "c \<Longrightarrow> x = u" |
1362 |
and "\<not> c \<Longrightarrow> y = v" |
|
20944 | 1363 |
shows "(if b then x else y) = (if c then u else v)" |
38525 | 1364 |
using assms by simp |
20944 | 1365 |
|
63575 | 1366 |
text \<open>Prevents simplification of \<open>x\<close> and \<open>y\<close>: |
60758 | 1367 |
faster and allows the execution of functional programs.\<close> |
20944 | 1368 |
lemma if_weak_cong [cong]: |
1369 |
assumes "b = c" |
|
1370 |
shows "(if b then x else y) = (if c then x else y)" |
|
23553 | 1371 |
using assms by (rule arg_cong) |
20944 | 1372 |
|
60758 | 1373 |
text \<open>Prevents simplification of t: much faster\<close> |
20944 | 1374 |
lemma let_weak_cong: |
1375 |
assumes "a = b" |
|
1376 |
shows "(let x = a in t x) = (let x = b in t x)" |
|
23553 | 1377 |
using assms by (rule arg_cong) |
20944 | 1378 |
|
60758 | 1379 |
text \<open>To tidy up the result of a simproc. Only the RHS will be simplified.\<close> |
20944 | 1380 |
lemma eq_cong2: |
1381 |
assumes "u = u'" |
|
1382 |
shows "(t \<equiv> u) \<equiv> (t \<equiv> u')" |
|
23553 | 1383 |
using assms by simp |
20944 | 1384 |
|
63575 | 1385 |
lemma if_distrib: "f (if c then x else y) = (if c then f x else f y)" |
20944 | 1386 |
by simp |
1387 |
||
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67719
diff
changeset
|
1388 |
lemma if_distribR: "(if b then f else g) x = (if b then f x else g x)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67719
diff
changeset
|
1389 |
by simp |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67719
diff
changeset
|
1390 |
|
67673
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
1391 |
lemma all_if_distrib: "(\<forall>x. if x = a then P x else Q x) \<longleftrightarrow> P a \<and> (\<forall>x. x\<noteq>a \<longrightarrow> Q x)" |
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
1392 |
by auto |
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
1393 |
|
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
1394 |
lemma ex_if_distrib: "(\<exists>x. if x = a then P x else Q x) \<longleftrightarrow> P a \<or> (\<exists>x. x\<noteq>a \<and> Q x)" |
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
1395 |
by auto |
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
1396 |
|
67719
bffb7482faaa
new material on matrices, etc., and consolidating duplicate results about of_nat
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1397 |
lemma if_if_eq_conj: "(if P then if Q then x else y else y) = (if P \<and> Q then x else y)" |
bffb7482faaa
new material on matrices, etc., and consolidating duplicate results about of_nat
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1398 |
by simp |
bffb7482faaa
new material on matrices, etc., and consolidating duplicate results about of_nat
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1399 |
|
63575 | 1400 |
text \<open>As a simplification rule, it replaces all function equalities by |
60758 | 1401 |
first-order equalities.\<close> |
44277
bcb696533579
moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace
haftmann
parents:
44121
diff
changeset
|
1402 |
lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)" |
bcb696533579
moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace
haftmann
parents:
44121
diff
changeset
|
1403 |
by auto |
bcb696533579
moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace
haftmann
parents:
44121
diff
changeset
|
1404 |
|
17459 | 1405 |
|
60758 | 1406 |
subsubsection \<open>Generic cases and induction\<close> |
17459 | 1407 |
|
60758 | 1408 |
text \<open>Rule projections:\<close> |
1409 |
ML \<open> |
|
32172 | 1410 |
structure Project_Rule = Project_Rule |
25388 | 1411 |
( |
27126
3ede9103de8e
eliminated obsolete case_split_thm -- use case_split;
wenzelm
parents:
27107
diff
changeset
|
1412 |
val conjunct1 = @{thm conjunct1} |
3ede9103de8e
eliminated obsolete case_split_thm -- use case_split;
wenzelm
parents:
27107
diff
changeset
|
1413 |
val conjunct2 = @{thm conjunct2} |
3ede9103de8e
eliminated obsolete case_split_thm -- use case_split;
wenzelm
parents:
27107
diff
changeset
|
1414 |
val mp = @{thm mp} |
59929 | 1415 |
); |
60758 | 1416 |
\<close> |
17459 | 1417 |
|
59940
087d81f5213e
local setup of induction tools, with restricted access to auxiliary consts;
wenzelm
parents:
59929
diff
changeset
|
1418 |
context |
087d81f5213e
local setup of induction tools, with restricted access to auxiliary consts;
wenzelm
parents:
59929
diff
changeset
|
1419 |
begin |
087d81f5213e
local setup of induction tools, with restricted access to auxiliary consts;
wenzelm
parents:
59929
diff
changeset
|
1420 |
|
59990
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59970
diff
changeset
|
1421 |
qualified definition "induct_forall P \<equiv> \<forall>x. P x" |
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59970
diff
changeset
|
1422 |
qualified definition "induct_implies A B \<equiv> A \<longrightarrow> B" |
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59970
diff
changeset
|
1423 |
qualified definition "induct_equal x y \<equiv> x = y" |
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59970
diff
changeset
|
1424 |
qualified definition "induct_conj A B \<equiv> A \<and> B" |
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59970
diff
changeset
|
1425 |
qualified definition "induct_true \<equiv> True" |
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59970
diff
changeset
|
1426 |
qualified definition "induct_false \<equiv> False" |
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35115
diff
changeset
|
1427 |
|
59929 | 1428 |
lemma induct_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (induct_forall (\<lambda>x. P x))" |
18457 | 1429 |
by (unfold atomize_all induct_forall_def) |
11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
1430 |
|
59929 | 1431 |
lemma induct_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (induct_implies A B)" |
18457 | 1432 |
by (unfold atomize_imp induct_implies_def) |
11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
1433 |
|
59929 | 1434 |
lemma induct_equal_eq: "(x \<equiv> y) \<equiv> Trueprop (induct_equal x y)" |
18457 | 1435 |
by (unfold atomize_eq induct_equal_def) |
1436 |
||
59929 | 1437 |
lemma induct_conj_eq: "(A &&& B) \<equiv> Trueprop (induct_conj A B)" |
18457 | 1438 |
by (unfold atomize_conj induct_conj_def) |
1439 |
||
34908
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1440 |
lemmas induct_atomize' = induct_forall_eq induct_implies_eq induct_conj_eq |
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1441 |
lemmas induct_atomize = induct_atomize' induct_equal_eq |
45607 | 1442 |
lemmas induct_rulify' [symmetric] = induct_atomize' |
1443 |
lemmas induct_rulify [symmetric] = induct_atomize |
|
18457 | 1444 |
lemmas induct_rulify_fallback = |
1445 |
induct_forall_def induct_implies_def induct_equal_def induct_conj_def |
|
34908
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1446 |
induct_true_def induct_false_def |
18457 | 1447 |
|
11989 | 1448 |
lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) = |
1449 |
induct_conj (induct_forall A) (induct_forall B)" |
|
17589 | 1450 |
by (unfold induct_forall_def induct_conj_def) iprover |
11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
1451 |
|
11989 | 1452 |
lemma induct_implies_conj: "induct_implies C (induct_conj A B) = |
1453 |
induct_conj (induct_implies C A) (induct_implies C B)" |
|
17589 | 1454 |
by (unfold induct_implies_def induct_conj_def) iprover |
11989 | 1455 |
|
59929 | 1456 |
lemma induct_conj_curry: "(induct_conj A B \<Longrightarrow> PROP C) \<equiv> (A \<Longrightarrow> B \<Longrightarrow> PROP C)" |
13598
8bc77b17f59f
Fixed problem with induct_conj_curry: variable C should have type prop.
berghofe
parents:
13596
diff
changeset
|
1457 |
proof |
59929 | 1458 |
assume r: "induct_conj A B \<Longrightarrow> PROP C" |
1459 |
assume ab: A B |
|
1460 |
show "PROP C" by (rule r) (simp add: induct_conj_def ab) |
|
13598
8bc77b17f59f
Fixed problem with induct_conj_curry: variable C should have type prop.
berghofe
parents:
13596
diff
changeset
|
1461 |
next |
59929 | 1462 |
assume r: "A \<Longrightarrow> B \<Longrightarrow> PROP C" |
1463 |
assume ab: "induct_conj A B" |
|
1464 |
show "PROP C" by (rule r) (simp_all add: ab [unfolded induct_conj_def]) |
|
13598
8bc77b17f59f
Fixed problem with induct_conj_curry: variable C should have type prop.
berghofe
parents:
13596
diff
changeset
|
1465 |
qed |
11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
1466 |
|
11989 | 1467 |
lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry |
11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
1468 |
|
34908
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1469 |
lemma induct_trueI: "induct_true" |
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1470 |
by (simp add: induct_true_def) |
11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
1471 |
|
60758 | 1472 |
text \<open>Method setup.\<close> |
11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
1473 |
|
69605 | 1474 |
ML_file \<open>~~/src/Tools/induct.ML\<close> |
60758 | 1475 |
ML \<open> |
32171 | 1476 |
structure Induct = Induct |
27126
3ede9103de8e
eliminated obsolete case_split_thm -- use case_split;
wenzelm
parents:
27107
diff
changeset
|
1477 |
( |
3ede9103de8e
eliminated obsolete case_split_thm -- use case_split;
wenzelm
parents:
27107
diff
changeset
|
1478 |
val cases_default = @{thm case_split} |
3ede9103de8e
eliminated obsolete case_split_thm -- use case_split;
wenzelm
parents:
27107
diff
changeset
|
1479 |
val atomize = @{thms induct_atomize} |
34908
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1480 |
val rulify = @{thms induct_rulify'} |
27126
3ede9103de8e
eliminated obsolete case_split_thm -- use case_split;
wenzelm
parents:
27107
diff
changeset
|
1481 |
val rulify_fallback = @{thms induct_rulify_fallback} |
34988
cca208c8d619
Added setup for simplification of equality constraints in cases rules.
berghofe
parents:
34917
diff
changeset
|
1482 |
val equal_def = @{thm induct_equal_def} |
69593 | 1483 |
fun dest_def (Const (\<^const_name>\<open>induct_equal\<close>, _) $ t $ u) = SOME (t, u) |
34908
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1484 |
| dest_def _ = NONE |
58957 | 1485 |
fun trivial_tac ctxt = match_tac ctxt @{thms induct_trueI} |
27126
3ede9103de8e
eliminated obsolete case_split_thm -- use case_split;
wenzelm
parents:
27107
diff
changeset
|
1486 |
) |
60758 | 1487 |
\<close> |
11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
1488 |
|
69605 | 1489 |
ML_file \<open>~~/src/Tools/induction.ML\<close> |
45014
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
44921
diff
changeset
|
1490 |
|
60758 | 1491 |
declaration \<open> |
59940
087d81f5213e
local setup of induction tools, with restricted access to auxiliary consts;
wenzelm
parents:
59929
diff
changeset
|
1492 |
fn _ => Induct.map_simpset (fn ss => ss |
34908
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1493 |
addsimprocs |
69593 | 1494 |
[Simplifier.make_simproc \<^context> "swap_induct_false" |
1495 |
{lhss = [\<^term>\<open>induct_false \<Longrightarrow> PROP P \<Longrightarrow> PROP Q\<close>], |
|
61144 | 1496 |
proc = fn _ => fn _ => fn ct => |
1497 |
(case Thm.term_of ct of |
|
69597 | 1498 |
_ $ (P as _ $ \<^const>\<open>induct_false\<close>) $ (_ $ Q $ _) => |
61144 | 1499 |
if P <> Q then SOME Drule.swap_prems_eq else NONE |
62913 | 1500 |
| _ => NONE)}, |
69593 | 1501 |
Simplifier.make_simproc \<^context> "induct_equal_conj_curry" |
1502 |
{lhss = [\<^term>\<open>induct_conj P Q \<Longrightarrow> PROP R\<close>], |
|
61144 | 1503 |
proc = fn _ => fn _ => fn ct => |
1504 |
(case Thm.term_of ct of |
|
1505 |
_ $ (_ $ P) $ _ => |
|
1506 |
let |
|
69597 | 1507 |
fun is_conj (\<^const>\<open>induct_conj\<close> $ P $ Q) = |
61144 | 1508 |
is_conj P andalso is_conj Q |
69593 | 1509 |
| is_conj (Const (\<^const_name>\<open>induct_equal\<close>, _) $ _ $ _) = true |
69597 | 1510 |
| is_conj \<^const>\<open>induct_true\<close> = true |
1511 |
| is_conj \<^const>\<open>induct_false\<close> = true |
|
61144 | 1512 |
| is_conj _ = false |
1513 |
in if is_conj P then SOME @{thm induct_conj_curry} else NONE end |
|
62913 | 1514 |
| _ => NONE)}] |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53146
diff
changeset
|
1515 |
|> Simplifier.set_mksimps (fn ctxt => |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53146
diff
changeset
|
1516 |
Simpdata.mksimps Simpdata.mksimps_pairs ctxt #> |
59940
087d81f5213e
local setup of induction tools, with restricted access to auxiliary consts;
wenzelm
parents:
59929
diff
changeset
|
1517 |
map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback})))) |
60758 | 1518 |
\<close> |
34908
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1519 |
|
60758 | 1520 |
text \<open>Pre-simplification of induction and cases rules\<close> |
34908
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1521 |
|
59929 | 1522 |
lemma [induct_simp]: "(\<And>x. induct_equal x t \<Longrightarrow> PROP P x) \<equiv> PROP P t" |
34908
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1523 |
unfolding induct_equal_def |
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1524 |
proof |
59929 | 1525 |
assume r: "\<And>x. x = t \<Longrightarrow> PROP P x" |
1526 |
show "PROP P t" by (rule r [OF refl]) |
|
34908
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1527 |
next |
59929 | 1528 |
fix x |
1529 |
assume "PROP P t" "x = t" |
|
34908
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1530 |
then show "PROP P x" by simp |
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1531 |
qed |
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1532 |
|
59929 | 1533 |
lemma [induct_simp]: "(\<And>x. induct_equal t x \<Longrightarrow> PROP P x) \<equiv> PROP P t" |
34908
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1534 |
unfolding induct_equal_def |
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1535 |
proof |
59929 | 1536 |
assume r: "\<And>x. t = x \<Longrightarrow> PROP P x" |
1537 |
show "PROP P t" by (rule r [OF refl]) |
|
34908
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1538 |
next |
59929 | 1539 |
fix x |
1540 |
assume "PROP P t" "t = x" |
|
34908
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1541 |
then show "PROP P x" by simp |
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1542 |
qed |
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1543 |
|
59929 | 1544 |
lemma [induct_simp]: "(induct_false \<Longrightarrow> P) \<equiv> Trueprop induct_true" |
34908
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1545 |
unfolding induct_false_def induct_true_def |
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1546 |
by (iprover intro: equal_intr_rule) |
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1547 |
|
59929 | 1548 |
lemma [induct_simp]: "(induct_true \<Longrightarrow> PROP P) \<equiv> PROP P" |
34908
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1549 |
unfolding induct_true_def |
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1550 |
proof |
59929 | 1551 |
assume "True \<Longrightarrow> PROP P" |
1552 |
then show "PROP P" using TrueI . |
|
34908
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1553 |
next |
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1554 |
assume "PROP P" |
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1555 |
then show "PROP P" . |
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1556 |
qed |
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1557 |
|
59929 | 1558 |
lemma [induct_simp]: "(PROP P \<Longrightarrow> induct_true) \<equiv> Trueprop induct_true" |
34908
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1559 |
unfolding induct_true_def |
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1560 |
by (iprover intro: equal_intr_rule) |
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1561 |
|
62958
b41c1cb5e251
Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents:
62913
diff
changeset
|
1562 |
lemma [induct_simp]: "(\<And>x::'a::{}. induct_true) \<equiv> Trueprop induct_true" |
34908
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1563 |
unfolding induct_true_def |
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1564 |
by (iprover intro: equal_intr_rule) |
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1565 |
|
59929 | 1566 |
lemma [induct_simp]: "induct_implies induct_true P \<equiv> P" |
34908
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1567 |
by (simp add: induct_implies_def induct_true_def) |
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1568 |
|
59929 | 1569 |
lemma [induct_simp]: "x = x \<longleftrightarrow> True" |
34908
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1570 |
by (rule simp_thms) |
d546e75631bb
Added setup for simplification of equality constraints in induction rules.
berghofe
parents:
34294
diff
changeset
|
1571 |
|
59940
087d81f5213e
local setup of induction tools, with restricted access to auxiliary consts;
wenzelm
parents:
59929
diff
changeset
|
1572 |
end |
18457 | 1573 |
|
69605 | 1574 |
ML_file \<open>~~/src/Tools/induct_tacs.ML\<close> |
27126
3ede9103de8e
eliminated obsolete case_split_thm -- use case_split;
wenzelm
parents:
27107
diff
changeset
|
1575 |
|
20944 | 1576 |
|
60758 | 1577 |
subsubsection \<open>Coherent logic\<close> |
28325 | 1578 |
|
69605 | 1579 |
ML_file \<open>~~/src/Tools/coherent.ML\<close> |
60758 | 1580 |
ML \<open> |
32734 | 1581 |
structure Coherent = Coherent |
28325 | 1582 |
( |
55632 | 1583 |
val atomize_elimL = @{thm atomize_elimL}; |
1584 |
val atomize_exL = @{thm atomize_exL}; |
|
1585 |
val atomize_conjL = @{thm atomize_conjL}; |
|
1586 |
val atomize_disjL = @{thm atomize_disjL}; |
|
69593 | 1587 |
val operator_names = [\<^const_name>\<open>HOL.disj\<close>, \<^const_name>\<open>HOL.conj\<close>, \<^const_name>\<open>Ex\<close>]; |
28325 | 1588 |
); |
60758 | 1589 |
\<close> |
28325 | 1590 |
|
1591 |
||
60758 | 1592 |
subsubsection \<open>Reorienting equalities\<close> |
31024
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
30980
diff
changeset
|
1593 |
|
60758 | 1594 |
ML \<open> |
31024
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
30980
diff
changeset
|
1595 |
signature REORIENT_PROC = |
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
30980
diff
changeset
|
1596 |
sig |
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
30980
diff
changeset
|
1597 |
val add : (term -> bool) -> theory -> theory |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51692
diff
changeset
|
1598 |
val proc : morphism -> Proof.context -> cterm -> thm option |
31024
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
30980
diff
changeset
|
1599 |
end; |
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
30980
diff
changeset
|
1600 |
|
33523 | 1601 |
structure Reorient_Proc : REORIENT_PROC = |
31024
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
30980
diff
changeset
|
1602 |
struct |
33523 | 1603 |
structure Data = Theory_Data |
31024
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
30980
diff
changeset
|
1604 |
( |
33523 | 1605 |
type T = ((term -> bool) * stamp) list; |
1606 |
val empty = []; |
|
31024
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
30980
diff
changeset
|
1607 |
val extend = I; |
67405
e9ab4ad7bd15
uniform use of Standard ML op-infix -- eliminated warnings;
wenzelm
parents:
67399
diff
changeset
|
1608 |
fun merge data : T = Library.merge (eq_snd (op =)) data; |
33523 | 1609 |
); |
1610 |
fun add m = Data.map (cons (m, stamp ())); |
|
1611 |
fun matches thy t = exists (fn (m, _) => m t) (Data.get thy); |
|
31024
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
30980
diff
changeset
|
1612 |
|
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
30980
diff
changeset
|
1613 |
val meta_reorient = @{thm eq_commute [THEN eq_reflection]}; |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51692
diff
changeset
|
1614 |
fun proc phi ctxt ct = |
31024
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
30980
diff
changeset
|
1615 |
let |
42361 | 1616 |
val thy = Proof_Context.theory_of ctxt; |
31024
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
30980
diff
changeset
|
1617 |
in |
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
30980
diff
changeset
|
1618 |
case Thm.term_of ct of |
33523 | 1619 |
(_ $ t $ u) => if matches thy u then NONE else SOME meta_reorient |
31024
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
30980
diff
changeset
|
1620 |
| _ => NONE |
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
30980
diff
changeset
|
1621 |
end; |
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
30980
diff
changeset
|
1622 |
end; |
60758 | 1623 |
\<close> |
31024
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
30980
diff
changeset
|
1624 |
|
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
30980
diff
changeset
|
1625 |
|
60758 | 1626 |
subsection \<open>Other simple lemmas and lemma duplicates\<close> |
20944 | 1627 |
|
68975
5ce4d117cea7
A few new results, elimination of duplicates and more use of "pairwise"
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
1628 |
lemma all_cong1: "(\<And>x. P x = P' x) \<Longrightarrow> (\<forall>x. P x) = (\<forall>x. P' x)" |
5ce4d117cea7
A few new results, elimination of duplicates and more use of "pairwise"
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
1629 |
by auto |
5ce4d117cea7
A few new results, elimination of duplicates and more use of "pairwise"
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
1630 |
|
5ce4d117cea7
A few new results, elimination of duplicates and more use of "pairwise"
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
1631 |
lemma ex_cong1: "(\<And>x. P x = P' x) \<Longrightarrow> (\<exists>x. P x) = (\<exists>x. P' x)" |
5ce4d117cea7
A few new results, elimination of duplicates and more use of "pairwise"
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
1632 |
by auto |
5ce4d117cea7
A few new results, elimination of duplicates and more use of "pairwise"
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
1633 |
|
67091 | 1634 |
lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow> (\<forall>x. Q x \<longrightarrow> P x) = (\<forall>x. Q x \<longrightarrow> P' x)" |
66836 | 1635 |
by auto |
1636 |
||
67091 | 1637 |
lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow> (\<exists>x. Q x \<and> P x) = (\<exists>x. Q x \<and> P' x)" |
66836 | 1638 |
by auto |
1639 |
||
60759 | 1640 |
lemma ex1_eq [iff]: "\<exists>!x. x = t" "\<exists>!x. t = x" |
20944 | 1641 |
by blast+ |
1642 |
||
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1643 |
lemma choice_eq: "(\<forall>x. \<exists>!y. P x y) = (\<exists>!f. \<forall>x. P x (f x))" (is "?lhs = ?rhs") |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1644 |
proof (intro iffI allI) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1645 |
assume L: ?lhs |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1646 |
then have \<section>: "\<forall>x. P x (THE y. P x y)" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1647 |
by (best intro: theI') |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1648 |
show ?rhs |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1649 |
by (rule ex1I) (use L \<section> in \<open>fast+\<close>) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1650 |
next |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1651 |
fix x |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1652 |
assume R: ?rhs |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1653 |
then obtain f where f: "\<forall>x. P x (f x)" and f1: "\<And>y. (\<forall>x. P x (y x)) \<Longrightarrow> y = f" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1654 |
by (blast elim: ex1E) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1655 |
show "\<exists>!y. P x y" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1656 |
proof (rule ex1I) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1657 |
show "P x (f x)" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1658 |
using f by blast |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1659 |
show "y = f x" if "P x y" for y |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1660 |
proof - |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1661 |
have "P z (if z = x then y else f z)" for z |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1662 |
using f that by (auto split: if_split) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1663 |
with f1 [of "\<lambda>z. if z = x then y else f z"] f |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1664 |
show ?thesis |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1665 |
by (auto simp add: split: if_split_asm dest: fun_cong) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1666 |
qed |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1667 |
qed |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71517
diff
changeset
|
1668 |
qed |
20944 | 1669 |
|
22218 | 1670 |
lemmas eq_sym_conv = eq_commute |
1671 |
||
23037
6c72943a71b1
added a set of NNF normalization lemmas and nnf_conv
chaieb
parents:
22993
diff
changeset
|
1672 |
lemma nnf_simps: |
63575 | 1673 |
"(\<not> (P \<and> Q)) = (\<not> P \<or> \<not> Q)" |
1674 |
"(\<not> (P \<or> Q)) = (\<not> P \<and> \<not> Q)" |
|
1675 |
"(P \<longrightarrow> Q) = (\<not> P \<or> Q)" |
|
1676 |
"(P = Q) = ((P \<and> Q) \<or> (\<not> P \<and> \<not> Q))" |
|
1677 |
"(\<not> (P = Q)) = ((P \<and> \<not> Q) \<or> (\<not> P \<and> Q))" |
|
1678 |
"(\<not> \<not> P) = P" |
|
1679 |
by blast+ |
|
1680 |
||
23037
6c72943a71b1
added a set of NNF normalization lemmas and nnf_conv
chaieb
parents:
22993
diff
changeset
|
1681 |
|
60758 | 1682 |
subsection \<open>Basic ML bindings\<close> |
21671 | 1683 |
|
60758 | 1684 |
ML \<open> |
22129 | 1685 |
val FalseE = @{thm FalseE} |
1686 |
val Let_def = @{thm Let_def} |
|
1687 |
val TrueI = @{thm TrueI} |
|
1688 |
val allE = @{thm allE} |
|
1689 |
val allI = @{thm allI} |
|
1690 |
val all_dupE = @{thm all_dupE} |
|
1691 |
val arg_cong = @{thm arg_cong} |
|
1692 |
val box_equals = @{thm box_equals} |
|
1693 |
val ccontr = @{thm ccontr} |
|
1694 |
val classical = @{thm classical} |
|
1695 |
val conjE = @{thm conjE} |
|
1696 |
val conjI = @{thm conjI} |
|
1697 |
val conjunct1 = @{thm conjunct1} |
|
1698 |
val conjunct2 = @{thm conjunct2} |
|
1699 |
val disjCI = @{thm disjCI} |
|
1700 |
val disjE = @{thm disjE} |
|
1701 |
val disjI1 = @{thm disjI1} |
|
1702 |
val disjI2 = @{thm disjI2} |
|
1703 |
val eq_reflection = @{thm eq_reflection} |
|
1704 |
val ex1E = @{thm ex1E} |
|
1705 |
val ex1I = @{thm ex1I} |
|
1706 |
val ex1_implies_ex = @{thm ex1_implies_ex} |
|
1707 |
val exE = @{thm exE} |
|
1708 |
val exI = @{thm exI} |
|
1709 |
val excluded_middle = @{thm excluded_middle} |
|
1710 |
val ext = @{thm ext} |
|
1711 |
val fun_cong = @{thm fun_cong} |
|
1712 |
val iffD1 = @{thm iffD1} |
|
1713 |
val iffD2 = @{thm iffD2} |
|
1714 |
val iffI = @{thm iffI} |
|
1715 |
val impE = @{thm impE} |
|
1716 |
val impI = @{thm impI} |
|
1717 |
val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq} |
|
1718 |
val mp = @{thm mp} |
|
1719 |
val notE = @{thm notE} |
|
1720 |
val notI = @{thm notI} |
|
1721 |
val not_all = @{thm not_all} |
|
1722 |
val not_ex = @{thm not_ex} |
|
1723 |
val not_iff = @{thm not_iff} |
|
1724 |
val not_not = @{thm not_not} |
|
1725 |
val not_sym = @{thm not_sym} |
|
1726 |
val refl = @{thm refl} |
|
1727 |
val rev_mp = @{thm rev_mp} |
|
1728 |
val spec = @{thm spec} |
|
1729 |
val ssubst = @{thm ssubst} |
|
1730 |
val subst = @{thm subst} |
|
1731 |
val sym = @{thm sym} |
|
1732 |
val trans = @{thm trans} |
|
60758 | 1733 |
\<close> |
21671 | 1734 |
|
70486 | 1735 |
locale cnf |
1736 |
begin |
|
1737 |
||
1738 |
lemma clause2raw_notE: "\<lbrakk>P; \<not>P\<rbrakk> \<Longrightarrow> False" by auto |
|
1739 |
lemma clause2raw_not_disj: "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> \<not> (P \<or> Q)" by auto |
|
1740 |
lemma clause2raw_not_not: "P \<Longrightarrow> \<not>\<not> P" by auto |
|
1741 |
||
1742 |
lemma iff_refl: "(P::bool) = P" by auto |
|
1743 |
lemma iff_trans: "[| (P::bool) = Q; Q = R |] ==> P = R" by auto |
|
1744 |
lemma conj_cong: "[| P = P'; Q = Q' |] ==> (P \<and> Q) = (P' \<and> Q')" by auto |
|
1745 |
lemma disj_cong: "[| P = P'; Q = Q' |] ==> (P \<or> Q) = (P' \<or> Q')" by auto |
|
1746 |
||
1747 |
lemma make_nnf_imp: "[| (\<not>P) = P'; Q = Q' |] ==> (P \<longrightarrow> Q) = (P' \<or> Q')" by auto |
|
1748 |
lemma make_nnf_iff: "[| P = P'; (\<not>P) = NP; Q = Q'; (\<not>Q) = NQ |] ==> (P = Q) = ((P' \<or> NQ) \<and> (NP \<or> Q'))" by auto |
|
1749 |
lemma make_nnf_not_false: "(\<not>False) = True" by auto |
|
1750 |
lemma make_nnf_not_true: "(\<not>True) = False" by auto |
|
1751 |
lemma make_nnf_not_conj: "[| (\<not>P) = P'; (\<not>Q) = Q' |] ==> (\<not>(P \<and> Q)) = (P' \<or> Q')" by auto |
|
1752 |
lemma make_nnf_not_disj: "[| (\<not>P) = P'; (\<not>Q) = Q' |] ==> (\<not>(P \<or> Q)) = (P' \<and> Q')" by auto |
|
1753 |
lemma make_nnf_not_imp: "[| P = P'; (\<not>Q) = Q' |] ==> (\<not>(P \<longrightarrow> Q)) = (P' \<and> Q')" by auto |
|
1754 |
lemma make_nnf_not_iff: "[| P = P'; (\<not>P) = NP; Q = Q'; (\<not>Q) = NQ |] ==> (\<not>(P = Q)) = ((P' \<or> Q') \<and> (NP \<or> NQ))" by auto |
|
1755 |
lemma make_nnf_not_not: "P = P' ==> (\<not>\<not>P) = P'" by auto |
|
1756 |
||
1757 |
lemma simp_TF_conj_True_l: "[| P = True; Q = Q' |] ==> (P \<and> Q) = Q'" by auto |
|
1758 |
lemma simp_TF_conj_True_r: "[| P = P'; Q = True |] ==> (P \<and> Q) = P'" by auto |
|
1759 |
lemma simp_TF_conj_False_l: "P = False ==> (P \<and> Q) = False" by auto |
|
1760 |
lemma simp_TF_conj_False_r: "Q = False ==> (P \<and> Q) = False" by auto |
|
1761 |
lemma simp_TF_disj_True_l: "P = True ==> (P \<or> Q) = True" by auto |
|
1762 |
lemma simp_TF_disj_True_r: "Q = True ==> (P \<or> Q) = True" by auto |
|
1763 |
lemma simp_TF_disj_False_l: "[| P = False; Q = Q' |] ==> (P \<or> Q) = Q'" by auto |
|
1764 |
lemma simp_TF_disj_False_r: "[| P = P'; Q = False |] ==> (P \<or> Q) = P'" by auto |
|
1765 |
||
1766 |
lemma make_cnf_disj_conj_l: "[| (P \<or> R) = PR; (Q \<or> R) = QR |] ==> ((P \<and> Q) \<or> R) = (PR \<and> QR)" by auto |
|
1767 |
lemma make_cnf_disj_conj_r: "[| (P \<or> Q) = PQ; (P \<or> R) = PR |] ==> (P \<or> (Q \<and> R)) = (PQ \<and> PR)" by auto |
|
1768 |
||
1769 |
lemma make_cnfx_disj_ex_l: "((\<exists>(x::bool). P x) \<or> Q) = (\<exists>x. P x \<or> Q)" by auto |
|
1770 |
lemma make_cnfx_disj_ex_r: "(P \<or> (\<exists>(x::bool). Q x)) = (\<exists>x. P \<or> Q x)" by auto |
|
1771 |
lemma make_cnfx_newlit: "(P \<or> Q) = (\<exists>x. (P \<or> x) \<and> (Q \<or> \<not>x))" by auto |
|
1772 |
lemma make_cnfx_ex_cong: "(\<forall>(x::bool). P x = Q x) \<Longrightarrow> (\<exists>x. P x) = (\<exists>x. Q x)" by auto |
|
1773 |
||
1774 |
lemma weakening_thm: "[| P; Q |] ==> Q" by auto |
|
1775 |
||
1776 |
lemma cnftac_eq_imp: "[| P = Q; P |] ==> Q" by auto |
|
1777 |
||
1778 |
end |
|
1779 |
||
69605 | 1780 |
ML_file \<open>Tools/cnf.ML\<close> |
55239 | 1781 |
|
21671 | 1782 |
|
61799 | 1783 |
section \<open>\<open>NO_MATCH\<close> simproc\<close> |
58775
9cd64a66a765
move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
hoelzl
parents:
58659
diff
changeset
|
1784 |
|
60758 | 1785 |
text \<open> |
63575 | 1786 |
The simplification procedure can be used to avoid simplification of terms |
1787 |
of a certain form. |
|
60758 | 1788 |
\<close> |
58775
9cd64a66a765
move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
hoelzl
parents:
58659
diff
changeset
|
1789 |
|
63575 | 1790 |
definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool" |
1791 |
where "NO_MATCH pat val \<equiv> True" |
|
58830 | 1792 |
|
63575 | 1793 |
lemma NO_MATCH_cong[cong]: "NO_MATCH pat val = NO_MATCH pat val" |
1794 |
by (rule refl) |
|
58775
9cd64a66a765
move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
hoelzl
parents:
58659
diff
changeset
|
1795 |
|
58830 | 1796 |
declare [[coercion_args NO_MATCH - -]] |
1797 |
||
60758 | 1798 |
simproc_setup NO_MATCH ("NO_MATCH pat val") = \<open>fn _ => fn ctxt => fn ct => |
58775
9cd64a66a765
move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
hoelzl
parents:
58659
diff
changeset
|
1799 |
let |
9cd64a66a765
move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
hoelzl
parents:
58659
diff
changeset
|
1800 |
val thy = Proof_Context.theory_of ctxt |
9cd64a66a765
move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
hoelzl
parents:
58659
diff
changeset
|
1801 |
val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd) |
9cd64a66a765
move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
hoelzl
parents:
58659
diff
changeset
|
1802 |
val m = Pattern.matches thy (dest_binop (Thm.term_of ct)) |
9cd64a66a765
move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
hoelzl
parents:
58659
diff
changeset
|
1803 |
in if m then NONE else SOME @{thm NO_MATCH_def} end |
60758 | 1804 |
\<close> |
58775
9cd64a66a765
move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
hoelzl
parents:
58659
diff
changeset
|
1805 |
|
60758 | 1806 |
text \<open> |
69593 | 1807 |
This setup ensures that a rewrite rule of the form \<^term>\<open>NO_MATCH pat val \<Longrightarrow> t\<close> |
63575 | 1808 |
is only applied, if the pattern \<open>pat\<close> does not match the value \<open>val\<close>. |
60758 | 1809 |
\<close> |
58775
9cd64a66a765
move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
hoelzl
parents:
58659
diff
changeset
|
1810 |
|
9cd64a66a765
move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
hoelzl
parents:
58659
diff
changeset
|
1811 |
|
63575 | 1812 |
text\<open> |
1813 |
Tagging a premise of a simp rule with ASSUMPTION forces the simplifier |
|
1814 |
not to simplify the argument and to solve it by an assumption. |
|
1815 |
\<close> |
|
61202 | 1816 |
|
63575 | 1817 |
definition ASSUMPTION :: "bool \<Rightarrow> bool" |
1818 |
where "ASSUMPTION A \<equiv> A" |
|
61202 | 1819 |
|
1820 |
lemma ASSUMPTION_cong[cong]: "ASSUMPTION A = ASSUMPTION A" |
|
63575 | 1821 |
by (rule refl) |
61202 | 1822 |
|
1823 |
lemma ASSUMPTION_I: "A \<Longrightarrow> ASSUMPTION A" |
|
63575 | 1824 |
by (simp add: ASSUMPTION_def) |
61202 | 1825 |
|
1826 |
lemma ASSUMPTION_D: "ASSUMPTION A \<Longrightarrow> A" |
|
63575 | 1827 |
by (simp add: ASSUMPTION_def) |
61202 | 1828 |
|
61222 | 1829 |
setup \<open> |
61202 | 1830 |
let |
1831 |
val asm_sol = mk_solver "ASSUMPTION" (fn ctxt => |
|
1832 |
resolve_tac ctxt [@{thm ASSUMPTION_I}] THEN' |
|
1833 |
resolve_tac ctxt (Simplifier.prems_of ctxt)) |
|
1834 |
in |
|
1835 |
map_theory_simpset (fn ctxt => Simplifier.addSolver (ctxt,asm_sol)) |
|
1836 |
end |
|
61222 | 1837 |
\<close> |
61202 | 1838 |
|
1839 |
||
60758 | 1840 |
subsection \<open>Code generator setup\<close> |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1841 |
|
60758 | 1842 |
subsubsection \<open>Generic code generator preprocessor setup\<close> |
31151 | 1843 |
|
63575 | 1844 |
lemma conj_left_cong: "P \<longleftrightarrow> Q \<Longrightarrow> P \<and> R \<longleftrightarrow> Q \<and> R" |
53146
3a93bc5d3370
congruence rules for code_simp to mimic typical non-strict behaviour of conj and disj
haftmann
parents:
52654
diff
changeset
|
1845 |
by (fact arg_cong) |
3a93bc5d3370
congruence rules for code_simp to mimic typical non-strict behaviour of conj and disj
haftmann
parents:
52654
diff
changeset
|
1846 |
|
63575 | 1847 |
lemma disj_left_cong: "P \<longleftrightarrow> Q \<Longrightarrow> P \<or> R \<longleftrightarrow> Q \<or> R" |
53146
3a93bc5d3370
congruence rules for code_simp to mimic typical non-strict behaviour of conj and disj
haftmann
parents:
52654
diff
changeset
|
1848 |
by (fact arg_cong) |
3a93bc5d3370
congruence rules for code_simp to mimic typical non-strict behaviour of conj and disj
haftmann
parents:
52654
diff
changeset
|
1849 |
|
60758 | 1850 |
setup \<open> |
58826 | 1851 |
Code_Preproc.map_pre (put_simpset HOL_basic_ss) #> |
1852 |
Code_Preproc.map_post (put_simpset HOL_basic_ss) #> |
|
1853 |
Code_Simp.map_ss (put_simpset HOL_basic_ss #> |
|
1854 |
Simplifier.add_cong @{thm conj_left_cong} #> |
|
1855 |
Simplifier.add_cong @{thm disj_left_cong}) |
|
60758 | 1856 |
\<close> |
31151 | 1857 |
|
53146
3a93bc5d3370
congruence rules for code_simp to mimic typical non-strict behaviour of conj and disj
haftmann
parents:
52654
diff
changeset
|
1858 |
|
60758 | 1859 |
subsubsection \<open>Equality\<close> |
24844
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24842
diff
changeset
|
1860 |
|
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38795
diff
changeset
|
1861 |
class equal = |
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38795
diff
changeset
|
1862 |
fixes equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38795
diff
changeset
|
1863 |
assumes equal_eq: "equal x y \<longleftrightarrow> x = y" |
26513 | 1864 |
begin |
1865 |
||
67399 | 1866 |
lemma equal: "equal = (=)" |
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38795
diff
changeset
|
1867 |
by (rule ext equal_eq)+ |
28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28325
diff
changeset
|
1868 |
|
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38795
diff
changeset
|
1869 |
lemma equal_refl: "equal x x \<longleftrightarrow> True" |
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38795
diff
changeset
|
1870 |
unfolding equal by rule+ |
28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28325
diff
changeset
|
1871 |
|
67399 | 1872 |
lemma eq_equal: "(=) \<equiv> equal" |
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38795
diff
changeset
|
1873 |
by (rule eq_reflection) (rule ext, rule ext, rule sym, rule equal_eq) |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1874 |
|
26513 | 1875 |
end |
1876 |
||
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38795
diff
changeset
|
1877 |
declare eq_equal [symmetric, code_post] |
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38795
diff
changeset
|
1878 |
declare eq_equal [code] |
30966 | 1879 |
|
60758 | 1880 |
setup \<open> |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51692
diff
changeset
|
1881 |
Code_Preproc.map_pre (fn ctxt => |
61144 | 1882 |
ctxt addsimprocs |
69593 | 1883 |
[Simplifier.make_simproc \<^context> "equal" |
1884 |
{lhss = [\<^term>\<open>HOL.eq\<close>], |
|
61144 | 1885 |
proc = fn _ => fn _ => fn ct => |
1886 |
(case Thm.term_of ct of |
|
69593 | 1887 |
Const (_, Type (\<^type_name>\<open>fun\<close>, [Type _, _])) => SOME @{thm eq_equal} |
62913 | 1888 |
| _ => NONE)}]) |
60758 | 1889 |
\<close> |
31151 | 1890 |
|
30966 | 1891 |
|
60758 | 1892 |
subsubsection \<open>Generic code generator foundation\<close> |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1893 |
|
69593 | 1894 |
text \<open>Datatype \<^typ>\<open>bool\<close>\<close> |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1895 |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1896 |
code_datatype True False |
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1897 |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1898 |
lemma [code]: |
33185
247f6c6969d9
tuned code setup for primitive boolean connectors
haftmann
parents:
33084
diff
changeset
|
1899 |
shows "False \<and> P \<longleftrightarrow> False" |
247f6c6969d9
tuned code setup for primitive boolean connectors
haftmann
parents:
33084
diff
changeset
|
1900 |
and "True \<and> P \<longleftrightarrow> P" |
247f6c6969d9
tuned code setup for primitive boolean connectors
haftmann
parents:
33084
diff
changeset
|
1901 |
and "P \<and> False \<longleftrightarrow> False" |
63575 | 1902 |
and "P \<and> True \<longleftrightarrow> P" |
1903 |
by simp_all |
|
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1904 |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1905 |
lemma [code]: |
33185
247f6c6969d9
tuned code setup for primitive boolean connectors
haftmann
parents:
33084
diff
changeset
|
1906 |
shows "False \<or> P \<longleftrightarrow> P" |
247f6c6969d9
tuned code setup for primitive boolean connectors
haftmann
parents:
33084
diff
changeset
|
1907 |
and "True \<or> P \<longleftrightarrow> True" |
247f6c6969d9
tuned code setup for primitive boolean connectors
haftmann
parents:
33084
diff
changeset
|
1908 |
and "P \<or> False \<longleftrightarrow> P" |
63575 | 1909 |
and "P \<or> True \<longleftrightarrow> True" |
1910 |
by simp_all |
|
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1911 |
|
33185
247f6c6969d9
tuned code setup for primitive boolean connectors
haftmann
parents:
33084
diff
changeset
|
1912 |
lemma [code]: |
247f6c6969d9
tuned code setup for primitive boolean connectors
haftmann
parents:
33084
diff
changeset
|
1913 |
shows "(False \<longrightarrow> P) \<longleftrightarrow> True" |
247f6c6969d9
tuned code setup for primitive boolean connectors
haftmann
parents:
33084
diff
changeset
|
1914 |
and "(True \<longrightarrow> P) \<longleftrightarrow> P" |
247f6c6969d9
tuned code setup for primitive boolean connectors
haftmann
parents:
33084
diff
changeset
|
1915 |
and "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P" |
63575 | 1916 |
and "(P \<longrightarrow> True) \<longleftrightarrow> True" |
1917 |
by simp_all |
|
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1918 |
|
69593 | 1919 |
text \<open>More about \<^typ>\<open>prop\<close>\<close> |
39421
b6a77cffc231
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents:
39403
diff
changeset
|
1920 |
|
b6a77cffc231
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents:
39403
diff
changeset
|
1921 |
lemma [code nbe]: |
58826 | 1922 |
shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q" |
39421
b6a77cffc231
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents:
39403
diff
changeset
|
1923 |
and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True" |
63575 | 1924 |
and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)" |
1925 |
by (auto intro!: equal_intr_rule) |
|
39421
b6a77cffc231
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents:
39403
diff
changeset
|
1926 |
|
63575 | 1927 |
lemma Trueprop_code [code]: "Trueprop True \<equiv> Code_Generator.holds" |
39421
b6a77cffc231
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents:
39403
diff
changeset
|
1928 |
by (auto intro!: equal_intr_rule holds) |
b6a77cffc231
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents:
39403
diff
changeset
|
1929 |
|
b6a77cffc231
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents:
39403
diff
changeset
|
1930 |
declare Trueprop_code [symmetric, code_post] |
b6a77cffc231
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents:
39403
diff
changeset
|
1931 |
|
60758 | 1932 |
text \<open>Equality\<close> |
39421
b6a77cffc231
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents:
39403
diff
changeset
|
1933 |
|
b6a77cffc231
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents:
39403
diff
changeset
|
1934 |
declare simp_thms(6) [code nbe] |
b6a77cffc231
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents:
39403
diff
changeset
|
1935 |
|
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38795
diff
changeset
|
1936 |
instantiation itself :: (type) equal |
31132 | 1937 |
begin |
1938 |
||
63575 | 1939 |
definition equal_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool" |
1940 |
where "equal_itself x y \<longleftrightarrow> x = y" |
|
31132 | 1941 |
|
63575 | 1942 |
instance |
1943 |
by standard (fact equal_itself_def) |
|
31132 | 1944 |
|
1945 |
end |
|
1946 |
||
63575 | 1947 |
lemma equal_itself_code [code]: "equal TYPE('a) TYPE('a) \<longleftrightarrow> True" |
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38795
diff
changeset
|
1948 |
by (simp add: equal) |
31132 | 1949 |
|
69593 | 1950 |
setup \<open>Sign.add_const_constraint (\<^const_name>\<open>equal\<close>, SOME \<^typ>\<open>'a::type \<Rightarrow> 'a \<Rightarrow> bool\<close>)\<close> |
31956
c3844c4d0c2c
more accurate certificates for constant aliasses
haftmann
parents:
31902
diff
changeset
|
1951 |
|
67399 | 1952 |
lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> (((=) :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)" |
63575 | 1953 |
(is "?ofclass \<equiv> ?equal") |
31956
c3844c4d0c2c
more accurate certificates for constant aliasses
haftmann
parents:
31902
diff
changeset
|
1954 |
proof |
c3844c4d0c2c
more accurate certificates for constant aliasses
haftmann
parents:
31902
diff
changeset
|
1955 |
assume "PROP ?ofclass" |
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38795
diff
changeset
|
1956 |
show "PROP ?equal" |
69593 | 1957 |
by (tactic \<open>ALLGOALS (resolve_tac \<^context> [Thm.unconstrainT @{thm eq_equal}])\<close>) |
60758 | 1958 |
(fact \<open>PROP ?ofclass\<close>) |
31956
c3844c4d0c2c
more accurate certificates for constant aliasses
haftmann
parents:
31902
diff
changeset
|
1959 |
next |
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38795
diff
changeset
|
1960 |
assume "PROP ?equal" |
31956
c3844c4d0c2c
more accurate certificates for constant aliasses
haftmann
parents:
31902
diff
changeset
|
1961 |
show "PROP ?ofclass" proof |
60758 | 1962 |
qed (simp add: \<open>PROP ?equal\<close>) |
31956
c3844c4d0c2c
more accurate certificates for constant aliasses
haftmann
parents:
31902
diff
changeset
|
1963 |
qed |
c3844c4d0c2c
more accurate certificates for constant aliasses
haftmann
parents:
31902
diff
changeset
|
1964 |
|
69593 | 1965 |
setup \<open>Sign.add_const_constraint (\<^const_name>\<open>equal\<close>, SOME \<^typ>\<open>'a::equal \<Rightarrow> 'a \<Rightarrow> bool\<close>)\<close> |
58826 | 1966 |
|
60758 | 1967 |
setup \<open>Nbe.add_const_alias @{thm equal_alias_cert}\<close> |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1968 |
|
60758 | 1969 |
text \<open>Cases\<close> |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1970 |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1971 |
lemma Let_case_cert: |
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1972 |
assumes "CASE \<equiv> (\<lambda>x. Let x f)" |
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1973 |
shows "CASE x \<equiv> f x" |
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1974 |
using assms by simp_all |
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1975 |
|
60758 | 1976 |
setup \<open> |
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66109
diff
changeset
|
1977 |
Code.declare_case_global @{thm Let_case_cert} #> |
69593 | 1978 |
Code.declare_undefined_global \<^const_name>\<open>undefined\<close> |
60758 | 1979 |
\<close> |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1980 |
|
54890
cb892d835803
fundamental treatment of undefined vs. universally partial replaces code_abort
haftmann
parents:
54742
diff
changeset
|
1981 |
declare [[code abort: undefined]] |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1982 |
|
38972 | 1983 |
|
60758 | 1984 |
subsubsection \<open>Generic code generator target languages\<close> |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1985 |
|
69593 | 1986 |
text \<open>type \<^typ>\<open>bool\<close>\<close> |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1987 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
1988 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
1989 |
type_constructor bool \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
1990 |
(SML) "bool" and (OCaml) "bool" and (Haskell) "Bool" and (Scala) "Boolean" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
1991 |
| constant True \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
1992 |
(SML) "true" and (OCaml) "true" and (Haskell) "True" and (Scala) "true" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
1993 |
| constant False \<rightharpoonup> |
58826 | 1994 |
(SML) "false" and (OCaml) "false" and (Haskell) "False" and (Scala) "false" |
34294 | 1995 |
|
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1996 |
code_reserved SML |
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
1997 |
bool true false |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1998 |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
1999 |
code_reserved OCaml |
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2000 |
bool |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
2001 |
|
34294 | 2002 |
code_reserved Scala |
2003 |
Boolean |
|
2004 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2005 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2006 |
constant Not \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2007 |
(SML) "not" and (OCaml) "not" and (Haskell) "not" and (Scala) "'! _" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2008 |
| constant HOL.conj \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2009 |
(SML) infixl 1 "andalso" and (OCaml) infixl 3 "&&" and (Haskell) infixr 3 "&&" and (Scala) infixl 3 "&&" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2010 |
| constant HOL.disj \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2011 |
(SML) infixl 0 "orelse" and (OCaml) infixl 2 "||" and (Haskell) infixl 2 "||" and (Scala) infixl 1 "||" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2012 |
| constant HOL.implies \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2013 |
(SML) "!(if (_)/ then (_)/ else true)" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2014 |
and (OCaml) "!(if (_)/ then (_)/ else true)" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2015 |
and (Haskell) "!(if (_)/ then (_)/ else True)" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2016 |
and (Scala) "!(if ((_))/ (_)/ else true)" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2017 |
| constant If \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2018 |
(SML) "!(if (_)/ then (_)/ else (_))" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2019 |
and (OCaml) "!(if (_)/ then (_)/ else (_))" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2020 |
and (Haskell) "!(if (_)/ then (_)/ else (_))" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2021 |
and (Scala) "!(if ((_))/ (_)/ else (_))" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2022 |
|
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2023 |
code_reserved SML |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2024 |
not |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2025 |
|
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2026 |
code_reserved OCaml |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2027 |
not |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2028 |
|
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2029 |
code_identifier |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2030 |
code_module Pure \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2031 |
(SML) HOL and (OCaml) HOL and (Haskell) HOL and (Scala) HOL |
39026 | 2032 |
|
63575 | 2033 |
text \<open>Using built-in Haskell equality.\<close> |
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2034 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2035 |
type_class equal \<rightharpoonup> (Haskell) "Eq" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2036 |
| constant HOL.equal \<rightharpoonup> (Haskell) infix 4 "==" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2037 |
| constant HOL.eq \<rightharpoonup> (Haskell) infix 4 "==" |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
2038 |
|
63575 | 2039 |
text \<open>\<open>undefined\<close>\<close> |
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2040 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2041 |
constant undefined \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2042 |
(SML) "!(raise/ Fail/ \"undefined\")" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2043 |
and (OCaml) "failwith/ \"undefined\"" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2044 |
and (Haskell) "error/ \"undefined\"" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2045 |
and (Scala) "!sys.error(\"undefined\")" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52432
diff
changeset
|
2046 |
|
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
2047 |
|
60758 | 2048 |
subsubsection \<open>Evaluation and normalization by evaluation\<close> |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
2049 |
|
60758 | 2050 |
method_setup eval = \<open> |
58826 | 2051 |
let |
2052 |
fun eval_tac ctxt = |
|
2053 |
let val conv = Code_Runtime.dynamic_holds_conv ctxt |
|
58839 | 2054 |
in |
2055 |
CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59028
diff
changeset
|
2056 |
resolve_tac ctxt [TrueI] |
58839 | 2057 |
end |
58826 | 2058 |
in |
2059 |
Scan.succeed (SIMPLE_METHOD' o eval_tac) |
|
2060 |
end |
|
60758 | 2061 |
\<close> "solve goal by evaluation" |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
2062 |
|
60758 | 2063 |
method_setup normalization = \<open> |
46190
a42c5f23109f
more conventional eval_tac vs. method_setup "eval";
wenzelm
parents:
46161
diff
changeset
|
2064 |
Scan.succeed (fn ctxt => |
a42c5f23109f
more conventional eval_tac vs. method_setup "eval";
wenzelm
parents:
46161
diff
changeset
|
2065 |
SIMPLE_METHOD' |
a42c5f23109f
more conventional eval_tac vs. method_setup "eval";
wenzelm
parents:
46161
diff
changeset
|
2066 |
(CHANGED_PROP o |
55757 | 2067 |
(CONVERSION (Nbe.dynamic_conv ctxt) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59028
diff
changeset
|
2068 |
THEN_ALL_NEW (TRY o resolve_tac ctxt [TrueI])))) |
60758 | 2069 |
\<close> "solve goal by normalization" |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
2070 |
|
31902 | 2071 |
|
60758 | 2072 |
subsection \<open>Counterexample Search Units\<close> |
33084 | 2073 |
|
60758 | 2074 |
subsubsection \<open>Quickcheck\<close> |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
2075 |
|
33084 | 2076 |
quickcheck_params [size = 5, iterations = 50] |
2077 |
||
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset
|
2078 |
|
60758 | 2079 |
subsubsection \<open>Nitpick setup\<close> |
30309
188f0658af9f
Added a "nitpick_maybe" symbol, which is used by Nitpick. This will go away once Nitpick is part of HOL.
blanchet
parents:
30254
diff
changeset
|
2080 |
|
59028 | 2081 |
named_theorems nitpick_unfold "alternative definitions of constants as needed by Nitpick" |
2082 |
and nitpick_simp "equational specification of constants as needed by Nitpick" |
|
2083 |
and nitpick_psimp "partial equational specification of constants as needed by Nitpick" |
|
2084 |
and nitpick_choice_spec "choice specification of constants as needed by Nitpick" |
|
30980 | 2085 |
|
41792
ff3cb0c418b7
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
blanchet
parents:
41636
diff
changeset
|
2086 |
declare if_bool_eq_conj [nitpick_unfold, no_atp] |
63575 | 2087 |
and if_bool_eq_disj [no_atp] |
41792
ff3cb0c418b7
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
blanchet
parents:
41636
diff
changeset
|
2088 |
|
29863
dadad1831e9d
Added "nitpick_const_simps" and "nitpick_ind_intros" attributes for theorems;
blanchet
parents:
29608
diff
changeset
|
2089 |
|
60758 | 2090 |
subsection \<open>Preprocessing for the predicate compiler\<close> |
33084 | 2091 |
|
59028 | 2092 |
named_theorems code_pred_def "alternative definitions of constants for the Predicate Compiler" |
2093 |
and code_pred_inline "inlining definitions for the Predicate Compiler" |
|
2094 |
and code_pred_simp "simplification rules for the optimisations in the Predicate Compiler" |
|
33084 | 2095 |
|
2096 |
||
60758 | 2097 |
subsection \<open>Legacy tactics and ML bindings\<close> |
21671 | 2098 |
|
60758 | 2099 |
ML \<open> |
58826 | 2100 |
(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *) |
2101 |
local |
|
69593 | 2102 |
fun wrong_prem (Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t)) = wrong_prem t |
58826 | 2103 |
| wrong_prem (Bound _) = true |
2104 |
| wrong_prem _ = false; |
|
2105 |
val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of); |
|
61914 | 2106 |
fun smp i = funpow i (fn m => filter_right ([spec] RL m)) [mp]; |
58826 | 2107 |
in |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59028
diff
changeset
|
2108 |
fun smp_tac ctxt j = EVERY' [dresolve_tac ctxt (smp j), assume_tac ctxt]; |
58826 | 2109 |
end; |
22839 | 2110 |
|
58826 | 2111 |
local |
2112 |
val nnf_ss = |
|
69593 | 2113 |
simpset_of (put_simpset HOL_basic_ss \<^context> addsimps @{thms simp_thms nnf_simps}); |
58826 | 2114 |
in |
2115 |
fun nnf_conv ctxt = Simplifier.rewrite (put_simpset nnf_ss ctxt); |
|
2116 |
end |
|
60758 | 2117 |
\<close> |
21671 | 2118 |
|
38866 | 2119 |
hide_const (open) eq equal |
2120 |
||
14357 | 2121 |
end |