# HG changeset patch # User wenzelm # Date 1231175606 -3600 # Node ID 642cac18e155add9a94bd6a1bf75632f865dc79d # Parent 6ef5ddf22d3a59e0c1a5514546d9dca5ea61b3fd misc tuning and modernization; diff -r 6ef5ddf22d3a -r 642cac18e155 src/HOLCF/HOLCF.thy --- a/src/HOLCF/HOLCF.thy Mon Jan 05 07:54:16 2009 -0800 +++ b/src/HOLCF/HOLCF.thy Mon Jan 05 18:13:26 2009 +0100 @@ -24,7 +24,7 @@ declaration {* fn _ => Simplifier.map_ss (fn simpset => simpset addSolver (mk_solver' "adm_tac" (fn ss => - adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss)))); + Adm.adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss)))); *} end diff -r 6ef5ddf22d3a -r 642cac18e155 src/HOLCF/Tools/adm_tac.ML --- a/src/HOLCF/Tools/adm_tac.ML Mon Jan 05 07:54:16 2009 -0800 +++ b/src/HOLCF/Tools/adm_tac.ML Mon Jan 05 18:13:26 2009 +0100 @@ -1,18 +1,16 @@ -(* ID: $Id$ - Author: Stefan Berghofer, TU Muenchen +(* 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)) + 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 = @@ -39,21 +37,19 @@ 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)]:: + if 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) + | 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)]] + (if 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 @@ -65,7 +61,7 @@ (*** 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 + if member (op =) paths path 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) $ @@ -79,30 +75,24 @@ | 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, _)::_) = +fun is_chfin thy T params ((t, _)::_) = let val parTs = map snd (rev params) - in Sign.of_sort sign (fastype_of1 (T::parTs, t), chfin_pcpoS) end; + in Sign.of_sort thy (fastype_of1 (T::parTs, t), @{sort "{chfin,pcpo}"}) 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, _)::_)) = +fun prove_cont tac thy s T prems params (ts as ((t, _)::_)) l = 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 = Term.all T $ (Abs (a, T, mk_all Ts t)); - val t = HOLogic.mk_Trueprop((Const (cont_name, contT)) $ (Abs(s, T, t))); + val t = HOLogic.mk_Trueprop (Const (@{const_name cont}, 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)); + val thm = Goal.prove (ProofContext.init thy) [] [] t' (K (tac 1)); in (ts, thm)::l end handle ERROR _ => l; @@ -111,71 +101,59 @@ fun inst_adm_subst_thm state i params s T subt t paths = let - val sign = Thm.theory_of_thm state; - val j = Thm.maxidx_of state + 1; - val parTs = map snd (rev params); - val rule = Thm.lift_rule (Thm.cprem_of state i) @{thm adm_subst}; - val types = valOf o (fst (Drule.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 + val thy = Thm.theory_of_thm state; + val j = Thm.maxidx_of state + 1; + val parTs = map snd (rev params); + val rule = Thm.lift_rule (Thm.cprem_of state i) @{thm adm_subst}; + val types = the o fst (Drule.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 thy (mk_abs (params @ [(s, T)]) subt); + val Pt = cterm_of thy (mk_abs (params @ [(s, fastype_of1 (T::parTs, subt))]) + (make_term t [] paths 0)); + val tye = Sign.typ_match thy (tT, #T (rep_cterm tt)) Vartab.empty; + val tye' = Sign.typ_match thy (PT, #T (rep_cterm Pt)) tye; + val ctye = map (fn (ixn, (S, T)) => + (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)) (Vartab.dest tye'); + val tv = cterm_of thy (Var (("t", j), Envir.typ_subst_TVars tye' tT)); + val Pv = cterm_of thy (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 +fun try_dest_adm (Const _ $ (Const (@{const_name adm}, _) $ Abs abs)) = SOME abs | 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 @{thm adm_chfin} i - end - | [] => no_tac) - end) - end; - +fun adm_tac tac i state = (i, state) |-> SUBGOAL (fn (goali, _) => + (case try_dest_adm (Logic.strip_assums_concl goali) of + NONE => no_tac + | SOME (s, T, t) => + let + val thy = 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' = filter eq_terms ts; + val ts'' = filter (is_chfin thy T params) ts'; + val thms = fold (prove_cont tac thy 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 + resolve_tac [cont_thm] i THEN + REPEAT (assume_tac i) THEN + resolve_tac [@{thm adm_chfin}] i + end + | [] => no_tac) + end)); end; - -open Adm;