48 val check_HOHH_tac2 = PRIMITIVE (fn thm => |
48 val check_HOHH_tac2 = PRIMITIVE (fn thm => |
49 if forall isG (prems_of thm) then thm else raise not_HOHH); |
49 if forall isG (prems_of thm) then thm else raise not_HOHH); |
50 fun check_HOHH thm = (if isD (concl_of thm) andalso forall isG (prems_of thm) |
50 fun check_HOHH thm = (if isD (concl_of thm) andalso forall isG (prems_of thm) |
51 then thm else raise not_HOHH); |
51 then thm else raise not_HOHH); |
52 |
52 |
53 fun atomizeD thm = let |
53 fun atomizeD ctxt thm = let |
54 fun at thm = case concl_of thm of |
54 fun at thm = case concl_of thm of |
55 _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (Drule.read_instantiate [("x", |
55 _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS |
56 "?"^(if s="P" then "PP" else s))] spec)) |
56 (RuleInsts.read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec)) |
57 | _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) |
57 | _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) |
58 | _$(Const("op -->",_)$_$_) => at(thm RS mp) |
58 | _$(Const("op -->",_)$_$_) => at(thm RS mp) |
59 | _ => [thm] |
59 | _ => [thm] |
60 in map zero_var_indexes (at thm) end; |
60 in map zero_var_indexes (at thm) end; |
61 |
61 |
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) st end; |
108 |
108 |
109 fun ptac prog = let |
109 fun ptac ctxt prog = let |
110 val proga = List.concat (map atomizeD prog) (* atomize the prog *) |
110 val proga = List.concat (map (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" *) |
113 rtac conjI, (* "[| P; Q |] ==> P & Q" *) |
113 rtac conjI, (* "[| P; Q |] ==> P & Q" *) |
114 rtac allI, (* "(!!x. P x) ==> ! x. P x" *) |
114 rtac allI, (* "(!!x. P x) ==> ! x. P x" *) |
115 rtac exI, (* "P x ==> ? x. P x" *) |
115 rtac exI, (* "P x ==> ? x. P x" *) |
120 ORELSE' resolve_tac [disjI1,disjI2] (* "P ==> P | Q","Q ==> P | Q"*) |
120 ORELSE' resolve_tac [disjI1,disjI2] (* "P ==> P | Q","Q ==> P | Q"*) |
121 ORELSE' ((resolve_tac proga APPEND' hyp_resolve_tac) |
121 ORELSE' ((resolve_tac proga APPEND' hyp_resolve_tac) |
122 THEN' (fn _ => check_HOHH_tac2)) |
122 THEN' (fn _ => check_HOHH_tac2)) |
123 end; |
123 end; |
124 |
124 |
125 fun prolog_tac prog = check_HOHH_tac1 THEN |
125 fun prolog_tac ctxt prog = |
126 DEPTH_SOLVE (ptac (map check_HOHH prog) 1); |
126 check_HOHH_tac1 THEN |
|
127 DEPTH_SOLVE (ptac ctxt (map check_HOHH prog) 1); |
127 |
128 |
128 val prog_HOHH = []; |
129 val prog_HOHH = []; |
129 |
130 |
130 end; |
131 end; |