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