--- a/src/HOLCF/HOLCF.thy Mon Mar 22 23:20:55 2010 +0100
+++ b/src/HOLCF/HOLCF.thy Mon Mar 22 23:48:27 2010 +0100
@@ -10,20 +10,10 @@
Domain
Powerdomains
Sum_Cpo
-uses
- "holcf_logic.ML"
- "Tools/adm_tac.ML"
begin
defaultsort pcpo
-declaration {* fn _ =>
- Simplifier.map_ss (fn simpset => simpset addSolver
- (mk_solver' "adm_tac" (fn ss =>
- Adm.adm_tac (Simplifier.the_context ss)
- (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
-*}
-
text {* Legacy theorem names *}
lemmas sq_ord_less_eq_trans = below_eq_trans
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Mon Mar 22 23:20:55 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Mon Mar 22 23:48:27 2010 +0100
@@ -814,9 +814,8 @@
lemma nForall_HDFilter:
"~Forall P y --> (? x. HD$(Filter (%a. ~P a)$y) = Def x)"
-(* Pay attention: is only admissible with chain-finite package to be added to
- adm test *)
-apply (rule_tac x="y" in Seq_induct)
+unfolding not_Undef_is_Def [symmetric]
+apply (induct y rule: Seq_induct)
apply (simp add: Forall_def sforall_def)
apply simp_all
done
--- a/src/HOLCF/IsaMakefile Mon Mar 22 23:20:55 2010 +0100
+++ b/src/HOLCF/IsaMakefile Mon Mar 22 23:48:27 2010 +0100
@@ -61,7 +61,6 @@
Universal.thy \
UpperPD.thy \
Up.thy \
- Tools/adm_tac.ML \
Tools/cont_consts.ML \
Tools/cont_proc.ML \
Tools/holcf_library.ML \
@@ -75,7 +74,6 @@
Tools/fixrec.ML \
Tools/pcpodef.ML \
Tools/repdef.ML \
- holcf_logic.ML \
document/root.tex
@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
--- a/src/HOLCF/Tools/adm_tac.ML Mon Mar 22 23:20:55 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,160 +0,0 @@
-(* Title: HOLCF/Tools/adm_tac.ML
- 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: Proof.context -> (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 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 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 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) $
- (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;
-
-
-(*** check whether type of terms in list is chain finite ***)
-
-fun is_chfin thy T params ((t, _)::_) =
- let val parTs = map snd (rev params)
- 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 ctxt tac s T prems params (ts as ((t, _)::_)) l = (* FIXME proper context *)
- 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 (@{const_name cont}, contT) $ Abs (s, T, t));
- val t' = mk_all params (Logic.list_implies (prems, t));
- val thm = Goal.prove ctxt [] [] 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 = 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.subst_type tye' tT));
- val Pv = cterm_of thy (Var (("P", j), Envir.subst_type tye' PT));
- val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule
- in rule' end;
-
-
-(*** the admissibility tactic ***)
-
-fun try_dest_adm (Const _ $ (Const (@{const_name adm}, _) $ Abs abs)) = SOME abs
- | try_dest_adm _ = NONE;
-
-fun adm_tac ctxt 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 = ProofContext.theory_of ctxt;
- 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 ctxt tac 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;
-
--- a/src/HOLCF/Tools/holcf_library.ML Mon Mar 22 23:20:55 2010 +0100
+++ b/src/HOLCF/Tools/holcf_library.ML Mon Mar 22 23:48:27 2010 +0100
@@ -62,7 +62,6 @@
(*** Continuous function space ***)
-(* ->> is taken from holcf_logic.ML *)
fun mk_cfunT (T, U) = Type(@{type_name cfun}, [T, U]);
val (op ->>) = mk_cfunT;
--- a/src/HOLCF/holcf_logic.ML Mon Mar 22 23:20:55 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-(* Title: HOLCF/holcf_logic.ML
- Author: David von Oheimb
-
-Abstract syntax operations for HOLCF.
-*)
-
-infixr 6 ->>;
-
-signature HOLCF_LOGIC =
-sig
- val mk_btyp: string -> typ * typ -> typ
- val pcpoS: sort
- val mk_TFree: string -> typ
- val cfun_arrow: string
- val ->> : typ * typ -> typ
- val mk_ssumT: typ * typ -> typ
- val mk_sprodT: typ * typ -> typ
- val mk_uT: typ -> typ
- val trT: typ
- val oneT: typ
-end;
-
-structure HOLCFLogic: HOLCF_LOGIC =
-struct
-
-(* sort pcpo *)
-
-val pcpoS = @{sort pcpo};
-fun mk_TFree s = TFree ("'" ^ s, pcpoS);
-
-
-(* basic types *)
-
-fun mk_btyp t (S, T) = Type (t, [S, T]);
-
-val cfun_arrow = @{type_name "cfun"};
-val op ->> = mk_btyp cfun_arrow;
-val mk_ssumT = mk_btyp (@{type_name "ssum"});
-val mk_sprodT = mk_btyp (@{type_name "sprod"});
-fun mk_uT T = Type (@{type_name u}, [T]);
-val trT = @{typ tr};
-val oneT = @{typ one};
-
-end;