Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
default.
--- a/NEWS Fri Oct 31 06:54:22 2003 +0100
+++ b/NEWS Thu Nov 06 14:18:05 2003 +0100
@@ -48,6 +48,8 @@
Resolve particular premise with <locale>.intro to obtain old form.
- Fixed bug in type inference ("unify_frozen") that prevented mix of target
specification and "includes" elements in goal statement.
+ - Rule sets <locale>.intro and <locale>.axioms no longer declared as
+ [intro?] and [elim?] (respectively) by default.
* HOL: Tactic emulation methods induct_tac and case_tac understand static
(Isar) contexts.
--- a/src/HOL/Algebra/Coset.thy Fri Oct 31 06:54:22 2003 +0100
+++ b/src/HOL/Algebra/Coset.thy Thu Nov 06 14:18:05 2003 +0100
@@ -46,7 +46,7 @@
*}
lemma (in group) is_coset:
"coset G"
- ..
+ by (rule coset.intro)
text{*Lemmas useful for Sylow's Theorem*}
--- a/src/HOL/Algebra/Group.thy Fri Oct 31 06:54:22 2003 +0100
+++ b/src/HOL/Algebra/Group.thy Thu Nov 06 14:18:05 2003 +0100
@@ -415,7 +415,7 @@
lemma (in subgroup) group_axiomsI [intro]:
includes group G
shows "group_axioms (G(| carrier := H |))"
- by rule (auto intro: l_inv r_inv simp add: Units_def)
+ by (rule group_axioms.intro) (auto intro: l_inv r_inv simp add: Units_def)
lemma (in subgroup) groupI [intro]:
includes group G
@@ -440,8 +440,8 @@
and inv: "!!a. a \<in> H ==> inv a \<in> H"
and mult: "!!a b. [|a \<in> H; b \<in> H|] ==> a \<otimes> b \<in> H"
shows "subgroup H G"
-proof
- from subset and mult show "submagma H G" ..
+proof (rule subgroup.intro)
+ from subset and mult show "submagma H G" by (rule submagma.intro)
next
have "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems)
with inv show "subgroup_axioms H G"
@@ -472,7 +472,7 @@
lemma (in subgroup) finite_imp_card_positive:
"finite (carrier G) ==> 0 < card H"
proof (rule classical)
- have sub: "subgroup H G" using prems ..
+ have sub: "subgroup H G" using prems by (rule subgroup.intro)
assume fin: "finite (carrier G)"
and zero: "~ 0 < card H"
then have "finite H" by (blast intro: finite_subset dest: subset)
@@ -505,12 +505,13 @@
lemma DirProdSemigroup_magma:
includes magma G + magma H
shows "magma (G \<times>\<^sub>s H)"
- by rule (auto simp add: DirProdSemigroup_def)
+ by (rule magma.intro) (auto simp add: DirProdSemigroup_def)
lemma DirProdSemigroup_semigroup_axioms:
includes semigroup G + semigroup H
shows "semigroup_axioms (G \<times>\<^sub>s H)"
- by rule (auto simp add: DirProdSemigroup_def G.m_assoc H.m_assoc)
+ by (rule semigroup_axioms.intro)
+ (auto simp add: DirProdSemigroup_def G.m_assoc H.m_assoc)
lemma DirProdSemigroup_semigroup:
includes semigroup G + semigroup H
@@ -522,13 +523,13 @@
lemma DirProdGroup_magma:
includes magma G + magma H
shows "magma (G \<times>\<^sub>g H)"
- by rule
+ by (rule magma.intro)
(auto simp add: DirProdGroup_def DirProdSemigroup_def)
lemma DirProdGroup_semigroup_axioms:
includes semigroup G + semigroup H
shows "semigroup_axioms (G \<times>\<^sub>g H)"
- by rule
+ by (rule semigroup_axioms.intro)
(auto simp add: DirProdGroup_def DirProdSemigroup_def
G.m_assoc H.m_assoc)
@@ -581,12 +582,12 @@
lemma (in semigroup) hom:
includes semigroup G
shows "semigroup (| carrier = hom G G, mult = op o |)"
-proof
+proof (rule semigroup.intro)
show "magma (| carrier = hom G G, mult = op o |)"
- by rule (simp add: Pi_def hom_def)
+ by (rule magma.intro) (simp add: Pi_def hom_def)
next
show "semigroup_axioms (| carrier = hom G G, mult = op o |)"
- by rule (simp add: o_assoc)
+ by (rule semigroup_axioms.intro) (simp add: o_assoc)
qed
lemma hom_mult:
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Fri Oct 31 06:54:22 2003 +0100
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Thu Nov 06 14:18:05 2003 +0100
@@ -23,6 +23,8 @@
locale continuous = var V + norm_syntax + linearform +
assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
+declare continuous.intro [intro?] continuous_axioms.intro [intro?]
+
lemma continuousI [intro]:
includes norm_syntax + linearform
assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
--- a/src/HOL/Real/HahnBanach/Linearform.thy Fri Oct 31 06:54:22 2003 +0100
+++ b/src/HOL/Real/HahnBanach/Linearform.thy Thu Nov 06 14:18:05 2003 +0100
@@ -16,6 +16,8 @@
assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
and mult [iff]: "x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * f x"
+declare linearform.intro [intro?]
+
lemma (in linearform) neg [iff]:
includes vectorspace
shows "x \<in> V \<Longrightarrow> f (- x) = - f x"
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy Fri Oct 31 06:54:22 2003 +0100
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Thu Nov 06 14:18:05 2003 +0100
@@ -23,6 +23,8 @@
and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
and subadditive [iff?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
+declare seminorm.intro [intro?]
+
lemma (in seminorm) diff_subadditive:
includes vectorspace
shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
@@ -71,6 +73,8 @@
locale normed_vectorspace = vectorspace + norm
+declare normed_vectorspace.intro [intro?]
+
lemma (in normed_vectorspace) gt_zero [intro?]:
"x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> 0 < \<parallel>x\<parallel>"
proof -
--- a/src/HOL/Real/HahnBanach/Subspace.thy Fri Oct 31 06:54:22 2003 +0100
+++ b/src/HOL/Real/HahnBanach/Subspace.thy Thu Nov 06 14:18:05 2003 +0100
@@ -22,6 +22,8 @@
and add_closed [iff]: "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U"
and mult_closed [iff]: "x \<in> U \<Longrightarrow> a \<cdot> x \<in> U"
+declare vectorspace.intro [intro?] subspace.intro [intro?]
+
syntax (symbols)
subspace :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infix "\<unlhd>" 50)
--- a/src/HOL/ex/Locales.thy Fri Oct 31 06:54:22 2003 +0100
+++ b/src/HOL/ex/Locales.thy Thu Nov 06 14:18:05 2003 +0100
@@ -321,6 +321,9 @@
assumes left_inv: "x\<inv> \<cdot> x = \<one>"
and left_one: "\<one> \<cdot> x = x"
+declare semigroup.intro [intro?]
+ group.intro [intro?] group_axioms.intro [intro?]
+
text {*
Note that we prefer to call the @{text group} record structure
@{text G} rather than @{text S} inherited from @{text semigroup}.
--- a/src/Pure/Isar/locale.ML Fri Oct 31 06:54:22 2003 +0100
+++ b/src/Pure/Isar/locale.ML Thu Nov 06 14:18:05 2003 +0100
@@ -887,17 +887,6 @@
val ((import_ctxt, axioms'), (import_elemss, _)) =
activate_facts prep_facts ((context, axioms), ps);
-(* CB: testing *)
-(*
-val axioms' = if true (* null axioms *) then axioms' else
-let val {view = (ax3_view, ax3_axioms), ...} =
- the_locale (ProofContext.theory_of context) "Type.ax3";
-val ax_TrueFalse = Thm.assume (read_cterm (sign_of_thm (hd axioms))
- ("True <-> False", propT));
-val {view = (ax4_view, ax4_axioms), ...} =
- the_locale (ProofContext.theory_of context) "Type.ax4";
-in axioms' @ ax3_axioms @ [ax_TrueFalse] @ (tl ax4_axioms) end;
-*)
val ((ctxt, _), (elemss, _)) =
activate_facts prep_facts ((import_ctxt, axioms'), qs);
in
@@ -1126,7 +1115,7 @@
[(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, ([], []))])]])];
in
def_thy |> have_thmss_qualified "" aname
- [((introN, [ContextRules.intro_query_global None]), [([intro], [])])]
+ [((introN, []), [([intro], [])])]
|> #1 |> rpair (elemss', [statement])
end;
val (thy'', view) =
@@ -1138,8 +1127,8 @@
val cstatement = Thm.cterm_of (Theory.sign_of def_thy) statement;
in
def_thy |> have_thmss_qualified "" bname
- [((introN, [ContextRules.intro_query_global None]), [([intro], [])]),
- ((axiomsN, [ContextRules.elim_query_global None]), [(map Drule.standard axioms, [])])]
+ [((introN, []), [([intro], [])]),
+ ((axiomsN, []), [(map Drule.standard axioms, [])])]
|> #1 |> rpair ([cstatement], axioms)
end;
in (thy'', (elemss', view)) end;