src/HOLCF/adm.ML
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 14643 130076a81b84
child 15531 08c8dad8e399
permissions -rw-r--r--
Merged in license change from Isabelle2004
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, _)::_) =
wenzelm@7652
    92
  let val parTs = map snd (rev params)
wenzelm@7652
    93
  in Sign.of_sort sign (fastype_of1 (T::parTs, t), chfin_pcpoS) end;
mueller@3655
    94
mueller@3655
    95
mueller@3655
    96
(*** try to prove that terms in list are continuous
mueller@3655
    97
     if successful, add continuity theorem to list l ***)
mueller@3655
    98
mueller@3655
    99
fun prove_cont tac sign s T prems params (l, ts as ((t, _)::_)) =
wenzelm@4039
   100
  let val parTs = map snd (rev params);
mueller@3655
   101
       val contT = (T --> (fastype_of1 (T::parTs, t))) --> HOLogic.boolT;
mueller@3655
   102
       fun mk_all [] t = t
mueller@3655
   103
         | mk_all ((a,T)::Ts) t = (all T) $ (Abs (a, T, mk_all Ts t));
oheimb@4005
   104
       val t = HOLogic.mk_Trueprop((Const (cont_name, contT)) $ (Abs(s, T, t)));
mueller@3655
   105
       val t' = mk_all params (Logic.list_implies (prems, t));
wenzelm@13480
   106
       val thm = Tactic.prove sign [] [] t' (K (tac 1));
wenzelm@4039
   107
  in (ts, thm)::l end
wenzelm@11630
   108
  handle ERROR_MESSAGE _ => l;
mueller@3655
   109
mueller@3655
   110
berghofe@8411
   111
(*** instantiation of adm_subst theorem (a bit tricky) ***)
mueller@3655
   112
mueller@3655
   113
fun inst_adm_subst_thm state i params s T subt t paths =
mueller@3655
   114
  let val {sign, maxidx, ...} = rep_thm state;
mueller@3655
   115
      val j = maxidx+1;
wenzelm@14643
   116
      val tsig = Sign.tsig_of sign;
mueller@3655
   117
      val parTs = map snd (rev params);
mueller@3655
   118
      val rule = lift_rule (state, i) adm_subst;
mueller@3655
   119
      val types = the o (fst (types_sorts rule));
mueller@3655
   120
      val tT = types ("t", j);
mueller@3655
   121
      val PT = types ("P", j);
mueller@3655
   122
      fun mk_abs [] t = t
mueller@3655
   123
        | mk_abs ((a,T)::Ts) t = Abs (a, T, mk_abs Ts t);
mueller@3655
   124
      val tt = cterm_of sign (mk_abs (params @ [(s, T)]) subt);
mueller@3655
   125
      val Pt = cterm_of sign (mk_abs (params @ [(s, fastype_of1 (T::parTs, subt))])
mueller@3655
   126
                     (make_term t [] paths 0));
berghofe@8411
   127
      val tye = Type.typ_match tsig (Vartab.empty, (tT, #T (rep_cterm tt)));
berghofe@8411
   128
      val tye' = Vartab.dest (Type.typ_match tsig (tye, (PT, #T (rep_cterm Pt))));
mueller@3655
   129
      val ctye = map (fn (x, y) => (x, ctyp_of sign y)) tye';
mueller@3655
   130
      val tv = cterm_of sign (Var (("t", j), typ_subst_TVars tye' tT));
mueller@3655
   131
      val Pv = cterm_of sign (Var (("P", j), typ_subst_TVars tye' PT));
mueller@3655
   132
      val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule
mueller@3655
   133
  in rule' end;
mueller@3655
   134
mueller@3655
   135
mueller@3655
   136
(*** extract subgoal i from proof state ***)
mueller@3655
   137
mueller@3655
   138
fun nth_subgoal i thm = nth_elem (i-1, prems_of thm);
mueller@3655
   139
mueller@3655
   140
berghofe@8411
   141
(*** the admissibility tactic ***)
mueller@3655
   142
wenzelm@4039
   143
fun try_dest_adm (Const _ $ (Const (name, _) $ Abs abs)) =
wenzelm@4039
   144
      if name = adm_name then Some abs else None
wenzelm@4039
   145
  | try_dest_adm _ = None;
wenzelm@4039
   146
mueller@3655
   147
fun adm_tac tac i state =
mueller@3655
   148
  state |>
wenzelm@4039
   149
  let val goali = nth_subgoal i state in
wenzelm@4039
   150
    (case try_dest_adm (Logic.strip_assums_concl goali) of
wenzelm@4039
   151
      None => no_tac
wenzelm@4039
   152
    | Some (s, T, t) =>
wenzelm@4039
   153
        let
wenzelm@4039
   154
          val sign = sign_of_thm state;
wenzelm@4039
   155
          val prems = Logic.strip_assums_hyp goali;
wenzelm@4039
   156
          val params = Logic.strip_params goali;
wenzelm@4039
   157
          val ts = find_subterms t 0 [];
wenzelm@4039
   158
          val ts' = filter eq_terms ts;
wenzelm@4039
   159
          val ts'' = filter (is_chfin sign T params) ts';
wenzelm@4039
   160
          val thms = foldl (prove_cont tac sign s T prems params) ([], ts'');
wenzelm@4039
   161
        in
wenzelm@4039
   162
          (case thms of
wenzelm@4039
   163
            ((ts as ((t', _)::_), cont_thm)::_) =>
wenzelm@4039
   164
              let
wenzelm@4039
   165
                val paths = map snd ts;
wenzelm@4039
   166
                val rule = inst_adm_subst_thm state i params s T t' t paths;
wenzelm@4039
   167
              in
wenzelm@4039
   168
                compose_tac (false, rule, 2) i THEN
wenzelm@4039
   169
                rtac cont_thm i THEN
wenzelm@4039
   170
                REPEAT (assume_tac i) THEN
oheimb@4721
   171
                rtac adm_chfin i
wenzelm@4039
   172
              end 
wenzelm@4039
   173
          | [] => no_tac)
wenzelm@4039
   174
        end)
mueller@3655
   175
    end;
mueller@3655
   176
wenzelm@4039
   177
mueller@3655
   178
end;
mueller@3655
   179
wenzelm@4039
   180
wenzelm@4039
   181
open Adm;