# HG changeset patch # User huffman # Date 1267676441 28800 # Node ID 20995afa8fa16be3d6f3261f2201d6320543fb0d # Parent f5ec817df77f07c2c8430f7a3e001987f513c26f# Parent 1e05ea0a5cd7a2f0a3433cea517c4159ca54bba0 merged diff -r 1e05ea0a5cd7 -r 20995afa8fa1 src/HOLCF/Representable.thy --- a/src/HOLCF/Representable.thy Wed Mar 03 22:50:35 2010 +0100 +++ b/src/HOLCF/Representable.thy Wed Mar 03 20:20:41 2010 -0800 @@ -189,21 +189,21 @@ lemma deflation_chain_min: assumes chain: "chain d" - assumes defl: "\i. deflation (d i)" - shows "d i\(d j\x) = d (min i j)\x" + assumes defl: "\n. deflation (d n)" + shows "d m\(d n\x) = d (min m n)\x" proof (rule linorder_le_cases) - assume "i \ j" - with chain have "d i \ d j" by (rule chain_mono) - then have "d i\(d j\x) = d i\x" + assume "m \ n" + with chain have "d m \ d n" by (rule chain_mono) + then have "d m\(d n\x) = d m\x" by (rule deflation_below_comp1 [OF defl defl]) - moreover from `i \ j` have "min i j = i" by simp + moreover from `m \ n` have "min m n = m" by simp ultimately show ?thesis by simp next - assume "j \ i" - with chain have "d j \ d i" by (rule chain_mono) - then have "d i\(d j\x) = d j\x" + assume "n \ m" + with chain have "d n \ d m" by (rule chain_mono) + then have "d m\(d n\x) = d n\x" by (rule deflation_below_comp2 [OF defl defl]) - moreover from `j \ i` have "min i j = j" by simp + moreover from `n \ m` have "min m n = n" by simp ultimately show ?thesis by simp qed diff -r 1e05ea0a5cd7 -r 20995afa8fa1 src/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOLCF/Tools/Domain/domain_axioms.ML Wed Mar 03 22:50:35 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Wed Mar 03 20:20:41 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 *) diff -r 1e05ea0a5cd7 -r 20995afa8fa1 src/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOLCF/Tools/Domain/domain_constructors.ML Wed Mar 03 22:50:35 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Wed Mar 03 20:20:41 2010 -0800 @@ -35,8 +35,10 @@ struct open HOLCF_Library; + infixr 6 ->>; infix -->>; +infix 9 `; (************************** miscellaneous functions ***************************) diff -r 1e05ea0a5cd7 -r 20995afa8fa1 src/HOLCF/Tools/Domain/domain_extender.ML --- a/src/HOLCF/Tools/Domain/domain_extender.ML Wed Mar 03 22:50:35 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML Wed Mar 03 20:20:41 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 diff -r 1e05ea0a5cd7 -r 20995afa8fa1 src/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Mar 03 22:50:35 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Mar 03 20:20:41 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, diff -r 1e05ea0a5cd7 -r 20995afa8fa1 src/HOLCF/Tools/Domain/domain_library.ML --- a/src/HOLCF/Tools/Domain/domain_library.ML Wed Mar 03 22:50:35 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_library.ML Wed Mar 03 20:20:41 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); diff -r 1e05ea0a5cd7 -r 20995afa8fa1 src/HOLCF/Tools/Domain/domain_take_proofs.ML --- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Wed Mar 03 22:50:35 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Wed Mar 03 20:20:41 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 diff -r 1e05ea0a5cd7 -r 20995afa8fa1 src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Wed Mar 03 22:50:35 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Wed Mar 03 20:20:41 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; diff -r 1e05ea0a5cd7 -r 20995afa8fa1 src/HOLCF/Tools/holcf_library.ML --- a/src/HOLCF/Tools/holcf_library.ML Wed Mar 03 22:50:35 2010 +0100 +++ b/src/HOLCF/Tools/holcf_library.ML Wed Mar 03 20:20:41 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; diff -r 1e05ea0a5cd7 -r 20995afa8fa1 src/HOLCF/ex/Stream.thy --- a/src/HOLCF/ex/Stream.thy Wed Mar 03 22:50:35 2010 +0100 +++ b/src/HOLCF/ex/Stream.thy Wed Mar 03 20:20:41 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"