--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/adm.ML Wed Sep 03 16:24:46 1997 +0200
@@ -0,0 +1,165 @@
+(******************* admissibility tactic ***********************
+ checks whether adm_subst theorem is applicable to the
+ current proof state. "t" is instantiated with a term of chain-
+ finite type, so that adm_chain_finite can be applied.
+
+ example of usage:
+
+ by (adm_tac cont_tacRs 1);
+
+*****************************************************************)
+
+local
+
+(*** find_subterms t 0 []
+ returns lists of terms with the following properties:
+ 1. all terms in the list are disjoint subterms of t
+ 2. all terms contain the variable which is bound at level 0
+ 3. all occurences of the variable which is bound at level 0
+ are "covered" by a term in the list
+ a list of integers is associated with every term which describes
+ the "path" leading to the subterm (required for instantiation of
+ the adm_subst theorem (see functions mk_term, inst_adm_subst_thm))
+***)
+
+fun find_subterms (Bound i) lev path =
+ if i = lev then [[(Bound 0, path)]]
+ else []
+ | find_subterms (t as (Abs (_, _, t2))) lev path =
+ if filter (fn x => x<=lev)
+ (add_loose_bnos (t, 0, [])) = [lev] then
+ [(incr_bv (~lev, 0, t), path)]::
+ (find_subterms t2 (lev+1) (0::path))
+ else find_subterms t2 (lev+1) (0::path)
+ | find_subterms (t as (t1 $ t2)) lev path =
+ let val ts1 = find_subterms t1 lev (0::path);
+ val ts2 = find_subterms t2 lev (1::path);
+ fun combine [] y = []
+ | combine (x::xs) ys =
+ (map (fn z => x @ z) ys) @ (combine xs ys)
+ in
+ (if filter (fn x => x<=lev)
+ (add_loose_bnos (t, 0, [])) = [lev] then
+ [[(incr_bv (~lev, 0, t), path)]]
+ else []) @
+ (if ts1 = [] then ts2
+ else if ts2 = [] then ts1
+ else combine ts1 ts2)
+ end
+ | find_subterms _ _ _ = [];
+
+
+(*** make term for instantiation of predicate "P" in adm_subst theorem ***)
+
+fun make_term t path paths lev =
+ if path mem paths then Bound lev
+ else case t of
+ (Abs (s, T, t1)) => Abs (s, T, make_term t1 (0::path) paths (lev+1))
+ | (t1 $ t2) => (make_term t1 (0::path) paths lev) $
+ (make_term t2 (1::path) paths lev)
+ | t1 => t1;
+
+
+(*** check whether all terms in list are equal ***)
+
+fun eq_terms (ts as ((t, _)::_)) = forall (fn (t2, _) => t2 aconv t) ts;
+
+
+(*** NOTE: when the following two functions are called, all terms in the list
+ are equal (only their "paths" differ!)
+***)
+
+(*** check whether type of terms in list is chain finite ***)
+
+fun is_chfin sign T params ((t, _)::_) =
+ let val {tsig, ...} = Sign.rep_sg sign;
+ val parTs = map snd (rev params)
+ in Type.of_sort tsig (fastype_of1 (T::parTs, t), ["chfin", "pcpo"]) end;
+
+
+(*** try to prove that terms in list are continuous
+ if successful, add continuity theorem to list l ***)
+
+fun prove_cont tac sign s T prems params (l, ts as ((t, _)::_)) =
+ (let val parTs = map snd (rev params);
+ val contT = (T --> (fastype_of1 (T::parTs, t))) --> HOLogic.boolT;
+ fun mk_all [] t = t
+ | mk_all ((a,T)::Ts) t = (all T) $ (Abs (a, T, mk_all Ts t));
+ val t = HOLogic.mk_Trueprop ((Const ("cont", contT)) $ (Abs (s, T, t)));
+ val t' = mk_all params (Logic.list_implies (prems, t));
+ val thm = prove_goalw_cterm [] (cterm_of sign t')
+ (fn ps => [cut_facts_tac ps 1, tac 1])
+ in (ts, thm)::l end) handle _ => l;
+
+
+(*** instantiation of adm_subst theorem (a bit tricky)
+ NOTE: maybe unnecessary (if "cont_thm RS adm_subst" works properly) ***)
+
+fun inst_adm_subst_thm state i params s T subt t paths =
+ let val {sign, maxidx, ...} = rep_thm state;
+ val j = maxidx+1;
+ val {tsig, ...} = Sign.rep_sg sign;
+ val parTs = map snd (rev params);
+ val rule = lift_rule (state, i) adm_subst;
+ val types = the o (fst (types_sorts rule));
+ val tT = types ("t", j);
+ val PT = types ("P", j);
+ fun mk_abs [] t = t
+ | mk_abs ((a,T)::Ts) t = Abs (a, T, mk_abs Ts t);
+ val tt = cterm_of sign (mk_abs (params @ [(s, T)]) subt);
+ val Pt = cterm_of sign (mk_abs (params @ [(s, fastype_of1 (T::parTs, subt))])
+ (make_term t [] paths 0));
+ val tye = Type.typ_match tsig ([], (tT, #T (rep_cterm tt)));
+ val tye' = Type.typ_match tsig (tye, (PT, #T (rep_cterm Pt)));
+ val ctye = map (fn (x, y) => (x, ctyp_of sign y)) tye';
+ val tv = cterm_of sign (Var (("t", j), typ_subst_TVars tye' tT));
+ val Pv = cterm_of sign (Var (("P", j), typ_subst_TVars tye' PT));
+ val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule
+ in rule' end;
+
+
+(*** extract subgoal i from proof state ***)
+
+fun nth_subgoal i thm = nth_elem (i-1, prems_of thm);
+
+
+in
+
+(*** the admissibility tactic
+ NOTE:
+ (compose_tac (false, rule, 2) i) THEN
+ (rtac cont_thm i) THEN ...
+ could probably be replaced by
+ (rtac (cont_thm RS adm_subst) 1) THEN ...
+***)
+
+fun adm_tac tac i state =
+ state |>
+ let val goali = nth_subgoal i state
+ in
+ case Logic.strip_assums_concl goali of
+ ((Const _) $ ((Const ("adm", _)) $ (Abs (s, T, t)))) =>
+ let val {sign, ...} = rep_thm state;
+ val prems = Logic.strip_assums_hyp goali;
+ val params = Logic.strip_params goali;
+ val ts = find_subterms t 0 [];
+ val ts' = filter eq_terms ts;
+ val ts'' = filter (is_chfin sign T params) ts';
+ val thms = foldl (prove_cont tac sign s T prems params) ([], ts'')
+ in case thms of
+ ((ts as ((t', _)::_), cont_thm)::_) =>
+ let val paths = map snd ts;
+ val rule = inst_adm_subst_thm state i params s T t' t paths;
+ in
+ (compose_tac (false, rule, 2) i) THEN
+ (rtac cont_thm i) THEN
+ (REPEAT (assume_tac i)) THEN
+ (rtac adm_chain_finite i)
+ end
+ | [] => no_tac
+ end
+ | _ => no_tac
+ end;
+
+end;
+