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