# HG changeset patch # User haftmann # Date 1267602228 -3600 # Node ID 00f3bbadbb2dd616d8e73742cff765d0a603970f # Parent 743e8ca36b18bc8314b3bebda5ca539155141d93# Parent 14d8d72f8b1fd1836471e3ec81d981ef60612738 merged diff -r 14d8d72f8b1f -r 00f3bbadbb2d doc-src/TutorialI/Protocol/NS_Public.thy --- 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) \Nonce NA, Agent A\)"} may be extended by an event of the form @{term [display,indent=5] "Says B A (Crypt (pubK A) \Nonce NA, Nonce NB, Agent B\)"} -where @{text NB} is a fresh nonce: @{term "Nonce NB \ used evs2"}. +where @{text NB} is a fresh nonce: @{term "Nonce NB \ 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 diff -r 14d8d72f8b1f -r 00f3bbadbb2d doc-src/TutorialI/Protocol/document/NS_Public.tex --- 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 diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOL/IsaMakefile --- 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 diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOL/List.thy --- 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 diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOL/ZF/HOLZF.thy --- 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) diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOL/ZF/Helper.thy --- 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 \ (!! x. P x \ Q x) \ 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 \ range f & z \ (f ` x)) = (z \ f ` x)" - by auto - -lemma f_x_in_range_f: "f x \ range f" - by (blast intro: image_eqI) - -lemma comp_inj: "inj f \ inj g \ 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 diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOL/ZF/Zet.thy --- 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 \ 'a zet \ 'a zet" where diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/Bifinite.thy --- 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\f\x = approx n\(f\(approx n\x))" by (simp add: approx_cfun_def) diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/Cfun.thy --- 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" ("(_ \/ _)" [1,0]0) +type_notation (xsymbols) + cfun ("(_ \/ _)" [1, 0] 0) notation Rep_CFun ("(_$/_)" [999,1000] 999) @@ -103,16 +103,16 @@ lemma UU_CFun: "\ \ 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 = diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/Domain.thy --- 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" diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/FOCUS/Fstream.thy --- 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) diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/Fixrec.thy --- 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 *} diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/IOA/meta_theory/Seq.thy --- 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< 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: "\Finite x; x \ y\ \ 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 diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/IOA/meta_theory/Sequence.thy --- 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 diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/IsaMakefile --- 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 \ diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/Representable.thy --- 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\prj\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\emb\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\emb\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}, diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/Sprod.thy --- 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 \ 'b. p = \ \ (fst p \ \ \ snd p \ \)}" 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" ("(_ \/ _)" [21,20] 20) + sprod :: "[type, type] => type" ("(_ \/ _)" [21,20] 20) syntax (HTML output) - "**" :: "[type, type] => type" ("(_ \/ _)" [21,20] 20) + sprod :: "[type, type] => type" ("(_ \/ _)" [21,20] 20) lemma spair_lemma: "(strictify\(\ b. a)\b, strictify\(\ a. b)\a) \ Sprod" @@ -80,11 +80,11 @@ apply fast done -lemma sprodE [cases type: **]: +lemma sprodE [cases type: sprod]: "\p = \ \ Q; \x y. \p = (:x, y:); x \ \; y \ \\ \ Q\ \ Q" by (cut_tac z=p in Exh_Sprod, auto) -lemma sprod_induct [induct type: **]: +lemma sprod_induct [induct type: sprod]: "\P \; \x y. \x \ \; y \ \\ \ P (:x, y:)\ \ 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 \ 'b" assume "x \ y" thus "x = \ \ x = y" @@ -312,7 +312,7 @@ subsection {* Strict product is a bifinite domain *} -instantiation "**" :: (bifinite, bifinite) bifinite +instantiation sprod :: (bifinite, bifinite) bifinite begin definition diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/Ssum.thy --- 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 \ ('a \ 'b). (fst p \ TT \ snd (snd p) = \) \ (fst p \ FF \ fst (snd p) = \)}" 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" ("(_ \/ _)" [21, 20] 20) + ssum :: "[type, type] => type" ("(_ \/ _)" [21, 20] 20) syntax (HTML output) - "++" :: "[type, type] => type" ("(_ \/ _)" [21, 20] 20) + ssum :: "[type, type] => type" ("(_ \/ _)" [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]: "\p = \ \ Q; \x. \p = sinl\x; x \ \\ \ Q; \y. \p = sinr\y; y \ \\ \ Q\ \ Q" by (cut_tac z=p in Exh_Ssum, auto) -lemma ssum_induct [induct type: ++]: +lemma ssum_induct [induct type: ssum]: "\P \; \x. x \ \ \ P (sinl\x); \y. y \ \ \ P (sinr\y)\ \ 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 diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/Tools/Domain/domain_axioms.ML --- 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 *) diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/Tools/Domain/domain_constructors.ML --- 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 diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/Tools/Domain/domain_extender.ML --- 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)) => diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/Tools/Domain/domain_isomorphism.ML --- 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 = diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/Tools/Domain/domain_library.ML --- 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 *) diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/Tools/Domain/domain_syntax.ML --- 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 *) diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/Tools/Domain/domain_take_proofs.ML --- /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; diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/Tools/Domain/domain_theorems.ML --- 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 = diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/Tools/cont_consts.ML --- 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 diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/Tools/fixrec.ML --- 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 *) diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/Tools/holcf_library.ML --- 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)); diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/Tools/repdef.ML --- 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); diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/ex/Dnat.thy --- 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 diff -r 14d8d72f8b1f -r 00f3bbadbb2d src/HOLCF/ex/Stream.thy --- 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"