--- a/src/HOLCF/Representable.thy Thu Nov 19 08:08:57 2009 -0800
+++ b/src/HOLCF/Representable.thy Thu Nov 19 08:22:00 2009 -0800
@@ -690,14 +690,14 @@
Abs_fin_defl (udom_emb oo
f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj))))"
-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 .
@@ -746,124 +746,124 @@
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_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)
@@ -963,59 +963,59 @@
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_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_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
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Thu Nov 19 08:08:57 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Thu Nov 19 08:22:00 2009 -0800
@@ -197,14 +197,14 @@
(* FIXME: use theory data for this *)
val defl_tab : term Symtab.table =
- Symtab.make [(@{type_name "->"}, @{term "cfun_typ"}),
- (@{type_name "++"}, @{term "ssum_typ"}),
- (@{type_name "**"}, @{term "sprod_typ"}),
- (@{type_name "*"}, @{term "cprod_typ"}),
- (@{type_name "u"}, @{term "u_typ"}),
- (@{type_name "upper_pd"}, @{term "upper_typ"}),
- (@{type_name "lower_pd"}, @{term "lower_typ"}),
- (@{type_name "convex_pd"}, @{term "convex_typ"})];
+ Symtab.make [(@{type_name "->"}, @{term "cfun_defl"}),
+ (@{type_name "++"}, @{term "ssum_defl"}),
+ (@{type_name "**"}, @{term "sprod_defl"}),
+ (@{type_name "*"}, @{term "cprod_defl"}),
+ (@{type_name "u"}, @{term "u_defl"}),
+ (@{type_name "upper_pd"}, @{term "upper_defl"}),
+ (@{type_name "lower_pd"}, @{term "lower_defl"}),
+ (@{type_name "convex_pd"}, @{term "convex_defl"})];
fun defl_of_typ
(tab : term Symtab.table)
@@ -306,20 +306,20 @@
end) doms;
val dom_binds = map (fn (_, tbind, _, _) => tbind) doms;
- (* declare type combinator constants *)
- fun declare_typ_const (vs, tbind, mx, rhs) thy =
+ (* declare deflation combinator constants *)
+ fun declare_defl_const (vs, tbind, mx, rhs) thy =
let
- val typ_type = Library.foldr cfunT (map (K deflT) vs, deflT);
- val typ_bind = Binding.suffix_name "_typ" tbind;
+ val defl_type = Library.foldr cfunT (map (K deflT) vs, deflT);
+ val defl_bind = Binding.suffix_name "_defl" tbind;
in
- Sign.declare_const ((typ_bind, typ_type), NoSyn) thy
+ Sign.declare_const ((defl_bind, defl_type), NoSyn) thy
end;
- val (typ_consts, thy) = fold_map declare_typ_const doms thy;
+ val (defl_consts, thy) = fold_map declare_defl_const doms thy;
(* defining equations for type combinators *)
val defl_tab1 = defl_tab; (* FIXME: use theory data *)
val defl_tab2 =
- Symtab.make (map (fst o dest_Type o fst) dom_eqns ~~ typ_consts);
+ Symtab.make (map (fst o dest_Type o fst) dom_eqns ~~ defl_consts);
val defl_tab' = Symtab.merge (K true) (defl_tab1, defl_tab2);
fun free a = Free (Library.unprefix "'" a, deflT);
fun mk_defl_spec (lhsT, rhsT) =
@@ -327,22 +327,22 @@
defl_of_typ defl_tab' free rhsT);
val defl_specs = map mk_defl_spec dom_eqns;
- (* register recursive definition of type combinators *)
- val typ_binds = map (Binding.suffix_name "_typ") dom_binds;
- val (typ_unfold_thms, thy) = add_fixdefs (typ_binds ~~ defl_specs) thy;
+ (* register recursive definition of deflation combinators *)
+ val defl_binds = map (Binding.suffix_name "_defl") dom_binds;
+ val (defl_unfold_thms, thy) = add_fixdefs (defl_binds ~~ defl_specs) thy;
(* define types using deflation combinators *)
- fun make_repdef ((vs, tbind, mx, _), typ_const) thy =
+ 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 (typ_const, reps);
+ 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 ~~ typ_consts) thy;
+ val (REP_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy;
(* FIXME: use theory data for this *)
val REP_simps = REP_thms @
@@ -355,7 +355,7 @@
val goal = mk_eqs (mk_Rep_of lhsT, mk_Rep_of rhsT);
val tac =
simp_tac (HOL_basic_ss addsimps REP_simps) 1
- THEN resolve_tac typ_unfold_thms 1;
+ THEN resolve_tac defl_unfold_thms 1;
in
Goal.prove_global thy [] [] goal (K tac)
end;
--- a/src/HOLCF/ex/Domain_Proofs.thy Thu Nov 19 08:08:57 2009 -0800
+++ b/src/HOLCF/ex/Domain_Proofs.thy Thu Nov 19 08:22:00 2009 -0800
@@ -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. Abs_CFun (\<lambda>(t1, t2, t3).
- ( ssum_typ\<cdot>REP(one)\<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))
+ , sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t3)
+ , sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(convex_defl\<cdot>t1)))))"
-lemma foo_bar_baz_typF_beta:
- "foo_bar_baz_typF\<cdot>a\<cdot>t =
- ( ssum_typ\<cdot>REP(one)\<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
+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))))
+ , sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(snd (snd t)))
+ , sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(fst t))))"
+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>REP(one)\<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 = sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(baz_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 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 = sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a)))"
+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>)"
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>)"
unfolding REP_foo REP_bar REP_baz REP_simps
-by (rule baz_typ_unfold)
+by (rule baz_defl_unfold)
(********************************************************************)
@@ -318,17 +318,17 @@
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 (simp add: foo_defl_def bar_defl_def baz_defl_def)
apply (rule parallel_fix_ind
- [where F="foo_bar_baz_typF\<cdot>t" and G="foo_bar_baz_mapF\<cdot>d"])
+ [where F="foo_bar_baz_deflF\<cdot>t" and G="foo_bar_baz_mapF\<cdot>d"])
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