93 "defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all; |
93 "defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all; |
94 |
94 |
95 |
95 |
96 (*** Case splitting ***) |
96 (*** Case splitting ***) |
97 |
97 |
98 structure SplitterData = |
98 structure Splitter = Splitter |
99 struct |
99 ( |
100 structure Simplifier = Simplifier |
100 val thy = @{theory} |
101 val mk_eq = mk_eq |
101 val mk_eq = mk_eq |
102 val meta_eq_to_iff = @{thm meta_eq_to_iff} |
102 val meta_eq_to_iff = @{thm meta_eq_to_iff} |
103 val iffD = @{thm iffD2} |
103 val iffD = @{thm iffD2} |
104 val disjE = @{thm disjE} |
104 val disjE = @{thm disjE} |
105 val conjE = @{thm conjE} |
105 val conjE = @{thm conjE} |
106 val exE = @{thm exE} |
106 val exE = @{thm exE} |
107 val contrapos = @{thm contrapos} |
107 val contrapos = @{thm contrapos} |
108 val contrapos2 = @{thm contrapos2} |
108 val contrapos2 = @{thm contrapos2} |
109 val notnotD = @{thm notnotD} |
109 val notnotD = @{thm notnotD} |
110 end; |
110 ); |
111 |
111 |
112 structure Splitter = SplitterFun(SplitterData); |
112 val split_tac = Splitter.split_tac; |
113 |
|
114 val split_tac = Splitter.split_tac; |
|
115 val split_inside_tac = Splitter.split_inside_tac; |
113 val split_inside_tac = Splitter.split_inside_tac; |
116 val split_asm_tac = Splitter.split_asm_tac; |
114 val split_asm_tac = Splitter.split_asm_tac; |
117 val op addsplits = Splitter.addsplits; |
115 val op addsplits = Splitter.addsplits; |
118 val op delsplits = Splitter.delsplits; |
116 val op delsplits = Splitter.delsplits; |
119 |
117 |
120 |
118 |
121 (*** Standard simpsets ***) |
119 (*** Standard simpsets ***) |
122 |
120 |
123 val triv_rls = [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @{thm notFalseI}]; |
121 val triv_rls = [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @{thm notFalseI}]; |