4039
|
1 |
(* Title: HOLCF/adm.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Stefan Berghofer, TU Muenchen
|
|
4 |
|
|
5 |
Admissibility tactic.
|
|
6 |
|
|
7 |
Checks whether adm_subst theorem is applicable to the current proof
|
|
8 |
state:
|
|
9 |
|
|
10 |
[| cont t; adm P |] ==> adm (%x. P (t x))
|
3655
|
11 |
|
4039
|
12 |
"t" is instantiated with a term of chain-finite type, so that
|
|
13 |
adm_chain_finite can be applied:
|
|
14 |
|
|
15 |
adm (P::'a::{chfin,pcpo} => bool)
|
|
16 |
|
|
17 |
*)
|
3655
|
18 |
|
4039
|
19 |
signature ADM =
|
|
20 |
sig
|
|
21 |
val adm_tac: (int -> tactic) -> int -> tactic
|
|
22 |
end;
|
3655
|
23 |
|
4039
|
24 |
structure Adm: ADM =
|
|
25 |
struct
|
|
26 |
|
3655
|
27 |
|
|
28 |
(*** find_subterms t 0 []
|
|
29 |
returns lists of terms with the following properties:
|
|
30 |
1. all terms in the list are disjoint subterms of t
|
|
31 |
2. all terms contain the variable which is bound at level 0
|
|
32 |
3. all occurences of the variable which is bound at level 0
|
|
33 |
are "covered" by a term in the list
|
|
34 |
a list of integers is associated with every term which describes
|
|
35 |
the "path" leading to the subterm (required for instantiation of
|
|
36 |
the adm_subst theorem (see functions mk_term, inst_adm_subst_thm))
|
|
37 |
***)
|
|
38 |
|
|
39 |
fun find_subterms (Bound i) lev path =
|
|
40 |
if i = lev then [[(Bound 0, path)]]
|
|
41 |
else []
|
|
42 |
| find_subterms (t as (Abs (_, _, t2))) lev path =
|
|
43 |
if filter (fn x => x<=lev)
|
|
44 |
(add_loose_bnos (t, 0, [])) = [lev] then
|
|
45 |
[(incr_bv (~lev, 0, t), path)]::
|
|
46 |
(find_subterms t2 (lev+1) (0::path))
|
|
47 |
else find_subterms t2 (lev+1) (0::path)
|
|
48 |
| find_subterms (t as (t1 $ t2)) lev path =
|
|
49 |
let val ts1 = find_subterms t1 lev (0::path);
|
|
50 |
val ts2 = find_subterms t2 lev (1::path);
|
|
51 |
fun combine [] y = []
|
|
52 |
| combine (x::xs) ys =
|
|
53 |
(map (fn z => x @ z) ys) @ (combine xs ys)
|
|
54 |
in
|
|
55 |
(if filter (fn x => x<=lev)
|
|
56 |
(add_loose_bnos (t, 0, [])) = [lev] then
|
|
57 |
[[(incr_bv (~lev, 0, t), path)]]
|
|
58 |
else []) @
|
|
59 |
(if ts1 = [] then ts2
|
|
60 |
else if ts2 = [] then ts1
|
|
61 |
else combine ts1 ts2)
|
|
62 |
end
|
|
63 |
| find_subterms _ _ _ = [];
|
|
64 |
|
|
65 |
|
|
66 |
(*** make term for instantiation of predicate "P" in adm_subst theorem ***)
|
|
67 |
|
|
68 |
fun make_term t path paths lev =
|
|
69 |
if path mem paths then Bound lev
|
|
70 |
else case t of
|
|
71 |
(Abs (s, T, t1)) => Abs (s, T, make_term t1 (0::path) paths (lev+1))
|
|
72 |
| (t1 $ t2) => (make_term t1 (0::path) paths lev) $
|
|
73 |
(make_term t2 (1::path) paths lev)
|
|
74 |
| t1 => t1;
|
|
75 |
|
|
76 |
|
|
77 |
(*** check whether all terms in list are equal ***)
|
|
78 |
|
4039
|
79 |
fun eq_terms [] = true
|
|
80 |
| eq_terms (ts as (t, _) :: _) = forall (fn (t2, _) => t2 aconv t) ts;
|
3655
|
81 |
|
|
82 |
|
4039
|
83 |
(*figure out internal names*)
|
|
84 |
val chfin_pcpoS = Sign.intern_sort (sign_of HOLCF.thy) ["chfin", "pcpo"];
|
4005
|
85 |
val cont_name = Sign.intern_const (sign_of HOLCF.thy) "cont";
|
4039
|
86 |
val adm_name = Sign.intern_const (sign_of HOLCF.thy) "adm";
|
4005
|
87 |
|
|
88 |
|
3655
|
89 |
(*** check whether type of terms in list is chain finite ***)
|
|
90 |
|
|
91 |
fun is_chfin sign T params ((t, _)::_) =
|
|
92 |
let val {tsig, ...} = Sign.rep_sg sign;
|
|
93 |
val parTs = map snd (rev params)
|
4039
|
94 |
in Type.of_sort tsig (fastype_of1 (T::parTs, t), chfin_pcpoS) end;
|
3655
|
95 |
|
|
96 |
|
|
97 |
(*** try to prove that terms in list are continuous
|
|
98 |
if successful, add continuity theorem to list l ***)
|
|
99 |
|
|
100 |
fun prove_cont tac sign s T prems params (l, ts as ((t, _)::_)) =
|
4039
|
101 |
let val parTs = map snd (rev params);
|
3655
|
102 |
val contT = (T --> (fastype_of1 (T::parTs, t))) --> HOLogic.boolT;
|
|
103 |
fun mk_all [] t = t
|
|
104 |
| mk_all ((a,T)::Ts) t = (all T) $ (Abs (a, T, mk_all Ts t));
|
4005
|
105 |
val t = HOLogic.mk_Trueprop((Const (cont_name, contT)) $ (Abs(s, T, t)));
|
3655
|
106 |
val t' = mk_all params (Logic.list_implies (prems, t));
|
|
107 |
val thm = prove_goalw_cterm [] (cterm_of sign t')
|
|
108 |
(fn ps => [cut_facts_tac ps 1, tac 1])
|
4039
|
109 |
in (ts, thm)::l end
|
|
110 |
handle _ => l;
|
3655
|
111 |
|
|
112 |
|
|
113 |
(*** instantiation of adm_subst theorem (a bit tricky)
|
|
114 |
NOTE: maybe unnecessary (if "cont_thm RS adm_subst" works properly) ***)
|
|
115 |
|
|
116 |
fun inst_adm_subst_thm state i params s T subt t paths =
|
|
117 |
let val {sign, maxidx, ...} = rep_thm state;
|
|
118 |
val j = maxidx+1;
|
|
119 |
val {tsig, ...} = Sign.rep_sg sign;
|
|
120 |
val parTs = map snd (rev params);
|
|
121 |
val rule = lift_rule (state, i) adm_subst;
|
|
122 |
val types = the o (fst (types_sorts rule));
|
|
123 |
val tT = types ("t", j);
|
|
124 |
val PT = types ("P", j);
|
|
125 |
fun mk_abs [] t = t
|
|
126 |
| mk_abs ((a,T)::Ts) t = Abs (a, T, mk_abs Ts t);
|
|
127 |
val tt = cterm_of sign (mk_abs (params @ [(s, T)]) subt);
|
|
128 |
val Pt = cterm_of sign (mk_abs (params @ [(s, fastype_of1 (T::parTs, subt))])
|
|
129 |
(make_term t [] paths 0));
|
|
130 |
val tye = Type.typ_match tsig ([], (tT, #T (rep_cterm tt)));
|
|
131 |
val tye' = Type.typ_match tsig (tye, (PT, #T (rep_cterm Pt)));
|
|
132 |
val ctye = map (fn (x, y) => (x, ctyp_of sign y)) tye';
|
|
133 |
val tv = cterm_of sign (Var (("t", j), typ_subst_TVars tye' tT));
|
|
134 |
val Pv = cterm_of sign (Var (("P", j), typ_subst_TVars tye' PT));
|
|
135 |
val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule
|
|
136 |
in rule' end;
|
|
137 |
|
|
138 |
|
|
139 |
(*** extract subgoal i from proof state ***)
|
|
140 |
|
|
141 |
fun nth_subgoal i thm = nth_elem (i-1, prems_of thm);
|
|
142 |
|
|
143 |
|
|
144 |
(*** the admissibility tactic
|
|
145 |
NOTE:
|
|
146 |
(compose_tac (false, rule, 2) i) THEN
|
|
147 |
(rtac cont_thm i) THEN ...
|
|
148 |
could probably be replaced by
|
|
149 |
(rtac (cont_thm RS adm_subst) 1) THEN ...
|
|
150 |
***)
|
|
151 |
|
4039
|
152 |
fun try_dest_adm (Const _ $ (Const (name, _) $ Abs abs)) =
|
|
153 |
if name = adm_name then Some abs else None
|
|
154 |
| try_dest_adm _ = None;
|
|
155 |
|
3655
|
156 |
fun adm_tac tac i state =
|
|
157 |
state |>
|
4039
|
158 |
let val goali = nth_subgoal i state in
|
|
159 |
(case try_dest_adm (Logic.strip_assums_concl goali) of
|
|
160 |
None => no_tac
|
|
161 |
| Some (s, T, t) =>
|
|
162 |
let
|
|
163 |
val sign = sign_of_thm state;
|
|
164 |
val prems = Logic.strip_assums_hyp goali;
|
|
165 |
val params = Logic.strip_params goali;
|
|
166 |
val ts = find_subterms t 0 [];
|
|
167 |
val ts' = filter eq_terms ts;
|
|
168 |
val ts'' = filter (is_chfin sign T params) ts';
|
|
169 |
val thms = foldl (prove_cont tac sign s T prems params) ([], ts'');
|
|
170 |
in
|
|
171 |
(case thms of
|
|
172 |
((ts as ((t', _)::_), cont_thm)::_) =>
|
|
173 |
let
|
|
174 |
val paths = map snd ts;
|
|
175 |
val rule = inst_adm_subst_thm state i params s T t' t paths;
|
|
176 |
in
|
|
177 |
compose_tac (false, rule, 2) i THEN
|
|
178 |
rtac cont_thm i THEN
|
|
179 |
REPEAT (assume_tac i) THEN
|
|
180 |
rtac adm_chain_finite i
|
|
181 |
end
|
|
182 |
| [] => no_tac)
|
|
183 |
end)
|
3655
|
184 |
end;
|
|
185 |
|
4039
|
186 |
|
3655
|
187 |
end;
|
|
188 |
|
4039
|
189 |
|
|
190 |
open Adm;
|