|
1 (* Title: HOL/Prolog/prolog.ML |
|
2 ID: $Id$ |
|
3 Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) |
|
4 *) |
|
5 |
|
6 set Proof.show_main_goal; |
|
7 |
|
8 structure Prolog = |
|
9 struct |
|
10 |
|
11 exception not_HOHH; |
|
12 |
|
13 fun isD t = case t of |
|
14 Const("Trueprop",_)$t => isD t |
|
15 | Const("op &" ,_)$l$r => isD l andalso isD r |
|
16 | Const("op -->",_)$l$r => isG l andalso isD r |
|
17 | Const( "==>",_)$l$r => isG l andalso isD r |
|
18 | Const("All",_)$Abs(s,_,t) => isD t |
|
19 | Const("all",_)$Abs(s,_,t) => isD t |
|
20 | Const("op |",_)$_$_ => false |
|
21 | Const("Ex" ,_)$_ => false |
|
22 | Const("not",_)$_ => false |
|
23 | Const("True",_) => false |
|
24 | Const("False",_) => false |
|
25 | l $ r => isD l |
|
26 | Const _ (* rigid atom *) => true |
|
27 | Bound _ (* rigid atom *) => true |
|
28 | Free _ (* rigid atom *) => true |
|
29 | _ (* flexible atom, |
|
30 anything else *) => false |
|
31 and |
|
32 isG t = case t of |
|
33 Const("Trueprop",_)$t => isG t |
|
34 | Const("op &" ,_)$l$r => isG l andalso isG r |
|
35 | Const("op |" ,_)$l$r => isG l andalso isG r |
|
36 | Const("op -->",_)$l$r => isD l andalso isG r |
|
37 | Const( "==>",_)$l$r => isD l andalso isG r |
|
38 | Const("All",_)$Abs(_,_,t) => isG t |
|
39 | Const("all",_)$Abs(_,_,t) => isG t |
|
40 | Const("Ex" ,_)$Abs(_,_,t) => isG t |
|
41 | Const("True",_) => true |
|
42 | Const("not",_)$_ => false |
|
43 | Const("False",_) => false |
|
44 | _ (* atom *) => true; |
|
45 |
|
46 val check_HOHH_tac1 = PRIMITIVE (fn thm => |
|
47 if isG (concl_of thm) then thm else raise not_HOHH); |
|
48 val check_HOHH_tac2 = PRIMITIVE (fn thm => |
|
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) |
|
51 then thm else raise not_HOHH); |
|
52 |
|
53 fun atomizeD thm = let |
|
54 fun at thm = case concl_of thm of |
|
55 _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (read_instantiate [("x", |
|
56 "?"^(if s="P" then "PP" else s))] spec)) |
|
57 | _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) |
|
58 | _$(Const("op -->",_)$_$_) => at(thm RS mp) |
|
59 | _ => [thm] |
|
60 in map zero_var_indexes (at thm) end; |
|
61 |
|
62 val atomize_ss = |
|
63 Simplifier.theory_context (the_context ()) empty_ss |
|
64 setmksimps (mksimps mksimps_pairs) |
|
65 addsimps [ |
|
66 all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *) |
|
67 imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *) |
|
68 imp_conjR, (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *) |
|
69 imp_all]; (* "((!x. D) :- G) = (!x. D :- G)" *) |
|
70 |
|
71 (*val hyp_resolve_tac = METAHYPS (fn prems => |
|
72 resolve_tac (List.concat (map atomizeD prems)) 1); |
|
73 -- is nice, but cannot instantiate unknowns in the assumptions *) |
|
74 fun hyp_resolve_tac i st = let |
|
75 fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a ,t)) |
|
76 | ap (Const("op -->",_)$_$t) =(case ap t of (k,_,t) => (k,true ,t)) |
|
77 | ap t = (0,false,t); |
|
78 (* |
|
79 fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t |
|
80 | rep_goal (Const ("==>",_)$s$t) = |
|
81 (case rep_goal t of (l,t) => (s::l,t)) |
|
82 | rep_goal t = ([] ,t); |
|
83 val (prems, Const("Trueprop", _)$concl) = rep_goal |
|
84 (#3(dest_state (st,i))); |
|
85 *) |
|
86 val subgoal = #3(dest_state (st,i)); |
|
87 val prems = Logic.strip_assums_hyp subgoal; |
|
88 val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal); |
|
89 fun drot_tac k i = DETERM (rotate_tac k i); |
|
90 fun spec_tac 0 i = all_tac |
|
91 | spec_tac k i = EVERY' [dtac spec, drot_tac ~1, spec_tac (k-1)] i; |
|
92 fun dup_spec_tac k i = if k = 0 then all_tac else EVERY' |
|
93 [DETERM o (etac all_dupE), drot_tac ~2, spec_tac (k-1)] i; |
|
94 fun same_head _ (Const (x,_)) (Const (y,_)) = x = y |
|
95 | same_head k (s$_) (t$_) = same_head k s t |
|
96 | same_head k (Bound i) (Bound j) = i = j + k |
|
97 | same_head _ _ _ = true; |
|
98 fun mapn f n [] = [] |
|
99 | mapn f n (x::xs) = f n x::mapn f (n+1) xs; |
|
100 fun pres_tac (k,arrow,t) n i = drot_tac n i THEN ( |
|
101 if same_head k t concl |
|
102 then dup_spec_tac k i THEN |
|
103 (if arrow then etac mp i THEN drot_tac (~n) i else atac i) |
|
104 else no_tac); |
|
105 val ptacs = mapn (fn n => fn t => |
|
106 pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems; |
|
107 in Library.foldl (op APPEND) (no_tac, ptacs) st end; |
|
108 |
|
109 fun ptac prog = let |
|
110 val proga = List.concat (map atomizeD prog) (* atomize the prog *) |
|
111 in (REPEAT_DETERM1 o FIRST' [ |
|
112 rtac TrueI, (* "True" *) |
|
113 rtac conjI, (* "[| P; Q |] ==> P & Q" *) |
|
114 rtac allI, (* "(!!x. P x) ==> ! x. P x" *) |
|
115 rtac exI, (* "P x ==> ? x. P x" *) |
|
116 rtac impI THEN' (* "(P ==> Q) ==> P --> Q" *) |
|
117 asm_full_simp_tac atomize_ss THEN' (* atomize the asms *) |
|
118 (REPEAT_DETERM o (etac conjE)) (* split the asms *) |
|
119 ]) |
|
120 ORELSE' resolve_tac [disjI1,disjI2] (* "P ==> P | Q","Q ==> P | Q"*) |
|
121 ORELSE' ((resolve_tac proga APPEND' hyp_resolve_tac) |
|
122 THEN' (fn _ => check_HOHH_tac2)) |
|
123 end; |
|
124 |
|
125 fun prolog_tac prog = check_HOHH_tac1 THEN |
|
126 DEPTH_SOLVE (ptac (map check_HOHH prog) 1); |
|
127 |
|
128 val prog_HOHH = []; |
|
129 |
|
130 end; |