src/HOLCF/Tools/adm_tac.ML

+(*  ID:         $Id$
+    Author:     Stefan Berghofer, TU Muenchen
+
+Admissibility tactic.
+
+Checks whether adm_subst theorem is applicable to the current proof
+state:
+
+  [| cont t; adm P |] ==> adm (%x. P (t x))
+
+"t" is instantiated with a term of chain-finite type, so that
+adm_chfin can be applied:
+
+  adm (P::'a::{chfin,pcpo} => bool)
+
+*)
+
+signature ADM =
+sig
+  val adm_tac: (int -> tactic) -> int -> tactic
+end;
+
+structure Adm: ADM =
+struct
+
+
+(*** find_subterms t 0 []
+     returns lists of terms with the following properties:
+       1. all terms in the list are disjoint subterms of t
+       2. all terms contain the variable which is bound at level 0
+       3. all occurences of the variable which is bound at level 0
+          are "covered" by a term in the list
+     a list of integers is associated with every term which describes
+     the "path" leading to the subterm (required for instantiation of
+     the adm_subst theorem (see functions mk_term, inst_adm_subst_thm))
+***)
+
+fun find_subterms (Bound i) lev path =
+      if i = lev then [[(Bound 0, path)]]
+      else []
+  | find_subterms (t as (Abs (_, _, t2))) lev path =
+      if List.filter (fn x => x<=lev)
+           (add_loose_bnos (t, 0, [])) = [lev] then
+        [(incr_bv (~lev, 0, t), path)]::
+        (find_subterms t2 (lev+1) (0::path))
+      else find_subterms t2 (lev+1) (0::path)
+  | find_subterms (t as (t1 $ t2)) lev path =
+      let val ts1 = find_subterms t1 lev (0::path);
+          val ts2 = find_subterms t2 lev (1::path);
+          fun combine [] y = []
+            | combine (x::xs) ys =
+                (map (fn z => x @ z) ys) @ (combine xs ys)
+      in
+        (if List.filter (fn x => x<=lev)
+              (add_loose_bnos (t, 0, [])) = [lev] then
+           [[(incr_bv (~lev, 0, t), path)]]
+         else []) @
+        (if ts1 = [] then ts2
+         else if ts2 = [] then ts1
+         else combine ts1 ts2)
+      end
+  | find_subterms _ _ _ = [];
+
+
+(*** make term for instantiation of predicate "P" in adm_subst theorem ***)
+
+fun make_term t path paths lev =
+  if path mem paths then Bound lev
+  else case t of
+      (Abs (s, T, t1)) => Abs (s, T, make_term t1 (0::path) paths (lev+1))
+    | (t1 $ t2) => (make_term t1 (0::path) paths lev) $
+                   (make_term t2 (1::path) paths lev)
+    | t1 => t1;
+
+
+(*** check whether all terms in list are equal ***)
+
+fun eq_terms [] = true
+  | eq_terms (ts as (t, _) :: _) = forall (fn (t2, _) => t2 aconv t) ts;
+
+
+(*figure out internal names*)
+val chfin_pcpoS = Sign.intern_sort (the_context ()) ["chfin", "pcpo"];
+val cont_name = Sign.intern_const (the_context ()) "cont";
+val adm_name = Sign.intern_const (the_context ()) "adm";
+
+
+(*** check whether type of terms in list is chain finite ***)
+
+fun is_chfin sign T params ((t, _)::_) =
+  let val parTs = map snd (rev params)
+  in Sign.of_sort sign (fastype_of1 (T::parTs, t), chfin_pcpoS) end;
+
+
+(*** try to prove that terms in list are continuous
+     if successful, add continuity theorem to list l ***)
+
+fun prove_cont tac sign s T prems params (l, ts as ((t, _)::_)) =
+  let val parTs = map snd (rev params);
+       val contT = (T --> (fastype_of1 (T::parTs, t))) --> HOLogic.boolT;
+       fun mk_all [] t = t
+         | mk_all ((a,T)::Ts) t = (all T) $ (Abs (a, T, mk_all Ts t));
+       val t = HOLogic.mk_Trueprop((Const (cont_name, contT)) $ (Abs(s, T, t)));
+       val t' = mk_all params (Logic.list_implies (prems, t));
+       val thm = Goal.prove (ProofContext.init sign) [] [] t' (K (tac 1));
+  in (ts, thm)::l end
+  handle ERROR _ => l;
+
+
+(*** instantiation of adm_subst theorem (a bit tricky) ***)
+
+fun inst_adm_subst_thm state i params s T subt t paths =
+  let val {thy = sign, maxidx, ...} = rep_thm state;
+      val j = maxidx+1;
+      val parTs = map snd (rev params);
+      val rule = Thm.lift_rule (Thm.cprem_of state i) adm_subst;
+      val types = valOf o (fst (types_sorts rule));
+      val tT = types ("t", j);
+      val PT = types ("P", j);
+      fun mk_abs [] t = t
+        | mk_abs ((a,T)::Ts) t = Abs (a, T, mk_abs Ts t);
+      val tt = cterm_of sign (mk_abs (params @ [(s, T)]) subt);
+      val Pt = cterm_of sign (mk_abs (params @ [(s, fastype_of1 (T::parTs, subt))])
+                     (make_term t [] paths 0));
+      val tye = Sign.typ_match sign (tT, #T (rep_cterm tt)) Vartab.empty;
+      val tye' = Sign.typ_match sign (PT, #T (rep_cterm Pt)) tye;
+      val ctye = map (fn (ixn, (S, T)) =>
+        (ctyp_of sign (TVar (ixn, S)), ctyp_of sign T)) (Vartab.dest tye');
+      val tv = cterm_of sign (Var (("t", j), Envir.typ_subst_TVars tye' tT));
+      val Pv = cterm_of sign (Var (("P", j), Envir.typ_subst_TVars tye' PT));
+      val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule
+  in rule' end;
+
+
+(*** extract subgoal i from proof state ***)
+
+fun nth_subgoal i thm = List.nth (prems_of thm, i-1);
+
+
+(*** the admissibility tactic ***)
+
+fun try_dest_adm (Const _ $ (Const (name, _) $ Abs abs)) =
+      if name = adm_name then SOME abs else NONE
+  | try_dest_adm _ = NONE;
+
+fun adm_tac tac i state =
+  state |>
+  let val goali = nth_subgoal i state in
+    (case try_dest_adm (Logic.strip_assums_concl goali) of
+      NONE => no_tac
+    | SOME (s, T, t) =>
+        let
+          val sign = Thm.theory_of_thm state;
+          val prems = Logic.strip_assums_hyp goali;
+          val params = Logic.strip_params goali;
+          val ts = find_subterms t 0 [];
+          val ts' = List.filter eq_terms ts;
+          val ts'' = List.filter (is_chfin sign T params) ts';
+          val thms = Library.foldl (prove_cont tac sign s T prems params) ([], ts'');
+        in
+          (case thms of
+            ((ts as ((t', _)::_), cont_thm)::_) =>
+              let
+                val paths = map snd ts;
+                val rule = inst_adm_subst_thm state i params s T t' t paths;
+              in
+                compose_tac (false, rule, 2) i THEN
+                rtac cont_thm i THEN
+                REPEAT (assume_tac i) THEN
+                rtac adm_chfin i
+              end 
+          | [] => no_tac)
+        end)
+    end;
+
+
+end;
+
+
+open Adm;