summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 03 Jul 2007 22:27:05 +0200 | |

changeset 23553 | af8ae54238f5 |

parent 23552 | 6403d06abe25 |

child 23554 | 151d60fbfffe |

use hologic.ML in basic HOL context;
tuned proofs;

src/HOL/HOL.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/HOL.thy Tue Jul 03 21:56:25 2007 +0200 +++ b/src/HOL/HOL.thy Tue Jul 03 22:27:05 2007 +0200 @@ -9,7 +9,7 @@ imports CPure uses "~~/src/Tools/integer.ML" - "hologic.ML" + ("hologic.ML") "~~/src/Tools/IsaPlanner/zipper.ML" "~~/src/Tools/IsaPlanner/isand.ML" "~~/src/Tools/IsaPlanner/rw_tools.ML" @@ -434,7 +434,7 @@ lemma impE: assumes "P-->Q" "P" "Q ==> R" shows "R" -by (iprover intro: prems mp) +by (iprover intro: assms mp) (* Reduces Q to P-->Q, allowing substitution in P. *) lemma rev_mp: "[| P; P --> Q |] ==> Q" @@ -511,8 +511,8 @@ done lemma context_conjI: - assumes prems: "P" "P ==> Q" shows "P & Q" -by (iprover intro: conjI prems) + assumes "P" "P ==> Q" shows "P & Q" +by (iprover intro: conjI assms) subsubsection {*Disjunction*} @@ -577,9 +577,9 @@ subsubsection {*Unique existence*} lemma ex1I: - assumes prems: "P a" "!!x. P(x) ==> x=a" + assumes "P a" "!!x. P(x) ==> x=a" shows "EX! x. P(x)" -by (unfold Ex1_def, iprover intro: prems exI conjI allI impI) +by (unfold Ex1_def, iprover intro: assms exI conjI allI impI) text{*Sometimes easier to use: the premises have no shared variables. Safe!*} lemma ex_ex1I: @@ -621,7 +621,7 @@ lemma theI: assumes "P a" and "!!x. P x ==> x=a" shows "P (THE x. P x)" -by (iprover intro: prems the_equality [THEN ssubst]) +by (iprover intro: assms the_equality [THEN ssubst]) lemma theI': "EX! x. P x ==> P (THE x. P x)" apply (erule ex1E) @@ -635,7 +635,7 @@ lemma theI2: assumes "P a" "!!x. P x ==> x=a" "!!x. P x ==> Q x" shows "Q (THE x. P x)" -by (iprover intro: prems theI) +by (iprover intro: assms theI) lemma the1_equality [elim?]: "[| EX!x. P x; P a |] ==> (THE x. P x) = a" apply (rule the_equality) @@ -662,7 +662,7 @@ lemma disjCI: assumes "~Q ==> P" shows "P|Q" apply (rule classical) -apply (iprover intro: prems disjI1 disjI2 notI elim: notE) +apply (iprover intro: assms disjI1 disjI2 notI elim: notE) done lemma excluded_middle: "~P | P" @@ -715,7 +715,7 @@ assumes "ALL x. ~P(x) ==> P(a)" shows "EX x. P(x)" apply (rule ccontr) -apply (iprover intro: prems exI allI notI notE [of "\<exists>x. P x"]) +apply (iprover intro: assms exI allI notI notE [of "\<exists>x. P x"]) done @@ -762,6 +762,8 @@ and [sym] = sym not_sym and [Pure.elim?] = iffD1 iffD2 impE +use "hologic.ML" + subsubsection {* Atomizing meta-level connectives *} @@ -771,7 +773,7 @@ then show "ALL x. P x" .. next assume "ALL x. P x" - thus "!!x. P x" by (rule allE) + then show "!!x. P x" by (rule allE) qed lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)" @@ -780,7 +782,7 @@ show "A --> B" by (rule impI) (rule r) next assume "A --> B" and A - thus B by (rule mp) + then show B by (rule mp) qed lemma atomize_not: "(A ==> False) == Trueprop (~A)" @@ -789,16 +791,16 @@ show "~A" by (rule notI) (rule r) next assume "~A" and A - thus False by (rule notE) + then show False by (rule notE) qed lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" proof assume "x == y" - show "x = y" by (unfold prems) (rule refl) + show "x = y" by (unfold `x == y`) (rule refl) next assume "x = y" - thus "x == y" by (rule eq_reflection) + then show "x == y" by (rule eq_reflection) qed lemma atomize_conj [atomize]: @@ -1173,13 +1175,13 @@ and P': "PROP P'" from PP' [symmetric] and P' have "PROP P" by (rule equal_elim_rule1) - hence "PROP Q" by (rule PQ) + then have "PROP Q" by (rule PQ) with P'QQ' [OF P'] show "PROP Q'" by (rule equal_elim_rule1) next assume P'Q': "PROP P' \<Longrightarrow> PROP Q'" and P: "PROP P" from PP' and P have P': "PROP P'" by (rule equal_elim_rule1) - hence "PROP Q'" by (rule P'Q') + then have "PROP Q'" by (rule P'Q') with P'QQ' [OF P', symmetric] show "PROP Q" by (rule equal_elim_rule1) qed @@ -1187,17 +1189,17 @@ lemma uncurry: assumes "P \<longrightarrow> Q \<longrightarrow> R" shows "P \<and> Q \<longrightarrow> R" - using prems by blast + using assms by blast lemma iff_allI: assumes "\<And>x. P x = Q x" shows "(\<forall>x. P x) = (\<forall>x. Q x)" - using prems by blast + using assms by blast lemma iff_exI: assumes "\<And>x. P x = Q x" shows "(\<exists>x. P x) = (\<exists>x. Q x)" - using prems by blast + using assms by blast lemma all_comm: "(\<forall>x y. P x y) = (\<forall>y x. P x y)" @@ -1288,26 +1290,26 @@ and "c \<Longrightarrow> x = u" and "\<not> c \<Longrightarrow> y = v" shows "(if b then x else y) = (if c then u else v)" - unfolding if_def using prems by simp + unfolding if_def using assms by simp text {* Prevents simplification of x and y: faster and allows the execution of functional programs. *} lemma if_weak_cong [cong]: assumes "b = c" shows "(if b then x else y) = (if c then x else y)" - using prems by (rule arg_cong) + using assms by (rule arg_cong) text {* Prevents simplification of t: much faster *} lemma let_weak_cong: assumes "a = b" shows "(let x = a in t x) = (let x = b in t x)" - using prems by (rule arg_cong) + using assms by (rule arg_cong) text {* To tidy up the result of a simproc. Only the RHS will be simplified. *} lemma eq_cong2: assumes "u = u'" shows "(t \<equiv> u) \<equiv> (t \<equiv> u')" - using prems by simp + using assms by simp lemma if_distrib: "f (if c then x else y) = (if c then f x else f y)" @@ -1318,7 +1320,7 @@ lemma restrict_to_left: assumes "x = y" shows "(x = z) = (y = z)" - using prems by simp + using assms by simp subsubsection {* Generic cases and induction *}