author | wenzelm |
Tue, 05 Nov 2019 14:28:00 +0100 | |
changeset 71047 | 87c132cf5860 |
parent 69597 | ff784d5a5bfb |
child 76091 | 922e3f9251ac |
permissions | -rw-r--r-- |
21425 | 1 |
(* Title: HOL/Prolog/prolog.ML |
2 |
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) |
|
3 |
*) |
|
4 |
||
69597 | 5 |
Options.default_put_bool \<^system_option>\<open>show_main_goal\<close> true; |
21425 | 6 |
|
7 |
structure Prolog = |
|
8 |
struct |
|
9 |
||
10 |
exception not_HOHH; |
|
11 |
||
12 |
fun isD t = case t of |
|
69597 | 13 |
Const(\<^const_name>\<open>Trueprop\<close>,_)$t => isD t |
14 |
| Const(\<^const_name>\<open>HOL.conj\<close> ,_)$l$r => isD l andalso isD r |
|
15 |
| Const(\<^const_name>\<open>HOL.implies\<close>,_)$l$r => isG l andalso isD r |
|
16 |
| Const(\<^const_name>\<open>Pure.imp\<close>,_)$l$r => isG l andalso isD r |
|
17 |
| Const(\<^const_name>\<open>All\<close>,_)$Abs(s,_,t) => isD t |
|
18 |
| Const(\<^const_name>\<open>Pure.all\<close>,_)$Abs(s,_,t) => isD t |
|
19 |
| Const(\<^const_name>\<open>HOL.disj\<close>,_)$_$_ => false |
|
20 |
| Const(\<^const_name>\<open>Ex\<close> ,_)$_ => false |
|
21 |
| Const(\<^const_name>\<open>Not\<close>,_)$_ => false |
|
22 |
| Const(\<^const_name>\<open>True\<close>,_) => false |
|
23 |
| Const(\<^const_name>\<open>False\<close>,_) => false |
|
21425 | 24 |
| l $ r => isD l |
25 |
| Const _ (* rigid atom *) => true |
|
26 |
| Bound _ (* rigid atom *) => true |
|
27 |
| Free _ (* rigid atom *) => true |
|
28 |
| _ (* flexible atom, |
|
29 |
anything else *) => false |
|
30 |
and |
|
31 |
isG t = case t of |
|
69597 | 32 |
Const(\<^const_name>\<open>Trueprop\<close>,_)$t => isG t |
33 |
| Const(\<^const_name>\<open>HOL.conj\<close> ,_)$l$r => isG l andalso isG r |
|
34 |
| Const(\<^const_name>\<open>HOL.disj\<close> ,_)$l$r => isG l andalso isG r |
|
35 |
| Const(\<^const_name>\<open>HOL.implies\<close>,_)$l$r => isD l andalso isG r |
|
36 |
| Const(\<^const_name>\<open>Pure.imp\<close>,_)$l$r => isD l andalso isG r |
|
37 |
| Const(\<^const_name>\<open>All\<close>,_)$Abs(_,_,t) => isG t |
|
38 |
| Const(\<^const_name>\<open>Pure.all\<close>,_)$Abs(_,_,t) => isG t |
|
39 |
| Const(\<^const_name>\<open>Ex\<close> ,_)$Abs(_,_,t) => isG t |
|
40 |
| Const(\<^const_name>\<open>True\<close>,_) => true |
|
41 |
| Const(\<^const_name>\<open>Not\<close>,_)$_ => false |
|
42 |
| Const(\<^const_name>\<open>False\<close>,_) => false |
|
21425 | 43 |
| _ (* atom *) => true; |
44 |
||
45 |
val check_HOHH_tac1 = PRIMITIVE (fn thm => |
|
59582 | 46 |
if isG (Thm.concl_of thm) then thm else raise not_HOHH); |
21425 | 47 |
val check_HOHH_tac2 = PRIMITIVE (fn thm => |
59582 | 48 |
if forall isG (Thm.prems_of thm) then thm else raise not_HOHH); |
49 |
fun check_HOHH thm = (if isD (Thm.concl_of thm) andalso forall isG (Thm.prems_of thm) |
|
21425 | 50 |
then thm else raise not_HOHH); |
51 |
||
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
52233
diff
changeset
|
52 |
fun atomizeD ctxt thm = |
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
52233
diff
changeset
|
53 |
let |
59582 | 54 |
fun at thm = case Thm.concl_of thm of |
69597 | 55 |
_$(Const(\<^const_name>\<open>All\<close> ,_)$Abs(s,_,_))=> |
59755 | 56 |
let val s' = if s="P" then "PP" else s in |
57 |
at(thm RS (Rule_Insts.read_instantiate ctxt [((("x", 0), Position.none), s')] [s'] spec)) |
|
58 |
end |
|
69597 | 59 |
| _$(Const(\<^const_name>\<open>HOL.conj\<close>,_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) |
60 |
| _$(Const(\<^const_name>\<open>HOL.implies\<close>,_)$_$_) => at(thm RS mp) |
|
21425 | 61 |
| _ => [thm] |
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
52233
diff
changeset
|
62 |
in map zero_var_indexes (at thm) end; |
21425 | 63 |
|
64 |
val atomize_ss = |
|
69597 | 65 |
(empty_simpset \<^context> |> Simplifier.set_mksimps (mksimps mksimps_pairs)) |
21425 | 66 |
addsimps [ |
45654 | 67 |
@{thm all_conj_distrib}, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *) |
46161 | 68 |
@{thm imp_conjL} RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *) |
69 |
@{thm imp_conjR}, (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *) |
|
52088 | 70 |
@{thm imp_all}] (* "((!x. D) :- G) = (!x. D :- G)" *) |
71 |
|> simpset_of; |
|
21425 | 72 |
|
45625
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
39125
diff
changeset
|
73 |
|
32283 | 74 |
(*val hyp_resolve_tac = Subgoal.FOCUS_PREMS (fn {prems, ...} => |
32260 | 75 |
resolve_tac (maps atomizeD prems) 1); |
21425 | 76 |
-- is nice, but cannot instantiate unknowns in the assumptions *) |
60754 | 77 |
fun hyp_resolve_tac ctxt = SUBGOAL (fn (subgoal, i) => |
46473 | 78 |
let |
69597 | 79 |
fun ap (Const(\<^const_name>\<open>All\<close>,_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a ,t)) |
80 |
| ap (Const(\<^const_name>\<open>HOL.implies\<close>,_)$_$t) =(case ap t of (k,_,t) => (k,true ,t)) |
|
21425 | 81 |
| ap t = (0,false,t); |
82 |
(* |
|
56245 | 83 |
fun rep_goal (Const (@{const_name Pure.all},_)$Abs (_,_,t)) = rep_goal t |
84 |
| rep_goal (Const (@{const_name Pure.imp},_)$s$t) = |
|
21425 | 85 |
(case rep_goal t of (l,t) => (s::l,t)) |
86 |
| rep_goal t = ([] ,t); |
|
38557 | 87 |
val (prems, Const(@{const_name Trueprop}, _)$concl) = rep_goal |
21425 | 88 |
(#3(dest_state (st,i))); |
89 |
*) |
|
90 |
val prems = Logic.strip_assums_hyp subgoal; |
|
91 |
val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal); |
|
92 |
fun drot_tac k i = DETERM (rotate_tac k i); |
|
93 |
fun spec_tac 0 i = all_tac |
|
60754 | 94 |
| spec_tac k i = EVERY' [dresolve_tac ctxt [spec], drot_tac ~1, spec_tac (k-1)] i; |
21425 | 95 |
fun dup_spec_tac k i = if k = 0 then all_tac else EVERY' |
60754 | 96 |
[DETERM o (eresolve_tac ctxt [all_dupE]), drot_tac ~2, spec_tac (k-1)] i; |
21425 | 97 |
fun same_head _ (Const (x,_)) (Const (y,_)) = x = y |
98 |
| same_head k (s$_) (t$_) = same_head k s t |
|
99 |
| same_head k (Bound i) (Bound j) = i = j + k |
|
100 |
| same_head _ _ _ = true; |
|
101 |
fun mapn f n [] = [] |
|
102 |
| mapn f n (x::xs) = f n x::mapn f (n+1) xs; |
|
103 |
fun pres_tac (k,arrow,t) n i = drot_tac n i THEN ( |
|
60754 | 104 |
if same_head k t concl |
105 |
then dup_spec_tac k i THEN |
|
106 |
(if arrow then eresolve_tac ctxt [mp] i THEN drot_tac (~n) i else assume_tac ctxt i) |
|
107 |
else no_tac); |
|
21425 | 108 |
val ptacs = mapn (fn n => fn t => |
109 |
pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems; |
|
46473 | 110 |
in Library.foldl (op APPEND) (no_tac, ptacs) end); |
21425 | 111 |
|
27229 | 112 |
fun ptac ctxt prog = let |
32952 | 113 |
val proga = maps (atomizeD ctxt) prog (* atomize the prog *) |
21425 | 114 |
in (REPEAT_DETERM1 o FIRST' [ |
60754 | 115 |
resolve_tac ctxt [TrueI], (* "True" *) |
116 |
resolve_tac ctxt [conjI], (* "[| P; Q |] ==> P & Q" *) |
|
117 |
resolve_tac ctxt [allI], (* "(!!x. P x) ==> ! x. P x" *) |
|
118 |
resolve_tac ctxt [exI], (* "P x ==> ? x. P x" *) |
|
119 |
resolve_tac ctxt [impI] THEN' (* "(P ==> Q) ==> P --> Q" *) |
|
52088 | 120 |
asm_full_simp_tac (put_simpset atomize_ss ctxt) THEN' (* atomize the asms *) |
60754 | 121 |
(REPEAT_DETERM o (eresolve_tac ctxt [conjE])) (* split the asms *) |
21425 | 122 |
]) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
56467
diff
changeset
|
123 |
ORELSE' resolve_tac ctxt [disjI1,disjI2] (* "P ==> P | Q","Q ==> P | Q"*) |
60754 | 124 |
ORELSE' ((resolve_tac ctxt proga APPEND' hyp_resolve_tac ctxt) |
21425 | 125 |
THEN' (fn _ => check_HOHH_tac2)) |
126 |
end; |
|
127 |
||
27229 | 128 |
fun prolog_tac ctxt prog = |
129 |
check_HOHH_tac1 THEN |
|
130 |
DEPTH_SOLVE (ptac ctxt (map check_HOHH prog) 1); |
|
21425 | 131 |
|
132 |
val prog_HOHH = []; |
|
133 |
||
134 |
end; |