Method intro_locales replaced by intro_locales and unfold_locales.
--- a/NEWS Tue Jul 04 12:13:38 2006 +0200
+++ b/NEWS Tue Jul 04 14:47:01 2006 +0200
@@ -215,12 +215,13 @@
INCOMPATIBILITY: different normal form of locale expressions.
In particular, in interpretations of locales with predicates,
goals repesenting already interpreted fragments are not removed
-automatically. Use method intro_locales; see below.
-
-* Isar/locales: new method intro_locales. Backward reasoning for locale
-predicates. In addition the method is aware of interpretations and
-discharges corresponding goals. Optional argument `!' prevents
-unfolding of predicates to assumptions.
+automatically. Use methods `intro_locales' and `unfold_locales'; see below.
+
+* Isar/locales: new methods `intro_locales' and `unfold_locales' provide
+backward reasoning on locales predicates. The methods are aware of
+interpretations and discharge corresponding goals. `intro_locales' is
+less aggressive then `unfold_locales' and does not unfold predicates to
+assumptions.
* Isar/locales: the order in which locale fragments are accumulated
has changed. This enables to override declarations from fragments
--- a/src/FOL/ex/LocaleTest.thy Tue Jul 04 12:13:38 2006 +0200
+++ b/src/FOL/ex/LocaleTest.thy Tue Jul 04 14:47:01 2006 +0200
@@ -115,7 +115,7 @@
arities i :: "term"
-interpretation i1: IC ["X::i" "Y::i"] by (intro_locales) auto
+interpretation i1: IC ["X::i" "Y::i"] by unfold_locales auto
print_interps IA (* output: i1 *)
@@ -128,7 +128,7 @@
(* without prefix *)
interpretation IC ["W::i" "Z::i"] . (* subsumed by i1: IC *)
-interpretation IC ["W::'a" "Z::i"] by intro_locales auto
+interpretation IC ["W::'a" "Z::i"] by unfold_locales auto
(* subsumes i1: IA and i1: IC *)
print_interps IA (* output: <no prefix>, i1 *)
@@ -139,13 +139,13 @@
ML {* check_thm "asm_C" *}
interpretation i2: ID [X "Y::i" "Y = X"]
- by (simp add: eq_commute) intro_locales
+ by (simp add: eq_commute) unfold_locales
print_interps IA (* output: <no prefix>, i1 *)
print_interps ID (* output: i2 *)
-interpretation i3: ID [X "Y::i"] by simp intro_locales
+interpretation i3: ID [X "Y::i"] by simp unfold_locales
(* duplicate: thm not added *)
@@ -194,10 +194,10 @@
proof -
fix alpha::i and beta::'a and gamma::o
(* FIXME: omitting type of beta leads to error later at interpret i6 *)
- have alpha_A: "IA(alpha)" by intro_locales simp
+ have alpha_A: "IA(alpha)" by unfold_locales simp
interpret i5: IA [alpha] . (* subsumed *)
print_interps IA (* output: <no prefix>, i1 *)
- interpret i6: IC [alpha beta] by intro_locales auto
+ interpret i6: IC [alpha beta] by unfold_locales auto
print_interps IA (* output: <no prefix>, i1 *)
print_interps IC (* output: <no prefix>, i1, i6 *)
interpret i11: IF [gamma] by (fast intro: IF.intro)
@@ -210,7 +210,7 @@
fix beta and gamma
interpret i9: ID [a beta _]
apply - apply assumption
- apply intro_locales
+ apply unfold_locales
apply (rule refl) done
qed rule
@@ -528,7 +528,7 @@
qed simp
interpretation Rplgrp < Rprgrp
- proof intro_locales
+ proof unfold_locales
{
fix x
have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
@@ -558,7 +558,7 @@
(* circular interpretation *)
interpretation Rprgrp < Rplgrp
- proof intro_locales
+ proof unfold_locales
{
fix x
have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
@@ -655,14 +655,14 @@
qed simp
interpretation Rqrgrp < Rprgrp
- apply intro_locales
+ apply unfold_locales
apply (rule assoc)
apply (rule rone)
apply (rule rinv)
done
interpretation R2: Rqlgrp ["op #" "rone" "rinv"]
- apply intro_locales (* FIXME: intro_locales is too eager and shouldn't
+ apply unfold_locales (* FIXME: unfold_locales is too eager and shouldn't
solve this. *)
done
@@ -672,7 +672,7 @@
interpretation Rqlgrp < Rqrgrp
- proof intro_locales
+ proof unfold_locales
{
fix x
have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
@@ -706,12 +706,12 @@
assumes x: "x = x" and y: "y = y"
interpretation Rtriv2 < Rtriv x
- apply intro_locales
+ apply unfold_locales
apply (rule x)
done
interpretation Rtriv2 < Rtriv y
- apply intro_locales
+ apply unfold_locales
apply (rule y)
done
@@ -721,7 +721,7 @@
assumes x: "x = x" and y: "y = y" and z: "z = z"
interpretation Rtriv3 < Rtriv2 x y
- apply intro_locales
+ apply unfold_locales
apply (rule x)
apply (rule y)
done
@@ -729,7 +729,7 @@
print_locale Rtriv3
interpretation Rtriv3 < Rtriv2 x z
- apply intro_locales
+ apply unfold_locales
apply (rule x_y_z.x)
apply (rule z)
done
--- a/src/HOL/Algebra/Group.thy Tue Jul 04 12:13:38 2006 +0200
+++ b/src/HOL/Algebra/Group.thy Tue Jul 04 14:47:01 2006 +0200
@@ -658,7 +658,7 @@
assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
x \<otimes> y = y \<otimes> x"
shows "comm_group G"
- by intro_locales (simp_all add: m_comm)
+ by unfold_locales (simp_all add: m_comm)
lemma comm_groupI:
fixes G (structure)
--- a/src/HOL/Algebra/Lattice.thy Tue Jul 04 12:13:38 2006 +0200
+++ b/src/HOL/Algebra/Lattice.thy Tue Jul 04 14:47:01 2006 +0200
@@ -654,7 +654,7 @@
lemma (in partial_order) total_orderI:
assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
shows "total_order L"
-proof (intro_locales!)
+proof intro_locales
show "lattice_axioms L"
proof (rule lattice_axioms.intro)
fix x y
@@ -716,7 +716,7 @@
and inf_exists:
"!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
shows "complete_lattice L"
-proof (intro_locales!)
+proof intro_locales
show "lattice_axioms L"
by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+
qed (assumption | rule complete_lattice_axioms.intro)+
--- a/src/HOL/Algebra/Module.thy Tue Jul 04 12:13:38 2006 +0200
+++ b/src/HOL/Algebra/Module.thy Tue Jul 04 14:47:01 2006 +0200
@@ -73,7 +73,7 @@
"!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
(a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
shows "algebra R M"
-apply (intro_locales!)
+apply intro_locales
apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms prems)+
apply (rule module_axioms.intro)
apply (simp add: smult_closed)
@@ -88,11 +88,11 @@
lemma (in algebra) R_cring:
"cring R"
- by intro_locales
+ by unfold_locales
lemma (in algebra) M_cring:
"cring M"
- by intro_locales
+ by unfold_locales
lemma (in algebra) module:
"module R M"
--- a/src/HOL/Algebra/UnivPoly.thy Tue Jul 04 12:13:38 2006 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Tue Jul 04 14:47:01 2006 +0200
@@ -397,7 +397,7 @@
*}
interpretation UP_cring < cring P
- by (intro_locales!)
+ by intro_locales
(rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms UP_cring)+
@@ -441,7 +441,7 @@
UP_smult_assoc1 UP_smult_assoc2)
interpretation UP_cring < algebra R P
- by (intro_locales!)
+ by intro_locales
(rule module.axioms algebra.axioms UP_algebra)+
@@ -945,7 +945,7 @@
*}
interpretation UP_domain < "domain" P
- by (intro_locales!) (rule domain.axioms UP_domain)+
+ by intro_locales (rule domain.axioms UP_domain)+
subsection {* Evaluation Homomorphism and Universal Property*}
@@ -1148,10 +1148,10 @@
interpretation UP_univ_prop < ring_hom_cring P S Eval
apply (unfold Eval_def)
- apply (intro_locales!)
+ apply intro_locales
apply (rule ring_hom_cring.axioms)
apply (rule ring_hom_cring.intro)
- apply intro_locales
+ apply unfold_locales
apply (rule eval_ring_hom)
apply rule
done
@@ -1276,7 +1276,7 @@
proof (rule ring_hom_cring.intro)
show "ring_hom_cring_axioms P S Phi"
by (rule ring_hom_cring_axioms.intro) (rule Phi)
-qed intro_locales
+qed unfold_locales
theorem (in UP_pre_univ_prop) UP_universal_property:
assumes S: "s \<in> carrier S"
--- a/src/HOL/Finite_Set.thy Tue Jul 04 12:13:38 2006 +0200
+++ b/src/HOL/Finite_Set.thy Tue Jul 04 14:47:01 2006 +0200
@@ -502,10 +502,10 @@
text{* Interpretation of locales: *}
interpretation AC_add: ACe ["op +" "0::'a::comm_monoid_add"]
- by intro_locales (auto intro: add_assoc add_commute)
+ by unfold_locales (auto intro: add_assoc add_commute)
interpretation AC_mult: ACe ["op *" "1::'a::comm_monoid_mult"]
- by intro_locales (auto intro: mult_assoc mult_commute)
+ by unfold_locales (auto intro: mult_assoc mult_commute)
subsubsection{*From @{term foldSet} to @{term fold}*}
@@ -2214,7 +2214,7 @@
done
lemma (in Lattice) ACIfSL_sup: "ACIfSL sup (%x y. y \<sqsubseteq> x)"
-(* FIXME: insert ACf_sup and use intro_locales *)
+(* FIXME: insert ACf_sup and use unfold_locales *)
apply(rule ACIfSL.intro)
apply(rule ACIf.intro)
apply(rule ACf_sup)
@@ -2370,43 +2370,43 @@
done
interpretation min: ACIf ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
-apply intro_locales
+apply unfold_locales
apply(auto simp:min_def)
done
interpretation max: ACf ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
-apply intro_locales
+apply unfold_locales
apply(auto simp:max_def)
done
interpretation max: ACIf ["max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
-apply intro_locales
+apply unfold_locales
apply(auto simp:max_def)
done
interpretation min:
ACIfSL ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>" "op <"]
apply(simp add:order_less_le)
-apply intro_locales
+apply unfold_locales
apply(auto simp:min_def)
done
interpretation min:
ACIfSLlin ["min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>" "op <"]
-apply intro_locales
+apply unfold_locales
apply(auto simp:min_def)
done
interpretation max:
ACIfSL ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x" "%x y. y<x"]
apply(simp add:order_less_le eq_sym_conv)
-apply intro_locales
+apply unfold_locales
apply(auto simp:max_def)
done
interpretation max:
ACIfSLlin ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x" "%x y. y<x"]
-apply intro_locales
+apply unfold_locales
apply(auto simp:max_def)
done
@@ -2415,13 +2415,13 @@
apply -
apply(rule Min_def)
apply(rule Max_def)
-apply intro_locales
+apply unfold_locales
done
interpretation min_max:
Distrib_Lattice ["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max" "Min" "Max"]
- by intro_locales
+ by unfold_locales
text{* Now we instantiate the recursion equations and declare them
--- a/src/HOL/Hyperreal/Filter.thy Tue Jul 04 12:13:38 2006 +0200
+++ b/src/HOL/Hyperreal/Filter.thy Tue Jul 04 14:47:01 2006 +0200
@@ -68,10 +68,10 @@
lemma (in freeultrafilter) finite: "finite A \<Longrightarrow> A \<notin> F"
by (erule contrapos_pn, erule infinite)
-lemma (in freeultrafilter) filter: "filter F" by intro_locales
+lemma (in freeultrafilter) filter: "filter F" by unfold_locales
lemma (in freeultrafilter) ultrafilter: "ultrafilter F"
- by intro_locales
+ by unfold_locales
subsection {* Collect properties *}
@@ -387,7 +387,7 @@
qed
from fil ultra free have "freeultrafilter U"
by (rule freeultrafilter.intro [OF ultrafilter.intro])
- (* FIXME: intro_locales should use chained facts *)
+ (* FIXME: unfold_locales should use chained facts *)
thus ?thesis ..
qed
--- a/src/HOL/Orderings.thy Tue Jul 04 12:13:38 2006 +0200
+++ b/src/HOL/Orderings.thy Tue Jul 04 14:47:01 2006 +0200
@@ -388,7 +388,7 @@
interpretation min_max:
lower_semilattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
-apply intro_locales
+apply unfold_locales
apply(simp add:min_def linorder_not_le order_less_imp_le)
apply(simp add:min_def linorder_not_le order_less_imp_le)
apply(simp add:min_def linorder_not_le order_less_imp_le)
@@ -396,7 +396,7 @@
interpretation min_max:
upper_semilattice["op \<le>" "max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
-apply intro_locales
+apply unfold_locales
apply(simp add: max_def linorder_not_le order_less_imp_le)
apply(simp add: max_def linorder_not_le order_less_imp_le)
apply(simp add: max_def linorder_not_le order_less_imp_le)
@@ -404,11 +404,11 @@
interpretation min_max:
lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
- by intro_locales
+ by unfold_locales
interpretation min_max:
distrib_lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
-apply intro_locales
+apply unfold_locales
apply(rule_tac x=x and y=y in linorder_le_cases)
apply(rule_tac x=x and y=z in linorder_le_cases)
apply(rule_tac x=y and y=z in linorder_le_cases)
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Tue Jul 04 12:13:38 2006 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Tue Jul 04 14:47:01 2006 +0200
@@ -207,7 +207,7 @@
proof cases
assume "x = 0"
then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp
- also have "f 0 = 0" by rule intro_locales
+ also have "f 0 = 0" by rule unfold_locales
also have "\<bar>\<dots>\<bar> = 0" by simp
also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
by (unfold B_def fn_norm_def) (rule fn_norm_ge_zero)
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Tue Jul 04 12:13:38 2006 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Tue Jul 04 14:47:01 2006 +0200
@@ -334,10 +334,10 @@
\<and> (\<forall>x \<in> F. g x = f x)
\<and> \<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
proof -
- have E: "vectorspace E" by intro_locales
- have E_norm: "normed_vectorspace E norm" by rule intro_locales
+ have E: "vectorspace E" by unfold_locales
+ have E_norm: "normed_vectorspace E norm" by rule unfold_locales
have FE: "F \<unlhd> E" .
- have F: "vectorspace F" by rule intro_locales
+ have F: "vectorspace F" by rule unfold_locales
have linearform: "linearform F f" .
have F_norm: "normed_vectorspace F norm"
by (rule subspace_normed_vs)
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy Tue Jul 04 12:13:38 2006 +0200
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Tue Jul 04 14:47:01 2006 +0200
@@ -97,9 +97,9 @@
includes subspace F E + normed_vectorspace E
shows "normed_vectorspace F norm"
proof
- show "vectorspace F" by (rule vectorspace) intro_locales
+ show "vectorspace F" by (rule vectorspace) unfold_locales
next
- have "NormedSpace.norm E norm" by intro_locales
+ have "NormedSpace.norm E norm" by unfold_locales
with subset show "NormedSpace.norm F norm"
by (simp add: norm_def seminorm_def norm_axioms_def)
qed
--- a/src/Pure/Isar/locale.ML Tue Jul 04 12:13:38 2006 +0200
+++ b/src/Pure/Isar/locale.ML Tue Jul 04 14:47:01 2006 +0200
@@ -2004,7 +2004,7 @@
in
-fun intro_locales_tac (ctxt, eager) facts st =
+fun intro_locales_tac eager ctxt facts st =
let
val wits = all_witnesses ctxt |> map Thm.varifyT;
val thy = ProofContext.theory_of ctxt;
@@ -2017,9 +2017,11 @@
val _ = Context.add_setup (Method.add_methods
[("intro_locales",
- fn src => fn ctxt => Method.METHOD (intro_locales_tac
- (Method.syntax (Scan.lift (Scan.optional (Args.bang >> K false) true)) src ctxt)),
- "back-chain introduction rules of locales and discharge goals with interpretations")]);
+ Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
+ "back-chain introduction rules of locales without unfolding predicates"),
+ ("unfold_locales",
+ Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
+ "back-chain all introduction rules of locales")]);
end;