--- a/src/HOLCF/Representable.thy Wed Mar 03 17:08:41 2010 +0100
+++ b/src/HOLCF/Representable.thy Wed Mar 03 10:40:40 2010 -0800
@@ -189,21 +189,21 @@
lemma deflation_chain_min:
assumes chain: "chain d"
- assumes defl: "\<And>i. deflation (d i)"
- shows "d i\<cdot>(d j\<cdot>x) = d (min i j)\<cdot>x"
+ assumes defl: "\<And>n. deflation (d n)"
+ shows "d m\<cdot>(d n\<cdot>x) = d (min m n)\<cdot>x"
proof (rule linorder_le_cases)
- assume "i \<le> j"
- with chain have "d i \<sqsubseteq> d j" by (rule chain_mono)
- then have "d i\<cdot>(d j\<cdot>x) = d i\<cdot>x"
+ assume "m \<le> n"
+ with chain have "d m \<sqsubseteq> d n" by (rule chain_mono)
+ then have "d m\<cdot>(d n\<cdot>x) = d m\<cdot>x"
by (rule deflation_below_comp1 [OF defl defl])
- moreover from `i \<le> j` have "min i j = i" by simp
+ moreover from `m \<le> n` have "min m n = m" by simp
ultimately show ?thesis by simp
next
- assume "j \<le> i"
- with chain have "d j \<sqsubseteq> d i" by (rule chain_mono)
- then have "d i\<cdot>(d j\<cdot>x) = d j\<cdot>x"
+ assume "n \<le> m"
+ with chain have "d n \<sqsubseteq> d m" by (rule chain_mono)
+ then have "d m\<cdot>(d n\<cdot>x) = d n\<cdot>x"
by (rule deflation_below_comp2 [OF defl defl])
- moreover from `j \<le> i` have "min i j = j" by simp
+ moreover from `n \<le> m` have "min m n = n" by simp
ultimately show ?thesis by simp
qed
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML Wed Mar 03 17:08:41 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Wed Mar 03 10:40:40 2010 -0800
@@ -11,42 +11,23 @@
binding * (typ * typ) ->
theory -> Domain_Take_Proofs.iso_info * theory
- val copy_of_dtyp :
- string Symtab.table -> (int -> term) -> Datatype.dtyp -> term
+ val axiomatize_lub_take :
+ binding * term -> theory -> thm * theory
val add_axioms :
- (binding * (typ * typ)) list ->
- theory -> theory
+ (binding * (typ * typ)) list -> theory ->
+ Domain_Take_Proofs.iso_info list * theory
end;
structure Domain_Axioms : DOMAIN_AXIOMS =
struct
-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;
+open HOLCF_Library;
-(* FIXME: use theory data for this *)
-val copy_tab : string Symtab.table =
- Symtab.make [(@{type_name cfun}, @{const_name "cfun_map"}),
- (@{type_name ssum}, @{const_name "ssum_map"}),
- (@{type_name sprod}, @{const_name "sprod_map"}),
- (@{type_name "*"}, @{const_name "cprod_map"}),
- (@{type_name "u"}, @{const_name "u_map"})];
-
-fun copy_of_dtyp tab r dt =
- if Datatype_Aux.is_rec_type dt then copy tab r dt else ID
-and copy tab r (Datatype_Aux.DtRec i) = r i
- | copy tab r (Datatype_Aux.DtTFree a) = ID
- | copy tab r (Datatype_Aux.DtType (c, ds)) =
- case Symtab.lookup tab c of
- SOME f => list_ccomb (%%:f, map (copy_of_dtyp tab r) ds)
- | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID);
-
-local open HOLCF_Library in
+infixr 6 ->>;
+infix -->>;
+infix 9 `;
fun axiomatize_isomorphism
(dbind : binding, (lhsT, rhsT))
@@ -96,20 +77,29 @@
(result, thy)
end;
-end;
+fun axiomatize_lub_take
+ (dbind : binding, take_const : term)
+ (thy : theory)
+ : thm * theory =
+ let
+ val dname = Long_Name.base_name (Binding.name_of dbind);
-(* legacy type inference *)
-
-fun legacy_infer_term thy t =
- singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t);
+ val i = Free ("i", natT);
+ val T = (fst o dest_cfunT o range_type o fastype_of) take_const;
-fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
+ val lub_take_eqn =
+ mk_trp (mk_eq (mk_lub (lambda i (take_const $ i)), mk_ID T));
-fun infer_props thy = map (apsnd (legacy_infer_prop thy));
+ val thy = Sign.add_path dname thy;
+ val (lub_take_thm, thy) =
+ yield_singleton PureThy.add_axioms
+ ((Binding.name "lub_take", lub_take_eqn), []) thy;
-fun add_axioms_i x = snd o PureThy.add_axioms (map (Thm.no_attributes o apfst Binding.name) x);
-fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy;
+ val thy = Sign.parent_path thy;
+ in
+ (lub_take_thm, thy)
+ end;
fun add_axioms
(dom_eqns : (binding * (typ * typ)) list)
@@ -120,37 +110,18 @@
val (iso_infos, thy) =
fold_map axiomatize_isomorphism dom_eqns thy;
- fun add_one (dnam, axs) =
- Sign.add_path dnam
- #> add_axioms_infer axs
- #> Sign.parent_path;
-
- (* define take function *)
+ (* define take functions *)
val (take_info, thy) =
Domain_Take_Proofs.define_take_functions
(map fst dom_eqns ~~ iso_infos) thy;
(* declare lub_take axioms *)
- local
- fun ax_lub_take (dbind, take_const) =
- let
- val dnam = Long_Name.base_name (Binding.name_of dbind);
- val lub = %%: @{const_name lub};
- val image = %%: @{const_name image};
- val UNIV = @{term "UNIV :: nat set"};
- val lhs = lub $ (image $ take_const $ UNIV);
- val ax = mk_trp (lhs === ID);
- in
- add_one (dnam, [("lub_take", ax)])
- end
- val dbinds = map fst dom_eqns;
- val take_consts = #take_consts take_info;
- in
- val thy = fold ax_lub_take (dbinds ~~ take_consts) thy
- end;
+ val (lub_take_thms, thy) =
+ fold_map axiomatize_lub_take
+ (map fst dom_eqns ~~ #take_consts take_info) thy;
in
- thy (* TODO: also return iso_infos, take_info, lub_take_thms *)
+ (iso_infos, thy) (* TODO: also return take_info, lub_take_thms *)
end;
end; (* struct *)
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML Wed Mar 03 17:08:41 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Wed Mar 03 10:40:40 2010 -0800
@@ -35,8 +35,10 @@
struct
open HOLCF_Library;
+
infixr 6 ->>;
infix -->>;
+infix 9 `;
(************************** miscellaneous functions ***************************)
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Wed Mar 03 17:08:41 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Wed Mar 03 10:40:40 2010 -0800
@@ -184,13 +184,14 @@
fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons);
val repTs : typ list = map mk_eq_typ eqs';
val dom_eqns : (binding * (typ * typ)) list = dbinds ~~ (dts ~~ repTs);
- val thy = Domain_Axioms.add_axioms dom_eqns thy;
+ val (iso_infos, thy) =
+ Domain_Axioms.add_axioms dom_eqns thy;
val ((rewss, take_rews), theorems_thy) =
thy
- |> fold_map (fn (eq, (x,cs)) =>
- Domain_Theorems.theorems (eq, eqs) (Type x, cs))
- (eqs ~~ eqs')
+ |> fold_map (fn ((eq, (x,cs)), info) =>
+ Domain_Theorems.theorems (eq, eqs) (Type x, cs) info)
+ (eqs ~~ eqs' ~~ iso_infos)
||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
in
theorems_thy
@@ -264,9 +265,9 @@
map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
val ((rewss, take_rews), theorems_thy) =
thy
- |> fold_map (fn (eq, (x,cs)) =>
- Domain_Theorems.theorems (eq, eqs) (Type x, cs))
- (eqs ~~ eqs')
+ |> fold_map (fn ((eq, (x,cs)), info) =>
+ Domain_Theorems.theorems (eq, eqs) (Type x, cs) info)
+ (eqs ~~ eqs' ~~ iso_infos)
||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
in
theorems_thy
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Mar 03 17:08:41 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Mar 03 10:40:40 2010 -0800
@@ -106,17 +106,6 @@
fun mk_deflation t =
Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t;
-fun mk_lub t =
- let
- val T = Term.range_type (Term.fastype_of t);
- val lub_const = Const (@{const_name lub}, (T --> boolT) --> T);
- val UNIV_const = @{term "UNIV :: nat set"};
- val image_type = (natT --> T) --> (natT --> boolT) --> T --> boolT;
- val image_const = Const (@{const_name image}, image_type);
- in
- lub_const $ (image_const $ t $ UNIV_const)
- end;
-
(* splits a cterm into the right and lefthand sides of equality *)
fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
@@ -638,8 +627,8 @@
(* prove lub of take equals ID *)
fun prove_lub_take (((bind, take_const), map_ID_thm), (lhsT, rhsT)) thy =
let
- val i = Free ("i", natT);
- val goal = mk_eqs (mk_lub (lambda i (take_const $ i)), mk_ID lhsT);
+ val n = Free ("n", natT);
+ val goal = mk_eqs (mk_lub (lambda n (take_const $ n)), mk_ID lhsT);
val tac =
EVERY
[rtac @{thm trans} 1, rtac map_ID_thm 2,
--- a/src/HOLCF/Tools/Domain/domain_library.ML Wed Mar 03 17:08:41 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_library.ML Wed Mar 03 10:40:40 2010 -0800
@@ -38,14 +38,10 @@
val string_of_typ : theory -> typ -> string;
(* Creating HOLCF types *)
- val ->> : typ * typ -> typ;
val mk_ssumT : typ * typ -> typ;
val mk_sprodT : typ * typ -> typ;
val mk_uT : typ -> typ;
val oneT : typ;
- val mk_maybeT : typ -> typ;
- val mk_ctupleT : typ list -> typ;
- val mk_TFree : string -> typ;
val pcpoS : sort;
(* Creating HOLCF terms *)
@@ -53,21 +49,12 @@
val %%: : string -> term;
val ` : term * term -> term;
val `% : term * string -> term;
- val /\ : string -> term -> term;
val UU : term;
val ID : term;
- val oo : term * term -> term;
- val mk_ctuple : term list -> term;
- val mk_fix : term -> term;
- val mk_iterate : term * term * term -> term;
- val mk_fail : term;
- val mk_return : term -> term;
val list_ccomb : term * term list -> term;
val con_app2 : string -> ('a -> term) -> 'a list -> term;
val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a
val proj : term -> 'a list -> int -> term;
- val mk_ctuple_pat : term list -> term;
- val mk_branch : term -> term;
(* Creating propositions *)
val mk_conj : term * term -> term;
@@ -78,7 +65,6 @@
val mk_ex : string * term -> term;
val mk_constrainall : string * typ * term -> term;
val === : term * term -> term;
- val strict : term -> term;
val defined : term -> term;
val mk_adm : term -> term;
val lift : ('a -> term) -> 'a list * term -> term;
@@ -88,7 +74,6 @@
val mk_trp : term -> term; (* HOLogic.mk_Trueprop *)
val == : term * term -> term;
val ===> : term * term -> term;
- val ==> : term * term -> term;
val mk_All : string * term -> term;
(* Domain specifications *)
@@ -106,20 +91,9 @@
val nonlazy : arg list -> string list;
val nonlazy_rec : arg list -> string list;
val %# : arg -> term;
- val /\# : arg * term -> term;
val bound_arg : ''a list -> ''a -> term; (* ''a = arg or string *)
val idx_name : 'a list -> string -> int -> string;
- val app_rec_arg : (int -> term) -> arg -> term;
val con_app : string -> arg list -> term;
- val dtyp_of_eq : eq -> Datatype.dtyp;
-
-
- (* Name mangling *)
- val strip_esc : string -> string;
- val extern_name : string -> string;
- val dis_name : string -> string;
- val mat_name : string -> string;
- val pat_name : string -> string;
end;
structure Domain_Library :> DOMAIN_LIBRARY =
@@ -155,26 +129,6 @@
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";
-
fun cpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort cpo});
fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo});
fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg;
@@ -210,36 +164,13 @@
fun nonlazy_rec args = map vname (filter is_nonlazy_rec args);
-(* ----- combinators for making dtyps ----- *)
-
-fun mk_uD T = Datatype_Aux.DtType(@{type_name "u"}, [T]);
-fun mk_sprodD (T, U) = Datatype_Aux.DtType(@{type_name sprod}, [T, U]);
-fun mk_ssumD (T, U) = Datatype_Aux.DtType(@{type_name ssum}, [T, U]);
-fun mk_liftD T = Datatype_Aux.DtType(@{type_name "lift"}, [T]);
-val unitD = Datatype_Aux.DtType(@{type_name "unit"}, []);
-val boolD = Datatype_Aux.DtType(@{type_name "bool"}, []);
-val oneD = mk_liftD unitD;
-val trD = mk_liftD boolD;
-fun big_sprodD ds = case ds of [] => oneD | _ => foldr1 mk_sprodD ds;
-fun big_ssumD ds = case ds of [] => unitD | _ => foldr1 mk_ssumD ds;
-
-fun dtyp_of_arg ((lazy, D), _) = if lazy then mk_uD D else D;
-fun dtyp_of_cons (_, args) = big_sprodD (map dtyp_of_arg args);
-fun dtyp_of_eq (_, cons) = big_ssumD (map dtyp_of_cons cons);
-
-
(* ----- support for type and mixfix expressions ----- *)
fun mk_uT T = Type(@{type_name "u"}, [T]);
-fun mk_cfunT (T, U) = Type(@{type_name cfun}, [T, U]);
fun mk_sprodT (T, U) = Type(@{type_name sprod}, [T, U]);
fun mk_ssumT (T, U) = Type(@{type_name ssum}, [T, U]);
val oneT = @{typ one};
-val op ->> = mk_cfunT;
-
-fun mk_TFree s = TFree ("'" ^ s, @{sort pcpo});
-
(* ----- support for term expressions ----- *)
fun %: s = Free(s,dummyT);
@@ -260,7 +191,6 @@
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);
@@ -275,42 +205,22 @@
fun mk_ssplit t = %%: @{const_name ssplit}`t;
fun mk_sscase (x, y) = %%: @{const_name sscase}`x`y;
fun mk_fup (t,u) = %%: @{const_name fup} ` t ` u;
-val ONE = @{term ONE};
-fun mk_iterate (n,f,z) = %%: @{const_name iterate} $ n ` f ` z;
-fun mk_fix t = %%: @{const_name fix}`t;
-fun mk_return t = %%: @{const_name Fixrec.return}`t;
-val mk_fail = %%: @{const_name Fixrec.fail};
-
-fun mk_branch t = %%: @{const_name Fixrec.branch} $ t;
val pcpoS = @{sort pcpo};
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 lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
-fun /\ v T = %%: @{const_name Abs_CFun} $ mk_lam(v,T);
-fun /\# (arg,T) = /\ (vname arg) T;
-infixr 9 oo; fun S oo T = %%: @{const_name cfcomp}`S`T;
val UU = %%: @{const_name UU};
-fun strict f = f`UU === UU;
fun defined t = t ~= UU;
fun cpair (t,u) = %%: @{const_name Pair} $ t $ u;
fun spair (t,u) = %%: @{const_name spair}`t`u;
-fun mk_ctuple [] = HOLogic.unit (* used in match_defs *)
- | mk_ctuple ts = foldr1 cpair 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) = %%: @{const_name cpair_pat} $ p1 $ p2;
-val mk_ctuple_pat = foldr1 cpair_pat;
fun lift_defined f = lift (fn x => defined (f x));
fun bound_arg vns v = Bound (length vns - find_index (fn v' => v' = v) vns - 1);
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Wed Mar 03 17:08:41 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Wed Mar 03 10:40:40 2010 -0800
@@ -116,17 +116,6 @@
fun mk_deflation t =
Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t;
-fun mk_lub t =
- let
- val T = Term.range_type (Term.fastype_of t);
- val lub_const = Const (@{const_name lub}, (T --> boolT) --> T);
- val UNIV_const = @{term "UNIV :: nat set"};
- val image_type = (natT --> T) --> (natT --> boolT) --> T --> boolT;
- val image_const = Const (@{const_name image}, image_type);
- in
- lub_const $ (image_const $ t $ UNIV_const)
- end;
-
(* splits a cterm into the right and lefthand sides of equality *)
fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
@@ -241,10 +230,10 @@
(mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns)));
val take_rhss =
let
- val i = Free ("i", HOLogic.natT);
- val rhs = mk_iterate (i, take_functional)
+ val n = Free ("n", HOLogic.natT);
+ val rhs = mk_iterate (n, take_functional);
in
- map (Term.lambda i o snd) (mk_projs dom_binds rhs)
+ map (lambda n o snd) (mk_projs dom_binds rhs)
end;
(* define take constants *)
@@ -295,12 +284,12 @@
fold_map prove_take_0 (take_consts ~~ dnames ~~ dom_eqns) thy;
(* prove take_Suc lemmas *)
- val i = Free ("i", natT);
- val take_is = map (fn t => t $ i) take_consts;
+ val n = Free ("n", natT);
+ val take_is = map (fn t => t $ n) take_consts;
fun prove_take_Suc
(((take_const, rep_abs), dname), (lhsT, rhsT)) thy =
let
- val lhs = take_const $ (@{term Suc} $ i);
+ val lhs = take_const $ (@{term Suc} $ n);
val body = map_of_typ thy (newTs ~~ take_is) rhsT;
val rhs = mk_cfcomp2 (rep_abs, body);
val goal = mk_eqs (lhs, rhs);
@@ -319,8 +308,8 @@
val deflation_abs_rep_thms = map deflation_abs_rep iso_infos;
val deflation_take_thm =
let
- val i = Free ("i", natT);
- fun mk_goal take_const = mk_deflation (take_const $ i);
+ val n = Free ("n", natT);
+ fun mk_goal take_const = mk_deflation (take_const $ n);
val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts));
val adm_rules =
@{thms adm_conj adm_subst [OF _ adm_deflation]
@@ -355,7 +344,7 @@
(* prove strictness of take functions *)
fun prove_take_strict (take_const, dname) thy =
let
- val goal = mk_trp (mk_strict (take_const $ Free ("i", natT)));
+ val goal = mk_trp (mk_strict (take_const $ Free ("n", natT)));
val tac = rtac @{thm deflation_strict} 1
THEN resolve_tac deflation_take_thms 1;
val take_strict_thm = Goal.prove_global thy [] [] goal (K tac);
@@ -369,7 +358,8 @@
fun prove_take_take ((chain_take, deflation_take), dname) thy =
let
val take_take_thm =
- @{thm deflation_chain_min} OF [chain_take, deflation_take];
+ Drule.export_without_context
+ (@{thm deflation_chain_min} OF [chain_take, deflation_take]);
in
add_qualified_thm "take_take" (dname, take_take_thm) thy
end;
@@ -385,10 +375,10 @@
val (finite_const, thy) =
Sign.declare_const ((finite_bind, finite_type), NoSyn) thy;
val x = Free ("x", lhsT);
- val i = Free ("i", natT);
+ val n = Free ("n", natT);
val finite_rhs =
lambda x (HOLogic.exists_const natT $
- (lambda i (mk_eq (mk_capply (take_const $ i, x), x))));
+ (lambda n (mk_eq (mk_capply (take_const $ n, x), x))));
val finite_eqn = Logic.mk_equals (finite_const, finite_rhs);
val (finite_def_thm, thy) =
thy
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Wed Mar 03 17:08:41 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Wed Mar 03 10:40:40 2010 -0800
@@ -12,6 +12,7 @@
val theorems:
Domain_Library.eq * Domain_Library.eq list
-> typ * (binding * (bool * binding option * typ) list * mixfix) list
+ -> Domain_Take_Proofs.iso_info
-> theory -> thm list * theory;
val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory;
@@ -28,30 +29,6 @@
fun message s = if !quiet_mode then () else writeln s;
fun trace s = if !trace_domain then tracing s else ();
-val adm_impl_admw = @{thm adm_impl_admw};
-val adm_all = @{thm adm_all};
-val adm_conj = @{thm adm_conj};
-val adm_subst = @{thm adm_subst};
-val ch2ch_fst = @{thm ch2ch_fst};
-val ch2ch_snd = @{thm ch2ch_snd};
-val ch2ch_Rep_CFunL = @{thm ch2ch_Rep_CFunL};
-val ch2ch_Rep_CFunR = @{thm ch2ch_Rep_CFunR};
-val chain_iterate = @{thm chain_iterate};
-val contlub_cfun_fun = @{thm contlub_cfun_fun};
-val contlub_fst = @{thm contlub_fst};
-val contlub_snd = @{thm contlub_snd};
-val contlubE = @{thm contlubE};
-val cont_const = @{thm cont_const};
-val cont_id = @{thm cont_id};
-val cont2cont_fst = @{thm cont2cont_fst};
-val cont2cont_snd = @{thm cont2cont_snd};
-val cont2cont_Rep_CFun = @{thm cont2cont_Rep_CFun};
-val fix_def2 = @{thm fix_def2};
-val lub_equal = @{thm lub_equal};
-val retraction_strict = @{thm retraction_strict};
-val wfix_ind = @{thm wfix_ind};
-val iso_intro = @{thm iso.intro};
-
open Domain_Library;
infixr 0 ===>;
infixr 0 ==>;
@@ -102,6 +79,7 @@
fun theorems
(((dname, _), cons) : eq, eqs : eq list)
(dom_eqn : typ * (binding * (bool * binding option * typ) list * mixfix) list)
+ (iso_info : Domain_Take_Proofs.iso_info)
(thy : theory) =
let
@@ -111,11 +89,15 @@
(* ----- getting the axioms and definitions --------------------------------- *)
+val ax_abs_iso = #abs_inverse iso_info;
+val ax_rep_iso = #rep_inverse iso_info;
+
+val abs_const = #abs_const iso_info;
+val rep_const = #rep_const iso_info;
+
local
fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
in
- val ax_abs_iso = ga "abs_iso" dname;
- val ax_rep_iso = ga "rep_iso" dname;
val ax_take_0 = ga "take_0" dname;
val ax_take_Suc = ga "take_Suc" dname;
val ax_take_strict = ga "take_strict" dname;
@@ -123,32 +105,6 @@
(* ----- define constructors ------------------------------------------------ *)
-val lhsT = fst dom_eqn;
-
-val rhsT =
- let
- fun mk_arg_typ (lazy, sel, T) = if lazy then mk_uT T else T;
- fun mk_con_typ (bind, args, mx) =
- if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args);
- fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons);
- in
- mk_eq_typ dom_eqn
- end;
-
-val rep_const = Const(dname^"_rep", lhsT ->> rhsT);
-
-val abs_const = Const(dname^"_abs", rhsT ->> lhsT);
-
-val iso_info : Domain_Take_Proofs.iso_info =
- {
- absT = lhsT,
- repT = rhsT,
- abs_const = abs_const,
- rep_const = rep_const,
- abs_inverse = ax_abs_iso,
- rep_inverse = ax_rep_iso
- };
-
val (result, thy) =
Domain_Constructors.add_domain_constructors
(Long_Name.base_name dname) (snd dom_eqn) iso_info thy;
@@ -167,6 +123,7 @@
val pg = pg' thy;
+val retraction_strict = @{thm retraction_strict};
val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
val iso_rews = map Drule.export_without_context [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
@@ -180,12 +137,21 @@
fun get_deflation_take dn = PureThy.get_thm thy (dn ^ ".deflation_take");
val axs_deflation_take = map get_deflation_take dnames;
+ fun copy_of_dtyp tab r dt =
+ if Datatype_Aux.is_rec_type dt then copy tab r dt else ID
+ and copy tab r (Datatype_Aux.DtRec i) = r i
+ | copy tab r (Datatype_Aux.DtTFree a) = ID
+ | copy tab r (Datatype_Aux.DtType (c, ds)) =
+ case Symtab.lookup tab c of
+ SOME f => list_ccomb (%%:f, map (copy_of_dtyp tab r) ds)
+ | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID);
+
fun one_take_app (con, args) =
let
fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
fun one_rhs arg =
if Datatype_Aux.is_rec_type (dtyp_of arg)
- then Domain_Axioms.copy_of_dtyp map_tab
+ then copy_of_dtyp map_tab
mk_take (dtyp_of arg) ` (%# arg)
else (%# arg);
val lhs = (dc_take dname $ (%%:"Suc" $ %:"n"))`(con_app con args);
@@ -199,7 +165,7 @@
[simp_tac (HOL_basic_ss addsimps rules) 1,
asm_simp_tac (HOL_basic_ss addsimps rules2) 1];
in pg con_appls goal (K tacs) end;
- val take_apps = map (Drule.export_without_context o one_take_app) cons;
+ val take_apps = map one_take_app cons;
in
val take_rews = ax_take_0 :: ax_take_strict :: take_apps;
end;
@@ -438,13 +404,15 @@
val take_lemmas =
let
fun take_lemma (ax_chain_take, ax_lub_take) =
- @{thm lub_ID_take_lemma} OF [ax_chain_take, ax_lub_take];
+ Drule.export_without_context
+ (@{thm lub_ID_take_lemma} OF [ax_chain_take, ax_lub_take]);
in map take_lemma (axs_chain_take ~~ axs_lub_take) end;
val axs_reach =
let
fun reach (ax_chain_take, ax_lub_take) =
- @{thm lub_ID_reach} OF [ax_chain_take, ax_lub_take];
+ Drule.export_without_context
+ (@{thm lub_ID_reach} OF [ax_chain_take, ax_lub_take]);
in map reach (axs_chain_take ~~ axs_lub_take) end;
(* ----- theorems concerning finiteness and induction ----------------------- *)
@@ -555,8 +523,8 @@
fun concf n dn = %:(P_name n) $ %:(x_name n);
in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end;
val cont_rules =
- [cont_id, cont_const, cont2cont_Rep_CFun,
- cont2cont_fst, cont2cont_snd];
+ @{thms cont_id cont_const cont2cont_Rep_CFun
+ cont2cont_fst cont2cont_snd};
val subgoal =
let fun p n dn = %:(P_name n) $ (dc_take dn $ Bound 0 `%(x_name n));
in mk_trp (mk_all ("n", foldr1 mk_conj (mapn p 1 dnames))) end;
--- a/src/HOLCF/Tools/holcf_library.ML Wed Mar 03 17:08:41 2010 +0100
+++ b/src/HOLCF/Tools/holcf_library.ML Wed Mar 03 10:40:40 2010 -0800
@@ -9,6 +9,7 @@
infixr 6 ->>;
infix -->>;
+infix 9 `;
(*** Operations from Isabelle/HOL ***)
@@ -47,6 +48,17 @@
fun mk_chain t =
Const (@{const_name chain}, Term.fastype_of t --> boolT) $ t;
+fun mk_lub t =
+ let
+ val T = Term.range_type (Term.fastype_of t);
+ val lub_const = Const (@{const_name lub}, (T --> boolT) --> T);
+ val UNIV_const = @{term "UNIV :: nat set"};
+ val image_type = (natT --> T) --> (natT --> boolT) --> T --> boolT;
+ val image_const = Const (@{const_name image}, image_type);
+ in
+ lub_const $ (image_const $ t $ UNIV_const)
+ end;
+
(*** Continuous function space ***)
@@ -88,7 +100,7 @@
| _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]);
in capply_const (S, T) $ t $ u end;
-infix 9 ` ; val (op `) = mk_capply;
+val (op `) = mk_capply;
val list_ccomb : term * term list -> term = Library.foldl mk_capply;
--- a/src/HOLCF/ex/Stream.thy Wed Mar 03 17:08:41 2010 +0100
+++ b/src/HOLCF/ex/Stream.thy Wed Mar 03 10:40:40 2010 -0800
@@ -290,12 +290,12 @@
lemma stream_finite_lemma1: "stream_finite xs ==> stream_finite (x && xs)"
apply (simp add: stream.finite_def,auto)
-apply (rule_tac x="Suc i" in exI)
+apply (rule_tac x="Suc n" in exI)
by (simp add: stream_take_lemma4)
lemma stream_finite_lemma2: "[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs"
apply (simp add: stream.finite_def, auto)
-apply (rule_tac x="i" in exI)
+apply (rule_tac x="n" in exI)
by (erule stream_take_lemma3,simp)
lemma stream_finite_rt_eq: "stream_finite (rt$s) = stream_finite s"