src/FOL/FOL.thy
changeset 18456 8cc35e95450a
parent 16417 9bc16273c2d4
child 18511 beed2bc052a3
equal deleted inserted replaced
18455:b293c1087f1d 18456:8cc35e95450a
     3     Author:     Lawrence C Paulson and Markus Wenzel
     3     Author:     Lawrence C Paulson and Markus Wenzel
     4 *)
     4 *)
     5 
     5 
     6 header {* Classical first-order logic *}
     6 header {* Classical first-order logic *}
     7 
     7 
     8 theory FOL 
     8 theory FOL
     9 imports IFOL
     9 imports IFOL
    10 uses ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
    10 uses ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
    11       ("eqrule_FOL_data.ML")
    11       ("eqrule_FOL_data.ML")
    12       ("~~/src/Provers/eqsubst.ML")
    12       ("~~/src/Provers/eqsubst.ML")
    13 begin  
    13 begin
    14 
    14 
    15 
    15 
    16 subsection {* The classical axiom *}
    16 subsection {* The classical axiom *}
    17 
    17 
    18 axioms
    18 axioms
    91 subsection {* Proof by cases and induction *}
    91 subsection {* Proof by cases and induction *}
    92 
    92 
    93 text {* Proper handling of non-atomic rule statements. *}
    93 text {* Proper handling of non-atomic rule statements. *}
    94 
    94 
    95 constdefs
    95 constdefs
    96   induct_forall :: "('a => o) => o"
    96   induct_forall where "induct_forall(P) == \<forall>x. P(x)"
    97   "induct_forall(P) == \<forall>x. P(x)"
    97   induct_implies where "induct_implies(A, B) == A \<longrightarrow> B"
    98   induct_implies :: "o => o => o"
    98   induct_equal where "induct_equal(x, y) == x = y"
    99   "induct_implies(A, B) == A --> B"
    99   induct_conj where "induct_conj(A, B) == A \<and> B"
   100   induct_equal :: "'a => 'a => o"
       
   101   "induct_equal(x, y) == x = y"
       
   102 
   100 
   103 lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\<lambda>x. P(x)))"
   101 lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\<lambda>x. P(x)))"
   104   by (simp only: atomize_all induct_forall_def)
   102   by (unfold atomize_all induct_forall_def)
   105 
   103 
   106 lemma induct_implies_eq: "(A ==> B) == Trueprop(induct_implies(A, B))"
   104 lemma induct_implies_eq: "(A ==> B) == Trueprop(induct_implies(A, B))"
   107   by (simp only: atomize_imp induct_implies_def)
   105   by (unfold atomize_imp induct_implies_def)
   108 
   106 
   109 lemma induct_equal_eq: "(x == y) == Trueprop(induct_equal(x, y))"
   107 lemma induct_equal_eq: "(x == y) == Trueprop(induct_equal(x, y))"
   110   by (simp only: atomize_eq induct_equal_def)
   108   by (unfold atomize_eq induct_equal_def)
   111 
   109 
   112 lemma induct_impliesI: "(A ==> B) ==> induct_implies(A, B)"
   110 lemma induct_conj_eq:
   113   by (simp add: induct_implies_def)
   111   includes meta_conjunction_syntax
       
   112   shows "(A && B) == Trueprop(induct_conj(A, B))"
       
   113   by (unfold atomize_conj induct_conj_def)
   114 
   114 
   115 lemmas induct_atomize = atomize_conj induct_forall_eq induct_implies_eq induct_equal_eq
   115 lemmas induct_atomize_old = induct_forall_eq induct_implies_eq induct_equal_eq atomize_conj
   116 lemmas induct_rulify1 [symmetric, standard] = induct_forall_eq induct_implies_eq induct_equal_eq
   116 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
   117 lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def
   117 lemmas induct_rulify [symmetric, standard] = induct_atomize
       
   118 lemmas induct_rulify_fallback =
       
   119   induct_forall_def induct_implies_def induct_equal_def induct_conj_def
   118 
   120 
   119 lemma all_conj_eq: "(ALL x. P(x)) & (ALL y. Q(y)) == (ALL x y. P(x) & Q(y))"
   121 hide const induct_forall induct_implies induct_equal induct_conj
   120   by simp
       
   121 
       
   122 hide const induct_forall induct_implies induct_equal
       
   123 
   122 
   124 
   123 
   125 text {* Method setup. *}
   124 text {* Method setup. *}
   126 
   125 
   127 ML {*
   126 ML {*
   128   structure InductMethod = InductMethodFun
   127   structure InductMethod = InductMethodFun
   129   (struct
   128   (struct
   130     val dest_concls = FOLogic.dest_concls;
       
   131     val cases_default = thm "case_split";
   129     val cases_default = thm "case_split";
   132     val local_impI = thm "induct_impliesI";
   130     val atomize_old = thms "induct_atomize_old";
   133     val conjI = thm "conjI";
       
   134     val atomize = thms "induct_atomize";
   131     val atomize = thms "induct_atomize";
   135     val rulify1 = thms "induct_rulify1";
   132     val rulify = thms "induct_rulify";
   136     val rulify2 = thms "induct_rulify2";
   133     val rulify_fallback = thms "induct_rulify_fallback";
   137     val localize = [Thm.symmetric (thm "induct_implies_def"),
       
   138       Thm.symmetric (thm "atomize_all"), thm "all_conj_eq"];
       
   139   end);
   134   end);
   140 *}
   135 *}
   141 
   136 
   142 setup InductMethod.setup
   137 setup InductMethod.setup
   143 
   138