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