163 end |
163 end |
164 val x = ((cterm_of thy) o the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o |
164 val x = ((cterm_of thy) o the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o |
165 Logic.dest_implies o prop_of) @{thm exI} |
165 Logic.dest_implies o prop_of) @{thm exI} |
166 fun prove_introrule (index, (ps, introrule)) = |
166 fun prove_introrule (index, (ps, introrule)) = |
167 let |
167 let |
168 val tac = Simplifier.simp_tac (HOL_basic_ss addsimps [th]) 1 |
168 val tac = Simplifier.simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [th]) 1 |
169 THEN EVERY1 (select_disj (length disjuncts) (index + 1)) |
169 THEN EVERY1 (select_disj (length disjuncts) (index + 1)) |
170 THEN (EVERY (map (fn y => |
170 THEN (EVERY (map (fn y => |
171 rtac (Drule.cterm_instantiate [(x, cterm_of thy (Free y))] @{thm exI}) 1) ps)) |
171 rtac (Drule.cterm_instantiate [(x, cterm_of thy (Free y))] @{thm exI}) 1) ps)) |
172 THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN atac 1) |
172 THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN atac 1) |
173 THEN TRY (atac 1) |
173 THEN TRY (atac 1) |
177 in |
177 in |
178 map_index prove_introrule (map mk_introrule disjuncts) |
178 map_index prove_introrule (map mk_introrule disjuncts) |
179 end |
179 end |
180 in maps introrulify' ths' |> Variable.export ctxt' ctxt end |
180 in maps introrulify' ths' |> Variable.export ctxt' ctxt end |
181 |
181 |
182 val rewrite = |
182 fun rewrite ctxt = |
183 Simplifier.simplify (HOL_basic_ss addsimps [@{thm Ball_def}, @{thm Bex_def}]) |
183 Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm Ball_def}, @{thm Bex_def}]) |
184 #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm all_not_ex}]) |
184 #> Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm all_not_ex}]) |
185 #> Conv.fconv_rule nnf_conv |
185 #> Conv.fconv_rule (nnf_conv ctxt) |
186 #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm ex_disj_distrib}]) |
186 #> Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm ex_disj_distrib}]) |
187 |
187 |
188 fun rewrite_intros thy = |
188 fun rewrite_intros thy = |
189 Simplifier.full_simplify (HOL_basic_ss addsimps [@{thm all_not_ex}]) |
189 Simplifier.full_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [@{thm all_not_ex}]) |
190 #> Simplifier.full_simplify |
190 #> Simplifier.full_simplify |
191 (HOL_basic_ss addsimps (tl @{thms bool_simps}) addsimps @{thms nnf_simps}) |
191 (Simplifier.global_context thy HOL_basic_ss |
|
192 addsimps (tl @{thms bool_simps}) addsimps @{thms nnf_simps}) |
192 #> split_conjuncts_in_assms (Proof_Context.init_global thy) |
193 #> split_conjuncts_in_assms (Proof_Context.init_global thy) |
193 |
194 |
194 fun print_specs options thy msg ths = |
195 fun print_specs options thy msg ths = |
195 if show_intermediate_results options then |
196 if show_intermediate_results options then |
196 (tracing (msg); tracing (commas (map (Display.string_of_thm_global thy) ths))) |
197 (tracing (msg); tracing (commas (map (Display.string_of_thm_global thy) ths))) |
203 | NONE =>*) |
204 | NONE =>*) |
204 let |
205 let |
205 val ctxt = Proof_Context.init_global thy |
206 val ctxt = Proof_Context.init_global thy |
206 val intros = |
207 val intros = |
207 if forall is_pred_equation specs then |
208 if forall is_pred_equation specs then |
208 map (split_conjuncts_in_assms ctxt) (introrulify thy (map rewrite specs)) |
209 map (split_conjuncts_in_assms ctxt) (introrulify thy (map (rewrite ctxt) specs)) |
209 else if forall (is_intro constname) specs then |
210 else if forall (is_intro constname) specs then |
210 map (rewrite_intros thy) specs |
211 map (rewrite_intros thy) specs |
211 else |
212 else |
212 error ("unexpected specification for constant " ^ quote constname ^ ":\n" |
213 error ("unexpected specification for constant " ^ quote constname ^ ":\n" |
213 ^ commas (map (quote o Display.string_of_thm_global thy) specs)) |
214 ^ commas (map (quote o Display.string_of_thm_global thy) specs)) |