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