src/FOL/FOL.thy
changeset 11988 8340fb172607
parent 11848 6e3017adb8c0
child 12127 219e543496a3
equal deleted inserted replaced
11987:bf31b35949ce 11988:8340fb172607
    56   by (simp only: atomize_imp induct_implies_def)
    56   by (simp only: atomize_imp induct_implies_def)
    57 
    57 
    58 lemma induct_equal_eq: "(x == y) == Trueprop(induct_equal(x, y))"
    58 lemma induct_equal_eq: "(x == y) == Trueprop(induct_equal(x, y))"
    59   by (simp only: atomize_eq induct_equal_def)
    59   by (simp only: atomize_eq induct_equal_def)
    60 
    60 
       
    61 lemma induct_impliesI: "(A ==> B) ==> induct_implies(A, B)"
       
    62   by (simp add: induct_implies_def)
       
    63 
    61 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq
    64 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq
    62 lemmas induct_rulify1 = induct_atomize [symmetric, standard]
    65 lemmas induct_rulify1 = induct_atomize [symmetric, standard]
    63 lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def
    66 lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def
    64 
    67 
    65 hide const induct_forall induct_implies induct_equal
    68 hide const induct_forall induct_implies induct_equal
    70 ML {*
    73 ML {*
    71   structure InductMethod = InductMethodFun
    74   structure InductMethod = InductMethodFun
    72   (struct
    75   (struct
    73     val dest_concls = FOLogic.dest_concls;
    76     val dest_concls = FOLogic.dest_concls;
    74     val cases_default = thm "case_split";
    77     val cases_default = thm "case_split";
       
    78     val local_impI = thm "induct_impliesI";
    75     val conjI = thm "conjI";
    79     val conjI = thm "conjI";
    76     val atomize = thms "induct_atomize";
    80     val atomize = thms "induct_atomize";
    77     val rulify1 = thms "induct_rulify1";
    81     val rulify1 = thms "induct_rulify1";
    78     val rulify2 = thms "induct_rulify2";
    82     val rulify2 = thms "induct_rulify2";
    79   end);
    83   end);