# HG changeset patch # User huffman # Date 1258690196 28800 # Node ID f5db63bd7aeed2fe9ff8d0aa8147d1532c54b08a # Parent 48ce3a1063f24150aa5f759a7a6c0a4c2d2a1222# Parent ccef2e6d8c218216b3e0d2e3c33bd89749a010a9 merged diff -r ccef2e6d8c21 -r f5db63bd7aee src/HOLCF/Domain.thy --- a/src/HOLCF/Domain.thy Fri Nov 20 00:54:20 2009 +0100 +++ b/src/HOLCF/Domain.thy Thu Nov 19 20:09:56 2009 -0800 @@ -5,7 +5,7 @@ header {* Domain package *} theory Domain -imports Ssum Sprod Up One Tr Fixrec +imports Ssum Sprod Up One Tr Fixrec Representable uses ("Tools/cont_consts.ML") ("Tools/cont_proc.ML") diff -r ccef2e6d8c21 -r f5db63bd7aee src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Fri Nov 20 00:54:20 2009 +0100 +++ b/src/HOLCF/IsaMakefile Thu Nov 19 20:09:56 2009 -0800 @@ -52,6 +52,7 @@ Pcpo.thy \ Porder.thy \ Product_Cpo.thy \ + Representable.thy \ Sprod.thy \ Ssum.thy \ Sum_Cpo.thy \ @@ -64,11 +65,13 @@ Tools/cont_proc.ML \ Tools/Domain/domain_extender.ML \ Tools/Domain/domain_axioms.ML \ + Tools/Domain/domain_isomorphism.ML \ Tools/Domain/domain_library.ML \ Tools/Domain/domain_syntax.ML \ Tools/Domain/domain_theorems.ML \ Tools/fixrec.ML \ Tools/pcpodef.ML \ + Tools/repdef.ML \ holcf_logic.ML \ document/root.tex @$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF diff -r ccef2e6d8c21 -r f5db63bd7aee src/HOLCF/Representable.thy --- a/src/HOLCF/Representable.thy Fri Nov 20 00:54:20 2009 +0100 +++ b/src/HOLCF/Representable.thy Thu Nov 19 20:09:56 2009 -0800 @@ -5,8 +5,10 @@ header {* Representable Types *} theory Representable -imports Algebraic Universal Ssum Sprod One ConvexPD -uses ("Tools/repdef.ML") +imports Algebraic Universal Ssum Sprod One ConvexPD Fixrec +uses + ("Tools/repdef.ML") + ("Tools/Domain/domain_isomorphism.ML") begin subsection {* Class of representable types *} @@ -159,6 +161,25 @@ apply simp done +text {* Isomorphism lemmas used internally by the domain package: *} + +lemma domain_abs_iso: + fixes abs and rep + assumes REP: "REP('b) = REP('a)" + assumes abs_def: "abs \ (coerce :: 'a \ 'b)" + assumes rep_def: "rep \ (coerce :: 'b \ 'a)" + shows "rep\(abs\x) = x" +unfolding abs_def rep_def by (simp add: REP) + +lemma domain_rep_iso: + fixes abs and rep + assumes REP: "REP('b) = REP('a)" + assumes abs_def: "abs \ (coerce :: 'a \ 'b)" + assumes rep_def: "rep \ (coerce :: 'b \ 'a)" + shows "abs\(rep\x) = x" +unfolding abs_def rep_def by (simp add: REP [symmetric]) + + subsection {* Proving a subtype is representable *} text {* @@ -671,16 +692,14 @@ Abs_fin_defl (udom_emb oo f\(Rep_fin_defl a)\(Rep_fin_defl b) oo udom_prj))))" -definition "one_typ = REP(one)" -definition "tr_typ = REP(tr)" -definition "cfun_typ = TypeRep_fun2 cfun_map" -definition "ssum_typ = TypeRep_fun2 ssum_map" -definition "sprod_typ = TypeRep_fun2 sprod_map" -definition "cprod_typ = TypeRep_fun2 cprod_map" -definition "u_typ = TypeRep_fun1 u_map" -definition "upper_typ = TypeRep_fun1 upper_map" -definition "lower_typ = TypeRep_fun1 lower_map" -definition "convex_typ = TypeRep_fun1 convex_map" +definition "cfun_defl = TypeRep_fun2 cfun_map" +definition "ssum_defl = TypeRep_fun2 ssum_map" +definition "sprod_defl = TypeRep_fun2 sprod_map" +definition "cprod_defl = TypeRep_fun2 cprod_map" +definition "u_defl = TypeRep_fun1 u_map" +definition "upper_defl = TypeRep_fun1 upper_map" +definition "lower_defl = TypeRep_fun1 lower_map" +definition "convex_defl = TypeRep_fun1 convex_map" lemma Rep_fin_defl_mono: "a \ b \ Rep_fin_defl a \ Rep_fin_defl b" unfolding below_fin_defl_def . @@ -729,138 +748,130 @@ Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1]) qed -lemma cast_cfun_typ: - "cast\(cfun_typ\A\B) = udom_emb oo cfun_map\(cast\A)\(cast\B) oo udom_prj" -unfolding cfun_typ_def +lemma cast_cfun_defl: + "cast\(cfun_defl\A\B) = udom_emb oo cfun_map\(cast\A)\(cast\B) oo udom_prj" +unfolding cfun_defl_def apply (rule cast_TypeRep_fun2) apply (erule (1) finite_deflation_cfun_map) done -lemma cast_ssum_typ: - "cast\(ssum_typ\A\B) = udom_emb oo ssum_map\(cast\A)\(cast\B) oo udom_prj" -unfolding ssum_typ_def +lemma cast_ssum_defl: + "cast\(ssum_defl\A\B) = udom_emb oo ssum_map\(cast\A)\(cast\B) oo udom_prj" +unfolding ssum_defl_def apply (rule cast_TypeRep_fun2) apply (erule (1) finite_deflation_ssum_map) done -lemma cast_sprod_typ: - "cast\(sprod_typ\A\B) = udom_emb oo sprod_map\(cast\A)\(cast\B) oo udom_prj" -unfolding sprod_typ_def +lemma cast_sprod_defl: + "cast\(sprod_defl\A\B) = udom_emb oo sprod_map\(cast\A)\(cast\B) oo udom_prj" +unfolding sprod_defl_def apply (rule cast_TypeRep_fun2) apply (erule (1) finite_deflation_sprod_map) done -lemma cast_cprod_typ: - "cast\(cprod_typ\A\B) = udom_emb oo cprod_map\(cast\A)\(cast\B) oo udom_prj" -unfolding cprod_typ_def +lemma cast_cprod_defl: + "cast\(cprod_defl\A\B) = udom_emb oo cprod_map\(cast\A)\(cast\B) oo udom_prj" +unfolding cprod_defl_def apply (rule cast_TypeRep_fun2) apply (erule (1) finite_deflation_cprod_map) done -lemma cast_u_typ: - "cast\(u_typ\A) = udom_emb oo u_map\(cast\A) oo udom_prj" -unfolding u_typ_def +lemma cast_u_defl: + "cast\(u_defl\A) = udom_emb oo u_map\(cast\A) oo udom_prj" +unfolding u_defl_def apply (rule cast_TypeRep_fun1) apply (erule finite_deflation_u_map) done -lemma cast_upper_typ: - "cast\(upper_typ\A) = udom_emb oo upper_map\(cast\A) oo udom_prj" -unfolding upper_typ_def +lemma cast_upper_defl: + "cast\(upper_defl\A) = udom_emb oo upper_map\(cast\A) oo udom_prj" +unfolding upper_defl_def apply (rule cast_TypeRep_fun1) apply (erule finite_deflation_upper_map) done -lemma cast_lower_typ: - "cast\(lower_typ\A) = udom_emb oo lower_map\(cast\A) oo udom_prj" -unfolding lower_typ_def +lemma cast_lower_defl: + "cast\(lower_defl\A) = udom_emb oo lower_map\(cast\A) oo udom_prj" +unfolding lower_defl_def apply (rule cast_TypeRep_fun1) apply (erule finite_deflation_lower_map) done -lemma cast_convex_typ: - "cast\(convex_typ\A) = udom_emb oo convex_map\(cast\A) oo udom_prj" -unfolding convex_typ_def +lemma cast_convex_defl: + "cast\(convex_defl\A) = udom_emb oo convex_map\(cast\A) oo udom_prj" +unfolding convex_defl_def apply (rule cast_TypeRep_fun1) apply (erule finite_deflation_convex_map) done text {* REP of type constructor = type combinator *} -lemma REP_one: "REP(one) = one_typ" -by (simp only: one_typ_def) - -lemma REP_tr: "REP(tr) = tr_typ" -by (simp only: tr_typ_def) - -lemma REP_cfun: "REP('a \ 'b) = cfun_typ\REP('a)\REP('b)" +lemma REP_cfun: "REP('a \ 'b) = cfun_defl\REP('a)\REP('b)" apply (rule cast_eq_imp_eq, rule ext_cfun) -apply (simp add: cast_REP cast_cfun_typ) +apply (simp add: cast_REP cast_cfun_defl) apply (simp add: cfun_map_def) apply (simp only: prj_cfun_def emb_cfun_def) apply (simp add: expand_cfun_eq ep_pair.e_eq_iff [OF ep_pair_udom]) done -lemma REP_ssum: "REP('a \ 'b) = ssum_typ\REP('a)\REP('b)" +lemma REP_ssum: "REP('a \ 'b) = ssum_defl\REP('a)\REP('b)" apply (rule cast_eq_imp_eq, rule ext_cfun) -apply (simp add: cast_REP cast_ssum_typ) +apply (simp add: cast_REP cast_ssum_defl) apply (simp add: prj_ssum_def) apply (simp add: emb_ssum_def) apply (simp add: ssum_map_map cfcomp1) done -lemma REP_sprod: "REP('a \ 'b) = sprod_typ\REP('a)\REP('b)" +lemma REP_sprod: "REP('a \ 'b) = sprod_defl\REP('a)\REP('b)" apply (rule cast_eq_imp_eq, rule ext_cfun) -apply (simp add: cast_REP cast_sprod_typ) +apply (simp add: cast_REP cast_sprod_defl) apply (simp add: prj_sprod_def) apply (simp add: emb_sprod_def) apply (simp add: sprod_map_map cfcomp1) done -lemma REP_cprod: "REP('a \ 'b) = cprod_typ\REP('a)\REP('b)" +lemma REP_cprod: "REP('a \ 'b) = cprod_defl\REP('a)\REP('b)" apply (rule cast_eq_imp_eq, rule ext_cfun) -apply (simp add: cast_REP cast_cprod_typ) +apply (simp add: cast_REP cast_cprod_defl) apply (simp add: prj_cprod_def) apply (simp add: emb_cprod_def) apply (simp add: cprod_map_map cfcomp1) done -lemma REP_up: "REP('a u) = u_typ\REP('a)" +lemma REP_up: "REP('a u) = u_defl\REP('a)" apply (rule cast_eq_imp_eq, rule ext_cfun) -apply (simp add: cast_REP cast_u_typ) +apply (simp add: cast_REP cast_u_defl) apply (simp add: prj_u_def) apply (simp add: emb_u_def) apply (simp add: u_map_map cfcomp1) done -lemma REP_upper: "REP('a upper_pd) = upper_typ\REP('a)" +lemma REP_upper: "REP('a upper_pd) = upper_defl\REP('a)" apply (rule cast_eq_imp_eq, rule ext_cfun) -apply (simp add: cast_REP cast_upper_typ) +apply (simp add: cast_REP cast_upper_defl) apply (simp add: prj_upper_pd_def) apply (simp add: emb_upper_pd_def) apply (simp add: upper_map_map cfcomp1) done -lemma REP_lower: "REP('a lower_pd) = lower_typ\REP('a)" +lemma REP_lower: "REP('a lower_pd) = lower_defl\REP('a)" apply (rule cast_eq_imp_eq, rule ext_cfun) -apply (simp add: cast_REP cast_lower_typ) +apply (simp add: cast_REP cast_lower_defl) apply (simp add: prj_lower_pd_def) apply (simp add: emb_lower_pd_def) apply (simp add: lower_map_map cfcomp1) done -lemma REP_convex: "REP('a convex_pd) = convex_typ\REP('a)" +lemma REP_convex: "REP('a convex_pd) = convex_defl\REP('a)" apply (rule cast_eq_imp_eq, rule ext_cfun) -apply (simp add: cast_REP cast_convex_typ) +apply (simp add: cast_REP cast_convex_defl) apply (simp add: prj_convex_pd_def) apply (simp add: emb_convex_pd_def) apply (simp add: convex_map_map cfcomp1) done lemmas REP_simps = - REP_one - REP_tr REP_cfun REP_ssum REP_sprod @@ -944,69 +955,111 @@ apply (simp add: emb_coerce coerce_prj REP) done +lemma isodefl_abs_rep: + fixes abs and rep and d + assumes REP: "REP('b) = REP('a)" + assumes abs_def: "abs \ (coerce :: 'a \ 'b)" + assumes rep_def: "rep \ (coerce :: 'b \ 'a)" + shows "isodefl d t \ isodefl (abs oo d oo rep) t" +unfolding abs_def rep_def using REP by (rule isodefl_coerce) + lemma isodefl_cfun: "isodefl d1 t1 \ isodefl d2 t2 \ - isodefl (cfun_map\d1\d2) (cfun_typ\t1\t2)" + isodefl (cfun_map\d1\d2) (cfun_defl\t1\t2)" apply (rule isodeflI) -apply (simp add: cast_cfun_typ cast_isodefl) +apply (simp add: cast_cfun_defl cast_isodefl) apply (simp add: emb_cfun_def prj_cfun_def) apply (simp add: cfun_map_map cfcomp1) done lemma isodefl_ssum: "isodefl d1 t1 \ isodefl d2 t2 \ - isodefl (ssum_map\d1\d2) (ssum_typ\t1\t2)" + isodefl (ssum_map\d1\d2) (ssum_defl\t1\t2)" apply (rule isodeflI) -apply (simp add: cast_ssum_typ cast_isodefl) +apply (simp add: cast_ssum_defl cast_isodefl) apply (simp add: emb_ssum_def prj_ssum_def) apply (simp add: ssum_map_map isodefl_strict) done lemma isodefl_sprod: "isodefl d1 t1 \ isodefl d2 t2 \ - isodefl (sprod_map\d1\d2) (sprod_typ\t1\t2)" + isodefl (sprod_map\d1\d2) (sprod_defl\t1\t2)" apply (rule isodeflI) -apply (simp add: cast_sprod_typ cast_isodefl) +apply (simp add: cast_sprod_defl cast_isodefl) apply (simp add: emb_sprod_def prj_sprod_def) apply (simp add: sprod_map_map isodefl_strict) done +lemma isodefl_cprod: + "isodefl d1 t1 \ isodefl d2 t2 \ + isodefl (cprod_map\d1\d2) (cprod_defl\t1\t2)" +apply (rule isodeflI) +apply (simp add: cast_cprod_defl cast_isodefl) +apply (simp add: emb_cprod_def prj_cprod_def) +apply (simp add: cprod_map_map cfcomp1) +done + lemma isodefl_u: - "isodefl d t \ isodefl (u_map\d) (u_typ\t)" + "isodefl d t \ isodefl (u_map\d) (u_defl\t)" apply (rule isodeflI) -apply (simp add: cast_u_typ cast_isodefl) +apply (simp add: cast_u_defl cast_isodefl) apply (simp add: emb_u_def prj_u_def) apply (simp add: u_map_map) done -lemma isodefl_one: "isodefl (ID :: one \ one) one_typ" -unfolding one_typ_def by (rule isodefl_ID_REP) - -lemma isodefl_tr: "isodefl (ID :: tr \ tr) tr_typ" -unfolding tr_typ_def by (rule isodefl_ID_REP) - lemma isodefl_upper: - "isodefl d t \ isodefl (upper_map\d) (upper_typ\t)" + "isodefl d t \ isodefl (upper_map\d) (upper_defl\t)" apply (rule isodeflI) -apply (simp add: cast_upper_typ cast_isodefl) +apply (simp add: cast_upper_defl cast_isodefl) apply (simp add: emb_upper_pd_def prj_upper_pd_def) apply (simp add: upper_map_map) done lemma isodefl_lower: - "isodefl d t \ isodefl (lower_map\d) (lower_typ\t)" + "isodefl d t \ isodefl (lower_map\d) (lower_defl\t)" apply (rule isodeflI) -apply (simp add: cast_lower_typ cast_isodefl) +apply (simp add: cast_lower_defl cast_isodefl) apply (simp add: emb_lower_pd_def prj_lower_pd_def) apply (simp add: lower_map_map) done lemma isodefl_convex: - "isodefl d t \ isodefl (convex_map\d) (convex_typ\t)" + "isodefl d t \ isodefl (convex_map\d) (convex_defl\t)" apply (rule isodeflI) -apply (simp add: cast_convex_typ cast_isodefl) +apply (simp add: cast_convex_defl cast_isodefl) apply (simp add: emb_convex_pd_def prj_convex_pd_def) apply (simp add: convex_map_map) done +subsection {* Constructing Domain Isomorphisms *} + +use "Tools/Domain/domain_isomorphism.ML" + +setup {* + fold Domain_Isomorphism.add_type_constructor + [(@{type_name "->"}, @{term cfun_defl}, @{const_name cfun_map}, + @{thm REP_cfun}, @{thm isodefl_cfun}), + + (@{type_name "++"}, @{term ssum_defl}, @{const_name ssum_map}, + @{thm REP_ssum}, @{thm isodefl_ssum}), + + (@{type_name "**"}, @{term sprod_defl}, @{const_name sprod_map}, + @{thm REP_sprod}, @{thm isodefl_sprod}), + + (@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map}, + @{thm REP_cprod}, @{thm isodefl_cprod}), + + (@{type_name "u"}, @{term u_defl}, @{const_name u_map}, + @{thm REP_up}, @{thm isodefl_u}), + + (@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map}, + @{thm REP_upper}, @{thm isodefl_upper}), + + (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map}, + @{thm REP_lower}, @{thm isodefl_lower}), + + (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map}, + @{thm REP_convex}, @{thm isodefl_convex})] +*} + end diff -r ccef2e6d8c21 -r f5db63bd7aee src/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOLCF/Tools/Domain/domain_axioms.ML Fri Nov 20 00:54:20 2009 +0100 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Thu Nov 19 20:09:56 2009 -0800 @@ -6,13 +6,16 @@ signature DOMAIN_AXIOMS = sig - val copy_of_dtyp : (int -> term) -> Datatype.dtyp -> term + val copy_of_dtyp : + string Symtab.table -> (int -> term) -> Datatype.dtyp -> term val calc_axioms : + bool -> string Symtab.table -> string -> Domain_Library.eq list -> int -> Domain_Library.eq -> string * (string * term) list * (string * term) list val add_axioms : + bool -> bstring -> Domain_Library.eq list -> theory -> theory end; @@ -34,119 +37,124 @@ (@{type_name "*"}, @{const_name "cprod_map"}), (@{type_name "u"}, @{const_name "u_map"})]; -fun copy_of_dtyp r dt = if DatatypeAux.is_rec_type dt then copy r dt else ID -and copy r (DatatypeAux.DtRec i) = r i - | copy r (DatatypeAux.DtTFree a) = ID - | copy r (DatatypeAux.DtType (c, ds)) = - case Symtab.lookup copy_tab c of - SOME f => list_ccomb (%%:f, map (copy_of_dtyp r) ds) +fun copy_of_dtyp tab r dt = + if DatatypeAux.is_rec_type dt then copy tab r dt else ID +and copy tab r (DatatypeAux.DtRec i) = r i + | copy tab r (DatatypeAux.DtTFree a) = ID + | copy tab r (DatatypeAux.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 calc_axioms - (comp_dname : string) - (eqs : eq list) - (n : int) - (eqn as ((dname,_),cons) : eq) + (definitional : bool) + (map_tab : string Symtab.table) + (comp_dname : string) + (eqs : eq list) + (n : int) + (eqn as ((dname,_),cons) : eq) : string * (string * term) list * (string * term) list = - let - - (* ----- axioms and definitions concerning the isomorphism ------------------ *) + let - 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 = Long_Name.base_name dname; +(* ----- axioms and definitions concerning the isomorphism ------------------ *) - 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 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 = Long_Name.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") == - List.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 r i = proj (Bound 0) eqs i; - in ("copy_def", %%:(dname^"_copy") == - /\ "f" (dc_abs oo (copy_of_dtyp r (dtyp_of_eq eqn)) oo dc_rep)) end; - - (* -- definitions concerning the constructors, discriminators and selectors - *) + val when_def = ("when_def",%%:(dname^"_when") == + List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) => + Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons)); - fun con_def m n (_,args) = let - fun idxs z x arg = (if is_lazy arg then mk_up else I) (Bound(z-x)); - fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs); - fun inj y 1 _ = y - | inj y _ 0 = mk_sinl y - | inj y i j = mk_sinr (inj y (i-1) (j-1)); - in List.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 copy_def = + let fun r i = proj (Bound 0) eqs i; + in + ("copy_def", %%:(dname^"_copy") == /\ "f" + (dc_abs oo (copy_of_dtyp map_tab r (dtyp_of_eq eqn)) oo dc_rep)) + 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 mk_up else I) (Bound(z-x)); + fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs); + fun inj y 1 _ = y + | inj y _ 0 = mk_sinl y + | inj y i j = mk_sinr (inj y (i-1) (j-1)); + in List.foldr /\# (dc_abs`(inj (parms args) m n)) args end; - val dis_defs = let - fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == - list_ccomb(%%:(dname^"_when"),map - (fn (con',args) => (List.foldr /\# + 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) => (List.foldr /\# (if con'=con then TT else FF) args)) cons)) - in map ddef cons end; - - val mat_defs = - let - fun mdef (con,_) = - let - val k = Bound 0 - val x = Bound 1 - fun one_con (con', args') = - if con'=con then k else List.foldr /\# mk_fail args' - val w = list_ccomb(%%:(dname^"_when"), map one_con cons) - val rhs = /\ "x" (/\ "k" (w ` x)) - in (mat_name con ^"_def", %%:(mat_name con) == rhs) end - in map mdef cons end; + in map ddef cons end; - val pat_defs = + val mat_defs = + let + fun mdef (con,_) = + let + val k = Bound 0 + val x = Bound 1 + fun one_con (con', args') = + if con'=con then k else List.foldr /\# mk_fail args' + val w = list_ccomb(%%:(dname^"_when"), map one_con cons) + val rhs = /\ "x" (/\ "k" (w ` x)) + in (mat_name con ^"_def", %%:(mat_name con) == rhs) end + in map mdef cons end; + + val pat_defs = + let + fun pdef (con,args) = 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 [] => mk_return HOLogic.unit - | _ => mk_ctuple_pat ps ` mk_ctuple xs; - fun one_con (con',args') = List.foldr /\# (if con'=con then rhs else mk_fail) 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 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 [] => mk_return HOLogic.unit + | _ => mk_ctuple_pat ps ` mk_ctuple xs; + fun one_con (con',args') = List.foldr /\# (if con'=con then rhs else mk_fail) 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 - List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg); - in map_filter I (maps (fn (con,args) => mapn (sdef con) 1 args) 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 + List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg); + in map_filter I (maps (fn (con,args) => mapn (sdef con) 1 args) cons) end; - (* ----- axiom and definitions concerning induction ------------------------- *) +(* ----- axiom and definitions concerning induction ------------------------- *) - val reach_ax = ("reach", mk_trp(proj (mk_fix (%%:(comp_dname^"_copy"))) eqs n - `%x_name === %:x_name)); - val take_def = - ("take_def", - %%:(dname^"_take") == - mk_lam("n",proj - (mk_iterate (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))); + val reach_ax = ("reach", mk_trp(proj (mk_fix (%%:(comp_dname^"_copy"))) eqs n + `%x_name === %:x_name)); + val take_def = + ("take_def", + %%:(dname^"_take") == + mk_lam("n",proj + (mk_iterate (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 (calc_axioms) *) + in (dnam, + (if definitional then [reach_ax] else [abs_iso_ax, rep_iso_ax, reach_ax]), + (if definitional then [when_def] else [when_def, copy_def]) @ + con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @ + [take_def, finite_def]) + end; (* let (calc_axioms) *) (* legacy type inference *) @@ -173,16 +181,17 @@ val ms = map qualify con_names ~~ map qualify mat_names; in Fixrec.add_matchers ms thy end; -fun add_axioms comp_dnam (eqs : eq list) thy' = - let - val comp_dname = Sign.full_bname 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"(mk_ctuple (map copy_app dnames))); +fun add_axioms definitional comp_dnam (eqs : eq list) thy' = + let + val comp_dname = Sign.full_bname 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"(mk_ctuple (map copy_app dnames))); - fun one_con (con,args) = let + fun one_con (con,args) = + let val nonrec_args = filter_out is_rec args; val rec_args = filter is_rec args; val recs_cnt = length rec_args; @@ -199,37 +208,45 @@ 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 = - List.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 List.foldr mk_ex - (Library.foldr mk_conj - (map (defined o Bound) nonlazy_idxs,capps)) allvns + List.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 + List.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)))); - val bisim_def = - ("bisim_def", - %%:(comp_dname^"_bisim")==mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs))); - - fun add_one (dnam, axs, dfs) = - Sign.add_path dnam + 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)))); + val bisim_def = + ("bisim_def", %%:(comp_dname^"_bisim") == + mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs))); + + fun add_one (dnam, axs, dfs) = + Sign.add_path dnam #> add_defs_infer dfs #> add_axioms_infer axs #> Sign.parent_path; - val thy = fold add_one (mapn (calc_axioms comp_dname eqs) 0 eqs) thy'; + val map_tab = Domain_Isomorphism.get_map_tab thy'; + + val thy = thy' + |> fold add_one (mapn (calc_axioms definitional map_tab comp_dname eqs) 0 eqs); - in thy |> Sign.add_path comp_dnam - |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else [])) - |> Sign.parent_path - |> fold add_matchers eqs - end; (* let (add_axioms) *) + in + thy + |> Sign.add_path comp_dnam + |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else [])) + |> Sign.parent_path + |> fold add_matchers eqs + end; (* let (add_axioms) *) end; (* struct *) diff -r ccef2e6d8c21 -r f5db63bd7aee src/HOLCF/Tools/Domain/domain_extender.ML --- a/src/HOLCF/Tools/Domain/domain_extender.ML Fri Nov 20 00:54:20 2009 +0100 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML Thu Nov 19 20:09:56 2009 -0800 @@ -6,14 +6,29 @@ signature DOMAIN_EXTENDER = sig - val add_domain_cmd: string -> - ((string * string option) list * binding * mixfix * - (binding * (bool * binding option * string) list * mixfix) list) list - -> theory -> theory - val add_domain: string -> - ((string * string option) list * binding * mixfix * - (binding * (bool * binding option * typ) list * mixfix) list) list - -> theory -> theory + val add_domain_cmd: + string -> + ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * string) list * mixfix) list) list + -> theory -> theory + + val add_domain: + string -> + ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * typ) list * mixfix) list) list + -> theory -> theory + + val add_new_domain_cmd: + string -> + ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * string) list * mixfix) list) list + -> theory -> theory + + val add_new_domain: + string -> + ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * typ) list * mixfix) list) list + -> theory -> theory end; structure Domain_Extender :> DOMAIN_EXTENDER = @@ -23,132 +38,231 @@ (* ----- general testing and preprocessing of constructor list -------------- *) fun check_and_sort_domain - (dtnvs : (string * typ list) list) - (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list) - (sg : theory) + (definitional : bool) + (dtnvs : (string * typ list) list) + (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list) + (thy : theory) : ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list = - 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 (Binding.name_of o first) (flat cons'')) of - [] => false | dups => error ("Duplicate constructors: " - ^ commas_quote dups)); - val test_dupl_sels = - (case duplicates (op =) (map Binding.name_of (map_filter second - (maps second (flat 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 (op =) (s, defaultS) orelse - eq_set (op =) (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 lazy T = - let val ok = if lazy then cpo_type else pcpo_type - in if ok sg T then T else error - ("Constructor argument type is not of sort pcpo: " ^ - string_of_typ sg T) - end; - fun analyse_arg (lazy, sel, T) = - (lazy, sel, check_pcpo lazy (analyse false T)); - fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx); - in ((dname,distinct_typevars), map analyse_con cons') end; - in ListPair.map analyse_equation (dtnvs,cons'') - end; (* let *) + let + val defaultS = Sign.defaultS thy; + + val test_dupl_typs = + case duplicates (op =) (map fst dtnvs) of + [] => false | dups => error ("Duplicate types: " ^ commas_quote dups); + + val all_cons = map (Binding.name_of o first) (flat cons''); + val test_dupl_cons = + case duplicates (op =) all_cons of + [] => false | dups => error ("Duplicate constructors: " + ^ commas_quote dups); + val all_sels = + (map Binding.name_of o map_filter second o maps second) (flat cons''); + val test_dupl_sels = + case duplicates (op =) all_sels of + [] => false | dups => error("Duplicate selectors: "^commas_quote dups); + + fun test_dupl_tvars s = + case duplicates (op =) (map(fst o dest_TFree)s) of + [] => false | dups => error("Duplicate type arguments: " + ^commas_quote dups); + val test_dupl_tvars' = exists test_dupl_tvars (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 (op =) (s, defaultS) orelse + eq_set (op =) (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 definitional orelse 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 thy 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 thy t) ^ + " with different arguments")) + | analyse indirect (TVar _) = Imposs "extender:analyse"; + fun check_pcpo lazy T = + let val ok = if lazy then cpo_type else pcpo_type + in if ok thy T then T + else error ("Constructor argument type is not of sort pcpo: " ^ + string_of_typ thy T) + end; + fun analyse_arg (lazy, sel, T) = + (lazy, sel, check_pcpo lazy (analyse false T)); + fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx); + 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 : theory -> 'a -> typ) - (comp_dnam : string) - (eqs''' : ((string * string option) list * binding * mixfix * - (binding * (bool * binding option * 'a) list * mixfix) list) list) - (thy''' : theory) = - let - fun readS (SOME s) = Syntax.read_sort_global thy''' s - | readS NONE = Sign.defaultS thy'''; - fun readTFree (a, s) = TFree (a, readS s); + (prep_typ : theory -> 'a -> typ) + (comp_dnam : string) + (eqs''' : ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * 'a) list * mixfix) list) list) + (thy''' : theory) = + let + fun readS (SOME s) = Syntax.read_sort_global thy''' s + | readS NONE = Sign.defaultS thy'''; + fun readTFree (a, s) = TFree (a, readS s); + + val dtnvs = map (fn (vs,dname:binding,mx,_) => + (dname, map readTFree vs, mx)) eqs'''; + val cons''' = map (fn (_,_,_,cons) => cons) eqs'''; + fun thy_type (dname,tvars,mx) = (dname, length tvars, mx); + fun thy_arity (dname,tvars,mx) = + (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, pcpoS); + val thy'' = + thy''' + |> Sign.add_types (map thy_type dtnvs) + |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs; + val cons'' = + map (map (upd_second (map (upd_third (prep_typ thy''))))) cons'''; + val dtnvs' = + map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs; + val eqs' : ((string * typ list) * + (binding * (bool * binding option * typ) list * mixfix) list) list = + check_and_sort_domain false dtnvs' cons'' thy''; + val thy' = thy'' |> Domain_Syntax.add_syntax false 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 (fn s => s = "'") ss + 1, ss); + fun typid (Type (id,_)) = + let val c = hd (Symbol.explode (Long_Name.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,args,mx) = + ((Syntax.const_name mx (Binding.name_of con)), + ListPair.map (fn ((lazy,sel,tp),vn) => + mk_arg ((lazy, DatatypeAux.dtyp_of_typ new_dts tp), + Option.map Binding.name_of sel,vn)) + (args,(mk_var_names(map (typid o third) args))) + ) : cons; + val eqs : eq list = + map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs'; + val thy = thy' |> Domain_Axioms.add_axioms false comp_dnam eqs; + val ((rewss, take_rews), theorems_thy) = + thy + |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs + ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs); + in + theorems_thy + |> Sign.add_path (Long_Name.base_name comp_dnam) + |> PureThy.add_thmss + [((Binding.name "rews", flat rewss @ take_rews), [])] + |> snd + |> Sign.parent_path + end; - val dtnvs = map (fn (vs,dname:binding,mx,_) => - (dname, map readTFree vs, mx)) eqs'''; - val cons''' = map (fn (_,_,_,cons) => cons) eqs'''; - fun thy_type (dname,tvars,mx) = (dname, length tvars, mx); - fun thy_arity (dname,tvars,mx) = (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, pcpoS); - val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs) - |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs; - val cons'' = map (map (upd_second (map (upd_third (prep_typ thy''))))) cons'''; - val dtnvs' = map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs; - val eqs' : ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list = - 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 (fn s => s = "'") ss + 1, ss); - fun typid (Type (id,_)) = - let val c = hd (Symbol.explode (Long_Name.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,args,mx) = - ((Syntax.const_name mx (Binding.name_of con)), - ListPair.map (fn ((lazy,sel,tp),vn) => mk_arg ((lazy, - DatatypeAux.dtyp_of_typ new_dts tp), - Option.map Binding.name_of 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 ((rewss, take_rews), theorems_thy) = - thy |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs - ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs); - in - theorems_thy - |> Sign.add_path (Long_Name.base_name comp_dnam) - |> (snd o (PureThy.add_thmss [((Binding.name "rews", flat rewss @ take_rews), [])])) - |> Sign.parent_path - end; +fun gen_add_new_domain + (prep_typ : theory -> 'a -> typ) + (comp_dnam : string) + (eqs''' : ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * 'a) list * mixfix) list) list) + (thy''' : theory) = + let + fun readS (SOME s) = Syntax.read_sort_global thy''' s + | readS NONE = Sign.defaultS thy'''; + fun readTFree (a, s) = TFree (a, readS s); + + val dtnvs = map (fn (vs,dname:binding,mx,_) => + (dname, map readTFree vs, mx)) eqs'''; + val cons''' = map (fn (_,_,_,cons) => cons) eqs'''; + fun thy_type (dname,tvars,mx) = (dname, length tvars, mx); + fun thy_arity (dname,tvars,mx) = + (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, @{sort rep}); + + (* this theory is used just for parsing and error checking *) + val tmp_thy = thy''' + |> Theory.copy + |> Sign.add_types (map thy_type dtnvs) + |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs; + + val cons'' : (binding * (bool * binding option * typ) list * mixfix) list list = + map (map (upd_second (map (upd_third (prep_typ tmp_thy))))) cons'''; + val dtnvs' : (string * typ list) list = + map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs; + val eqs' : ((string * typ list) * + (binding * (bool * binding option * typ) list * mixfix) list) list = + check_and_sort_domain true dtnvs' cons'' tmp_thy; + + fun mk_arg_typ (lazy, dest_opt, 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); + + val thy'' = thy''' |> + Domain_Isomorphism.domain_isomorphism + (map (fn ((vs, dname, mx, _), eq) => + (map fst vs, dname, mx, mk_eq_typ eq)) + (eqs''' ~~ eqs')) + + val thy' = thy'' |> Domain_Syntax.add_syntax true 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 (fn s => s = "'") ss + 1, ss); + fun typid (Type (id,_)) = + let val c = hd (Symbol.explode (Long_Name.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,args,mx) = + ((Syntax.const_name mx (Binding.name_of con)), + ListPair.map (fn ((lazy,sel,tp),vn) => + mk_arg ((lazy, DatatypeAux.dtyp_of_typ new_dts tp), + Option.map Binding.name_of sel,vn)) + (args,(mk_var_names(map (typid o third) args))) + ) : cons; + val eqs : eq list = + map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs'; + val thy = thy' |> Domain_Axioms.add_axioms true comp_dnam eqs; + val ((rewss, take_rews), theorems_thy) = + thy + |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs + ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs); + in + theorems_thy + |> Sign.add_path (Long_Name.base_name comp_dnam) + |> PureThy.add_thmss + [((Binding.name "rews", flat rewss @ take_rews), [])] + |> snd + |> Sign.parent_path + end; val add_domain = gen_add_domain Sign.certify_typ; val add_domain_cmd = gen_add_domain Syntax.read_typ_global; +val add_new_domain = gen_add_new_domain Sign.certify_typ; +val add_new_domain_cmd = gen_add_new_domain Syntax.read_typ_global; + (** outer syntax **) @@ -157,47 +271,57 @@ val _ = OuterKeyword.keyword "lazy"; val dest_decl : (bool * binding option * string) parser = - P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false -- - (P.binding >> 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)); + P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false -- + (P.binding >> 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.binding -- Scan.repeat dest_decl -- P.opt_mixfix; + P.binding -- Scan.repeat dest_decl -- P.opt_mixfix; val type_var' : (string * string option) parser = - (P.type_ident -- Scan.option (P.$$$ "::" |-- P.!!! P.sort)); + (P.type_ident -- Scan.option (P.$$$ "::" |-- P.!!! P.sort)); val type_args' : (string * string option) list parser = - type_var' >> single || - P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") || - Scan.succeed []; + type_var' >> single + || P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") + || Scan.succeed []; val domain_decl = - (type_args' -- P.binding -- P.opt_infix) -- - (P.$$$ "=" |-- P.enum1 "|" cons_decl); + (type_args' -- P.binding -- P.opt_infix) -- + (P.$$$ "=" |-- P.enum1 "|" cons_decl); val domains_decl = - Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- - P.and_list1 domain_decl; + Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- + P.and_list1 domain_decl; -fun mk_domain (opt_name : string option, - doms : ((((string * string option) list * binding) * mixfix) * - ((binding * (bool * binding option * string) list) * mixfix) list) list ) = - let - val names = map (fn (((_, t), _), _) => Binding.name_of t) doms; - val specs : ((string * string option) list * binding * mixfix * - (binding * (bool * binding option * string) list * mixfix) list) list = - map (fn (((vs, t), mx), cons) => - (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms; - val comp_dnam = - case opt_name of NONE => space_implode "_" names | SOME s => s; - in add_domain_cmd comp_dnam specs end; +fun mk_domain + (definitional : bool) + (opt_name : string option, + doms : ((((string * string option) list * binding) * mixfix) * + ((binding * (bool * binding option * string) list) * mixfix) list) list ) = + let + val names = map (fn (((_, t), _), _) => Binding.name_of t) doms; + val specs : ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * string) list * mixfix) list) list = + map (fn (((vs, t), mx), cons) => + (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms; + val comp_dnam = + case opt_name of NONE => space_implode "_" names | SOME s => s; + in + if definitional + then add_new_domain_cmd comp_dnam specs + else add_domain_cmd comp_dnam specs + end; val _ = - OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl - (domains_decl >> (Toplevel.theory o mk_domain)); + OuterSyntax.command "domain" "define recursive domains (HOLCF)" + K.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false)); + +val _ = + OuterSyntax.command "new_domain" "define recursive domains (HOLCF)" + K.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true)); end; diff -r ccef2e6d8c21 -r f5db63bd7aee src/HOLCF/Tools/Domain/domain_isomorphism.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Thu Nov 19 20:09:56 2009 -0800 @@ -0,0 +1,636 @@ +(* Title: HOLCF/Tools/domain/domain_isomorphism.ML + Author: Brian Huffman + +Defines new types satisfying the given domain equations. +*) + +signature DOMAIN_ISOMORPHISM = +sig + val domain_isomorphism: + (string list * binding * mixfix * typ) list -> theory -> theory + val domain_isomorphism_cmd: + (string list * binding * mixfix * string) list -> theory -> theory + val add_type_constructor: + (string * term * string * thm * thm) -> theory -> theory + val get_map_tab: + theory -> string Symtab.table +end; + +structure Domain_Isomorphism :> DOMAIN_ISOMORPHISM = +struct + +val beta_ss = + HOL_basic_ss + addsimps simp_thms + addsimps [@{thm beta_cfun}] + addsimprocs [@{simproc cont_proc}]; + +val beta_tac = simp_tac beta_ss; + +(******************************************************************************) +(******************************** theory data *********************************) +(******************************************************************************) + +structure DeflData = Theory_Data +( + type T = term Symtab.table; + val empty = Symtab.empty; + val extend = I; + fun merge data = Symtab.merge (K true) data; +); + +structure MapData = Theory_Data +( + type T = string Symtab.table; + val empty = Symtab.empty; + val extend = I; + fun merge data = Symtab.merge (K true) data; +); + +structure RepData = Theory_Data +( + type T = thm list; + val empty = []; + val extend = I; + val merge = Thm.merge_thms; +); + +structure IsodeflData = Theory_Data +( + type T = thm list; + val empty = []; + val extend = I; + val merge = Thm.merge_thms; +); + +fun add_type_constructor + (tname, defl_const, map_name, REP_thm, isodefl_thm) = + DeflData.map (Symtab.insert (K true) (tname, defl_const)) + #> MapData.map (Symtab.insert (K true) (tname, map_name)) + #> RepData.map (Thm.add_thm REP_thm) + #> IsodeflData.map (Thm.add_thm isodefl_thm); + +val get_map_tab = MapData.get; + + +(******************************************************************************) +(******************************* building types *******************************) +(******************************************************************************) + +(* ->> is taken from holcf_logic.ML *) +fun cfunT (T, U) = Type(@{type_name "->"}, [T, U]); + +infixr 6 ->>; val (op ->>) = cfunT; + +fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U) + | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []); + +fun tupleT [] = HOLogic.unitT + | tupleT [T] = T + | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts); + +val deflT = @{typ "udom alg_defl"}; + +fun mapT (T as Type (_, Ts)) = + Library.foldr cfunT (map (fn T => T ->> T) Ts, T ->> T); + +(******************************************************************************) +(******************************* building terms *******************************) +(******************************************************************************) + +(* builds the expression (v1,v2,..,vn) *) +fun mk_tuple [] = HOLogic.unit +| mk_tuple (t::[]) = t +| mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts); + +(* builds the expression (%(v1,v2,..,vn). rhs) *) +fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs + | lambda_tuple (v::[]) rhs = Term.lambda v rhs + | lambda_tuple (v::vs) rhs = + HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs)); + +(* continuous application and abstraction *) + +fun capply_const (S, T) = + Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T)); + +fun cabs_const (S, T) = + Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T)); + +fun mk_cabs t = + let val T = Term.fastype_of t + in cabs_const (Term.domain_type T, Term.range_type T) $ t end + +(* builds the expression (LAM v. rhs) *) +fun big_lambda v rhs = + cabs_const (Term.fastype_of v, Term.fastype_of rhs) $ 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); + +fun mk_capply (t, u) = + let val (S, T) = + case Term.fastype_of t of + Type(@{type_name "->"}, [S, T]) => (S, T) + | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]); + in capply_const (S, T) $ t $ u end; + +(* miscellaneous term constructions *) + +val mk_trp = HOLogic.mk_Trueprop; + +val mk_fst = HOLogic.mk_fst; +val mk_snd = HOLogic.mk_snd; + +fun mk_cont t = + let val T = Term.fastype_of t + in Const(@{const_name cont}, T --> HOLogic.boolT) $ t end; + +fun mk_fix t = + let val (T, _) = dest_cfunT (Term.fastype_of t) + in mk_capply (Const(@{const_name fix}, (T ->> T) ->> T), t) end; + +fun ID_const T = Const (@{const_name ID}, cfunT (T, T)); + +fun cfcomp_const (T, U, V) = + Const (@{const_name cfcomp}, (U ->> V) ->> (T ->> U) ->> (T ->> V)); + +fun mk_cfcomp (f, g) = + let + val (U, V) = dest_cfunT (Term.fastype_of f); + val (T, U') = dest_cfunT (Term.fastype_of g); + in + if U = U' + then mk_capply (mk_capply (cfcomp_const (T, U, V), f), g) + else raise TYPE ("mk_cfcomp", [U, U'], [f, g]) + end; + +fun mk_Rep_of T = + Const (@{const_name Rep_of}, Term.itselfT T --> deflT) $ Logic.mk_type T; + +fun coerce_const T = Const (@{const_name coerce}, T); + +fun isodefl_const T = + Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT); + +(* splits a cterm into the right and lefthand sides of equality *) +fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t); + +fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)); + +(******************************************************************************) +(*************** fixed-point definitions and unfolding theorems ***************) +(******************************************************************************) + +fun add_fixdefs + (spec : (binding * term) list) + (thy : theory) : (thm list * thm list) * theory = + let + val binds = map fst spec; + val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec); + val functional = lambda_tuple lhss (mk_tuple rhss); + val fixpoint = mk_fix (mk_cabs functional); + + (* project components of fixpoint *) + fun mk_projs (x::[]) t = [(x, t)] + | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t); + val projs = mk_projs lhss fixpoint; + + (* convert parameters to lambda abstractions *) + fun mk_eqn (lhs, rhs) = + case lhs of + Const (@{const_name Rep_CFun}, _) $ f $ (x as Free _) => + mk_eqn (f, big_lambda x rhs) + | Const _ => Logic.mk_equals (lhs, rhs) + | _ => raise TERM ("lhs not of correct form", [lhs, rhs]); + val eqns = map mk_eqn projs; + + (* register constant definitions *) + val (fixdef_thms, thy) = + (PureThy.add_defs false o map Thm.no_attributes) + (map (Binding.suffix_name "_def") binds ~~ eqns) thy; + + (* prove applied version of definitions *) + fun prove_proj (lhs, rhs) = + let + val tac = rewrite_goals_tac fixdef_thms THEN beta_tac 1; + val goal = Logic.mk_equals (lhs, rhs); + in Goal.prove_global thy [] [] goal (K tac) end; + val proj_thms = map prove_proj projs; + + (* mk_tuple lhss == fixpoint *) + fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2]; + val tuple_fixdef_thm = foldr1 pair_equalI proj_thms; + + val cont_thm = + Goal.prove_global thy [] [] (mk_trp (mk_cont functional)) + (K (beta_tac 1)); + val tuple_unfold_thm = + (@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm]) + |> LocalDefs.unfold (ProofContext.init thy) @{thms split_conv}; + + fun mk_unfold_thms [] thm = [] + | mk_unfold_thms (n::[]) thm = [(n, thm)] + | mk_unfold_thms (n::ns) thm = let + val thmL = thm RS @{thm Pair_eqD1}; + val thmR = thm RS @{thm Pair_eqD2}; + in (n, thmL) :: mk_unfold_thms ns thmR end; + val unfold_binds = map (Binding.suffix_name "_unfold") binds; + + (* register unfold theorems *) + val (unfold_thms, thy) = + (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.standard)) + (mk_unfold_thms unfold_binds tuple_unfold_thm) thy; + in + ((proj_thms, unfold_thms), thy) + end; + + +(******************************************************************************) +(****************** deflation combinators and map functions *******************) +(******************************************************************************) + +fun defl_of_typ + (tab : term Symtab.table) + (T : typ) : term = + let + fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts + | is_closed_typ _ = false; + fun defl_of (TFree (a, _)) = Free (Library.unprefix "'" a, deflT) + | defl_of (TVar _) = error ("defl_of_typ: TVar") + | defl_of (T as Type (c, Ts)) = + case Symtab.lookup tab c of + SOME t => Library.foldl mk_capply (t, map defl_of Ts) + | NONE => if is_closed_typ T + then mk_Rep_of T + else error ("defl_of_typ: type variable under unsupported type constructor " ^ c); + in defl_of T end; + +fun map_of_typ + (tab : string Symtab.table) + (T : typ) : term = + let + fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts + | is_closed_typ _ = false; + fun map_of (T as TFree (a, _)) = Free (Library.unprefix "'" a, T ->> T) + | map_of (T as TVar _) = error ("map_of_typ: TVar") + | map_of (T as Type (c, Ts)) = + case Symtab.lookup tab c of + SOME t => Library.foldl mk_capply (Const (t, mapT T), map map_of Ts) + | NONE => if is_closed_typ T + then ID_const T + else error ("map_of_typ: type variable under unsupported type constructor " ^ c); + in map_of T end; + + +(******************************************************************************) +(* prepare datatype specifications *) + +fun read_typ thy str sorts = + let + val ctxt = ProofContext.init thy + |> fold (Variable.declare_typ o TFree) sorts; + val T = Syntax.read_typ ctxt str; + in (T, Term.add_tfreesT T sorts) end; + +fun cert_typ sign raw_T sorts = + let + val T = Type.no_tvars (Sign.certify_typ sign raw_T) + handle TYPE (msg, _, _) => error msg; + val sorts' = Term.add_tfreesT T sorts; + val _ = + case duplicates (op =) (map fst sorts') of + [] => () + | dups => error ("Inconsistent sort constraints for " ^ commas dups) + in (T, sorts') end; + +fun gen_domain_isomorphism + (prep_typ: theory -> 'a -> (string * sort) list -> typ * (string * sort) list) + (doms_raw: (string list * binding * mixfix * 'a) list) + (thy: theory) + : theory = + let + val _ = Theory.requires thy "Representable" "domain isomorphisms"; + + (* this theory is used just for parsing *) + val tmp_thy = thy |> + Theory.copy |> + Sign.add_types (map (fn (tvs, tname, mx, _) => + (tname, length tvs, mx)) doms_raw); + + fun prep_dom thy (vs, t, mx, typ_raw) sorts = + let val (typ, sorts') = prep_typ thy typ_raw sorts + in ((vs, t, mx, typ), sorts') end; + + val (doms : (string list * binding * mixfix * typ) list, + sorts : (string * sort) list) = + fold_map (prep_dom tmp_thy) doms_raw []; + + (* domain equations *) + fun mk_dom_eqn (vs, tbind, mx, rhs) = + let fun arg v = TFree (v, the (AList.lookup (op =) sorts v)); + in (Type (Sign.full_name tmp_thy tbind, map arg vs), rhs) end; + val dom_eqns = map mk_dom_eqn doms; + + (* check for valid type parameters *) + val (tyvars, _, _, _)::_ = doms; + val new_doms = map (fn (tvs, tname, mx, _) => + let val full_tname = Sign.full_name tmp_thy tname + in + (case duplicates (op =) tvs of + [] => + if eq_set (op =) (tyvars, tvs) then (full_tname, tvs) + else error ("Mutually recursive domains must have same type parameters") + | dups => error ("Duplicate parameter(s) for domain " ^ quote (Binding.str_of tname) ^ + " : " ^ commas dups)) + end) doms; + val dom_binds = map (fn (_, tbind, _, _) => tbind) doms; + + (* declare deflation combinator constants *) + fun declare_defl_const (vs, tbind, mx, rhs) thy = + let + val defl_type = Library.foldr cfunT (map (K deflT) vs, deflT); + val defl_bind = Binding.suffix_name "_defl" tbind; + in + Sign.declare_const ((defl_bind, defl_type), NoSyn) thy + end; + val (defl_consts, thy) = fold_map declare_defl_const doms thy; + + (* defining equations for type combinators *) + val defl_tab1 = DeflData.get thy; + val defl_tab2 = + Symtab.make (map (fst o dest_Type o fst) dom_eqns ~~ defl_consts); + val defl_tab' = Symtab.merge (K true) (defl_tab1, defl_tab2); + val thy = DeflData.put defl_tab' thy; + fun mk_defl_spec (lhsT, rhsT) = + mk_eqs (defl_of_typ defl_tab' lhsT, + defl_of_typ defl_tab' rhsT); + val defl_specs = map mk_defl_spec dom_eqns; + + (* register recursive definition of deflation combinators *) + val defl_binds = map (Binding.suffix_name "_defl") dom_binds; + val ((defl_apply_thms, defl_unfold_thms), thy) = + add_fixdefs (defl_binds ~~ defl_specs) thy; + + (* define types using deflation combinators *) + fun make_repdef ((vs, tbind, mx, _), defl_const) thy = + let + fun tfree a = TFree (a, the (AList.lookup (op =) sorts a)) + val reps = map (mk_Rep_of o tfree) vs; + val defl = Library.foldl mk_capply (defl_const, reps); + val ((_, _, _, {REP, ...}), thy) = + Repdef.add_repdef false NONE (tbind, vs, mx) defl NONE thy; + in + (REP, thy) + end; + val (REP_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy; + val thy = RepData.map (fold Thm.add_thm REP_thms) thy; + + (* prove REP equations *) + fun mk_REP_eq_thm (lhsT, rhsT) = + let + val goal = mk_eqs (mk_Rep_of lhsT, mk_Rep_of rhsT); + val REP_simps = RepData.get thy; + val tac = + simp_tac (HOL_basic_ss addsimps REP_simps) 1 + THEN resolve_tac defl_unfold_thms 1; + in + Goal.prove_global thy [] [] goal (K tac) + end; + val REP_eq_thms = map mk_REP_eq_thm dom_eqns; + + (* register REP equations *) + val REP_eq_binds = map (Binding.prefix_name "REP_eq_") dom_binds; + val (_, thy) = thy |> + (PureThy.add_thms o map Thm.no_attributes) + (REP_eq_binds ~~ REP_eq_thms); + + (* define rep/abs functions *) + fun mk_rep_abs (tbind, (lhsT, rhsT)) thy = + let + val rep_type = cfunT (lhsT, rhsT); + val abs_type = cfunT (rhsT, lhsT); + val rep_bind = Binding.suffix_name "_rep" tbind; + val abs_bind = Binding.suffix_name "_abs" tbind; + val (rep_const, thy) = thy |> + Sign.declare_const ((rep_bind, rep_type), NoSyn); + val (abs_const, thy) = thy |> + Sign.declare_const ((abs_bind, abs_type), NoSyn); + val rep_eqn = Logic.mk_equals (rep_const, coerce_const rep_type); + val abs_eqn = Logic.mk_equals (abs_const, coerce_const abs_type); + val ([rep_def, abs_def], thy) = thy |> + (PureThy.add_defs false o map Thm.no_attributes) + [(Binding.suffix_name "_rep_def" tbind, rep_eqn), + (Binding.suffix_name "_abs_def" tbind, abs_eqn)]; + in + (((rep_const, abs_const), (rep_def, abs_def)), thy) + end; + val ((rep_abs_consts, rep_abs_defs), thy) = thy + |> fold_map mk_rep_abs (dom_binds ~~ dom_eqns) + |>> ListPair.unzip; + + (* prove isomorphism and isodefl rules *) + fun mk_iso_thms ((tbind, REP_eq), (rep_def, abs_def)) thy = + let + fun make thm = Drule.standard (thm OF [REP_eq, abs_def, rep_def]); + val rep_iso_thm = make @{thm domain_rep_iso}; + val abs_iso_thm = make @{thm domain_abs_iso}; + val isodefl_thm = make @{thm isodefl_abs_rep}; + val rep_iso_bind = Binding.name "rep_iso"; + val abs_iso_bind = Binding.name "abs_iso"; + val isodefl_bind = Binding.name "isodefl_abs_rep"; + val (_, thy) = thy + |> Sign.add_path (Binding.name_of tbind) + |> (PureThy.add_thms o map Thm.no_attributes) + [(rep_iso_bind, rep_iso_thm), + (abs_iso_bind, abs_iso_thm), + (isodefl_bind, isodefl_thm)] + ||> Sign.parent_path; + in + (((rep_iso_thm, abs_iso_thm), isodefl_thm), thy) + end; + val ((iso_thms, isodefl_abs_rep_thms), thy) = thy + |> fold_map mk_iso_thms (dom_binds ~~ REP_eq_thms ~~ rep_abs_defs) + |>> ListPair.unzip; + + (* declare map functions *) + fun declare_map_const (tbind, (lhsT, rhsT)) thy = + let + val map_type = mapT lhsT; + val map_bind = Binding.suffix_name "_map" tbind; + in + Sign.declare_const ((map_bind, map_type), NoSyn) thy + end; + val (map_consts, thy) = thy |> + fold_map declare_map_const (dom_binds ~~ dom_eqns); + + (* defining equations for map functions *) + val map_tab1 = MapData.get thy; + val map_tab2 = + Symtab.make (map (fst o dest_Type o fst) dom_eqns + ~~ map (fst o dest_Const) map_consts); + val map_tab' = Symtab.merge (K true) (map_tab1, map_tab2); + val thy = MapData.put map_tab' thy; + fun mk_map_spec ((rep_const, abs_const), (lhsT, rhsT)) = + let + val lhs = map_of_typ map_tab' lhsT; + val body = map_of_typ map_tab' rhsT; + val rhs = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const)); + in mk_eqs (lhs, rhs) end; + val map_specs = map mk_map_spec (rep_abs_consts ~~ dom_eqns); + + (* register recursive definition of map functions *) + val map_binds = map (Binding.suffix_name "_map") dom_binds; + val ((map_apply_thms, map_unfold_thms), thy) = + add_fixdefs (map_binds ~~ map_specs) thy; + + (* prove isodefl rules for map functions *) + val isodefl_thm = + let + fun unprime a = Library.unprefix "'" a; + fun mk_d (TFree (a, _)) = Free ("d" ^ unprime a, deflT); + fun mk_f (T as TFree (a, _)) = Free ("f" ^ unprime a, T ->> T); + fun mk_assm T = mk_trp (isodefl_const T $ mk_f T $ mk_d T); + fun mk_goal ((map_const, defl_const), (T as Type (c, Ts), rhsT)) = + let + val map_term = Library.foldl mk_capply (map_const, map mk_f Ts); + val defl_term = Library.foldl mk_capply (defl_const, map mk_d Ts); + in isodefl_const T $ map_term $ defl_term end; + val assms = (map mk_assm o snd o dest_Type o fst o hd) dom_eqns; + val goals = map mk_goal (map_consts ~~ defl_consts ~~ dom_eqns); + val goal = mk_trp (foldr1 HOLogic.mk_conj goals); + val start_thms = + @{thm split_def} :: defl_apply_thms @ map_apply_thms; + val adm_rules = + @{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id}; + val bottom_rules = + @{thms fst_strict snd_strict isodefl_bottom simp_thms}; + val isodefl_rules = + @{thms conjI isodefl_ID_REP} + @ isodefl_abs_rep_thms + @ IsodeflData.get thy; + fun tacf {prems, ...} = EVERY + [simp_tac (HOL_basic_ss addsimps start_thms) 1, + (* FIXME: how reliable is unification here? *) + (* Maybe I should instantiate the rule. *) + rtac @{thm parallel_fix_ind} 1, + REPEAT (resolve_tac adm_rules 1), + simp_tac (HOL_basic_ss addsimps bottom_rules) 1, + simp_tac beta_ss 1, + simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1, + REPEAT (etac @{thm conjE} 1), + REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)]; + in + Goal.prove_global thy [] assms goal tacf + end; + val isodefl_binds = map (Binding.prefix_name "isodefl_") dom_binds; + fun conjuncts [] thm = [] + | conjuncts (n::[]) thm = [(n, thm)] + | conjuncts (n::ns) thm = let + val thmL = thm RS @{thm conjunct1}; + val thmR = thm RS @{thm conjunct2}; + in (n, thmL):: conjuncts ns thmR end; + val (isodefl_thms, thy) = thy |> + (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.standard)) + (conjuncts isodefl_binds isodefl_thm); + val thy = IsodeflData.map (fold Thm.add_thm isodefl_thms) thy; + + (* prove map_ID theorems *) + fun prove_map_ID_thm + (((map_const, (lhsT, _)), REP_thm), isodefl_thm) = + let + val Ts = snd (dest_Type lhsT); + val lhs = Library.foldl mk_capply (map_const, map ID_const Ts); + val goal = mk_eqs (lhs, ID_const lhsT); + val tac = EVERY + [rtac @{thm isodefl_REP_imp_ID} 1, + stac REP_thm 1, + rtac isodefl_thm 1, + REPEAT (rtac @{thm isodefl_ID_REP} 1)]; + in + Goal.prove_global thy [] [] goal (K tac) + end; + val map_ID_binds = map (Binding.suffix_name "_map_ID") dom_binds; + val map_ID_thms = + map prove_map_ID_thm + (map_consts ~~ dom_eqns ~~ REP_thms ~~ isodefl_thms); + val (_, thy) = thy |> + (PureThy.add_thms o map Thm.no_attributes) + (map_ID_binds ~~ map_ID_thms); + + (* define copy combinators *) + val new_dts = + map (apsnd (map (fst o dest_TFree)) o dest_Type o fst) dom_eqns; + val copy_arg_type = tupleT (map (fn (T, _) => T ->> T) dom_eqns); + val copy_args = + let fun mk_copy_args [] t = [] + | mk_copy_args (_::[]) t = [t] + | mk_copy_args (_::xs) t = + HOLogic.mk_fst t :: mk_copy_args xs (HOLogic.mk_snd t); + in mk_copy_args doms (Free ("f", copy_arg_type)) end; + fun copy_of_dtyp (T, dt) = + if DatatypeAux.is_rec_type dt + then copy_of_dtyp' (T, dt) + else ID_const T + and copy_of_dtyp' (T, DatatypeAux.DtRec i) = nth copy_args i + | copy_of_dtyp' (T, DatatypeAux.DtTFree a) = ID_const T + | copy_of_dtyp' (T as Type (_, Ts), DatatypeAux.DtType (c, ds)) = + case Symtab.lookup map_tab' c of + SOME f => + Library.foldl mk_capply + (Const (f, mapT T), map copy_of_dtyp (Ts ~~ ds)) + | NONE => + (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID_const T); + fun define_copy ((tbind, (rep_const, abs_const)), (lhsT, rhsT)) thy = + let + val copy_type = copy_arg_type ->> (lhsT ->> lhsT); + val copy_bind = Binding.suffix_name "_copy" tbind; + val (copy_const, thy) = thy |> + Sign.declare_const ((copy_bind, copy_type), NoSyn); + val dtyp = DatatypeAux.dtyp_of_typ new_dts rhsT; + val body = copy_of_dtyp (rhsT, dtyp); + val comp = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const)); + val rhs = big_lambda (Free ("f", copy_arg_type)) comp; + val eqn = Logic.mk_equals (copy_const, rhs); + val ([copy_def], thy) = + thy + |> Sign.add_path (Binding.name_of tbind) + |> (PureThy.add_defs false o map Thm.no_attributes) + [(Binding.name "copy_def", eqn)] + ||> Sign.parent_path; + in ((copy_const, copy_def), thy) end; + val ((copy_consts, copy_defs), thy) = thy + |> fold_map define_copy (dom_binds ~~ rep_abs_consts ~~ dom_eqns) + |>> ListPair.unzip; + + in + thy + end; + +val domain_isomorphism = gen_domain_isomorphism cert_typ; +val domain_isomorphism_cmd = gen_domain_isomorphism read_typ; + +(******************************************************************************) +(******************************** outer syntax ********************************) +(******************************************************************************) + +local + +structure P = OuterParse and K = OuterKeyword + +val parse_domain_iso : (string list * binding * mixfix * string) parser = + (P.type_args -- P.binding -- P.opt_infix -- (P.$$$ "=" |-- P.typ)) + >> (fn (((vs, t), mx), rhs) => (vs, t, mx, rhs)); + +val parse_domain_isos = P.and_list1 parse_domain_iso; + +in + +val _ = + OuterSyntax.command "domain_isomorphism" "define domain isomorphisms (HOLCF)" K.thy_decl + (parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd)); + +end; + +end; diff -r ccef2e6d8c21 -r f5db63bd7aee src/HOLCF/Tools/Domain/domain_syntax.ML --- a/src/HOLCF/Tools/Domain/domain_syntax.ML Fri Nov 20 00:54:20 2009 +0100 +++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Thu Nov 19 20:09:56 2009 -0800 @@ -7,12 +7,14 @@ signature DOMAIN_SYNTAX = sig val calc_syntax: + bool -> typ -> (string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list -> (binding * typ * mixfix) list * ast Syntax.trrule list val add_syntax: + bool -> string -> ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list -> @@ -27,155 +29,176 @@ infixr 5 -->; infixr 6 ->>; fun calc_syntax - (dtypeprod : typ) - ((dname : string, typevars : typ list), - (cons': (binding * (bool * binding option * typ) list * mixfix) list)) + (definitional : bool) + (dtypeprod : typ) + ((dname : string, typevars : typ list), + (cons': (binding * (bool * binding option * typ) list * mixfix) list)) : (binding * typ * mixfix) list * ast Syntax.trrule list = - let - (* ----- constants concerning the isomorphism ------------------------------- *) + let +(* ----- constants concerning the isomorphism ------------------------------- *) + local + fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t + fun prod (_,args,_) = case args of [] => oneT + | _ => 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,_) = List.foldr (op ->>) (freetvar "t") (map third args); + in + val dtype = Type(dname,typevars); + val dtype2 = foldr1 mk_ssumT (map prod cons'); + val dnam = Long_Name.base_name dname; + fun dbind s = Binding.name (dnam ^ s); + val const_rep = (dbind "_rep" , dtype ->> dtype2, NoSyn); + val const_abs = (dbind "_abs" , dtype2 ->> dtype , NoSyn); + val const_when = (dbind "_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn); + val const_copy = (dbind "_copy", dtypeprod ->> dtype ->> dtype , NoSyn); + end; - local - fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t - fun prod (_,args,_) = case args of [] => oneT - | _ => 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,_) = List.foldr (op ->>) (freetvar "t") (map third args); - in - val dtype = Type(dname,typevars); - val dtype2 = foldr1 mk_ssumT (map prod cons'); - val dnam = Long_Name.base_name dname; - fun dbind s = Binding.name (dnam ^ s); - val const_rep = (dbind "_rep" , dtype ->> dtype2, NoSyn); - val const_abs = (dbind "_abs" , dtype2 ->> dtype , NoSyn); - val const_when = (dbind "_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn); - val const_copy = (dbind "_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; - (* ----- constants concerning constructors, discriminators, and selectors --- *) + fun dis_name_ con = + Binding.name ("is_" ^ strip_esc (Binding.name_of con)); + fun mat_name_ con = + Binding.name ("match_" ^ strip_esc (Binding.name_of con)); + fun pat_name_ con = + Binding.name (strip_esc (Binding.name_of con) ^ "_pat"); + fun con (name,args,mx) = + (name, List.foldr (op ->>) dtype (map third args), mx); + fun dis (con,args,mx) = + (dis_name_ con, dtype->>trT, + Mixfix(escape ("is_" ^ Binding.name_of 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 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; - 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 dis_name_ con = Binding.name ("is_" ^ strip_esc (Binding.name_of con)); - fun mat_name_ con = Binding.name ("match_" ^ strip_esc (Binding.name_of con)); - fun pat_name_ con = Binding.name (strip_esc (Binding.name_of con) ^ "_pat"); - fun con (name,args,mx) = (name, List.foldr (op ->>) dtype (map third args), mx); - fun dis (con,args,mx) = (dis_name_ con, dtype->>trT, - Mixfix(escape ("is_" ^ Binding.name_of 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 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_matT (a,bs,c) = a ->> List.foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c; - fun mat (con,args,mx) = (mat_name_ con, - mk_matT(dtype, map third args, freetvar "t" 1), - Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri)); - fun sel1 (_,sel,typ) = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel; - fun sel (con,args,mx) = map_filter sel1 args; - 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,args,mx) = (pat_name_ con, - (mapn pat_arg_typ 1 args) - ---> - mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))), - Mixfix(escape (Binding.name_of con ^ "_pat"), [], Syntax.max_pri)); + fun mk_matT (a,bs,c) = + a ->> List.foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c; + fun mat (con,args,mx) = + (mat_name_ con, + mk_matT(dtype, map third args, freetvar "t" 1), + Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri)); + fun sel1 (_,sel,typ) = + Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel; + fun sel (con,args,mx) = map_filter sel1 args; + 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,args,mx) = + (pat_name_ con, + (mapn pat_arg_typ 1 args) + ---> + mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))), + Mixfix(escape (Binding.name_of 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 = maps sel cons'; + end; + +(* ----- constants concerning induction ------------------------------------- *) + + val const_take = (dbind "_take" , HOLogic.natT-->dtype->>dtype, NoSyn); + val const_finite = (dbind "_finite", dtype-->HOLogic.boolT , NoSyn); + +(* ----- case translation --------------------------------------------------- *) + local open Syntax in + local + fun c_ast con mx = Constant (Syntax.const_name mx (Binding.name_of con)); + 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,args,mx) = Library.foldl capp (c_ast con mx, argvars n args); + fun case1 n (con,args,mx) = app "_case1" (con1 n (con,args,mx), expvar n); + fun arg1 n (con,args,_) = List.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 "_variable") [x, Variable "rhs"]; + fun app_pat x = mk_appl (Constant "_pat") [x]; + fun args_list [] = Constant "_noargs" + | 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")); + + fun one_abscon_trans n (con,mx,args) = + ParsePrintRule + (cabs (con1 n (con,mx,args), expvar n), + Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons')); + val abscon_trans = mapn one_abscon_trans 1 cons'; + + fun one_case_trans (con,args,mx) = + let + val cname = c_ast con mx; + val pname = Constant (strip_esc (Binding.name_of con) ^ "_pat"); + 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 - 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 = maps sel cons'; - end; - - (* ----- constants concerning induction ------------------------------------- *) - - val const_take = (dbind "_take" , HOLogic.natT-->dtype->>dtype, NoSyn); - val const_finite = (dbind "_finite", dtype-->HOLogic.boolT , NoSyn); - - (* ----- case translation --------------------------------------------------- *) - - local open Syntax in - local - fun c_ast con mx = Constant (Syntax.const_name mx (Binding.name_of con)); - 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,args,mx) = Library.foldl capp (c_ast con mx, argvars n args); - fun case1 n (con,args,mx) = app "_case1" (con1 n (con,args,mx), expvar n); - fun arg1 n (con,args,_) = List.foldr cabs (expvar n) (argvars n args); - fun when1 n m = if n = m then arg1 n else K (Constant "UU"); + [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; + val Case_trans = maps one_case_trans cons'; + end; + end; + val optional_consts = + if definitional then [] else [const_rep, const_abs, const_copy]; - fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"]; - fun app_pat x = mk_appl (Constant "_pat") [x]; - fun args_list [] = Constant "_noargs" - | 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")); - - fun one_abscon_trans n (con,mx,args) = - ParsePrintRule - (cabs (con1 n (con,mx,args), expvar n), - Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons')); - val abscon_trans = mapn one_abscon_trans 1 cons'; - - fun one_case_trans (con,args,mx) = - let - val cname = c_ast con mx; - val pname = Constant (strip_esc (Binding.name_of con) ^ "_pat"); - 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; - val Case_trans = maps one_case_trans 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 *) + in (optional_consts @ [const_when] @ + 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 ------------------------------ *) fun add_syntax - (comp_dnam : string) - (eqs' : ((string * typ list) * - (binding * (bool * binding option * typ) list * mixfix) list) list) - (thy'' : theory) = - 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 = (Binding.name (comp_dnam^"_copy"), funprod ->> funprod, NoSyn); - val const_bisim = (Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn); - val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list = map (calc_syntax funprod) eqs'; - in thy'' |> ContConsts.add_consts_i (maps fst ctt @ - (if length eqs'>1 then [const_copy] else[])@ - [const_bisim]) - |> Sign.add_trrules_i (maps snd ctt) - end; (* let *) + (definitional : bool) + (comp_dnam : string) + (eqs' : ((string * typ list) * + (binding * (bool * binding option * typ) list * mixfix) list) list) + (thy'' : theory) = + 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 = + (Binding.name (comp_dnam^"_copy"), funprod ->> funprod, NoSyn); + val const_bisim = + (Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn); + val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list = + map (calc_syntax definitional funprod) eqs'; + in thy'' + |> ContConsts.add_consts_i + (maps fst ctt @ + (if length eqs'>1 then [const_copy] else[])@ + [const_bisim]) + |> Sign.add_trrules_i (maps snd ctt) + end; (* let *) end; (* struct *) diff -r ccef2e6d8c21 -r f5db63bd7aee src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Fri Nov 20 00:54:20 2009 +0100 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Nov 19 20:09:56 2009 -0800 @@ -141,6 +141,8 @@ val _ = message ("Proving isomorphism properties of domain "^dname^" ..."); val pg = pg' thy; +val map_tab = Domain_Isomorphism.get_map_tab thy; + (* ----- getting the axioms and definitions --------------------------------- *) @@ -599,7 +601,8 @@ val lhs = dc_copy`%"f"`(con_app con args); fun one_rhs arg = if DatatypeAux.is_rec_type (dtyp_of arg) - then Domain_Axioms.copy_of_dtyp (proj (%:"f") eqs) (dtyp_of arg) ` (%# arg) + then Domain_Axioms.copy_of_dtyp map_tab + (proj (%:"f") eqs) (dtyp_of arg) ` (%# arg) else (%# arg); val rhs = con_app2 con one_rhs args; val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs)); @@ -660,6 +663,7 @@ fun comp_theorems (comp_dnam, eqs: eq list) thy = let val global_ctxt = ProofContext.init thy; +val map_tab = Domain_Isomorphism.get_map_tab thy; val dnames = map (fst o fst) eqs; val conss = map snd eqs; @@ -727,7 +731,8 @@ fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n"; fun one_rhs arg = if DatatypeAux.is_rec_type (dtyp_of arg) - then Domain_Axioms.copy_of_dtyp mk_take (dtyp_of arg) ` (%# arg) + then Domain_Axioms.copy_of_dtyp map_tab + mk_take (dtyp_of arg) ` (%# arg) else (%# arg); val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args); val rhs = con_app2 con one_rhs args; diff -r ccef2e6d8c21 -r f5db63bd7aee src/HOLCF/ex/Domain_Proofs.thy --- a/src/HOLCF/ex/Domain_Proofs.thy Fri Nov 20 00:54:20 2009 +0100 +++ b/src/HOLCF/ex/Domain_Proofs.thy Thu Nov 19 20:09:56 2009 -0800 @@ -16,8 +16,8 @@ datatypes: domain 'a foo = Foo1 | Foo2 (lazy 'a) (lazy "'a bar") - and 'a bar = Bar (lazy 'a) (lazy "'a baz") - and 'a baz = Baz (lazy 'a) (lazy "'a foo convex_pd") + and 'a bar = Bar (lazy "'a baz \ tr") + and 'a baz = Baz (lazy "'a foo convex_pd \ tr") *) @@ -28,47 +28,47 @@ text {* Start with the one-step non-recursive version *} definition - foo_bar_baz_typF :: + foo_bar_baz_deflF :: "TypeRep \ TypeRep \ TypeRep \ TypeRep \ TypeRep \ TypeRep \ TypeRep" where - "foo_bar_baz_typF = (\ a (t1, t2, t3). - ( ssum_typ\one_typ\(sprod_typ\(u_typ\a)\(u_typ\t2)) - , sprod_typ\(u_typ\a)\(u_typ\t3) - , sprod_typ\(u_typ\a)\(u_typ\(convex_typ\t1))))" + "foo_bar_baz_deflF = (\ a. Abs_CFun (\(t1, t2, t3). + ( ssum_defl\REP(one)\(sprod_defl\(u_defl\a)\(u_defl\t2)) + , u_defl\(cfun_defl\t3\REP(tr)) + , u_defl\(cfun_defl\(convex_defl\t1)\REP(tr)))))" -lemma foo_bar_baz_typF_beta: - "foo_bar_baz_typF\a\t = - ( ssum_typ\one_typ\(sprod_typ\(u_typ\a)\(u_typ\(fst (snd t)))) - , sprod_typ\(u_typ\a)\(u_typ\(snd (snd t))) - , sprod_typ\(u_typ\a)\(u_typ\(convex_typ\(fst t))))" -unfolding foo_bar_baz_typF_def -by (simp add: csplit_def cfst_def csnd_def) +lemma foo_bar_baz_deflF_beta: + "foo_bar_baz_deflF\a\t = + ( ssum_defl\REP(one)\(sprod_defl\(u_defl\a)\(u_defl\(fst (snd t)))) + , u_defl\(cfun_defl\(snd (snd t))\REP(tr)) + , u_defl\(cfun_defl\(convex_defl\(fst t))\REP(tr)))" +unfolding foo_bar_baz_deflF_def +by (simp add: split_def) text {* Individual type combinators are projected from the fixed point. *} -definition foo_typ :: "TypeRep \ TypeRep" -where "foo_typ = (\ a. fst (fix\(foo_bar_baz_typF\a)))" +definition foo_defl :: "TypeRep \ TypeRep" +where "foo_defl = (\ a. fst (fix\(foo_bar_baz_deflF\a)))" -definition bar_typ :: "TypeRep \ TypeRep" -where "bar_typ = (\ a. fst (snd (fix\(foo_bar_baz_typF\a))))" +definition bar_defl :: "TypeRep \ TypeRep" +where "bar_defl = (\ a. fst (snd (fix\(foo_bar_baz_deflF\a))))" -definition baz_typ :: "TypeRep \ TypeRep" -where "baz_typ = (\ a. snd (snd (fix\(foo_bar_baz_typF\a))))" +definition baz_defl :: "TypeRep \ TypeRep" +where "baz_defl = (\ a. snd (snd (fix\(foo_bar_baz_deflF\a))))" text {* Unfold rules for each combinator. *} -lemma foo_typ_unfold: - "foo_typ\a = ssum_typ\one_typ\(sprod_typ\(u_typ\a)\(u_typ\(bar_typ\a)))" -unfolding foo_typ_def bar_typ_def baz_typ_def -by (subst fix_eq, simp add: foo_bar_baz_typF_beta) +lemma foo_defl_unfold: + "foo_defl\a = ssum_defl\REP(one)\(sprod_defl\(u_defl\a)\(u_defl\(bar_defl\a)))" +unfolding foo_defl_def bar_defl_def baz_defl_def +by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) -lemma bar_typ_unfold: "bar_typ\a = sprod_typ\(u_typ\a)\(u_typ\(baz_typ\a))" -unfolding foo_typ_def bar_typ_def baz_typ_def -by (subst fix_eq, simp add: foo_bar_baz_typF_beta) +lemma bar_defl_unfold: "bar_defl\a = u_defl\(cfun_defl\(baz_defl\a)\REP(tr))" +unfolding foo_defl_def bar_defl_def baz_defl_def +by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) -lemma baz_typ_unfold: "baz_typ\a = sprod_typ\(u_typ\a)\(u_typ\(convex_typ\(foo_typ\a)))" -unfolding foo_typ_def bar_typ_def baz_typ_def -by (subst fix_eq, simp add: foo_bar_baz_typF_beta) +lemma baz_defl_unfold: "baz_defl\a = u_defl\(cfun_defl\(convex_defl\(foo_defl\a))\REP(tr))" +unfolding foo_defl_def bar_defl_def baz_defl_def +by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) text "The automation for the previous steps will be quite similar to how the fixrec package works." @@ -79,13 +79,13 @@ text {* Use @{text pcpodef} with the appropriate type combinator. *} -pcpodef (open) 'a foo = "{x. x ::: foo_typ\REP('a)}" +pcpodef (open) 'a foo = "{x. x ::: foo_defl\REP('a)}" by (simp_all add: adm_in_deflation) -pcpodef (open) 'a bar = "{x. x ::: bar_typ\REP('a)}" +pcpodef (open) 'a bar = "{x. x ::: bar_defl\REP('a)}" by (simp_all add: adm_in_deflation) -pcpodef (open) 'a baz = "{x. x ::: baz_typ\REP('a)}" +pcpodef (open) 'a baz = "{x. x ::: baz_defl\REP('a)}" by (simp_all add: adm_in_deflation) text {* Prove rep instance using lemma @{text typedef_rep_class}. *} @@ -97,10 +97,10 @@ 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_defl\REP('a))\y))" definition approx_foo :: "nat \ 'a foo \ 'a foo" -where "approx_foo \ repdef_approx Rep_foo Abs_foo (foo_typ\REP('a))" +where "approx_foo \ repdef_approx Rep_foo Abs_foo (foo_defl\REP('a))" instance apply (rule typedef_rep_class) @@ -120,10 +120,10 @@ 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_defl\REP('a))\y))" definition approx_bar :: "nat \ 'a bar \ 'a bar" -where "approx_bar \ repdef_approx Rep_bar Abs_bar (bar_typ\REP('a))" +where "approx_bar \ repdef_approx Rep_bar Abs_bar (bar_defl\REP('a))" instance apply (rule typedef_rep_class) @@ -143,10 +143,10 @@ 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_defl\REP('a))\y))" definition approx_baz :: "nat \ 'a baz \ 'a baz" -where "approx_baz \ repdef_approx Rep_baz Abs_baz (baz_typ\REP('a))" +where "approx_baz \ repdef_approx Rep_baz Abs_baz (baz_defl\REP('a))" instance apply (rule typedef_rep_class) @@ -161,7 +161,7 @@ text {* Prove REP rules using lemma @{text typedef_REP}. *} -lemma REP_foo: "REP('a foo) = foo_typ\REP('a)" +lemma REP_foo: "REP('a foo) = foo_defl\REP('a)" apply (rule typedef_REP) apply (rule type_definition_foo) apply (rule below_foo_def) @@ -169,7 +169,7 @@ apply (rule prj_foo_def) done -lemma REP_bar: "REP('a bar) = bar_typ\REP('a)" +lemma REP_bar: "REP('a bar) = bar_defl\REP('a)" apply (rule typedef_REP) apply (rule type_definition_bar) apply (rule below_bar_def) @@ -177,7 +177,7 @@ apply (rule prj_bar_def) done -lemma REP_baz: "REP('a baz) = baz_typ\REP('a)" +lemma REP_baz: "REP('a baz) = baz_defl\REP('a)" apply (rule typedef_REP) apply (rule type_definition_baz) apply (rule below_baz_def) @@ -189,15 +189,15 @@ lemma REP_foo': "REP('a foo) = REP(one \ 'a\<^sub>\ \ ('a bar)\<^sub>\)" unfolding REP_foo REP_bar REP_baz REP_simps -by (rule foo_typ_unfold) +by (rule foo_defl_unfold) -lemma REP_bar': "REP('a bar) = REP('a\<^sub>\ \ ('a baz)\<^sub>\)" +lemma REP_bar': "REP('a bar) = REP(('a baz \ tr)\<^sub>\)" unfolding REP_foo REP_bar REP_baz REP_simps -by (rule bar_typ_unfold) +by (rule bar_defl_unfold) -lemma REP_baz': "REP('a baz) = REP('a\<^sub>\ \ ('a foo convex_pd)\<^sub>\)" +lemma REP_baz': "REP('a baz) = REP(('a foo convex_pd \ tr)\<^sub>\)" unfolding REP_foo REP_bar REP_baz REP_simps -by (rule baz_typ_unfold) +by (rule baz_defl_unfold) (********************************************************************) @@ -206,41 +206,56 @@ text {* Define them all using @{text coerce}! *} definition foo_rep :: "'a foo \ one \ ('a\<^sub>\ \ ('a bar)\<^sub>\)" -where "foo_rep = coerce" +where "foo_rep \ coerce" definition foo_abs :: "one \ ('a\<^sub>\ \ ('a bar)\<^sub>\) \ 'a foo" -where "foo_abs = coerce" +where "foo_abs \ coerce" + +definition bar_rep :: "'a bar \ ('a baz \ tr)\<^sub>\" +where "bar_rep \ coerce" + +definition bar_abs :: "('a baz \ tr)\<^sub>\ \ 'a bar" +where "bar_abs \ coerce" -definition bar_rep :: "'a bar \ 'a\<^sub>\ \ ('a baz)\<^sub>\" -where "bar_rep = coerce" +definition baz_rep :: "'a baz \ ('a foo convex_pd \ tr)\<^sub>\" +where "baz_rep \ coerce" + +definition baz_abs :: "('a foo convex_pd \ tr)\<^sub>\ \ 'a baz" +where "baz_abs \ coerce" + +text {* Prove isomorphism rules. *} -definition bar_abs :: "'a\<^sub>\ \ ('a baz)\<^sub>\ \ 'a bar" -where "bar_abs = coerce" +lemma foo_abs_iso: "foo_rep\(foo_abs\x) = x" +by (rule domain_abs_iso [OF REP_foo' foo_abs_def foo_rep_def]) + +lemma foo_rep_iso: "foo_abs\(foo_rep\x) = x" +by (rule domain_rep_iso [OF REP_foo' foo_abs_def foo_rep_def]) + +lemma bar_abs_iso: "bar_rep\(bar_abs\x) = x" +by (rule domain_abs_iso [OF REP_bar' bar_abs_def bar_rep_def]) -definition baz_rep :: "'a baz \ 'a\<^sub>\ \ ('a foo convex_pd)\<^sub>\" -where "baz_rep = coerce" +lemma bar_rep_iso: "bar_abs\(bar_rep\x) = x" +by (rule domain_rep_iso [OF REP_bar' bar_abs_def bar_rep_def]) -definition baz_abs :: "'a\<^sub>\ \ ('a foo convex_pd)\<^sub>\ \ 'a baz" -where "baz_abs = coerce" +lemma baz_abs_iso: "baz_rep\(baz_abs\x) = x" +by (rule domain_abs_iso [OF REP_baz' baz_abs_def baz_rep_def]) + +lemma baz_rep_iso: "baz_abs\(baz_rep\x) = x" +by (rule domain_rep_iso [OF REP_baz' baz_abs_def baz_rep_def]) text {* Prove isodefl rules using @{text isodefl_coerce}. *} lemma isodefl_foo_abs: "isodefl d t \ isodefl (foo_abs oo d oo foo_rep) t" -unfolding foo_abs_def foo_rep_def -by (rule isodefl_coerce [OF REP_foo']) +by (rule isodefl_abs_rep [OF REP_foo' foo_abs_def foo_rep_def]) lemma isodefl_bar_abs: "isodefl d t \ isodefl (bar_abs oo d oo bar_rep) t" -unfolding bar_abs_def bar_rep_def -by (rule isodefl_coerce [OF REP_bar']) +by (rule isodefl_abs_rep [OF REP_bar' bar_abs_def bar_rep_def]) lemma isodefl_baz_abs: "isodefl d t \ isodefl (baz_abs oo d oo baz_rep) t" -unfolding baz_abs_def baz_rep_def -by (rule isodefl_coerce [OF REP_baz']) - -text {* TODO: prove iso predicate for rep and abs. *} +by (rule isodefl_abs_rep [OF REP_baz' baz_abs_def baz_rep_def]) (********************************************************************) @@ -253,20 +268,20 @@ definition foo_bar_baz_mapF :: - "('a \ 'b) - \ ('a foo \ 'b foo) \ ('a bar \ 'b bar) \ ('a baz \ 'b baz) - \ ('a foo \ 'b foo) \ ('a bar \ 'b bar) \ ('a baz \ 'b baz)" + "('a \ 'b) \ + ('a foo \ 'b foo) \ ('a bar \ 'b bar) \ ('b baz \ 'a baz) \ + ('a foo \ 'b foo) \ ('a bar \ 'b bar) \ ('b baz \ 'a baz)" where - "foo_bar_baz_mapF = (\ f (d1, d2, d3). + "foo_bar_baz_mapF = (\ f. Abs_CFun (\(d1, d2, d3). ( foo_abs oo ssum_map\ID\(sprod_map\(u_map\f)\(u_map\d2)) oo foo_rep , - bar_abs oo sprod_map\(u_map\f)\(u_map\d3) oo bar_rep + bar_abs oo u_map\(cfun_map\d3\ID) oo bar_rep , - baz_abs oo sprod_map\(u_map\f)\(u_map\(convex_map\d1)) oo baz_rep - ))" + baz_abs oo u_map\(cfun_map\(convex_map\d1)\ID) oo baz_rep + )))" lemma foo_bar_baz_mapF_beta: "foo_bar_baz_mapF\f\d = @@ -275,12 +290,12 @@ ssum_map\ID\(sprod_map\(u_map\f)\(u_map\(fst (snd d)))) oo foo_rep , - bar_abs oo sprod_map\(u_map\f)\(u_map\(snd (snd d))) oo bar_rep + bar_abs oo u_map\(cfun_map\(snd (snd d))\ID) oo bar_rep , - baz_abs oo sprod_map\(u_map\f)\(u_map\(convex_map\(fst d))) oo baz_rep + baz_abs oo u_map\(cfun_map\(convex_map\(fst d))\ID) oo baz_rep )" unfolding foo_bar_baz_mapF_def -by (simp add: csplit_def cfst_def csnd_def) +by (simp add: split_def) text {* Individual map functions are projected from the fixed point. *} @@ -290,7 +305,7 @@ definition bar_map :: "('a \ 'b) \ ('a bar \ 'b bar)" where "bar_map = (\ f. fst (snd (fix\(foo_bar_baz_mapF\f))))" -definition baz_map :: "('a \ 'b) \ ('a baz \ 'b baz)" +definition baz_map :: "('a \ 'b) \ ('b baz \ 'a baz)" where "baz_map = (\ f. snd (snd (fix\(foo_bar_baz_mapF\f))))" text {* Prove isodefl rules for all map functions simultaneously. *} @@ -298,17 +313,16 @@ lemma isodefl_foo_bar_baz: assumes isodefl_d: "isodefl d t" shows - "isodefl (foo_map\d) (foo_typ\t) \ - isodefl (bar_map\d) (bar_typ\t) \ - isodefl (baz_map\d) (baz_typ\t)" + "isodefl (foo_map\d) (foo_defl\t) \ + isodefl (bar_map\d) (bar_defl\t) \ + isodefl (baz_map\d) (baz_defl\t)" apply (simp add: foo_map_def bar_map_def baz_map_def) - apply (simp add: foo_typ_def bar_typ_def baz_typ_def) - apply (rule parallel_fix_ind - [where F="foo_bar_baz_typF\t" and G="foo_bar_baz_mapF\d"]) + apply (simp add: foo_defl_def bar_defl_def baz_defl_def) + apply (rule parallel_fix_ind) apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id) apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms) apply (simp only: foo_bar_baz_mapF_beta - foo_bar_baz_typF_beta + foo_bar_baz_deflF_beta fst_conv snd_conv) apply (elim conjE) apply (intro @@ -316,7 +330,8 @@ isodefl_foo_abs isodefl_bar_abs isodefl_baz_abs - isodefl_ssum isodefl_sprod isodefl_one isodefl_u isodefl_convex + isodefl_ssum isodefl_sprod isodefl_ID_REP + isodefl_u isodefl_convex isodefl_cfun isodefl_d ) apply assumption+ @@ -353,23 +368,63 @@ subsection {* Step 5: Define copy functions, prove reach lemmas *} -definition "foo_bar_baz_copy = foo_bar_baz_mapF\ID" -definition "foo_copy = (\ f. fst (foo_bar_baz_copy\f))" -definition "bar_copy = (\ f. fst (snd (foo_bar_baz_copy\f)))" -definition "baz_copy = (\ f. snd (snd (foo_bar_baz_copy\f)))" +text {* Define copy functions just like the old domain package does. *} + +definition + foo_copy :: + "('a foo \ 'a foo) \ ('a bar \ 'a bar) \ ('a baz \ 'a baz) \ + 'a foo \ 'a foo" +where + "foo_copy = (\ p. foo_abs oo + ssum_map\ID\(sprod_map\(u_map\ID)\(u_map\(fst (snd p)))) + oo foo_rep)" + +definition + bar_copy :: + "('a foo \ 'a foo) \ ('a bar \ 'a bar) \ ('a baz \ 'a baz) \ + 'a bar \ 'a bar" +where + "bar_copy = (\ p. bar_abs oo + u_map\(cfun_map\(snd (snd p))\ID) oo bar_rep)" + +definition + baz_copy :: + "('a foo \ 'a foo) \ ('a bar \ 'a bar) \ ('a baz \ 'a baz) \ + 'a baz \ 'a baz" +where + "baz_copy = (\ p. baz_abs oo + u_map\(cfun_map\(convex_map\(fst p))\ID) oo baz_rep)" + +definition + foo_bar_baz_copy :: + "('a foo \ 'a foo) \ ('a bar \ 'a bar) \ ('a baz \ 'a baz) \ + ('a foo \ 'a foo) \ ('a bar \ 'a bar) \ ('a baz \ 'a baz)" +where + "foo_bar_baz_copy = (\ f. (foo_copy\f, bar_copy\f, baz_copy\f))" lemma fix_foo_bar_baz_copy: "fix\foo_bar_baz_copy = (foo_map\ID, bar_map\ID, baz_map\ID)" -unfolding foo_bar_baz_copy_def foo_map_def bar_map_def baz_map_def -by simp +unfolding foo_map_def bar_map_def baz_map_def +apply (subst beta_cfun, simp)+ +apply (subst pair_collapse)+ +apply (rule cfun_arg_cong) +unfolding foo_bar_baz_mapF_def split_def +unfolding foo_bar_baz_copy_def +unfolding foo_copy_def bar_copy_def baz_copy_def +apply (subst beta_cfun, simp)+ +apply (rule refl) +done lemma foo_reach: "fst (fix\foo_bar_baz_copy)\x = x" -unfolding fix_foo_bar_baz_copy by (simp add: foo_map_ID) +unfolding fix_foo_bar_baz_copy fst_conv snd_conv +unfolding foo_map_ID by (rule ID1) lemma bar_reach: "fst (snd (fix\foo_bar_baz_copy))\x = x" -unfolding fix_foo_bar_baz_copy by (simp add: bar_map_ID) +unfolding fix_foo_bar_baz_copy fst_conv snd_conv +unfolding bar_map_ID by (rule ID1) lemma baz_reach: "snd (snd (fix\foo_bar_baz_copy))\x = x" -unfolding fix_foo_bar_baz_copy by (simp add: baz_map_ID) +unfolding fix_foo_bar_baz_copy fst_conv snd_conv +unfolding baz_map_ID by (rule ID1) end