--- a/doc-src/TutorialI/Protocol/NS_Public.thy Wed Mar 03 08:28:33 2010 +0100
+++ b/doc-src/TutorialI/Protocol/NS_Public.thy Wed Mar 03 08:43:48 2010 +0100
@@ -76,7 +76,7 @@
@{term [display,indent=5] "Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>)"}
may be extended by an event of the form
@{term [display,indent=5] "Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)"}
-where @{text NB} is a fresh nonce: @{term "Nonce NB \<in> used evs2"}.
+where @{text NB} is a fresh nonce: @{term "Nonce NB \<notin> used evs2"}.
Writing the sender as @{text A'} indicates that @{text B} does not
know who sent the message. Calling the trace variable @{text evs2} rather
than simply @{text evs} helps us know where we are in a proof after many
--- a/doc-src/TutorialI/Protocol/document/NS_Public.tex Wed Mar 03 08:28:33 2010 +0100
+++ b/doc-src/TutorialI/Protocol/document/NS_Public.tex Wed Mar 03 08:43:48 2010 +0100
@@ -84,7 +84,7 @@
\begin{isabelle}%
\ \ \ \ \ Says\ B\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}%
\end{isabelle}
-where \isa{NB} is a fresh nonce: \isa{Nonce\ NB\ {\isasymin}\ used\ evs{\isadigit{2}}}.
+where \isa{NB} is a fresh nonce: \isa{Nonce\ NB\ {\isasymnotin}\ used\ evs{\isadigit{2}}}.
Writing the sender as \isa{A{\isacharprime}} indicates that \isa{B} does not
know who sent the message. Calling the trace variable \isa{evs{\isadigit{2}}} rather
than simply \isa{evs} helps us know where we are in a proof after many
--- a/src/HOL/IsaMakefile Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOL/IsaMakefile Wed Mar 03 08:43:48 2010 +0100
@@ -756,7 +756,7 @@
HOL-ZF: HOL $(LOG)/HOL-ZF.gz
-$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/Helper.thy ZF/LProd.thy \
+$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy \
ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF
--- a/src/HOL/List.thy Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOL/List.thy Wed Mar 03 08:43:48 2010 +0100
@@ -761,13 +761,13 @@
by(induct ys, auto simp add: Cons_eq_map_conv)
lemma map_eq_imp_length_eq:
- assumes "map f xs = map f ys"
+ assumes "map f xs = map g ys"
shows "length xs = length ys"
using assms proof (induct ys arbitrary: xs)
case Nil then show ?case by simp
next
case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto
- from Cons xs have "map f zs = map f ys" by simp
+ from Cons xs have "map f zs = map g ys" by simp
moreover with Cons have "length zs = length ys" by blast
with xs show ?case by simp
qed
--- a/src/HOL/ZF/HOLZF.thy Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOL/ZF/HOLZF.thy Wed Mar 03 08:43:48 2010 +0100
@@ -6,7 +6,7 @@
*)
theory HOLZF
-imports Helper
+imports Main
begin
typedecl ZF
@@ -298,7 +298,7 @@
apply (rule_tac x="Fst z" in exI)
apply (simp add: isOpair_def)
apply (auto simp add: Fst Snd Opair)
- apply (rule theI2')
+ apply (rule the1I2)
apply auto
apply (drule Fun_implies_PFun)
apply (drule_tac x="Opair x ya" and y="Opair x yb" in PFun_inj)
@@ -306,7 +306,7 @@
apply (drule Fun_implies_PFun)
apply (drule_tac x="Opair x y" and y="Opair x ya" in PFun_inj)
apply (auto simp add: Fst Snd)
- apply (rule theI2')
+ apply (rule the1I2)
apply (auto simp add: Fun_total)
apply (drule Fun_implies_PFun)
apply (drule_tac x="Opair a x" and y="Opair a y" in PFun_inj)
--- a/src/HOL/ZF/Helper.thy Wed Mar 03 08:28:33 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-(* Title: HOL/ZF/Helper.thy
- ID: $Id$
- Author: Steven Obua
-
- Some helpful lemmas that probably will end up elsewhere.
-*)
-
-theory Helper
-imports Main
-begin
-
-lemma theI2' : "?! x. P x \<Longrightarrow> (!! x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (THE x. P x)"
- apply auto
- apply (subgoal_tac "P (THE x. P x)")
- apply blast
- apply (rule theI)
- apply auto
- done
-
-lemma in_range_superfluous: "(z \<in> range f & z \<in> (f ` x)) = (z \<in> f ` x)"
- by auto
-
-lemma f_x_in_range_f: "f x \<in> range f"
- by (blast intro: image_eqI)
-
-lemma comp_inj: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (g o f)"
- by (blast intro: comp_inj_on subset_inj_on)
-
-lemma comp_image_eq: "(g o f) ` x = g ` f ` x"
- by auto
-
-end
\ No newline at end of file
--- a/src/HOL/ZF/Zet.thy Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOL/ZF/Zet.thy Wed Mar 03 08:43:48 2010 +0100
@@ -35,7 +35,7 @@
apply (rule_tac x="Repl z (g o (inv_into A f))" in exI)
apply (simp add: explode_Repl_eq)
apply (subgoal_tac "explode z = f ` A")
- apply (simp_all add: comp_image_eq)
+ apply (simp_all add: image_compose)
done
lemma zet_image_mem:
@@ -56,7 +56,7 @@
apply (auto simp add: subset injf)
done
show ?thesis
- apply (simp add: zet_def' comp_image_eq[symmetric])
+ apply (simp add: zet_def' image_compose[symmetric])
apply (rule exI[where x="?w"])
apply (simp add: injw image_zet_rep Azet)
done
@@ -108,7 +108,7 @@
lemma comp_zimage_eq: "zimage g (zimage f A) = zimage (g o f) A"
apply (simp add: zimage_def)
apply (subst Abs_zet_inverse)
- apply (simp_all add: comp_image_eq zet_image_mem Rep_zet)
+ apply (simp_all add: image_compose zet_image_mem Rep_zet)
done
definition zunion :: "'a zet \<Rightarrow> 'a zet \<Rightarrow> 'a zet" where
--- a/src/HOLCF/Bifinite.thy Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOLCF/Bifinite.thy Wed Mar 03 08:43:48 2010 +0100
@@ -295,7 +295,7 @@
by (rule finite_range_imp_finite_fixes)
qed
-instantiation "->" :: (profinite, profinite) profinite
+instantiation cfun :: (profinite, profinite) profinite
begin
definition
@@ -325,7 +325,7 @@
end
-instance "->" :: (profinite, bifinite) bifinite ..
+instance cfun :: (profinite, bifinite) bifinite ..
lemma approx_cfun: "approx n\<cdot>f\<cdot>x = approx n\<cdot>(f\<cdot>(approx n\<cdot>x))"
by (simp add: approx_cfun_def)
--- a/src/HOLCF/Cfun.thy Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOLCF/Cfun.thy Wed Mar 03 08:43:48 2010 +0100
@@ -20,11 +20,11 @@
lemma adm_cont: "adm cont"
by (rule admI, rule cont_lub_fun)
-cpodef (CFun) ('a, 'b) "->" (infixr "->" 0) = "{f::'a => 'b. cont f}"
+cpodef (CFun) ('a, 'b) cfun (infixr "->" 0) = "{f::'a => 'b. cont f}"
by (simp_all add: Ex_cont adm_cont)
-syntax (xsymbols)
- "->" :: "[type, type] => type" ("(_ \<rightarrow>/ _)" [1,0]0)
+type_notation (xsymbols)
+ cfun ("(_ \<rightarrow>/ _)" [1, 0] 0)
notation
Rep_CFun ("(_$/_)" [999,1000] 999)
@@ -103,16 +103,16 @@
lemma UU_CFun: "\<bottom> \<in> CFun"
by (simp add: CFun_def inst_fun_pcpo cont_const)
-instance "->" :: (finite_po, finite_po) finite_po
+instance cfun :: (finite_po, finite_po) finite_po
by (rule typedef_finite_po [OF type_definition_CFun])
-instance "->" :: (finite_po, chfin) chfin
+instance cfun :: (finite_po, chfin) chfin
by (rule typedef_chfin [OF type_definition_CFun below_CFun_def])
-instance "->" :: (cpo, discrete_cpo) discrete_cpo
+instance cfun :: (cpo, discrete_cpo) discrete_cpo
by intro_classes (simp add: below_CFun_def Rep_CFun_inject)
-instance "->" :: (cpo, pcpo) pcpo
+instance cfun :: (cpo, pcpo) pcpo
by (rule typedef_pcpo [OF type_definition_CFun below_CFun_def UU_CFun])
lemmas Rep_CFun_strict =
--- a/src/HOLCF/Domain.thy Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOLCF/Domain.thy Wed Mar 03 08:43:48 2010 +0100
@@ -11,7 +11,6 @@
("Tools/cont_proc.ML")
("Tools/Domain/domain_constructors.ML")
("Tools/Domain/domain_library.ML")
- ("Tools/Domain/domain_syntax.ML")
("Tools/Domain/domain_axioms.ML")
("Tools/Domain/domain_theorems.ML")
("Tools/Domain/domain_extender.ML")
@@ -274,7 +273,6 @@
use "Tools/cont_consts.ML"
use "Tools/cont_proc.ML"
use "Tools/Domain/domain_library.ML"
-use "Tools/Domain/domain_syntax.ML"
use "Tools/Domain/domain_axioms.ML"
use "Tools/Domain/domain_constructors.ML"
use "Tools/Domain/domain_theorems.ML"
--- a/src/HOLCF/FOCUS/Fstream.thy Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOLCF/FOCUS/Fstream.thy Wed Mar 03 08:43:48 2010 +0100
@@ -83,7 +83,7 @@
by (simp add: fscons_def2)
lemma fstream_prefix: "a~> s << t ==> ? tt. t = a~> tt & s << tt"
-apply (rule_tac x="t" in stream.casedist)
+apply (cases t)
apply (cut_tac fscons_not_empty)
apply (fast dest: eq_UU_iff [THEN iffD2])
apply (simp add: fscons_def2)
--- a/src/HOLCF/Fixrec.thy Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOLCF/Fixrec.thy Wed Mar 03 08:43:48 2010 +0100
@@ -6,7 +6,9 @@
theory Fixrec
imports Sprod Ssum Up One Tr Fix
-uses ("Tools/fixrec.ML")
+uses
+ ("Tools/holcf_library.ML")
+ ("Tools/fixrec.ML")
begin
subsection {* Maybe monad type *}
@@ -603,6 +605,7 @@
subsection {* Initializing the fixrec package *}
+use "Tools/holcf_library.ML"
use "Tools/fixrec.ML"
setup {* Fixrec.setup *}
--- a/src/HOLCF/IOA/meta_theory/Seq.thy Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy Wed Mar 03 08:43:48 2010 +0100
@@ -191,7 +191,7 @@
by simp
lemma nil_less_is_nil: "nil<<x ==> nil=x"
-apply (rule_tac x="x" in seq.casedist)
+apply (cases x)
apply simp
apply simp
apply simp
@@ -286,8 +286,8 @@
lemma Finite_upward: "\<lbrakk>Finite x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> Finite y"
apply (induct arbitrary: y set: Finite)
-apply (rule_tac x=y in seq.casedist, simp, simp, simp)
-apply (rule_tac x=y in seq.casedist, simp, simp)
+apply (case_tac y, simp, simp, simp)
+apply (case_tac y, simp, simp)
apply simp
done
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Wed Mar 03 08:43:48 2010 +0100
@@ -163,8 +163,7 @@
lemma Last_cons: "Last$(x>>xs)= (if xs=nil then Def x else Last$xs)"
apply (simp add: Last_def Consq_def)
-apply (rule_tac x="xs" in seq.casedist)
-apply simp
+apply (cases xs)
apply simp_all
done
@@ -208,7 +207,7 @@
lemma Zip_UU2: "x~=nil ==> Zip$x$UU =UU"
apply (subst Zip_unfold)
apply simp
-apply (rule_tac x="x" in seq.casedist)
+apply (cases x)
apply simp_all
done
--- a/src/HOLCF/IsaMakefile Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOLCF/IsaMakefile Wed Mar 03 08:43:48 2010 +0100
@@ -70,7 +70,7 @@
Tools/Domain/domain_constructors.ML \
Tools/Domain/domain_isomorphism.ML \
Tools/Domain/domain_library.ML \
- Tools/Domain/domain_syntax.ML \
+ Tools/Domain/domain_take_proofs.ML \
Tools/Domain/domain_theorems.ML \
Tools/fixrec.ML \
Tools/pcpodef.ML \
--- a/src/HOLCF/Representable.thy Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOLCF/Representable.thy Wed Mar 03 08:43:48 2010 +0100
@@ -8,7 +8,7 @@
imports Algebraic Universal Ssum Sprod One Fixrec
uses
("Tools/repdef.ML")
- ("Tools/holcf_library.ML")
+ ("Tools/Domain/domain_take_proofs.ML")
("Tools/Domain/domain_isomorphism.ML")
begin
@@ -415,7 +415,7 @@
text "Functions between representable types are representable."
-instantiation "->" :: (rep, rep) rep
+instantiation cfun :: (rep, rep) rep
begin
definition emb_cfun_def: "emb = udom_emb oo cfun_map\<cdot>prj\<cdot>emb"
@@ -430,7 +430,7 @@
text "Strict products of representable types are representable."
-instantiation "**" :: (rep, rep) rep
+instantiation sprod :: (rep, rep) rep
begin
definition emb_sprod_def: "emb = udom_emb oo sprod_map\<cdot>emb\<cdot>emb"
@@ -445,7 +445,7 @@
text "Strict sums of representable types are representable."
-instantiation "++" :: (rep, rep) rep
+instantiation ssum :: (rep, rep) rep
begin
definition emb_ssum_def: "emb = udom_emb oo ssum_map\<cdot>emb\<cdot>emb"
@@ -777,18 +777,18 @@
subsection {* Constructing Domain Isomorphisms *}
-use "Tools/holcf_library.ML"
+use "Tools/Domain/domain_take_proofs.ML"
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},
+ [(@{type_name cfun}, @{term cfun_defl}, @{const_name cfun_map}, @{thm REP_cfun},
@{thm isodefl_cfun}, @{thm cfun_map_ID}, @{thm deflation_cfun_map}),
- (@{type_name "++"}, @{term ssum_defl}, @{const_name ssum_map}, @{thm REP_ssum},
+ (@{type_name ssum}, @{term ssum_defl}, @{const_name ssum_map}, @{thm REP_ssum},
@{thm isodefl_ssum}, @{thm ssum_map_ID}, @{thm deflation_ssum_map}),
- (@{type_name "**"}, @{term sprod_defl}, @{const_name sprod_map}, @{thm REP_sprod},
+ (@{type_name sprod}, @{term sprod_defl}, @{const_name sprod_map}, @{thm REP_sprod},
@{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}),
(@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map}, @{thm REP_cprod},
--- a/src/HOLCF/Sprod.thy Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOLCF/Sprod.thy Wed Mar 03 08:43:48 2010 +0100
@@ -12,20 +12,20 @@
subsection {* Definition of strict product type *}
-pcpodef (Sprod) ('a, 'b) "**" (infixr "**" 20) =
+pcpodef (Sprod) ('a, 'b) sprod (infixr "**" 20) =
"{p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
by simp_all
-instance "**" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
+instance sprod :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
by (rule typedef_finite_po [OF type_definition_Sprod])
-instance "**" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
+instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
by (rule typedef_chfin [OF type_definition_Sprod below_Sprod_def])
syntax (xsymbols)
- "**" :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20)
+ sprod :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20)
syntax (HTML output)
- "**" :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20)
+ sprod :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20)
lemma spair_lemma:
"(strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a) \<in> Sprod"
@@ -80,11 +80,11 @@
apply fast
done
-lemma sprodE [cases type: **]:
+lemma sprodE [cases type: sprod]:
"\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x y. \<lbrakk>p = (:x, y:); x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
by (cut_tac z=p in Exh_Sprod, auto)
-lemma sprod_induct [induct type: **]:
+lemma sprod_induct [induct type: sprod]:
"\<lbrakk>P \<bottom>; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> P (:x, y:)\<rbrakk> \<Longrightarrow> P x"
by (cases x, simp_all)
@@ -221,7 +221,7 @@
subsection {* Strict product preserves flatness *}
-instance "**" :: (flat, flat) flat
+instance sprod :: (flat, flat) flat
proof
fix x y :: "'a \<otimes> 'b"
assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y"
@@ -312,7 +312,7 @@
subsection {* Strict product is a bifinite domain *}
-instantiation "**" :: (bifinite, bifinite) bifinite
+instantiation sprod :: (bifinite, bifinite) bifinite
begin
definition
--- a/src/HOLCF/Ssum.thy Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOLCF/Ssum.thy Wed Mar 03 08:43:48 2010 +0100
@@ -12,22 +12,22 @@
subsection {* Definition of strict sum type *}
-pcpodef (Ssum) ('a, 'b) "++" (infixr "++" 10) =
+pcpodef (Ssum) ('a, 'b) ssum (infixr "++" 10) =
"{p :: tr \<times> ('a \<times> 'b).
(fst p \<sqsubseteq> TT \<longleftrightarrow> snd (snd p) = \<bottom>) \<and>
(fst p \<sqsubseteq> FF \<longleftrightarrow> fst (snd p) = \<bottom>)}"
by simp_all
-instance "++" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
+instance ssum :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
by (rule typedef_finite_po [OF type_definition_Ssum])
-instance "++" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
+instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def])
syntax (xsymbols)
- "++" :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20)
+ ssum :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20)
syntax (HTML output)
- "++" :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20)
+ ssum :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20)
subsection {* Definitions of constructors *}
@@ -150,13 +150,13 @@
apply (simp add: sinr_Abs_Ssum Ssum_def)
done
-lemma ssumE [cases type: ++]:
+lemma ssumE [cases type: ssum]:
"\<lbrakk>p = \<bottom> \<Longrightarrow> Q;
\<And>x. \<lbrakk>p = sinl\<cdot>x; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q;
\<And>y. \<lbrakk>p = sinr\<cdot>y; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
by (cut_tac z=p in Exh_Ssum, auto)
-lemma ssum_induct [induct type: ++]:
+lemma ssum_induct [induct type: ssum]:
"\<lbrakk>P \<bottom>;
\<And>x. x \<noteq> \<bottom> \<Longrightarrow> P (sinl\<cdot>x);
\<And>y. y \<noteq> \<bottom> \<Longrightarrow> P (sinr\<cdot>y)\<rbrakk> \<Longrightarrow> P x"
@@ -203,7 +203,7 @@
subsection {* Strict sum preserves flatness *}
-instance "++" :: (flat, flat) flat
+instance ssum :: (flat, flat) flat
apply (intro_classes, clarify)
apply (case_tac x, simp)
apply (case_tac y, simp_all add: flat_below_iff)
@@ -296,7 +296,7 @@
subsection {* Strict sum is a bifinite domain *}
-instantiation "++" :: (bifinite, bifinite) bifinite
+instantiation ssum :: (bifinite, bifinite) bifinite
begin
definition
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Wed Mar 03 08:43:48 2010 +0100
@@ -1,24 +1,22 @@
(* Title: HOLCF/Tools/Domain/domain_axioms.ML
Author: David von Oheimb
+ Author: Brian Huffman
Syntax generator for domain command.
*)
signature DOMAIN_AXIOMS =
sig
+ val axiomatize_isomorphism :
+ binding * (typ * typ) ->
+ theory -> Domain_Take_Proofs.iso_info * theory
+
val copy_of_dtyp :
string Symtab.table -> (int -> term) -> Datatype.dtyp -> term
- val calc_axioms :
- bool -> string Symtab.table ->
- Domain_Library.eq list -> int -> Domain_Library.eq ->
- string * (string * term) list * (string * term) list
-
val add_axioms :
- bool ->
- ((string * typ list) *
- (binding * (bool * binding option * typ) list * mixfix) list) list ->
- Domain_Library.eq list -> theory -> theory
+ (binding * (typ * typ)) list ->
+ theory -> theory
end;
@@ -33,9 +31,9 @@
(* FIXME: use theory data for this *)
val copy_tab : string Symtab.table =
- Symtab.make [(@{type_name "->"}, @{const_name "cfun_map"}),
- (@{type_name "++"}, @{const_name "ssum_map"}),
- (@{type_name "**"}, @{const_name "sprod_map"}),
+ Symtab.make [(@{type_name cfun}, @{const_name "cfun_map"}),
+ (@{type_name ssum}, @{const_name "ssum_map"}),
+ (@{type_name sprod}, @{const_name "sprod_map"}),
(@{type_name "*"}, @{const_name "cprod_map"}),
(@{type_name "u"}, @{const_name "u_map"})];
@@ -48,39 +46,57 @@
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
- (definitional : bool)
- (map_tab : string Symtab.table)
- (eqs : eq list)
- (n : int)
- (eqn as ((dname,_),cons) : eq)
- : string * (string * term) list * (string * term) list =
+local open HOLCF_Library in
+
+fun axiomatize_isomorphism
+ (dbind : binding, (lhsT, rhsT))
+ (thy : theory)
+ : Domain_Take_Proofs.iso_info * theory =
let
+ val dname = Long_Name.base_name (Binding.name_of dbind);
-(* ----- axioms and definitions concerning the isomorphism ------------------ *)
+ val abs_bind = Binding.suffix_name "_abs" dbind;
+ val rep_bind = Binding.suffix_name "_rep" dbind;
- 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_const, thy) =
+ Sign.declare_const ((abs_bind, rhsT ->> lhsT), NoSyn) thy;
+ val (rep_const, thy) =
+ Sign.declare_const ((rep_bind, lhsT ->> rhsT), NoSyn) thy;
+
+ val x = Free ("x", lhsT);
+ val y = Free ("y", rhsT);
+
+ val abs_iso_eqn =
+ Logic.all y (mk_trp (mk_eq (rep_const ` (abs_const ` y), y)));
+ val rep_iso_eqn =
+ Logic.all x (mk_trp (mk_eq (abs_const ` (rep_const ` x), x)));
- 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 thy = Sign.add_path dname thy;
+
+ val (abs_iso_thm, thy) =
+ yield_singleton PureThy.add_axioms
+ ((Binding.name "abs_iso", abs_iso_eqn), []) thy;
-(* ----- axiom and definitions concerning induction ------------------------- *)
+ val (rep_iso_thm, thy) =
+ yield_singleton PureThy.add_axioms
+ ((Binding.name "rep_iso", rep_iso_eqn), []) thy;
+
+ val thy = Sign.parent_path thy;
- val finite_def =
- ("finite_def",
- %%:(dname^"_finite") ==
- mk_lam(x_name,
- mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
+ val result =
+ {
+ absT = lhsT,
+ repT = rhsT,
+ abs_const = abs_const,
+ rep_const = rep_const,
+ abs_inverse = abs_iso_thm,
+ rep_inverse = rep_iso_thm
+ };
+ in
+ (result, thy)
+ end;
- in (dnam,
- (if definitional then [] else [abs_iso_ax, rep_iso_ax]),
- [finite_def])
- end; (* let (calc_axioms) *)
-
+end;
(* legacy type inference *)
@@ -95,78 +111,46 @@
fun add_axioms_i x = snd o PureThy.add_axioms (map (Thm.no_attributes o apfst Binding.name) x);
fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy;
-fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x);
-fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
-
-fun add_axioms definitional eqs' (eqs : eq list) thy' =
+fun add_axioms
+ (dom_eqns : (binding * (typ * typ)) list)
+ (thy : theory) =
let
- val dnames = map (fst o fst) eqs;
- val x_name = idx_name dnames "x";
- fun add_one (dnam, axs, dfs) =
+ (* declare and axiomatize abs/rep *)
+ val (iso_infos, thy) =
+ fold_map axiomatize_isomorphism dom_eqns thy;
+
+ fun add_one (dnam, axs) =
Sign.add_path dnam
#> add_axioms_infer axs
#> Sign.parent_path;
- val map_tab = Domain_Isomorphism.get_map_tab thy';
- val axs = mapn (calc_axioms definitional map_tab eqs) 0 eqs;
- val thy = thy' |> fold add_one axs;
-
- fun get_iso_info ((dname, tyvars), cons') =
- let
- 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);
- val ax_abs_iso = PureThy.get_thm thy (dname ^ ".abs_iso");
- val ax_rep_iso = PureThy.get_thm thy (dname ^ ".rep_iso");
- val lhsT = Type(dname,tyvars);
- val rhsT = foldr1 mk_ssumT (map prod cons');
- val rep_const = Const(dname^"_rep", lhsT ->> rhsT);
- val abs_const = Const(dname^"_abs", rhsT ->> lhsT);
- in
- {
- absT = lhsT,
- repT = rhsT,
- abs_const = abs_const,
- rep_const = rep_const,
- abs_inverse = ax_abs_iso,
- rep_inverse = ax_rep_iso
- }
- end;
- val dom_binds = map (Binding.name o Long_Name.base_name) dnames;
- val thy =
- if definitional then thy
- else snd (Domain_Isomorphism.define_take_functions
- (dom_binds ~~ map get_iso_info eqs') thy);
-
- fun add_one' (dnam, axs, dfs) =
- Sign.add_path dnam
- #> add_defs_infer dfs
- #> Sign.parent_path;
- val thy = fold add_one' axs thy;
+ (* define take function *)
+ val (take_info, thy) =
+ Domain_Take_Proofs.define_take_functions
+ (map fst dom_eqns ~~ iso_infos) thy;
(* declare lub_take axioms *)
local
- fun ax_lub_take dname =
+ fun ax_lub_take (dbind, take_const) =
let
- val dnam : string = Long_Name.base_name dname;
- val take_const = %%:(dname^"_take");
+ val dnam = Long_Name.base_name (Binding.name_of dbind);
val lub = %%: @{const_name lub};
val image = %%: @{const_name image};
val UNIV = @{term "UNIV :: nat set"};
val lhs = lub $ (image $ take_const $ UNIV);
val ax = mk_trp (lhs === ID);
in
- add_one (dnam, [("lub_take", ax)], [])
+ add_one (dnam, [("lub_take", ax)])
end
+ val dbinds = map fst dom_eqns;
+ val take_consts = #take_consts take_info;
in
- val thy =
- if definitional then thy
- else fold ax_lub_take dnames thy
+ val thy = fold ax_lub_take (dbinds ~~ take_consts) thy
end;
+
in
- thy
- end; (* let (add_axioms) *)
+ thy (* TODO: also return iso_infos, take_info, lub_take_thms *)
+ end;
end; (* struct *)
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Wed Mar 03 08:43:48 2010 +0100
@@ -10,7 +10,7 @@
val add_domain_constructors :
string
-> (binding * (bool * binding option * typ) list * mixfix) list
- -> Domain_Isomorphism.iso_info
+ -> Domain_Take_Proofs.iso_info
-> theory
-> { con_consts : term list,
con_betas : thm list,
@@ -190,15 +190,15 @@
val thm2 = rewrite_rule (map mk_meta_eq @{thms ex_defined_iffs}) thm1;
val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2;
- val x = Free ("x", lhsT);
+ val y = Free ("y", lhsT);
fun one_con (con, args) =
let
- val (vs, nonlazy) = get_vars_avoiding ["x"] args;
- val eqn = mk_eq (x, list_ccomb (con, vs));
+ val (vs, nonlazy) = get_vars_avoiding ["y"] args;
+ val eqn = mk_eq (y, list_ccomb (con, vs));
val conj = foldr1 mk_conj (eqn :: map mk_defined nonlazy);
in Library.foldr mk_ex (vs, conj) end;
- val goal = mk_trp (foldr1 mk_disj (mk_undef x :: map one_con spec'));
- (* first 3 rules replace "x = UU \/ P" with "rep$x = UU \/ P" *)
+ val goal = mk_trp (foldr1 mk_disj (mk_undef y :: map one_con spec'));
+ (* first 3 rules replace "y = UU \/ P" with "rep$y = UU \/ P" *)
val tacs = [
rtac (iso_locale RS @{thm iso.casedist_rule}) 1,
rewrite_goals_tac [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})],
@@ -1011,7 +1011,7 @@
fun add_domain_constructors
(dname : string)
(spec : (binding * (bool * binding option * typ) list * mixfix) list)
- (iso_info : Domain_Isomorphism.iso_info)
+ (iso_info : Domain_Take_Proofs.iso_info)
(thy : theory) =
let
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Wed Mar 03 08:43:48 2010 +0100
@@ -79,7 +79,9 @@
| 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"]
+ val indirect_ok =
+ [@{type_name "*"}, @{type_name cfun}, @{type_name ssum},
+ @{type_name sprod}, @{type_name u}];
fun analyse indirect (TFree(v,s)) =
(case AList.lookup (op =) tvars v of
NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
@@ -127,44 +129,63 @@
(comp_dnam : string)
(eqs''' : ((string * string option) list * binding * mixfix *
(binding * (bool * binding option * 'a) list * mixfix) list) list)
- (thy''' : theory) =
+ (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 : (binding * typ list * mixfix) list =
+ let
+ fun readS (SOME s) = Syntax.read_sort_global thy s
+ | readS NONE = Sign.defaultS thy;
+ fun readTFree (a, s) = TFree (a, readS s);
+ in
+ map (fn (vs,dname:binding,mx,_) =>
+ (dname, map readTFree vs, mx)) eqs'''
+ 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;
+ (* declare new types *)
+ val thy =
+ let
+ 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);
+ in
+ thy
+ |> Sign.add_types (map thy_type dtnvs)
+ |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs
+ end;
+
+ val dbinds : binding list =
+ map (fn (_,dbind,_,_) => dbind) eqs''';
+ val cons''' :
+ (binding * (bool * binding option * 'a) list * mixfix) list list =
+ map (fn (_,_,_,cons) => cons) eqs''';
+ val cons'' :
+ (binding * (bool * binding option * typ) list * mixfix) list list =
+ map (map (upd_second (map (upd_third (prep_typ 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 false dtnvs' cons'' thy'';
- val thy' = thy'' |> Domain_Syntax.add_syntax false 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 = drop (find_index (fn s => s = "'") ss + 1) ss;
- fun one_con (con,args,mx) =
+ check_and_sort_domain false dtnvs' cons'' thy;
+(* val thy = Domain_Syntax.add_syntax eqs' thy; *)
+ val dts : typ list = map (Type o fst) eqs';
+ val new_dts : (string * string list) list =
+ map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
+ fun one_con (con,args,mx) : cons =
(Binding.name_of con, (* FIXME preverse binding (!?) *)
- mx,
ListPair.map (fn ((lazy,sel,tp),vn) =>
- mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp),
- Option.map Binding.name_of sel,vn))
- (args, Datatype_Prop.make_tnames (map third args))
- ) : cons;
+ mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn))
+ (args, Datatype_Prop.make_tnames (map third args)));
val eqs : eq list =
map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
- val thy = thy' |> Domain_Axioms.add_axioms false eqs' eqs;
+
+ 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 repTs : typ list = map mk_eq_typ eqs';
+ val dom_eqns : (binding * (typ * typ)) list = dbinds ~~ (dts ~~ repTs);
+ val thy = Domain_Axioms.add_axioms dom_eqns thy;
+
val ((rewss, take_rews), theorems_thy) =
thy
|> fold_map (fn (eq, (x,cs)) =>
@@ -185,59 +206,62 @@
(comp_dnam : string)
(eqs''' : ((string * string option) list * binding * mixfix *
(binding * (bool * binding option * 'a) list * mixfix) list) list)
- (thy''' : theory) =
+ (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 : (binding * typ list * mixfix) list =
+ let
+ fun readS (SOME s) = Syntax.read_sort_global thy s
+ | readS NONE = Sign.defaultS thy;
+ fun readTFree (a, s) = TFree (a, readS s);
+ in
+ map (fn (vs,dname:binding,mx,_) =>
+ (dname, map readTFree vs, mx)) eqs'''
+ 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, @{sort rep});
+ (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'''
+ 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 cons''' :
+ (binding * (bool * binding option * 'a) list * mixfix) list list =
+ map (fn (_,_,_,cons) => cons) eqs''';
+ 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;
+ 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;
+ 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 (iso_infos, thy'') = thy''' |>
+ val (iso_infos, thy) = thy |>
Domain_Isomorphism.domain_isomorphism
(map (fn ((vs, dname, mx, _), eq) =>
(map fst vs, dname, mx, mk_eq_typ eq, NONE))
(eqs''' ~~ eqs'))
- val thy' = thy'' |> Domain_Syntax.add_syntax true 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 = drop (find_index (fn s => s = "'") ss + 1) ss;
- fun one_con (con,args,mx) =
+ val dts : typ list = map (Type o fst) eqs';
+ val new_dts : (string * string list) list =
+ map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
+ fun one_con (con,args,mx) : cons =
(Binding.name_of con, (* FIXME preverse binding (!?) *)
- mx,
ListPair.map (fn ((lazy,sel,tp),vn) =>
- mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp),
- Option.map Binding.name_of sel,vn))
+ mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn))
(args, Datatype_Prop.make_tnames (map 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 eqs' eqs;
val ((rewss, take_rews), theorems_thy) =
thy
|> fold_map (fn (eq, (x,cs)) =>
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Mar 03 08:43:48 2010 +0100
@@ -6,37 +6,17 @@
signature DOMAIN_ISOMORPHISM =
sig
- type iso_info =
- {
- repT : typ,
- absT : typ,
- rep_const : term,
- abs_const : term,
- rep_inverse : thm,
- abs_inverse : thm
- }
val domain_isomorphism :
(string list * binding * mixfix * typ * (binding * binding) option) list
- -> theory -> iso_info list * theory
+ -> theory -> Domain_Take_Proofs.iso_info list * theory
val domain_isomorphism_cmd :
(string list * binding * mixfix * string * (binding * binding) option) list
-> theory -> theory
val add_type_constructor :
(string * term * string * thm * thm * thm * thm) -> theory -> theory
- val get_map_tab :
- theory -> string Symtab.table
- val define_take_functions :
- (binding * iso_info) list -> theory ->
- { take_consts : term list,
- take_defs : thm list,
- chain_take_thms : thm list,
- take_0_thms : thm list,
- take_Suc_thms : thm list,
- deflation_take_thms : thm list
- } * theory;
end;
-structure Domain_Isomorphism :> DOMAIN_ISOMORPHISM =
+structure Domain_Isomorphism : DOMAIN_ISOMORPHISM =
struct
val beta_ss =
@@ -53,47 +33,51 @@
structure DeflData = Theory_Data
(
+ (* terms like "foo_defl" *)
type T = term Symtab.table;
val empty = Symtab.empty;
val extend = I;
fun merge data = Symtab.merge (K true) data;
);
-structure MapData = Theory_Data
+structure RepData = Theory_Data
(
- type T = string Symtab.table;
- val empty = Symtab.empty;
- val extend = I;
- fun merge data = Symtab.merge (K true) data;
-);
-
-structure Thm_List : THEORY_DATA_ARGS =
-struct
+ (* theorems like "REP('a foo) = foo_defl$REP('a)" *)
type T = thm list;
val empty = [];
val extend = I;
val merge = Thm.merge_thms;
-end;
-
-structure RepData = Theory_Data (Thm_List);
+);
-structure IsodeflData = Theory_Data (Thm_List);
+structure MapIdData = Theory_Data
+(
+ (* theorems like "foo_map$ID = ID" *)
+ type T = thm list;
+ val empty = [];
+ val extend = I;
+ val merge = Thm.merge_thms;
+);
-structure MapIdData = Theory_Data (Thm_List);
-
-structure DeflMapData = Theory_Data (Thm_List);
+structure IsodeflData = Theory_Data
+(
+ (* theorems like "isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)" *)
+ 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, map_ID_thm, defl_map_thm) =
DeflData.map (Symtab.insert (K true) (tname, defl_const))
- #> MapData.map (Symtab.insert (K true) (tname, map_name))
+ #> Domain_Take_Proofs.add_map_function (tname, map_name, defl_map_thm)
#> RepData.map (Thm.add_thm REP_thm)
#> IsodeflData.map (Thm.add_thm isodefl_thm)
- #> MapIdData.map (Thm.add_thm map_ID_thm)
- #> DeflMapData.map (Thm.add_thm defl_map_thm);
+ #> MapIdData.map (Thm.add_thm map_ID_thm);
-val get_map_tab = MapData.get;
+
+(* val get_map_tab = MapData.get; *)
(******************************************************************************)
@@ -142,17 +126,7 @@
(****************************** isomorphism info ******************************)
(******************************************************************************)
-type iso_info =
- {
- absT : typ,
- repT : typ,
- abs_const : term,
- rep_const : term,
- abs_inverse : thm,
- rep_inverse : thm
- }
-
-fun deflation_abs_rep (info : iso_info) : thm =
+fun deflation_abs_rep (info : Domain_Take_Proofs.iso_info) : thm =
let
val abs_iso = #abs_inverse info;
val rep_iso = #rep_inverse info;
@@ -250,22 +224,6 @@
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 => list_ccomb (Const (t, mapT T), map map_of Ts)
- | NONE => if is_closed_typ T
- then mk_ID T
- else error ("map_of_typ: type variable under unsupported type constructor " ^ c);
- in map_of T end;
-
(******************************************************************************)
(********************* declaring definitions and theorems *********************)
@@ -293,217 +251,6 @@
||> Sign.parent_path;
(******************************************************************************)
-(************************** defining take functions ***************************)
-(******************************************************************************)
-
-fun define_take_functions
- (spec : (binding * iso_info) list)
- (thy : theory) =
- let
-
- (* retrieve components of spec *)
- val dom_binds = map fst spec;
- val iso_infos = map snd spec;
- val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos;
- val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos;
- val dnames = map Binding.name_of dom_binds;
-
- (* get table of map functions *)
- val map_tab = MapData.get thy;
-
- fun mk_projs [] t = []
- | mk_projs (x::[]) t = [(x, t)]
- | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);
-
- fun mk_cfcomp2 ((rep_const, abs_const), f) =
- mk_cfcomp (abs_const, mk_cfcomp (f, rep_const));
-
- (* defining map functions over dtyps *)
- fun copy_of_dtyp recs (T, dt) =
- if Datatype_Aux.is_rec_type dt
- then copy_of_dtyp' recs (T, dt)
- else mk_ID T
- and copy_of_dtyp' recs (T, Datatype_Aux.DtRec i) = nth recs i
- | copy_of_dtyp' recs (T, Datatype_Aux.DtTFree a) = mk_ID T
- | copy_of_dtyp' recs (T, Datatype_Aux.DtType (c, ds)) =
- case Symtab.lookup map_tab c of
- SOME f =>
- list_ccomb
- (Const (f, mapT T),
- map (copy_of_dtyp recs) (snd (dest_Type T) ~~ ds))
- | NONE =>
- (warning ("copy_of_dtyp: unknown type constructor " ^ c); mk_ID T);
-
- (* define take functional *)
- val new_dts : (string * string list) list =
- map (apsnd (map (fst o dest_TFree)) o dest_Type o fst) dom_eqns;
- val copy_arg_type = mk_tupleT (map (fn (T, _) => T ->> T) dom_eqns);
- val copy_arg = Free ("f", copy_arg_type);
- val copy_args = map snd (mk_projs dom_binds copy_arg);
- fun one_copy_rhs (rep_abs, (lhsT, rhsT)) =
- let
- val dtyp = Datatype_Aux.dtyp_of_typ new_dts rhsT;
- val body = copy_of_dtyp copy_args (rhsT, dtyp);
- in
- mk_cfcomp2 (rep_abs, body)
- end;
- val take_functional =
- big_lambda copy_arg
- (mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns)));
- val take_rhss =
- let
- val i = Free ("i", HOLogic.natT);
- val rhs = mk_iterate (i, take_functional)
- in
- map (Term.lambda i o snd) (mk_projs dom_binds rhs)
- end;
-
- (* define take constants *)
- fun define_take_const ((tbind, take_rhs), (lhsT, rhsT)) thy =
- let
- val take_type = HOLogic.natT --> lhsT ->> lhsT;
- val take_bind = Binding.suffix_name "_take" tbind;
- val (take_const, thy) =
- Sign.declare_const ((take_bind, take_type), NoSyn) thy;
- val take_eqn = Logic.mk_equals (take_const, take_rhs);
- val (take_def_thm, thy) =
- thy
- |> Sign.add_path (Binding.name_of tbind)
- |> yield_singleton
- (PureThy.add_defs false o map Thm.no_attributes)
- (Binding.name "take_def", take_eqn)
- ||> Sign.parent_path;
- in ((take_const, take_def_thm), thy) end;
- val ((take_consts, take_defs), thy) = thy
- |> fold_map define_take_const (dom_binds ~~ take_rhss ~~ dom_eqns)
- |>> ListPair.unzip;
-
- (* prove chain_take lemmas *)
- fun prove_chain_take (take_const, dname) thy =
- let
- val goal = mk_trp (mk_chain take_const);
- val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd};
- val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
- val chain_take_thm = Goal.prove_global thy [] [] goal (K tac);
- in
- add_qualified_thm "chain_take" (dname, chain_take_thm) thy
- end;
- val (chain_take_thms, thy) =
- fold_map prove_chain_take (take_consts ~~ dnames) thy;
-
- (* prove take_0 lemmas *)
- fun prove_take_0 ((take_const, dname), (lhsT, rhsT)) thy =
- let
- val lhs = take_const $ @{term "0::nat"};
- val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT));
- val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict};
- val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
- val take_0_thm = Goal.prove_global thy [] [] goal (K tac);
- in
- add_qualified_thm "take_0" (dname, take_0_thm) thy
- end;
- val (take_0_thms, thy) =
- fold_map prove_take_0 (take_consts ~~ dnames ~~ dom_eqns) thy;
-
- (* prove take_Suc lemmas *)
- val i = Free ("i", natT);
- val take_is = map (fn t => t $ i) take_consts;
- fun prove_take_Suc
- (((take_const, rep_abs), dname), (lhsT, rhsT)) thy =
- let
- val lhs = take_const $ (@{term Suc} $ i);
- val dtyp = Datatype_Aux.dtyp_of_typ new_dts rhsT;
- val body = copy_of_dtyp take_is (rhsT, dtyp);
- val rhs = mk_cfcomp2 (rep_abs, body);
- val goal = mk_eqs (lhs, rhs);
- val simps = @{thms iterate_Suc fst_conv snd_conv}
- val rules = take_defs @ simps;
- val tac = simp_tac (beta_ss addsimps rules) 1;
- val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac);
- in
- add_qualified_thm "take_Suc" (dname, take_Suc_thm) thy
- end;
- val (take_Suc_thms, thy) =
- fold_map prove_take_Suc
- (take_consts ~~ rep_abs_consts ~~ dnames ~~ dom_eqns) thy;
-
- (* prove deflation theorems for take functions *)
- val deflation_abs_rep_thms = map deflation_abs_rep iso_infos;
- val deflation_take_thm =
- let
- val i = Free ("i", natT);
- fun mk_goal take_const = mk_deflation (take_const $ i);
- val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts));
- val adm_rules =
- @{thms adm_conj adm_subst [OF _ adm_deflation]
- cont2cont_fst cont2cont_snd cont_id};
- val bottom_rules =
- take_0_thms @ @{thms deflation_UU simp_thms};
- val deflation_rules =
- @{thms conjI deflation_ID}
- @ deflation_abs_rep_thms
- @ DeflMapData.get thy;
- in
- Goal.prove_global thy [] [] goal (fn _ =>
- EVERY
- [rtac @{thm nat.induct} 1,
- simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
- asm_simp_tac (HOL_basic_ss addsimps take_Suc_thms) 1,
- REPEAT (etac @{thm conjE} 1
- ORELSE resolve_tac deflation_rules 1
- ORELSE atac 1)])
- end;
- 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 (deflation_take_thms, thy) =
- fold_map (add_qualified_thm "deflation_take")
- (map (apsnd Drule.export_without_context)
- (conjuncts dnames deflation_take_thm)) thy;
-
- (* prove strictness of take functions *)
- fun prove_take_strict (take_const, dname) thy =
- let
- val goal = mk_trp (mk_strict (take_const $ Free ("i", natT)));
- val tac = rtac @{thm deflation_strict} 1
- THEN resolve_tac deflation_take_thms 1;
- val take_strict_thm = Goal.prove_global thy [] [] goal (K tac);
- in
- add_qualified_thm "take_strict" (dname, take_strict_thm) thy
- end;
- val (take_strict_thms, thy) =
- fold_map prove_take_strict (take_consts ~~ dnames) thy;
-
- (* prove take/take rules *)
- fun prove_take_take ((chain_take, deflation_take), dname) thy =
- let
- val take_take_thm =
- @{thm deflation_chain_min} OF [chain_take, deflation_take];
- in
- add_qualified_thm "take_take" (dname, take_take_thm) thy
- end;
- val (take_take_thms, thy) =
- fold_map prove_take_take
- (chain_take_thms ~~ deflation_take_thms ~~ dnames) thy;
-
- val result =
- {
- take_consts = take_consts,
- take_defs = take_defs,
- chain_take_thms = chain_take_thms,
- take_0_thms = take_0_thms,
- take_Suc_thms = take_Suc_thms,
- deflation_take_thms = deflation_take_thms
- };
-
- in
- (result, thy)
- end;
-
-(******************************************************************************)
(******************************* main function ********************************)
(******************************************************************************)
@@ -529,7 +276,7 @@
(prep_typ: theory -> 'a -> (string * sort) list -> typ * (string * sort) list)
(doms_raw: (string list * binding * mixfix * 'a * (binding * binding) option) list)
(thy: theory)
- : iso_info list * theory =
+ : Domain_Take_Proofs.iso_info list * theory =
let
val _ = Theory.requires thy "Representable" "domain isomorphisms";
@@ -669,7 +416,7 @@
|>> ListPair.unzip;
(* collect info about rep/abs *)
- val iso_infos : iso_info list =
+ val iso_infos : Domain_Take_Proofs.iso_info list =
let
fun mk_info (((lhsT, rhsT), (repC, absC)), (rep_iso, abs_iso)) =
{
@@ -696,19 +443,24 @@
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);
+ local
+ fun unprime a = Library.unprefix "'" a;
+ fun mapvar T = Free (unprime (fst (dest_TFree T)), T ->> T);
+ fun map_lhs (map_const, lhsT) =
+ (lhsT, list_ccomb (map_const, map mapvar (snd (dest_Type lhsT))));
+ val tab1 = map map_lhs (map_consts ~~ map fst dom_eqns);
+ val Ts = (snd o dest_Type o fst o hd) dom_eqns;
+ val tab = (Ts ~~ map mapvar Ts) @ tab1;
+ fun mk_map_spec (((rep_const, abs_const), map_const), (lhsT, rhsT)) =
+ let
+ val lhs = Domain_Take_Proofs.map_of_typ thy tab lhsT;
+ val body = Domain_Take_Proofs.map_of_typ thy tab rhsT;
+ val rhs = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const));
+ in mk_eqs (lhs, rhs) end;
+ in
+ val map_specs =
+ map mk_map_spec (rep_abs_consts ~~ map_consts ~~ dom_eqns);
+ end;
(* register recursive definition of map functions *)
val map_binds = map (Binding.suffix_name "_map") dom_binds;
@@ -816,7 +568,7 @@
val deflation_rules =
@{thms conjI deflation_ID}
@ deflation_abs_rep_thms
- @ DeflMapData.get thy;
+ @ Domain_Take_Proofs.get_deflation_thms thy;
in
Goal.prove_global thy [] assms goal (fn {prems, ...} =>
EVERY
@@ -834,13 +586,25 @@
val (deflation_map_thms, thy) = thy |>
(PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.export_without_context))
(conjuncts deflation_map_binds deflation_map_thm);
- val thy = DeflMapData.map (fold Thm.add_thm deflation_map_thms) thy;
+
+ (* register map functions in theory data *)
+ local
+ fun register_map ((dname, map_name), defl_thm) =
+ Domain_Take_Proofs.add_map_function (dname, map_name, defl_thm);
+ val dnames = map (fst o dest_Type o fst) dom_eqns;
+ val map_names = map (fst o dest_Const) map_consts;
+ in
+ val thy =
+ fold register_map (dnames ~~ map_names ~~ deflation_map_thms) thy;
+ end;
(* definitions and proofs related to take functions *)
val (take_info, thy) =
- define_take_functions (dom_binds ~~ iso_infos) thy;
- val {take_consts, take_defs, chain_take_thms, take_0_thms,
- take_Suc_thms, deflation_take_thms} = take_info;
+ Domain_Take_Proofs.define_take_functions
+ (dom_binds ~~ iso_infos) thy;
+ val { take_consts, take_defs, chain_take_thms, take_0_thms,
+ take_Suc_thms, deflation_take_thms,
+ finite_consts, finite_defs } = take_info;
(* least-upper-bound lemma for take functions *)
val lub_take_lemma =
--- a/src/HOLCF/Tools/Domain/domain_library.ML Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_library.ML Wed Mar 03 08:43:48 2010 +0100
@@ -93,13 +93,12 @@
(* Domain specifications *)
eqtype arg;
- type cons = string * mixfix * arg list;
+ type cons = string * arg list;
type eq = (string * typ list) * cons list;
- val mk_arg : (bool * Datatype.dtyp) * string option * string -> arg;
+ val mk_arg : (bool * Datatype.dtyp) * string -> arg;
val is_lazy : arg -> bool;
val rec_of : arg -> int;
val dtyp_of : arg -> Datatype.dtyp;
- val sel_of : arg -> string option;
val vname : arg -> string;
val upd_vname : (string -> string) -> arg -> arg;
val is_rec : arg -> bool;
@@ -108,8 +107,6 @@
val nonlazy_rec : arg list -> string list;
val %# : arg -> term;
val /\# : arg * term -> term;
- val when_body : cons list -> (int * int -> term) -> term;
- val when_funs : 'a list -> string list;
val bound_arg : ''a list -> ''a -> term; (* ''a = arg or string *)
val idx_name : 'a list -> string -> int -> string;
val app_rec_arg : (int -> term) -> arg -> term;
@@ -186,12 +183,10 @@
type arg =
(bool * Datatype.dtyp) * (* (lazy, recursive element) *)
- string option * (* selector name *)
string; (* argument name *)
type cons =
string * (* operator name of constr *)
- mixfix * (* mixfix syntax of constructor *)
arg list; (* argument list *)
type eq =
@@ -201,15 +196,14 @@
val mk_arg = I;
-fun rec_of ((_,dtyp),_,_) =
+fun rec_of ((_,dtyp),_) =
case dtyp of Datatype_Aux.DtRec i => i | _ => ~1;
(* FIXME: what about indirect recursion? *)
-fun is_lazy arg = fst (first arg);
-fun dtyp_of arg = snd (first arg);
-val sel_of = second;
-val vname = third;
-val upd_vname = upd_third;
+fun is_lazy arg = fst (fst arg);
+fun dtyp_of arg = snd (fst arg);
+val vname = snd;
+val upd_vname = apsnd;
fun is_rec arg = rec_of arg >=0;
fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
fun nonlazy args = map vname (filter_out is_lazy args);
@@ -219,8 +213,8 @@
(* ----- combinators for making dtyps ----- *)
fun mk_uD T = Datatype_Aux.DtType(@{type_name "u"}, [T]);
-fun mk_sprodD (T, U) = Datatype_Aux.DtType(@{type_name "**"}, [T, U]);
-fun mk_ssumD (T, U) = Datatype_Aux.DtType(@{type_name "++"}, [T, U]);
+fun mk_sprodD (T, U) = Datatype_Aux.DtType(@{type_name sprod}, [T, U]);
+fun mk_ssumD (T, U) = Datatype_Aux.DtType(@{type_name ssum}, [T, U]);
fun mk_liftD T = Datatype_Aux.DtType(@{type_name "lift"}, [T]);
val unitD = Datatype_Aux.DtType(@{type_name "unit"}, []);
val boolD = Datatype_Aux.DtType(@{type_name "bool"}, []);
@@ -229,17 +223,17 @@
fun big_sprodD ds = case ds of [] => oneD | _ => foldr1 mk_sprodD ds;
fun big_ssumD ds = case ds of [] => unitD | _ => foldr1 mk_ssumD ds;
-fun dtyp_of_arg ((lazy, D), _, _) = if lazy then mk_uD D else D;
-fun dtyp_of_cons (_, _, args) = big_sprodD (map dtyp_of_arg args);
+fun dtyp_of_arg ((lazy, D), _) = if lazy then mk_uD D else D;
+fun dtyp_of_cons (_, args) = big_sprodD (map dtyp_of_arg args);
fun dtyp_of_eq (_, cons) = big_ssumD (map dtyp_of_cons cons);
(* ----- support for type and mixfix expressions ----- *)
fun mk_uT T = Type(@{type_name "u"}, [T]);
-fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
-fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]);
-fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]);
+fun mk_cfunT (T, U) = Type(@{type_name cfun}, [T, U]);
+fun mk_sprodT (T, U) = Type(@{type_name sprod}, [T, U]);
+fun mk_ssumT (T, U) = Type(@{type_name ssum}, [T, U]);
val oneT = @{typ one};
val op ->> = mk_cfunT;
@@ -330,23 +324,5 @@
| cont_eta_contract t = t;
fun idx_name dnames s n = s^(if length dnames = 1 then "" else string_of_int n);
-fun when_funs cons = if length cons = 1 then ["f"]
- else mapn (fn n => K("f"^(string_of_int n))) 1 cons;
-fun when_body cons funarg =
- let
- fun one_fun n (_,_,[] ) = /\ "dummy" (funarg(1,n))
- | one_fun n (_,_,args) = let
- val l2 = length args;
- fun idxs m arg = (if is_lazy arg then (fn t => mk_fup (ID, t))
- else I) (Bound(l2-m));
- in cont_eta_contract
- (foldr''
- (fn (a,t) => mk_ssplit (/\# (a,t)))
- (args,
- fn a=> /\#(a,(list_ccomb(funarg(l2,n),mapn idxs 1 args))))
- ) end;
- in (if length cons = 1 andalso length(third(hd cons)) <= 1
- then mk_strictify else I)
- (foldr1 mk_sscase (mapn one_fun 1 cons)) end;
end; (* struct *)
--- a/src/HOLCF/Tools/Domain/domain_syntax.ML Wed Mar 03 08:28:33 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-(* Title: HOLCF/Tools/Domain/domain_syntax.ML
- Author: David von Oheimb
-
-Syntax generator for domain command.
-*)
-
-signature DOMAIN_SYNTAX =
-sig
- val calc_syntax:
- theory ->
- bool ->
- (string * typ list) *
- (binding * (bool * binding option * typ) list * mixfix) list ->
- (binding * typ * mixfix) list
-
- val add_syntax:
- bool ->
- ((string * typ list) *
- (binding * (bool * binding option * typ) list * mixfix) list) list ->
- theory -> theory
-end;
-
-
-structure Domain_Syntax :> DOMAIN_SYNTAX =
-struct
-
-open Domain_Library;
-infixr 5 -->; infixr 6 ->>;
-
-fun calc_syntax thy
- (definitional : bool)
- ((dname : string, typevars : typ list),
- (cons': (binding * (bool * binding option * typ) list * mixfix) list))
- : (binding * typ * mixfix) list =
- 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);
- 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);
- end;
-
- val const_finite = (dbind "_finite", dtype-->HOLogic.boolT , NoSyn);
-
- val optional_consts =
- if definitional then [] else [const_rep, const_abs];
-
- in (optional_consts @ [const_finite])
- end; (* let *)
-
-(* ----- putting all the syntax stuff together ------------------------------ *)
-
-fun add_syntax
- (definitional : bool)
- (eqs' : ((string * typ list) *
- (binding * (bool * binding option * typ) list * mixfix) list) list)
- (thy'' : theory) =
- let
- val ctt : (binding * typ * mixfix) list list =
- map (calc_syntax thy'' definitional) eqs';
- in thy''
- |> Cont_Consts.add_consts (flat ctt)
- end; (* let *)
-
-end; (* struct *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Wed Mar 03 08:43:48 2010 +0100
@@ -0,0 +1,421 @@
+(* Title: HOLCF/Tools/domain/domain_take_proofs.ML
+ Author: Brian Huffman
+
+Defines take functions for the given domain equation
+and proves related theorems.
+*)
+
+signature DOMAIN_TAKE_PROOFS =
+sig
+ type iso_info =
+ {
+ absT : typ,
+ repT : typ,
+ abs_const : term,
+ rep_const : term,
+ abs_inverse : thm,
+ rep_inverse : thm
+ }
+
+ val define_take_functions :
+ (binding * iso_info) list -> theory ->
+ { take_consts : term list,
+ take_defs : thm list,
+ chain_take_thms : thm list,
+ take_0_thms : thm list,
+ take_Suc_thms : thm list,
+ deflation_take_thms : thm list,
+ finite_consts : term list,
+ finite_defs : thm list
+ } * theory
+
+ val map_of_typ :
+ theory -> (typ * term) list -> typ -> term
+
+ val add_map_function :
+ (string * string * thm) -> theory -> theory
+
+ val get_map_tab : theory -> string Symtab.table
+ val get_deflation_thms : theory -> thm list
+end;
+
+structure Domain_Take_Proofs : DOMAIN_TAKE_PROOFS =
+struct
+
+type iso_info =
+ {
+ absT : typ,
+ repT : typ,
+ abs_const : term,
+ rep_const : term,
+ abs_inverse : thm,
+ rep_inverse : thm
+ };
+
+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 MapData = Theory_Data
+(
+ (* constant names like "foo_map" *)
+ type T = string Symtab.table;
+ val empty = Symtab.empty;
+ val extend = I;
+ fun merge data = Symtab.merge (K true) data;
+);
+
+structure DeflMapData = Theory_Data
+(
+ (* theorems like "deflation a ==> deflation (foo_map$a)" *)
+ type T = thm list;
+ val empty = [];
+ val extend = I;
+ val merge = Thm.merge_thms;
+);
+
+fun add_map_function (tname, map_name, deflation_map_thm) =
+ MapData.map (Symtab.insert (K true) (tname, map_name))
+ #> DeflMapData.map (Thm.add_thm deflation_map_thm);
+
+val get_map_tab = MapData.get;
+val get_deflation_thms = DeflMapData.get;
+
+(******************************************************************************)
+(************************** building types and terms **************************)
+(******************************************************************************)
+
+open HOLCF_Library;
+
+infixr 6 ->>;
+infix -->>;
+infix 9 `;
+
+val deflT = @{typ "udom alg_defl"};
+
+fun mapT (T as Type (_, Ts)) =
+ (map (fn T => T ->> T) Ts) -->> (T ->> T)
+ | mapT T = T ->> T;
+
+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);
+
+fun mk_deflation t =
+ Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t;
+
+fun mk_lub t =
+ let
+ val T = Term.range_type (Term.fastype_of t);
+ val lub_const = Const (@{const_name lub}, (T --> boolT) --> T);
+ val UNIV_const = @{term "UNIV :: nat set"};
+ val image_type = (natT --> T) --> (natT --> boolT) --> T --> boolT;
+ val image_const = Const (@{const_name image}, image_type);
+ in
+ lub_const $ (image_const $ t $ UNIV_const)
+ end;
+
+(* 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));
+
+(******************************************************************************)
+(****************************** isomorphism info ******************************)
+(******************************************************************************)
+
+fun deflation_abs_rep (info : iso_info) : thm =
+ let
+ val abs_iso = #abs_inverse info;
+ val rep_iso = #rep_inverse info;
+ val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso];
+ in
+ Drule.export_without_context thm
+ end
+
+(******************************************************************************)
+(********************* building map functions over types **********************)
+(******************************************************************************)
+
+fun map_of_typ (thy : theory) (sub : (typ * term) list) (T : typ) : term =
+ let
+ val map_tab = get_map_tab thy;
+ fun auto T = T ->> T;
+ fun map_of T =
+ case AList.lookup (op =) sub T of
+ SOME m => (m, true) | NONE => map_of' T
+ and map_of' (T as (Type (c, Ts))) =
+ (case Symtab.lookup map_tab c of
+ SOME map_name =>
+ let
+ val map_type = map auto Ts -->> auto T;
+ val (ms, bs) = map_split map_of Ts;
+ in
+ if exists I bs
+ then (list_ccomb (Const (map_name, map_type), ms), true)
+ else (mk_ID T, false)
+ end
+ | NONE => (mk_ID T, false))
+ | map_of' T = (mk_ID T, false);
+ in
+ fst (map_of T)
+ end;
+
+
+(******************************************************************************)
+(********************* declaring definitions and theorems *********************)
+(******************************************************************************)
+
+fun define_const
+ (bind : binding, rhs : term)
+ (thy : theory)
+ : (term * thm) * theory =
+ let
+ val typ = Term.fastype_of rhs;
+ val (const, thy) = Sign.declare_const ((bind, typ), NoSyn) thy;
+ val eqn = Logic.mk_equals (const, rhs);
+ val def = Thm.no_attributes (Binding.suffix_name "_def" bind, eqn);
+ val (def_thm, thy) = yield_singleton (PureThy.add_defs false) def thy;
+ in
+ ((const, def_thm), thy)
+ end;
+
+fun add_qualified_thm name (path, thm) thy =
+ thy
+ |> Sign.add_path path
+ |> yield_singleton PureThy.add_thms
+ (Thm.no_attributes (Binding.name name, thm))
+ ||> Sign.parent_path;
+
+(******************************************************************************)
+(************************** defining take functions ***************************)
+(******************************************************************************)
+
+fun define_take_functions
+ (spec : (binding * iso_info) list)
+ (thy : theory) =
+ let
+
+ (* retrieve components of spec *)
+ val dom_binds = map fst spec;
+ val iso_infos = map snd spec;
+ val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos;
+ val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos;
+ val dnames = map Binding.name_of dom_binds;
+
+ (* get table of map functions *)
+ val map_tab = MapData.get thy;
+
+ fun mk_projs [] t = []
+ | mk_projs (x::[]) t = [(x, t)]
+ | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);
+
+ fun mk_cfcomp2 ((rep_const, abs_const), f) =
+ mk_cfcomp (abs_const, mk_cfcomp (f, rep_const));
+
+ (* define take functional *)
+ val newTs : typ list = map fst dom_eqns;
+ val copy_arg_type = mk_tupleT (map (fn T => T ->> T) newTs);
+ val copy_arg = Free ("f", copy_arg_type);
+ val copy_args = map snd (mk_projs dom_binds copy_arg);
+ fun one_copy_rhs (rep_abs, (lhsT, rhsT)) =
+ let
+ val body = map_of_typ thy (newTs ~~ copy_args) rhsT;
+ in
+ mk_cfcomp2 (rep_abs, body)
+ end;
+ val take_functional =
+ big_lambda copy_arg
+ (mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns)));
+ val take_rhss =
+ let
+ val i = Free ("i", HOLogic.natT);
+ val rhs = mk_iterate (i, take_functional)
+ in
+ map (Term.lambda i o snd) (mk_projs dom_binds rhs)
+ end;
+
+ (* define take constants *)
+ fun define_take_const ((tbind, take_rhs), (lhsT, rhsT)) thy =
+ let
+ val take_type = HOLogic.natT --> lhsT ->> lhsT;
+ val take_bind = Binding.suffix_name "_take" tbind;
+ val (take_const, thy) =
+ Sign.declare_const ((take_bind, take_type), NoSyn) thy;
+ val take_eqn = Logic.mk_equals (take_const, take_rhs);
+ val (take_def_thm, thy) =
+ thy
+ |> Sign.add_path (Binding.name_of tbind)
+ |> yield_singleton
+ (PureThy.add_defs false o map Thm.no_attributes)
+ (Binding.name "take_def", take_eqn)
+ ||> Sign.parent_path;
+ in ((take_const, take_def_thm), thy) end;
+ val ((take_consts, take_defs), thy) = thy
+ |> fold_map define_take_const (dom_binds ~~ take_rhss ~~ dom_eqns)
+ |>> ListPair.unzip;
+
+ (* prove chain_take lemmas *)
+ fun prove_chain_take (take_const, dname) thy =
+ let
+ val goal = mk_trp (mk_chain take_const);
+ val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd};
+ val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
+ val chain_take_thm = Goal.prove_global thy [] [] goal (K tac);
+ in
+ add_qualified_thm "chain_take" (dname, chain_take_thm) thy
+ end;
+ val (chain_take_thms, thy) =
+ fold_map prove_chain_take (take_consts ~~ dnames) thy;
+
+ (* prove take_0 lemmas *)
+ fun prove_take_0 ((take_const, dname), (lhsT, rhsT)) thy =
+ let
+ val lhs = take_const $ @{term "0::nat"};
+ val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT));
+ val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict};
+ val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
+ val take_0_thm = Goal.prove_global thy [] [] goal (K tac);
+ in
+ add_qualified_thm "take_0" (dname, take_0_thm) thy
+ end;
+ val (take_0_thms, thy) =
+ fold_map prove_take_0 (take_consts ~~ dnames ~~ dom_eqns) thy;
+
+ (* prove take_Suc lemmas *)
+ val i = Free ("i", natT);
+ val take_is = map (fn t => t $ i) take_consts;
+ fun prove_take_Suc
+ (((take_const, rep_abs), dname), (lhsT, rhsT)) thy =
+ let
+ val lhs = take_const $ (@{term Suc} $ i);
+ val body = map_of_typ thy (newTs ~~ take_is) rhsT;
+ val rhs = mk_cfcomp2 (rep_abs, body);
+ val goal = mk_eqs (lhs, rhs);
+ val simps = @{thms iterate_Suc fst_conv snd_conv}
+ val rules = take_defs @ simps;
+ val tac = simp_tac (beta_ss addsimps rules) 1;
+ val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac);
+ in
+ add_qualified_thm "take_Suc" (dname, take_Suc_thm) thy
+ end;
+ val (take_Suc_thms, thy) =
+ fold_map prove_take_Suc
+ (take_consts ~~ rep_abs_consts ~~ dnames ~~ dom_eqns) thy;
+
+ (* prove deflation theorems for take functions *)
+ val deflation_abs_rep_thms = map deflation_abs_rep iso_infos;
+ val deflation_take_thm =
+ let
+ val i = Free ("i", natT);
+ fun mk_goal take_const = mk_deflation (take_const $ i);
+ val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts));
+ val adm_rules =
+ @{thms adm_conj adm_subst [OF _ adm_deflation]
+ cont2cont_fst cont2cont_snd cont_id};
+ val bottom_rules =
+ take_0_thms @ @{thms deflation_UU simp_thms};
+ val deflation_rules =
+ @{thms conjI deflation_ID}
+ @ deflation_abs_rep_thms
+ @ DeflMapData.get thy;
+ in
+ Goal.prove_global thy [] [] goal (fn _ =>
+ EVERY
+ [rtac @{thm nat.induct} 1,
+ simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
+ asm_simp_tac (HOL_basic_ss addsimps take_Suc_thms) 1,
+ REPEAT (etac @{thm conjE} 1
+ ORELSE resolve_tac deflation_rules 1
+ ORELSE atac 1)])
+ end;
+ 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 (deflation_take_thms, thy) =
+ fold_map (add_qualified_thm "deflation_take")
+ (map (apsnd Drule.export_without_context)
+ (conjuncts dnames deflation_take_thm)) thy;
+
+ (* prove strictness of take functions *)
+ fun prove_take_strict (take_const, dname) thy =
+ let
+ val goal = mk_trp (mk_strict (take_const $ Free ("i", natT)));
+ val tac = rtac @{thm deflation_strict} 1
+ THEN resolve_tac deflation_take_thms 1;
+ val take_strict_thm = Goal.prove_global thy [] [] goal (K tac);
+ in
+ add_qualified_thm "take_strict" (dname, take_strict_thm) thy
+ end;
+ val (take_strict_thms, thy) =
+ fold_map prove_take_strict (take_consts ~~ dnames) thy;
+
+ (* prove take/take rules *)
+ fun prove_take_take ((chain_take, deflation_take), dname) thy =
+ let
+ val take_take_thm =
+ @{thm deflation_chain_min} OF [chain_take, deflation_take];
+ in
+ add_qualified_thm "take_take" (dname, take_take_thm) thy
+ end;
+ val (take_take_thms, thy) =
+ fold_map prove_take_take
+ (chain_take_thms ~~ deflation_take_thms ~~ dnames) thy;
+
+ (* define finiteness predicates *)
+ fun define_finite_const ((tbind, take_const), (lhsT, rhsT)) thy =
+ let
+ val finite_type = lhsT --> boolT;
+ val finite_bind = Binding.suffix_name "_finite" tbind;
+ val (finite_const, thy) =
+ Sign.declare_const ((finite_bind, finite_type), NoSyn) thy;
+ val x = Free ("x", lhsT);
+ val i = Free ("i", natT);
+ val finite_rhs =
+ lambda x (HOLogic.exists_const natT $
+ (lambda i (mk_eq (mk_capply (take_const $ i, x), x))));
+ val finite_eqn = Logic.mk_equals (finite_const, finite_rhs);
+ val (finite_def_thm, thy) =
+ thy
+ |> Sign.add_path (Binding.name_of tbind)
+ |> yield_singleton
+ (PureThy.add_defs false o map Thm.no_attributes)
+ (Binding.name "finite_def", finite_eqn)
+ ||> Sign.parent_path;
+ in ((finite_const, finite_def_thm), thy) end;
+ val ((finite_consts, finite_defs), thy) = thy
+ |> fold_map define_finite_const (dom_binds ~~ take_consts ~~ dom_eqns)
+ |>> ListPair.unzip;
+
+ val result =
+ {
+ take_consts = take_consts,
+ take_defs = take_defs,
+ chain_take_thms = chain_take_thms,
+ take_0_thms = take_0_thms,
+ take_Suc_thms = take_Suc_thms,
+ deflation_take_thms = deflation_take_thms,
+ finite_consts = finite_consts,
+ finite_defs = finite_defs
+ };
+
+ in
+ (result, thy)
+ end;
+
+end;
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Wed Mar 03 08:43:48 2010 +0100
@@ -95,10 +95,6 @@
InductTacs.case_tac ctxt (v^"=UU") i THEN
asm_simp_tac (HOLCF_ss addsimps rews) i;
-val chain_tac =
- REPEAT_DETERM o resolve_tac
- [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL, ch2ch_fst, ch2ch_snd];
-
(* ----- general proofs ----------------------------------------------------- *)
val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp}
@@ -110,7 +106,7 @@
let
val _ = message ("Proving isomorphism properties of domain "^dname^" ...");
-val map_tab = Domain_Isomorphism.get_map_tab thy;
+val map_tab = Domain_Take_Proofs.get_map_tab thy;
(* ----- getting the axioms and definitions --------------------------------- *)
@@ -143,7 +139,7 @@
val abs_const = Const(dname^"_abs", rhsT ->> lhsT);
-val iso_info : Domain_Isomorphism.iso_info =
+val iso_info : Domain_Take_Proofs.iso_info =
{
absT = lhsT,
repT = rhsT,
@@ -171,8 +167,6 @@
val pg = pg' thy;
-val dc_copy = %%:(dname^"_copy");
-
val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
val iso_rews = map Drule.export_without_context [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
@@ -182,10 +176,11 @@
local
fun dc_take dn = %%:(dn^"_take");
val dnames = map (fst o fst) eqs;
- fun get_take_strict dn = PureThy.get_thm thy (dn ^ ".take_strict");
- val axs_take_strict = map get_take_strict dnames;
+ val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy;
+ fun get_deflation_take dn = PureThy.get_thm thy (dn ^ ".deflation_take");
+ val axs_deflation_take = map get_deflation_take dnames;
- fun one_take_app (con, _, args) =
+ fun one_take_app (con, args) =
let
fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
fun one_rhs arg =
@@ -195,13 +190,11 @@
else (%# arg);
val lhs = (dc_take dname $ (%%:"Suc" $ %:"n"))`(con_app con args);
val rhs = con_app2 con one_rhs args;
- fun is_rec arg = Datatype_Aux.is_rec_type (dtyp_of arg);
- fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
- fun nonlazy_rec args = map vname (filter is_nonlazy_rec args);
- val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
val goal = mk_trp (lhs === rhs);
val rules = [ax_take_Suc, ax_abs_iso, @{thm cfcomp2}];
- val rules2 = @{thms take_con_rules ID1} @ axs_take_strict;
+ val rules2 =
+ @{thms take_con_rules ID1 deflation_strict}
+ @ deflation_thms @ axs_deflation_take;
val tacs =
[simp_tac (HOL_basic_ss addsimps rules) 1,
asm_simp_tac (HOL_basic_ss addsimps rules2) 1];
@@ -239,7 +232,7 @@
fun comp_theorems (comp_dnam, eqs: eq list) thy =
let
-val map_tab = Domain_Isomorphism.get_map_tab thy;
+val map_tab = Domain_Take_Proofs.get_map_tab thy;
val dnames = map (fst o fst) eqs;
val conss = map snd eqs;
@@ -273,7 +266,7 @@
val dnames = map (fst o fst) eqs;
val x_name = idx_name dnames "x";
- fun one_con (con, _, args) =
+ fun one_con (con, args) =
let
val nonrec_args = filter_out is_rec args;
val rec_args = filter is_rec args;
@@ -353,7 +346,7 @@
maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;
local
- fun one_con p (con, _, args) =
+ fun one_con p (con, args) =
let
val P_names = map P_name (1 upto (length dnames));
val vns = Name.variant_list P_names (map vname args);
@@ -377,7 +370,7 @@
fun ind_prems_tac prems = EVERY
(maps (fn cons =>
(resolve_tac prems 1 ::
- maps (fn (_,_,args) =>
+ maps (fn (_,args) =>
resolve_tac prems 1 ::
map (K(atac 1)) (nonlazy args) @
map (K(atac 1)) (filter is_rec args))
@@ -392,7 +385,7 @@
((rec_of arg = n andalso nfn(lazy_rec orelse is_lazy arg)) orelse
rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns)
(lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
- ) o third) cons;
+ ) o snd) cons;
fun all_rec_to ns = rec_to forall not all_rec_to ns;
fun warn (n,cons) =
if all_rec_to [] false (n,cons)
@@ -424,14 +417,14 @@
(* FIXME! case_UU_tac *)
case_UU_tac context (prems @ con_rews) 1
(List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
- fun con_tacs (con, _, args) =
+ fun con_tacs (con, args) =
asm_simp_tac take_ss 1 ::
map arg_tac (filter is_nonlazy_rec args) @
[resolve_tac prems 1] @
map (K (atac 1)) (nonlazy args) @
map (K (etac spec 1)) (filter is_rec args);
fun cases_tacs (cons, cases) =
- res_inst_tac context [(("x", 0), "x")] cases 1 ::
+ res_inst_tac context [(("y", 0), "x")] cases 1 ::
asm_simp_tac (take_ss addsimps prems) 1 ::
maps con_tacs cons;
in
@@ -500,13 +493,13 @@
etac disjE 1,
asm_simp_tac (HOL_ss addsimps con_rews) 1,
asm_simp_tac take_ss 1];
- fun con_tacs ctxt (con, _, args) =
+ fun con_tacs ctxt (con, args) =
asm_simp_tac take_ss 1 ::
maps (arg_tacs ctxt) (nonlazy_rec args);
fun foo_tacs ctxt n (cons, cases) =
simp_tac take_ss 1 ::
rtac allI 1 ::
- res_inst_tac ctxt [(("x", 0), x_name n)] cases 1 ::
+ res_inst_tac ctxt [(("y", 0), x_name n)] cases 1 ::
asm_simp_tac take_ss 1 ::
maps (con_tacs ctxt) cons;
fun tacs ctxt =
--- a/src/HOLCF/Tools/cont_consts.ML Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOLCF/Tools/cont_consts.ML Wed Mar 03 08:43:48 2010 +0100
@@ -56,7 +56,7 @@
trans_rules (syntax c2) (syntax c1) n mx)
end;
-fun cfun_arity (Type (n, [_, T])) = if n = @{type_name "->"} then 1 + cfun_arity T else 0
+fun cfun_arity (Type (n, [_, T])) = if n = @{type_name cfun} then 1 + cfun_arity T else 0
| cfun_arity _ = 0;
fun is_contconst (_, _, NoSyn) = false
--- a/src/HOLCF/Tools/fixrec.ML Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOLCF/Tools/fixrec.ML Wed Mar 03 08:43:48 2010 +0100
@@ -22,10 +22,15 @@
structure Fixrec :> FIXREC =
struct
+open HOLCF_Library;
+
+infixr 6 ->>;
+infix -->>;
+infix 9 `;
+
val def_cont_fix_eq = @{thm def_cont_fix_eq};
val def_cont_fix_ind = @{thm def_cont_fix_ind};
-
fun fixrec_err s = error ("fixrec definition error:\n" ^ s);
fun fixrec_eq_err thy s eq =
fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq));
@@ -34,42 +39,23 @@
(***************************** 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 maybeT T = Type(@{type_name "maybe"}, [T]);
-
-fun dest_maybeT (Type(@{type_name "maybe"}, [T])) = T
- | dest_maybeT T = raise TYPE ("dest_maybeT", [T], []);
-
-fun tupleT [] = HOLogic.unitT
- | tupleT [T] = T
- | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts);
-
local
-fun binder_cfun (Type(@{type_name "->"},[T, U])) = T :: binder_cfun U
+fun binder_cfun (Type(@{type_name cfun},[T, U])) = T :: binder_cfun U
| binder_cfun (Type(@{type_name "fun"},[T, U])) = T :: binder_cfun U
| binder_cfun _ = [];
-fun body_cfun (Type(@{type_name "->"},[T, U])) = body_cfun U
+fun body_cfun (Type(@{type_name cfun},[T, U])) = body_cfun U
| body_cfun (Type(@{type_name "fun"},[T, U])) = body_cfun U
| body_cfun T = T;
fun strip_cfun T : typ list * typ =
(binder_cfun T, body_cfun T);
-fun cfunsT (Ts, U) = List.foldr cfunT U Ts;
-
in
-fun matchT (T, U) =
- body_cfun T ->> cfunsT (binder_cfun T, U) ->> U;
+fun matcherT (T, U) =
+ body_cfun T ->> (binder_cfun T -->> U) ->> U;
end
@@ -86,43 +72,8 @@
fun chead_of (Const(@{const_name Rep_CFun},_)$f$t) = chead_of f
| chead_of u = u;
-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
-
-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;
-
infix 0 ==; val (op ==) = Logic.mk_equals;
infix 1 ===; val (op ===) = HOLogic.mk_eq;
-infix 9 ` ; val (op `) = mk_capply;
-
-(* 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_return t =
- let val T = Term.fastype_of t
- in Const(@{const_name Fixrec.return}, T ->> maybeT T) ` t end;
-
-fun mk_bind (t, u) =
- let val (T, mU) = dest_cfunT (Term.fastype_of u);
- val bindT = maybeT T ->> (T ->> mU) ->> mU;
- in Const(@{const_name Fixrec.bind}, bindT) ` t ` u end;
fun mk_mplus (t, u) =
let val mT = Term.fastype_of t
@@ -130,31 +81,9 @@
fun mk_run t =
let val mT = Term.fastype_of t
- val T = dest_maybeT mT
+ val T = dest_matchT mT
in Const(@{const_name Fixrec.run}, mT ->> T) ` t end;
-fun mk_fix t =
- let val (T, _) = dest_cfunT (Term.fastype_of t)
- in Const(@{const_name fix}, (T ->> T) ->> T) ` t end;
-
-fun mk_cont t =
- let val T = Term.fastype_of t
- in Const(@{const_name cont}, T --> HOLogic.boolT) $ t end;
-
-val mk_fst = HOLogic.mk_fst
-val mk_snd = HOLogic.mk_snd
-
-(* 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));
-
(*************************************************************************)
(************* fixed-point definitions and unfolding theorems ************)
@@ -288,11 +217,11 @@
| Const(c,T) =>
let
val n = Name.variant taken "v";
- fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs
+ fun result_type (Type(@{type_name cfun},[_,T])) (x::xs) = result_type T xs
| result_type (Type (@{type_name "fun"},[_,T])) (x::xs) = result_type T xs
| result_type T _ = T;
val v = Free(n, result_type T vs);
- val m = Const(match_name c, matchT (T, fastype_of rhs));
+ val m = Const(match_name c, matcherT (T, fastype_of rhs));
val k = big_lambdas vs rhs;
in
(m`v`k, v, n::taken)
@@ -340,7 +269,7 @@
val msum = foldr1 mk_mplus (map (unLAM arity) ms);
val (Ts, U) = LAM_Ts arity (hd ms)
in
- reLAM (rev Ts, dest_maybeT U) (mk_run msum)
+ reLAM (rev Ts, dest_matchT U) (mk_run msum)
end;
(* this is the pattern-matching compiler function *)
--- a/src/HOLCF/Tools/holcf_library.ML Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOLCF/Tools/holcf_library.ML Wed Mar 03 08:43:48 2010 +0100
@@ -51,12 +51,12 @@
(*** Continuous function space ***)
(* ->> is taken from holcf_logic.ML *)
-fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
+fun mk_cfunT (T, U) = Type(@{type_name cfun}, [T, U]);
val (op ->>) = mk_cfunT;
val (op -->>) = Library.foldr mk_cfunT;
-fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
+fun dest_cfunT (Type(@{type_name cfun}, [T, U])) = (T, U)
| dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
fun capply_const (S, T) =
@@ -84,7 +84,7 @@
fun mk_capply (t, u) =
let val (S, T) =
case fastype_of t of
- Type(@{type_name "->"}, [S, T]) => (S, T)
+ Type(@{type_name cfun}, [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;
@@ -153,9 +153,9 @@
val oneT = @{typ "one"};
-fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]);
+fun mk_sprodT (T, U) = Type(@{type_name sprod}, [T, U]);
-fun dest_sprodT (Type(@{type_name "**"}, [T, U])) = (T, U)
+fun dest_sprodT (Type(@{type_name sprod}, [T, U])) = (T, U)
| dest_sprodT T = raise TYPE ("dest_sprodT", [T], []);
fun spair_const (T, U) =
@@ -179,9 +179,9 @@
(*** Strict sum type ***)
-fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]);
+fun mk_ssumT (T, U) = Type(@{type_name ssum}, [T, U]);
-fun dest_ssumT (Type(@{type_name "++"}, [T, U])) = (T, U)
+fun dest_ssumT (Type(@{type_name ssum}, [T, U])) = (T, U)
| dest_ssumT T = raise TYPE ("dest_ssumT", [T], []);
fun sinl_const (T, U) = Const(@{const_name sinl}, T ->> mk_ssumT (T, U));
--- a/src/HOLCF/Tools/repdef.ML Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOLCF/Tools/repdef.ML Wed Mar 03 08:43:48 2010 +0100
@@ -20,32 +20,28 @@
structure Repdef :> REPDEF =
struct
+open HOLCF_Library;
+
+infixr 6 ->>;
+infix -->>;
+
(** type definitions **)
type rep_info =
{ emb_def: thm, prj_def: thm, approx_def: thm, REP: thm };
-(* building terms *)
+(* building types and terms *)
-fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
-fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
-
-fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
-
-val natT = @{typ nat};
val udomT = @{typ udom};
fun alg_deflT T = Type (@{type_name alg_defl}, [T]);
-fun cfunT (T, U) = Type (@{type_name "->"}, [T, U]);
-fun emb_const T = Const (@{const_name emb}, cfunT (T, udomT));
-fun prj_const T = Const (@{const_name prj}, cfunT (udomT, T));
-fun approx_const T = Const (@{const_name approx}, natT --> cfunT (T, T));
+fun emb_const T = Const (@{const_name emb}, T ->> udomT);
+fun prj_const T = Const (@{const_name prj}, udomT ->> T);
+fun approx_const T = Const (@{const_name approx}, natT --> (T ->> T));
-fun LAM_const (T, U) = Const (@{const_name Abs_CFun}, (T --> U) --> cfunT (T, U));
-fun APP_const (T, U) = Const (@{const_name Rep_CFun}, cfunT (T, U) --> (T --> U));
-fun cast_const T = Const (@{const_name cast}, cfunT (alg_deflT T, cfunT (T, T)));
+fun cast_const T = Const (@{const_name cast}, alg_deflT T ->> T ->> T);
fun mk_cast (t, x) =
- APP_const (udomT, udomT)
- $ (APP_const (alg_deflT udomT, cfunT (udomT, udomT)) $ cast_const udomT $ t)
+ capply_const (udomT, udomT)
+ $ (capply_const (alg_deflT udomT, udomT ->> udomT) $ cast_const udomT $ t)
$ x;
(* manipulating theorems *)
@@ -99,12 +95,12 @@
(*definitions*)
val Rep_const = Const (#Rep_name info, newT --> udomT);
val Abs_const = Const (#Abs_name info, udomT --> newT);
- val emb_eqn = Logic.mk_equals (emb_const newT, LAM_const (newT, udomT) $ Rep_const);
- val prj_eqn = Logic.mk_equals (prj_const newT, LAM_const (udomT, newT) $
+ val emb_eqn = Logic.mk_equals (emb_const newT, cabs_const (newT, udomT) $ Rep_const);
+ val prj_eqn = Logic.mk_equals (prj_const newT, cabs_const (udomT, newT) $
Abs ("x", udomT, Abs_const $ mk_cast (defl, Bound 0)));
val repdef_approx_const =
Const (@{const_name repdef_approx}, (newT --> udomT) --> (udomT --> newT)
- --> alg_deflT udomT --> natT --> cfunT (newT, newT));
+ --> alg_deflT udomT --> natT --> (newT ->> newT));
val approx_eqn = Logic.mk_equals (approx_const newT,
repdef_approx_const $ Rep_const $ Abs_const $ defl);
--- a/src/HOLCF/ex/Dnat.thy Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOLCF/ex/Dnat.thy Wed Mar 03 08:43:48 2010 +0100
@@ -55,12 +55,12 @@
apply (induct_tac x rule: dnat.ind)
apply fast
apply (rule allI)
- apply (rule_tac x = y in dnat.casedist)
+ apply (case_tac y)
apply simp
apply simp
apply simp
apply (rule allI)
- apply (rule_tac x = y in dnat.casedist)
+ apply (case_tac y)
apply (fast intro!: UU_I)
apply (thin_tac "ALL y. dnat << y --> dnat = UU | dnat = y")
apply simp
--- a/src/HOLCF/ex/Stream.thy Wed Mar 03 08:28:33 2010 +0100
+++ b/src/HOLCF/ex/Stream.thy Wed Mar 03 08:43:48 2010 +0100
@@ -290,12 +290,12 @@
lemma stream_finite_lemma1: "stream_finite xs ==> stream_finite (x && xs)"
apply (simp add: stream.finite_def,auto)
-apply (rule_tac x="Suc n" in exI)
+apply (rule_tac x="Suc i" in exI)
by (simp add: stream_take_lemma4)
lemma stream_finite_lemma2: "[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs"
apply (simp add: stream.finite_def, auto)
-apply (rule_tac x="n" in exI)
+apply (rule_tac x="i" in exI)
by (erule stream_take_lemma3,simp)
lemma stream_finite_rt_eq: "stream_finite (rt$s) = stream_finite s"