--- 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")
--- 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
--- 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 \<equiv> (coerce :: 'a \<rightarrow> 'b)"
+ assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
+ shows "rep\<cdot>(abs\<cdot>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 \<equiv> (coerce :: 'a \<rightarrow> 'b)"
+ assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
+ shows "abs\<cdot>(rep\<cdot>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\<cdot>(Rep_fin_defl a)\<cdot>(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 \<sqsubseteq> b \<Longrightarrow> Rep_fin_defl a \<sqsubseteq> 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\<cdot>(cfun_typ\<cdot>A\<cdot>B) = udom_emb oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
-unfolding cfun_typ_def
+lemma cast_cfun_defl:
+ "cast\<cdot>(cfun_defl\<cdot>A\<cdot>B) = udom_emb oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>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\<cdot>(ssum_typ\<cdot>A\<cdot>B) = udom_emb oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
-unfolding ssum_typ_def
+lemma cast_ssum_defl:
+ "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) = udom_emb oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>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\<cdot>(sprod_typ\<cdot>A\<cdot>B) = udom_emb oo sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
-unfolding sprod_typ_def
+lemma cast_sprod_defl:
+ "cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) = udom_emb oo sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>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\<cdot>(cprod_typ\<cdot>A\<cdot>B) = udom_emb oo cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
-unfolding cprod_typ_def
+lemma cast_cprod_defl:
+ "cast\<cdot>(cprod_defl\<cdot>A\<cdot>B) = udom_emb oo cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>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\<cdot>(u_typ\<cdot>A) = udom_emb oo u_map\<cdot>(cast\<cdot>A) oo udom_prj"
-unfolding u_typ_def
+lemma cast_u_defl:
+ "cast\<cdot>(u_defl\<cdot>A) = udom_emb oo u_map\<cdot>(cast\<cdot>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\<cdot>(upper_typ\<cdot>A) = udom_emb oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj"
-unfolding upper_typ_def
+lemma cast_upper_defl:
+ "cast\<cdot>(upper_defl\<cdot>A) = udom_emb oo upper_map\<cdot>(cast\<cdot>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\<cdot>(lower_typ\<cdot>A) = udom_emb oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj"
-unfolding lower_typ_def
+lemma cast_lower_defl:
+ "cast\<cdot>(lower_defl\<cdot>A) = udom_emb oo lower_map\<cdot>(cast\<cdot>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\<cdot>(convex_typ\<cdot>A) = udom_emb oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj"
-unfolding convex_typ_def
+lemma cast_convex_defl:
+ "cast\<cdot>(convex_defl\<cdot>A) = udom_emb oo convex_map\<cdot>(cast\<cdot>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 \<rightarrow> 'b) = cfun_typ\<cdot>REP('a)\<cdot>REP('b)"
+lemma REP_cfun: "REP('a \<rightarrow> 'b) = cfun_defl\<cdot>REP('a)\<cdot>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 \<oplus> 'b) = ssum_typ\<cdot>REP('a)\<cdot>REP('b)"
+lemma REP_ssum: "REP('a \<oplus> 'b) = ssum_defl\<cdot>REP('a)\<cdot>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 \<otimes> 'b) = sprod_typ\<cdot>REP('a)\<cdot>REP('b)"
+lemma REP_sprod: "REP('a \<otimes> 'b) = sprod_defl\<cdot>REP('a)\<cdot>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 \<times> 'b) = cprod_typ\<cdot>REP('a)\<cdot>REP('b)"
+lemma REP_cprod: "REP('a \<times> 'b) = cprod_defl\<cdot>REP('a)\<cdot>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\<cdot>REP('a)"
+lemma REP_up: "REP('a u) = u_defl\<cdot>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\<cdot>REP('a)"
+lemma REP_upper: "REP('a upper_pd) = upper_defl\<cdot>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\<cdot>REP('a)"
+lemma REP_lower: "REP('a lower_pd) = lower_defl\<cdot>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\<cdot>REP('a)"
+lemma REP_convex: "REP('a convex_pd) = convex_defl\<cdot>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 \<equiv> (coerce :: 'a \<rightarrow> 'b)"
+ assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
+ shows "isodefl d t \<Longrightarrow> isodefl (abs oo d oo rep) t"
+unfolding abs_def rep_def using REP by (rule isodefl_coerce)
+
lemma isodefl_cfun:
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
- isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_typ\<cdot>t1\<cdot>t2)"
+ isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_defl\<cdot>t1\<cdot>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 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
- isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_typ\<cdot>t1\<cdot>t2)"
+ isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_defl\<cdot>t1\<cdot>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 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
- isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_typ\<cdot>t1\<cdot>t2)"
+ isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_defl\<cdot>t1\<cdot>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 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
+ isodefl (cprod_map\<cdot>d1\<cdot>d2) (cprod_defl\<cdot>t1\<cdot>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 \<Longrightarrow> isodefl (u_map\<cdot>d) (u_typ\<cdot>t)"
+ "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>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 \<rightarrow> one) one_typ"
-unfolding one_typ_def by (rule isodefl_ID_REP)
-
-lemma isodefl_tr: "isodefl (ID :: tr \<rightarrow> tr) tr_typ"
-unfolding tr_typ_def by (rule isodefl_ID_REP)
-
lemma isodefl_upper:
- "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_typ\<cdot>t)"
+ "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>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 \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_typ\<cdot>t)"
+ "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>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 \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_typ\<cdot>t)"
+ "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>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
--- 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 *)
--- 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;
--- /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;
--- 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 *)
--- 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;
--- 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 \<rightarrow> tr")
+ and 'a baz = Baz (lazy "'a foo convex_pd \<rightarrow> tr")
*)
@@ -28,47 +28,47 @@
text {* Start with the one-step non-recursive version *}
definition
- foo_bar_baz_typF ::
+ foo_bar_baz_deflF ::
"TypeRep \<rightarrow> TypeRep \<times> TypeRep \<times> TypeRep \<rightarrow> TypeRep \<times> TypeRep \<times> TypeRep"
where
- "foo_bar_baz_typF = (\<Lambda> a (t1, t2, t3).
- ( ssum_typ\<cdot>one_typ\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>t2))
- , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>t3)
- , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>t1))))"
+ "foo_bar_baz_deflF = (\<Lambda> a. Abs_CFun (\<lambda>(t1, t2, t3).
+ ( ssum_defl\<cdot>REP(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t2))
+ , u_defl\<cdot>(cfun_defl\<cdot>t3\<cdot>REP(tr))
+ , u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>t1)\<cdot>REP(tr)))))"
-lemma foo_bar_baz_typF_beta:
- "foo_bar_baz_typF\<cdot>a\<cdot>t =
- ( ssum_typ\<cdot>one_typ\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(fst (snd t))))
- , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(snd (snd t)))
- , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>(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\<cdot>a\<cdot>t =
+ ( ssum_defl\<cdot>REP(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(fst (snd t))))
+ , u_defl\<cdot>(cfun_defl\<cdot>(snd (snd t))\<cdot>REP(tr))
+ , u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(fst t))\<cdot>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 \<rightarrow> TypeRep"
-where "foo_typ = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_typF\<cdot>a)))"
+definition foo_defl :: "TypeRep \<rightarrow> TypeRep"
+where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
-definition bar_typ :: "TypeRep \<rightarrow> TypeRep"
-where "bar_typ = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_typF\<cdot>a))))"
+definition bar_defl :: "TypeRep \<rightarrow> TypeRep"
+where "bar_defl = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
-definition baz_typ :: "TypeRep \<rightarrow> TypeRep"
-where "baz_typ = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_typF\<cdot>a))))"
+definition baz_defl :: "TypeRep \<rightarrow> TypeRep"
+where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
text {* Unfold rules for each combinator. *}
-lemma foo_typ_unfold:
- "foo_typ\<cdot>a = ssum_typ\<cdot>one_typ\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(bar_typ\<cdot>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\<cdot>a = ssum_defl\<cdot>REP(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(bar_defl\<cdot>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\<cdot>a = sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(baz_typ\<cdot>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\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(baz_defl\<cdot>a)\<cdot>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\<cdot>a = sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>(foo_typ\<cdot>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\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a))\<cdot>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\<cdot>REP('a)}"
+pcpodef (open) 'a foo = "{x. x ::: foo_defl\<cdot>REP('a)}"
by (simp_all add: adm_in_deflation)
-pcpodef (open) 'a bar = "{x. x ::: bar_typ\<cdot>REP('a)}"
+pcpodef (open) 'a bar = "{x. x ::: bar_defl\<cdot>REP('a)}"
by (simp_all add: adm_in_deflation)
-pcpodef (open) 'a baz = "{x. x ::: baz_typ\<cdot>REP('a)}"
+pcpodef (open) 'a baz = "{x. x ::: baz_defl\<cdot>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 \<equiv> (\<Lambda> x. Rep_foo x)"
definition prj_foo :: "udom \<rightarrow> 'a foo"
-where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_typ\<cdot>REP('a))\<cdot>y))"
+where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>REP('a))\<cdot>y))"
definition approx_foo :: "nat \<Rightarrow> 'a foo \<rightarrow> 'a foo"
-where "approx_foo \<equiv> repdef_approx Rep_foo Abs_foo (foo_typ\<cdot>REP('a))"
+where "approx_foo \<equiv> repdef_approx Rep_foo Abs_foo (foo_defl\<cdot>REP('a))"
instance
apply (rule typedef_rep_class)
@@ -120,10 +120,10 @@
where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)"
definition prj_bar :: "udom \<rightarrow> 'a bar"
-where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_typ\<cdot>REP('a))\<cdot>y))"
+where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>REP('a))\<cdot>y))"
definition approx_bar :: "nat \<Rightarrow> 'a bar \<rightarrow> 'a bar"
-where "approx_bar \<equiv> repdef_approx Rep_bar Abs_bar (bar_typ\<cdot>REP('a))"
+where "approx_bar \<equiv> repdef_approx Rep_bar Abs_bar (bar_defl\<cdot>REP('a))"
instance
apply (rule typedef_rep_class)
@@ -143,10 +143,10 @@
where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)"
definition prj_baz :: "udom \<rightarrow> 'a baz"
-where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_typ\<cdot>REP('a))\<cdot>y))"
+where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>REP('a))\<cdot>y))"
definition approx_baz :: "nat \<Rightarrow> 'a baz \<rightarrow> 'a baz"
-where "approx_baz \<equiv> repdef_approx Rep_baz Abs_baz (baz_typ\<cdot>REP('a))"
+where "approx_baz \<equiv> repdef_approx Rep_baz Abs_baz (baz_defl\<cdot>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\<cdot>REP('a)"
+lemma REP_foo: "REP('a foo) = foo_defl\<cdot>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\<cdot>REP('a)"
+lemma REP_bar: "REP('a bar) = bar_defl\<cdot>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\<cdot>REP('a)"
+lemma REP_baz: "REP('a baz) = baz_defl\<cdot>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 \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
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>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom>)"
+lemma REP_bar': "REP('a bar) = REP(('a baz \<rightarrow> tr)\<^sub>\<bottom>)"
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>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom>)"
+lemma REP_baz': "REP('a baz) = REP(('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>)"
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 \<rightarrow> one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
-where "foo_rep = coerce"
+where "foo_rep \<equiv> coerce"
definition foo_abs :: "one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>) \<rightarrow> 'a foo"
-where "foo_abs = coerce"
+where "foo_abs \<equiv> coerce"
+
+definition bar_rep :: "'a bar \<rightarrow> ('a baz \<rightarrow> tr)\<^sub>\<bottom>"
+where "bar_rep \<equiv> coerce"
+
+definition bar_abs :: "('a baz \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a bar"
+where "bar_abs \<equiv> coerce"
-definition bar_rep :: "'a bar \<rightarrow> 'a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom>"
-where "bar_rep = coerce"
+definition baz_rep :: "'a baz \<rightarrow> ('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>"
+where "baz_rep \<equiv> coerce"
+
+definition baz_abs :: "('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a baz"
+where "baz_abs \<equiv> coerce"
+
+text {* Prove isomorphism rules. *}
-definition bar_abs :: "'a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom> \<rightarrow> 'a bar"
-where "bar_abs = coerce"
+lemma foo_abs_iso: "foo_rep\<cdot>(foo_abs\<cdot>x) = x"
+by (rule domain_abs_iso [OF REP_foo' foo_abs_def foo_rep_def])
+
+lemma foo_rep_iso: "foo_abs\<cdot>(foo_rep\<cdot>x) = x"
+by (rule domain_rep_iso [OF REP_foo' foo_abs_def foo_rep_def])
+
+lemma bar_abs_iso: "bar_rep\<cdot>(bar_abs\<cdot>x) = x"
+by (rule domain_abs_iso [OF REP_bar' bar_abs_def bar_rep_def])
-definition baz_rep :: "'a baz \<rightarrow> 'a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom>"
-where "baz_rep = coerce"
+lemma bar_rep_iso: "bar_abs\<cdot>(bar_rep\<cdot>x) = x"
+by (rule domain_rep_iso [OF REP_bar' bar_abs_def bar_rep_def])
-definition baz_abs :: "'a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom> \<rightarrow> 'a baz"
-where "baz_abs = coerce"
+lemma baz_abs_iso: "baz_rep\<cdot>(baz_abs\<cdot>x) = x"
+by (rule domain_abs_iso [OF REP_baz' baz_abs_def baz_rep_def])
+
+lemma baz_rep_iso: "baz_abs\<cdot>(baz_rep\<cdot>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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<rightarrow> 'b)
- \<rightarrow> ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('a baz \<rightarrow> 'b baz)
- \<rightarrow> ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('a baz \<rightarrow> 'b baz)"
+ "('a \<rightarrow> 'b) \<rightarrow>
+ ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz) \<rightarrow>
+ ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz)"
where
- "foo_bar_baz_mapF = (\<Lambda> f (d1, d2, d3).
+ "foo_bar_baz_mapF = (\<Lambda> f. Abs_CFun (\<lambda>(d1, d2, d3).
(
foo_abs oo
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d2))
oo foo_rep
,
- bar_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d3) oo bar_rep
+ bar_abs oo u_map\<cdot>(cfun_map\<cdot>d3\<cdot>ID) oo bar_rep
,
- baz_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(convex_map\<cdot>d1)) oo baz_rep
- ))"
+ baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>d1)\<cdot>ID) oo baz_rep
+ )))"
lemma foo_bar_baz_mapF_beta:
"foo_bar_baz_mapF\<cdot>f\<cdot>d =
@@ -275,12 +290,12 @@
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(fst (snd d))))
oo foo_rep
,
- bar_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(snd (snd d))) oo bar_rep
+ bar_abs oo u_map\<cdot>(cfun_map\<cdot>(snd (snd d))\<cdot>ID) oo bar_rep
,
- baz_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(convex_map\<cdot>(fst d))) oo baz_rep
+ baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst d))\<cdot>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 \<rightarrow> 'b) \<rightarrow> ('a bar \<rightarrow> 'b bar)"
where "bar_map = (\<Lambda> f. fst (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))"
-definition baz_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a baz \<rightarrow> 'b baz)"
+definition baz_map :: "('a \<rightarrow> 'b) \<rightarrow> ('b baz \<rightarrow> 'a baz)"
where "baz_map = (\<Lambda> f. snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>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\<cdot>d) (foo_typ\<cdot>t) \<and>
- isodefl (bar_map\<cdot>d) (bar_typ\<cdot>t) \<and>
- isodefl (baz_map\<cdot>d) (baz_typ\<cdot>t)"
+ "isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and>
+ isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and>
+ isodefl (baz_map\<cdot>d) (baz_defl\<cdot>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\<cdot>t" and G="foo_bar_baz_mapF\<cdot>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\<cdot>ID"
-definition "foo_copy = (\<Lambda> f. fst (foo_bar_baz_copy\<cdot>f))"
-definition "bar_copy = (\<Lambda> f. fst (snd (foo_bar_baz_copy\<cdot>f)))"
-definition "baz_copy = (\<Lambda> f. snd (snd (foo_bar_baz_copy\<cdot>f)))"
+text {* Define copy functions just like the old domain package does. *}
+
+definition
+ foo_copy ::
+ "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
+ 'a foo \<rightarrow> 'a foo"
+where
+ "foo_copy = (\<Lambda> p. foo_abs oo
+ ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p))))
+ oo foo_rep)"
+
+definition
+ bar_copy ::
+ "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
+ 'a bar \<rightarrow> 'a bar"
+where
+ "bar_copy = (\<Lambda> p. bar_abs oo
+ u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep)"
+
+definition
+ baz_copy ::
+ "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
+ 'a baz \<rightarrow> 'a baz"
+where
+ "baz_copy = (\<Lambda> p. baz_abs oo
+ u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep)"
+
+definition
+ foo_bar_baz_copy ::
+ "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
+ ('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz)"
+where
+ "foo_bar_baz_copy = (\<Lambda> f. (foo_copy\<cdot>f, bar_copy\<cdot>f, baz_copy\<cdot>f))"
lemma fix_foo_bar_baz_copy:
"fix\<cdot>foo_bar_baz_copy = (foo_map\<cdot>ID, bar_map\<cdot>ID, baz_map\<cdot>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\<cdot>foo_bar_baz_copy)\<cdot>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\<cdot>foo_bar_baz_copy))\<cdot>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\<cdot>foo_bar_baz_copy))\<cdot>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