cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
--- a/src/HOLCF/Adm.ML Tue May 24 10:23:24 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-
-(* legacy ML bindings *)
-
-val adm_def = thm "adm_def";
-val admI = thm "admI";
-val triv_admI = thm "triv_admI";
-val admD = thm "admD";
-val adm_max_in_chain = thm "adm_max_in_chain";
-val adm_chfin = thm "adm_chfin";
-val adm_chfindom = thm "adm_chfindom";
-val admI2 = thm "admI2";
-val adm_less = thm "adm_less";
-val adm_conj = thm "adm_conj";
-val adm_not_free = thm "adm_not_free";
-val adm_not_less = thm "adm_not_less";
-val adm_all = thm "adm_all";
-val adm_all2 = thm "adm_all2";
-val adm_subst = thm "adm_subst";
-val adm_UU_not_less = thm "adm_UU_not_less";
-val adm_not_UU = thm "adm_not_UU";
-val adm_eq = thm "adm_eq";
-val adm_disj_lemma1 = thm "adm_disj_lemma1";
-val adm_disj_lemma2 = thm "adm_disj_lemma2";
-val adm_disj_lemma3 = thm "adm_disj_lemma3";
-val adm_disj_lemma4 = thm "adm_disj_lemma4";
-val adm_disj_lemma5 = thm "adm_disj_lemma5";
-val adm_disj_lemma6 = thm "adm_disj_lemma6";
-val adm_disj_lemma7 = thm "adm_disj_lemma7";
-val adm_disj = thm "adm_disj";
-val adm_imp = thm "adm_imp";
-val adm_iff = thm "adm_iff";
-val adm_not_conj = thm "adm_not_conj";
-val adm_lemmas = [adm_not_free, adm_imp, adm_disj, adm_eq, adm_not_UU,
- adm_UU_not_less, adm_all2, adm_not_less, adm_not_conj, adm_iff]
--- a/src/HOLCF/Adm.thy Tue May 24 10:23:24 2005 +0200
+++ b/src/HOLCF/Adm.thy Tue May 24 10:55:11 2005 +0200
@@ -260,5 +260,41 @@
declare adm_lemmas [simp]
+(* legacy ML bindings *)
+ML
+{*
+val adm_def = thm "adm_def";
+val admI = thm "admI";
+val triv_admI = thm "triv_admI";
+val admD = thm "admD";
+val adm_max_in_chain = thm "adm_max_in_chain";
+val adm_chfin = thm "adm_chfin";
+val adm_chfindom = thm "adm_chfindom";
+val admI2 = thm "admI2";
+val adm_less = thm "adm_less";
+val adm_conj = thm "adm_conj";
+val adm_not_free = thm "adm_not_free";
+val adm_not_less = thm "adm_not_less";
+val adm_all = thm "adm_all";
+val adm_all2 = thm "adm_all2";
+val adm_subst = thm "adm_subst";
+val adm_UU_not_less = thm "adm_UU_not_less";
+val adm_not_UU = thm "adm_not_UU";
+val adm_eq = thm "adm_eq";
+val adm_disj_lemma1 = thm "adm_disj_lemma1";
+val adm_disj_lemma2 = thm "adm_disj_lemma2";
+val adm_disj_lemma3 = thm "adm_disj_lemma3";
+val adm_disj_lemma4 = thm "adm_disj_lemma4";
+val adm_disj_lemma5 = thm "adm_disj_lemma5";
+val adm_disj_lemma6 = thm "adm_disj_lemma6";
+val adm_disj_lemma7 = thm "adm_disj_lemma7";
+val adm_disj = thm "adm_disj";
+val adm_imp = thm "adm_imp";
+val adm_iff = thm "adm_iff";
+val adm_not_conj = thm "adm_not_conj";
+val adm_lemmas = [adm_not_free, adm_imp, adm_disj, adm_eq, adm_not_UU,
+ adm_UU_not_less, adm_all2, adm_not_less, adm_not_conj, adm_iff]
+*}
+
end
--- a/src/HOLCF/HOLCF.ML Tue May 24 10:23:24 2005 +0200
+++ b/src/HOLCF/HOLCF.ML Tue May 24 10:55:11 2005 +0200
@@ -8,7 +8,7 @@
val thy = the_context ();
end;
-use"adm.ML";
+use "adm_tac.ML";
simpset_ref() := simpset() addSolver
(mk_solver "adm_tac" (fn thms => (adm_tac (cut_facts_tac thms THEN' cont_tacRs))));
--- a/src/HOLCF/IsaMakefile Tue May 24 10:23:24 2005 +0200
+++ b/src/HOLCF/IsaMakefile Tue May 24 10:55:11 2005 +0200
@@ -27,7 +27,7 @@
HOL:
@cd $(SRC)/HOL; $(ISATOOL) make HOL
-$(OUT)/HOLCF: $(OUT)/HOL Adm.ML Adm.thy Cfun.ML Cfun.thy \
+$(OUT)/HOLCF: $(OUT)/HOL Adm.thy Cfun.ML Cfun.thy \
Cont.ML Cont.thy Cprod.ML Cprod.thy \
Discrete.thy Domain.thy Fix.ML Fix.thy FunCpo.ML \
FunCpo.thy HOLCF.ML HOLCF.thy Lift.ML \
@@ -35,7 +35,7 @@
ROOT.ML Sprod.ML Sprod.thy \
Ssum.ML Ssum.thy \
Tr.ML Tr.thy TypedefPcpo.thy Up.ML \
- Up.thy adm.ML cont_consts.ML \
+ Up.thy adm_tac.ML cont_consts.ML \
domain/axioms.ML domain/extender.ML domain/interface.ML \
domain/library.ML domain/syntax.ML domain/theorems.ML holcf_logic.ML \
ex/Stream.thy document/root.tex
--- a/src/HOLCF/adm.ML Tue May 24 10:23:24 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,182 +0,0 @@
-(* Title: HOLCF/adm.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 (sign_of HOLCF.thy) ["chfin", "pcpo"];
-val cont_name = Sign.intern_const (sign_of HOLCF.thy) "cont";
-val adm_name = Sign.intern_const (sign_of HOLCF.thy) "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 = Tactic.prove sign [] [] t' (K (tac 1));
- in (ts, thm)::l end
- handle ERROR_MESSAGE _ => l;
-
-
-(*** instantiation of adm_subst theorem (a bit tricky) ***)
-
-fun inst_adm_subst_thm state i params s T subt t paths =
- let val {sign, maxidx, ...} = rep_thm state;
- val j = maxidx+1;
- val tsig = Sign.tsig_of sign;
- val parTs = map snd (rev params);
- val rule = lift_rule (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 = Type.typ_match tsig (Vartab.empty, (tT, #T (rep_cterm tt)));
- val tye' = Type.typ_match tsig (tye, (PT, #T (rep_cterm Pt)));
- 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 = sign_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;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/adm_tac.ML Tue May 24 10:55:11 2005 +0200
@@ -0,0 +1,181 @@
+(* 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 (sign_of HOLCF.thy) ["chfin", "pcpo"];
+val cont_name = Sign.intern_const (sign_of HOLCF.thy) "cont";
+val adm_name = Sign.intern_const (sign_of HOLCF.thy) "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 = Tactic.prove sign [] [] t' (K (tac 1));
+ in (ts, thm)::l end
+ handle ERROR_MESSAGE _ => l;
+
+
+(*** instantiation of adm_subst theorem (a bit tricky) ***)
+
+fun inst_adm_subst_thm state i params s T subt t paths =
+ let val {sign, maxidx, ...} = rep_thm state;
+ val j = maxidx+1;
+ val tsig = Sign.tsig_of sign;
+ val parTs = map snd (rev params);
+ val rule = lift_rule (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 = Type.typ_match tsig (Vartab.empty, (tT, #T (rep_cterm tt)));
+ val tye' = Type.typ_match tsig (tye, (PT, #T (rep_cterm Pt)));
+ 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 = sign_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;