--- a/src/HOL/Auth/Message.thy Tue Jul 21 11:01:07 2009 +0200
+++ b/src/HOL/Auth/Message.thy Tue Jul 21 11:13:47 2009 +0200
@@ -856,6 +856,8 @@
Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
+fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
+
(*Apply rules to break down assumptions of the form
Y \<in> parts(insert X H) and Y \<in> analz(insert X H)
*)
--- a/src/HOL/PReal.thy Tue Jul 21 11:01:07 2009 +0200
+++ b/src/HOL/PReal.thy Tue Jul 21 11:13:47 2009 +0200
@@ -52,7 +52,7 @@
definition
psup :: "preal set => preal" where
- "psup P = Abs_preal (\<Union>X \<in> P. Rep_preal X)"
+ [code del]: "psup P = Abs_preal (\<Union>X \<in> P. Rep_preal X)"
definition
add_set :: "[rat set,rat set] => rat set" where
--- a/src/HOL/SET-Protocol/MessageSET.thy Tue Jul 21 11:01:07 2009 +0200
+++ b/src/HOL/SET-Protocol/MessageSET.thy Tue Jul 21 11:13:47 2009 +0200
@@ -854,6 +854,8 @@
Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
+fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
+
(*Apply rules to break down assumptions of the form
Y \<in> parts(insert X H) and Y \<in> analz(insert X H)
*)
--- a/src/HOL/Set.thy Tue Jul 21 11:01:07 2009 +0200
+++ b/src/HOL/Set.thy Tue Jul 21 11:13:47 2009 +0200
@@ -80,12 +80,30 @@
lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}"
by simp
+text {*
+Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}
+to the front (and similarly for @{text "t=x"}):
+*}
+
+setup {*
+let
+ val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
+ ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
+ DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
+ val defColl_regroup = Simplifier.simproc @{theory}
+ "defined Collect" ["{x. P x & Q x}"]
+ (Quantifier1.rearrange_Coll Coll_perm_tac)
+in
+ Simplifier.map_simpset (fn ss => ss addsimprocs [defColl_regroup])
+end
+*}
+
lemmas CollectE = CollectD [elim_format]
text {* Set enumerations *}
definition empty :: "'a set" ("{}") where
- "empty \<equiv> {x. False}"
+ "empty = {x. False}"
definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
@@ -311,6 +329,23 @@
in [("Collect", setcompr_tr')] end;
*}
+setup {*
+let
+ val unfold_bex_tac = unfold_tac @{thms "Bex_def"};
+ fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
+ val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
+ val unfold_ball_tac = unfold_tac @{thms "Ball_def"};
+ fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
+ val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
+ val defBEX_regroup = Simplifier.simproc @{theory}
+ "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
+ val defBALL_regroup = Simplifier.simproc @{theory}
+ "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
+in
+ Simplifier.map_simpset (fn ss => ss addsimprocs [defBALL_regroup, defBEX_regroup])
+end
+*}
+
lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"
by (simp add: Ball_def)
@@ -319,20 +354,6 @@
lemma bspec [dest?]: "ALL x:A. P x ==> x:A ==> P x"
by (simp add: Ball_def)
-lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"
- by (unfold Ball_def) blast
-
-ML {* bind_thm ("rev_ballE", Thm.permute_prems 1 1 @{thm ballE}) *}
-
-text {*
- \medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and
- @{prop "a:A"}; creates assumption @{prop "P a"}.
-*}
-
-ML {*
- fun ball_tac i = etac @{thm ballE} i THEN contr_tac (i + 1)
-*}
-
text {*
Gives better instantiation for bound:
*}
@@ -341,6 +362,26 @@
Classical.map_cs (fn cs => cs addbefore ("bspec", datac @{thm bspec} 1))
*}
+ML {*
+structure Simpdata =
+struct
+
+open Simpdata;
+
+val mksimps_pairs = [(@{const_name Ball}, @{thms bspec})] @ mksimps_pairs;
+
+end;
+
+open Simpdata;
+*}
+
+declaration {* fn _ =>
+ Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
+*}
+
+lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"
+ by (unfold Ball_def) blast
+
lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x"
-- {* Normally the best argument order: @{prop "P x"} constrains the
choice of @{prop "x:A"}. *}
@@ -382,24 +423,6 @@
lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)"
by blast
-ML {*
- local
- val unfold_bex_tac = unfold_tac @{thms "Bex_def"};
- fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
- val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
-
- val unfold_ball_tac = unfold_tac @{thms "Ball_def"};
- fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
- val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
- in
- val defBEX_regroup = Simplifier.simproc @{theory}
- "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
- val defBALL_regroup = Simplifier.simproc @{theory}
- "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
- end;
-
- Addsimprocs [defBALL_regroup, defBEX_regroup];
-*}
text {* Congruence rules *}
@@ -450,25 +473,12 @@
\medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
*}
-ML {*
- fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
-*}
-
lemma subsetCE [elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
-- {* Classical elimination rule. *}
by (unfold mem_def) blast
lemma subset_eq: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
-text {*
- \medskip Takes assumptions @{prop "A \<subseteq> B"}; @{prop "c \<in> A"} and
- creates the assumption @{prop "c \<in> B"}.
-*}
-
-ML {*
- fun set_mp_tac i = etac @{thm subsetCE} i THEN mp_tac i
-*}
-
lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
by blast
@@ -538,7 +548,7 @@
subsubsection {* The universal set -- UNIV *}
definition UNIV :: "'a set" where
- "UNIV \<equiv> {x. True}"
+ "UNIV = {x. True}"
lemma UNIV_I [simp]: "x : UNIV"
by (simp add: UNIV_def)
@@ -647,7 +657,7 @@
subsubsection {* Binary union -- Un *}
definition Un :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
- "A Un B \<equiv> {x. x \<in> A \<or> x \<in> B}"
+ "A Un B = {x. x \<in> A \<or> x \<in> B}"
notation (xsymbols)
"Un" (infixl "\<union>" 65)
@@ -678,7 +688,7 @@
lemma UnE [elim!]: "c : A Un B ==> (c:A ==> P) ==> (c:B ==> P) ==> P"
by (unfold Un_def) blast
-lemma insert_def: "insert a B \<equiv> {x. x = a} \<union> B"
+lemma insert_def: "insert a B = {x. x = a} \<union> B"
by (simp add: Collect_def mem_def insert_compr Un_def)
lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
@@ -690,7 +700,7 @@
subsubsection {* Binary intersection -- Int *}
definition Int :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
- "A Int B \<equiv> {x. x \<in> A \<and> x \<in> B}"
+ "A Int B = {x. x \<in> A \<and> x \<in> B}"
notation (xsymbols)
"Int" (infixl "\<inter>" 70)
@@ -883,34 +893,15 @@
by blast
-subsubsection {* Some proof tools *}
+subsubsection {* Some rules with @{text "if"} *}
text{* Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}. *}
lemma Collect_conv_if: "{x. x=a & P x} = (if P a then {a} else {})"
-by auto
+ by auto
lemma Collect_conv_if2: "{x. a=x & P x} = (if P a then {a} else {})"
-by auto
-
-text {*
-Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}
-to the front (and similarly for @{text "t=x"}):
-*}
-
-ML{*
- local
- val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
- ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
- DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
- in
- val defColl_regroup = Simplifier.simproc @{theory}
- "defined Collect" ["{x. P x & Q x}"]
- (Quantifier1.rearrange_Coll Coll_perm_tac)
- end;
-
- Addsimprocs [defColl_regroup];
-*}
+ by auto
text {*
Rewrite rules for boolean case-splitting: faster than @{text
@@ -945,13 +936,6 @@
("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
*)
-ML {*
- val mksimps_pairs = [(@{const_name Ball}, @{thms bspec})] @ mksimps_pairs;
-*}
-declaration {* fn _ =>
- Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
-*}
-
subsection {* Complete lattices *}
@@ -1029,10 +1013,10 @@
using top_greatest [of x] by (simp add: le_iff_inf inf_commute)
definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
- "SUPR A f == \<Squnion> (f ` A)"
+ "SUPR A f = \<Squnion> (f ` A)"
definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
- "INFI A f == \<Sqinter> (f ` A)"
+ "INFI A f = \<Sqinter> (f ` A)"
end
@@ -1136,10 +1120,43 @@
by rule (simp add: Sup_fun_def, simp add: empty_def)
+subsubsection {* Union *}
+
+definition Union :: "'a set set \<Rightarrow> 'a set" where
+ Union_eq [code del]: "Union A = {x. \<exists>B \<in> A. x \<in> B}"
+
+notation (xsymbols)
+ Union ("\<Union>_" [90] 90)
+
+lemma Sup_set_eq:
+ "\<Squnion>S = \<Union>S"
+proof (rule set_ext)
+ fix x
+ have "(\<exists>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<exists>A\<in>S. x \<in> A)"
+ by auto
+ then show "x \<in> \<Squnion>S \<longleftrightarrow> x \<in> \<Union>S"
+ by (simp add: Sup_fun_def Sup_bool_def Union_eq) (simp add: mem_def)
+qed
+
+lemma Union_iff [simp, noatp]:
+ "A \<in> \<Union>C \<longleftrightarrow> (\<exists>X\<in>C. A\<in>X)"
+ by (unfold Union_eq) blast
+
+lemma UnionI [intro]:
+ "X \<in> C \<Longrightarrow> A \<in> X \<Longrightarrow> A \<in> \<Union>C"
+ -- {* The order of the premises presupposes that @{term C} is rigid;
+ @{term A} may be flexible. *}
+ by auto
+
+lemma UnionE [elim!]:
+ "A \<in> \<Union>C \<Longrightarrow> (\<And>X. A\<in>X \<Longrightarrow> X\<in>C \<Longrightarrow> R) \<Longrightarrow> R"
+ by auto
+
+
subsubsection {* Unions of families *}
definition UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
- "UNION A B \<equiv> {y. \<exists>x\<in>A. y \<in> B x}"
+ UNION_eq_Union_image: "UNION A B = \<Union>(B`A)"
syntax
"@UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" [0, 10] 10)
@@ -1177,8 +1194,22 @@
in [(@{const_syntax UNION}, btr' "@UNION")] end
*}
-declare UNION_def [noatp]
-
+lemma SUPR_set_eq:
+ "(SUP x:S. f x) = (\<Union>x\<in>S. f x)"
+ by (simp add: SUPR_def UNION_eq_Union_image Sup_set_eq)
+
+lemma Union_def:
+ "\<Union>S = (\<Union>x\<in>S. x)"
+ by (simp add: UNION_eq_Union_image image_def)
+
+lemma UNION_def [noatp]:
+ "UNION A B = {y. \<exists>x\<in>A. y \<in> B x}"
+ by (auto simp add: UNION_eq_Union_image Union_eq)
+
+lemma Union_image_eq [simp]:
+ "\<Union>(B`A) = (\<Union>x\<in>A. B x)"
+ by (rule sym) (fact UNION_eq_Union_image)
+
lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)"
by (unfold UNION_def) blast
@@ -1202,10 +1233,49 @@
by blast
+subsubsection {* Inter *}
+
+definition Inter :: "'a set set \<Rightarrow> 'a set" where
+ Inter_eq [code del]: "Inter A = {x. \<forall>B \<in> A. x \<in> B}"
+
+notation (xsymbols)
+ Inter ("\<Inter>_" [90] 90)
+
+lemma Inf_set_eq:
+ "\<Sqinter>S = \<Inter>S"
+proof (rule set_ext)
+ fix x
+ have "(\<forall>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<forall>A\<in>S. x \<in> A)"
+ by auto
+ then show "x \<in> \<Sqinter>S \<longleftrightarrow> x \<in> \<Inter>S"
+ by (simp add: Inter_eq Inf_fun_def Inf_bool_def) (simp add: mem_def)
+qed
+
+lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
+ by (unfold Inter_eq) blast
+
+lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
+ by (simp add: Inter_eq)
+
+text {*
+ \medskip A ``destruct'' rule -- every @{term X} in @{term C}
+ contains @{term A} as an element, but @{prop "A:X"} can hold when
+ @{prop "X:C"} does not! This rule is analogous to @{text spec}.
+*}
+
+lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X"
+ by auto
+
+lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"
+ -- {* ``Classical'' elimination rule -- does not require proving
+ @{prop "X:C"}. *}
+ by (unfold Inter_eq) blast
+
+
subsubsection {* Intersections of families *}
definition INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
- "INTER A B \<equiv> {y. \<forall>x\<in>A. y \<in> B x}"
+ INTER_eq_Inter_image: "INTER A B = \<Inter>(B`A)"
syntax
"@INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" [0, 10] 10)
@@ -1234,6 +1304,22 @@
in [(@{const_syntax INTER}, btr' "@INTER")] end
*}
+lemma INFI_set_eq:
+ "(INF x:S. f x) = (\<Inter>x\<in>S. f x)"
+ by (simp add: INFI_def INTER_eq_Inter_image Inf_set_eq)
+
+lemma Inter_def:
+ "Inter S = INTER S (\<lambda>x. x)"
+ by (simp add: INTER_eq_Inter_image image_def)
+
+lemma INTER_def:
+ "INTER A B = {y. \<forall>x\<in>A. y \<in> B x}"
+ by (auto simp add: INTER_eq_Inter_image Inter_eq)
+
+lemma Inter_image_eq [simp]:
+ "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
+ by (rule sym) (fact INTER_eq_Inter_image)
+
lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)"
by (unfold INTER_def) blast
@@ -1252,99 +1338,6 @@
by (simp add: INTER_def)
-subsubsection {* Union *}
-
-definition Union :: "'a set set \<Rightarrow> 'a set" where
- "Union S \<equiv> UNION S (\<lambda>x. x)"
-
-notation (xsymbols)
- Union ("\<Union>_" [90] 90)
-
-lemma Union_image_eq [simp]:
- "\<Union>(B`A) = (\<Union>x\<in>A. B x)"
- by (auto simp add: Union_def UNION_def image_def)
-
-lemma Union_eq:
- "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
- by (simp add: Union_def UNION_def)
-
-lemma Sup_set_eq:
- "\<Squnion>S = \<Union>S"
-proof (rule set_ext)
- fix x
- have "(\<exists>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<exists>A\<in>S. x \<in> A)"
- by auto
- then show "x \<in> \<Squnion>S \<longleftrightarrow> x \<in> \<Union>S"
- by (simp add: Union_eq Sup_fun_def Sup_bool_def) (simp add: mem_def)
-qed
-
-lemma SUPR_set_eq:
- "(SUP x:S. f x) = (\<Union>x\<in>S. f x)"
- by (simp add: SUPR_def Sup_set_eq)
-
-lemma Union_iff [simp,noatp]: "(A : Union C) = (EX X:C. A:X)"
- by (unfold Union_def) blast
-
-lemma UnionI [intro]: "X:C ==> A:X ==> A : Union C"
- -- {* The order of the premises presupposes that @{term C} is rigid;
- @{term A} may be flexible. *}
- by auto
-
-lemma UnionE [elim!]: "A : Union C ==> (!!X. A:X ==> X:C ==> R) ==> R"
- by (unfold Union_def) blast
-
-
-subsubsection {* Inter *}
-
-definition Inter :: "'a set set \<Rightarrow> 'a set" where
- "Inter S \<equiv> INTER S (\<lambda>x. x)"
-
-notation (xsymbols)
- Inter ("\<Inter>_" [90] 90)
-
-lemma Inter_image_eq [simp]:
- "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
- by (auto simp add: Inter_def INTER_def image_def)
-
-lemma Inter_eq:
- "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
- by (simp add: Inter_def INTER_def)
-
-lemma Inf_set_eq:
- "\<Sqinter>S = \<Inter>S"
-proof (rule set_ext)
- fix x
- have "(\<forall>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<forall>A\<in>S. x \<in> A)"
- by auto
- then show "x \<in> \<Sqinter>S \<longleftrightarrow> x \<in> \<Inter>S"
- by (simp add: Inter_eq Inf_fun_def Inf_bool_def) (simp add: mem_def)
-qed
-
-lemma INFI_set_eq:
- "(INF x:S. f x) = (\<Inter>x\<in>S. f x)"
- by (simp add: INFI_def Inf_set_eq)
-
-lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
- by (unfold Inter_def) blast
-
-lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
- by (simp add: Inter_def)
-
-text {*
- \medskip A ``destruct'' rule -- every @{term X} in @{term C}
- contains @{term A} as an element, but @{prop "A:X"} can hold when
- @{prop "X:C"} does not! This rule is analogous to @{text spec}.
-*}
-
-lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X"
- by auto
-
-lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"
- -- {* ``Classical'' elimination rule -- does not require proving
- @{prop "X:C"}. *}
- by (unfold Inter_def) blast
-
-
no_notation
less_eq (infix "\<sqsubseteq>" 50) and
less (infix "\<sqsubset>" 50) and
@@ -2467,23 +2460,24 @@
text {* Rudimentary code generation *}
-lemma empty_code [code]: "{} x \<longleftrightarrow> False"
- unfolding empty_def Collect_def ..
-
-lemma UNIV_code [code]: "UNIV x \<longleftrightarrow> True"
- unfolding UNIV_def Collect_def ..
+lemma [code]: "{} = bot"
+ by (rule sym) (fact bot_set_eq)
+
+lemma [code]: "UNIV = top"
+ by (rule sym) (fact top_set_eq)
+
+lemma [code]: "op \<inter> = inf"
+ by (rule ext)+ (simp add: inf_set_eq)
+
+lemma [code]: "op \<union> = sup"
+ by (rule ext)+ (simp add: sup_set_eq)
lemma insert_code [code]: "insert y A x \<longleftrightarrow> y = x \<or> A x"
- unfolding insert_def Collect_def mem_def Un_def by auto
-
-lemma inter_code [code]: "(A \<inter> B) x \<longleftrightarrow> A x \<and> B x"
- unfolding Int_def Collect_def mem_def ..
-
-lemma union_code [code]: "(A \<union> B) x \<longleftrightarrow> A x \<or> B x"
- unfolding Un_def Collect_def mem_def ..
+ by (auto simp add: insert_compr Collect_def mem_def)
lemma vimage_code [code]: "(f -` A) x = A (f x)"
- unfolding vimage_def Collect_def mem_def ..
+ by (simp add: vimage_def Collect_def mem_def)
+
text {* Misc theorem and ML bindings *}
--- a/src/Pure/Isar/class.ML Tue Jul 21 11:01:07 2009 +0200
+++ b/src/Pure/Isar/class.ML Tue Jul 21 11:13:47 2009 +0200
@@ -68,9 +68,8 @@
val base_morph = inst_morph
$> Morphism.binding_morphism (Binding.prefix false (class_prefix class))
$> Element.satisfy_morphism (the_list wit);
- val defs = these_defs thy sups;
- val eq_morph = Element.eq_morphism thy defs;
- val morph = base_morph $> eq_morph;
+ val eqs = these_defs thy sups;
+ val eq_morph = Element.eq_morphism thy eqs;
(* assm_intro *)
fun prove_assm_intro thm =
@@ -97,7 +96,7 @@
ORELSE' Tactic.assume_tac));
val of_class = SkipProof.prove_global thy [] [] of_class_prop (K tac);
- in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end;
+ in (base_morph, eqs, export_morph, axiom, assm_intro, of_class) end;
(* reading and processing class specifications *)
@@ -284,9 +283,8 @@
||> Theory.checkpoint
|-> (fn (param_map, params, assm_axiom) =>
`(fn thy => calculate thy class sups base_sort param_map assm_axiom)
- #-> (fn (base_morph, morph, export_morph, axiom, assm_intro, of_class) =>
- Locale.add_registration (class, (morph, export_morph))
- #> Context.theory_map (Locale.activate_facts (class, morph $> export_morph))
+ #-> (fn (base_morph, eqs, export_morph, axiom, assm_intro, of_class) =>
+ Locale.add_registration_eqs (class, base_morph) eqs export_morph
#> register class sups params base_sort base_morph axiom assm_intro of_class))
|> TheoryTarget.init (SOME class)
|> pair class
--- a/src/Pure/Isar/locale.ML Tue Jul 21 11:01:07 2009 +0200
+++ b/src/Pure/Isar/locale.ML Tue Jul 21 11:13:47 2009 +0200
@@ -68,9 +68,8 @@
val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
(* Registrations and dependencies *)
- val add_registration: string * (morphism * morphism) -> theory -> theory
+ val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory
val amend_registration: morphism -> string * morphism -> theory -> theory
- val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory
val add_dependency: string -> string * morphism -> morphism -> theory -> theory
(* Diagnostic *)
@@ -295,8 +294,7 @@
fun activate_declarations dep = Context.proof_map (fn context =>
let
val thy = Context.theory_of context;
- val context' = roundup thy activate_decls dep (get_idents context, context) |-> put_idents;
- in context' end);
+ in roundup thy activate_decls dep (get_idents context, context) |-> put_idents end);
fun activate_facts dep context =
let
@@ -346,11 +344,6 @@
fun all_registrations thy = Registrations.get thy
|> map reg_morph;
-fun add_registration (name, (base_morph, export)) thy =
- roundup thy (fn (name', morph') => Registrations.map (cons ((name', (morph', export)), stamp ())))
- (name, base_morph) (get_idents (Context.Theory thy), thy)
- (* FIXME |-> (Context.theory_map o put_idents_diag)*) |> snd;
-
fun amend_registration morph (name, base_morph) thy =
let
val regs = map #1 (Registrations.get thy);
@@ -373,8 +366,10 @@
val morph = if null eqns then proto_morph
else proto_morph $> Element.eq_morphism thy eqns;
in
- thy
- |> add_registration (dep, (morph, export))
+ (get_idents (Context.Theory thy), thy)
+ |> roundup thy (fn (dep', morph') =>
+ Registrations.map (cons ((dep', (morph', export)), stamp ()))) (dep, morph)
+ |> snd
|> Context.theory_map (activate_facts (dep, morph $> export))
end;