# HG changeset patch
# User ballarin
# Date 1152017221 -7200
# Node ID 29bb4659f80a471f2af22c75ff2ea44decb975ad
# Parent  d649506f40c3783d3b91227c12ca9ae4222a3113
Method intro_locales replaced by intro_locales and unfold_locales.

diff -r d649506f40c3 -r 29bb4659f80a NEWS
--- 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
diff -r d649506f40c3 -r 29bb4659f80a src/FOL/ex/LocaleTest.thy
--- 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
diff -r d649506f40c3 -r 29bb4659f80a src/HOL/Algebra/Group.thy
--- 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)
diff -r d649506f40c3 -r 29bb4659f80a src/HOL/Algebra/Lattice.thy
--- 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)+
diff -r d649506f40c3 -r 29bb4659f80a src/HOL/Algebra/Module.thy
--- 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"
diff -r d649506f40c3 -r 29bb4659f80a src/HOL/Algebra/UnivPoly.thy
--- 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"
diff -r d649506f40c3 -r 29bb4659f80a src/HOL/Finite_Set.thy
--- 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
diff -r d649506f40c3 -r 29bb4659f80a src/HOL/Hyperreal/Filter.thy
--- 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
 
diff -r d649506f40c3 -r 29bb4659f80a src/HOL/Orderings.thy
--- 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)
diff -r d649506f40c3 -r 29bb4659f80a src/HOL/Real/HahnBanach/FunctionNorm.thy
--- 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)
diff -r d649506f40c3 -r 29bb4659f80a src/HOL/Real/HahnBanach/HahnBanach.thy
--- 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)
diff -r d649506f40c3 -r 29bb4659f80a src/HOL/Real/HahnBanach/NormedSpace.thy
--- 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
diff -r d649506f40c3 -r 29bb4659f80a src/Pure/Isar/locale.ML
--- 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;