36 | Const("all",_)$Abs(_,_,t) => isG t |
34 | Const("all",_)$Abs(_,_,t) => isG t |
37 | Const("Ex" ,_)$Abs(_,_,t) => isG t |
35 | Const("Ex" ,_)$Abs(_,_,t) => isG t |
38 | Const("True",_) => true |
36 | Const("True",_) => true |
39 | Const("not",_)$_ => false |
37 | Const("not",_)$_ => false |
40 | Const("False",_) => false |
38 | Const("False",_) => false |
41 | _ (* atom *) => true; |
39 | _ (* atom *) => true; |
42 |
40 |
43 val check_HOHH_tac1 = PRIMITIVE (fn thm => |
41 val check_HOHH_tac1 = PRIMITIVE (fn thm => |
44 if isG (concl_of thm) then thm else raise not_HOHH); |
42 if isG (concl_of thm) then thm else raise not_HOHH); |
45 val check_HOHH_tac2 = PRIMITIVE (fn thm => |
43 val check_HOHH_tac2 = PRIMITIVE (fn thm => |
46 if forall isG (prems_of thm) then thm else raise not_HOHH); |
44 if forall isG (prems_of thm) then thm else raise not_HOHH); |
47 fun check_HOHH thm = (if isD (concl_of thm) andalso forall isG (prems_of thm) |
45 fun check_HOHH thm = (if isD (concl_of thm) andalso forall isG (prems_of thm) |
48 then thm else raise not_HOHH); |
46 then thm else raise not_HOHH); |
49 |
47 |
50 fun atomizeD thm = let |
48 fun atomizeD thm = let |
51 fun at thm = case concl_of thm of |
49 fun at thm = case concl_of thm of |
52 _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (read_instantiate [("x", |
50 _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (read_instantiate [("x", |
53 "?"^(if s="P" then "PP" else s))] spec)) |
51 "?"^(if s="P" then "PP" else s))] spec)) |
54 | _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) |
52 | _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) |
55 | _$(Const("op -->",_)$_$_) => at(thm RS mp) |
53 | _$(Const("op -->",_)$_$_) => at(thm RS mp) |
56 | _ => [thm] |
54 | _ => [thm] |
57 in map zero_var_indexes (at thm) end; |
55 in map zero_var_indexes (at thm) end; |
58 |
56 |
59 val atomize_ss = empty_ss setmksimps (mksimps mksimps_pairs) addsimps [ |
57 val atomize_ss = empty_ss setmksimps (mksimps mksimps_pairs) addsimps [ |
60 all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *) |
58 all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *) |
61 imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *) |
59 imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *) |
62 imp_conjR, (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *) |
60 imp_conjR, (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *) |
63 imp_all]; (* "((!x. D) :- G) = (!x. D :- G)" *) |
61 imp_all]; (* "((!x. D) :- G) = (!x. D :- G)" *) |
64 |
62 |
65 (*val hyp_resolve_tac = METAHYPS (fn prems => |
63 (*val hyp_resolve_tac = METAHYPS (fn prems => |
66 resolve_tac (List.concat (map atomizeD prems)) 1); |
64 resolve_tac (List.concat (map atomizeD prems)) 1); |
67 -- is nice, but cannot instantiate unknowns in the assumptions *) |
65 -- is nice, but cannot instantiate unknowns in the assumptions *) |
68 fun hyp_resolve_tac i st = let |
66 fun hyp_resolve_tac i st = let |
69 fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a ,t)) |
67 fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a ,t)) |
70 | ap (Const("op -->",_)$_$t) =(case ap t of (k,_,t) => (k,true ,t)) |
68 | ap (Const("op -->",_)$_$t) =(case ap t of (k,_,t) => (k,true ,t)) |
71 | ap t = (0,false,t); |
69 | ap t = (0,false,t); |
72 (* |
70 (* |
73 fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t |
71 fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t |
74 | rep_goal (Const ("==>",_)$s$t) = |
72 | rep_goal (Const ("==>",_)$s$t) = |
75 (case rep_goal t of (l,t) => (s::l,t)) |
73 (case rep_goal t of (l,t) => (s::l,t)) |
76 | rep_goal t = ([] ,t); |
74 | rep_goal t = ([] ,t); |
77 val (prems, Const("Trueprop", _)$concl) = rep_goal |
75 val (prems, Const("Trueprop", _)$concl) = rep_goal |
78 (#3(dest_state (st,i))); |
76 (#3(dest_state (st,i))); |
79 *) |
77 *) |
80 val subgoal = #3(dest_state (st,i)); |
78 val subgoal = #3(dest_state (st,i)); |
81 val prems = Logic.strip_assums_hyp subgoal; |
79 val prems = Logic.strip_assums_hyp subgoal; |
82 val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal); |
80 val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal); |
83 fun drot_tac k i = DETERM (rotate_tac k i); |
81 fun drot_tac k i = DETERM (rotate_tac k i); |
84 fun spec_tac 0 i = all_tac |
82 fun spec_tac 0 i = all_tac |
85 | spec_tac k i = EVERY' [dtac spec, drot_tac ~1, spec_tac (k-1)] i; |
83 | spec_tac k i = EVERY' [dtac spec, drot_tac ~1, spec_tac (k-1)] i; |
86 fun dup_spec_tac k i = if k = 0 then all_tac else EVERY' |
84 fun dup_spec_tac k i = if k = 0 then all_tac else EVERY' |
87 [DETERM o (etac all_dupE), drot_tac ~2, spec_tac (k-1)] i; |
85 [DETERM o (etac all_dupE), drot_tac ~2, spec_tac (k-1)] i; |
88 fun same_head _ (Const (x,_)) (Const (y,_)) = x = y |
86 fun same_head _ (Const (x,_)) (Const (y,_)) = x = y |
89 | same_head k (s$_) (t$_) = same_head k s t |
87 | same_head k (s$_) (t$_) = same_head k s t |
90 | same_head k (Bound i) (Bound j) = i = j + k |
88 | same_head k (Bound i) (Bound j) = i = j + k |
91 | same_head _ _ _ = true; |
89 | same_head _ _ _ = true; |
92 fun mapn f n [] = [] |
90 fun mapn f n [] = [] |
93 | mapn f n (x::xs) = f n x::mapn f (n+1) xs; |
91 | mapn f n (x::xs) = f n x::mapn f (n+1) xs; |
94 fun pres_tac (k,arrow,t) n i = drot_tac n i THEN ( |
92 fun pres_tac (k,arrow,t) n i = drot_tac n i THEN ( |
95 if same_head k t concl |
93 if same_head k t concl |
96 then dup_spec_tac k i THEN |
94 then dup_spec_tac k i THEN |
97 (if arrow then etac mp i THEN drot_tac (~n) i else atac i) |
95 (if arrow then etac mp i THEN drot_tac (~n) i else atac i) |
98 else no_tac); |
96 else no_tac); |
99 val ptacs = mapn (fn n => fn t => |
97 val ptacs = mapn (fn n => fn t => |
100 pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems; |
98 pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems; |
101 in Library.foldl (op APPEND) (no_tac, ptacs) st end; |
99 in Library.foldl (op APPEND) (no_tac, ptacs) st end; |
102 |
100 |
103 fun ptac prog = let |
101 fun ptac prog = let |
104 val proga = List.concat (map atomizeD prog) (* atomize the prog *) |
102 val proga = List.concat (map atomizeD prog) (* atomize the prog *) |
105 in (REPEAT_DETERM1 o FIRST' [ |
103 in (REPEAT_DETERM1 o FIRST' [ |
106 rtac TrueI, (* "True" *) |
104 rtac TrueI, (* "True" *) |
107 rtac conjI, (* "[| P; Q |] ==> P & Q" *) |
105 rtac conjI, (* "[| P; Q |] ==> P & Q" *) |
108 rtac allI, (* "(!!x. P x) ==> ! x. P x" *) |
106 rtac allI, (* "(!!x. P x) ==> ! x. P x" *) |
109 rtac exI, (* "P x ==> ? x. P x" *) |
107 rtac exI, (* "P x ==> ? x. P x" *) |
110 rtac impI THEN' (* "(P ==> Q) ==> P --> Q" *) |
108 rtac impI THEN' (* "(P ==> Q) ==> P --> Q" *) |
111 asm_full_simp_tac atomize_ss THEN' (* atomize the asms *) |
109 asm_full_simp_tac atomize_ss THEN' (* atomize the asms *) |
112 (REPEAT_DETERM o (etac conjE)) (* split the asms *) |
110 (REPEAT_DETERM o (etac conjE)) (* split the asms *) |
113 ]) |
111 ]) |
114 ORELSE' resolve_tac [disjI1,disjI2] (* "P ==> P | Q","Q ==> P | Q"*) |
112 ORELSE' resolve_tac [disjI1,disjI2] (* "P ==> P | Q","Q ==> P | Q"*) |
115 ORELSE' ((resolve_tac proga APPEND' hyp_resolve_tac) |
113 ORELSE' ((resolve_tac proga APPEND' hyp_resolve_tac) |
116 THEN' (fn _ => check_HOHH_tac2)) |
114 THEN' (fn _ => check_HOHH_tac2)) |
117 end; |
115 end; |
118 |
116 |
119 fun prolog_tac prog = check_HOHH_tac1 THEN |
117 fun prolog_tac prog = check_HOHH_tac1 THEN |
120 DEPTH_SOLVE (ptac (map check_HOHH prog) 1); |
118 DEPTH_SOLVE (ptac (map check_HOHH prog) 1); |
121 |
119 |
122 val prog_HOHH = []; |
120 val prog_HOHH = []; |