--- a/src/HOLCF/Bifinite.thy Fri Nov 20 09:21:59 2009 +0100
+++ b/src/HOLCF/Bifinite.thy Fri Nov 20 09:22:14 2009 +0100
@@ -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 09:21:59 2009 +0100
+++ b/src/HOLCF/ConvexPD.thy Fri Nov 20 09:22:14 2009 +0100
@@ -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/IsaMakefile Fri Nov 20 09:21:59 2009 +0100
+++ b/src/HOLCF/IsaMakefile Fri Nov 20 09:22:14 2009 +0100
@@ -100,6 +100,7 @@
ex/Focus_ex.thy \
ex/Hoare.thy \
ex/Loop.thy \
+ ex/New_Domain.thy \
ex/Powerdomain_ex.thy \
ex/Stream.thy \
ex/ROOT.ML
--- a/src/HOLCF/LowerPD.thy Fri Nov 20 09:21:59 2009 +0100
+++ b/src/HOLCF/LowerPD.thy Fri Nov 20 09:22:14 2009 +0100
@@ -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 09:21:59 2009 +0100
+++ b/src/HOLCF/Representable.thy Fri Nov 20 09:22:14 2009 +0100
@@ -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 09:21:59 2009 +0100
+++ b/src/HOLCF/Sprod.thy Fri Nov 20 09:22:14 2009 +0100
@@ -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 09:21:59 2009 +0100
+++ b/src/HOLCF/Ssum.thy Fri Nov 20 09:22:14 2009 +0100
@@ -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 09:21:59 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Fri Nov 20 09:22:14 2009 +0100
@@ -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 09:21:59 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Nov 20 09:22:14 2009 +0100
@@ -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 09:21:59 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Fri Nov 20 09:22:14 2009 +0100
@@ -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 09:21:59 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Fri Nov 20 09:22:14 2009 +0100
@@ -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/Tools/repdef.ML Fri Nov 20 09:21:59 2009 +0100
+++ b/src/HOLCF/Tools/repdef.ML Fri Nov 20 09:22:14 2009 +0100
@@ -172,7 +172,7 @@
((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name), (t, vs, mx), A, morphs);
val _ =
- OuterSyntax.command "repdef" "HOLCF definition of representable domains" K.thy_goal
+ OuterSyntax.command "repdef" "HOLCF definition of representable domains" K.thy_decl
(repdef_decl >>
(Toplevel.print oo (Toplevel.theory o mk_repdef)));
--- a/src/HOLCF/Up.thy Fri Nov 20 09:21:59 2009 +0100
+++ b/src/HOLCF/Up.thy Fri Nov 20 09:22:14 2009 +0100
@@ -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 09:21:59 2009 +0100
+++ b/src/HOLCF/UpperPD.thy Fri Nov 20 09:22:14 2009 +0100
@@ -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)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/New_Domain.thy Fri Nov 20 09:22:14 2009 +0100
@@ -0,0 +1,92 @@
+(* Title: HOLCF/ex/New_Domain.thy
+ Author: Brian Huffman
+*)
+
+header {* Definitional domain package *}
+
+theory New_Domain
+imports HOLCF
+begin
+
+text {*
+ The definitional domain package only works with representable domains,
+ i.e. types in class @{text rep}.
+*}
+
+defaultsort rep
+
+text {*
+ Provided that @{text rep} is the default sort, the @{text new_domain}
+ package should work with any type definition supported by the old
+ domain package.
+*}
+
+new_domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
+
+text {*
+ The difference is that the new domain package is completely
+ definitional, and does not generate any axioms. The following type
+ and constant definitions are not produced by the old domain package.
+*}
+
+thm type_definition_llist
+thm llist_abs_def llist_rep_def
+
+text {*
+ The new domain package also adds support for indirect recursion with
+ user-defined datatypes. This definition of a tree datatype uses
+ indirect recursion through the lazy list type constructor.
+*}
+
+new_domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
+
+text {*
+ For indirect-recursive definitions, the domain package is not able to
+ generate a high-level induction rule. (It produces a warning
+ message instead.) The low-level reach lemma (now proved as a
+ theorem, no longer generated as an axiom) can be used to derive
+ other induction rules.
+*}
+
+thm ltree.reach
+
+text {*
+ The definition of the copy function uses map functions associated with
+ each type constructor involved in the definition. A map function
+ for the lazy list type has been generated by the new domain package.
+*}
+
+thm ltree.copy_def
+thm llist_map_def
+
+lemma ltree_induct:
+ fixes P :: "'a ltree \<Rightarrow> bool"
+ assumes adm: "adm P"
+ assumes bot: "P \<bottom>"
+ assumes Leaf: "\<And>x. P (Leaf\<cdot>x)"
+ assumes Branch: "\<And>f l. \<forall>x. P (f\<cdot>x) \<Longrightarrow> P (Branch\<cdot>(llist_map\<cdot>f\<cdot>l))"
+ shows "P x"
+proof -
+ have "\<forall>x. P (fix\<cdot>ltree_copy\<cdot>x)"
+ proof (rule fix_ind)
+ show "adm (\<lambda>a. \<forall>x. P (a\<cdot>x))"
+ by (simp add: adm_subst [OF _ adm])
+ next
+ show "\<forall>x. P (\<bottom>\<cdot>x)"
+ by (simp add: bot)
+ next
+ fix f :: "'a ltree \<rightarrow> 'a ltree"
+ assume f: "\<forall>x. P (f\<cdot>x)"
+ show "\<forall>x. P (ltree_copy\<cdot>f\<cdot>x)"
+ apply (rule allI)
+ apply (case_tac x)
+ apply (simp add: bot)
+ apply (simp add: Leaf)
+ apply (simp add: Branch [OF f])
+ done
+ qed
+ thus ?thesis
+ by (simp add: ltree.reach)
+qed
+
+end
--- a/src/HOLCF/ex/ROOT.ML Fri Nov 20 09:21:59 2009 +0100
+++ b/src/HOLCF/ex/ROOT.ML Fri Nov 20 09:22:14 2009 +0100
@@ -4,4 +4,5 @@
*)
use_thys ["Dnat", "Stream", "Dagstuhl", "Focus_ex", "Fix2", "Hoare",
- "Loop", "Fixrec_ex", "Powerdomain_ex", "Domain_ex", "Domain_Proofs"];
+ "Loop", "Fixrec_ex", "Powerdomain_ex", "Domain_ex", "Domain_Proofs",
+ "New_Domain"];