# HG changeset patch # User huffman # Date 1258155080 28800 # Node ID 3317128796660c3573968b9d28325dc211ddc079 # Parent 2a2014cbb2a6aa32599562fe51f0a16e47a2c50a automate definition of representable domains from algebraic deflations diff -r 2a2014cbb2a6 -r 331712879666 src/HOLCF/Representable.thy --- a/src/HOLCF/Representable.thy Fri Nov 13 15:29:48 2009 -0800 +++ b/src/HOLCF/Representable.thy Fri Nov 13 15:31:20 2009 -0800 @@ -6,6 +6,7 @@ theory Representable imports Algebraic Universal Ssum Sprod One ConvexPD +uses ("Tools/repdef.ML") begin subsection {* Class of representable types *} @@ -174,16 +175,21 @@ setup {* Sign.add_const_constraint (@{const_name prj}, SOME @{typ "udom \ 'a::pcpo"}) *} +definition + repdef_approx :: + "('a::pcpo \ udom) \ (udom \ 'a) \ udom alg_defl \ nat \ 'a \ 'a" +where + "repdef_approx Rep Abs t = (\i. \ x. Abs (cast\(approx i\t)\(Rep x)))" + lemma typedef_rep_class: fixes Rep :: "'a::pcpo \ udom" fixes Abs :: "udom \ 'a::pcpo" fixes t :: TypeRep assumes type: "type_definition Rep Abs {x. x ::: t}" assumes below: "op \ \ \x y. Rep x \ Rep y" - assumes emb: "emb = (\ x. Rep x)" - assumes prj: "prj = (\ x. Abs (cast\t\x))" - assumes approx: - "(approx :: nat \ 'a \ 'a) = (\i. prj oo cast\(approx i\t) oo emb)" + assumes emb: "emb \ (\ x. Rep x)" + assumes prj: "prj \ (\ x. Abs (cast\t\x))" + assumes approx: "(approx :: nat \ 'a \ 'a) \ repdef_approx Rep Abs t" shows "OFCLASS('a, rep_class)" proof have adm: "adm (\x. x \ {x. x ::: t})" @@ -199,6 +205,19 @@ apply (rule typedef_cont_Abs [OF type below adm]) apply simp_all done + have cast_cast_approx: + "\i x. cast\t\(cast\(approx i\t)\x) = cast\(approx i\t)\x" + apply (rule cast_fixed) + apply (rule subdeflationD) + apply (rule approx.below) + apply (rule cast_in_deflation) + done + have approx': + "approx = (\i. \(x::'a). prj\(cast\(approx i\t)\(emb\x)))" + unfolding approx repdef_approx_def + apply (subst cast_cast_approx [symmetric]) + apply (simp add: prj_beta [symmetric] emb_beta [symmetric]) + done have emb_in_deflation: "\x::'a. emb\x ::: t" using type_definition.Rep [OF type] by (simp add: emb_beta) @@ -216,22 +235,15 @@ apply (simp add: emb_prj cast.below) done show "chain (approx :: nat \ 'a \ 'a)" - unfolding approx by simp + unfolding approx' by simp show "\x::'a. (\i. approx i\x) = x" - unfolding approx + unfolding approx' apply (simp add: lub_distribs) apply (subst cast_fixed [OF emb_in_deflation]) apply (rule prj_emb) done - have cast_cast_approx: - "\i x. cast\t\(cast\(approx i\t)\x) = cast\(approx i\t)\x" - apply (rule cast_fixed) - apply (rule subdeflationD) - apply (rule approx.below) - apply (rule cast_in_deflation) - done show "\(i::nat) (x::'a). approx i\(approx i\x) = approx i\x" - unfolding approx + unfolding approx' apply simp apply (simp add: emb_prj) apply (simp add: cast_cast_approx) @@ -239,7 +251,7 @@ show "\i::nat. finite {x::'a. approx i\x = x}" apply (rule_tac B="(\x. prj\x) ` {x. cast\(approx i\t)\x = x}" in finite_subset) - apply (clarsimp simp add: approx) + apply (clarsimp simp add: approx') apply (drule_tac f="\x. emb\x" in arg_cong) apply (rule image_eqI) apply (rule prj_emb [symmetric]) @@ -269,8 +281,8 @@ fixes t :: TypeRep assumes type: "type_definition Rep Abs {x. x ::: t}" assumes below: "op \ \ \x y. Rep x \ Rep y" - assumes emb: "emb = (\ x. Rep x)" - assumes prj: "prj = (\ x. Abs (cast\t\x))" + assumes emb: "emb \ (\ x. Rep x)" + assumes prj: "prj \ (\ x. Abs (cast\t\x))" shows "REP('a) = t" proof - have adm: "adm (\x. x \ {x. x ::: t})" @@ -303,6 +315,11 @@ done qed +lemma adm_mem_Collect_in_deflation: "adm (\x. x \ {x. x ::: A})" +unfolding mem_Collect_eq by (rule adm_in_deflation) + +use "Tools/repdef.ML" + subsection {* Instances of class @{text rep} *} diff -r 2a2014cbb2a6 -r 331712879666 src/HOLCF/Tools/repdef.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/repdef.ML Fri Nov 13 15:31:20 2009 -0800 @@ -0,0 +1,181 @@ +(* Title: HOLCF/Tools/repdef.ML + Author: Brian Huffman + +Defining representable domains using algebraic deflations. +*) + +signature REPDEF = +sig + type rep_info = + { emb_def: thm, prj_def: thm, approx_def: thm, REP: thm } + + val add_repdef: bool -> binding option -> binding * string list * mixfix -> + term -> (binding * binding) option -> theory -> + (Typedef.info * Pcpodef.cpo_info * Pcpodef.pcpo_info * rep_info) * theory + + val repdef_cmd: (bool * binding) * (binding * string list * mixfix) * string + * (binding * binding) option -> theory -> theory +end; + +structure Repdef :> REPDEF = +struct + +(** type definitions **) + +type rep_info = + { emb_def: thm, prj_def: thm, approx_def: thm, REP: thm }; + +(* building terms *) + +fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT); +fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P); + +fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT); + +val natT = @{typ nat}; +val udomT = @{typ udom}; +fun alg_deflT T = Type (@{type_name alg_defl}, [T]); +fun cfunT (T, U) = Type (@{type_name "->"}, [T, U]); +fun emb_const T = Const (@{const_name emb}, cfunT (T, udomT)); +fun prj_const T = Const (@{const_name prj}, cfunT (udomT, T)); +fun approx_const T = Const (@{const_name approx}, natT --> cfunT (T, T)); + +fun LAM_const (T, U) = Const (@{const_name Abs_CFun}, (T --> U) --> cfunT (T, U)); +fun APP_const (T, U) = Const (@{const_name Rep_CFun}, cfunT (T, U) --> (T --> U)); +fun cast_const T = Const (@{const_name cast}, cfunT (alg_deflT T, cfunT (T, T))); +fun mk_cast (t, x) = + APP_const (udomT, udomT) + $ (APP_const (alg_deflT udomT, cfunT (udomT, udomT)) $ cast_const udomT $ t) + $ x; + +(* manipulating theorems *) + +(* proving class instances *) + +fun declare_type_name a = + Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS))); + +fun gen_add_repdef + (prep_term: Proof.context -> 'a -> term) + (def: bool) + (name: binding) + (typ as (t, vs, mx) : binding * string list * mixfix) + (raw_defl: 'a) + (opt_morphs: (binding * binding) option) + (thy: theory) + : (Typedef.info * Pcpodef.cpo_info * Pcpodef.pcpo_info * rep_info) * theory = + let + val _ = Theory.requires thy "Representable" "repdefs"; + val ctxt = ProofContext.init thy; + + (*rhs*) + val defl = prep_term (ctxt |> fold declare_type_name vs) raw_defl; + val deflT = Term.fastype_of defl; + val _ = if deflT = @{typ "udom alg_defl"} then () + else error ("Not type udom alg_defl: " ^ quote (Syntax.string_of_typ ctxt deflT)); + val rhs_tfrees = Term.add_tfrees defl []; + + (*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 = Binding.map_name (Syntax.type_name mx) t; + val full_tname = Sign.full_name thy tname; + val newT = Type (full_tname, map TFree lhs_tfrees); + + (*morphisms*) + val morphs = opt_morphs + |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name); + + (*set*) + val in_defl = @{term "in_deflation :: udom => udom alg_defl => bool"}; + val set = HOLogic.Collect_const udomT $ Abs ("x", udomT, in_defl $ Bound 0 $ defl); + + (*pcpodef*) + val tac1 = rtac @{thm CollectI} 1 THEN rtac @{thm bottom_in_deflation} 1; + val tac2 = rtac @{thm adm_mem_Collect_in_deflation} 1; + val ((info, cpo_info, pcpo_info), thy2) = thy + |> Pcpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2); + + (*definitions*) + val Rep_const = Const (#Rep_name info, newT --> udomT); + val Abs_const = Const (#Abs_name info, udomT --> newT); + val emb_eqn = Logic.mk_equals (emb_const newT, LAM_const (newT, udomT) $ Rep_const); + val prj_eqn = Logic.mk_equals (prj_const newT, LAM_const (udomT, newT) $ + Abs ("x", udomT, Abs_const $ mk_cast (defl, Bound 0))); + val repdef_approx_const = + Const (@{const_name repdef_approx}, (newT --> udomT) --> (udomT --> newT) + --> alg_deflT udomT --> natT --> cfunT (newT, newT)); + val approx_eqn = Logic.mk_equals (approx_const newT, + repdef_approx_const $ Rep_const $ Abs_const $ defl); + + (*instantiate class rep*) + val name_def = Binding.suffix_name "_def" name; + val ([emb_ldef, prj_ldef, approx_ldef], lthy3) = thy2 + |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort rep}) + |> fold_map Specification.definition + [ (NONE, ((Binding.prefix_name "emb_" name_def, []), emb_eqn)) + , (NONE, ((Binding.prefix_name "prj_" name_def, []), prj_eqn)) + , (NONE, ((Binding.prefix_name "approx_" name_def, []), approx_eqn)) ] + |>> map (snd o snd); + val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy3); + val [emb_def, prj_def, approx_def] = + ProofContext.export lthy3 ctxt_thy [emb_ldef, prj_ldef, approx_ldef]; + val typedef_thms = + [#type_definition info, #below_def cpo_info, emb_def, prj_def, approx_def]; + val thy4 = lthy3 + |> Class.prove_instantiation_instance + (K (Tactic.rtac (@{thm typedef_rep_class} OF typedef_thms) 1)) + |> LocalTheory.exit_global; + + (*other theorems*) + val typedef_thms' = map (Thm.transfer thy4) + [#type_definition info, #below_def cpo_info, emb_def, prj_def]; + val ([REP_thm], thy5) = thy4 + |> Sign.add_path (Binding.name_of name) + |> PureThy.add_thms + [((Binding.prefix_name "REP_" name, + Drule.standard (@{thm typedef_REP} OF typedef_thms')), [])] + ||> Sign.parent_path; + + val rep_info = + { emb_def = emb_def, prj_def = prj_def, approx_def = approx_def, REP = REP_thm }; + in + ((info, cpo_info, pcpo_info, rep_info), thy5) + end + handle ERROR msg => + cat_error msg ("The error(s) above occurred in repdef " ^ quote (Binding.str_of name)); + +fun add_repdef def opt_name typ defl opt_morphs thy = + let + val name = the_default (#1 typ) opt_name; + in + gen_add_repdef Syntax.check_term def name typ defl opt_morphs thy + end; + +fun repdef_cmd ((def, name), typ, A, morphs) = + snd o gen_add_repdef Syntax.read_term def name typ A morphs; + +(** outer syntax **) + +local structure P = OuterParse and K = OuterKeyword in + +val repdef_decl = + Scan.optional (P.$$$ "(" |-- + ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s))) + --| P.$$$ ")") (true, NONE) -- + (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- + Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)); + +fun mk_repdef ((((((def, opt_name), (vs, t)), mx), A), morphs)) = + repdef_cmd + ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name), (t, vs, mx), A, morphs); + +val _ = + OuterSyntax.command "repdef" "HOLCF definition of representable domains" K.thy_goal + (repdef_decl >> + (Toplevel.print oo (Toplevel.theory o mk_repdef))); + +end; + +end; diff -r 2a2014cbb2a6 -r 331712879666 src/HOLCF/ex/Domain_Proofs.thy --- a/src/HOLCF/ex/Domain_Proofs.thy Fri Nov 13 15:29:48 2009 -0800 +++ b/src/HOLCF/ex/Domain_Proofs.thy Fri Nov 13 15:31:20 2009 -0800 @@ -94,13 +94,13 @@ begin definition emb_foo :: "'a foo \ udom" -where "emb_foo = (\ x. Rep_foo x)" +where "emb_foo \ (\ x. Rep_foo x)" definition prj_foo :: "udom \ 'a foo" -where "prj_foo = (\ y. Abs_foo (cast\(foo_typ\REP('a))\y))" +where "prj_foo \ (\ y. Abs_foo (cast\(foo_typ\REP('a))\y))" definition approx_foo :: "nat \ 'a foo \ 'a foo" -where "approx_foo = (\i. prj oo cast\(approx i\(foo_typ\REP('a))) oo emb)" +where "approx_foo \ repdef_approx Rep_foo Abs_foo (foo_typ\REP('a))" instance apply (rule typedef_rep_class) @@ -117,13 +117,13 @@ begin definition emb_bar :: "'a bar \ udom" -where "emb_bar = (\ x. Rep_bar x)" +where "emb_bar \ (\ x. Rep_bar x)" definition prj_bar :: "udom \ 'a bar" -where "prj_bar = (\ y. Abs_bar (cast\(bar_typ\REP('a))\y))" +where "prj_bar \ (\ y. Abs_bar (cast\(bar_typ\REP('a))\y))" definition approx_bar :: "nat \ 'a bar \ 'a bar" -where "approx_bar = (\i. prj oo cast\(approx i\(bar_typ\REP('a))) oo emb)" +where "approx_bar \ repdef_approx Rep_bar Abs_bar (bar_typ\REP('a))" instance apply (rule typedef_rep_class) @@ -140,13 +140,13 @@ begin definition emb_baz :: "'a baz \ udom" -where "emb_baz = (\ x. Rep_baz x)" +where "emb_baz \ (\ x. Rep_baz x)" definition prj_baz :: "udom \ 'a baz" -where "prj_baz = (\ y. Abs_baz (cast\(baz_typ\REP('a))\y))" +where "prj_baz \ (\ y. Abs_baz (cast\(baz_typ\REP('a))\y))" definition approx_baz :: "nat \ 'a baz \ 'a baz" -where "approx_baz = (\i. prj oo cast\(approx i\(baz_typ\REP('a))) oo emb)" +where "approx_baz \ repdef_approx Rep_baz Abs_baz (baz_typ\REP('a))" instance apply (rule typedef_rep_class)