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

author | wenzelm |

Tue, 04 Dec 2001 02:01:13 +0100 | |

changeset 12354 | 5f5ee25513c5 |

parent 12353 | e4be26df707a |

child 12355 | c8d3c3d09080 |

setup "rules" method;

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

--- a/src/HOL/HOL.thy Tue Dec 04 02:00:45 2001 +0100 +++ b/src/HOL/HOL.thy Tue Dec 04 02:01:13 2001 +0100 @@ -263,6 +263,39 @@ setup Blast.setup +subsubsection {* Intuitionistic Reasoning *} + +lemma impE': + (assumes 1: "P --> Q" and 2: "Q ==> R" and 3: "P --> Q ==> P") R +proof - + from 3 and 1 have P . + with 1 have Q .. + with 2 show R . +qed + +lemma allE': + (assumes 1: "ALL x. P x" and 2: "P x ==> ALL x. P x ==> Q") Q +proof - + from 1 have "P x" .. + from this and 1 show Q by (rule 2) +qed + +lemma notE': (assumes 1: "~ P" and 2: "~ P ==> P") R +proof - + from 2 and 1 have P . + with 1 show R by (rule notE) +qed + +lemmas [CPure.elim!] = disjE iffE FalseE conjE exE + and [CPure.intro!] = iffI conjI impI TrueI notI allI refl + and [CPure.elim 2] = allE notE' impE' + and [CPure.intro] = exI disjI2 disjI1 + +ML_setup {* + Context.>> (ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)); +*} + + subsubsection {* Simplifier setup *} lemma meta_eq_to_obj_eq: "x == y ==> x = y" @@ -301,7 +334,7 @@ by blast+ lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P --> Q) = (P' --> Q'))" - by blast + by rules lemma ex_simps: "!!P Q. (EX x. P x & Q) = ((EX x. P x) & Q)" @@ -387,11 +420,11 @@ lemma conj_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P & Q) = (P' & Q'))" - by blast + by rules lemma rev_conj_cong: "(Q = Q') ==> (Q' ==> (P = P')) ==> ((P & Q) = (P' & Q'))" - by blast + by rules text {* The @{text "|"} congruence rule: not included by default! *} @@ -400,7 +433,7 @@ by blast lemma eq_sym_conv: "(x = y) = (y = x)" - by blast + by rules text {* \medskip if-then-else rules *} @@ -486,14 +519,14 @@ lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) = induct_conj (induct_forall A) (induct_forall B)" - by (unfold induct_forall_def induct_conj_def) blast + by (unfold induct_forall_def induct_conj_def) rules lemma induct_implies_conj: "induct_implies C (induct_conj A B) = induct_conj (induct_implies C A) (induct_implies C B)" - by (unfold induct_implies_def induct_conj_def) blast + by (unfold induct_implies_def induct_conj_def) rules lemma induct_conj_curry: "(induct_conj A B ==> C) == (A ==> B ==> C)" - by (simp only: atomize_imp atomize_eq induct_conj_def) (rule equal_intr_rule, blast+) + by (simp only: atomize_imp atomize_eq induct_conj_def) (rules intro: equal_intr_rule) lemma induct_impliesI: "(A ==> B) ==> induct_implies A B" by (simp add: induct_implies_def) @@ -561,10 +594,10 @@ "mono f == ALL A B. A <= B --> f A <= f B" lemma monoI [intro?]: "(!!A B. A <= B ==> f A <= f B) ==> mono f" - by (unfold mono_def) blast + by (unfold mono_def) rules lemma monoD [dest?]: "mono f ==> A <= B ==> f A <= f B" - by (unfold mono_def) blast + by (unfold mono_def) rules constdefs min :: "['a::ord, 'a] => 'a"