equal
deleted
inserted
replaced
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); 