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