--- a/src/HOLCF/Bifinite.thy Fri Nov 20 07:24:21 2009 +0100
+++ b/src/HOLCF/Bifinite.thy Thu Nov 19 22:30:14 2009 -0800
@@ -114,6 +114,9 @@
lemma cprod_map_Pair [simp]: "cprod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
unfolding cprod_map_def by simp
+lemma cprod_map_ID: "cprod_map\<cdot>ID\<cdot>ID = ID"
+unfolding expand_cfun_eq by auto
+
lemma cprod_map_map:
"cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
cprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
@@ -207,6 +210,9 @@
lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))"
unfolding cfun_map_def by simp
+lemma cfun_map_ID: "cfun_map\<cdot>ID\<cdot>ID = ID"
+unfolding expand_cfun_eq by simp
+
lemma cfun_map_map:
"cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
--- a/src/HOLCF/ConvexPD.thy Fri Nov 20 07:24:21 2009 +0100
+++ b/src/HOLCF/ConvexPD.thy Thu Nov 19 22:30:14 2009 -0800
@@ -495,6 +495,9 @@
lemma convex_map_ident: "convex_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
by (induct xs rule: convex_pd_induct, simp_all)
+lemma convex_map_ID: "convex_map\<cdot>ID = ID"
+by (simp add: expand_cfun_eq ID_def convex_map_ident)
+
lemma convex_map_map:
"convex_map\<cdot>f\<cdot>(convex_map\<cdot>g\<cdot>xs) = convex_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
by (induct xs rule: convex_pd_induct, simp_all)
--- a/src/HOLCF/LowerPD.thy Fri Nov 20 07:24:21 2009 +0100
+++ b/src/HOLCF/LowerPD.thy Thu Nov 19 22:30:14 2009 -0800
@@ -471,6 +471,9 @@
lemma lower_map_ident: "lower_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
by (induct xs rule: lower_pd_induct, simp_all)
+lemma lower_map_ID: "lower_map\<cdot>ID = ID"
+by (simp add: expand_cfun_eq ID_def lower_map_ident)
+
lemma lower_map_map:
"lower_map\<cdot>f\<cdot>(lower_map\<cdot>g\<cdot>xs) = lower_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
by (induct xs rule: lower_pd_induct, simp_all)
--- a/src/HOLCF/Representable.thy Fri Nov 20 07:24:21 2009 +0100
+++ b/src/HOLCF/Representable.thy Thu Nov 19 22:30:14 2009 -0800
@@ -1038,28 +1038,28 @@
setup {*
fold Domain_Isomorphism.add_type_constructor
[(@{type_name "->"}, @{term cfun_defl}, @{const_name cfun_map},
- @{thm REP_cfun}, @{thm isodefl_cfun}),
+ @{thm REP_cfun}, @{thm isodefl_cfun}, @{thm cfun_map_ID}),
(@{type_name "++"}, @{term ssum_defl}, @{const_name ssum_map},
- @{thm REP_ssum}, @{thm isodefl_ssum}),
+ @{thm REP_ssum}, @{thm isodefl_ssum}, @{thm ssum_map_ID}),
(@{type_name "**"}, @{term sprod_defl}, @{const_name sprod_map},
- @{thm REP_sprod}, @{thm isodefl_sprod}),
+ @{thm REP_sprod}, @{thm isodefl_sprod}, @{thm sprod_map_ID}),
(@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map},
- @{thm REP_cprod}, @{thm isodefl_cprod}),
+ @{thm REP_cprod}, @{thm isodefl_cprod}, @{thm cprod_map_ID}),
(@{type_name "u"}, @{term u_defl}, @{const_name u_map},
- @{thm REP_up}, @{thm isodefl_u}),
+ @{thm REP_up}, @{thm isodefl_u}, @{thm u_map_ID}),
(@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map},
- @{thm REP_upper}, @{thm isodefl_upper}),
+ @{thm REP_upper}, @{thm isodefl_upper}, @{thm upper_map_ID}),
(@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map},
- @{thm REP_lower}, @{thm isodefl_lower}),
+ @{thm REP_lower}, @{thm isodefl_lower}, @{thm lower_map_ID}),
(@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map},
- @{thm REP_convex}, @{thm isodefl_convex})]
+ @{thm REP_convex}, @{thm isodefl_convex}, @{thm convex_map_ID})]
*}
end
--- a/src/HOLCF/Sprod.thy Fri Nov 20 07:24:21 2009 +0100
+++ b/src/HOLCF/Sprod.thy Thu Nov 19 22:30:14 2009 -0800
@@ -245,6 +245,9 @@
"x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
by (simp add: sprod_map_def)
+lemma sprod_map_ID: "sprod_map\<cdot>ID\<cdot>ID = ID"
+unfolding sprod_map_def by (simp add: expand_cfun_eq eta_cfun)
+
lemma sprod_map_map:
"\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
sprod_map\<cdot>f1\<cdot>g1\<cdot>(sprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
--- a/src/HOLCF/Ssum.thy Fri Nov 20 07:24:21 2009 +0100
+++ b/src/HOLCF/Ssum.thy Thu Nov 19 22:30:14 2009 -0800
@@ -226,6 +226,9 @@
lemma ssum_map_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
unfolding ssum_map_def by simp
+lemma ssum_map_ID: "ssum_map\<cdot>ID\<cdot>ID = ID"
+unfolding ssum_map_def by (simp add: expand_cfun_eq eta_cfun)
+
lemma ssum_map_map:
"\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) =
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML Fri Nov 20 07:24:21 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Thu Nov 19 22:30:14 2009 -0800
@@ -150,7 +150,7 @@
mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
in (dnam,
- (if definitional then [reach_ax] else [abs_iso_ax, rep_iso_ax, reach_ax]),
+ (if definitional then [] 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])
@@ -241,10 +241,11 @@
val thy = thy'
|> fold add_one (mapn (calc_axioms definitional map_tab comp_dname eqs) 0 eqs);
+ val use_copy_def = length eqs>1 andalso not definitional;
in
thy
|> Sign.add_path comp_dnam
- |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else []))
+ |> add_defs_infer (bisim_def::(if use_copy_def then [copy_def] else []))
|> Sign.parent_path
|> fold add_matchers eqs
end; (* let (add_axioms) *)
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Nov 20 07:24:21 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Thu Nov 19 22:30:14 2009 -0800
@@ -11,7 +11,7 @@
val domain_isomorphism_cmd:
(string list * binding * mixfix * string) list -> theory -> theory
val add_type_constructor:
- (string * term * string * thm * thm) -> theory -> theory
+ (string * term * string * thm * thm * thm) -> theory -> theory
val get_map_tab:
theory -> string Symtab.table
end;
@@ -63,12 +63,21 @@
val merge = Thm.merge_thms;
);
+structure MapIdData = 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) =
+ (tname, defl_const, map_name, REP_thm, isodefl_thm, map_ID_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);
+ #> IsodeflData.map (Thm.add_thm isodefl_thm)
+ #> MapIdData.map (Thm.add_thm map_ID_thm);
val get_map_tab = MapData.get;
@@ -558,17 +567,19 @@
val (_, thy) = thy |>
(PureThy.add_thms o map Thm.no_attributes)
(map_ID_binds ~~ map_ID_thms);
+ val thy = MapIdData.map (fold Thm.add_thm map_ID_thms) thy;
(* 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_arg = Free ("f", copy_arg_type);
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;
+ mk_fst t :: mk_copy_args xs (mk_snd t);
+ in mk_copy_args doms copy_arg end;
fun copy_of_dtyp (T, dt) =
if DatatypeAux.is_rec_type dt
then copy_of_dtyp' (T, dt)
@@ -591,7 +602,7 @@
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 rhs = big_lambda copy_arg comp;
val eqn = Logic.mk_equals (copy_const, rhs);
val ([copy_def], thy) =
thy
@@ -604,6 +615,69 @@
|> fold_map define_copy (dom_binds ~~ rep_abs_consts ~~ dom_eqns)
|>> ListPair.unzip;
+ (* define combined copy combinator *)
+ val ((c_const, c_def_thms), thy) =
+ if length doms = 1
+ then ((hd copy_consts, []), thy)
+ else
+ let
+ val c_type = copy_arg_type ->> copy_arg_type;
+ val c_name = space_implode "_" (map Binding.name_of dom_binds);
+ val c_bind = Binding.name (c_name ^ "_copy");
+ val c_body =
+ mk_tuple (map (mk_capply o rpair copy_arg) copy_consts);
+ val c_rhs = big_lambda copy_arg c_body;
+ val (c_const, thy) =
+ Sign.declare_const ((c_bind, c_type), NoSyn) thy;
+ val c_eqn = Logic.mk_equals (c_const, c_rhs);
+ val (c_def_thms, thy) =
+ thy
+ |> Sign.add_path c_name
+ |> (PureThy.add_defs false o map Thm.no_attributes)
+ [(Binding.name "copy_def", c_eqn)]
+ ||> Sign.parent_path;
+ in ((c_const, c_def_thms), thy) end;
+
+ (* fixed-point lemma for combined copy combinator *)
+ val fix_copy_lemma =
+ let
+ fun mk_map_ID (map_const, (Type (c, Ts), rhsT)) =
+ Library.foldl mk_capply (map_const, map ID_const Ts);
+ val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns));
+ val goal = mk_eqs (mk_fix c_const, rhs);
+ val rules =
+ [@{thm pair_collapse}, @{thm split_def}]
+ @ map_apply_thms
+ @ c_def_thms @ copy_defs
+ @ MapIdData.get thy;
+ val tac = simp_tac (beta_ss addsimps rules) 1;
+ in
+ Goal.prove_global thy [] [] goal (K tac)
+ end;
+
+ (* prove reach lemmas *)
+ val reach_thm_projs =
+ let fun mk_projs (x::[]) t = [(x, t)]
+ | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);
+ in mk_projs dom_binds (mk_fix c_const) end;
+ fun prove_reach_thm (((bind, t), map_ID_thm), (lhsT, rhsT)) thy =
+ let
+ val x = Free ("x", lhsT);
+ val goal = mk_eqs (mk_capply (t, x), x);
+ val rules =
+ fix_copy_lemma :: map_ID_thm :: @{thms fst_conv snd_conv ID1};
+ val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
+ val reach_thm = Goal.prove_global thy [] [] goal (K tac);
+ in
+ thy
+ |> Sign.add_path (Binding.name_of bind)
+ |> yield_singleton (PureThy.add_thms o map Thm.no_attributes)
+ (Binding.name "reach", reach_thm)
+ ||> Sign.parent_path
+ end;
+ val (reach_thms, thy) = thy |>
+ fold_map prove_reach_thm (reach_thm_projs ~~ map_ID_thms ~~ dom_eqns);
+
in
thy
end;
--- a/src/HOLCF/Tools/Domain/domain_syntax.ML Fri Nov 20 07:24:21 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Thu Nov 19 22:30:14 2009 -0800
@@ -196,7 +196,8 @@
in thy''
|> ContConsts.add_consts_i
(maps fst ctt @
- (if length eqs'>1 then [const_copy] else[])@
+ (if length eqs'>1 andalso not definitional
+ then [const_copy] else []) @
[const_bisim])
|> Sign.add_trrules_i (maps snd ctt)
end; (* let *)
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Fri Nov 20 07:24:21 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Nov 19 22:30:14 2009 -0800
@@ -998,7 +998,7 @@
handle THM _ =>
(warning "Induction proofs failed (THM raised)."; ([], TrueI))
| ERROR _ =>
- (warning "Induction proofs failed (ERROR raised)."; ([], TrueI));
+ (warning "Cannot prove induction rule"; ([], TrueI));
end; (* local *)
--- a/src/HOLCF/Up.thy Fri Nov 20 07:24:21 2009 +0100
+++ b/src/HOLCF/Up.thy Thu Nov 19 22:30:14 2009 -0800
@@ -303,6 +303,9 @@
lemma u_map_up [simp]: "u_map\<cdot>f\<cdot>(up\<cdot>x) = up\<cdot>(f\<cdot>x)"
unfolding u_map_def by simp
+lemma u_map_ID: "u_map\<cdot>ID = ID"
+unfolding u_map_def by (simp add: expand_cfun_eq eta_cfun)
+
lemma u_map_map: "u_map\<cdot>f\<cdot>(u_map\<cdot>g\<cdot>p) = u_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>p"
by (induct p) simp_all
--- a/src/HOLCF/UpperPD.thy Fri Nov 20 07:24:21 2009 +0100
+++ b/src/HOLCF/UpperPD.thy Thu Nov 19 22:30:14 2009 -0800
@@ -466,6 +466,9 @@
lemma upper_map_ident: "upper_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
by (induct xs rule: upper_pd_induct, simp_all)
+lemma upper_map_ID: "upper_map\<cdot>ID = ID"
+by (simp add: expand_cfun_eq ID_def upper_map_ident)
+
lemma upper_map_map:
"upper_map\<cdot>f\<cdot>(upper_map\<cdot>g\<cdot>xs) = upper_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
by (induct xs rule: upper_pd_induct, simp_all)