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