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