equal
deleted
inserted
replaced
81 | Free _ => |
81 | Free _ => |
82 Subgoal.FOCUS_PREMS (fn {context = ctxt, params = params, prems, asms, concl, schematics} => |
82 Subgoal.FOCUS_PREMS (fn {context = ctxt, params = params, prems, asms, concl, schematics} => |
83 let |
83 let |
84 val prems' = maps dest_conjunct_prem (take nargs prems) |
84 val prems' = maps dest_conjunct_prem (take nargs prems) |
85 in |
85 in |
86 MetaSimplifier.rewrite_goal_tac |
86 Simplifier.rewrite_goal_tac |
87 (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1 |
87 (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1 |
88 end) ctxt 1 |
88 end) ctxt 1 |
89 | Abs _ => raise Fail "prove_param: No valid parameter term" |
89 | Abs _ => raise Fail "prove_param: No valid parameter term" |
90 in |
90 in |
91 REPEAT_DETERM (rtac @{thm ext} 1) |
91 REPEAT_DETERM (rtac @{thm ext} 1) |
182 THEN asm_simp_tac HOL_basic_ss' 1 |
182 THEN asm_simp_tac HOL_basic_ss' 1 |
183 THEN TRY ( |
183 THEN TRY ( |
184 let |
184 let |
185 val prems' = maps dest_conjunct_prem (take nargs prems) |
185 val prems' = maps dest_conjunct_prem (take nargs prems) |
186 in |
186 in |
187 MetaSimplifier.rewrite_goal_tac |
187 Simplifier.rewrite_goal_tac |
188 (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1 |
188 (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1 |
189 end |
189 end |
190 THEN REPEAT_DETERM (rtac @{thm refl} 1)) |
190 THEN REPEAT_DETERM (rtac @{thm refl} 1)) |
191 THEN print_tac options "after if simp; in SUBPROOF") ctxt 1)))) |
191 THEN print_tac options "after if simp; in SUBPROOF") ctxt 1)))) |
192 THEN print_tac options "after if simplification" |
192 THEN print_tac options "after if simplification" |
223 THEN Subgoal.FOCUS_PREMS |
223 THEN Subgoal.FOCUS_PREMS |
224 (fn {context = ctxt, params = params, prems, asms, concl, schematics} => |
224 (fn {context = ctxt, params = params, prems, asms, concl, schematics} => |
225 let |
225 let |
226 val prems' = maps dest_conjunct_prem (take nargs prems) |
226 val prems' = maps dest_conjunct_prem (take nargs prems) |
227 in |
227 in |
228 MetaSimplifier.rewrite_goal_tac |
228 Simplifier.rewrite_goal_tac |
229 (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1 |
229 (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1 |
230 end) ctxt 1 |
230 end) ctxt 1 |
231 THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1) |
231 THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1) |
232 | prove_prems out_ts ((p, deriv) :: ps) = |
232 | prove_prems out_ts ((p, deriv) :: ps) = |
233 let |
233 let |