src/HOLCF/Tools/adm_tac.ML
author wenzelm
Fri Jul 17 23:11:40 2009 +0200 (2009-07-17)
changeset 32035 8e77b6a250d5
parent 31023 d027411c9a38
child 33440 181fae134b43
permissions -rw-r--r--
tuned/modernized Envir.subst_XXX;
wenzelm@29355
     1
(*  Author:     Stefan Berghofer, TU Muenchen
wenzelm@23152
     2
wenzelm@23152
     3
Admissibility tactic.
wenzelm@23152
     4
wenzelm@23152
     5
Checks whether adm_subst theorem is applicable to the current proof
wenzelm@23152
     6
state:
wenzelm@23152
     7
wenzelm@29355
     8
  cont t ==> adm P ==> adm (%x. P (t x))
wenzelm@23152
     9
wenzelm@23152
    10
"t" is instantiated with a term of chain-finite type, so that
wenzelm@23152
    11
adm_chfin can be applied:
wenzelm@23152
    12
wenzelm@23152
    13
  adm (P::'a::{chfin,pcpo} => bool)
wenzelm@23152
    14
*)
wenzelm@23152
    15
wenzelm@23152
    16
signature ADM =
wenzelm@23152
    17
sig
wenzelm@30603
    18
  val adm_tac: Proof.context -> (int -> tactic) -> int -> tactic
wenzelm@23152
    19
end;
wenzelm@23152
    20
huffman@31023
    21
structure Adm :> ADM =
wenzelm@23152
    22
struct
wenzelm@23152
    23
wenzelm@23152
    24
wenzelm@23152
    25
(*** find_subterms t 0 []
wenzelm@23152
    26
     returns lists of terms with the following properties:
wenzelm@23152
    27
       1. all terms in the list are disjoint subterms of t
wenzelm@23152
    28
       2. all terms contain the variable which is bound at level 0
wenzelm@23152
    29
       3. all occurences of the variable which is bound at level 0
wenzelm@23152
    30
          are "covered" by a term in the list
wenzelm@23152
    31
     a list of integers is associated with every term which describes
wenzelm@23152
    32
     the "path" leading to the subterm (required for instantiation of
wenzelm@23152
    33
     the adm_subst theorem (see functions mk_term, inst_adm_subst_thm))
wenzelm@23152
    34
***)
wenzelm@23152
    35
wenzelm@23152
    36
fun find_subterms (Bound i) lev path =
wenzelm@23152
    37
      if i = lev then [[(Bound 0, path)]]
wenzelm@23152
    38
      else []
wenzelm@23152
    39
  | find_subterms (t as (Abs (_, _, t2))) lev path =
wenzelm@29355
    40
      if filter (fn x => x <= lev) (add_loose_bnos (t, 0, [])) = [lev]
wenzelm@29355
    41
      then
wenzelm@29355
    42
        [(incr_bv (~lev, 0, t), path)] ::
wenzelm@23152
    43
        (find_subterms t2 (lev+1) (0::path))
wenzelm@23152
    44
      else find_subterms t2 (lev+1) (0::path)
wenzelm@23152
    45
  | find_subterms (t as (t1 $ t2)) lev path =
wenzelm@23152
    46
      let val ts1 = find_subterms t1 lev (0::path);
wenzelm@23152
    47
          val ts2 = find_subterms t2 lev (1::path);
wenzelm@23152
    48
          fun combine [] y = []
wenzelm@29355
    49
            | combine (x::xs) ys = map (fn z => x @ z) ys @ combine xs ys
wenzelm@23152
    50
      in
wenzelm@29355
    51
        (if filter (fn x => x <= lev) (add_loose_bnos (t, 0, [])) = [lev]
wenzelm@29355
    52
         then [[(incr_bv (~lev, 0, t), path)]]
wenzelm@23152
    53
         else []) @
wenzelm@23152
    54
        (if ts1 = [] then ts2
wenzelm@23152
    55
         else if ts2 = [] then ts1
wenzelm@23152
    56
         else combine ts1 ts2)
wenzelm@23152
    57
      end
wenzelm@23152
    58
  | find_subterms _ _ _ = [];
wenzelm@23152
    59
wenzelm@23152
    60
wenzelm@23152
    61
(*** make term for instantiation of predicate "P" in adm_subst theorem ***)
wenzelm@23152
    62
wenzelm@23152
    63
fun make_term t path paths lev =
wenzelm@29355
    64
  if member (op =) paths path then Bound lev
wenzelm@23152
    65
  else case t of
wenzelm@23152
    66
      (Abs (s, T, t1)) => Abs (s, T, make_term t1 (0::path) paths (lev+1))
wenzelm@23152
    67
    | (t1 $ t2) => (make_term t1 (0::path) paths lev) $
wenzelm@23152
    68
                   (make_term t2 (1::path) paths lev)
wenzelm@23152
    69
    | t1 => t1;
wenzelm@23152
    70
wenzelm@23152
    71
wenzelm@23152
    72
(*** check whether all terms in list are equal ***)
wenzelm@23152
    73
wenzelm@23152
    74
fun eq_terms [] = true
wenzelm@23152
    75
  | eq_terms (ts as (t, _) :: _) = forall (fn (t2, _) => t2 aconv t) ts;
wenzelm@23152
    76
wenzelm@23152
    77
wenzelm@23152
    78
(*** check whether type of terms in list is chain finite ***)
wenzelm@23152
    79
wenzelm@29355
    80
fun is_chfin thy T params ((t, _)::_) =
wenzelm@23152
    81
  let val parTs = map snd (rev params)
wenzelm@29355
    82
  in Sign.of_sort thy (fastype_of1 (T::parTs, t), @{sort "{chfin,pcpo}"}) end;
wenzelm@23152
    83
wenzelm@23152
    84
wenzelm@23152
    85
(*** try to prove that terms in list are continuous
wenzelm@23152
    86
     if successful, add continuity theorem to list l ***)
wenzelm@23152
    87
wenzelm@30603
    88
fun prove_cont ctxt tac s T prems params (ts as ((t, _)::_)) l =  (* FIXME proper context *)
wenzelm@23152
    89
  let val parTs = map snd (rev params);
wenzelm@23152
    90
       val contT = (T --> (fastype_of1 (T::parTs, t))) --> HOLogic.boolT;
wenzelm@23152
    91
       fun mk_all [] t = t
wenzelm@27331
    92
         | mk_all ((a,T)::Ts) t = Term.all T $ (Abs (a, T, mk_all Ts t));
wenzelm@29355
    93
       val t = HOLogic.mk_Trueprop (Const (@{const_name cont}, contT) $ Abs (s, T, t));
wenzelm@23152
    94
       val t' = mk_all params (Logic.list_implies (prems, t));
wenzelm@30603
    95
       val thm = Goal.prove ctxt [] [] t' (K (tac 1));
wenzelm@23152
    96
  in (ts, thm)::l end
wenzelm@23152
    97
  handle ERROR _ => l;
wenzelm@23152
    98
wenzelm@23152
    99
wenzelm@23152
   100
(*** instantiation of adm_subst theorem (a bit tricky) ***)
wenzelm@23152
   101
wenzelm@23152
   102
fun inst_adm_subst_thm state i params s T subt t paths =
wenzelm@26626
   103
  let
wenzelm@29355
   104
    val thy = Thm.theory_of_thm state;
wenzelm@29355
   105
    val j = Thm.maxidx_of state + 1;
wenzelm@29355
   106
    val parTs = map snd (rev params);
wenzelm@29355
   107
    val rule = Thm.lift_rule (Thm.cprem_of state i) @{thm adm_subst};
wenzelm@29355
   108
    val types = the o fst (Drule.types_sorts rule);
wenzelm@29355
   109
    val tT = types ("t", j);
wenzelm@29355
   110
    val PT = types ("P", j);
wenzelm@29355
   111
    fun mk_abs [] t = t
wenzelm@29355
   112
      | mk_abs ((a,T)::Ts) t = Abs (a, T, mk_abs Ts t);
wenzelm@29355
   113
    val tt = cterm_of thy (mk_abs (params @ [(s, T)]) subt);
wenzelm@29355
   114
    val Pt = cterm_of thy (mk_abs (params @ [(s, fastype_of1 (T::parTs, subt))])
wenzelm@29355
   115
                   (make_term t [] paths 0));
wenzelm@29355
   116
    val tye = Sign.typ_match thy (tT, #T (rep_cterm tt)) Vartab.empty;
wenzelm@29355
   117
    val tye' = Sign.typ_match thy (PT, #T (rep_cterm Pt)) tye;
wenzelm@29355
   118
    val ctye = map (fn (ixn, (S, T)) =>
wenzelm@29355
   119
      (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)) (Vartab.dest tye');
wenzelm@32035
   120
    val tv = cterm_of thy (Var (("t", j), Envir.subst_type tye' tT));
wenzelm@32035
   121
    val Pv = cterm_of thy (Var (("P", j), Envir.subst_type tye' PT));
wenzelm@29355
   122
    val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule
wenzelm@23152
   123
  in rule' end;
wenzelm@23152
   124
wenzelm@23152
   125
wenzelm@23152
   126
(*** the admissibility tactic ***)
wenzelm@23152
   127
wenzelm@29355
   128
fun try_dest_adm (Const _ $ (Const (@{const_name adm}, _) $ Abs abs)) = SOME abs
wenzelm@23152
   129
  | try_dest_adm _ = NONE;
wenzelm@23152
   130
wenzelm@30603
   131
fun adm_tac ctxt tac i state = (i, state) |-> SUBGOAL (fn (goali, _) =>
wenzelm@29355
   132
  (case try_dest_adm (Logic.strip_assums_concl goali) of
wenzelm@29355
   133
    NONE => no_tac
wenzelm@29355
   134
  | SOME (s, T, t) =>
wenzelm@29355
   135
      let
wenzelm@30603
   136
        val thy = ProofContext.theory_of ctxt;
wenzelm@29355
   137
        val prems = Logic.strip_assums_hyp goali;
wenzelm@29355
   138
        val params = Logic.strip_params goali;
wenzelm@29355
   139
        val ts = find_subterms t 0 [];
wenzelm@29355
   140
        val ts' = filter eq_terms ts;
wenzelm@29355
   141
        val ts'' = filter (is_chfin thy T params) ts';
wenzelm@30603
   142
        val thms = fold (prove_cont ctxt tac s T prems params) ts'' [];
wenzelm@29355
   143
      in
wenzelm@29355
   144
        (case thms of
wenzelm@29355
   145
          ((ts as ((t', _)::_), cont_thm) :: _) =>
wenzelm@29355
   146
            let
wenzelm@29355
   147
              val paths = map snd ts;
wenzelm@29355
   148
              val rule = inst_adm_subst_thm state i params s T t' t paths;
wenzelm@29355
   149
            in
wenzelm@29355
   150
              compose_tac (false, rule, 2) i THEN
wenzelm@29355
   151
              resolve_tac [cont_thm] i THEN
wenzelm@29355
   152
              REPEAT (assume_tac i) THEN
wenzelm@29355
   153
              resolve_tac [@{thm adm_chfin}] i
wenzelm@29355
   154
            end
wenzelm@29355
   155
        | [] => no_tac)
wenzelm@29355
   156
      end));
wenzelm@23152
   157
wenzelm@23152
   158
end;
wenzelm@23152
   159