summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/FOL/FOL.thy

author | wenzelm |

Mon, 19 Nov 2001 20:46:05 +0100 | |

changeset 12240 | 0760eda193c4 |

parent 12164 | 0b219d9e3384 |

child 12303 | 67ca723a02dd |

permissions | -rw-r--r-- |

induct method: localize rews for rule;

(* Title: FOL/FOL.thy ID: $Id$ Author: Lawrence C Paulson and Markus Wenzel *) header {* Classical first-order logic *} theory FOL = IFOL files ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("FOL_lemmas2.ML"): subsection {* The classical axiom *} axioms classical: "(~P ==> P) ==> P" subsection {* Lemmas and proof tools *} use "FOL_lemmas1.ML" theorems case_split = case_split_thm [case_names True False, cases type: o] use "cladata.ML" setup Cla.setup setup clasetup use "blastdata.ML" setup Blast.setup use "FOL_lemmas2.ML" use "simpdata.ML" setup simpsetup setup "Simplifier.method_setup Splitter.split_modifiers" setup Splitter.setup setup Clasimp.setup subsection {* Proof by cases and induction *} text {* Proper handling of non-atomic rule statements. *} constdefs induct_forall :: "('a => o) => o" "induct_forall(P) == \<forall>x. P(x)" induct_implies :: "o => o => o" "induct_implies(A, B) == A --> B" induct_equal :: "'a => 'a => o" "induct_equal(x, y) == x = y" lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\<lambda>x. P(x)))" by (simp only: atomize_all induct_forall_def) lemma induct_implies_eq: "(A ==> B) == Trueprop(induct_implies(A, B))" by (simp only: atomize_imp induct_implies_def) lemma induct_equal_eq: "(x == y) == Trueprop(induct_equal(x, y))" by (simp only: atomize_eq induct_equal_def) lemma induct_impliesI: "(A ==> B) ==> induct_implies(A, B)" by (simp add: induct_implies_def) lemmas induct_atomize = atomize_conj induct_forall_eq induct_implies_eq induct_equal_eq lemmas induct_rulify1 [symmetric, standard] = induct_forall_eq induct_implies_eq induct_equal_eq lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def lemma all_conj_eq: "(ALL x. P(x)) & (ALL y. Q(y)) == (ALL x y. P(x) & Q(y))" by simp hide const induct_forall induct_implies induct_equal text {* Method setup. *} ML {* structure InductMethod = InductMethodFun (struct val dest_concls = FOLogic.dest_concls; val cases_default = thm "case_split"; val local_impI = thm "induct_impliesI"; val conjI = thm "conjI"; val atomize = thms "induct_atomize"; val rulify1 = thms "induct_rulify1"; val rulify2 = thms "induct_rulify2"; val localize = [Thm.symmetric (thm "induct_implies_def"), Thm.symmetric (thm "atomize_all"), thm "all_conj_eq"]; end); *} setup InductMethod.setup end