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