248 where @{term C} is the goal to be proved and the @{term "A\<^sub>i"} are |
248 where @{term C} is the goal to be proved and the @{term "A\<^sub>i"} are |
249 the subgoals. So after setting up the lemma, the goal state is always of the |
249 the subgoals. So after setting up the lemma, the goal state is always of the |
250 form @{text "C \<Longrightarrow> #C"}; when the proof is finished we are left with @{text |
250 form @{text "C \<Longrightarrow> #C"}; when the proof is finished we are left with @{text |
251 "#C"}. Since the goal @{term C} can potentially be an implication, there is a |
251 "#C"}. Since the goal @{term C} can potentially be an implication, there is a |
252 ``protector'' wrapped around it (the wrapper is the outermost constant |
252 ``protector'' wrapped around it (the wrapper is the outermost constant |
253 @{text "Const (\"prop\", bool \<Rightarrow> bool)"}; in the figure we make it visible |
253 @{text "Const (\"Pure.prop\", bool \<Rightarrow> bool)"}; in the figure we make it visible |
254 as a @{text #}). This wrapper prevents that premises of @{text C} are |
254 as a @{text #}). This wrapper prevents that premises of @{text C} are |
255 misinterpreted as open subgoals. While tactics can operate on the subgoals |
255 misinterpreted as open subgoals. While tactics can operate on the subgoals |
256 (the @{text "A\<^sub>i"} above), they are expected to leave the conclusion |
256 (the @{text "A\<^sub>i"} above), they are expected to leave the conclusion |
257 @{term C} intact, with the exception of possibly instantiating schematic |
257 @{term C} intact, with the exception of possibly instantiating schematic |
258 variables. This instantiations of schematic variables can be observed |
258 variables. This instantiations of schematic variables can be observed |
1481 Congruences rules: |
1481 Congruences rules: |
1482 Simproc patterns:"} |
1482 Simproc patterns:"} |
1483 |
1483 |
1484 \footnote{\bf FIXME: Why does it print out ??.unknown} |
1484 \footnote{\bf FIXME: Why does it print out ??.unknown} |
1485 |
1485 |
1486 Adding also the congruence rule @{thm [source] UN_cong} |
1486 Adding also the congruence rule @{thm [source] strong_INF_cong} |
1487 *} |
1487 *} |
1488 |
1488 |
1489 ML %grayML{*val ss2 = ss1 |> Simplifier.add_cong (@{thm UN_cong} RS @{thm eq_reflection}) *} |
1489 ML %grayML{*val ss2 = ss1 |> Simplifier.add_cong (@{thm strong_INF_cong} RS @{thm eq_reflection}) *} |
1490 |
1490 |
1491 text {* |
1491 text {* |
1492 gives |
1492 gives |
1493 |
1493 |
1494 @{ML_response_fake [display,gray] |
1494 @{ML_response_fake [display,gray] |
1495 "print_ss @{context} (Raw_Simplifier.simpset_of ss2)" |
1495 "print_ss @{context} (Raw_Simplifier.simpset_of ss2)" |
1496 "Simplification rules: |
1496 "Simplification rules: |
1497 ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C) |
1497 ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C) |
1498 Congruences rules: |
1498 Congruences rules: |
1499 UNION: \<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk> \<Longrightarrow> \<Union>x\<in>A. C x \<equiv> \<Union>x\<in>B. D x |
1499 Complete_Lattices.Inf_class.INFIMUM: |
|
1500 \<lbrakk>A1 = B1; \<And>x. x \<in> B1 =simp=> C1 x = D1 x\<rbrakk> \<Longrightarrow> INFIMUM A1 C1 \<equiv> INFIMUM B1 D1 |
1500 Simproc patterns:"} |
1501 Simproc patterns:"} |
1501 |
1502 |
1502 Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} |
1503 Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} |
1503 expects this form of the simplification and congruence rules. This is |
1504 expects this form of the simplification and congruence rules. This is |
1504 different, if we use for example the simpset @{ML HOL_basic_ss} (see below), |
1505 different, if we use for example the simpset @{ML HOL_basic_ss} (see below), |
2114 val ten = @{cterm \"10::nat\"} |
2115 val ten = @{cterm \"10::nat\"} |
2115 val ctrm = Thm.apply (Thm.apply add two) ten |
2116 val ctrm = Thm.apply (Thm.apply add two) ten |
2116 in |
2117 in |
2117 Thm.prop_of (Thm.beta_conversion true ctrm) |
2118 Thm.prop_of (Thm.beta_conversion true ctrm) |
2118 end" |
2119 end" |
2119 "Const (\"==\",\<dots>) $ |
2120 "Const (\"Pure.eq\",\<dots>) $ |
2120 (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $ |
2121 (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $ |
2121 (Const (\"Groups.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} |
2122 (Const (\"Groups.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} |
2122 |
2123 |
2123 or in the pretty-printed form |
2124 or in the pretty-printed form |
2124 |
2125 |