Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
authorballarin
Thu Nov 06 14:18:05 2003 +0100 (2003-11-06)
changeset 14254342634f38451
parent 14253 91a64a93bdb4
child 14255 e6e3e3f0deed
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
default.
NEWS
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Group.thy
src/HOL/Real/HahnBanach/FunctionNorm.thy
src/HOL/Real/HahnBanach/Linearform.thy
src/HOL/Real/HahnBanach/NormedSpace.thy
src/HOL/Real/HahnBanach/Subspace.thy
src/HOL/ex/Locales.thy
src/Pure/Isar/locale.ML
     1.1 --- a/NEWS	Fri Oct 31 06:54:22 2003 +0100
     1.2 +++ b/NEWS	Thu Nov 06 14:18:05 2003 +0100
     1.3 @@ -48,6 +48,8 @@
     1.4      Resolve particular premise with <locale>.intro to obtain old form.
     1.5    - Fixed bug in type inference ("unify_frozen") that prevented mix of target
     1.6      specification and "includes" elements in goal statement.
     1.7 +  - Rule sets <locale>.intro and <locale>.axioms no longer declared as
     1.8 +    [intro?] and [elim?] (respectively) by default.
     1.9  
    1.10  * HOL: Tactic emulation methods induct_tac and case_tac understand static
    1.11    (Isar) contexts.
     2.1 --- a/src/HOL/Algebra/Coset.thy	Fri Oct 31 06:54:22 2003 +0100
     2.2 +++ b/src/HOL/Algebra/Coset.thy	Thu Nov 06 14:18:05 2003 +0100
     2.3 @@ -46,7 +46,7 @@
     2.4  *}
     2.5  lemma (in group) is_coset:
     2.6    "coset G"
     2.7 -  ..
     2.8 +  by (rule coset.intro)
     2.9  
    2.10  text{*Lemmas useful for Sylow's Theorem*}
    2.11  
     3.1 --- a/src/HOL/Algebra/Group.thy	Fri Oct 31 06:54:22 2003 +0100
     3.2 +++ b/src/HOL/Algebra/Group.thy	Thu Nov 06 14:18:05 2003 +0100
     3.3 @@ -415,7 +415,7 @@
     3.4  lemma (in subgroup) group_axiomsI [intro]:
     3.5    includes group G
     3.6    shows "group_axioms (G(| carrier := H |))"
     3.7 -  by rule (auto intro: l_inv r_inv simp add: Units_def)
     3.8 +  by (rule group_axioms.intro) (auto intro: l_inv r_inv simp add: Units_def)
     3.9  
    3.10  lemma (in subgroup) groupI [intro]:
    3.11    includes group G
    3.12 @@ -440,8 +440,8 @@
    3.13      and inv: "!!a. a \<in> H ==> inv a \<in> H"
    3.14      and mult: "!!a b. [|a \<in> H; b \<in> H|] ==> a \<otimes> b \<in> H"
    3.15    shows "subgroup H G"
    3.16 -proof
    3.17 -  from subset and mult show "submagma H G" ..
    3.18 +proof (rule subgroup.intro)
    3.19 +  from subset and mult show "submagma H G" by (rule submagma.intro)
    3.20  next
    3.21    have "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems)
    3.22    with inv show "subgroup_axioms H G"
    3.23 @@ -472,7 +472,7 @@
    3.24  lemma (in subgroup) finite_imp_card_positive:
    3.25    "finite (carrier G) ==> 0 < card H"
    3.26  proof (rule classical)
    3.27 -  have sub: "subgroup H G" using prems ..
    3.28 +  have sub: "subgroup H G" using prems by (rule subgroup.intro)
    3.29    assume fin: "finite (carrier G)"
    3.30      and zero: "~ 0 < card H"
    3.31    then have "finite H" by (blast intro: finite_subset dest: subset)
    3.32 @@ -505,12 +505,13 @@
    3.33  lemma DirProdSemigroup_magma:
    3.34    includes magma G + magma H
    3.35    shows "magma (G \<times>\<^sub>s H)"
    3.36 -  by rule (auto simp add: DirProdSemigroup_def)
    3.37 +  by (rule magma.intro) (auto simp add: DirProdSemigroup_def)
    3.38  
    3.39  lemma DirProdSemigroup_semigroup_axioms:
    3.40    includes semigroup G + semigroup H
    3.41    shows "semigroup_axioms (G \<times>\<^sub>s H)"
    3.42 -  by rule (auto simp add: DirProdSemigroup_def G.m_assoc H.m_assoc)
    3.43 +  by (rule semigroup_axioms.intro)
    3.44 +    (auto simp add: DirProdSemigroup_def G.m_assoc H.m_assoc)
    3.45  
    3.46  lemma DirProdSemigroup_semigroup:
    3.47    includes semigroup G + semigroup H
    3.48 @@ -522,13 +523,13 @@
    3.49  lemma DirProdGroup_magma:
    3.50    includes magma G + magma H
    3.51    shows "magma (G \<times>\<^sub>g H)"
    3.52 -  by rule
    3.53 +  by (rule magma.intro)
    3.54      (auto simp add: DirProdGroup_def DirProdSemigroup_def)
    3.55  
    3.56  lemma DirProdGroup_semigroup_axioms:
    3.57    includes semigroup G + semigroup H
    3.58    shows "semigroup_axioms (G \<times>\<^sub>g H)"
    3.59 -  by rule
    3.60 +  by (rule semigroup_axioms.intro)
    3.61      (auto simp add: DirProdGroup_def DirProdSemigroup_def
    3.62        G.m_assoc H.m_assoc)
    3.63  
    3.64 @@ -581,12 +582,12 @@
    3.65  lemma (in semigroup) hom:
    3.66    includes semigroup G
    3.67    shows "semigroup (| carrier = hom G G, mult = op o |)"
    3.68 -proof
    3.69 +proof (rule semigroup.intro)
    3.70    show "magma (| carrier = hom G G, mult = op o |)"
    3.71 -    by rule (simp add: Pi_def hom_def)
    3.72 +    by (rule magma.intro) (simp add: Pi_def hom_def)
    3.73  next
    3.74    show "semigroup_axioms (| carrier = hom G G, mult = op o |)"
    3.75 -    by rule (simp add: o_assoc)
    3.76 +    by (rule semigroup_axioms.intro) (simp add: o_assoc)
    3.77  qed
    3.78  
    3.79  lemma hom_mult:
     4.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Fri Oct 31 06:54:22 2003 +0100
     4.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Thu Nov 06 14:18:05 2003 +0100
     4.3 @@ -23,6 +23,8 @@
     4.4  locale continuous = var V + norm_syntax + linearform +
     4.5    assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
     4.6  
     4.7 +declare continuous.intro [intro?] continuous_axioms.intro [intro?]
     4.8 +
     4.9  lemma continuousI [intro]:
    4.10    includes norm_syntax + linearform
    4.11    assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
     5.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Fri Oct 31 06:54:22 2003 +0100
     5.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Thu Nov 06 14:18:05 2003 +0100
     5.3 @@ -16,6 +16,8 @@
     5.4    assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
     5.5      and mult [iff]: "x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * f x"
     5.6  
     5.7 +declare linearform.intro [intro?]
     5.8 +
     5.9  lemma (in linearform) neg [iff]:
    5.10    includes vectorspace
    5.11    shows "x \<in> V \<Longrightarrow> f (- x) = - f x"
     6.1 --- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Fri Oct 31 06:54:22 2003 +0100
     6.2 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Thu Nov 06 14:18:05 2003 +0100
     6.3 @@ -23,6 +23,8 @@
     6.4      and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
     6.5      and subadditive [iff?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
     6.6  
     6.7 +declare seminorm.intro [intro?]
     6.8 +
     6.9  lemma (in seminorm) diff_subadditive:
    6.10    includes vectorspace
    6.11    shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
    6.12 @@ -71,6 +73,8 @@
    6.13  
    6.14  locale normed_vectorspace = vectorspace + norm
    6.15  
    6.16 +declare normed_vectorspace.intro [intro?]
    6.17 +
    6.18  lemma (in normed_vectorspace) gt_zero [intro?]:
    6.19    "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> 0 < \<parallel>x\<parallel>"
    6.20  proof -
     7.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Fri Oct 31 06:54:22 2003 +0100
     7.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Thu Nov 06 14:18:05 2003 +0100
     7.3 @@ -22,6 +22,8 @@
     7.4      and add_closed [iff]: "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U"
     7.5      and mult_closed [iff]: "x \<in> U \<Longrightarrow> a \<cdot> x \<in> U"
     7.6  
     7.7 +declare vectorspace.intro [intro?] subspace.intro [intro?]
     7.8 +
     7.9  syntax (symbols)
    7.10    subspace :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"    (infix "\<unlhd>" 50)
    7.11  
     8.1 --- a/src/HOL/ex/Locales.thy	Fri Oct 31 06:54:22 2003 +0100
     8.2 +++ b/src/HOL/ex/Locales.thy	Thu Nov 06 14:18:05 2003 +0100
     8.3 @@ -321,6 +321,9 @@
     8.4    assumes left_inv: "x\<inv> \<cdot> x = \<one>"
     8.5      and left_one: "\<one> \<cdot> x = x"
     8.6  
     8.7 +declare semigroup.intro [intro?]
     8.8 +  group.intro [intro?] group_axioms.intro [intro?]
     8.9 +
    8.10  text {*
    8.11    Note that we prefer to call the @{text group} record structure
    8.12    @{text G} rather than @{text S} inherited from @{text semigroup}.
     9.1 --- a/src/Pure/Isar/locale.ML	Fri Oct 31 06:54:22 2003 +0100
     9.2 +++ b/src/Pure/Isar/locale.ML	Thu Nov 06 14:18:05 2003 +0100
     9.3 @@ -887,17 +887,6 @@
     9.4      val ((import_ctxt, axioms'), (import_elemss, _)) =
     9.5        activate_facts prep_facts ((context, axioms), ps);
     9.6  
     9.7 -(* CB: testing *)
     9.8 -(*
     9.9 -val axioms' = if true (* null axioms *) then axioms' else
    9.10 -let val {view = (ax3_view, ax3_axioms), ...} =
    9.11 -  the_locale (ProofContext.theory_of context) "Type.ax3";
    9.12 -val ax_TrueFalse = Thm.assume (read_cterm (sign_of_thm (hd axioms))
    9.13 -  ("True <-> False", propT));
    9.14 -val {view = (ax4_view, ax4_axioms), ...} =
    9.15 -  the_locale (ProofContext.theory_of context) "Type.ax4";
    9.16 -in axioms' @ ax3_axioms @ [ax_TrueFalse] @ (tl ax4_axioms) end;
    9.17 -*)
    9.18      val ((ctxt, _), (elemss, _)) =
    9.19        activate_facts prep_facts ((import_ctxt, axioms'), qs);
    9.20    in
    9.21 @@ -1126,7 +1115,7 @@
    9.22              [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, ([], []))])]])];
    9.23          in
    9.24            def_thy |> have_thmss_qualified "" aname
    9.25 -            [((introN, [ContextRules.intro_query_global None]), [([intro], [])])]
    9.26 +            [((introN, []), [([intro], [])])]
    9.27            |> #1 |> rpair (elemss', [statement])
    9.28          end;
    9.29      val (thy'', view) =
    9.30 @@ -1138,8 +1127,8 @@
    9.31            val cstatement = Thm.cterm_of (Theory.sign_of def_thy) statement;
    9.32          in
    9.33            def_thy |> have_thmss_qualified "" bname
    9.34 -            [((introN, [ContextRules.intro_query_global None]), [([intro], [])]),
    9.35 -             ((axiomsN, [ContextRules.elim_query_global None]), [(map Drule.standard axioms, [])])]
    9.36 +            [((introN, []), [([intro], [])]),
    9.37 +             ((axiomsN, []), [(map Drule.standard axioms, [])])]
    9.38            |> #1 |> rpair ([cstatement], axioms)
    9.39          end;
    9.40    in (thy'', (elemss', view)) end;