69 |
69 |
70 |
70 |
71 (*val hyp_resolve_tac = Subgoal.FOCUS_PREMS (fn {prems, ...} => |
71 (*val hyp_resolve_tac = Subgoal.FOCUS_PREMS (fn {prems, ...} => |
72 resolve_tac (maps atomizeD prems) 1); |
72 resolve_tac (maps atomizeD prems) 1); |
73 -- is nice, but cannot instantiate unknowns in the assumptions *) |
73 -- is nice, but cannot instantiate unknowns in the assumptions *) |
74 fun hyp_resolve_tac i st = let |
74 val hyp_resolve_tac = SUBGOAL (fn (subgoal, i) => |
|
75 let |
75 fun ap (Const(@{const_name All},_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a ,t)) |
76 fun ap (Const(@{const_name All},_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a ,t)) |
76 | ap (Const(@{const_name HOL.implies},_)$_$t) =(case ap t of (k,_,t) => (k,true ,t)) |
77 | ap (Const(@{const_name HOL.implies},_)$_$t) =(case ap t of (k,_,t) => (k,true ,t)) |
77 | ap t = (0,false,t); |
78 | ap t = (0,false,t); |
78 (* |
79 (* |
79 fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t |
80 fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t |
81 (case rep_goal t of (l,t) => (s::l,t)) |
82 (case rep_goal t of (l,t) => (s::l,t)) |
82 | rep_goal t = ([] ,t); |
83 | rep_goal t = ([] ,t); |
83 val (prems, Const(@{const_name Trueprop}, _)$concl) = rep_goal |
84 val (prems, Const(@{const_name Trueprop}, _)$concl) = rep_goal |
84 (#3(dest_state (st,i))); |
85 (#3(dest_state (st,i))); |
85 *) |
86 *) |
86 val subgoal = #3(Thm.dest_state (st,i)); |
|
87 val prems = Logic.strip_assums_hyp subgoal; |
87 val prems = Logic.strip_assums_hyp subgoal; |
88 val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal); |
88 val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal); |
89 fun drot_tac k i = DETERM (rotate_tac k i); |
89 fun drot_tac k i = DETERM (rotate_tac k i); |
90 fun spec_tac 0 i = all_tac |
90 fun spec_tac 0 i = all_tac |
91 | spec_tac k i = EVERY' [dtac spec, drot_tac ~1, spec_tac (k-1)] i; |
91 | spec_tac k i = EVERY' [dtac spec, drot_tac ~1, spec_tac (k-1)] i; |
102 then dup_spec_tac k i THEN |
102 then dup_spec_tac k i THEN |
103 (if arrow then etac mp i THEN drot_tac (~n) i else atac i) |
103 (if arrow then etac mp i THEN drot_tac (~n) i else atac i) |
104 else no_tac); |
104 else no_tac); |
105 val ptacs = mapn (fn n => fn t => |
105 val ptacs = mapn (fn n => fn t => |
106 pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems; |
106 pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems; |
107 in Library.foldl (op APPEND) (no_tac, ptacs) st end; |
107 in Library.foldl (op APPEND) (no_tac, ptacs) end); |
108 |
108 |
109 fun ptac ctxt prog = let |
109 fun ptac ctxt prog = let |
110 val proga = maps (atomizeD ctxt) prog (* atomize the prog *) |
110 val proga = maps (atomizeD ctxt) prog (* atomize the prog *) |
111 in (REPEAT_DETERM1 o FIRST' [ |
111 in (REPEAT_DETERM1 o FIRST' [ |
112 rtac TrueI, (* "True" *) |
112 rtac TrueI, (* "True" *) |