--- a/src/HOLCF/Cfun.thy Thu May 31 13:24:13 2007 +0200
+++ b/src/HOLCF/Cfun.thy Thu May 31 14:01:58 2007 +0200
@@ -9,7 +9,7 @@
theory Cfun
imports Pcpodef
-uses ("cont_proc.ML")
+uses ("Tools/cont_proc.ML")
begin
defaultsort cpo
@@ -325,7 +325,7 @@
lemmas cont_lemmas1 =
cont_const cont_id cont_Rep_CFun2 cont2cont_Rep_CFun cont2cont_LAM
-use "cont_proc.ML";
+use "Tools/cont_proc.ML";
setup ContProc.setup;
(*val cont_tac = (fn i => (resolve_tac cont_lemmas i));*)
--- a/src/HOLCF/Domain.thy Thu May 31 13:24:13 2007 +0200
+++ b/src/HOLCF/Domain.thy Thu May 31 14:01:58 2007 +0200
@@ -7,15 +7,6 @@
theory Domain
imports Ssum Sprod Up One Tr Fixrec
-(*
-files
- ("domain/library.ML")
- ("domain/syntax.ML")
- ("domain/axioms.ML")
- ("domain/theorems.ML")
- ("domain/extender.ML")
- ("domain/interface.ML")
-*)
begin
defaultsort pcpo
--- a/src/HOLCF/Fixrec.thy Thu May 31 13:24:13 2007 +0200
+++ b/src/HOLCF/Fixrec.thy Thu May 31 14:01:58 2007 +0200
@@ -7,7 +7,7 @@
theory Fixrec
imports Sprod Ssum Up One Tr Fix
-uses ("fixrec_package.ML")
+uses ("Tools/fixrec_package.ML")
begin
subsection {* Maybe monad type *}
@@ -542,7 +542,7 @@
subsection {* Initializing the fixrec package *}
-use "fixrec_package.ML"
+use "Tools/fixrec_package.ML"
hide (open) const return bind fail run
--- a/src/HOLCF/HOLCF.thy Thu May 31 13:24:13 2007 +0200
+++ b/src/HOLCF/HOLCF.thy Thu May 31 14:01:58 2007 +0200
@@ -9,13 +9,13 @@
imports Sprod Ssum Up Lift Discrete One Tr Domain Main
uses
"holcf_logic.ML"
- "cont_consts.ML"
- "domain/library.ML"
- "domain/syntax.ML"
- "domain/axioms.ML"
- "domain/theorems.ML"
- "domain/extender.ML"
- "adm_tac.ML"
+ "Tools/cont_consts.ML"
+ "Tools/domain/domain_library.ML"
+ "Tools/domain/domain_syntax.ML"
+ "Tools/domain/domain_axioms.ML"
+ "Tools/domain/domain_theorems.ML"
+ "Tools/domain/domain_extender.ML"
+ "Tools/adm_tac.ML"
begin
--- a/src/HOLCF/IsaMakefile Thu May 31 13:24:13 2007 +0200
+++ b/src/HOLCF/IsaMakefile Thu May 31 14:01:58 2007 +0200
@@ -27,15 +27,15 @@
HOL:
@cd $(SRC)/HOL; $(ISATOOL) make HOL
-$(OUT)/HOLCF: $(OUT)/HOL Adm.thy Cfun.thy Cont.thy \
- Cprod.thy Discrete.thy Domain.thy Fix.thy Fixrec.thy \
- Ffun.thy HOLCF.thy Lift.thy One.thy \
- Pcpo.thy Porder.thy ROOT.ML Sprod.thy \
- Ssum.thy Tr.thy Pcpodef.thy pcpodef_package.ML \
- Up.thy adm_tac.ML cont_consts.ML cont_proc.ML fixrec_package.ML \
- domain/axioms.ML domain/extender.ML domain/library.ML \
- domain/syntax.ML domain/theorems.ML holcf_logic.ML ex/Stream.thy \
- document/root.tex
+$(OUT)/HOLCF: $(OUT)/HOL Adm.thy Cfun.thy Cont.thy Cprod.thy \
+ Discrete.thy Domain.thy Ffun.thy Fix.thy Fixrec.thy HOLCF.thy Lift.thy \
+ One.thy Pcpo.thy Pcpodef.thy Porder.thy ROOT.ML Sprod.thy Ssum.thy \
+ Tools/adm_tac.ML Tools/cont_consts.ML Tools/cont_proc.ML \
+ Tools/domain/domain_extender.ML Tools/domain/domain_axioms.ML \
+ Tools/domain/domain_library.ML Tools/domain/domain_syntax.ML \
+ Tools/domain/domain_theorems.ML Tools/fixrec_package.ML \
+ Tools/pcpodef_package.ML Tr.thy Up.thy document/root.tex ex/Stream.thy \
+ holcf_logic.ML
@$(ISATOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
--- a/src/HOLCF/Pcpodef.thy Thu May 31 13:24:13 2007 +0200
+++ b/src/HOLCF/Pcpodef.thy Thu May 31 14:01:58 2007 +0200
@@ -7,7 +7,7 @@
theory Pcpodef
imports Adm
-uses ("pcpodef_package.ML")
+uses ("Tools/pcpodef_package.ML")
begin
subsection {* Proving a subtype is a partial order *}
@@ -266,6 +266,6 @@
subsection {* HOLCF type definition package *}
-use "pcpodef_package.ML"
+use "Tools/pcpodef_package.ML"
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/adm_tac.ML Thu May 31 14:01:58 2007 +0200
@@ -0,0 +1,180 @@
+(* 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;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/cont_consts.ML Thu May 31 14:01:58 2007 +0200
@@ -0,0 +1,110 @@
+(* Title: HOLCF/Tools/cont_consts.ML
+ ID: $Id$
+ Author: Tobias Mayr, David von Oheimb, and Markus Wenzel
+
+HOLCF version of consts: handle continuous function types in mixfix
+syntax.
+*)
+
+signature CONT_CONSTS =
+sig
+ val add_consts: (bstring * string * mixfix) list -> theory -> theory
+ val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
+end;
+
+structure ContConsts: CONT_CONSTS =
+struct
+
+
+(* misc utils *)
+
+open HOLCFLogic;
+
+fun first (x,_,_) = x;
+fun second (_,x,_) = x;
+fun third (_,_,x) = x;
+fun upd_first f (x,y,z) = (f x, y, z);
+fun upd_second f (x,y,z) = ( x, f y, z);
+fun upd_third f (x,y,z) = ( x, y, f z);
+
+fun change_arrow 0 T = T
+| change_arrow n (Type(_,[S,T])) = Type ("fun",[S,change_arrow (n-1) T])
+| change_arrow _ _ = sys_error "cont_consts: change_arrow";
+
+fun trans_rules name2 name1 n mx = let
+ fun argnames _ 0 = []
+ | argnames c n = chr c::argnames (c+1) (n-1);
+ val vnames = argnames (ord "A") n;
+ val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1);
+ in [Syntax.ParsePrintRule (Syntax.mk_appl (Constant name2) (map Variable vnames),
+ Library.foldl (fn (t,arg) => (Syntax.mk_appl (Constant "Rep_CFun")
+ [t,Variable arg]))
+ (Constant name1,vnames))]
+ @(case mx of InfixName _ => [extra_parse_rule]
+ | InfixlName _ => [extra_parse_rule]
+ | InfixrName _ => [extra_parse_rule] | _ => []) end;
+
+
+(* transforming infix/mixfix declarations of constants with type ...->...
+ a declaration of such a constant is transformed to a normal declaration with
+ an internal name, the same type, and nofix. Additionally, a purely syntactic
+ declaration with the original name, type ...=>..., and the original mixfix
+ is generated and connected to the other declaration via some translation.
+*)
+fun fix_mixfix (syn , T, mx as Infix p ) =
+ (Syntax.const_name syn mx, T, InfixName (syn, p))
+ | fix_mixfix (syn , T, mx as Infixl p ) =
+ (Syntax.const_name syn mx, T, InfixlName (syn, p))
+ | fix_mixfix (syn , T, mx as Infixr p ) =
+ (Syntax.const_name syn mx, T, InfixrName (syn, p))
+ | fix_mixfix decl = decl;
+fun transform decl = let
+ val (c, T, mx) = fix_mixfix decl;
+ val c2 = "_cont_" ^ c;
+ val n = Syntax.mixfix_args mx
+ in ((c , T,NoSyn),
+ (c2,change_arrow n T,mx ),
+ trans_rules c2 c n mx) end;
+
+fun cfun_arity (Type(n,[_,T])) = if n = cfun_arrow then 1+cfun_arity T else 0
+| cfun_arity _ = 0;
+
+fun is_contconst (_,_,NoSyn ) = false
+| is_contconst (_,_,Binder _) = false
+| is_contconst (c,T,mx ) = cfun_arity T >= Syntax.mixfix_args mx
+ handle ERROR msg => cat_error msg ("in mixfix annotation for " ^
+ quote (Syntax.const_name c mx));
+
+
+(* add_consts(_i) *)
+
+fun gen_add_consts prep_typ raw_decls thy =
+ let
+ val decls = map (upd_second (prep_typ thy)) raw_decls;
+ val (contconst_decls, normal_decls) = List.partition is_contconst decls;
+ val transformed_decls = map transform contconst_decls;
+ in
+ thy
+ |> Sign.add_consts_i normal_decls
+ |> Sign.add_consts_i (map first transformed_decls)
+ |> Sign.add_syntax_i (map second transformed_decls)
+ |> Sign.add_trrules_i (List.concat (map third transformed_decls))
+ end;
+
+val add_consts = gen_add_consts Sign.read_typ;
+val add_consts_i = gen_add_consts Sign.certify_typ;
+
+
+(* outer syntax *)
+
+local structure P = OuterParse and K = OuterKeyword in
+
+val constsP =
+ OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
+ (Scan.repeat1 P.const >> (Toplevel.theory o add_consts));
+
+val _ = OuterSyntax.add_parsers [constsP];
+
+end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/cont_proc.ML Thu May 31 14:01:58 2007 +0200
@@ -0,0 +1,145 @@
+(* Title: HOLCF/Tools/cont_proc.ML
+ ID: $Id$
+ Author: Brian Huffman
+*)
+
+signature CONT_PROC =
+sig
+ val is_lcf_term: term -> bool
+ val cont_thms: term -> thm list
+ val all_cont_thms: term -> thm list
+ val cont_tac: int -> tactic
+ val cont_proc: theory -> simproc
+ val setup: theory -> theory
+end;
+
+structure ContProc: CONT_PROC =
+struct
+
+(** theory context references **)
+
+val cont_K = thm "cont_const";
+val cont_I = thm "cont_id";
+val cont_A = thm "cont2cont_Rep_CFun";
+val cont_L = thm "cont2cont_LAM";
+val cont_R = thm "cont_Rep_CFun2";
+
+(* checks whether a term contains no dangling bound variables *)
+val is_closed_term =
+ let
+ fun bound_less i (t $ u) =
+ bound_less i t andalso bound_less i u
+ | bound_less i (Abs (_, _, t)) = bound_less (i+1) t
+ | bound_less i (Bound n) = n < i
+ | bound_less i _ = true; (* Const, Free, and Var are OK *)
+ in bound_less 0 end;
+
+(* checks whether a term is written entirely in the LCF sublanguage *)
+fun is_lcf_term (Const ("Cfun.Rep_CFun", _) $ t $ u) =
+ is_lcf_term t andalso is_lcf_term u
+ | is_lcf_term (Const ("Cfun.Abs_CFun", _) $ Abs (_, _, t)) = is_lcf_term t
+ | is_lcf_term (Const ("Cfun.Abs_CFun", _) $ _) = false
+ | is_lcf_term (Bound _) = true
+ | is_lcf_term t = is_closed_term t;
+
+(*
+ efficiently generates a cont thm for every LAM abstraction in a term,
+ using forward proof and reusing common subgoals
+*)
+local
+ fun var 0 = [SOME cont_I]
+ | var n = NONE :: var (n-1);
+
+ fun k NONE = cont_K
+ | k (SOME x) = x;
+
+ fun ap NONE NONE = NONE
+ | ap x y = SOME (k y RS (k x RS cont_A));
+
+ fun zip [] [] = []
+ | zip [] (y::ys) = (ap NONE y ) :: zip [] ys
+ | zip (x::xs) [] = (ap x NONE) :: zip xs []
+ | zip (x::xs) (y::ys) = (ap x y ) :: zip xs ys
+
+ fun lam [] = ([], cont_K)
+ | lam (x::ys) =
+ let
+ (* should use "standard" for thms that are used multiple times *)
+ (* it seems to allow for sharing in explicit proof objects *)
+ val x' = standard (k x);
+ val Lx = x' RS cont_L;
+ in (map (fn y => SOME (k y RS Lx)) ys, x') end;
+
+ (* first list: cont thm for each dangling bound variable *)
+ (* second list: cont thm for each LAM in t *)
+ (* if b = false, only return cont thm for outermost LAMs *)
+ fun cont_thms1 b (Const ("Cfun.Rep_CFun", _) $ f $ t) =
+ let
+ val (cs1,ls1) = cont_thms1 b f;
+ val (cs2,ls2) = cont_thms1 b t;
+ in (zip cs1 cs2, if b then ls1 @ ls2 else []) end
+ | cont_thms1 b (Const ("Cfun.Abs_CFun", _) $ Abs (_, _, t)) =
+ let
+ val (cs, ls) = cont_thms1 b t;
+ val (cs', l) = lam cs;
+ in (cs', l::ls) end
+ | cont_thms1 _ (Bound n) = (var n, [])
+ | cont_thms1 _ _ = ([], []);
+in
+ (* precondition: is_lcf_term t = true *)
+ fun cont_thms t = snd (cont_thms1 false t);
+ fun all_cont_thms t = snd (cont_thms1 true t);
+end;
+
+(*
+ Given the term "cont f", the procedure tries to construct the
+ theorem "cont f == True". If this theorem cannot be completely
+ solved by the introduction rules, then the procedure returns a
+ conditional rewrite rule with the unsolved subgoals as premises.
+*)
+
+local
+ val rules = [cont_K, cont_I, cont_R, cont_A, cont_L];
+
+ val prev_cont_thms : thm list ref = ref [];
+
+ fun old_cont_tac i thm =
+ case !prev_cont_thms of
+ [] => no_tac thm
+ | (c::cs) => (prev_cont_thms := cs; rtac c i thm);
+
+ fun new_cont_tac f' i thm =
+ case all_cont_thms f' of
+ [] => no_tac thm
+ | (c::cs) => (prev_cont_thms := cs; rtac c i thm);
+
+ fun cont_tac_of_term (Const ("Cont.cont", _) $ f) =
+ let
+ val f' = Const ("Cfun.Abs_CFun", dummyT) $ f;
+ in
+ if is_lcf_term f'
+ then old_cont_tac ORELSE' new_cont_tac f'
+ else REPEAT_ALL_NEW (resolve_tac rules)
+ end
+ | cont_tac_of_term _ = K no_tac;
+in
+ val cont_tac =
+ SUBGOAL (fn (t, i) => cont_tac_of_term (HOLogic.dest_Trueprop t) i);
+end;
+
+local
+ fun solve_cont thy _ t =
+ let
+ val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI;
+ in Option.map fst (Seq.pull (cont_tac 1 tr)) end
+in
+ fun cont_proc thy =
+ Simplifier.simproc thy "cont_proc" ["cont f"] solve_cont;
+end;
+
+val setup =
+ (fn thy =>
+ (Simplifier.change_simpset_of thy
+ (fn ss => ss addsimprocs [cont_proc thy]); thy));
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML Thu May 31 14:01:58 2007 +0200
@@ -0,0 +1,170 @@
+(* Title: HOLCF/Tools/domain/domain_axioms.ML
+ ID: $Id$
+ Author: David von Oheimb
+
+Syntax generator for domain command.
+*)
+
+structure Domain_Axioms = struct
+
+local
+
+open Domain_Library;
+infixr 0 ===>;infixr 0 ==>;infix 0 == ;
+infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<;
+infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo;
+
+fun calc_axioms comp_dname (eqs : eq list) n (((dname,_),cons) : eq)=
+let
+
+(* ----- axioms and definitions concerning the isomorphism ------------------ *)
+
+ val dc_abs = %%:(dname^"_abs");
+ val dc_rep = %%:(dname^"_rep");
+ val x_name'= "x";
+ val x_name = idx_name eqs x_name' (n+1);
+ val dnam = Sign.base_name dname;
+
+ val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name'));
+ val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));
+
+ val when_def = ("when_def",%%:(dname^"_when") ==
+ foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) =>
+ Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
+
+ val copy_def = let
+ fun idxs z x arg = if is_rec arg
+ then (cproj (Bound z) eqs (rec_of arg))`Bound(z-x)
+ else Bound(z-x);
+ fun one_con (con,args) =
+ foldr /\# (list_ccomb (%%:con, mapn (idxs (length args)) 1 args)) args;
+ in ("copy_def", %%:(dname^"_copy") ==
+ /\"f" (list_ccomb (%%:(dname^"_when"), map one_con cons))) end;
+
+(* -- definitions concerning the constructors, discriminators and selectors - *)
+
+ fun con_def m n (_,args) = let
+ fun idxs z x arg = (if is_lazy arg then fn t => %%:upN`t else I) (Bound(z-x));
+ fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs);
+ fun inj y 1 _ = y
+ | inj y _ 0 = %%:sinlN`y
+ | inj y i j = %%:sinrN`(inj y (i-1) (j-1));
+ in foldr /\# (dc_abs`(inj (parms args) m n)) args end;
+
+ val con_defs = mapn (fn n => fn (con,args) =>
+ (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons;
+
+ val dis_defs = let
+ fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) ==
+ list_ccomb(%%:(dname^"_when"),map
+ (fn (con',args) => (foldr /\#
+ (if con'=con then %%:TT_N else %%:FF_N) args)) cons))
+ in map ddef cons end;
+
+ val mat_defs = let
+ fun mdef (con,_) = (mat_name con ^"_def",%%:(mat_name con) ==
+ list_ccomb(%%:(dname^"_when"),map
+ (fn (con',args) => (foldr /\#
+ (if con'=con
+ then %%:returnN`(mk_ctuple (map (bound_arg args) args))
+ else %%:failN) args)) cons))
+ in map mdef cons end;
+
+ val pat_defs =
+ let
+ fun pdef (con,args) =
+ let
+ val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
+ val xs = map (bound_arg args) args;
+ val r = Bound (length args);
+ val rhs = case args of [] => %%:returnN ` HOLogic.unit
+ | _ => foldr1 cpair_pat ps ` mk_ctuple xs;
+ fun one_con (con',args') = foldr /\# (if con'=con then rhs else %%:failN) args';
+ in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) ==
+ list_ccomb(%%:(dname^"_when"), map one_con cons))
+ end
+ in map pdef cons end;
+
+ val sel_defs = let
+ fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel ==
+ list_ccomb(%%:(dname^"_when"),map
+ (fn (con',args) => if con'<>con then UU else
+ foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
+ in List.mapPartial I (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end;
+
+
+(* ----- axiom and definitions concerning induction ------------------------- *)
+
+ val reach_ax = ("reach", mk_trp(cproj (%%:fixN`%%(comp_dname^"_copy")) eqs n
+ `%x_name === %:x_name));
+ val take_def = ("take_def",%%:(dname^"_take") == mk_lam("n",cproj
+ (%%:iterateN $ Bound 0 ` %%:(comp_dname^"_copy") ` UU) eqs n));
+ val finite_def = ("finite_def",%%:(dname^"_finite") == mk_lam(x_name,
+ mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
+
+in (dnam,
+ [abs_iso_ax, rep_iso_ax, reach_ax],
+ [when_def, copy_def] @
+ con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @
+ [take_def, finite_def])
+end; (* let *)
+
+fun infer_props thy = map (apsnd (FixrecPackage.legacy_infer_prop thy));
+
+fun add_axioms_i x = snd o PureThy.add_axioms_i (map Thm.no_attributes x);
+fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy;
+
+fun add_defs_i x = snd o (PureThy.add_defs_i false) (map Thm.no_attributes x);
+fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
+
+in (* local *)
+
+fun add_axioms (comp_dnam, eqs : eq list) thy' = let
+ val comp_dname = Sign.full_name thy' comp_dnam;
+ val dnames = map (fst o fst) eqs;
+ val x_name = idx_name dnames "x";
+ fun copy_app dname = %%:(dname^"_copy")`Bound 0;
+ val copy_def = ("copy_def" , %%:(comp_dname^"_copy") ==
+ /\"f"(foldr1 cpair (map copy_app dnames)));
+ val bisim_def = ("bisim_def",%%:(comp_dname^"_bisim")==mk_lam("R",
+ let
+ fun one_con (con,args) = let
+ val nonrec_args = filter_out is_rec args;
+ val rec_args = List.filter is_rec args;
+ val recs_cnt = length rec_args;
+ val allargs = nonrec_args @ rec_args
+ @ map (upd_vname (fn s=> s^"'")) rec_args;
+ val allvns = map vname allargs;
+ fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg;
+ val vns1 = map (vname_arg "" ) args;
+ val vns2 = map (vname_arg "'") args;
+ val allargs_cnt = length nonrec_args + 2*recs_cnt;
+ val rec_idxs = (recs_cnt-1) downto 0;
+ val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg)
+ (allargs~~((allargs_cnt-1) downto 0)));
+ fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $
+ Bound (2*recs_cnt-i) $ Bound (recs_cnt-i);
+ val capps = foldr mk_conj (mk_conj(
+ Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1),
+ Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2)))
+ (mapn rel_app 1 rec_args);
+ in foldr mk_ex (Library.foldr mk_conj
+ (map (defined o Bound) nonlazy_idxs,capps)) allvns end;
+ fun one_comp n (_,cons) =mk_all(x_name(n+1),mk_all(x_name(n+1)^"'",mk_imp(
+ proj (Bound 2) eqs n $ Bound 1 $ Bound 0,
+ foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
+ ::map one_con cons))));
+ in foldr1 mk_conj (mapn one_comp 0 eqs)end ));
+ fun add_one (thy,(dnam,axs,dfs)) = thy
+ |> Theory.add_path dnam
+ |> add_defs_infer dfs
+ |> add_axioms_infer axs
+ |> Theory.parent_path;
+ val thy = Library.foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs);
+in thy |> Theory.add_path comp_dnam
+ |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else []))
+ |> Theory.parent_path
+end;
+
+end; (* local *)
+end; (* struct *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/domain/domain_extender.ML Thu May 31 14:01:58 2007 +0200
@@ -0,0 +1,183 @@
+(* Title: HOLCF/Tools/domain/domain_extender.ML
+ ID: $Id$
+ Author: David von Oheimb
+
+Theory extender for domain command, including theory syntax.
+
+###TODO:
+
+this definition
+domain empty = silly empty
+yields
+Exception-
+ TERM
+ ("typ_of_term: bad encoding of type",
+ [Abs ("uu", "_", Const ("NONE", "_"))]) raised
+but this works fine:
+domain Empty = silly Empty
+
+strange syntax errors are produced for:
+domain xx = xx ("x yy")
+domain 'a foo = foo (sel::"'a")
+and bar = bar ("'a dummy")
+
+*)
+
+signature DOMAIN_EXTENDER =
+sig
+ val add_domain: string * ((bstring * string list) *
+ (string * mixfix * (bool * string option * string) list) list) list
+ -> theory -> theory
+ val add_domain_i: string * ((bstring * string list) *
+ (string * mixfix * (bool * string option * typ) list) list) list
+ -> theory -> theory
+end;
+
+structure Domain_Extender: DOMAIN_EXTENDER =
+struct
+
+open Domain_Library;
+
+(* ----- general testing and preprocessing of constructor list -------------- *)
+fun check_and_sort_domain (dtnvs: (string * typ list) list,
+ cons'' : ((string * mixfix * (bool * string option * typ) list) list) list) sg =
+ let
+ val defaultS = Sign.defaultS sg;
+ val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of
+ [] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
+ val test_dupl_cons = (case duplicates (op =) (map first (List.concat cons'')) of
+ [] => false | dups => error ("Duplicate constructors: "
+ ^ commas_quote dups));
+ val test_dupl_sels = (case duplicates (op =) (List.mapPartial second
+ (List.concat (map third (List.concat cons'')))) of
+ [] => false | dups => error("Duplicate selectors: "^commas_quote dups));
+ val test_dupl_tvars = exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of
+ [] => false | dups => error("Duplicate type arguments: "
+ ^commas_quote dups)) (map snd dtnvs);
+ (* test for free type variables, illegal sort constraints on rhs,
+ non-pcpo-types and invalid use of recursive type;
+ replace sorts in type variables on rhs *)
+ fun analyse_equation ((dname,typevars),cons') =
+ let
+ val tvars = map dest_TFree typevars;
+ val distinct_typevars = map TFree tvars;
+ fun rm_sorts (TFree(s,_)) = TFree(s,[])
+ | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
+ | rm_sorts (TVar(s,_)) = TVar(s,[])
+ and remove_sorts l = map rm_sorts l;
+ val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
+ fun analyse indirect (TFree(v,s)) = (case AList.lookup (op =) tvars v of
+ NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
+ | SOME sort => if eq_set_string (s,defaultS) orelse
+ eq_set_string (s,sort )
+ then TFree(v,sort)
+ else error ("Inconsistent sort constraint" ^
+ " for type variable " ^ quote v))
+ | analyse indirect (t as Type(s,typl)) = (case AList.lookup (op =) dtnvs s of
+ NONE => if s mem indirect_ok
+ then Type(s,map (analyse false) typl)
+ else Type(s,map (analyse true) typl)
+ | SOME typevars => if indirect
+ then error ("Indirect recursion of type " ^
+ quote (string_of_typ sg t))
+ else if dname <> s orelse (** BUG OR FEATURE?:
+ mutual recursion may use different arguments **)
+ remove_sorts typevars = remove_sorts typl
+ then Type(s,map (analyse true) typl)
+ else error ("Direct recursion of type " ^
+ quote (string_of_typ sg t) ^
+ " with different arguments"))
+ | analyse indirect (TVar _) = Imposs "extender:analyse";
+ fun check_pcpo T = if pcpo_type sg T then T
+ else error("Constructor argument type is not of sort pcpo: "^string_of_typ sg T);
+ val analyse_con = upd_third (map (upd_third (check_pcpo o analyse false)));
+ in ((dname,distinct_typevars), map analyse_con cons') end;
+ in ListPair.map analyse_equation (dtnvs,cons'')
+ end; (* let *)
+
+(* ----- calls for building new thy and thms -------------------------------- *)
+
+fun gen_add_domain prep_typ (comp_dnam, eqs''') thy''' =
+ let
+ val dtnvs = map ((fn (dname,vs) =>
+ (Sign.full_name thy''' dname, map (Sign.read_typ thy''') vs))
+ o fst) eqs''';
+ val cons''' = map snd eqs''';
+ fun thy_type (dname,tvars) = (Sign.base_name dname, length tvars, NoSyn);
+ fun thy_arity (dname,tvars) = (dname, map (snd o dest_TFree) tvars, pcpoS);
+ val thy'' = thy''' |> Theory.add_types (map thy_type dtnvs)
+ |> fold (AxClass.axiomatize_arity_i o thy_arity) dtnvs;
+ val cons'' = map (map (upd_third (map (upd_third (prep_typ thy''))))) cons''';
+ val eqs' = check_and_sort_domain (dtnvs,cons'') thy'';
+ val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs');
+ val dts = map (Type o fst) eqs';
+ val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
+ fun strip ss = Library.drop (find_index_eq "'" ss +1, ss);
+ fun typid (Type (id,_)) =
+ let val c = hd (Symbol.explode (Sign.base_name id))
+ in if Symbol.is_letter c then c else "t" end
+ | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id)))
+ | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
+ fun one_con (con,mx,args) =
+ ((Syntax.const_name con mx),
+ ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
+ find_index_eq tp dts,
+ DatatypeAux.dtyp_of_typ new_dts tp),
+ sel,vn))
+ (args,(mk_var_names(map (typid o third) args)))
+ ) : cons;
+ val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list;
+ val thy = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs);
+ val (theorems_thy, (rewss, take_rews)) = (foldl_map (fn (thy0,eq) =>
+ Domain_Theorems.theorems (eq,eqs) thy0) (thy,eqs))
+ |>>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
+ in
+ theorems_thy
+ |> Theory.add_path (Sign.base_name comp_dnam)
+ |> (snd o (PureThy.add_thmss [(("rews", List.concat rewss @ take_rews), [])]))
+ |> Theory.parent_path
+ end;
+
+val add_domain_i = gen_add_domain Sign.certify_typ;
+val add_domain = gen_add_domain Sign.read_typ;
+
+
+(** outer syntax **)
+
+local structure P = OuterParse and K = OuterKeyword in
+
+val dest_decl =
+ P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
+ (P.name >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1
+ || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
+ >> (fn t => (true,NONE,t))
+ || P.typ >> (fn t => (false,NONE,t));
+
+val cons_decl =
+ P.name -- Scan.repeat dest_decl -- P.opt_mixfix
+ >> (fn ((c, ds), mx) => (c, mx, ds));
+
+val type_var' = (P.type_ident ^^
+ Scan.optional (P.$$$ "::" ^^ P.!!! P.sort) "");
+val type_args' = type_var' >> single ||
+ P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") ||
+ Scan.succeed [];
+
+val domain_decl = (type_args' -- P.name >> Library.swap) --
+ (P.$$$ "=" |-- P.enum1 "|" cons_decl);
+val domains_decl =
+ Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.and_list1 domain_decl
+ >> (fn (opt_name, doms) =>
+ (case opt_name of NONE => space_implode "_" (map (#1 o #1) doms) | SOME s => s, doms));
+
+val domainP =
+ OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
+ (domains_decl >> (Toplevel.theory o add_domain));
+
+
+val _ = OuterSyntax.add_keywords ["lazy"];
+val _ = OuterSyntax.add_parsers [domainP];
+
+end; (* local structure *)
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/domain/domain_library.ML Thu May 31 14:01:58 2007 +0200
@@ -0,0 +1,230 @@
+(* Title: HOLCF/Tools/domain/domain_library.ML
+ ID: $Id$
+ Author: David von Oheimb
+
+Library for domain command.
+*)
+
+
+(* ----- general support ---------------------------------------------------- *)
+
+fun mapn f n [] = []
+| mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs;
+
+fun foldr'' f (l,f2) = let fun itr [] = raise Fail "foldr''"
+ | itr [a] = f2 a
+ | itr (a::l) = f(a, itr l)
+in itr l end;
+fun map_cumulr f start xs = foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) =>
+ (y::ys,res2)) ([],start) xs;
+
+
+fun first (x,_,_) = x; fun second (_,x,_) = x; fun third (_,_,x) = x;
+fun upd_first f (x,y,z) = (f x, y, z);
+fun upd_second f (x,y,z) = ( x, f y, z);
+fun upd_third f (x,y,z) = ( x, y, f z);
+
+fun atomize thm = let val r_inst = read_instantiate;
+ fun at thm = case concl_of thm of
+ _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
+ | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [("x","?"^s)] spec))
+ | _ => [thm];
+in map zero_var_indexes (at thm) end;
+
+(* ----- specific support for domain ---------------------------------------- *)
+
+structure Domain_Library = struct
+
+open HOLCFLogic;
+
+exception Impossible of string;
+fun Imposs msg = raise Impossible ("Domain:"^msg);
+
+(* ----- name handling ----- *)
+
+val strip_esc = let fun strip ("'" :: c :: cs) = c :: strip cs
+ | strip ["'"] = []
+ | strip (c :: cs) = c :: strip cs
+ | strip [] = [];
+in implode o strip o Symbol.explode end;
+
+fun extern_name con = case Symbol.explode con of
+ ("o"::"p"::" "::rest) => implode rest
+ | _ => con;
+fun dis_name con = "is_"^ (extern_name con);
+fun dis_name_ con = "is_"^ (strip_esc con);
+fun mat_name con = "match_"^ (extern_name con);
+fun mat_name_ con = "match_"^ (strip_esc con);
+fun pat_name con = (extern_name con) ^ "_pat";
+fun pat_name_ con = (strip_esc con) ^ "_pat";
+
+(* make distinct names out of the type list,
+ forbidding "o","n..","x..","f..","P.." as names *)
+(* a number string is added if necessary *)
+fun mk_var_names ids : string list = let
+ fun nonreserved s = if s mem ["n","x","f","P"] then s^"'" else s;
+ fun index_vnames(vn::vns,occupied) =
+ (case AList.lookup (op =) occupied vn of
+ NONE => if vn mem vns
+ then (vn^"1") :: index_vnames(vns,(vn,1) ::occupied)
+ else vn :: index_vnames(vns, occupied)
+ | SOME(i) => (vn^(string_of_int (i+1)))
+ :: index_vnames(vns,(vn,i+1)::occupied))
+ | index_vnames([],occupied) = [];
+in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end;
+
+fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, pcpoS);
+fun string_of_typ sg = Sign.string_of_typ sg o Sign.certify_typ sg;
+
+(* ----- constructor list handling ----- *)
+
+type cons = (string * (* operator name of constr *)
+ ((bool*int*DatatypeAux.dtyp)* (* (lazy,recursive element or ~1) *)
+ string option* (* selector name *)
+ string) (* argument name *)
+ list); (* argument list *)
+type eq = (string * (* name of abstracted type *)
+ typ list) * (* arguments of abstracted type *)
+ cons list; (* represented type, as a constructor list *)
+
+fun rec_of arg = second (first arg);
+fun is_lazy arg = first (first arg);
+val sel_of = second;
+val vname = third;
+val upd_vname = upd_third;
+fun is_rec arg = rec_of arg >=0;
+fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
+fun nonlazy args = map vname (filter_out is_lazy args);
+fun nonlazy_rec args = map vname (List.filter is_nonlazy_rec args);
+
+(* ----- qualified names of HOLCF constants ----- *)
+
+val lessN = "Porder.<<"
+val UU_N = "Pcpo.UU";
+val admN = "Adm.adm";
+val compactN = "Adm.compact";
+val Rep_CFunN = "Cfun.Rep_CFun";
+val Abs_CFunN = "Cfun.Abs_CFun";
+val ID_N = "Cfun.ID";
+val cfcompN = "Cfun.cfcomp";
+val strictifyN = "Cfun.strictify";
+val cpairN = "Cprod.cpair";
+val cfstN = "Cprod.cfst";
+val csndN = "Cprod.csnd";
+val csplitN = "Cprod.csplit";
+val spairN = "Sprod.spair";
+val sfstN = "Sprod.sfst";
+val ssndN = "Sprod.ssnd";
+val ssplitN = "Sprod.ssplit";
+val sinlN = "Ssum.sinl";
+val sinrN = "Ssum.sinr";
+val sscaseN = "Ssum.sscase";
+val upN = "Up.up";
+val fupN = "Up.fup";
+val ONE_N = "One.ONE";
+val TT_N = "Tr.TT";
+val FF_N = "Tr.FF";
+val iterateN = "Fix.iterate";
+val fixN = "Fix.fix";
+val returnN = "Fixrec.return";
+val failN = "Fixrec.fail";
+val cpair_patN = "Fixrec.cpair_pat";
+val branchN = "Fixrec.branch";
+
+val pcpoN = "Pcpo.pcpo"
+val pcpoS = [pcpoN];
+
+
+(* ----- support for type and mixfix expressions ----- *)
+
+infixr 5 -->;
+
+(* ----- support for term expressions ----- *)
+
+fun %: s = Free(s,dummyT);
+fun %# arg = %:(vname arg);
+fun %%: s = Const(s,dummyT);
+
+local open HOLogic in
+val mk_trp = mk_Trueprop;
+fun mk_conj (S,T) = conj $ S $ T;
+fun mk_disj (S,T) = disj $ S $ T;
+fun mk_imp (S,T) = imp $ S $ T;
+fun mk_lam (x,T) = Abs(x,dummyT,T);
+fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P);
+fun mk_ex (x,P) = mk_exists (x,dummyT,P);
+fun mk_constrain (typ,T) = TypeInfer.constrain T typ;
+fun mk_constrainall (x,typ,P) = %%:"All" $ (TypeInfer.constrain (mk_lam(x,P)) (typ --> boolT));
+end
+
+fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
+
+infixr 0 ===>; fun S ===> T = %%:"==>" $ S $ T;
+infixr 0 ==>; fun S ==> T = mk_trp S ===> mk_trp T;
+infix 0 ==; fun S == T = %%:"==" $ S $ T;
+infix 1 ===; fun S === T = %%:"op =" $ S $ T;
+infix 1 ~=; fun S ~= T = HOLogic.mk_not (S === T);
+infix 1 <<; fun S << T = %%:lessN $ S $ T;
+infix 1 ~<<; fun S ~<< T = HOLogic.mk_not (S << T);
+
+infix 9 ` ; fun f` x = %%:Rep_CFunN $ f $ x;
+infix 9 `% ; fun f`% s = f` %: s;
+infix 9 `%%; fun f`%%s = f` %%:s;
+val list_ccomb = Library.foldl (op `); (* continuous version of list_comb *)
+fun con_app2 con f args = list_ccomb(%%:con,map f args);
+fun con_app con = con_app2 con %#;
+fun if_rec arg f y = if is_rec arg then f (rec_of arg) else y;
+fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) I (%# arg);
+fun prj _ _ x ( _::[]) _ = x
+| prj f1 _ x (_::y::ys) 0 = f1 x y
+| prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1);
+fun proj x = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
+fun cproj x = prj (fn S => K(%%:cfstN`S)) (fn S => K(%%:csndN`S)) x;
+fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
+
+fun /\ v T = %%:Abs_CFunN $ mk_lam(v,T);
+fun /\# (arg,T) = /\ (vname arg) T;
+infixr 9 oo; fun S oo T = %%:cfcompN`S`T;
+val UU = %%:UU_N;
+fun strict f = f`UU === UU;
+fun defined t = t ~= UU;
+fun cpair (t,u) = %%:cpairN`t`u;
+fun spair (t,u) = %%:spairN`t`u;
+fun mk_ctuple [] = HOLogic.unit (* used in match_defs *)
+| mk_ctuple ts = foldr1 cpair ts;
+fun mk_stuple [] = %%:ONE_N
+| mk_stuple ts = foldr1 spair ts;
+fun mk_ctupleT [] = HOLogic.unitT (* used in match_defs *)
+| mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts;
+fun mk_maybeT T = Type ("Fixrec.maybe",[T]);
+fun cpair_pat (p1,p2) = %%:cpair_patN $ p1 $ p2;
+fun lift_defined f = lift (fn x => defined (f x));
+fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
+
+fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) =
+ (case cont_eta_contract body of
+ body' as (Const("Cfun.Rep_CFun",Ta) $ f $ Bound 0) =>
+ if not (0 mem loose_bnos f) then incr_boundvars ~1 f
+ else Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body')
+ | body' => Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body'))
+| cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t
+| cont_eta_contract t = t;
+
+fun idx_name dnames s n = s^(if length dnames = 1 then "" else string_of_int n);
+fun when_funs cons = if length cons = 1 then ["f"]
+ else mapn (fn n => K("f"^(string_of_int n))) 1 cons;
+fun when_body cons funarg = let
+ fun one_fun n (_,[] ) = /\ "dummy" (funarg(1,n))
+ | one_fun n (_,args) = let
+ val l2 = length args;
+ fun idxs m arg = (if is_lazy arg then fn x=> %%:fupN` %%:ID_N`x
+ else I) (Bound(l2-m));
+ in cont_eta_contract (foldr''
+ (fn (a,t) => %%:ssplitN`(/\# (a,t)))
+ (args,
+ fn a=> /\#(a,(list_ccomb(funarg(l2,n),mapn idxs 1 args))))
+ ) end;
+in (if length cons = 1 andalso length(snd(hd cons)) <= 1
+ then fn t => %%:strictifyN`t else I)
+ (foldr1 (fn (x,y)=> %%:sscaseN`x`y) (mapn one_fun 1 cons)) end;
+end; (* struct *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/domain/domain_syntax.ML Thu May 31 14:01:58 2007 +0200
@@ -0,0 +1,151 @@
+(* Title: HOLCF/Tools/domain/domain_syntax.ML
+ ID: $Id$
+ Author: David von Oheimb
+
+Syntax generator for domain command.
+*)
+
+structure Domain_Syntax = struct
+
+local
+
+open Domain_Library;
+infixr 5 -->; infixr 6 ->>;
+fun calc_syntax dtypeprod ((dname, typevars),
+ (cons': (string * mixfix * (bool * string option * typ) list) list)) =
+let
+(* ----- constants concerning the isomorphism ------------------------------- *)
+
+local
+ fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
+ fun prod (_,_,args) = if args = [] then oneT
+ else foldr1 mk_sprodT (map opt_lazy args);
+ fun freetvar s = let val tvar = mk_TFree s in
+ if tvar mem typevars then freetvar ("t"^s) else tvar end;
+ fun when_type (_ ,_,args) = foldr (op ->>) (freetvar "t") (map third args);
+in
+ val dtype = Type(dname,typevars);
+ val dtype2 = foldr1 mk_ssumT (map prod cons');
+ val dnam = Sign.base_name dname;
+ val const_rep = (dnam^"_rep" , dtype ->> dtype2, NoSyn);
+ val const_abs = (dnam^"_abs" , dtype2 ->> dtype , NoSyn);
+ val const_when = (dnam^"_when",foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
+ val const_copy = (dnam^"_copy", dtypeprod ->> dtype ->> dtype , NoSyn);
+end;
+
+(* ----- constants concerning constructors, discriminators, and selectors --- *)
+
+local
+ val escape = let
+ fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs
+ else c::esc cs
+ | esc [] = []
+ in implode o esc o Symbol.explode end;
+ fun con (name,s,args) = (name,foldr (op ->>) dtype (map third args),s);
+ fun dis (con ,s,_ ) = (dis_name_ con, dtype->>trT,
+ Mixfix(escape ("is_" ^ con), [], Syntax.max_pri));
+ (* strictly speaking, these constants have one argument,
+ but the mixfix (without arguments) is introduced only
+ to generate parse rules for non-alphanumeric names*)
+ fun mat (con ,s,args) = (mat_name_ con, dtype->>mk_maybeT(mk_ctupleT(map third args)),
+ Mixfix(escape ("match_" ^ con), [], Syntax.max_pri));
+ fun sel1 (_,sel,typ) = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
+ fun sel (_ ,_,args) = List.mapPartial sel1 args;
+ fun freetvar s n = let val tvar = mk_TFree (s ^ string_of_int n) in
+ if tvar mem typevars then freetvar ("t"^s) n else tvar end;
+ fun mk_patT (a,b) = a ->> mk_maybeT b;
+ fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n);
+ fun pat (con ,s,args) = (pat_name_ con, (mapn pat_arg_typ 1 args) --->
+ mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))),
+ Mixfix(escape (con ^ "_pat"), [], Syntax.max_pri));
+
+in
+ val consts_con = map con cons';
+ val consts_dis = map dis cons';
+ val consts_mat = map mat cons';
+ val consts_pat = map pat cons';
+ val consts_sel = List.concat(map sel cons');
+end;
+
+(* ----- constants concerning induction ------------------------------------- *)
+
+ val const_take = (dnam^"_take" , HOLogic.natT-->dtype->>dtype, NoSyn);
+ val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT , NoSyn);
+
+(* ----- case translation --------------------------------------------------- *)
+
+local open Syntax in
+ local
+ fun c_ast con mx = Constant (const_name con mx);
+ fun expvar n = Variable ("e"^(string_of_int n));
+ fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
+ (string_of_int m));
+ fun argvars n args = mapn (argvar n) 1 args;
+ fun app s (l,r) = mk_appl (Constant s) [l,r];
+ val cabs = app "_cabs";
+ val capp = app "Rep_CFun";
+ fun con1 n (con,mx,args) = Library.foldl capp (c_ast con mx, argvars n args);
+ fun case1 n (con,mx,args) = app "_case1" (con1 n (con,mx,args), expvar n);
+ fun arg1 n (con,_,args) = foldr cabs (expvar n) (argvars n args);
+ fun when1 n m = if n = m then arg1 n else K (Constant "UU");
+
+ fun app_var x = mk_appl (Constant "_var") [x, Variable "rhs"];
+ fun app_pat x = mk_appl (Constant "_pat") [x];
+ fun args_list [] = Constant "Unity"
+ | args_list xs = foldr1 (app "_args") xs;
+ in
+ val case_trans = ParsePrintRule
+ (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn case1 1 cons')),
+ capp (Library.foldl capp (Constant (dnam^"_when"), mapn arg1 1 cons'), Variable "x"));
+
+ val abscon_trans = mapn (fn n => fn (con,mx,args) => ParsePrintRule
+ (cabs (con1 n (con,mx,args), expvar n),
+ Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons'))) 1 cons';
+
+ val Case_trans = List.concat (map (fn (con,mx,args) =>
+ let
+ val cname = c_ast con mx;
+ val pname = Constant (pat_name_ con);
+ val ns = 1 upto length args;
+ val xs = map (fn n => Variable ("x"^(string_of_int n))) ns;
+ val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
+ val vs = map (fn n => Variable ("v"^(string_of_int n))) ns;
+ in
+ [ParseRule (app_pat (Library.foldl capp (cname, xs)),
+ mk_appl pname (map app_pat xs)),
+ ParseRule (app_var (Library.foldl capp (cname, xs)),
+ app_var (args_list xs)),
+ PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)),
+ app "_match" (mk_appl pname ps, args_list vs))]
+ end) cons');
+ end;
+end;
+
+in ([const_rep, const_abs, const_when, const_copy] @
+ consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @
+ [const_take, const_finite],
+ (case_trans::(abscon_trans @ Case_trans)))
+end; (* let *)
+
+(* ----- putting all the syntax stuff together ------------------------------ *)
+
+in (* local *)
+
+fun add_syntax (comp_dnam,eqs': ((string * typ list) *
+ (string * mixfix * (bool * string option * typ) list) list) list) thy'' =
+let
+ val dtypes = map (Type o fst) eqs';
+ val boolT = HOLogic.boolT;
+ val funprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp ->> tp ) dtypes);
+ val relprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
+ val const_copy = (comp_dnam^"_copy" ,funprod ->> funprod, NoSyn);
+ val const_bisim = (comp_dnam^"_bisim" ,relprod --> boolT , NoSyn);
+ val ctt = map (calc_syntax funprod) eqs';
+in thy'' |> ContConsts.add_consts_i (List.concat (map fst ctt) @
+ (if length eqs'>1 then [const_copy] else[])@
+ [const_bisim])
+ |> Sign.add_trrules_i (List.concat(map snd ctt))
+end; (* let *)
+
+end; (* local *)
+end; (* struct *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML Thu May 31 14:01:58 2007 +0200
@@ -0,0 +1,951 @@
+(* Title: HOLCF/Tools/domain/domain_theorems.ML
+ ID: $Id$
+ Author: David von Oheimb
+ New proofs/tactics by Brian Huffman
+
+Proof generator for domain command.
+*)
+
+val HOLCF_ss = simpset();
+
+structure Domain_Theorems = struct
+
+local
+
+val adm_impl_admw = thm "adm_impl_admw";
+val antisym_less_inverse = thm "antisym_less_inverse";
+val beta_cfun = thm "beta_cfun";
+val cfun_arg_cong = thm "cfun_arg_cong";
+val ch2ch_Rep_CFunL = thm "ch2ch_Rep_CFunL";
+val ch2ch_Rep_CFunR = thm "ch2ch_Rep_CFunR";
+val chain_iterate = thm "chain_iterate";
+val compact_ONE = thm "compact_ONE";
+val compact_sinl = thm "compact_sinl";
+val compact_sinr = thm "compact_sinr";
+val compact_spair = thm "compact_spair";
+val compact_up = thm "compact_up";
+val contlub_cfun_arg = thm "contlub_cfun_arg";
+val contlub_cfun_fun = thm "contlub_cfun_fun";
+val fix_def2 = thm "fix_def2";
+val injection_eq = thm "injection_eq";
+val injection_less = thm "injection_less";
+val lub_equal = thm "lub_equal";
+val monofun_cfun_arg = thm "monofun_cfun_arg";
+val retraction_strict = thm "retraction_strict";
+val spair_eq = thm "spair_eq";
+val spair_less = thm "spair_less";
+val sscase1 = thm "sscase1";
+val ssplit1 = thm "ssplit1";
+val strictify1 = thm "strictify1";
+val wfix_ind = thm "wfix_ind";
+
+open Domain_Library;
+infixr 0 ===>;
+infixr 0 ==>;
+infix 0 == ;
+infix 1 ===;
+infix 1 ~= ;
+infix 1 <<;
+infix 1 ~<<;
+infix 9 ` ;
+infix 9 `% ;
+infix 9 `%%;
+infixr 9 oo;
+
+(* ----- general proof facilities ------------------------------------------- *)
+
+fun pg'' thy defs t tacs =
+ let
+ val t' = FixrecPackage.legacy_infer_term thy t;
+ val asms = Logic.strip_imp_prems t';
+ val prop = Logic.strip_imp_concl t';
+ fun tac prems =
+ rewrite_goals_tac defs THEN
+ EVERY (tacs (map (rewrite_rule defs) prems));
+ in Goal.prove_global thy [] asms prop tac end;
+
+fun pg' thy defs t tacsf =
+ let
+ fun tacs [] = tacsf
+ | tacs prems = cut_facts_tac prems 1 :: tacsf;
+ in pg'' thy defs t tacs end;
+
+fun case_UU_tac rews i v =
+ case_tac (v^"=UU") i THEN
+ asm_simp_tac (HOLCF_ss addsimps rews) i;
+
+val chain_tac =
+ REPEAT_DETERM o resolve_tac
+ [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL];
+
+(* ----- general proofs ----------------------------------------------------- *)
+
+val all2E = prove_goal HOL.thy "[| !x y . P x y; P x y ==> R |] ==> R"
+ (fn prems =>[
+ resolve_tac prems 1,
+ cut_facts_tac prems 1,
+ fast_tac HOL_cs 1]);
+
+val dist_eqI = prove_goal (the_context ()) "!!x::'a::po. ~ x << y ==> x ~= y"
+ (fn prems =>
+ [blast_tac (claset () addDs [antisym_less_inverse]) 1]);
+
+in
+
+fun theorems (((dname, _), cons) : eq, eqs : eq list) thy =
+let
+
+val dummy = writeln ("Proving isomorphism properties of domain "^dname^" ...");
+val pg = pg' thy;
+
+(* ----- getting the axioms and definitions --------------------------------- *)
+
+local
+ fun ga s dn = get_thm thy (Name (dn ^ "." ^ s));
+in
+ val ax_abs_iso = ga "abs_iso" dname;
+ val ax_rep_iso = ga "rep_iso" dname;
+ val ax_when_def = ga "when_def" dname;
+ fun get_def mk_name (con,_) = ga (mk_name con^"_def") dname;
+ val axs_con_def = map (get_def extern_name) cons;
+ val axs_dis_def = map (get_def dis_name) cons;
+ val axs_mat_def = map (get_def mat_name) cons;
+ val axs_pat_def = map (get_def pat_name) cons;
+ val axs_sel_def =
+ let
+ fun def_of_sel sel = ga (sel^"_def") dname;
+ fun def_of_arg arg = Option.map def_of_sel (sel_of arg);
+ fun defs_of_con (_, args) = List.mapPartial def_of_arg args;
+ in
+ List.concat (map defs_of_con cons)
+ end;
+ val ax_copy_def = ga "copy_def" dname;
+end; (* local *)
+
+(* ----- theorems concerning the isomorphism -------------------------------- *)
+
+val dc_abs = %%:(dname^"_abs");
+val dc_rep = %%:(dname^"_rep");
+val dc_copy = %%:(dname^"_copy");
+val x_name = "x";
+
+val iso_locale = iso_intro OF [ax_abs_iso, ax_rep_iso];
+val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
+val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
+val abs_defin' = iso_locale RS iso_abs_defin';
+val rep_defin' = iso_locale RS iso_rep_defin';
+val iso_rews = map standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
+
+(* ----- generating beta reduction rules from definitions-------------------- *)
+
+local
+ fun arglist (Const _ $ Abs (s, _, t)) =
+ let
+ val (vars,body) = arglist t;
+ in (s :: vars, body) end
+ | arglist t = ([], t);
+ fun bind_fun vars t = Library.foldr mk_All (vars, t);
+ fun bound_vars 0 = []
+ | bound_vars i = Bound (i-1) :: bound_vars (i - 1);
+in
+ fun appl_of_def def =
+ let
+ val (_ $ con $ lam) = concl_of def;
+ val (vars, rhs) = arglist lam;
+ val lhs = list_ccomb (con, bound_vars (length vars));
+ val appl = bind_fun vars (lhs == rhs);
+ val cs = ContProc.cont_thms lam;
+ val betas = map (fn c => mk_meta_eq (c RS beta_cfun)) cs;
+ in pg (def::betas) appl [rtac reflexive_thm 1] end;
+end;
+
+val when_appl = appl_of_def ax_when_def;
+val con_appls = map appl_of_def axs_con_def;
+
+local
+ fun arg2typ n arg =
+ let val t = TVar (("'a", n), pcpoS)
+ in (n + 1, if is_lazy arg then mk_uT t else t) end;
+
+ fun args2typ n [] = (n, oneT)
+ | args2typ n [arg] = arg2typ n arg
+ | args2typ n (arg::args) =
+ let
+ val (n1, t1) = arg2typ n arg;
+ val (n2, t2) = args2typ n1 args
+ in (n2, mk_sprodT (t1, t2)) end;
+
+ fun cons2typ n [] = (n,oneT)
+ | cons2typ n [con] = args2typ n (snd con)
+ | cons2typ n (con::cons) =
+ let
+ val (n1, t1) = args2typ n (snd con);
+ val (n2, t2) = cons2typ n1 cons
+ in (n2, mk_ssumT (t1, t2)) end;
+in
+ fun cons2ctyp cons = ctyp_of thy (snd (cons2typ 1 cons));
+end;
+
+local
+ val iso_swap = iso_locale RS iso_iso_swap;
+ fun one_con (con, args) =
+ let
+ val vns = map vname args;
+ val eqn = %:x_name === con_app2 con %: vns;
+ val conj = foldr1 mk_conj (eqn :: map (defined o %:) (nonlazy args));
+ in Library.foldr mk_ex (vns, conj) end;
+
+ val conj_assoc = thm "conj_assoc";
+ val exh = foldr1 mk_disj ((%:x_name === UU) :: map one_con cons);
+ val thm1 = instantiate' [SOME (cons2ctyp cons)] [] exh_start;
+ val thm2 = rewrite_rule (map mk_meta_eq ex_defined_iffs) thm1;
+ val thm3 = rewrite_rule [mk_meta_eq conj_assoc] thm2;
+
+ (* first 3 rules replace "x = UU \/ P" with "rep$x = UU \/ P" *)
+ val tacs = [
+ rtac disjE 1,
+ etac (rep_defin' RS disjI1) 2,
+ etac disjI2 2,
+ rewrite_goals_tac [mk_meta_eq iso_swap],
+ rtac thm3 1];
+in
+ val exhaust = pg con_appls (mk_trp exh) tacs;
+ val casedist =
+ standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
+end;
+
+local
+ fun bind_fun t = Library.foldr mk_All (when_funs cons, t);
+ fun bound_fun i _ = Bound (length cons - i);
+ val when_app = list_ccomb (%%:(dname^"_when"), mapn bound_fun 1 cons);
+in
+ val when_strict =
+ let
+ val axs = [when_appl, mk_meta_eq rep_strict];
+ val goal = bind_fun (mk_trp (strict when_app));
+ val tacs = [resolve_tac [sscase1, ssplit1, strictify1] 1];
+ in pg axs goal tacs end;
+
+ val when_apps =
+ let
+ fun one_when n (con,args) =
+ let
+ val axs = when_appl :: con_appls;
+ val goal = bind_fun (lift_defined %: (nonlazy args,
+ mk_trp (when_app`(con_app con args) ===
+ list_ccomb (bound_fun n 0, map %# args))));
+ val tacs = [asm_simp_tac (HOLCF_ss addsimps [ax_abs_iso]) 1];
+ in pg axs goal tacs end;
+ in mapn one_when 1 cons end;
+end;
+val when_rews = when_strict :: when_apps;
+
+(* ----- theorems concerning the constructors, discriminators and selectors - *)
+
+local
+ fun dis_strict (con, _) =
+ let
+ val goal = mk_trp (strict (%%:(dis_name con)));
+ in pg axs_dis_def goal [rtac when_strict 1] end;
+
+ fun dis_app c (con, args) =
+ let
+ val lhs = %%:(dis_name c) ` con_app con args;
+ val rhs = %%:(if con = c then TT_N else FF_N);
+ val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
+ val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
+ in pg axs_dis_def goal tacs end;
+
+ val dis_apps = List.concat (map (fn (c,_) => map (dis_app c) cons) cons);
+
+ fun dis_defin (con, args) =
+ let
+ val goal = defined (%:x_name) ==> defined (%%:(dis_name con) `% x_name);
+ val tacs =
+ [rtac casedist 1,
+ contr_tac 1,
+ DETERM_UNTIL_SOLVED (CHANGED
+ (asm_simp_tac (HOLCF_ss addsimps dis_apps) 1))];
+ in pg [] goal tacs end;
+
+ val dis_stricts = map dis_strict cons;
+ val dis_defins = map dis_defin cons;
+in
+ val dis_rews = dis_stricts @ dis_defins @ dis_apps;
+end;
+
+local
+ fun mat_strict (con, _) =
+ let
+ val goal = mk_trp (strict (%%:(mat_name con)));
+ val tacs = [rtac when_strict 1];
+ in pg axs_mat_def goal tacs end;
+
+ val mat_stricts = map mat_strict cons;
+
+ fun one_mat c (con, args) =
+ let
+ val lhs = %%:(mat_name c) ` con_app con args;
+ val rhs =
+ if con = c
+ then %%:returnN ` mk_ctuple (map %# args)
+ else %%:failN;
+ val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
+ val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
+ in pg axs_mat_def goal tacs end;
+
+ val mat_apps =
+ List.concat (map (fn (c,_) => map (one_mat c) cons) cons);
+in
+ val mat_rews = mat_stricts @ mat_apps;
+end;
+
+local
+ fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
+
+ fun pat_lhs (con,args) = %%:branchN $ list_comb (%%:(pat_name con), ps args);
+
+ fun pat_rhs (con,[]) = %%:returnN ` ((%:"rhs") ` HOLogic.unit)
+ | pat_rhs (con,args) =
+ (%%:branchN $ foldr1 cpair_pat (ps args))
+ `(%:"rhs")`(mk_ctuple (map %# args));
+
+ fun pat_strict c =
+ let
+ val axs = branch_def :: axs_pat_def;
+ val goal = mk_trp (strict (pat_lhs c ` (%:"rhs")));
+ val tacs = [simp_tac (HOLCF_ss addsimps [when_strict]) 1];
+ in pg axs goal tacs end;
+
+ fun pat_app c (con, args) =
+ let
+ val axs = branch_def :: axs_pat_def;
+ val lhs = (pat_lhs c)`(%:"rhs")`(con_app con args);
+ val rhs = if con = fst c then pat_rhs c else %%:failN;
+ val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
+ val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
+ in pg axs goal tacs end;
+
+ val pat_stricts = map pat_strict cons;
+ val pat_apps = List.concat (map (fn c => map (pat_app c) cons) cons);
+in
+ val pat_rews = pat_stricts @ pat_apps;
+end;
+
+local
+ val rev_contrapos = thm "rev_contrapos";
+ fun con_strict (con, args) =
+ let
+ fun one_strict vn =
+ let
+ fun f arg = if vname arg = vn then UU else %# arg;
+ val goal = mk_trp (con_app2 con f args === UU);
+ val tacs = [asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1];
+ in pg con_appls goal tacs end;
+ in map one_strict (nonlazy args) end;
+
+ fun con_defin (con, args) =
+ let
+ val concl = mk_trp (defined (con_app con args));
+ val goal = lift_defined %: (nonlazy args, concl);
+ val tacs = [
+ rtac rev_contrapos 1,
+ eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1,
+ asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
+ in pg [] goal tacs end;
+in
+ val con_stricts = List.concat (map con_strict cons);
+ val con_defins = map con_defin cons;
+ val con_rews = con_stricts @ con_defins;
+end;
+
+local
+ val rules =
+ [compact_sinl, compact_sinr, compact_spair, compact_up, compact_ONE];
+ fun con_compact (con, args) =
+ let
+ val concl = mk_trp (%%:compactN $ con_app con args);
+ val goal = lift (fn x => %%:compactN $ %#x) (args, concl);
+ val tacs = [
+ rtac (iso_locale RS iso_compact_abs) 1,
+ REPEAT (resolve_tac rules 1 ORELSE atac 1)];
+ in pg con_appls goal tacs end;
+in
+ val con_compacts = map con_compact cons;
+end;
+
+local
+ fun one_sel sel =
+ pg axs_sel_def (mk_trp (strict (%%:sel)))
+ [simp_tac (HOLCF_ss addsimps when_rews) 1];
+
+ fun sel_strict (_, args) =
+ List.mapPartial (Option.map one_sel o sel_of) args;
+in
+ val sel_stricts = List.concat (map sel_strict cons);
+end;
+
+local
+ fun sel_app_same c n sel (con, args) =
+ let
+ val nlas = nonlazy args;
+ val vns = map vname args;
+ val vnn = List.nth (vns, n);
+ val nlas' = List.filter (fn v => v <> vnn) nlas;
+ val lhs = (%%:sel)`(con_app con args);
+ val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn));
+ val tacs1 =
+ if vnn mem nlas
+ then [case_UU_tac (when_rews @ con_stricts) 1 vnn]
+ else [];
+ val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
+ in pg axs_sel_def goal (tacs1 @ tacs2) end;
+
+ fun sel_app_diff c n sel (con, args) =
+ let
+ val nlas = nonlazy args;
+ val goal = mk_trp (%%:sel ` con_app con args === UU);
+ val tacs1 = map (case_UU_tac (when_rews @ con_stricts) 1) nlas;
+ val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
+ in pg axs_sel_def goal (tacs1 @ tacs2) end;
+
+ fun sel_app c n sel (con, args) =
+ if con = c
+ then sel_app_same c n sel (con, args)
+ else sel_app_diff c n sel (con, args);
+
+ fun one_sel c n sel = map (sel_app c n sel) cons;
+ fun one_sel' c n arg = Option.map (one_sel c n) (sel_of arg);
+ fun one_con (c, args) =
+ List.concat (List.mapPartial I (mapn (one_sel' c) 0 args));
+in
+ val sel_apps = List.concat (map one_con cons);
+end;
+
+local
+ fun sel_defin sel =
+ let
+ val goal = defined (%:x_name) ==> defined (%%:sel`%x_name);
+ val tacs = [
+ rtac casedist 1,
+ contr_tac 1,
+ DETERM_UNTIL_SOLVED (CHANGED
+ (asm_simp_tac (HOLCF_ss addsimps sel_apps) 1))];
+ in pg [] goal tacs end;
+in
+ val sel_defins =
+ if length cons = 1
+ then List.mapPartial (fn arg => Option.map sel_defin (sel_of arg))
+ (filter_out is_lazy (snd (hd cons)))
+ else [];
+end;
+
+val sel_rews = sel_stricts @ sel_defins @ sel_apps;
+val rev_contrapos = thm "rev_contrapos";
+
+val distincts_le =
+ let
+ fun dist (con1, args1) (con2, args2) =
+ let
+ val goal = lift_defined %: (nonlazy args1,
+ mk_trp (con_app con1 args1 ~<< con_app con2 args2));
+ val tacs = [
+ rtac rev_contrapos 1,
+ eres_inst_tac [("f", dis_name con1)] monofun_cfun_arg 1]
+ @ map (case_UU_tac (con_stricts @ dis_rews) 1) (nonlazy args2)
+ @ [asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
+ in pg [] goal tacs end;
+
+ fun distinct (con1, args1) (con2, args2) =
+ let
+ val arg1 = (con1, args1);
+ val arg2 =
+ (con2, ListPair.map (fn (arg,vn) => upd_vname (K vn) arg)
+ (args2, Name.variant_list (map vname args1) (map vname args2)));
+ in [dist arg1 arg2, dist arg2 arg1] end;
+ fun distincts [] = []
+ | distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
+ in distincts cons end;
+val dist_les = List.concat (List.concat distincts_le);
+val dist_eqs =
+ let
+ fun distinct (_,args1) ((_,args2), leqs) =
+ let
+ val (le1,le2) = (hd leqs, hd(tl leqs));
+ val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI)
+ in
+ if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else
+ if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else
+ [eq1, eq2]
+ end;
+ fun distincts [] = []
+ | distincts ((c,leqs)::cs) = List.concat
+ (ListPair.map (distinct c) ((map #1 cs),leqs)) @
+ distincts cs;
+ in map standard (distincts (cons ~~ distincts_le)) end;
+
+local
+ fun pgterm rel con args =
+ let
+ fun append s = upd_vname (fn v => v^s);
+ val (largs, rargs) = (args, map (append "'") args);
+ val concl =
+ foldr1 mk_conj (ListPair.map rel (map %# largs, map %# rargs));
+ val prem = rel (con_app con largs, con_app con rargs);
+ val sargs = case largs of [_] => [] | _ => nonlazy args;
+ val prop = lift_defined %: (sargs, mk_trp (prem === concl));
+ in pg con_appls prop end;
+ val cons' = List.filter (fn (_,args) => args<>[]) cons;
+in
+ val inverts =
+ let
+ val abs_less = ax_abs_iso RS (allI RS injection_less);
+ val tacs =
+ [asm_full_simp_tac (HOLCF_ss addsimps [abs_less, spair_less]) 1];
+ in map (fn (con, args) => pgterm (op <<) con args tacs) cons' end;
+
+ val injects =
+ let
+ val abs_eq = ax_abs_iso RS (allI RS injection_eq);
+ val tacs = [asm_full_simp_tac (HOLCF_ss addsimps [abs_eq, spair_eq]) 1];
+ in map (fn (con, args) => pgterm (op ===) con args tacs) cons' end;
+end;
+
+(* ----- theorems concerning one induction step ----------------------------- *)
+
+val copy_strict =
+ let
+ val goal = mk_trp (strict (dc_copy `% "f"));
+ val tacs = [asm_simp_tac (HOLCF_ss addsimps [abs_strict, when_strict]) 1];
+ in pg [ax_copy_def] goal tacs end;
+
+local
+ fun copy_app (con, args) =
+ let
+ val lhs = dc_copy`%"f"`(con_app con args);
+ val rhs = con_app2 con (app_rec_arg (cproj (%:"f") eqs)) args;
+ val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
+ val args' = List.filter (fn a => not (is_rec a orelse is_lazy a)) args;
+ val stricts = abs_strict::when_strict::con_stricts;
+ val tacs1 = map (case_UU_tac stricts 1 o vname) args';
+ val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_apps) 1];
+ in pg [ax_copy_def] goal (tacs1 @ tacs2) end;
+in
+ val copy_apps = map copy_app cons;
+end;
+
+local
+ fun one_strict (con, args) =
+ let
+ val goal = mk_trp (dc_copy`UU`(con_app con args) === UU);
+ val rews = copy_strict :: copy_apps @ con_rews;
+ val tacs = map (case_UU_tac rews 1) (nonlazy args) @
+ [asm_simp_tac (HOLCF_ss addsimps rews) 1];
+ in pg [] goal tacs end;
+
+ fun has_nonlazy_rec (_, args) = exists is_nonlazy_rec args;
+in
+ val copy_stricts = map one_strict (List.filter has_nonlazy_rec cons);
+end;
+
+val copy_rews = copy_strict :: copy_apps @ copy_stricts;
+
+in
+ thy
+ |> Theory.add_path (Sign.base_name dname)
+ |> (snd o (PureThy.add_thmss (map Thm.no_attributes [
+ ("iso_rews" , iso_rews ),
+ ("exhaust" , [exhaust] ),
+ ("casedist" , [casedist]),
+ ("when_rews", when_rews ),
+ ("compacts", con_compacts),
+ ("con_rews", con_rews),
+ ("sel_rews", sel_rews),
+ ("dis_rews", dis_rews),
+ ("pat_rews", pat_rews),
+ ("dist_les", dist_les),
+ ("dist_eqs", dist_eqs),
+ ("inverts" , inverts ),
+ ("injects" , injects ),
+ ("copy_rews", copy_rews)])))
+ |> (snd o PureThy.add_thmss
+ [(("match_rews", mat_rews), [Simplifier.simp_add])])
+ |> Theory.parent_path
+ |> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
+ pat_rews @ dist_les @ dist_eqs @ copy_rews)
+end; (* let *)
+
+fun comp_theorems (comp_dnam, eqs: eq list) thy =
+let
+val dnames = map (fst o fst) eqs;
+val conss = map snd eqs;
+val comp_dname = Sign.full_name thy comp_dnam;
+
+val d = writeln("Proving induction properties of domain "^comp_dname^" ...");
+val pg = pg' thy;
+
+(* ----- getting the composite axiom and definitions ------------------------ *)
+
+local
+ fun ga s dn = get_thm thy (Name (dn ^ "." ^ s));
+in
+ val axs_reach = map (ga "reach" ) dnames;
+ val axs_take_def = map (ga "take_def" ) dnames;
+ val axs_finite_def = map (ga "finite_def") dnames;
+ val ax_copy2_def = ga "copy_def" comp_dnam;
+ val ax_bisim_def = ga "bisim_def" comp_dnam;
+end;
+
+local
+ fun gt s dn = get_thm thy (Name (dn ^ "." ^ s));
+ fun gts s dn = get_thms thy (Name (dn ^ "." ^ s));
+in
+ val cases = map (gt "casedist" ) dnames;
+ val con_rews = List.concat (map (gts "con_rews" ) dnames);
+ val copy_rews = List.concat (map (gts "copy_rews") dnames);
+end;
+
+fun dc_take dn = %%:(dn^"_take");
+val x_name = idx_name dnames "x";
+val P_name = idx_name dnames "P";
+val n_eqs = length eqs;
+
+(* ----- theorems concerning finite approximation and finite induction ------ *)
+
+local
+ val iterate_Cprod_ss = simpset_of (theory "Fix");
+ val copy_con_rews = copy_rews @ con_rews;
+ val copy_take_defs =
+ (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
+ val take_stricts =
+ let
+ fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n");
+ val goal = mk_trp (foldr1 mk_conj (map one_eq eqs));
+ val tacs = [
+ induct_tac "n" 1,
+ simp_tac iterate_Cprod_ss 1,
+ asm_simp_tac (iterate_Cprod_ss addsimps copy_rews) 1];
+ in pg copy_take_defs goal tacs end;
+
+ val take_stricts' = rewrite_rule copy_take_defs take_stricts;
+ fun take_0 n dn =
+ let
+ val goal = mk_trp ((dc_take dn $ %%:"HOL.zero") `% x_name n === UU);
+ in pg axs_take_def goal [simp_tac iterate_Cprod_ss 1] end;
+ val take_0s = mapn take_0 1 dnames;
+ val c_UU_tac = case_UU_tac (take_stricts'::copy_con_rews) 1;
+ val take_apps =
+ let
+ fun mk_eqn dn (con, args) =
+ let
+ fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
+ val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args);
+ val rhs = con_app2 con (app_rec_arg mk_take) args;
+ in Library.foldr mk_all (map vname args, lhs === rhs) end;
+ fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons;
+ val goal = mk_trp (foldr1 mk_conj (List.concat (map mk_eqns eqs)));
+ val simps = List.filter (has_fewer_prems 1) copy_rews;
+ fun con_tac (con, args) =
+ if nonlazy_rec args = []
+ then all_tac
+ else EVERY (map c_UU_tac (nonlazy_rec args)) THEN
+ asm_full_simp_tac (HOLCF_ss addsimps copy_rews) 1;
+ fun eq_tacs ((dn, _), cons) = map con_tac cons;
+ val tacs =
+ simp_tac iterate_Cprod_ss 1 ::
+ induct_tac "n" 1 ::
+ simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 ::
+ asm_full_simp_tac (HOLCF_ss addsimps simps) 1 ::
+ TRY (safe_tac HOL_cs) ::
+ List.concat (map eq_tacs eqs);
+ in pg copy_take_defs goal tacs end;
+in
+ val take_rews = map standard
+ (atomize take_stricts @ take_0s @ atomize take_apps);
+end; (* local *)
+
+local
+ fun one_con p (con,args) =
+ let
+ fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg;
+ val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args);
+ val t2 = lift ind_hyp (List.filter is_rec args, t1);
+ val t3 = lift_defined (bound_arg (map vname args)) (nonlazy args, t2);
+ in Library.foldr mk_All (map vname args, t3) end;
+
+ fun one_eq ((p, cons), concl) =
+ mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl);
+
+ fun ind_term concf = Library.foldr one_eq
+ (mapn (fn n => fn x => (P_name n, x)) 1 conss,
+ mk_trp (foldr1 mk_conj (mapn concf 1 dnames)));
+ val take_ss = HOL_ss addsimps take_rews;
+ fun quant_tac i = EVERY
+ (mapn (fn n => fn _ => res_inst_tac [("x", x_name n)] spec i) 1 dnames);
+
+ fun ind_prems_tac prems = EVERY
+ (List.concat (map (fn cons =>
+ (resolve_tac prems 1 ::
+ List.concat (map (fn (_,args) =>
+ resolve_tac prems 1 ::
+ map (K(atac 1)) (nonlazy args) @
+ map (K(atac 1)) (List.filter is_rec args))
+ cons)))
+ conss));
+ local
+ (* check whether every/exists constructor of the n-th part of the equation:
+ it has a possibly indirectly recursive argument that isn't/is possibly
+ indirectly lazy *)
+ fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg =>
+ is_rec arg andalso not(rec_of arg mem ns) andalso
+ ((rec_of arg = n andalso nfn(lazy_rec orelse is_lazy arg)) orelse
+ rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns)
+ (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
+ ) o snd) cons;
+ fun all_rec_to ns = rec_to forall not all_rec_to ns;
+ fun warn (n,cons) =
+ if all_rec_to [] false (n,cons)
+ then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true)
+ else false;
+ fun lazy_rec_to ns = rec_to exists I lazy_rec_to ns;
+
+ in
+ val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
+ val is_emptys = map warn n__eqs;
+ val is_finite = forall (not o lazy_rec_to [] false) n__eqs;
+ end;
+in (* local *)
+ val finite_ind =
+ let
+ fun concf n dn = %:(P_name n) $ (dc_take dn $ %:"n" `%(x_name n));
+ val goal = ind_term concf;
+
+ fun tacf prems =
+ let
+ val tacs1 = [
+ quant_tac 1,
+ simp_tac HOL_ss 1,
+ induct_tac "n" 1,
+ simp_tac (take_ss addsimps prems) 1,
+ TRY (safe_tac HOL_cs)];
+ fun arg_tac arg =
+ case_UU_tac (prems @ con_rews) 1
+ (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
+ fun con_tacs (con, args) =
+ asm_simp_tac take_ss 1 ::
+ map arg_tac (List.filter is_nonlazy_rec args) @
+ [resolve_tac prems 1] @
+ map (K (atac 1)) (nonlazy args) @
+ map (K (etac spec 1)) (List.filter is_rec args);
+ fun cases_tacs (cons, cases) =
+ res_inst_tac [("x","x")] cases 1 ::
+ asm_simp_tac (take_ss addsimps prems) 1 ::
+ List.concat (map con_tacs cons);
+ in
+ tacs1 @ List.concat (map cases_tacs (conss ~~ cases))
+ end;
+ in pg'' thy [] goal tacf end;
+
+ val take_lemmas =
+ let
+ fun take_lemma n (dn, ax_reach) =
+ let
+ val lhs = dc_take dn $ Bound 0 `%(x_name n);
+ val rhs = dc_take dn $ Bound 0 `%(x_name n^"'");
+ val concl = mk_trp (%:(x_name n) === %:(x_name n^"'"));
+ val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl;
+ fun tacf prems = [
+ res_inst_tac [("t", x_name n )] (ax_reach RS subst) 1,
+ res_inst_tac [("t", x_name n^"'")] (ax_reach RS subst) 1,
+ stac fix_def2 1,
+ REPEAT (CHANGED
+ (rtac (contlub_cfun_arg RS ssubst) 1 THEN chain_tac 1)),
+ stac contlub_cfun_fun 1,
+ stac contlub_cfun_fun 2,
+ rtac lub_equal 3,
+ chain_tac 1,
+ rtac allI 1,
+ resolve_tac prems 1];
+ in pg'' thy axs_take_def goal tacf end;
+ in mapn take_lemma 1 (dnames ~~ axs_reach) end;
+
+(* ----- theorems concerning finiteness and induction ----------------------- *)
+
+ val (finites, ind) =
+ if is_finite
+ then (* finite case *)
+ let
+ fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %:"x" === %:"x");
+ fun dname_lemma dn =
+ let
+ val prem1 = mk_trp (defined (%:"x"));
+ val disj1 = mk_all ("n", dc_take dn $ Bound 0 ` %:"x" === UU);
+ val prem2 = mk_trp (mk_disj (disj1, take_enough dn));
+ val concl = mk_trp (take_enough dn);
+ val goal = prem1 ===> prem2 ===> concl;
+ val tacs = [
+ etac disjE 1,
+ etac notE 1,
+ resolve_tac take_lemmas 1,
+ asm_simp_tac take_ss 1,
+ atac 1];
+ in pg [] goal tacs end;
+ val finite_lemmas1a = map dname_lemma dnames;
+
+ val finite_lemma1b =
+ let
+ fun mk_eqn n ((dn, args), _) =
+ let
+ val disj1 = dc_take dn $ Bound 1 ` Bound 0 === UU;
+ val disj2 = dc_take dn $ Bound 1 ` Bound 0 === Bound 0;
+ in
+ mk_constrainall
+ (x_name n, Type (dn,args), mk_disj (disj1, disj2))
+ end;
+ val goal =
+ mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs)));
+ fun arg_tacs vn = [
+ eres_inst_tac [("x", vn)] all_dupE 1,
+ etac disjE 1,
+ asm_simp_tac (HOL_ss addsimps con_rews) 1,
+ asm_simp_tac take_ss 1];
+ fun con_tacs (con, args) =
+ asm_simp_tac take_ss 1 ::
+ List.concat (map arg_tacs (nonlazy_rec args));
+ fun foo_tacs n (cons, cases) =
+ simp_tac take_ss 1 ::
+ rtac allI 1 ::
+ res_inst_tac [("x",x_name n)] cases 1 ::
+ asm_simp_tac take_ss 1 ::
+ List.concat (map con_tacs cons);
+ val tacs =
+ rtac allI 1 ::
+ induct_tac "n" 1 ::
+ simp_tac take_ss 1 ::
+ TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) ::
+ List.concat (mapn foo_tacs 1 (conss ~~ cases));
+ in pg [] goal tacs end;
+
+ fun one_finite (dn, l1b) =
+ let
+ val goal = mk_trp (%%:(dn^"_finite") $ %:"x");
+ val tacs = [
+ case_UU_tac take_rews 1 "x",
+ eresolve_tac finite_lemmas1a 1,
+ step_tac HOL_cs 1,
+ step_tac HOL_cs 1,
+ cut_facts_tac [l1b] 1,
+ fast_tac HOL_cs 1];
+ in pg axs_finite_def goal tacs end;
+
+ val finites = map one_finite (dnames ~~ atomize finite_lemma1b);
+ val ind =
+ let
+ fun concf n dn = %:(P_name n) $ %:(x_name n);
+ fun tacf prems =
+ let
+ fun finite_tacs (finite, fin_ind) = [
+ rtac(rewrite_rule axs_finite_def finite RS exE)1,
+ etac subst 1,
+ rtac fin_ind 1,
+ ind_prems_tac prems];
+ in
+ TRY (safe_tac HOL_cs) ::
+ List.concat (map finite_tacs (finites ~~ atomize finite_ind))
+ end;
+ in pg'' thy [] (ind_term concf) tacf end;
+ in (finites, ind) end (* let *)
+
+ else (* infinite case *)
+ let
+ fun one_finite n dn =
+ read_instantiate_sg thy
+ [("P",dn^"_finite "^x_name n)] excluded_middle;
+ val finites = mapn one_finite 1 dnames;
+
+ val goal =
+ let
+ fun one_adm n _ = mk_trp (%%:admN $ %:(P_name n));
+ fun concf n dn = %:(P_name n) $ %:(x_name n);
+ in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end;
+ fun tacf prems =
+ map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [
+ quant_tac 1,
+ rtac (adm_impl_admw RS wfix_ind) 1,
+ REPEAT_DETERM (rtac adm_all2 1),
+ REPEAT_DETERM (
+ TRY (rtac adm_conj 1) THEN
+ rtac adm_subst 1 THEN
+ cont_tacR 1 THEN resolve_tac prems 1),
+ strip_tac 1,
+ rtac (rewrite_rule axs_take_def finite_ind) 1,
+ ind_prems_tac prems];
+ val ind = (pg'' thy [] goal tacf
+ handle ERROR _ =>
+ (warning "Cannot prove infinite induction rule"; refl));
+ in (finites, ind) end;
+end; (* local *)
+
+(* ----- theorem concerning coinduction ------------------------------------- *)
+
+local
+ val xs = mapn (fn n => K (x_name n)) 1 dnames;
+ fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
+ val take_ss = HOL_ss addsimps take_rews;
+ val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")"));
+ val coind_lemma =
+ let
+ fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1;
+ fun mk_eqn n dn =
+ (dc_take dn $ %:"n" ` bnd_arg n 0) ===
+ (dc_take dn $ %:"n" ` bnd_arg n 1);
+ fun mk_all2 (x,t) = mk_all (x, mk_all (x^"'", t));
+ val goal =
+ mk_trp (mk_imp (%%:(comp_dname^"_bisim") $ %:"R",
+ Library.foldr mk_all2 (xs,
+ Library.foldr mk_imp (mapn mk_prj 0 dnames,
+ foldr1 mk_conj (mapn mk_eqn 0 dnames)))));
+ fun x_tacs n x = [
+ rotate_tac (n+1) 1,
+ etac all2E 1,
+ eres_inst_tac [("P1", sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
+ TRY (safe_tac HOL_cs),
+ REPEAT (CHANGED (asm_simp_tac take_ss 1))];
+ val tacs = [
+ rtac impI 1,
+ induct_tac "n" 1,
+ simp_tac take_ss 1,
+ safe_tac HOL_cs] @
+ List.concat (mapn x_tacs 0 xs);
+ in pg [ax_bisim_def] goal tacs end;
+in
+ val coind =
+ let
+ fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'"));
+ fun mk_eqn x = %:x === %:(x^"'");
+ val goal =
+ mk_trp (%%:(comp_dname^"_bisim") $ %:"R") ===>
+ Logic.list_implies (mapn mk_prj 0 xs,
+ mk_trp (foldr1 mk_conj (map mk_eqn xs)));
+ val tacs =
+ TRY (safe_tac HOL_cs) ::
+ List.concat (map (fn take_lemma => [
+ rtac take_lemma 1,
+ cut_facts_tac [coind_lemma] 1,
+ fast_tac HOL_cs 1])
+ take_lemmas);
+ in pg [] goal tacs end;
+end; (* local *)
+
+in thy |> Theory.add_path comp_dnam
+ |> (snd o (PureThy.add_thmss (map Thm.no_attributes [
+ ("take_rews" , take_rews ),
+ ("take_lemmas", take_lemmas),
+ ("finites" , finites ),
+ ("finite_ind", [finite_ind]),
+ ("ind" , [ind ]),
+ ("coind" , [coind ])])))
+ |> Theory.parent_path |> rpair take_rews
+end; (* let *)
+end; (* local *)
+end; (* struct *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/fixrec_package.ML Thu May 31 14:01:58 2007 +0200
@@ -0,0 +1,317 @@
+(* Title: HOLCF/Tools/fixrec_package.ML
+ ID: $Id$
+ Author: Amber Telfer and Brian Huffman
+
+Recursive function definition package for HOLCF.
+*)
+
+signature FIXREC_PACKAGE =
+sig
+ val legacy_infer_term: theory -> term -> term
+ val legacy_infer_prop: theory -> term -> term
+ val add_fixrec: bool -> ((string * Attrib.src list) * string) list list -> theory -> theory
+ val add_fixrec_i: bool -> ((string * attribute list) * term) list list -> theory -> theory
+ val add_fixpat: (string * Attrib.src list) * string list -> theory -> theory
+ val add_fixpat_i: (string * attribute list) * term list -> theory -> theory
+end;
+
+structure FixrecPackage: FIXREC_PACKAGE =
+struct
+
+(* legacy type inference *)
+
+fun legacy_infer_term thy t =
+ singleton (ProofContext.infer_types (ProofContext.init thy)) (Sign.intern_term thy t);
+
+fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain t propT);
+
+
+val fix_eq2 = thm "fix_eq2";
+val def_fix_ind = thm "def_fix_ind";
+
+
+fun fixrec_err s = error ("fixrec definition error:\n" ^ s);
+fun fixrec_eq_err thy s eq =
+ fixrec_err (s ^ "\nin\n" ^ quote (Sign.string_of_term thy eq));
+
+(* ->> is taken from holcf_logic.ML *)
+(* TODO: fix dependencies so we can import HOLCFLogic here *)
+infixr 6 ->>;
+fun S ->> T = Type ("Cfun.->",[S,T]);
+
+(* extern_name is taken from domain/library.ML *)
+fun extern_name con = case Symbol.explode con of
+ ("o"::"p"::" "::rest) => implode rest
+ | _ => con;
+
+val mk_trp = HOLogic.mk_Trueprop;
+
+(* splits a cterm into the right and lefthand sides of equality *)
+fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
+
+(* similar to Thm.head_of, but for continuous application *)
+fun chead_of (Const("Cfun.Rep_CFun",_)$f$t) = chead_of f
+ | chead_of u = u;
+
+(* these are helpful functions copied from HOLCF/domain/library.ML *)
+fun %: s = Free(s,dummyT);
+fun %%: s = Const(s,dummyT);
+infix 0 ==; fun S == T = %%:"==" $ S $ T;
+infix 1 ===; fun S === T = %%:"op =" $ S $ T;
+infix 9 ` ; fun f ` x = %%:"Cfun.Rep_CFun" $ f $ x;
+
+(* builds the expression (LAM v. rhs) *)
+fun big_lambda v rhs = %%:"Cfun.Abs_CFun"$(Term.lambda v rhs);
+
+(* builds the expression (LAM v1 v2 .. vn. rhs) *)
+fun big_lambdas [] rhs = rhs
+ | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs);
+
+(* builds the expression (LAM <v1,v2,..,vn>. rhs) *)
+fun lambda_ctuple [] rhs = big_lambda (%:"unit") rhs
+ | lambda_ctuple (v::[]) rhs = big_lambda v rhs
+ | lambda_ctuple (v::vs) rhs =
+ %%:"Cprod.csplit"`(big_lambda v (lambda_ctuple vs rhs));
+
+(* builds the expression <v1,v2,..,vn> *)
+fun mk_ctuple [] = %%:"UU"
+| mk_ctuple (t::[]) = t
+| mk_ctuple (t::ts) = %%:"Cprod.cpair"`t`(mk_ctuple ts);
+
+(*************************************************************************)
+(************* fixed-point definitions and unfolding theorems ************)
+(*************************************************************************)
+
+fun add_fixdefs eqs thy =
+ let
+ val (lhss,rhss) = ListPair.unzip (map dest_eqs eqs);
+ val fixpoint = %%:"Fix.fix"`lambda_ctuple lhss (mk_ctuple rhss);
+
+ fun one_def (l as Const(n,T)) r =
+ let val b = Sign.base_name n in (b, (b^"_def", l == r)) end
+ | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form";
+ fun defs [] _ = []
+ | defs (l::[]) r = [one_def l r]
+ | defs (l::ls) r = one_def l (%%:"Cprod.cfst"`r) :: defs ls (%%:"Cprod.csnd"`r);
+ val (names, pre_fixdefs) = ListPair.unzip (defs lhss fixpoint);
+
+ val fixdefs = map (apsnd (legacy_infer_prop thy)) pre_fixdefs;
+ val (fixdef_thms, thy') =
+ PureThy.add_defs_i false (map Thm.no_attributes fixdefs) thy;
+ val ctuple_fixdef_thm = foldr1 (fn (x,y) => cpair_equalI OF [x,y]) fixdef_thms;
+
+ val ctuple_unfold = legacy_infer_term thy' (mk_trp (mk_ctuple lhss === mk_ctuple rhss));
+ val ctuple_unfold_thm = Goal.prove_global thy' [] [] ctuple_unfold
+ (fn _ => EVERY [rtac (ctuple_fixdef_thm RS fix_eq2 RS trans) 1,
+ simp_tac (simpset_of thy') 1]);
+ val ctuple_induct_thm =
+ (space_implode "_" names ^ "_induct", ctuple_fixdef_thm RS def_fix_ind);
+
+ fun unfolds [] thm = []
+ | unfolds (n::[]) thm = [(n^"_unfold", thm)]
+ | unfolds (n::ns) thm = let
+ val thmL = thm RS cpair_eqD1;
+ val thmR = thm RS cpair_eqD2;
+ in (n^"_unfold", thmL) :: unfolds ns thmR end;
+ val unfold_thms = unfolds names ctuple_unfold_thm;
+ val thms = ctuple_induct_thm :: unfold_thms;
+ val (_, thy'') = PureThy.add_thms (map Thm.no_attributes thms) thy';
+ in
+ (thy'', names, fixdef_thms, map snd unfold_thms)
+ end;
+
+(*************************************************************************)
+(*********** monadic notation and pattern matching compilation ***********)
+(*************************************************************************)
+
+fun add_names (Const(a,_), bs) = insert (op =) (Sign.base_name a) bs
+ | add_names (Free(a,_) , bs) = insert (op =) a bs
+ | add_names (f $ u , bs) = add_names (f, add_names(u, bs))
+ | add_names (Abs(a,_,t), bs) = add_names (t, insert (op =) a bs)
+ | add_names (_ , bs) = bs;
+
+fun add_terms ts xs = foldr add_names xs ts;
+
+(* builds a monadic term for matching a constructor pattern *)
+fun pre_build pat rhs vs taken =
+ case pat of
+ Const("Cfun.Rep_CFun",_)$f$(v as Free(n,T)) =>
+ pre_build f rhs (v::vs) taken
+ | Const("Cfun.Rep_CFun",_)$f$x =>
+ let val (rhs', v, taken') = pre_build x rhs [] taken;
+ in pre_build f rhs' (v::vs) taken' end
+ | Const(c,T) =>
+ let
+ val n = Name.variant taken "v";
+ fun result_type (Type("Cfun.->",[_,T])) (x::xs) = result_type T xs
+ | result_type T _ = T;
+ val v = Free(n, result_type T vs);
+ val m = "match_"^(extern_name(Sign.base_name c));
+ val k = lambda_ctuple vs rhs;
+ in
+ (%%:"Fixrec.bind"`(%%:m`v)`k, v, n::taken)
+ end
+ | Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n)
+ | _ => fixrec_err "pre_build: invalid pattern";
+
+(* builds a monadic term for matching a function definition pattern *)
+(* returns (name, arity, matcher) *)
+fun building pat rhs vs taken =
+ case pat of
+ Const("Cfun.Rep_CFun", _)$f$(v as Free(n,T)) =>
+ building f rhs (v::vs) taken
+ | Const("Cfun.Rep_CFun", _)$f$x =>
+ let val (rhs', v, taken') = pre_build x rhs [] taken;
+ in building f rhs' (v::vs) taken' end
+ | Const(name,_) => (name, length vs, big_lambdas vs rhs)
+ | _ => fixrec_err "function is not declared as constant in theory";
+
+fun match_eq eq =
+ let val (lhs,rhs) = dest_eqs eq;
+ in building lhs (%%:"Fixrec.return"`rhs) [] (add_terms [eq] []) end;
+
+(* returns the sum (using +++) of the terms in ms *)
+(* also applies "run" to the result! *)
+fun fatbar arity ms =
+ let
+ fun unLAM 0 t = t
+ | unLAM n (_$Abs(_,_,t)) = unLAM (n-1) t
+ | unLAM _ _ = fixrec_err "fatbar: internal error, not enough LAMs";
+ fun reLAM 0 t = t
+ | reLAM n t = reLAM (n-1) (%%:"Cfun.Abs_CFun" $ Abs("",dummyT,t));
+ fun mplus (x,y) = %%:"Fixrec.mplus"`x`y;
+ val msum = foldr1 mplus (map (unLAM arity) ms);
+ in
+ reLAM arity (%%:"Fixrec.run"`msum)
+ end;
+
+fun unzip3 [] = ([],[],[])
+ | unzip3 ((x,y,z)::ts) =
+ let val (xs,ys,zs) = unzip3 ts
+ in (x::xs, y::ys, z::zs) end;
+
+(* this is the pattern-matching compiler function *)
+fun compile_pats eqs =
+ let
+ val ((n::names),(a::arities),mats) = unzip3 (map match_eq eqs);
+ val cname = if forall (fn x => n=x) names then n
+ else fixrec_err "all equations in block must define the same function";
+ val arity = if forall (fn x => a=x) arities then a
+ else fixrec_err "all equations in block must have the same arity";
+ val rhs = fatbar arity mats;
+ in
+ mk_trp (%%:cname === rhs)
+ end;
+
+(*************************************************************************)
+(********************** Proving associated theorems **********************)
+(*************************************************************************)
+
+(* proves a block of pattern matching equations as theorems, using unfold *)
+fun make_simps thy (unfold_thm, eqns) =
+ let
+ val tacs = [rtac (unfold_thm RS ssubst_lhs) 1, asm_simp_tac (simpset_of thy) 1];
+ fun prove_term t = Goal.prove_global thy [] [] t (K (EVERY tacs));
+ fun prove_eqn ((name, eqn_t), atts) = ((name, prove_term eqn_t), atts);
+ in
+ map prove_eqn eqns
+ end;
+
+(*************************************************************************)
+(************************* Main fixrec function **************************)
+(*************************************************************************)
+
+fun gen_add_fixrec prep_prop prep_attrib strict blocks thy =
+ let
+ val eqns = List.concat blocks;
+ val lengths = map length blocks;
+
+ val ((names, srcss), strings) = apfst split_list (split_list eqns);
+ val atts = map (map (prep_attrib thy)) srcss;
+ val eqn_ts = map (prep_prop thy) strings;
+ val rec_ts = map (fn eq => chead_of (fst (dest_eqs (Logic.strip_imp_concl eq)))
+ handle TERM _ => fixrec_eq_err thy "not a proper equation" eq) eqn_ts;
+ val (_, eqn_ts') = OldInductivePackage.unify_consts thy rec_ts eqn_ts;
+
+ fun unconcat [] _ = []
+ | unconcat (n::ns) xs = List.take (xs,n) :: unconcat ns (List.drop (xs,n));
+ val pattern_blocks = unconcat lengths (map Logic.strip_imp_concl eqn_ts');
+ val compiled_ts = map (legacy_infer_term thy o compile_pats) pattern_blocks;
+ val (thy', cnames, fixdef_thms, unfold_thms) = add_fixdefs compiled_ts thy;
+ in
+ if strict then let (* only prove simp rules if strict = true *)
+ val eqn_blocks = unconcat lengths ((names ~~ eqn_ts') ~~ atts);
+ val simps = List.concat (map (make_simps thy') (unfold_thms ~~ eqn_blocks));
+ val (simp_thms, thy'') = PureThy.add_thms simps thy';
+
+ val simp_names = map (fn name => name^"_simps") cnames;
+ val simp_attribute = rpair [Simplifier.simp_add];
+ val simps' = map simp_attribute (simp_names ~~ unconcat lengths simp_thms);
+ in
+ (snd o PureThy.add_thmss simps') thy''
+ end
+ else thy'
+ end;
+
+val add_fixrec = gen_add_fixrec Sign.read_prop Attrib.attribute;
+val add_fixrec_i = gen_add_fixrec Sign.cert_prop (K I);
+
+
+(*************************************************************************)
+(******************************** Fixpat *********************************)
+(*************************************************************************)
+
+fun fix_pat thy t =
+ let
+ val T = fastype_of t;
+ val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
+ val cname = case chead_of t of Const(c,_) => c | _ =>
+ fixrec_err "function is not declared as constant in theory";
+ val unfold_thm = PureThy.get_thm thy (Name (cname^"_unfold"));
+ val simp = Goal.prove_global thy [] [] eq
+ (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
+ in simp end;
+
+fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy =
+ let
+ val atts = map (prep_attrib thy) srcs;
+ val ts = map (prep_term thy) strings;
+ val simps = map (fix_pat thy) ts;
+ in
+ (snd o PureThy.add_thmss [((name, simps), atts)]) thy
+ end;
+
+val add_fixpat = gen_add_fixpat Sign.read_term Attrib.attribute;
+val add_fixpat_i = gen_add_fixpat Sign.cert_term (K I);
+
+
+(*************************************************************************)
+(******************************** Parsers ********************************)
+(*************************************************************************)
+
+local structure P = OuterParse and K = OuterKeyword in
+
+val fixrec_eqn = SpecParse.opt_thm_name ":" -- P.prop;
+
+val fixrec_strict = P.opt_keyword "permissive" >> not;
+
+val fixrec_decl = fixrec_strict -- P.and_list1 (Scan.repeat1 fixrec_eqn);
+
+(* this builds a parser for a new keyword, fixrec, whose functionality
+is defined by add_fixrec *)
+val fixrecP =
+ OuterSyntax.command "fixrec" "define recursive functions (HOLCF)" K.thy_decl
+ (fixrec_decl >> (Toplevel.theory o uncurry add_fixrec));
+
+(* fixpat parser *)
+val fixpat_decl = SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop;
+
+val fixpatP =
+ OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
+ (fixpat_decl >> (Toplevel.theory o add_fixpat));
+
+val _ = OuterSyntax.add_parsers [fixrecP, fixpatP];
+
+end; (* local structure *)
+
+end; (* struct *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/pcpodef_package.ML Thu May 31 14:01:58 2007 +0200
@@ -0,0 +1,213 @@
+(* Title: HOLCF/Tools/pcpodef_package.ML
+ ID: $Id$
+ Author: Brian Huffman
+
+Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
+typedef.
+*)
+
+signature PCPODEF_PACKAGE =
+sig
+ val quiet_mode: bool ref
+ val pcpodef_proof: (bool * string) * (bstring * string list * mixfix) * string
+ * (string * string) option -> theory -> Proof.state
+ val pcpodef_proof_i: (bool * string) * (bstring * string list * mixfix) * term
+ * (string * string) option -> theory -> Proof.state
+ val cpodef_proof: (bool * string) * (bstring * string list * mixfix) * string
+ * (string * string) option -> theory -> Proof.state
+ val cpodef_proof_i: (bool * string) * (bstring * string list * mixfix) * term
+ * (string * string) option -> theory -> Proof.state
+end;
+
+structure PcpodefPackage: PCPODEF_PACKAGE =
+struct
+
+(** theory context references **)
+
+val typedef_po = thm "typedef_po";
+val typedef_cpo = thm "typedef_cpo";
+val typedef_pcpo = thm "typedef_pcpo";
+val typedef_lub = thm "typedef_lub";
+val typedef_thelub = thm "typedef_thelub";
+val typedef_compact = thm "typedef_compact";
+val cont_Rep = thm "typedef_cont_Rep";
+val cont_Abs = thm "typedef_cont_Abs";
+val Rep_strict = thm "typedef_Rep_strict";
+val Abs_strict = thm "typedef_Abs_strict";
+val Rep_defined = thm "typedef_Rep_defined";
+val Abs_defined = thm "typedef_Abs_defined";
+
+
+(** type definitions **)
+
+(* messages *)
+
+val quiet_mode = ref false;
+fun message s = if ! quiet_mode then () else writeln s;
+
+
+(* prepare_cpodef *)
+
+fun err_in_cpodef msg name =
+ cat_error msg ("The error(s) above occurred in cpodef " ^ quote name);
+
+fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
+
+fun adm_const T = Const ("Adm.adm", (T --> HOLogic.boolT) --> HOLogic.boolT);
+fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
+
+fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy =
+ let
+ val ctxt = ProofContext.init thy;
+ val full = Sign.full_name thy;
+
+ (*rhs*)
+ val full_name = full name;
+ val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
+ val setT = Term.fastype_of set;
+ val rhs_tfrees = term_tfrees set;
+ val oldT = HOLogic.dest_setT setT handle TYPE _ =>
+ error ("Not a set type: " ^ quote (ProofContext.string_of_typ ctxt setT));
+ fun mk_nonempty A =
+ HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A));
+ fun mk_admissible A =
+ mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A));
+ fun mk_UU_mem A = HOLogic.mk_mem (Const ("Pcpo.UU", oldT), A);
+ val goal = if pcpo
+ then HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_UU_mem set, mk_admissible set))
+ else HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_nonempty set, mk_admissible set));
+
+ (*lhs*)
+ val defS = Sign.defaultS thy;
+ val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
+ val lhs_sorts = map snd lhs_tfrees;
+ val tname = Syntax.type_name t mx;
+ val full_tname = full tname;
+ val newT = Type (full_tname, map TFree lhs_tfrees);
+
+ val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs;
+ val RepC = Const (full Rep_name, newT --> oldT);
+ fun lessC T = Const ("Porder.<<", T --> T --> HOLogic.boolT);
+ val less_def = ("less_" ^ name ^ "_def", Logic.mk_equals (lessC newT,
+ Abs ("x", newT, Abs ("y", newT, lessC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0)))));
+
+ fun make_po tac theory = theory
+ |> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac
+ ||> AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.sq_ord"])
+ (ClassPackage.intro_classes_tac [])
+ ||>> PureThy.add_defs_i true [Thm.no_attributes less_def]
+ |-> (fn ((_, {type_definition, set_def, ...}), [less_definition]) =>
+ AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.po"])
+ (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1)
+ #> pair (type_definition, less_definition, set_def));
+
+ fun make_cpo admissible (type_def, less_def, set_def) theory =
+ let
+ val admissible' = fold_rule (the_list set_def) admissible;
+ val cpo_thms = [type_def, less_def, admissible'];
+ in
+ theory
+ |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.cpo"])
+ (Tactic.rtac (typedef_cpo OF cpo_thms) 1)
+ |> Theory.add_path name
+ |> PureThy.add_thms
+ ([(("adm_" ^ name, admissible'), []),
+ (("cont_" ^ Rep_name, cont_Rep OF cpo_thms), []),
+ (("cont_" ^ Abs_name, cont_Abs OF cpo_thms), []),
+ (("lub_" ^ name, typedef_lub OF cpo_thms), []),
+ (("thelub_" ^ name, typedef_thelub OF cpo_thms), []),
+ (("compact_" ^ name, typedef_compact OF cpo_thms), [])])
+ |> snd
+ |> Theory.parent_path
+ end;
+
+ fun make_pcpo UUmem (type_def, less_def, set_def) theory =
+ let
+ val UUmem' = fold_rule (the_list set_def) UUmem;
+ val pcpo_thms = [type_def, less_def, UUmem'];
+ in
+ theory
+ |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.pcpo"])
+ (Tactic.rtac (typedef_pcpo OF pcpo_thms) 1)
+ |> Theory.add_path name
+ |> PureThy.add_thms
+ ([((Rep_name ^ "_strict", Rep_strict OF pcpo_thms), []),
+ ((Abs_name ^ "_strict", Abs_strict OF pcpo_thms), []),
+ ((Rep_name ^ "_defined", Rep_defined OF pcpo_thms), []),
+ ((Abs_name ^ "_defined", Abs_defined OF pcpo_thms), [])
+ ])
+ |> snd
+ |> Theory.parent_path
+ end;
+
+ fun pcpodef_result UUmem_admissible theory =
+ let
+ val UUmem = UUmem_admissible RS conjunct1;
+ val admissible = UUmem_admissible RS conjunct2;
+ in
+ theory
+ |> make_po (Tactic.rtac exI 1 THEN Tactic.rtac UUmem 1)
+ |-> (fn defs => make_cpo admissible defs #> make_pcpo UUmem defs)
+ end;
+
+ fun cpodef_result nonempty_admissible theory =
+ let
+ val nonempty = nonempty_admissible RS conjunct1;
+ val admissible = nonempty_admissible RS conjunct2;
+ in
+ theory
+ |> make_po (Tactic.rtac nonempty 1)
+ |-> make_cpo admissible
+ end;
+
+ in (goal, if pcpo then pcpodef_result else cpodef_result) end
+ handle ERROR msg => err_in_cpodef msg name;
+
+
+(* cpodef_proof interface *)
+
+fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy =
+ let
+ val (goal, pcpodef_result) =
+ prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy;
+ fun after_qed [[th]] = ProofContext.theory (pcpodef_result th);
+ in Proof.theorem_i NONE after_qed [[(goal, [])]] (ProofContext.init thy) end;
+
+fun pcpodef_proof x = gen_pcpodef_proof ProofContext.read_term true x;
+fun pcpodef_proof_i x = gen_pcpodef_proof ProofContext.cert_term true x;
+
+fun cpodef_proof x = gen_pcpodef_proof ProofContext.read_term false x;
+fun cpodef_proof_i x = gen_pcpodef_proof ProofContext.cert_term false x;
+
+
+(** outer syntax **)
+
+local structure P = OuterParse and K = OuterKeyword in
+
+(* copied from HOL/Tools/typedef_package.ML *)
+val typedef_proof_decl =
+ Scan.optional (P.$$$ "(" |--
+ ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
+ --| P.$$$ ")") (true, NONE) --
+ (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
+ Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
+
+fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
+ (if pcpo then pcpodef_proof else cpodef_proof)
+ ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
+
+val pcpodefP =
+ OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
+ (typedef_proof_decl >>
+ (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
+
+val cpodefP =
+ OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
+ (typedef_proof_decl >>
+ (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
+
+val _ = OuterSyntax.add_parsers [pcpodefP, cpodefP];
+
+end;
+
+end;
--- a/src/HOLCF/adm_tac.ML Thu May 31 13:24:13 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,180 +0,0 @@
-(* 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;
--- a/src/HOLCF/cont_consts.ML Thu May 31 13:24:13 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,110 +0,0 @@
-(* Title: HOLCF/cont_consts.ML
- ID: $Id$
- Author: Tobias Mayr, David von Oheimb, and Markus Wenzel
-
-HOLCF version of consts: handle continuous function types in mixfix
-syntax.
-*)
-
-signature CONT_CONSTS =
-sig
- val add_consts: (bstring * string * mixfix) list -> theory -> theory
- val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
-end;
-
-structure ContConsts: CONT_CONSTS =
-struct
-
-
-(* misc utils *)
-
-open HOLCFLogic;
-
-fun first (x,_,_) = x;
-fun second (_,x,_) = x;
-fun third (_,_,x) = x;
-fun upd_first f (x,y,z) = (f x, y, z);
-fun upd_second f (x,y,z) = ( x, f y, z);
-fun upd_third f (x,y,z) = ( x, y, f z);
-
-fun change_arrow 0 T = T
-| change_arrow n (Type(_,[S,T])) = Type ("fun",[S,change_arrow (n-1) T])
-| change_arrow _ _ = sys_error "cont_consts: change_arrow";
-
-fun trans_rules name2 name1 n mx = let
- fun argnames _ 0 = []
- | argnames c n = chr c::argnames (c+1) (n-1);
- val vnames = argnames (ord "A") n;
- val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1);
- in [Syntax.ParsePrintRule (Syntax.mk_appl (Constant name2) (map Variable vnames),
- Library.foldl (fn (t,arg) => (Syntax.mk_appl (Constant "Rep_CFun")
- [t,Variable arg]))
- (Constant name1,vnames))]
- @(case mx of InfixName _ => [extra_parse_rule]
- | InfixlName _ => [extra_parse_rule]
- | InfixrName _ => [extra_parse_rule] | _ => []) end;
-
-
-(* transforming infix/mixfix declarations of constants with type ...->...
- a declaration of such a constant is transformed to a normal declaration with
- an internal name, the same type, and nofix. Additionally, a purely syntactic
- declaration with the original name, type ...=>..., and the original mixfix
- is generated and connected to the other declaration via some translation.
-*)
-fun fix_mixfix (syn , T, mx as Infix p ) =
- (Syntax.const_name syn mx, T, InfixName (syn, p))
- | fix_mixfix (syn , T, mx as Infixl p ) =
- (Syntax.const_name syn mx, T, InfixlName (syn, p))
- | fix_mixfix (syn , T, mx as Infixr p ) =
- (Syntax.const_name syn mx, T, InfixrName (syn, p))
- | fix_mixfix decl = decl;
-fun transform decl = let
- val (c, T, mx) = fix_mixfix decl;
- val c2 = "_cont_" ^ c;
- val n = Syntax.mixfix_args mx
- in ((c , T,NoSyn),
- (c2,change_arrow n T,mx ),
- trans_rules c2 c n mx) end;
-
-fun cfun_arity (Type(n,[_,T])) = if n = cfun_arrow then 1+cfun_arity T else 0
-| cfun_arity _ = 0;
-
-fun is_contconst (_,_,NoSyn ) = false
-| is_contconst (_,_,Binder _) = false
-| is_contconst (c,T,mx ) = cfun_arity T >= Syntax.mixfix_args mx
- handle ERROR msg => cat_error msg ("in mixfix annotation for " ^
- quote (Syntax.const_name c mx));
-
-
-(* add_consts(_i) *)
-
-fun gen_add_consts prep_typ raw_decls thy =
- let
- val decls = map (upd_second (prep_typ thy)) raw_decls;
- val (contconst_decls, normal_decls) = List.partition is_contconst decls;
- val transformed_decls = map transform contconst_decls;
- in
- thy
- |> Sign.add_consts_i normal_decls
- |> Sign.add_consts_i (map first transformed_decls)
- |> Sign.add_syntax_i (map second transformed_decls)
- |> Sign.add_trrules_i (List.concat (map third transformed_decls))
- end;
-
-val add_consts = gen_add_consts Sign.read_typ;
-val add_consts_i = gen_add_consts Sign.certify_typ;
-
-
-(* outer syntax *)
-
-local structure P = OuterParse and K = OuterKeyword in
-
-val constsP =
- OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
- (Scan.repeat1 P.const >> (Toplevel.theory o add_consts));
-
-val _ = OuterSyntax.add_parsers [constsP];
-
-end;
-
-end;
--- a/src/HOLCF/cont_proc.ML Thu May 31 13:24:13 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,145 +0,0 @@
-(* Title: HOLCF/cont_proc.ML
- ID: $Id$
- Author: Brian Huffman
-*)
-
-signature CONT_PROC =
-sig
- val is_lcf_term: term -> bool
- val cont_thms: term -> thm list
- val all_cont_thms: term -> thm list
- val cont_tac: int -> tactic
- val cont_proc: theory -> simproc
- val setup: theory -> theory
-end;
-
-structure ContProc: CONT_PROC =
-struct
-
-(** theory context references **)
-
-val cont_K = thm "cont_const";
-val cont_I = thm "cont_id";
-val cont_A = thm "cont2cont_Rep_CFun";
-val cont_L = thm "cont2cont_LAM";
-val cont_R = thm "cont_Rep_CFun2";
-
-(* checks whether a term contains no dangling bound variables *)
-val is_closed_term =
- let
- fun bound_less i (t $ u) =
- bound_less i t andalso bound_less i u
- | bound_less i (Abs (_, _, t)) = bound_less (i+1) t
- | bound_less i (Bound n) = n < i
- | bound_less i _ = true; (* Const, Free, and Var are OK *)
- in bound_less 0 end;
-
-(* checks whether a term is written entirely in the LCF sublanguage *)
-fun is_lcf_term (Const ("Cfun.Rep_CFun", _) $ t $ u) =
- is_lcf_term t andalso is_lcf_term u
- | is_lcf_term (Const ("Cfun.Abs_CFun", _) $ Abs (_, _, t)) = is_lcf_term t
- | is_lcf_term (Const ("Cfun.Abs_CFun", _) $ _) = false
- | is_lcf_term (Bound _) = true
- | is_lcf_term t = is_closed_term t;
-
-(*
- efficiently generates a cont thm for every LAM abstraction in a term,
- using forward proof and reusing common subgoals
-*)
-local
- fun var 0 = [SOME cont_I]
- | var n = NONE :: var (n-1);
-
- fun k NONE = cont_K
- | k (SOME x) = x;
-
- fun ap NONE NONE = NONE
- | ap x y = SOME (k y RS (k x RS cont_A));
-
- fun zip [] [] = []
- | zip [] (y::ys) = (ap NONE y ) :: zip [] ys
- | zip (x::xs) [] = (ap x NONE) :: zip xs []
- | zip (x::xs) (y::ys) = (ap x y ) :: zip xs ys
-
- fun lam [] = ([], cont_K)
- | lam (x::ys) =
- let
- (* should use "standard" for thms that are used multiple times *)
- (* it seems to allow for sharing in explicit proof objects *)
- val x' = standard (k x);
- val Lx = x' RS cont_L;
- in (map (fn y => SOME (k y RS Lx)) ys, x') end;
-
- (* first list: cont thm for each dangling bound variable *)
- (* second list: cont thm for each LAM in t *)
- (* if b = false, only return cont thm for outermost LAMs *)
- fun cont_thms1 b (Const ("Cfun.Rep_CFun", _) $ f $ t) =
- let
- val (cs1,ls1) = cont_thms1 b f;
- val (cs2,ls2) = cont_thms1 b t;
- in (zip cs1 cs2, if b then ls1 @ ls2 else []) end
- | cont_thms1 b (Const ("Cfun.Abs_CFun", _) $ Abs (_, _, t)) =
- let
- val (cs, ls) = cont_thms1 b t;
- val (cs', l) = lam cs;
- in (cs', l::ls) end
- | cont_thms1 _ (Bound n) = (var n, [])
- | cont_thms1 _ _ = ([], []);
-in
- (* precondition: is_lcf_term t = true *)
- fun cont_thms t = snd (cont_thms1 false t);
- fun all_cont_thms t = snd (cont_thms1 true t);
-end;
-
-(*
- Given the term "cont f", the procedure tries to construct the
- theorem "cont f == True". If this theorem cannot be completely
- solved by the introduction rules, then the procedure returns a
- conditional rewrite rule with the unsolved subgoals as premises.
-*)
-
-local
- val rules = [cont_K, cont_I, cont_R, cont_A, cont_L];
-
- val prev_cont_thms : thm list ref = ref [];
-
- fun old_cont_tac i thm =
- case !prev_cont_thms of
- [] => no_tac thm
- | (c::cs) => (prev_cont_thms := cs; rtac c i thm);
-
- fun new_cont_tac f' i thm =
- case all_cont_thms f' of
- [] => no_tac thm
- | (c::cs) => (prev_cont_thms := cs; rtac c i thm);
-
- fun cont_tac_of_term (Const ("Cont.cont", _) $ f) =
- let
- val f' = Const ("Cfun.Abs_CFun", dummyT) $ f;
- in
- if is_lcf_term f'
- then old_cont_tac ORELSE' new_cont_tac f'
- else REPEAT_ALL_NEW (resolve_tac rules)
- end
- | cont_tac_of_term _ = K no_tac;
-in
- val cont_tac =
- SUBGOAL (fn (t, i) => cont_tac_of_term (HOLogic.dest_Trueprop t) i);
-end;
-
-local
- fun solve_cont thy _ t =
- let
- val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI;
- in Option.map fst (Seq.pull (cont_tac 1 tr)) end
-in
- fun cont_proc thy =
- Simplifier.simproc thy "cont_proc" ["cont f"] solve_cont;
-end;
-
-val setup =
- (fn thy =>
- (Simplifier.change_simpset_of thy
- (fn ss => ss addsimprocs [cont_proc thy]); thy));
-
-end;
--- a/src/HOLCF/domain/axioms.ML Thu May 31 13:24:13 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,170 +0,0 @@
-(* Title: HOLCF/domain/axioms.ML
- ID: $Id$
- Author: David von Oheimb
-
-Syntax generator for domain section.
-*)
-
-structure Domain_Axioms = struct
-
-local
-
-open Domain_Library;
-infixr 0 ===>;infixr 0 ==>;infix 0 == ;
-infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<;
-infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo;
-
-fun calc_axioms comp_dname (eqs : eq list) n (((dname,_),cons) : eq)=
-let
-
-(* ----- axioms and definitions concerning the isomorphism ------------------ *)
-
- val dc_abs = %%:(dname^"_abs");
- val dc_rep = %%:(dname^"_rep");
- val x_name'= "x";
- val x_name = idx_name eqs x_name' (n+1);
- val dnam = Sign.base_name dname;
-
- val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name'));
- val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));
-
- val when_def = ("when_def",%%:(dname^"_when") ==
- foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) =>
- Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
-
- val copy_def = let
- fun idxs z x arg = if is_rec arg
- then (cproj (Bound z) eqs (rec_of arg))`Bound(z-x)
- else Bound(z-x);
- fun one_con (con,args) =
- foldr /\# (list_ccomb (%%:con, mapn (idxs (length args)) 1 args)) args;
- in ("copy_def", %%:(dname^"_copy") ==
- /\"f" (list_ccomb (%%:(dname^"_when"), map one_con cons))) end;
-
-(* -- definitions concerning the constructors, discriminators and selectors - *)
-
- fun con_def m n (_,args) = let
- fun idxs z x arg = (if is_lazy arg then fn t => %%:upN`t else I) (Bound(z-x));
- fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs);
- fun inj y 1 _ = y
- | inj y _ 0 = %%:sinlN`y
- | inj y i j = %%:sinrN`(inj y (i-1) (j-1));
- in foldr /\# (dc_abs`(inj (parms args) m n)) args end;
-
- val con_defs = mapn (fn n => fn (con,args) =>
- (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons;
-
- val dis_defs = let
- fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) ==
- list_ccomb(%%:(dname^"_when"),map
- (fn (con',args) => (foldr /\#
- (if con'=con then %%:TT_N else %%:FF_N) args)) cons))
- in map ddef cons end;
-
- val mat_defs = let
- fun mdef (con,_) = (mat_name con ^"_def",%%:(mat_name con) ==
- list_ccomb(%%:(dname^"_when"),map
- (fn (con',args) => (foldr /\#
- (if con'=con
- then %%:returnN`(mk_ctuple (map (bound_arg args) args))
- else %%:failN) args)) cons))
- in map mdef cons end;
-
- val pat_defs =
- let
- fun pdef (con,args) =
- let
- val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
- val xs = map (bound_arg args) args;
- val r = Bound (length args);
- val rhs = case args of [] => %%:returnN ` HOLogic.unit
- | _ => foldr1 cpair_pat ps ` mk_ctuple xs;
- fun one_con (con',args') = foldr /\# (if con'=con then rhs else %%:failN) args';
- in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) ==
- list_ccomb(%%:(dname^"_when"), map one_con cons))
- end
- in map pdef cons end;
-
- val sel_defs = let
- fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel ==
- list_ccomb(%%:(dname^"_when"),map
- (fn (con',args) => if con'<>con then UU else
- foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
- in List.mapPartial I (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end;
-
-
-(* ----- axiom and definitions concerning induction ------------------------- *)
-
- val reach_ax = ("reach", mk_trp(cproj (%%:fixN`%%(comp_dname^"_copy")) eqs n
- `%x_name === %:x_name));
- val take_def = ("take_def",%%:(dname^"_take") == mk_lam("n",cproj
- (%%:iterateN $ Bound 0 ` %%:(comp_dname^"_copy") ` UU) eqs n));
- val finite_def = ("finite_def",%%:(dname^"_finite") == mk_lam(x_name,
- mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
-
-in (dnam,
- [abs_iso_ax, rep_iso_ax, reach_ax],
- [when_def, copy_def] @
- con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @
- [take_def, finite_def])
-end; (* let *)
-
-fun infer_props thy = map (apsnd (FixrecPackage.legacy_infer_prop thy));
-
-fun add_axioms_i x = snd o PureThy.add_axioms_i (map Thm.no_attributes x);
-fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy;
-
-fun add_defs_i x = snd o (PureThy.add_defs_i false) (map Thm.no_attributes x);
-fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
-
-in (* local *)
-
-fun add_axioms (comp_dnam, eqs : eq list) thy' = let
- val comp_dname = Sign.full_name thy' comp_dnam;
- val dnames = map (fst o fst) eqs;
- val x_name = idx_name dnames "x";
- fun copy_app dname = %%:(dname^"_copy")`Bound 0;
- val copy_def = ("copy_def" , %%:(comp_dname^"_copy") ==
- /\"f"(foldr1 cpair (map copy_app dnames)));
- val bisim_def = ("bisim_def",%%:(comp_dname^"_bisim")==mk_lam("R",
- let
- fun one_con (con,args) = let
- val nonrec_args = filter_out is_rec args;
- val rec_args = List.filter is_rec args;
- val recs_cnt = length rec_args;
- val allargs = nonrec_args @ rec_args
- @ map (upd_vname (fn s=> s^"'")) rec_args;
- val allvns = map vname allargs;
- fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg;
- val vns1 = map (vname_arg "" ) args;
- val vns2 = map (vname_arg "'") args;
- val allargs_cnt = length nonrec_args + 2*recs_cnt;
- val rec_idxs = (recs_cnt-1) downto 0;
- val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg)
- (allargs~~((allargs_cnt-1) downto 0)));
- fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $
- Bound (2*recs_cnt-i) $ Bound (recs_cnt-i);
- val capps = foldr mk_conj (mk_conj(
- Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1),
- Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2)))
- (mapn rel_app 1 rec_args);
- in foldr mk_ex (Library.foldr mk_conj
- (map (defined o Bound) nonlazy_idxs,capps)) allvns end;
- fun one_comp n (_,cons) =mk_all(x_name(n+1),mk_all(x_name(n+1)^"'",mk_imp(
- proj (Bound 2) eqs n $ Bound 1 $ Bound 0,
- foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
- ::map one_con cons))));
- in foldr1 mk_conj (mapn one_comp 0 eqs)end ));
- fun add_one (thy,(dnam,axs,dfs)) = thy
- |> Theory.add_path dnam
- |> add_defs_infer dfs
- |> add_axioms_infer axs
- |> Theory.parent_path;
- val thy = Library.foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs);
-in thy |> Theory.add_path comp_dnam
- |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else []))
- |> Theory.parent_path
-end;
-
-end; (* local *)
-end; (* struct *)
--- a/src/HOLCF/domain/extender.ML Thu May 31 13:24:13 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,183 +0,0 @@
-(* Title: HOLCF/domain/extender.ML
- ID: $Id$
- Author: David von Oheimb
-
-Theory extender for domain section, including new-style theory syntax.
-
-###TODO:
-
-this definition
-domain empty = silly empty
-yields
-Exception-
- TERM
- ("typ_of_term: bad encoding of type",
- [Abs ("uu", "_", Const ("NONE", "_"))]) raised
-but this works fine:
-domain Empty = silly Empty
-
-strange syntax errors are produced for:
-domain xx = xx ("x yy")
-domain 'a foo = foo (sel::"'a")
-and bar = bar ("'a dummy")
-
-*)
-
-signature DOMAIN_EXTENDER =
-sig
- val add_domain: string * ((bstring * string list) *
- (string * mixfix * (bool * string option * string) list) list) list
- -> theory -> theory
- val add_domain_i: string * ((bstring * string list) *
- (string * mixfix * (bool * string option * typ) list) list) list
- -> theory -> theory
-end;
-
-structure Domain_Extender: DOMAIN_EXTENDER =
-struct
-
-open Domain_Library;
-
-(* ----- general testing and preprocessing of constructor list -------------- *)
-fun check_and_sort_domain (dtnvs: (string * typ list) list,
- cons'' : ((string * mixfix * (bool * string option * typ) list) list) list) sg =
- let
- val defaultS = Sign.defaultS sg;
- val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of
- [] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
- val test_dupl_cons = (case duplicates (op =) (map first (List.concat cons'')) of
- [] => false | dups => error ("Duplicate constructors: "
- ^ commas_quote dups));
- val test_dupl_sels = (case duplicates (op =) (List.mapPartial second
- (List.concat (map third (List.concat cons'')))) of
- [] => false | dups => error("Duplicate selectors: "^commas_quote dups));
- val test_dupl_tvars = exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of
- [] => false | dups => error("Duplicate type arguments: "
- ^commas_quote dups)) (map snd dtnvs);
- (* test for free type variables, illegal sort constraints on rhs,
- non-pcpo-types and invalid use of recursive type;
- replace sorts in type variables on rhs *)
- fun analyse_equation ((dname,typevars),cons') =
- let
- val tvars = map dest_TFree typevars;
- val distinct_typevars = map TFree tvars;
- fun rm_sorts (TFree(s,_)) = TFree(s,[])
- | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
- | rm_sorts (TVar(s,_)) = TVar(s,[])
- and remove_sorts l = map rm_sorts l;
- val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
- fun analyse indirect (TFree(v,s)) = (case AList.lookup (op =) tvars v of
- NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
- | SOME sort => if eq_set_string (s,defaultS) orelse
- eq_set_string (s,sort )
- then TFree(v,sort)
- else error ("Inconsistent sort constraint" ^
- " for type variable " ^ quote v))
- | analyse indirect (t as Type(s,typl)) = (case AList.lookup (op =) dtnvs s of
- NONE => if s mem indirect_ok
- then Type(s,map (analyse false) typl)
- else Type(s,map (analyse true) typl)
- | SOME typevars => if indirect
- then error ("Indirect recursion of type " ^
- quote (string_of_typ sg t))
- else if dname <> s orelse (** BUG OR FEATURE?:
- mutual recursion may use different arguments **)
- remove_sorts typevars = remove_sorts typl
- then Type(s,map (analyse true) typl)
- else error ("Direct recursion of type " ^
- quote (string_of_typ sg t) ^
- " with different arguments"))
- | analyse indirect (TVar _) = Imposs "extender:analyse";
- fun check_pcpo T = if pcpo_type sg T then T
- else error("Constructor argument type is not of sort pcpo: "^string_of_typ sg T);
- val analyse_con = upd_third (map (upd_third (check_pcpo o analyse false)));
- in ((dname,distinct_typevars), map analyse_con cons') end;
- in ListPair.map analyse_equation (dtnvs,cons'')
- end; (* let *)
-
-(* ----- calls for building new thy and thms -------------------------------- *)
-
-fun gen_add_domain prep_typ (comp_dnam, eqs''') thy''' =
- let
- val dtnvs = map ((fn (dname,vs) =>
- (Sign.full_name thy''' dname, map (Sign.read_typ thy''') vs))
- o fst) eqs''';
- val cons''' = map snd eqs''';
- fun thy_type (dname,tvars) = (Sign.base_name dname, length tvars, NoSyn);
- fun thy_arity (dname,tvars) = (dname, map (snd o dest_TFree) tvars, pcpoS);
- val thy'' = thy''' |> Theory.add_types (map thy_type dtnvs)
- |> fold (AxClass.axiomatize_arity_i o thy_arity) dtnvs;
- val cons'' = map (map (upd_third (map (upd_third (prep_typ thy''))))) cons''';
- val eqs' = check_and_sort_domain (dtnvs,cons'') thy'';
- val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs');
- val dts = map (Type o fst) eqs';
- val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
- fun strip ss = Library.drop (find_index_eq "'" ss +1, ss);
- fun typid (Type (id,_)) =
- let val c = hd (Symbol.explode (Sign.base_name id))
- in if Symbol.is_letter c then c else "t" end
- | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id)))
- | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
- fun one_con (con,mx,args) =
- ((Syntax.const_name con mx),
- ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
- find_index_eq tp dts,
- DatatypeAux.dtyp_of_typ new_dts tp),
- sel,vn))
- (args,(mk_var_names(map (typid o third) args)))
- ) : cons;
- val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list;
- val thy = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs);
- val (theorems_thy, (rewss, take_rews)) = (foldl_map (fn (thy0,eq) =>
- Domain_Theorems.theorems (eq,eqs) thy0) (thy,eqs))
- |>>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
- in
- theorems_thy
- |> Theory.add_path (Sign.base_name comp_dnam)
- |> (snd o (PureThy.add_thmss [(("rews", List.concat rewss @ take_rews), [])]))
- |> Theory.parent_path
- end;
-
-val add_domain_i = gen_add_domain Sign.certify_typ;
-val add_domain = gen_add_domain Sign.read_typ;
-
-
-(** outer syntax **)
-
-local structure P = OuterParse and K = OuterKeyword in
-
-val dest_decl =
- P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
- (P.name >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1
- || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
- >> (fn t => (true,NONE,t))
- || P.typ >> (fn t => (false,NONE,t));
-
-val cons_decl =
- P.name -- Scan.repeat dest_decl -- P.opt_mixfix
- >> (fn ((c, ds), mx) => (c, mx, ds));
-
-val type_var' = (P.type_ident ^^
- Scan.optional (P.$$$ "::" ^^ P.!!! P.sort) "");
-val type_args' = type_var' >> single ||
- P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") ||
- Scan.succeed [];
-
-val domain_decl = (type_args' -- P.name >> Library.swap) --
- (P.$$$ "=" |-- P.enum1 "|" cons_decl);
-val domains_decl =
- Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.and_list1 domain_decl
- >> (fn (opt_name, doms) =>
- (case opt_name of NONE => space_implode "_" (map (#1 o #1) doms) | SOME s => s, doms));
-
-val domainP =
- OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
- (domains_decl >> (Toplevel.theory o add_domain));
-
-
-val _ = OuterSyntax.add_keywords ["lazy"];
-val _ = OuterSyntax.add_parsers [domainP];
-
-end; (* local structure *)
-
-end;
--- a/src/HOLCF/domain/library.ML Thu May 31 13:24:13 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,230 +0,0 @@
-(* Title: HOLCF/domain/library.ML
- ID: $Id$
- Author: David von Oheimb
-
-Library for domain section.
-*)
-
-
-(* ----- general support ---------------------------------------------------- *)
-
-fun mapn f n [] = []
-| mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs;
-
-fun foldr'' f (l,f2) = let fun itr [] = raise Fail "foldr''"
- | itr [a] = f2 a
- | itr (a::l) = f(a, itr l)
-in itr l end;
-fun map_cumulr f start xs = foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) =>
- (y::ys,res2)) ([],start) xs;
-
-
-fun first (x,_,_) = x; fun second (_,x,_) = x; fun third (_,_,x) = x;
-fun upd_first f (x,y,z) = (f x, y, z);
-fun upd_second f (x,y,z) = ( x, f y, z);
-fun upd_third f (x,y,z) = ( x, y, f z);
-
-fun atomize thm = let val r_inst = read_instantiate;
- fun at thm = case concl_of thm of
- _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
- | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [("x","?"^s)] spec))
- | _ => [thm];
-in map zero_var_indexes (at thm) end;
-
-(* ----- specific support for domain ---------------------------------------- *)
-
-structure Domain_Library = struct
-
-open HOLCFLogic;
-
-exception Impossible of string;
-fun Imposs msg = raise Impossible ("Domain:"^msg);
-
-(* ----- name handling ----- *)
-
-val strip_esc = let fun strip ("'" :: c :: cs) = c :: strip cs
- | strip ["'"] = []
- | strip (c :: cs) = c :: strip cs
- | strip [] = [];
-in implode o strip o Symbol.explode end;
-
-fun extern_name con = case Symbol.explode con of
- ("o"::"p"::" "::rest) => implode rest
- | _ => con;
-fun dis_name con = "is_"^ (extern_name con);
-fun dis_name_ con = "is_"^ (strip_esc con);
-fun mat_name con = "match_"^ (extern_name con);
-fun mat_name_ con = "match_"^ (strip_esc con);
-fun pat_name con = (extern_name con) ^ "_pat";
-fun pat_name_ con = (strip_esc con) ^ "_pat";
-
-(* make distinct names out of the type list,
- forbidding "o","n..","x..","f..","P.." as names *)
-(* a number string is added if necessary *)
-fun mk_var_names ids : string list = let
- fun nonreserved s = if s mem ["n","x","f","P"] then s^"'" else s;
- fun index_vnames(vn::vns,occupied) =
- (case AList.lookup (op =) occupied vn of
- NONE => if vn mem vns
- then (vn^"1") :: index_vnames(vns,(vn,1) ::occupied)
- else vn :: index_vnames(vns, occupied)
- | SOME(i) => (vn^(string_of_int (i+1)))
- :: index_vnames(vns,(vn,i+1)::occupied))
- | index_vnames([],occupied) = [];
-in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end;
-
-fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, pcpoS);
-fun string_of_typ sg = Sign.string_of_typ sg o Sign.certify_typ sg;
-
-(* ----- constructor list handling ----- *)
-
-type cons = (string * (* operator name of constr *)
- ((bool*int*DatatypeAux.dtyp)* (* (lazy,recursive element or ~1) *)
- string option* (* selector name *)
- string) (* argument name *)
- list); (* argument list *)
-type eq = (string * (* name of abstracted type *)
- typ list) * (* arguments of abstracted type *)
- cons list; (* represented type, as a constructor list *)
-
-fun rec_of arg = second (first arg);
-fun is_lazy arg = first (first arg);
-val sel_of = second;
-val vname = third;
-val upd_vname = upd_third;
-fun is_rec arg = rec_of arg >=0;
-fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
-fun nonlazy args = map vname (filter_out is_lazy args);
-fun nonlazy_rec args = map vname (List.filter is_nonlazy_rec args);
-
-(* ----- qualified names of HOLCF constants ----- *)
-
-val lessN = "Porder.<<"
-val UU_N = "Pcpo.UU";
-val admN = "Adm.adm";
-val compactN = "Adm.compact";
-val Rep_CFunN = "Cfun.Rep_CFun";
-val Abs_CFunN = "Cfun.Abs_CFun";
-val ID_N = "Cfun.ID";
-val cfcompN = "Cfun.cfcomp";
-val strictifyN = "Cfun.strictify";
-val cpairN = "Cprod.cpair";
-val cfstN = "Cprod.cfst";
-val csndN = "Cprod.csnd";
-val csplitN = "Cprod.csplit";
-val spairN = "Sprod.spair";
-val sfstN = "Sprod.sfst";
-val ssndN = "Sprod.ssnd";
-val ssplitN = "Sprod.ssplit";
-val sinlN = "Ssum.sinl";
-val sinrN = "Ssum.sinr";
-val sscaseN = "Ssum.sscase";
-val upN = "Up.up";
-val fupN = "Up.fup";
-val ONE_N = "One.ONE";
-val TT_N = "Tr.TT";
-val FF_N = "Tr.FF";
-val iterateN = "Fix.iterate";
-val fixN = "Fix.fix";
-val returnN = "Fixrec.return";
-val failN = "Fixrec.fail";
-val cpair_patN = "Fixrec.cpair_pat";
-val branchN = "Fixrec.branch";
-
-val pcpoN = "Pcpo.pcpo"
-val pcpoS = [pcpoN];
-
-
-(* ----- support for type and mixfix expressions ----- *)
-
-infixr 5 -->;
-
-(* ----- support for term expressions ----- *)
-
-fun %: s = Free(s,dummyT);
-fun %# arg = %:(vname arg);
-fun %%: s = Const(s,dummyT);
-
-local open HOLogic in
-val mk_trp = mk_Trueprop;
-fun mk_conj (S,T) = conj $ S $ T;
-fun mk_disj (S,T) = disj $ S $ T;
-fun mk_imp (S,T) = imp $ S $ T;
-fun mk_lam (x,T) = Abs(x,dummyT,T);
-fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P);
-fun mk_ex (x,P) = mk_exists (x,dummyT,P);
-fun mk_constrain (typ,T) = TypeInfer.constrain T typ;
-fun mk_constrainall (x,typ,P) = %%:"All" $ (TypeInfer.constrain (mk_lam(x,P)) (typ --> boolT));
-end
-
-fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
-
-infixr 0 ===>; fun S ===> T = %%:"==>" $ S $ T;
-infixr 0 ==>; fun S ==> T = mk_trp S ===> mk_trp T;
-infix 0 ==; fun S == T = %%:"==" $ S $ T;
-infix 1 ===; fun S === T = %%:"op =" $ S $ T;
-infix 1 ~=; fun S ~= T = HOLogic.mk_not (S === T);
-infix 1 <<; fun S << T = %%:lessN $ S $ T;
-infix 1 ~<<; fun S ~<< T = HOLogic.mk_not (S << T);
-
-infix 9 ` ; fun f` x = %%:Rep_CFunN $ f $ x;
-infix 9 `% ; fun f`% s = f` %: s;
-infix 9 `%%; fun f`%%s = f` %%:s;
-val list_ccomb = Library.foldl (op `); (* continuous version of list_comb *)
-fun con_app2 con f args = list_ccomb(%%:con,map f args);
-fun con_app con = con_app2 con %#;
-fun if_rec arg f y = if is_rec arg then f (rec_of arg) else y;
-fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) I (%# arg);
-fun prj _ _ x ( _::[]) _ = x
-| prj f1 _ x (_::y::ys) 0 = f1 x y
-| prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1);
-fun proj x = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
-fun cproj x = prj (fn S => K(%%:cfstN`S)) (fn S => K(%%:csndN`S)) x;
-fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
-
-fun /\ v T = %%:Abs_CFunN $ mk_lam(v,T);
-fun /\# (arg,T) = /\ (vname arg) T;
-infixr 9 oo; fun S oo T = %%:cfcompN`S`T;
-val UU = %%:UU_N;
-fun strict f = f`UU === UU;
-fun defined t = t ~= UU;
-fun cpair (t,u) = %%:cpairN`t`u;
-fun spair (t,u) = %%:spairN`t`u;
-fun mk_ctuple [] = HOLogic.unit (* used in match_defs *)
-| mk_ctuple ts = foldr1 cpair ts;
-fun mk_stuple [] = %%:ONE_N
-| mk_stuple ts = foldr1 spair ts;
-fun mk_ctupleT [] = HOLogic.unitT (* used in match_defs *)
-| mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts;
-fun mk_maybeT T = Type ("Fixrec.maybe",[T]);
-fun cpair_pat (p1,p2) = %%:cpair_patN $ p1 $ p2;
-fun lift_defined f = lift (fn x => defined (f x));
-fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
-
-fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) =
- (case cont_eta_contract body of
- body' as (Const("Cfun.Rep_CFun",Ta) $ f $ Bound 0) =>
- if not (0 mem loose_bnos f) then incr_boundvars ~1 f
- else Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body')
- | body' => Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body'))
-| cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t
-| cont_eta_contract t = t;
-
-fun idx_name dnames s n = s^(if length dnames = 1 then "" else string_of_int n);
-fun when_funs cons = if length cons = 1 then ["f"]
- else mapn (fn n => K("f"^(string_of_int n))) 1 cons;
-fun when_body cons funarg = let
- fun one_fun n (_,[] ) = /\ "dummy" (funarg(1,n))
- | one_fun n (_,args) = let
- val l2 = length args;
- fun idxs m arg = (if is_lazy arg then fn x=> %%:fupN` %%:ID_N`x
- else I) (Bound(l2-m));
- in cont_eta_contract (foldr''
- (fn (a,t) => %%:ssplitN`(/\# (a,t)))
- (args,
- fn a=> /\#(a,(list_ccomb(funarg(l2,n),mapn idxs 1 args))))
- ) end;
-in (if length cons = 1 andalso length(snd(hd cons)) <= 1
- then fn t => %%:strictifyN`t else I)
- (foldr1 (fn (x,y)=> %%:sscaseN`x`y) (mapn one_fun 1 cons)) end;
-end; (* struct *)
--- a/src/HOLCF/domain/syntax.ML Thu May 31 13:24:13 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,151 +0,0 @@
-(* Title: HOLCF/domain/syntax.ML
- ID: $Id$
- Author: David von Oheimb
-
-Syntax generator for domain section.
-*)
-
-structure Domain_Syntax = struct
-
-local
-
-open Domain_Library;
-infixr 5 -->; infixr 6 ->>;
-fun calc_syntax dtypeprod ((dname, typevars),
- (cons': (string * mixfix * (bool * string option * typ) list) list)) =
-let
-(* ----- constants concerning the isomorphism ------------------------------- *)
-
-local
- fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
- fun prod (_,_,args) = if args = [] then oneT
- else foldr1 mk_sprodT (map opt_lazy args);
- fun freetvar s = let val tvar = mk_TFree s in
- if tvar mem typevars then freetvar ("t"^s) else tvar end;
- fun when_type (_ ,_,args) = foldr (op ->>) (freetvar "t") (map third args);
-in
- val dtype = Type(dname,typevars);
- val dtype2 = foldr1 mk_ssumT (map prod cons');
- val dnam = Sign.base_name dname;
- val const_rep = (dnam^"_rep" , dtype ->> dtype2, NoSyn);
- val const_abs = (dnam^"_abs" , dtype2 ->> dtype , NoSyn);
- val const_when = (dnam^"_when",foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
- val const_copy = (dnam^"_copy", dtypeprod ->> dtype ->> dtype , NoSyn);
-end;
-
-(* ----- constants concerning constructors, discriminators, and selectors --- *)
-
-local
- val escape = let
- fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs
- else c::esc cs
- | esc [] = []
- in implode o esc o Symbol.explode end;
- fun con (name,s,args) = (name,foldr (op ->>) dtype (map third args),s);
- fun dis (con ,s,_ ) = (dis_name_ con, dtype->>trT,
- Mixfix(escape ("is_" ^ con), [], Syntax.max_pri));
- (* strictly speaking, these constants have one argument,
- but the mixfix (without arguments) is introduced only
- to generate parse rules for non-alphanumeric names*)
- fun mat (con ,s,args) = (mat_name_ con, dtype->>mk_maybeT(mk_ctupleT(map third args)),
- Mixfix(escape ("match_" ^ con), [], Syntax.max_pri));
- fun sel1 (_,sel,typ) = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
- fun sel (_ ,_,args) = List.mapPartial sel1 args;
- fun freetvar s n = let val tvar = mk_TFree (s ^ string_of_int n) in
- if tvar mem typevars then freetvar ("t"^s) n else tvar end;
- fun mk_patT (a,b) = a ->> mk_maybeT b;
- fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n);
- fun pat (con ,s,args) = (pat_name_ con, (mapn pat_arg_typ 1 args) --->
- mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))),
- Mixfix(escape (con ^ "_pat"), [], Syntax.max_pri));
-
-in
- val consts_con = map con cons';
- val consts_dis = map dis cons';
- val consts_mat = map mat cons';
- val consts_pat = map pat cons';
- val consts_sel = List.concat(map sel cons');
-end;
-
-(* ----- constants concerning induction ------------------------------------- *)
-
- val const_take = (dnam^"_take" , HOLogic.natT-->dtype->>dtype, NoSyn);
- val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT , NoSyn);
-
-(* ----- case translation --------------------------------------------------- *)
-
-local open Syntax in
- local
- fun c_ast con mx = Constant (const_name con mx);
- fun expvar n = Variable ("e"^(string_of_int n));
- fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
- (string_of_int m));
- fun argvars n args = mapn (argvar n) 1 args;
- fun app s (l,r) = mk_appl (Constant s) [l,r];
- val cabs = app "_cabs";
- val capp = app "Rep_CFun";
- fun con1 n (con,mx,args) = Library.foldl capp (c_ast con mx, argvars n args);
- fun case1 n (con,mx,args) = app "_case1" (con1 n (con,mx,args), expvar n);
- fun arg1 n (con,_,args) = foldr cabs (expvar n) (argvars n args);
- fun when1 n m = if n = m then arg1 n else K (Constant "UU");
-
- fun app_var x = mk_appl (Constant "_var") [x, Variable "rhs"];
- fun app_pat x = mk_appl (Constant "_pat") [x];
- fun args_list [] = Constant "Unity"
- | args_list xs = foldr1 (app "_args") xs;
- in
- val case_trans = ParsePrintRule
- (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn case1 1 cons')),
- capp (Library.foldl capp (Constant (dnam^"_when"), mapn arg1 1 cons'), Variable "x"));
-
- val abscon_trans = mapn (fn n => fn (con,mx,args) => ParsePrintRule
- (cabs (con1 n (con,mx,args), expvar n),
- Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons'))) 1 cons';
-
- val Case_trans = List.concat (map (fn (con,mx,args) =>
- let
- val cname = c_ast con mx;
- val pname = Constant (pat_name_ con);
- val ns = 1 upto length args;
- val xs = map (fn n => Variable ("x"^(string_of_int n))) ns;
- val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
- val vs = map (fn n => Variable ("v"^(string_of_int n))) ns;
- in
- [ParseRule (app_pat (Library.foldl capp (cname, xs)),
- mk_appl pname (map app_pat xs)),
- ParseRule (app_var (Library.foldl capp (cname, xs)),
- app_var (args_list xs)),
- PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)),
- app "_match" (mk_appl pname ps, args_list vs))]
- end) cons');
- end;
-end;
-
-in ([const_rep, const_abs, const_when, const_copy] @
- consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @
- [const_take, const_finite],
- (case_trans::(abscon_trans @ Case_trans)))
-end; (* let *)
-
-(* ----- putting all the syntax stuff together ------------------------------ *)
-
-in (* local *)
-
-fun add_syntax (comp_dnam,eqs': ((string * typ list) *
- (string * mixfix * (bool * string option * typ) list) list) list) thy'' =
-let
- val dtypes = map (Type o fst) eqs';
- val boolT = HOLogic.boolT;
- val funprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp ->> tp ) dtypes);
- val relprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
- val const_copy = (comp_dnam^"_copy" ,funprod ->> funprod, NoSyn);
- val const_bisim = (comp_dnam^"_bisim" ,relprod --> boolT , NoSyn);
- val ctt = map (calc_syntax funprod) eqs';
-in thy'' |> ContConsts.add_consts_i (List.concat (map fst ctt) @
- (if length eqs'>1 then [const_copy] else[])@
- [const_bisim])
- |> Sign.add_trrules_i (List.concat(map snd ctt))
-end; (* let *)
-
-end; (* local *)
-end; (* struct *)
--- a/src/HOLCF/domain/theorems.ML Thu May 31 13:24:13 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,951 +0,0 @@
-(* Title: HOLCF/domain/theorems.ML
- ID: $Id$
- Author: David von Oheimb
- New proofs/tactics by Brian Huffman
-
-Proof generator for domain section.
-*)
-
-val HOLCF_ss = simpset();
-
-structure Domain_Theorems = struct
-
-local
-
-val adm_impl_admw = thm "adm_impl_admw";
-val antisym_less_inverse = thm "antisym_less_inverse";
-val beta_cfun = thm "beta_cfun";
-val cfun_arg_cong = thm "cfun_arg_cong";
-val ch2ch_Rep_CFunL = thm "ch2ch_Rep_CFunL";
-val ch2ch_Rep_CFunR = thm "ch2ch_Rep_CFunR";
-val chain_iterate = thm "chain_iterate";
-val compact_ONE = thm "compact_ONE";
-val compact_sinl = thm "compact_sinl";
-val compact_sinr = thm "compact_sinr";
-val compact_spair = thm "compact_spair";
-val compact_up = thm "compact_up";
-val contlub_cfun_arg = thm "contlub_cfun_arg";
-val contlub_cfun_fun = thm "contlub_cfun_fun";
-val fix_def2 = thm "fix_def2";
-val injection_eq = thm "injection_eq";
-val injection_less = thm "injection_less";
-val lub_equal = thm "lub_equal";
-val monofun_cfun_arg = thm "monofun_cfun_arg";
-val retraction_strict = thm "retraction_strict";
-val spair_eq = thm "spair_eq";
-val spair_less = thm "spair_less";
-val sscase1 = thm "sscase1";
-val ssplit1 = thm "ssplit1";
-val strictify1 = thm "strictify1";
-val wfix_ind = thm "wfix_ind";
-
-open Domain_Library;
-infixr 0 ===>;
-infixr 0 ==>;
-infix 0 == ;
-infix 1 ===;
-infix 1 ~= ;
-infix 1 <<;
-infix 1 ~<<;
-infix 9 ` ;
-infix 9 `% ;
-infix 9 `%%;
-infixr 9 oo;
-
-(* ----- general proof facilities ------------------------------------------- *)
-
-fun pg'' thy defs t tacs =
- let
- val t' = FixrecPackage.legacy_infer_term thy t;
- val asms = Logic.strip_imp_prems t';
- val prop = Logic.strip_imp_concl t';
- fun tac prems =
- rewrite_goals_tac defs THEN
- EVERY (tacs (map (rewrite_rule defs) prems));
- in Goal.prove_global thy [] asms prop tac end;
-
-fun pg' thy defs t tacsf =
- let
- fun tacs [] = tacsf
- | tacs prems = cut_facts_tac prems 1 :: tacsf;
- in pg'' thy defs t tacs end;
-
-fun case_UU_tac rews i v =
- case_tac (v^"=UU") i THEN
- asm_simp_tac (HOLCF_ss addsimps rews) i;
-
-val chain_tac =
- REPEAT_DETERM o resolve_tac
- [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL];
-
-(* ----- general proofs ----------------------------------------------------- *)
-
-val all2E = prove_goal HOL.thy "[| !x y . P x y; P x y ==> R |] ==> R"
- (fn prems =>[
- resolve_tac prems 1,
- cut_facts_tac prems 1,
- fast_tac HOL_cs 1]);
-
-val dist_eqI = prove_goal (the_context ()) "!!x::'a::po. ~ x << y ==> x ~= y"
- (fn prems =>
- [blast_tac (claset () addDs [antisym_less_inverse]) 1]);
-
-in
-
-fun theorems (((dname, _), cons) : eq, eqs : eq list) thy =
-let
-
-val dummy = writeln ("Proving isomorphism properties of domain "^dname^" ...");
-val pg = pg' thy;
-
-(* ----- getting the axioms and definitions --------------------------------- *)
-
-local
- fun ga s dn = get_thm thy (Name (dn ^ "." ^ s));
-in
- val ax_abs_iso = ga "abs_iso" dname;
- val ax_rep_iso = ga "rep_iso" dname;
- val ax_when_def = ga "when_def" dname;
- fun get_def mk_name (con,_) = ga (mk_name con^"_def") dname;
- val axs_con_def = map (get_def extern_name) cons;
- val axs_dis_def = map (get_def dis_name) cons;
- val axs_mat_def = map (get_def mat_name) cons;
- val axs_pat_def = map (get_def pat_name) cons;
- val axs_sel_def =
- let
- fun def_of_sel sel = ga (sel^"_def") dname;
- fun def_of_arg arg = Option.map def_of_sel (sel_of arg);
- fun defs_of_con (_, args) = List.mapPartial def_of_arg args;
- in
- List.concat (map defs_of_con cons)
- end;
- val ax_copy_def = ga "copy_def" dname;
-end; (* local *)
-
-(* ----- theorems concerning the isomorphism -------------------------------- *)
-
-val dc_abs = %%:(dname^"_abs");
-val dc_rep = %%:(dname^"_rep");
-val dc_copy = %%:(dname^"_copy");
-val x_name = "x";
-
-val iso_locale = iso_intro OF [ax_abs_iso, ax_rep_iso];
-val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
-val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
-val abs_defin' = iso_locale RS iso_abs_defin';
-val rep_defin' = iso_locale RS iso_rep_defin';
-val iso_rews = map standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
-
-(* ----- generating beta reduction rules from definitions-------------------- *)
-
-local
- fun arglist (Const _ $ Abs (s, _, t)) =
- let
- val (vars,body) = arglist t;
- in (s :: vars, body) end
- | arglist t = ([], t);
- fun bind_fun vars t = Library.foldr mk_All (vars, t);
- fun bound_vars 0 = []
- | bound_vars i = Bound (i-1) :: bound_vars (i - 1);
-in
- fun appl_of_def def =
- let
- val (_ $ con $ lam) = concl_of def;
- val (vars, rhs) = arglist lam;
- val lhs = list_ccomb (con, bound_vars (length vars));
- val appl = bind_fun vars (lhs == rhs);
- val cs = ContProc.cont_thms lam;
- val betas = map (fn c => mk_meta_eq (c RS beta_cfun)) cs;
- in pg (def::betas) appl [rtac reflexive_thm 1] end;
-end;
-
-val when_appl = appl_of_def ax_when_def;
-val con_appls = map appl_of_def axs_con_def;
-
-local
- fun arg2typ n arg =
- let val t = TVar (("'a", n), pcpoS)
- in (n + 1, if is_lazy arg then mk_uT t else t) end;
-
- fun args2typ n [] = (n, oneT)
- | args2typ n [arg] = arg2typ n arg
- | args2typ n (arg::args) =
- let
- val (n1, t1) = arg2typ n arg;
- val (n2, t2) = args2typ n1 args
- in (n2, mk_sprodT (t1, t2)) end;
-
- fun cons2typ n [] = (n,oneT)
- | cons2typ n [con] = args2typ n (snd con)
- | cons2typ n (con::cons) =
- let
- val (n1, t1) = args2typ n (snd con);
- val (n2, t2) = cons2typ n1 cons
- in (n2, mk_ssumT (t1, t2)) end;
-in
- fun cons2ctyp cons = ctyp_of thy (snd (cons2typ 1 cons));
-end;
-
-local
- val iso_swap = iso_locale RS iso_iso_swap;
- fun one_con (con, args) =
- let
- val vns = map vname args;
- val eqn = %:x_name === con_app2 con %: vns;
- val conj = foldr1 mk_conj (eqn :: map (defined o %:) (nonlazy args));
- in Library.foldr mk_ex (vns, conj) end;
-
- val conj_assoc = thm "conj_assoc";
- val exh = foldr1 mk_disj ((%:x_name === UU) :: map one_con cons);
- val thm1 = instantiate' [SOME (cons2ctyp cons)] [] exh_start;
- val thm2 = rewrite_rule (map mk_meta_eq ex_defined_iffs) thm1;
- val thm3 = rewrite_rule [mk_meta_eq conj_assoc] thm2;
-
- (* first 3 rules replace "x = UU \/ P" with "rep$x = UU \/ P" *)
- val tacs = [
- rtac disjE 1,
- etac (rep_defin' RS disjI1) 2,
- etac disjI2 2,
- rewrite_goals_tac [mk_meta_eq iso_swap],
- rtac thm3 1];
-in
- val exhaust = pg con_appls (mk_trp exh) tacs;
- val casedist =
- standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
-end;
-
-local
- fun bind_fun t = Library.foldr mk_All (when_funs cons, t);
- fun bound_fun i _ = Bound (length cons - i);
- val when_app = list_ccomb (%%:(dname^"_when"), mapn bound_fun 1 cons);
-in
- val when_strict =
- let
- val axs = [when_appl, mk_meta_eq rep_strict];
- val goal = bind_fun (mk_trp (strict when_app));
- val tacs = [resolve_tac [sscase1, ssplit1, strictify1] 1];
- in pg axs goal tacs end;
-
- val when_apps =
- let
- fun one_when n (con,args) =
- let
- val axs = when_appl :: con_appls;
- val goal = bind_fun (lift_defined %: (nonlazy args,
- mk_trp (when_app`(con_app con args) ===
- list_ccomb (bound_fun n 0, map %# args))));
- val tacs = [asm_simp_tac (HOLCF_ss addsimps [ax_abs_iso]) 1];
- in pg axs goal tacs end;
- in mapn one_when 1 cons end;
-end;
-val when_rews = when_strict :: when_apps;
-
-(* ----- theorems concerning the constructors, discriminators and selectors - *)
-
-local
- fun dis_strict (con, _) =
- let
- val goal = mk_trp (strict (%%:(dis_name con)));
- in pg axs_dis_def goal [rtac when_strict 1] end;
-
- fun dis_app c (con, args) =
- let
- val lhs = %%:(dis_name c) ` con_app con args;
- val rhs = %%:(if con = c then TT_N else FF_N);
- val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
- val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
- in pg axs_dis_def goal tacs end;
-
- val dis_apps = List.concat (map (fn (c,_) => map (dis_app c) cons) cons);
-
- fun dis_defin (con, args) =
- let
- val goal = defined (%:x_name) ==> defined (%%:(dis_name con) `% x_name);
- val tacs =
- [rtac casedist 1,
- contr_tac 1,
- DETERM_UNTIL_SOLVED (CHANGED
- (asm_simp_tac (HOLCF_ss addsimps dis_apps) 1))];
- in pg [] goal tacs end;
-
- val dis_stricts = map dis_strict cons;
- val dis_defins = map dis_defin cons;
-in
- val dis_rews = dis_stricts @ dis_defins @ dis_apps;
-end;
-
-local
- fun mat_strict (con, _) =
- let
- val goal = mk_trp (strict (%%:(mat_name con)));
- val tacs = [rtac when_strict 1];
- in pg axs_mat_def goal tacs end;
-
- val mat_stricts = map mat_strict cons;
-
- fun one_mat c (con, args) =
- let
- val lhs = %%:(mat_name c) ` con_app con args;
- val rhs =
- if con = c
- then %%:returnN ` mk_ctuple (map %# args)
- else %%:failN;
- val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
- val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
- in pg axs_mat_def goal tacs end;
-
- val mat_apps =
- List.concat (map (fn (c,_) => map (one_mat c) cons) cons);
-in
- val mat_rews = mat_stricts @ mat_apps;
-end;
-
-local
- fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
-
- fun pat_lhs (con,args) = %%:branchN $ list_comb (%%:(pat_name con), ps args);
-
- fun pat_rhs (con,[]) = %%:returnN ` ((%:"rhs") ` HOLogic.unit)
- | pat_rhs (con,args) =
- (%%:branchN $ foldr1 cpair_pat (ps args))
- `(%:"rhs")`(mk_ctuple (map %# args));
-
- fun pat_strict c =
- let
- val axs = branch_def :: axs_pat_def;
- val goal = mk_trp (strict (pat_lhs c ` (%:"rhs")));
- val tacs = [simp_tac (HOLCF_ss addsimps [when_strict]) 1];
- in pg axs goal tacs end;
-
- fun pat_app c (con, args) =
- let
- val axs = branch_def :: axs_pat_def;
- val lhs = (pat_lhs c)`(%:"rhs")`(con_app con args);
- val rhs = if con = fst c then pat_rhs c else %%:failN;
- val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
- val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
- in pg axs goal tacs end;
-
- val pat_stricts = map pat_strict cons;
- val pat_apps = List.concat (map (fn c => map (pat_app c) cons) cons);
-in
- val pat_rews = pat_stricts @ pat_apps;
-end;
-
-local
- val rev_contrapos = thm "rev_contrapos";
- fun con_strict (con, args) =
- let
- fun one_strict vn =
- let
- fun f arg = if vname arg = vn then UU else %# arg;
- val goal = mk_trp (con_app2 con f args === UU);
- val tacs = [asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1];
- in pg con_appls goal tacs end;
- in map one_strict (nonlazy args) end;
-
- fun con_defin (con, args) =
- let
- val concl = mk_trp (defined (con_app con args));
- val goal = lift_defined %: (nonlazy args, concl);
- val tacs = [
- rtac rev_contrapos 1,
- eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1,
- asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
- in pg [] goal tacs end;
-in
- val con_stricts = List.concat (map con_strict cons);
- val con_defins = map con_defin cons;
- val con_rews = con_stricts @ con_defins;
-end;
-
-local
- val rules =
- [compact_sinl, compact_sinr, compact_spair, compact_up, compact_ONE];
- fun con_compact (con, args) =
- let
- val concl = mk_trp (%%:compactN $ con_app con args);
- val goal = lift (fn x => %%:compactN $ %#x) (args, concl);
- val tacs = [
- rtac (iso_locale RS iso_compact_abs) 1,
- REPEAT (resolve_tac rules 1 ORELSE atac 1)];
- in pg con_appls goal tacs end;
-in
- val con_compacts = map con_compact cons;
-end;
-
-local
- fun one_sel sel =
- pg axs_sel_def (mk_trp (strict (%%:sel)))
- [simp_tac (HOLCF_ss addsimps when_rews) 1];
-
- fun sel_strict (_, args) =
- List.mapPartial (Option.map one_sel o sel_of) args;
-in
- val sel_stricts = List.concat (map sel_strict cons);
-end;
-
-local
- fun sel_app_same c n sel (con, args) =
- let
- val nlas = nonlazy args;
- val vns = map vname args;
- val vnn = List.nth (vns, n);
- val nlas' = List.filter (fn v => v <> vnn) nlas;
- val lhs = (%%:sel)`(con_app con args);
- val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn));
- val tacs1 =
- if vnn mem nlas
- then [case_UU_tac (when_rews @ con_stricts) 1 vnn]
- else [];
- val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
- in pg axs_sel_def goal (tacs1 @ tacs2) end;
-
- fun sel_app_diff c n sel (con, args) =
- let
- val nlas = nonlazy args;
- val goal = mk_trp (%%:sel ` con_app con args === UU);
- val tacs1 = map (case_UU_tac (when_rews @ con_stricts) 1) nlas;
- val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
- in pg axs_sel_def goal (tacs1 @ tacs2) end;
-
- fun sel_app c n sel (con, args) =
- if con = c
- then sel_app_same c n sel (con, args)
- else sel_app_diff c n sel (con, args);
-
- fun one_sel c n sel = map (sel_app c n sel) cons;
- fun one_sel' c n arg = Option.map (one_sel c n) (sel_of arg);
- fun one_con (c, args) =
- List.concat (List.mapPartial I (mapn (one_sel' c) 0 args));
-in
- val sel_apps = List.concat (map one_con cons);
-end;
-
-local
- fun sel_defin sel =
- let
- val goal = defined (%:x_name) ==> defined (%%:sel`%x_name);
- val tacs = [
- rtac casedist 1,
- contr_tac 1,
- DETERM_UNTIL_SOLVED (CHANGED
- (asm_simp_tac (HOLCF_ss addsimps sel_apps) 1))];
- in pg [] goal tacs end;
-in
- val sel_defins =
- if length cons = 1
- then List.mapPartial (fn arg => Option.map sel_defin (sel_of arg))
- (filter_out is_lazy (snd (hd cons)))
- else [];
-end;
-
-val sel_rews = sel_stricts @ sel_defins @ sel_apps;
-val rev_contrapos = thm "rev_contrapos";
-
-val distincts_le =
- let
- fun dist (con1, args1) (con2, args2) =
- let
- val goal = lift_defined %: (nonlazy args1,
- mk_trp (con_app con1 args1 ~<< con_app con2 args2));
- val tacs = [
- rtac rev_contrapos 1,
- eres_inst_tac [("f", dis_name con1)] monofun_cfun_arg 1]
- @ map (case_UU_tac (con_stricts @ dis_rews) 1) (nonlazy args2)
- @ [asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
- in pg [] goal tacs end;
-
- fun distinct (con1, args1) (con2, args2) =
- let
- val arg1 = (con1, args1);
- val arg2 =
- (con2, ListPair.map (fn (arg,vn) => upd_vname (K vn) arg)
- (args2, Name.variant_list (map vname args1) (map vname args2)));
- in [dist arg1 arg2, dist arg2 arg1] end;
- fun distincts [] = []
- | distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
- in distincts cons end;
-val dist_les = List.concat (List.concat distincts_le);
-val dist_eqs =
- let
- fun distinct (_,args1) ((_,args2), leqs) =
- let
- val (le1,le2) = (hd leqs, hd(tl leqs));
- val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI)
- in
- if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else
- if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else
- [eq1, eq2]
- end;
- fun distincts [] = []
- | distincts ((c,leqs)::cs) = List.concat
- (ListPair.map (distinct c) ((map #1 cs),leqs)) @
- distincts cs;
- in map standard (distincts (cons ~~ distincts_le)) end;
-
-local
- fun pgterm rel con args =
- let
- fun append s = upd_vname (fn v => v^s);
- val (largs, rargs) = (args, map (append "'") args);
- val concl =
- foldr1 mk_conj (ListPair.map rel (map %# largs, map %# rargs));
- val prem = rel (con_app con largs, con_app con rargs);
- val sargs = case largs of [_] => [] | _ => nonlazy args;
- val prop = lift_defined %: (sargs, mk_trp (prem === concl));
- in pg con_appls prop end;
- val cons' = List.filter (fn (_,args) => args<>[]) cons;
-in
- val inverts =
- let
- val abs_less = ax_abs_iso RS (allI RS injection_less);
- val tacs =
- [asm_full_simp_tac (HOLCF_ss addsimps [abs_less, spair_less]) 1];
- in map (fn (con, args) => pgterm (op <<) con args tacs) cons' end;
-
- val injects =
- let
- val abs_eq = ax_abs_iso RS (allI RS injection_eq);
- val tacs = [asm_full_simp_tac (HOLCF_ss addsimps [abs_eq, spair_eq]) 1];
- in map (fn (con, args) => pgterm (op ===) con args tacs) cons' end;
-end;
-
-(* ----- theorems concerning one induction step ----------------------------- *)
-
-val copy_strict =
- let
- val goal = mk_trp (strict (dc_copy `% "f"));
- val tacs = [asm_simp_tac (HOLCF_ss addsimps [abs_strict, when_strict]) 1];
- in pg [ax_copy_def] goal tacs end;
-
-local
- fun copy_app (con, args) =
- let
- val lhs = dc_copy`%"f"`(con_app con args);
- val rhs = con_app2 con (app_rec_arg (cproj (%:"f") eqs)) args;
- val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
- val args' = List.filter (fn a => not (is_rec a orelse is_lazy a)) args;
- val stricts = abs_strict::when_strict::con_stricts;
- val tacs1 = map (case_UU_tac stricts 1 o vname) args';
- val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_apps) 1];
- in pg [ax_copy_def] goal (tacs1 @ tacs2) end;
-in
- val copy_apps = map copy_app cons;
-end;
-
-local
- fun one_strict (con, args) =
- let
- val goal = mk_trp (dc_copy`UU`(con_app con args) === UU);
- val rews = copy_strict :: copy_apps @ con_rews;
- val tacs = map (case_UU_tac rews 1) (nonlazy args) @
- [asm_simp_tac (HOLCF_ss addsimps rews) 1];
- in pg [] goal tacs end;
-
- fun has_nonlazy_rec (_, args) = exists is_nonlazy_rec args;
-in
- val copy_stricts = map one_strict (List.filter has_nonlazy_rec cons);
-end;
-
-val copy_rews = copy_strict :: copy_apps @ copy_stricts;
-
-in
- thy
- |> Theory.add_path (Sign.base_name dname)
- |> (snd o (PureThy.add_thmss (map Thm.no_attributes [
- ("iso_rews" , iso_rews ),
- ("exhaust" , [exhaust] ),
- ("casedist" , [casedist]),
- ("when_rews", when_rews ),
- ("compacts", con_compacts),
- ("con_rews", con_rews),
- ("sel_rews", sel_rews),
- ("dis_rews", dis_rews),
- ("pat_rews", pat_rews),
- ("dist_les", dist_les),
- ("dist_eqs", dist_eqs),
- ("inverts" , inverts ),
- ("injects" , injects ),
- ("copy_rews", copy_rews)])))
- |> (snd o PureThy.add_thmss
- [(("match_rews", mat_rews), [Simplifier.simp_add])])
- |> Theory.parent_path
- |> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
- pat_rews @ dist_les @ dist_eqs @ copy_rews)
-end; (* let *)
-
-fun comp_theorems (comp_dnam, eqs: eq list) thy =
-let
-val dnames = map (fst o fst) eqs;
-val conss = map snd eqs;
-val comp_dname = Sign.full_name thy comp_dnam;
-
-val d = writeln("Proving induction properties of domain "^comp_dname^" ...");
-val pg = pg' thy;
-
-(* ----- getting the composite axiom and definitions ------------------------ *)
-
-local
- fun ga s dn = get_thm thy (Name (dn ^ "." ^ s));
-in
- val axs_reach = map (ga "reach" ) dnames;
- val axs_take_def = map (ga "take_def" ) dnames;
- val axs_finite_def = map (ga "finite_def") dnames;
- val ax_copy2_def = ga "copy_def" comp_dnam;
- val ax_bisim_def = ga "bisim_def" comp_dnam;
-end;
-
-local
- fun gt s dn = get_thm thy (Name (dn ^ "." ^ s));
- fun gts s dn = get_thms thy (Name (dn ^ "." ^ s));
-in
- val cases = map (gt "casedist" ) dnames;
- val con_rews = List.concat (map (gts "con_rews" ) dnames);
- val copy_rews = List.concat (map (gts "copy_rews") dnames);
-end;
-
-fun dc_take dn = %%:(dn^"_take");
-val x_name = idx_name dnames "x";
-val P_name = idx_name dnames "P";
-val n_eqs = length eqs;
-
-(* ----- theorems concerning finite approximation and finite induction ------ *)
-
-local
- val iterate_Cprod_ss = simpset_of (theory "Fix");
- val copy_con_rews = copy_rews @ con_rews;
- val copy_take_defs =
- (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
- val take_stricts =
- let
- fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n");
- val goal = mk_trp (foldr1 mk_conj (map one_eq eqs));
- val tacs = [
- induct_tac "n" 1,
- simp_tac iterate_Cprod_ss 1,
- asm_simp_tac (iterate_Cprod_ss addsimps copy_rews) 1];
- in pg copy_take_defs goal tacs end;
-
- val take_stricts' = rewrite_rule copy_take_defs take_stricts;
- fun take_0 n dn =
- let
- val goal = mk_trp ((dc_take dn $ %%:"HOL.zero") `% x_name n === UU);
- in pg axs_take_def goal [simp_tac iterate_Cprod_ss 1] end;
- val take_0s = mapn take_0 1 dnames;
- val c_UU_tac = case_UU_tac (take_stricts'::copy_con_rews) 1;
- val take_apps =
- let
- fun mk_eqn dn (con, args) =
- let
- fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
- val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args);
- val rhs = con_app2 con (app_rec_arg mk_take) args;
- in Library.foldr mk_all (map vname args, lhs === rhs) end;
- fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons;
- val goal = mk_trp (foldr1 mk_conj (List.concat (map mk_eqns eqs)));
- val simps = List.filter (has_fewer_prems 1) copy_rews;
- fun con_tac (con, args) =
- if nonlazy_rec args = []
- then all_tac
- else EVERY (map c_UU_tac (nonlazy_rec args)) THEN
- asm_full_simp_tac (HOLCF_ss addsimps copy_rews) 1;
- fun eq_tacs ((dn, _), cons) = map con_tac cons;
- val tacs =
- simp_tac iterate_Cprod_ss 1 ::
- induct_tac "n" 1 ::
- simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 ::
- asm_full_simp_tac (HOLCF_ss addsimps simps) 1 ::
- TRY (safe_tac HOL_cs) ::
- List.concat (map eq_tacs eqs);
- in pg copy_take_defs goal tacs end;
-in
- val take_rews = map standard
- (atomize take_stricts @ take_0s @ atomize take_apps);
-end; (* local *)
-
-local
- fun one_con p (con,args) =
- let
- fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg;
- val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args);
- val t2 = lift ind_hyp (List.filter is_rec args, t1);
- val t3 = lift_defined (bound_arg (map vname args)) (nonlazy args, t2);
- in Library.foldr mk_All (map vname args, t3) end;
-
- fun one_eq ((p, cons), concl) =
- mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl);
-
- fun ind_term concf = Library.foldr one_eq
- (mapn (fn n => fn x => (P_name n, x)) 1 conss,
- mk_trp (foldr1 mk_conj (mapn concf 1 dnames)));
- val take_ss = HOL_ss addsimps take_rews;
- fun quant_tac i = EVERY
- (mapn (fn n => fn _ => res_inst_tac [("x", x_name n)] spec i) 1 dnames);
-
- fun ind_prems_tac prems = EVERY
- (List.concat (map (fn cons =>
- (resolve_tac prems 1 ::
- List.concat (map (fn (_,args) =>
- resolve_tac prems 1 ::
- map (K(atac 1)) (nonlazy args) @
- map (K(atac 1)) (List.filter is_rec args))
- cons)))
- conss));
- local
- (* check whether every/exists constructor of the n-th part of the equation:
- it has a possibly indirectly recursive argument that isn't/is possibly
- indirectly lazy *)
- fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg =>
- is_rec arg andalso not(rec_of arg mem ns) andalso
- ((rec_of arg = n andalso nfn(lazy_rec orelse is_lazy arg)) orelse
- rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns)
- (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
- ) o snd) cons;
- fun all_rec_to ns = rec_to forall not all_rec_to ns;
- fun warn (n,cons) =
- if all_rec_to [] false (n,cons)
- then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true)
- else false;
- fun lazy_rec_to ns = rec_to exists I lazy_rec_to ns;
-
- in
- val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
- val is_emptys = map warn n__eqs;
- val is_finite = forall (not o lazy_rec_to [] false) n__eqs;
- end;
-in (* local *)
- val finite_ind =
- let
- fun concf n dn = %:(P_name n) $ (dc_take dn $ %:"n" `%(x_name n));
- val goal = ind_term concf;
-
- fun tacf prems =
- let
- val tacs1 = [
- quant_tac 1,
- simp_tac HOL_ss 1,
- induct_tac "n" 1,
- simp_tac (take_ss addsimps prems) 1,
- TRY (safe_tac HOL_cs)];
- fun arg_tac arg =
- case_UU_tac (prems @ con_rews) 1
- (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
- fun con_tacs (con, args) =
- asm_simp_tac take_ss 1 ::
- map arg_tac (List.filter is_nonlazy_rec args) @
- [resolve_tac prems 1] @
- map (K (atac 1)) (nonlazy args) @
- map (K (etac spec 1)) (List.filter is_rec args);
- fun cases_tacs (cons, cases) =
- res_inst_tac [("x","x")] cases 1 ::
- asm_simp_tac (take_ss addsimps prems) 1 ::
- List.concat (map con_tacs cons);
- in
- tacs1 @ List.concat (map cases_tacs (conss ~~ cases))
- end;
- in pg'' thy [] goal tacf end;
-
- val take_lemmas =
- let
- fun take_lemma n (dn, ax_reach) =
- let
- val lhs = dc_take dn $ Bound 0 `%(x_name n);
- val rhs = dc_take dn $ Bound 0 `%(x_name n^"'");
- val concl = mk_trp (%:(x_name n) === %:(x_name n^"'"));
- val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl;
- fun tacf prems = [
- res_inst_tac [("t", x_name n )] (ax_reach RS subst) 1,
- res_inst_tac [("t", x_name n^"'")] (ax_reach RS subst) 1,
- stac fix_def2 1,
- REPEAT (CHANGED
- (rtac (contlub_cfun_arg RS ssubst) 1 THEN chain_tac 1)),
- stac contlub_cfun_fun 1,
- stac contlub_cfun_fun 2,
- rtac lub_equal 3,
- chain_tac 1,
- rtac allI 1,
- resolve_tac prems 1];
- in pg'' thy axs_take_def goal tacf end;
- in mapn take_lemma 1 (dnames ~~ axs_reach) end;
-
-(* ----- theorems concerning finiteness and induction ----------------------- *)
-
- val (finites, ind) =
- if is_finite
- then (* finite case *)
- let
- fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %:"x" === %:"x");
- fun dname_lemma dn =
- let
- val prem1 = mk_trp (defined (%:"x"));
- val disj1 = mk_all ("n", dc_take dn $ Bound 0 ` %:"x" === UU);
- val prem2 = mk_trp (mk_disj (disj1, take_enough dn));
- val concl = mk_trp (take_enough dn);
- val goal = prem1 ===> prem2 ===> concl;
- val tacs = [
- etac disjE 1,
- etac notE 1,
- resolve_tac take_lemmas 1,
- asm_simp_tac take_ss 1,
- atac 1];
- in pg [] goal tacs end;
- val finite_lemmas1a = map dname_lemma dnames;
-
- val finite_lemma1b =
- let
- fun mk_eqn n ((dn, args), _) =
- let
- val disj1 = dc_take dn $ Bound 1 ` Bound 0 === UU;
- val disj2 = dc_take dn $ Bound 1 ` Bound 0 === Bound 0;
- in
- mk_constrainall
- (x_name n, Type (dn,args), mk_disj (disj1, disj2))
- end;
- val goal =
- mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs)));
- fun arg_tacs vn = [
- eres_inst_tac [("x", vn)] all_dupE 1,
- etac disjE 1,
- asm_simp_tac (HOL_ss addsimps con_rews) 1,
- asm_simp_tac take_ss 1];
- fun con_tacs (con, args) =
- asm_simp_tac take_ss 1 ::
- List.concat (map arg_tacs (nonlazy_rec args));
- fun foo_tacs n (cons, cases) =
- simp_tac take_ss 1 ::
- rtac allI 1 ::
- res_inst_tac [("x",x_name n)] cases 1 ::
- asm_simp_tac take_ss 1 ::
- List.concat (map con_tacs cons);
- val tacs =
- rtac allI 1 ::
- induct_tac "n" 1 ::
- simp_tac take_ss 1 ::
- TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) ::
- List.concat (mapn foo_tacs 1 (conss ~~ cases));
- in pg [] goal tacs end;
-
- fun one_finite (dn, l1b) =
- let
- val goal = mk_trp (%%:(dn^"_finite") $ %:"x");
- val tacs = [
- case_UU_tac take_rews 1 "x",
- eresolve_tac finite_lemmas1a 1,
- step_tac HOL_cs 1,
- step_tac HOL_cs 1,
- cut_facts_tac [l1b] 1,
- fast_tac HOL_cs 1];
- in pg axs_finite_def goal tacs end;
-
- val finites = map one_finite (dnames ~~ atomize finite_lemma1b);
- val ind =
- let
- fun concf n dn = %:(P_name n) $ %:(x_name n);
- fun tacf prems =
- let
- fun finite_tacs (finite, fin_ind) = [
- rtac(rewrite_rule axs_finite_def finite RS exE)1,
- etac subst 1,
- rtac fin_ind 1,
- ind_prems_tac prems];
- in
- TRY (safe_tac HOL_cs) ::
- List.concat (map finite_tacs (finites ~~ atomize finite_ind))
- end;
- in pg'' thy [] (ind_term concf) tacf end;
- in (finites, ind) end (* let *)
-
- else (* infinite case *)
- let
- fun one_finite n dn =
- read_instantiate_sg thy
- [("P",dn^"_finite "^x_name n)] excluded_middle;
- val finites = mapn one_finite 1 dnames;
-
- val goal =
- let
- fun one_adm n _ = mk_trp (%%:admN $ %:(P_name n));
- fun concf n dn = %:(P_name n) $ %:(x_name n);
- in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end;
- fun tacf prems =
- map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [
- quant_tac 1,
- rtac (adm_impl_admw RS wfix_ind) 1,
- REPEAT_DETERM (rtac adm_all2 1),
- REPEAT_DETERM (
- TRY (rtac adm_conj 1) THEN
- rtac adm_subst 1 THEN
- cont_tacR 1 THEN resolve_tac prems 1),
- strip_tac 1,
- rtac (rewrite_rule axs_take_def finite_ind) 1,
- ind_prems_tac prems];
- val ind = (pg'' thy [] goal tacf
- handle ERROR _ =>
- (warning "Cannot prove infinite induction rule"; refl));
- in (finites, ind) end;
-end; (* local *)
-
-(* ----- theorem concerning coinduction ------------------------------------- *)
-
-local
- val xs = mapn (fn n => K (x_name n)) 1 dnames;
- fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
- val take_ss = HOL_ss addsimps take_rews;
- val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")"));
- val coind_lemma =
- let
- fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1;
- fun mk_eqn n dn =
- (dc_take dn $ %:"n" ` bnd_arg n 0) ===
- (dc_take dn $ %:"n" ` bnd_arg n 1);
- fun mk_all2 (x,t) = mk_all (x, mk_all (x^"'", t));
- val goal =
- mk_trp (mk_imp (%%:(comp_dname^"_bisim") $ %:"R",
- Library.foldr mk_all2 (xs,
- Library.foldr mk_imp (mapn mk_prj 0 dnames,
- foldr1 mk_conj (mapn mk_eqn 0 dnames)))));
- fun x_tacs n x = [
- rotate_tac (n+1) 1,
- etac all2E 1,
- eres_inst_tac [("P1", sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
- TRY (safe_tac HOL_cs),
- REPEAT (CHANGED (asm_simp_tac take_ss 1))];
- val tacs = [
- rtac impI 1,
- induct_tac "n" 1,
- simp_tac take_ss 1,
- safe_tac HOL_cs] @
- List.concat (mapn x_tacs 0 xs);
- in pg [ax_bisim_def] goal tacs end;
-in
- val coind =
- let
- fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'"));
- fun mk_eqn x = %:x === %:(x^"'");
- val goal =
- mk_trp (%%:(comp_dname^"_bisim") $ %:"R") ===>
- Logic.list_implies (mapn mk_prj 0 xs,
- mk_trp (foldr1 mk_conj (map mk_eqn xs)));
- val tacs =
- TRY (safe_tac HOL_cs) ::
- List.concat (map (fn take_lemma => [
- rtac take_lemma 1,
- cut_facts_tac [coind_lemma] 1,
- fast_tac HOL_cs 1])
- take_lemmas);
- in pg [] goal tacs end;
-end; (* local *)
-
-in thy |> Theory.add_path comp_dnam
- |> (snd o (PureThy.add_thmss (map Thm.no_attributes [
- ("take_rews" , take_rews ),
- ("take_lemmas", take_lemmas),
- ("finites" , finites ),
- ("finite_ind", [finite_ind]),
- ("ind" , [ind ]),
- ("coind" , [coind ])])))
- |> Theory.parent_path |> rpair take_rews
-end; (* let *)
-end; (* local *)
-end; (* struct *)
--- a/src/HOLCF/fixrec_package.ML Thu May 31 13:24:13 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,317 +0,0 @@
-(* Title: HOLCF/fixrec_package.ML
- ID: $Id$
- Author: Amber Telfer and Brian Huffman
-
-Recursive function definition package for HOLCF.
-*)
-
-signature FIXREC_PACKAGE =
-sig
- val legacy_infer_term: theory -> term -> term
- val legacy_infer_prop: theory -> term -> term
- val add_fixrec: bool -> ((string * Attrib.src list) * string) list list -> theory -> theory
- val add_fixrec_i: bool -> ((string * attribute list) * term) list list -> theory -> theory
- val add_fixpat: (string * Attrib.src list) * string list -> theory -> theory
- val add_fixpat_i: (string * attribute list) * term list -> theory -> theory
-end;
-
-structure FixrecPackage: FIXREC_PACKAGE =
-struct
-
-(* legacy type inference *)
-
-fun legacy_infer_term thy t =
- singleton (ProofContext.infer_types (ProofContext.init thy)) (Sign.intern_term thy t);
-
-fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain t propT);
-
-
-val fix_eq2 = thm "fix_eq2";
-val def_fix_ind = thm "def_fix_ind";
-
-
-fun fixrec_err s = error ("fixrec definition error:\n" ^ s);
-fun fixrec_eq_err thy s eq =
- fixrec_err (s ^ "\nin\n" ^ quote (Sign.string_of_term thy eq));
-
-(* ->> is taken from holcf_logic.ML *)
-(* TODO: fix dependencies so we can import HOLCFLogic here *)
-infixr 6 ->>;
-fun S ->> T = Type ("Cfun.->",[S,T]);
-
-(* extern_name is taken from domain/library.ML *)
-fun extern_name con = case Symbol.explode con of
- ("o"::"p"::" "::rest) => implode rest
- | _ => con;
-
-val mk_trp = HOLogic.mk_Trueprop;
-
-(* splits a cterm into the right and lefthand sides of equality *)
-fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
-
-(* similar to Thm.head_of, but for continuous application *)
-fun chead_of (Const("Cfun.Rep_CFun",_)$f$t) = chead_of f
- | chead_of u = u;
-
-(* these are helpful functions copied from HOLCF/domain/library.ML *)
-fun %: s = Free(s,dummyT);
-fun %%: s = Const(s,dummyT);
-infix 0 ==; fun S == T = %%:"==" $ S $ T;
-infix 1 ===; fun S === T = %%:"op =" $ S $ T;
-infix 9 ` ; fun f ` x = %%:"Cfun.Rep_CFun" $ f $ x;
-
-(* builds the expression (LAM v. rhs) *)
-fun big_lambda v rhs = %%:"Cfun.Abs_CFun"$(Term.lambda v rhs);
-
-(* builds the expression (LAM v1 v2 .. vn. rhs) *)
-fun big_lambdas [] rhs = rhs
- | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs);
-
-(* builds the expression (LAM <v1,v2,..,vn>. rhs) *)
-fun lambda_ctuple [] rhs = big_lambda (%:"unit") rhs
- | lambda_ctuple (v::[]) rhs = big_lambda v rhs
- | lambda_ctuple (v::vs) rhs =
- %%:"Cprod.csplit"`(big_lambda v (lambda_ctuple vs rhs));
-
-(* builds the expression <v1,v2,..,vn> *)
-fun mk_ctuple [] = %%:"UU"
-| mk_ctuple (t::[]) = t
-| mk_ctuple (t::ts) = %%:"Cprod.cpair"`t`(mk_ctuple ts);
-
-(*************************************************************************)
-(************* fixed-point definitions and unfolding theorems ************)
-(*************************************************************************)
-
-fun add_fixdefs eqs thy =
- let
- val (lhss,rhss) = ListPair.unzip (map dest_eqs eqs);
- val fixpoint = %%:"Fix.fix"`lambda_ctuple lhss (mk_ctuple rhss);
-
- fun one_def (l as Const(n,T)) r =
- let val b = Sign.base_name n in (b, (b^"_def", l == r)) end
- | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form";
- fun defs [] _ = []
- | defs (l::[]) r = [one_def l r]
- | defs (l::ls) r = one_def l (%%:"Cprod.cfst"`r) :: defs ls (%%:"Cprod.csnd"`r);
- val (names, pre_fixdefs) = ListPair.unzip (defs lhss fixpoint);
-
- val fixdefs = map (apsnd (legacy_infer_prop thy)) pre_fixdefs;
- val (fixdef_thms, thy') =
- PureThy.add_defs_i false (map Thm.no_attributes fixdefs) thy;
- val ctuple_fixdef_thm = foldr1 (fn (x,y) => cpair_equalI OF [x,y]) fixdef_thms;
-
- val ctuple_unfold = legacy_infer_term thy' (mk_trp (mk_ctuple lhss === mk_ctuple rhss));
- val ctuple_unfold_thm = Goal.prove_global thy' [] [] ctuple_unfold
- (fn _ => EVERY [rtac (ctuple_fixdef_thm RS fix_eq2 RS trans) 1,
- simp_tac (simpset_of thy') 1]);
- val ctuple_induct_thm =
- (space_implode "_" names ^ "_induct", ctuple_fixdef_thm RS def_fix_ind);
-
- fun unfolds [] thm = []
- | unfolds (n::[]) thm = [(n^"_unfold", thm)]
- | unfolds (n::ns) thm = let
- val thmL = thm RS cpair_eqD1;
- val thmR = thm RS cpair_eqD2;
- in (n^"_unfold", thmL) :: unfolds ns thmR end;
- val unfold_thms = unfolds names ctuple_unfold_thm;
- val thms = ctuple_induct_thm :: unfold_thms;
- val (_, thy'') = PureThy.add_thms (map Thm.no_attributes thms) thy';
- in
- (thy'', names, fixdef_thms, map snd unfold_thms)
- end;
-
-(*************************************************************************)
-(*********** monadic notation and pattern matching compilation ***********)
-(*************************************************************************)
-
-fun add_names (Const(a,_), bs) = insert (op =) (Sign.base_name a) bs
- | add_names (Free(a,_) , bs) = insert (op =) a bs
- | add_names (f $ u , bs) = add_names (f, add_names(u, bs))
- | add_names (Abs(a,_,t), bs) = add_names (t, insert (op =) a bs)
- | add_names (_ , bs) = bs;
-
-fun add_terms ts xs = foldr add_names xs ts;
-
-(* builds a monadic term for matching a constructor pattern *)
-fun pre_build pat rhs vs taken =
- case pat of
- Const("Cfun.Rep_CFun",_)$f$(v as Free(n,T)) =>
- pre_build f rhs (v::vs) taken
- | Const("Cfun.Rep_CFun",_)$f$x =>
- let val (rhs', v, taken') = pre_build x rhs [] taken;
- in pre_build f rhs' (v::vs) taken' end
- | Const(c,T) =>
- let
- val n = Name.variant taken "v";
- fun result_type (Type("Cfun.->",[_,T])) (x::xs) = result_type T xs
- | result_type T _ = T;
- val v = Free(n, result_type T vs);
- val m = "match_"^(extern_name(Sign.base_name c));
- val k = lambda_ctuple vs rhs;
- in
- (%%:"Fixrec.bind"`(%%:m`v)`k, v, n::taken)
- end
- | Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n)
- | _ => fixrec_err "pre_build: invalid pattern";
-
-(* builds a monadic term for matching a function definition pattern *)
-(* returns (name, arity, matcher) *)
-fun building pat rhs vs taken =
- case pat of
- Const("Cfun.Rep_CFun", _)$f$(v as Free(n,T)) =>
- building f rhs (v::vs) taken
- | Const("Cfun.Rep_CFun", _)$f$x =>
- let val (rhs', v, taken') = pre_build x rhs [] taken;
- in building f rhs' (v::vs) taken' end
- | Const(name,_) => (name, length vs, big_lambdas vs rhs)
- | _ => fixrec_err "function is not declared as constant in theory";
-
-fun match_eq eq =
- let val (lhs,rhs) = dest_eqs eq;
- in building lhs (%%:"Fixrec.return"`rhs) [] (add_terms [eq] []) end;
-
-(* returns the sum (using +++) of the terms in ms *)
-(* also applies "run" to the result! *)
-fun fatbar arity ms =
- let
- fun unLAM 0 t = t
- | unLAM n (_$Abs(_,_,t)) = unLAM (n-1) t
- | unLAM _ _ = fixrec_err "fatbar: internal error, not enough LAMs";
- fun reLAM 0 t = t
- | reLAM n t = reLAM (n-1) (%%:"Cfun.Abs_CFun" $ Abs("",dummyT,t));
- fun mplus (x,y) = %%:"Fixrec.mplus"`x`y;
- val msum = foldr1 mplus (map (unLAM arity) ms);
- in
- reLAM arity (%%:"Fixrec.run"`msum)
- end;
-
-fun unzip3 [] = ([],[],[])
- | unzip3 ((x,y,z)::ts) =
- let val (xs,ys,zs) = unzip3 ts
- in (x::xs, y::ys, z::zs) end;
-
-(* this is the pattern-matching compiler function *)
-fun compile_pats eqs =
- let
- val ((n::names),(a::arities),mats) = unzip3 (map match_eq eqs);
- val cname = if forall (fn x => n=x) names then n
- else fixrec_err "all equations in block must define the same function";
- val arity = if forall (fn x => a=x) arities then a
- else fixrec_err "all equations in block must have the same arity";
- val rhs = fatbar arity mats;
- in
- mk_trp (%%:cname === rhs)
- end;
-
-(*************************************************************************)
-(********************** Proving associated theorems **********************)
-(*************************************************************************)
-
-(* proves a block of pattern matching equations as theorems, using unfold *)
-fun make_simps thy (unfold_thm, eqns) =
- let
- val tacs = [rtac (unfold_thm RS ssubst_lhs) 1, asm_simp_tac (simpset_of thy) 1];
- fun prove_term t = Goal.prove_global thy [] [] t (K (EVERY tacs));
- fun prove_eqn ((name, eqn_t), atts) = ((name, prove_term eqn_t), atts);
- in
- map prove_eqn eqns
- end;
-
-(*************************************************************************)
-(************************* Main fixrec function **************************)
-(*************************************************************************)
-
-fun gen_add_fixrec prep_prop prep_attrib strict blocks thy =
- let
- val eqns = List.concat blocks;
- val lengths = map length blocks;
-
- val ((names, srcss), strings) = apfst split_list (split_list eqns);
- val atts = map (map (prep_attrib thy)) srcss;
- val eqn_ts = map (prep_prop thy) strings;
- val rec_ts = map (fn eq => chead_of (fst (dest_eqs (Logic.strip_imp_concl eq)))
- handle TERM _ => fixrec_eq_err thy "not a proper equation" eq) eqn_ts;
- val (_, eqn_ts') = OldInductivePackage.unify_consts thy rec_ts eqn_ts;
-
- fun unconcat [] _ = []
- | unconcat (n::ns) xs = List.take (xs,n) :: unconcat ns (List.drop (xs,n));
- val pattern_blocks = unconcat lengths (map Logic.strip_imp_concl eqn_ts');
- val compiled_ts = map (legacy_infer_term thy o compile_pats) pattern_blocks;
- val (thy', cnames, fixdef_thms, unfold_thms) = add_fixdefs compiled_ts thy;
- in
- if strict then let (* only prove simp rules if strict = true *)
- val eqn_blocks = unconcat lengths ((names ~~ eqn_ts') ~~ atts);
- val simps = List.concat (map (make_simps thy') (unfold_thms ~~ eqn_blocks));
- val (simp_thms, thy'') = PureThy.add_thms simps thy';
-
- val simp_names = map (fn name => name^"_simps") cnames;
- val simp_attribute = rpair [Simplifier.simp_add];
- val simps' = map simp_attribute (simp_names ~~ unconcat lengths simp_thms);
- in
- (snd o PureThy.add_thmss simps') thy''
- end
- else thy'
- end;
-
-val add_fixrec = gen_add_fixrec Sign.read_prop Attrib.attribute;
-val add_fixrec_i = gen_add_fixrec Sign.cert_prop (K I);
-
-
-(*************************************************************************)
-(******************************** Fixpat *********************************)
-(*************************************************************************)
-
-fun fix_pat thy t =
- let
- val T = fastype_of t;
- val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
- val cname = case chead_of t of Const(c,_) => c | _ =>
- fixrec_err "function is not declared as constant in theory";
- val unfold_thm = PureThy.get_thm thy (Name (cname^"_unfold"));
- val simp = Goal.prove_global thy [] [] eq
- (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
- in simp end;
-
-fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy =
- let
- val atts = map (prep_attrib thy) srcs;
- val ts = map (prep_term thy) strings;
- val simps = map (fix_pat thy) ts;
- in
- (snd o PureThy.add_thmss [((name, simps), atts)]) thy
- end;
-
-val add_fixpat = gen_add_fixpat Sign.read_term Attrib.attribute;
-val add_fixpat_i = gen_add_fixpat Sign.cert_term (K I);
-
-
-(*************************************************************************)
-(******************************** Parsers ********************************)
-(*************************************************************************)
-
-local structure P = OuterParse and K = OuterKeyword in
-
-val fixrec_eqn = SpecParse.opt_thm_name ":" -- P.prop;
-
-val fixrec_strict = P.opt_keyword "permissive" >> not;
-
-val fixrec_decl = fixrec_strict -- P.and_list1 (Scan.repeat1 fixrec_eqn);
-
-(* this builds a parser for a new keyword, fixrec, whose functionality
-is defined by add_fixrec *)
-val fixrecP =
- OuterSyntax.command "fixrec" "define recursive functions (HOLCF)" K.thy_decl
- (fixrec_decl >> (Toplevel.theory o uncurry add_fixrec));
-
-(* fixpat parser *)
-val fixpat_decl = SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop;
-
-val fixpatP =
- OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
- (fixpat_decl >> (Toplevel.theory o add_fixpat));
-
-val _ = OuterSyntax.add_parsers [fixrecP, fixpatP];
-
-end; (* local structure *)
-
-end; (* struct *)
--- a/src/HOLCF/pcpodef_package.ML Thu May 31 13:24:13 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,213 +0,0 @@
-(* Title: HOLCF/pcpodef_package.ML
- ID: $Id$
- Author: Brian Huffman
-
-Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
-typedef.
-*)
-
-signature PCPODEF_PACKAGE =
-sig
- val quiet_mode: bool ref
- val pcpodef_proof: (bool * string) * (bstring * string list * mixfix) * string
- * (string * string) option -> theory -> Proof.state
- val pcpodef_proof_i: (bool * string) * (bstring * string list * mixfix) * term
- * (string * string) option -> theory -> Proof.state
- val cpodef_proof: (bool * string) * (bstring * string list * mixfix) * string
- * (string * string) option -> theory -> Proof.state
- val cpodef_proof_i: (bool * string) * (bstring * string list * mixfix) * term
- * (string * string) option -> theory -> Proof.state
-end;
-
-structure PcpodefPackage: PCPODEF_PACKAGE =
-struct
-
-(** theory context references **)
-
-val typedef_po = thm "typedef_po";
-val typedef_cpo = thm "typedef_cpo";
-val typedef_pcpo = thm "typedef_pcpo";
-val typedef_lub = thm "typedef_lub";
-val typedef_thelub = thm "typedef_thelub";
-val typedef_compact = thm "typedef_compact";
-val cont_Rep = thm "typedef_cont_Rep";
-val cont_Abs = thm "typedef_cont_Abs";
-val Rep_strict = thm "typedef_Rep_strict";
-val Abs_strict = thm "typedef_Abs_strict";
-val Rep_defined = thm "typedef_Rep_defined";
-val Abs_defined = thm "typedef_Abs_defined";
-
-
-(** type definitions **)
-
-(* messages *)
-
-val quiet_mode = ref false;
-fun message s = if ! quiet_mode then () else writeln s;
-
-
-(* prepare_cpodef *)
-
-fun err_in_cpodef msg name =
- cat_error msg ("The error(s) above occurred in cpodef " ^ quote name);
-
-fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
-
-fun adm_const T = Const ("Adm.adm", (T --> HOLogic.boolT) --> HOLogic.boolT);
-fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
-
-fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy =
- let
- val ctxt = ProofContext.init thy;
- val full = Sign.full_name thy;
-
- (*rhs*)
- val full_name = full name;
- val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
- val setT = Term.fastype_of set;
- val rhs_tfrees = term_tfrees set;
- val oldT = HOLogic.dest_setT setT handle TYPE _ =>
- error ("Not a set type: " ^ quote (ProofContext.string_of_typ ctxt setT));
- fun mk_nonempty A =
- HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A));
- fun mk_admissible A =
- mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A));
- fun mk_UU_mem A = HOLogic.mk_mem (Const ("Pcpo.UU", oldT), A);
- val goal = if pcpo
- then HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_UU_mem set, mk_admissible set))
- else HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_nonempty set, mk_admissible set));
-
- (*lhs*)
- val defS = Sign.defaultS thy;
- val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
- val lhs_sorts = map snd lhs_tfrees;
- val tname = Syntax.type_name t mx;
- val full_tname = full tname;
- val newT = Type (full_tname, map TFree lhs_tfrees);
-
- val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs;
- val RepC = Const (full Rep_name, newT --> oldT);
- fun lessC T = Const ("Porder.<<", T --> T --> HOLogic.boolT);
- val less_def = ("less_" ^ name ^ "_def", Logic.mk_equals (lessC newT,
- Abs ("x", newT, Abs ("y", newT, lessC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0)))));
-
- fun make_po tac theory = theory
- |> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac
- ||> AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.sq_ord"])
- (ClassPackage.intro_classes_tac [])
- ||>> PureThy.add_defs_i true [Thm.no_attributes less_def]
- |-> (fn ((_, {type_definition, set_def, ...}), [less_definition]) =>
- AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.po"])
- (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1)
- #> pair (type_definition, less_definition, set_def));
-
- fun make_cpo admissible (type_def, less_def, set_def) theory =
- let
- val admissible' = fold_rule (the_list set_def) admissible;
- val cpo_thms = [type_def, less_def, admissible'];
- in
- theory
- |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.cpo"])
- (Tactic.rtac (typedef_cpo OF cpo_thms) 1)
- |> Theory.add_path name
- |> PureThy.add_thms
- ([(("adm_" ^ name, admissible'), []),
- (("cont_" ^ Rep_name, cont_Rep OF cpo_thms), []),
- (("cont_" ^ Abs_name, cont_Abs OF cpo_thms), []),
- (("lub_" ^ name, typedef_lub OF cpo_thms), []),
- (("thelub_" ^ name, typedef_thelub OF cpo_thms), []),
- (("compact_" ^ name, typedef_compact OF cpo_thms), [])])
- |> snd
- |> Theory.parent_path
- end;
-
- fun make_pcpo UUmem (type_def, less_def, set_def) theory =
- let
- val UUmem' = fold_rule (the_list set_def) UUmem;
- val pcpo_thms = [type_def, less_def, UUmem'];
- in
- theory
- |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.pcpo"])
- (Tactic.rtac (typedef_pcpo OF pcpo_thms) 1)
- |> Theory.add_path name
- |> PureThy.add_thms
- ([((Rep_name ^ "_strict", Rep_strict OF pcpo_thms), []),
- ((Abs_name ^ "_strict", Abs_strict OF pcpo_thms), []),
- ((Rep_name ^ "_defined", Rep_defined OF pcpo_thms), []),
- ((Abs_name ^ "_defined", Abs_defined OF pcpo_thms), [])
- ])
- |> snd
- |> Theory.parent_path
- end;
-
- fun pcpodef_result UUmem_admissible theory =
- let
- val UUmem = UUmem_admissible RS conjunct1;
- val admissible = UUmem_admissible RS conjunct2;
- in
- theory
- |> make_po (Tactic.rtac exI 1 THEN Tactic.rtac UUmem 1)
- |-> (fn defs => make_cpo admissible defs #> make_pcpo UUmem defs)
- end;
-
- fun cpodef_result nonempty_admissible theory =
- let
- val nonempty = nonempty_admissible RS conjunct1;
- val admissible = nonempty_admissible RS conjunct2;
- in
- theory
- |> make_po (Tactic.rtac nonempty 1)
- |-> make_cpo admissible
- end;
-
- in (goal, if pcpo then pcpodef_result else cpodef_result) end
- handle ERROR msg => err_in_cpodef msg name;
-
-
-(* cpodef_proof interface *)
-
-fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy =
- let
- val (goal, pcpodef_result) =
- prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy;
- fun after_qed [[th]] = ProofContext.theory (pcpodef_result th);
- in Proof.theorem_i NONE after_qed [[(goal, [])]] (ProofContext.init thy) end;
-
-fun pcpodef_proof x = gen_pcpodef_proof ProofContext.read_term true x;
-fun pcpodef_proof_i x = gen_pcpodef_proof ProofContext.cert_term true x;
-
-fun cpodef_proof x = gen_pcpodef_proof ProofContext.read_term false x;
-fun cpodef_proof_i x = gen_pcpodef_proof ProofContext.cert_term false x;
-
-
-(** outer syntax **)
-
-local structure P = OuterParse and K = OuterKeyword in
-
-(* copied from HOL/Tools/typedef_package.ML *)
-val typedef_proof_decl =
- Scan.optional (P.$$$ "(" |--
- ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
- --| P.$$$ ")") (true, NONE) --
- (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
-
-fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
- (if pcpo then pcpodef_proof else cpodef_proof)
- ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
-
-val pcpodefP =
- OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
- (typedef_proof_decl >>
- (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
-
-val cpodefP =
- OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
- (typedef_proof_decl >>
- (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
-
-val _ = OuterSyntax.add_parsers [pcpodefP, cpodefP];
-
-end;
-
-end;