88 induct_implies where "induct_implies(A, B) == A \<longrightarrow> B" |
88 induct_implies where "induct_implies(A, B) == A \<longrightarrow> B" |
89 induct_equal where "induct_equal(x, y) == x = y" |
89 induct_equal where "induct_equal(x, y) == x = y" |
90 induct_conj where "induct_conj(A, B) == A \<and> B" |
90 induct_conj where "induct_conj(A, B) == A \<and> B" |
91 |
91 |
92 lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\<lambda>x. P(x)))" |
92 lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\<lambda>x. P(x)))" |
93 by (unfold atomize_all induct_forall_def) |
93 unfolding atomize_all induct_forall_def . |
94 |
94 |
95 lemma induct_implies_eq: "(A ==> B) == Trueprop(induct_implies(A, B))" |
95 lemma induct_implies_eq: "(A ==> B) == Trueprop(induct_implies(A, B))" |
96 by (unfold atomize_imp induct_implies_def) |
96 unfolding atomize_imp induct_implies_def . |
97 |
97 |
98 lemma induct_equal_eq: "(x == y) == Trueprop(induct_equal(x, y))" |
98 lemma induct_equal_eq: "(x == y) == Trueprop(induct_equal(x, y))" |
99 by (unfold atomize_eq induct_equal_def) |
99 unfolding atomize_eq induct_equal_def . |
100 |
100 |
101 lemma induct_conj_eq: |
101 lemma induct_conj_eq: |
102 includes meta_conjunction_syntax |
102 includes meta_conjunction_syntax |
103 shows "(A && B) == Trueprop(induct_conj(A, B))" |
103 shows "(A && B) == Trueprop(induct_conj(A, B))" |
104 by (unfold atomize_conj induct_conj_def) |
104 unfolding atomize_conj induct_conj_def . |
105 |
105 |
106 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq |
106 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq |
107 lemmas induct_rulify [symmetric, standard] = induct_atomize |
107 lemmas induct_rulify [symmetric, standard] = induct_atomize |
108 lemmas induct_rulify_fallback = |
108 lemmas induct_rulify_fallback = |
109 induct_forall_def induct_implies_def induct_equal_def induct_conj_def |
109 induct_forall_def induct_implies_def induct_equal_def induct_conj_def |