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