1.1 --- a/src/HOLCF/HOLCF.thy Mon Jan 05 07:54:16 2009 -0800
1.2 +++ b/src/HOLCF/HOLCF.thy Mon Jan 05 18:13:26 2009 +0100
1.3 @@ -24,7 +24,7 @@
1.4 declaration {* fn _ =>
1.5 Simplifier.map_ss (fn simpset => simpset addSolver
1.6 (mk_solver' "adm_tac" (fn ss =>
1.7 - adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
1.8 + Adm.adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
1.9 *}
1.10
1.11 end
2.1 --- a/src/HOLCF/Tools/adm_tac.ML Mon Jan 05 07:54:16 2009 -0800
2.2 +++ b/src/HOLCF/Tools/adm_tac.ML Mon Jan 05 18:13:26 2009 +0100
2.3 @@ -1,18 +1,16 @@
2.4 -(* ID: $Id$
2.5 - Author: Stefan Berghofer, TU Muenchen
2.6 +(* Author: Stefan Berghofer, TU Muenchen
2.7
2.8 Admissibility tactic.
2.9
2.10 Checks whether adm_subst theorem is applicable to the current proof
2.11 state:
2.12
2.13 - [| cont t; adm P |] ==> adm (%x. P (t x))
2.14 + cont t ==> adm P ==> adm (%x. P (t x))
2.15
2.16 "t" is instantiated with a term of chain-finite type, so that
2.17 adm_chfin can be applied:
2.18
2.19 adm (P::'a::{chfin,pcpo} => bool)
2.20 -
2.21 *)
2.22
2.23 signature ADM =
2.24 @@ -39,21 +37,19 @@
2.25 if i = lev then [[(Bound 0, path)]]
2.26 else []
2.27 | find_subterms (t as (Abs (_, _, t2))) lev path =
2.28 - if List.filter (fn x => x<=lev)
2.29 - (add_loose_bnos (t, 0, [])) = [lev] then
2.30 - [(incr_bv (~lev, 0, t), path)]::
2.31 + if filter (fn x => x <= lev) (add_loose_bnos (t, 0, [])) = [lev]
2.32 + then
2.33 + [(incr_bv (~lev, 0, t), path)] ::
2.34 (find_subterms t2 (lev+1) (0::path))
2.35 else find_subterms t2 (lev+1) (0::path)
2.36 | find_subterms (t as (t1 $ t2)) lev path =
2.37 let val ts1 = find_subterms t1 lev (0::path);
2.38 val ts2 = find_subterms t2 lev (1::path);
2.39 fun combine [] y = []
2.40 - | combine (x::xs) ys =
2.41 - (map (fn z => x @ z) ys) @ (combine xs ys)
2.42 + | combine (x::xs) ys = map (fn z => x @ z) ys @ combine xs ys
2.43 in
2.44 - (if List.filter (fn x => x<=lev)
2.45 - (add_loose_bnos (t, 0, [])) = [lev] then
2.46 - [[(incr_bv (~lev, 0, t), path)]]
2.47 + (if filter (fn x => x <= lev) (add_loose_bnos (t, 0, [])) = [lev]
2.48 + then [[(incr_bv (~lev, 0, t), path)]]
2.49 else []) @
2.50 (if ts1 = [] then ts2
2.51 else if ts2 = [] then ts1
2.52 @@ -65,7 +61,7 @@
2.53 (*** make term for instantiation of predicate "P" in adm_subst theorem ***)
2.54
2.55 fun make_term t path paths lev =
2.56 - if path mem paths then Bound lev
2.57 + if member (op =) paths path then Bound lev
2.58 else case t of
2.59 (Abs (s, T, t1)) => Abs (s, T, make_term t1 (0::path) paths (lev+1))
2.60 | (t1 $ t2) => (make_term t1 (0::path) paths lev) $
2.61 @@ -79,30 +75,24 @@
2.62 | eq_terms (ts as (t, _) :: _) = forall (fn (t2, _) => t2 aconv t) ts;
2.63
2.64
2.65 -(*figure out internal names*)
2.66 -val chfin_pcpoS = Sign.intern_sort (the_context ()) ["chfin", "pcpo"];
2.67 -val cont_name = Sign.intern_const (the_context ()) "cont";
2.68 -val adm_name = Sign.intern_const (the_context ()) "adm";
2.69 -
2.70 -
2.71 (*** check whether type of terms in list is chain finite ***)
2.72
2.73 -fun is_chfin sign T params ((t, _)::_) =
2.74 +fun is_chfin thy T params ((t, _)::_) =
2.75 let val parTs = map snd (rev params)
2.76 - in Sign.of_sort sign (fastype_of1 (T::parTs, t), chfin_pcpoS) end;
2.77 + in Sign.of_sort thy (fastype_of1 (T::parTs, t), @{sort "{chfin,pcpo}"}) end;
2.78
2.79
2.80 (*** try to prove that terms in list are continuous
2.81 if successful, add continuity theorem to list l ***)
2.82
2.83 -fun prove_cont tac sign s T prems params (l, ts as ((t, _)::_)) =
2.84 +fun prove_cont tac thy s T prems params (ts as ((t, _)::_)) l =
2.85 let val parTs = map snd (rev params);
2.86 val contT = (T --> (fastype_of1 (T::parTs, t))) --> HOLogic.boolT;
2.87 fun mk_all [] t = t
2.88 | mk_all ((a,T)::Ts) t = Term.all T $ (Abs (a, T, mk_all Ts t));
2.89 - val t = HOLogic.mk_Trueprop((Const (cont_name, contT)) $ (Abs(s, T, t)));
2.90 + val t = HOLogic.mk_Trueprop (Const (@{const_name cont}, contT) $ Abs (s, T, t));
2.91 val t' = mk_all params (Logic.list_implies (prems, t));
2.92 - val thm = Goal.prove (ProofContext.init sign) [] [] t' (K (tac 1));
2.93 + val thm = Goal.prove (ProofContext.init thy) [] [] t' (K (tac 1));
2.94 in (ts, thm)::l end
2.95 handle ERROR _ => l;
2.96
2.97 @@ -111,71 +101,59 @@
2.98
2.99 fun inst_adm_subst_thm state i params s T subt t paths =
2.100 let
2.101 - val sign = Thm.theory_of_thm state;
2.102 - val j = Thm.maxidx_of state + 1;
2.103 - val parTs = map snd (rev params);
2.104 - val rule = Thm.lift_rule (Thm.cprem_of state i) @{thm adm_subst};
2.105 - val types = valOf o (fst (Drule.types_sorts rule));
2.106 - val tT = types ("t", j);
2.107 - val PT = types ("P", j);
2.108 - fun mk_abs [] t = t
2.109 - | mk_abs ((a,T)::Ts) t = Abs (a, T, mk_abs Ts t);
2.110 - val tt = cterm_of sign (mk_abs (params @ [(s, T)]) subt);
2.111 - val Pt = cterm_of sign (mk_abs (params @ [(s, fastype_of1 (T::parTs, subt))])
2.112 - (make_term t [] paths 0));
2.113 - val tye = Sign.typ_match sign (tT, #T (rep_cterm tt)) Vartab.empty;
2.114 - val tye' = Sign.typ_match sign (PT, #T (rep_cterm Pt)) tye;
2.115 - val ctye = map (fn (ixn, (S, T)) =>
2.116 - (ctyp_of sign (TVar (ixn, S)), ctyp_of sign T)) (Vartab.dest tye');
2.117 - val tv = cterm_of sign (Var (("t", j), Envir.typ_subst_TVars tye' tT));
2.118 - val Pv = cterm_of sign (Var (("P", j), Envir.typ_subst_TVars tye' PT));
2.119 - val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule
2.120 + val thy = Thm.theory_of_thm state;
2.121 + val j = Thm.maxidx_of state + 1;
2.122 + val parTs = map snd (rev params);
2.123 + val rule = Thm.lift_rule (Thm.cprem_of state i) @{thm adm_subst};
2.124 + val types = the o fst (Drule.types_sorts rule);
2.125 + val tT = types ("t", j);
2.126 + val PT = types ("P", j);
2.127 + fun mk_abs [] t = t
2.128 + | mk_abs ((a,T)::Ts) t = Abs (a, T, mk_abs Ts t);
2.129 + val tt = cterm_of thy (mk_abs (params @ [(s, T)]) subt);
2.130 + val Pt = cterm_of thy (mk_abs (params @ [(s, fastype_of1 (T::parTs, subt))])
2.131 + (make_term t [] paths 0));
2.132 + val tye = Sign.typ_match thy (tT, #T (rep_cterm tt)) Vartab.empty;
2.133 + val tye' = Sign.typ_match thy (PT, #T (rep_cterm Pt)) tye;
2.134 + val ctye = map (fn (ixn, (S, T)) =>
2.135 + (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)) (Vartab.dest tye');
2.136 + val tv = cterm_of thy (Var (("t", j), Envir.typ_subst_TVars tye' tT));
2.137 + val Pv = cterm_of thy (Var (("P", j), Envir.typ_subst_TVars tye' PT));
2.138 + val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule
2.139 in rule' end;
2.140
2.141
2.142 -(*** extract subgoal i from proof state ***)
2.143 -
2.144 -fun nth_subgoal i thm = List.nth (prems_of thm, i-1);
2.145 -
2.146 -
2.147 (*** the admissibility tactic ***)
2.148
2.149 -fun try_dest_adm (Const _ $ (Const (name, _) $ Abs abs)) =
2.150 - if name = adm_name then SOME abs else NONE
2.151 +fun try_dest_adm (Const _ $ (Const (@{const_name adm}, _) $ Abs abs)) = SOME abs
2.152 | try_dest_adm _ = NONE;
2.153
2.154 -fun adm_tac tac i state =
2.155 - state |>
2.156 - let val goali = nth_subgoal i state in
2.157 - (case try_dest_adm (Logic.strip_assums_concl goali) of
2.158 - NONE => no_tac
2.159 - | SOME (s, T, t) =>
2.160 - let
2.161 - val sign = Thm.theory_of_thm state;
2.162 - val prems = Logic.strip_assums_hyp goali;
2.163 - val params = Logic.strip_params goali;
2.164 - val ts = find_subterms t 0 [];
2.165 - val ts' = List.filter eq_terms ts;
2.166 - val ts'' = List.filter (is_chfin sign T params) ts';
2.167 - val thms = Library.foldl (prove_cont tac sign s T prems params) ([], ts'');
2.168 - in
2.169 - (case thms of
2.170 - ((ts as ((t', _)::_), cont_thm)::_) =>
2.171 - let
2.172 - val paths = map snd ts;
2.173 - val rule = inst_adm_subst_thm state i params s T t' t paths;
2.174 - in
2.175 - compose_tac (false, rule, 2) i THEN
2.176 - rtac cont_thm i THEN
2.177 - REPEAT (assume_tac i) THEN
2.178 - rtac @{thm adm_chfin} i
2.179 - end
2.180 - | [] => no_tac)
2.181 - end)
2.182 - end;
2.183 -
2.184 +fun adm_tac tac i state = (i, state) |-> SUBGOAL (fn (goali, _) =>
2.185 + (case try_dest_adm (Logic.strip_assums_concl goali) of
2.186 + NONE => no_tac
2.187 + | SOME (s, T, t) =>
2.188 + let
2.189 + val thy = Thm.theory_of_thm state;
2.190 + val prems = Logic.strip_assums_hyp goali;
2.191 + val params = Logic.strip_params goali;
2.192 + val ts = find_subterms t 0 [];
2.193 + val ts' = filter eq_terms ts;
2.194 + val ts'' = filter (is_chfin thy T params) ts';
2.195 + val thms = fold (prove_cont tac thy s T prems params) ts'' [];
2.196 + in
2.197 + (case thms of
2.198 + ((ts as ((t', _)::_), cont_thm) :: _) =>
2.199 + let
2.200 + val paths = map snd ts;
2.201 + val rule = inst_adm_subst_thm state i params s T t' t paths;
2.202 + in
2.203 + compose_tac (false, rule, 2) i THEN
2.204 + resolve_tac [cont_thm] i THEN
2.205 + REPEAT (assume_tac i) THEN
2.206 + resolve_tac [@{thm adm_chfin}] i
2.207 + end
2.208 + | [] => no_tac)
2.209 + end));
2.210
2.211 end;
2.212
2.213 -
2.214 -open Adm;