| author | ballarin |
| Tue, 20 Jun 2006 15:53:44 +0200 | |
| changeset 19931 | fb32b43e7f80 |
| parent 19930 | baeb0aeb4891 |
| child 19932 | 63bd0eeb4e0d |
--- a/NEWS Tue Jun 20 14:51:59 2006 +0200 +++ b/NEWS Tue Jun 20 15:53:44 2006 +0200 @@ -209,6 +209,23 @@ This enables, for example, to define a locale for endomorphisms thus: locale endom = homom mult mult h. +* Isar/locales: changed the way locales with predicates are defined. +Instead of accumulating the specification, the imported expression is +now an interpretation. +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. + +* Isar/locales: the order in which locale fragments are accumulated +has changed. This enables to override declarations from fragments +due to interpretations -- for example, unwanted simp rules. + * Provers/induct: improved internal context management to support local fixes and defines on-the-fly. Thus explicit meta-level connectives !! and ==> are rarely required anymore in inductive goals
--- a/src/Cube/Example.thy Tue Jun 20 14:51:59 2006 +0200 +++ b/src/Cube/Example.thy Tue Jun 20 15:53:44 2006 +0200 @@ -16,7 +16,7 @@ method_setup depth_solve = {* Method.thms_args (fn thms => Method.METHOD (fn facts => - (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms)))))) + (DEPTH_SOLVE (HEADGOAL (ares_tac (PolyML.print (facts @ thms))))))) *} "" method_setup depth_solve1 = {*
--- a/src/FOL/ex/LocaleTest.thy Tue Jun 20 14:51:59 2006 +0200 +++ b/src/FOL/ex/LocaleTest.thy Tue Jun 20 15:53:44 2006 +0200 @@ -104,7 +104,10 @@ theorem (in IA) includes ID - shows True .. + shows True + print_interps! IA + print_interps! ID + .. theorem (in ID) True .. @@ -112,7 +115,7 @@ arities i :: "term" -interpretation i1: IC ["X::i" "Y::i"] by (auto intro: IA.intro IC_axioms.intro) +interpretation i1: IC ["X::i" "Y::i"] by (intro_locales) auto print_interps IA (* output: i1 *) @@ -125,10 +128,9 @@ (* without prefix *) interpretation IC ["W::i" "Z::i"] . (* subsumed by i1: IC *) -interpretation IC ["W::'a" "Z::i"] by (auto intro: IA.intro IC_axioms.intro) +interpretation IC ["W::'a" "Z::i"] by intro_locales auto (* subsumes i1: IA and i1: IC *) - print_interps IA (* output: <no prefix>, i1 *) (* possible accesses *) @@ -136,13 +138,14 @@ ML {* check_thm "asm_C" *} -interpretation i2: ID [X "Y::i" "Y = X"] by (simp add: eq_commute) +interpretation i2: ID [X "Y::i" "Y = X"] + by (simp add: eq_commute) intro_locales print_interps IA (* output: <no prefix>, i1 *) print_interps ID (* output: i2 *) -interpretation i3: ID [X "Y::i"] . +interpretation i3: ID [X "Y::i"] by simp intro_locales (* duplicate: thm not added *) @@ -191,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 (auto intro: IA.intro) + have alpha_A: "IA(alpha)" by intro_locales simp interpret i5: IA [alpha] . (* subsumed *) print_interps IA (* output: <no prefix>, i1 *) - interpret i6: IC [alpha beta] by (auto intro: IC_axioms.intro) + interpret i6: IC [alpha beta] by intro_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) @@ -203,11 +206,12 @@ theorem (in IA) True proof - - print_interps IA + print_interps! IA fix beta and gamma interpret i9: ID [a beta _] - (* no proof obligation for IA !!! *) - apply - apply (rule refl) apply assumption done + apply - apply assumption + apply intro_locales + apply (rule refl) done qed rule @@ -316,7 +320,7 @@ lemma "(x::i) # y # z # w = y # x # w # z" proof - interpret my: IL4 ["op #"] - by (auto intro: IL3.intro IL4_axioms.intro i_assoc i_comm) + by (auto intro: IL4.intro IL3.intro IL4_axioms.intro i_assoc i_comm) show ?thesis by (simp only: my.OP.AC) (* or simply AC *) qed @@ -399,7 +403,7 @@ (* effect on printed locale *) -print_locale Rlgrp +print_locale! Rlgrp (* use of derived theorem *) @@ -453,11 +457,6 @@ print_interps RA5 using A_B_C_D_E.eq apply (blast intro: RA5.intro) done -lemma (in RA5) True -print_facts -print_interps RA5 - .. - interpretation RA5 < RA5 _ C D B _ . (* Any even permutation of parameters is subsumed by the above. *) @@ -529,7 +528,7 @@ qed simp interpretation Rplgrp < Rprgrp - proof (rule Rprgrp_axioms.intro) + proof intro_locales { fix x have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone) @@ -546,7 +545,7 @@ (* effect on printed locale *) -print_locale Rplgrp +print_locale! Rplgrp (* use of derived theorem *) @@ -559,7 +558,7 @@ (* circular interpretation *) interpretation Rprgrp < Rplgrp - proof (rule Rplgrp_axioms.intro) + proof intro_locales { fix x have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone) @@ -576,8 +575,8 @@ (* effect on printed locale *) -print_locale Rprgrp -print_locale Rplgrp +print_locale! Rprgrp +print_locale! Rplgrp subsection {* Interaction of Interpretation in Theories and Locales: in Locale, then in Theory *} @@ -656,27 +655,16 @@ qed simp interpretation Rqrgrp < Rprgrp -proof - - show "Rpsemi(op **)" - apply (rule Rpsemi.intro) apply (rule assoc) done -next - show "Rprgrp_axioms(op **, one, inv)" - apply (rule Rprgrp_axioms.intro) apply (rule rone) apply (rule rinv) done -qed + apply intro_locales + apply (rule assoc) + apply (rule rone) + apply (rule rinv) + done interpretation R2: Rqlgrp ["op #" "rone" "rinv"] -proof - - apply_end (rule Rqsemi.intro) - fix x y z - { - show "(x # y) # z = x # (y # z)" by (rule i_assoc) - next - apply_end (rule Rqlgrp_axioms.intro) - show "rone # x = x" by (rule r_one) - next - show "rinv(x) # x = rone" by (rule r_inv) - } -qed + apply intro_locales (* FIXME: intro_locales is too eager and shouldn't + solve this. *) + done print_interps Rqsemi print_interps Rqlgrp @@ -684,7 +672,7 @@ interpretation Rqlgrp < Rqrgrp - proof (rule Rqrgrp_axioms.intro) + proof intro_locales { fix x have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone) @@ -718,12 +706,12 @@ assumes x: "x = x" and y: "y = y" interpretation Rtriv2 < Rtriv x - apply (rule Rtriv.intro) + apply intro_locales apply (rule x) done interpretation Rtriv2 < Rtriv y - apply (rule Rtriv.intro) + apply intro_locales apply (rule y) done @@ -733,7 +721,7 @@ assumes x: "x = x" and y: "y = y" and z: "z = z" interpretation Rtriv3 < Rtriv2 x y - apply (rule Rtriv2.intro) + apply intro_locales apply (rule x) apply (rule y) done @@ -741,7 +729,7 @@ print_locale Rtriv3 interpretation Rtriv3 < Rtriv2 x z - apply (rule Rtriv2.intro) + apply intro_locales apply (rule x_y_z.x) apply (rule z) done @@ -774,7 +762,8 @@ proof (rule Rpsemi.intro) fix x y z show "(x *** y) *** z = x *** (y *** z)" - by (unfold P_def) (simp add: assoc) + apply (simp only: P_def) apply (simp add: assoc) (* FIXME: unfold P_def fails *) + done qed locale Rsemi_rev = Rpsemi + var rprod (infixl "++" 65) +
--- a/src/HOL/Algebra/CRing.thy Tue Jun 20 14:51:59 2006 +0200 +++ b/src/HOL/Algebra/CRing.thy Tue Jun 20 15:53:44 2006 +0200 @@ -80,7 +80,8 @@ lemma (in abelian_group) a_group: "group (| carrier = carrier G, mult = add G, one = zero G |)" -by (simp add: group_def a_monoid comm_group.axioms a_comm_group) + by (simp add: group_def a_monoid) + (simp add: comm_group.axioms group.axioms a_comm_group) lemmas monoid_record_simps = partial_object.simps monoid.simps @@ -336,16 +337,13 @@ by (auto intro!: monoidI m_assoc) lemma cringI: -(* - includes struct R -*) fixes R (structure) assumes abelian_group: "abelian_group R" and comm_monoid: "comm_monoid R" and l_distr: "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |] ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z" shows "cring R" - proof (rule cring.intro) + proof (intro cring.intro ring.intro) show "ring_axioms R" -- {* Right-distributivity follows from left-distributivity and commutativity. *}
--- a/src/HOL/Algebra/Coset.thy Tue Jun 20 14:51:59 2006 +0200 +++ b/src/HOL/Algebra/Coset.thy Tue Jun 20 15:53:44 2006 +0200 @@ -305,7 +305,7 @@ "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)" by (simp add: setmult_rcos_assoc coset_mult_assoc - subgroup_mult_id subset prems) + subgroup_mult_id normal.axioms subset prems) lemma (in normal) rcos_sum: "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> @@ -315,7 +315,7 @@ lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M" -- {* generalizes @{text subgroup_mult_id} *} by (auto simp add: RCOSETS_def subset - setmult_rcos_assoc subgroup_mult_id prems) + setmult_rcos_assoc subgroup_mult_id normal.axioms prems) subsubsection{*An Equivalence Relation*} @@ -504,7 +504,7 @@ lemma (in normal) rcosets_inv_mult_group_eq: "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H" -by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset prems) +by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset normal.axioms prems) theorem (in normal) factorgroup_is_group: "group (G Mod H)" @@ -552,8 +552,8 @@ text{*The kernel of a homomorphism is a normal subgroup*} lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G" -apply (simp add: group.normal_inv_iff subgroup_kernel group.intro prems) -apply (simp add: kernel_def) +apply (simp add: G.normal_inv_iff subgroup_kernel) +apply (simp add: kernel_def) done lemma (in group_hom) FactGroup_nonempty:
--- a/src/HOL/Algebra/Group.thy Tue Jun 20 14:51:59 2006 +0200 +++ b/src/HOL/Algebra/Group.thy Tue Jun 20 15:53:44 2006 +0200 @@ -189,8 +189,7 @@ assumes Units: "carrier G <= Units G" -lemma (in group) is_group: "group G" - by (rule group.intro [OF prems]) +lemma (in group) is_group: "group G" . theorem groupI: fixes G (structure) @@ -468,7 +467,7 @@ and h: "h \<in> carrier H" shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)" apply (rule group.inv_equality [OF DirProd_group]) - apply (simp_all add: prems group_def group.l_inv) + apply (simp_all add: prems group.l_inv) done text{*This alternative proof of the previous result demonstrates interpret. @@ -643,8 +642,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 (fast intro: comm_group.intro comm_monoid_axioms.intro - is_group prems) + by intro_locales (simp_all add: m_comm) lemma comm_groupI: fixes G (structure) @@ -679,7 +677,7 @@ lemma (in group) subgroup_imp_group: "subgroup H G ==> group (G(| carrier := H |))" - using subgroup.subgroup_is_group [OF _ group.intro] . + by (rule subgroup.subgroup_is_group) lemma (in group) is_monoid [intro, simp]: "monoid G"
--- a/src/HOL/Algebra/Lattice.thy Tue Jun 20 14:51:59 2006 +0200 +++ b/src/HOL/Algebra/Lattice.thy Tue Jun 20 15:53:44 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 (rule total_order.intro) +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 (rule complete_lattice.intro) +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 Jun 20 14:51:59 2006 +0200 +++ b/src/HOL/Algebra/Module.thy Tue Jun 20 15:53:44 2006 +0200 @@ -73,16 +73,26 @@ "!!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" - by (auto intro!: algebra.intro algebra_axioms.intro cring.axioms - module_axioms.intro prems) +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) + apply (simp add: smult_l_distr) + apply (simp add: smult_r_distr) + apply (simp add: smult_assoc1) + apply (simp add: smult_one) +apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms prems)+ +apply (rule algebra_axioms.intro) + apply (simp add: smult_assoc2) +done lemma (in algebra) R_cring: "cring R" - by (rule cring.intro) + by intro_locales lemma (in algebra) M_cring: "cring M" - by (rule cring.intro) + by intro_locales lemma (in algebra) module: "module R M"
--- a/src/HOL/Algebra/UnivPoly.thy Tue Jun 20 14:51:59 2006 +0200 +++ b/src/HOL/Algebra/UnivPoly.thy Tue Jun 20 15:53:44 2006 +0200 @@ -397,8 +397,8 @@ *} interpretation UP_cring < cring P - using UP_cring - by - (erule cring.axioms)+ + by (intro_locales!) + (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms UP_cring)+ subsection {* Polynomials form an Algebra *} @@ -441,8 +441,8 @@ UP_smult_assoc1 UP_smult_assoc2) interpretation UP_cring < algebra R P - using UP_algebra - by - (erule algebra.axioms)+ + by (intro_locales!) + (rule module.axioms algebra.axioms UP_algebra)+ subsection {* Further lemmas involving monomials *} @@ -945,8 +945,7 @@ *} interpretation UP_domain < "domain" P - using UP_domain - by (rule domain.axioms) + by (intro_locales!) (rule domain.axioms UP_domain)+ subsection {* Evaluation Homomorphism and Universal Property*} @@ -1148,9 +1147,15 @@ text {* Interpretation of ring homomorphism lemmas. *} interpretation UP_univ_prop < ring_hom_cring P S Eval - by (unfold Eval_def) - (fast intro!: ring_hom_cring.intro UP_cring cring.axioms prems - intro: ring_hom_cring_axioms.intro eval_ring_hom) + apply (unfold Eval_def) + apply (intro_locales!) + apply (rule ring_hom_cring.axioms) + apply (rule ring_hom_cring.intro) + apply intro_locales + apply (rule eval_ring_hom) + apply rule + done + text {* Further properties of the evaluation homomorphism. *} @@ -1220,8 +1225,8 @@ assumes R: "r \<in> carrier R" and S: "s \<in> carrier S" shows "eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n" proof - - from S interpret UP_univ_prop [R S h P s _] - by (auto intro!: UP_univ_prop_axioms.intro) + interpret UP_univ_prop [R S h P s _] + by (auto! intro: UP_univ_prop.intro UP_univ_prop_axioms.intro) from R show ?thesis by (rule Eval_monom) qed @@ -1271,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 (auto intro: P.cring cring.axioms) +qed intro_locales theorem (in UP_pre_univ_prop) UP_universal_property: assumes S: "s \<in> carrier S" @@ -1291,9 +1296,9 @@ assumes "cring R" and "cring S" and "h \<in> ring_hom R S" - shows "UP_pre_univ_prop R S h " - by (fast intro: UP_pre_univ_prop.intro ring_hom_cring_axioms.intro - cring.axioms prems) + shows "UP_pre_univ_prop R S h" + by (auto intro!: UP_pre_univ_prop.intro ring_hom_cring.intro + ring_hom_cring_axioms.intro UP_cring.intro) constdefs INTEG :: "int ring" @@ -1315,8 +1320,10 @@ *} interpretation INTEG: UP_pre_univ_prop [INTEG INTEG id] + apply simp using INTEG_id_eval - by - (erule UP_pre_univ_prop.axioms)+ + apply simp + done lemma INTEG_closed [intro, simp]: "z \<in> carrier INTEG"
--- a/src/HOL/Algebra/ringsimp.ML Tue Jun 20 14:51:59 2006 +0200 +++ b/src/HOL/Algebra/ringsimp.ML Tue Jun 20 15:53:44 2006 +0200 @@ -16,20 +16,38 @@ val cring_ss = HOL_ss settermless termless_ring; fun cring_normalise ctxt = let - fun ring_filter t = (case HOLogic.dest_Trueprop t of - Const ("CRing.ring_axioms", _) $ Free (s, _) => [s] + fun filter p t = (case HOLogic.dest_Trueprop t of + Const (p', _) $ Free (s, _) => if p = p' then [s] else [] + | _ => []) + handle TERM _ => []; + fun filter21 p t = (case HOLogic.dest_Trueprop t of + Const (p', _) $ Free (s, _) $ _ => if p = p' then [s] else [] | _ => []) handle TERM _ => []; - fun comm_filter t = (case HOLogic.dest_Trueprop t of - Const ("Group.comm_monoid_axioms", _) $ Free (s, _) => [s] + fun filter22 p t = (case HOLogic.dest_Trueprop t of + Const (p', _) $ _ $ Free (s, _) => if p = p' then [s] else [] + | _ => []) + handle TERM _ => []; + fun filter31 p t = (case HOLogic.dest_Trueprop t of + Const (p', _) $ Free (s, _) $ _ $ _ => if p = p' then [s] else [] + | _ => []) + handle TERM _ => []; + fun filter32 p t = (case HOLogic.dest_Trueprop t of + Const (p', _) $ _ $ Free (s, _) $ _ => if p = p' then [s] else [] | _ => []) handle TERM _ => []; val prems = ProofContext.prems_of ctxt; - val rings = List.concat (map (ring_filter o #prop o rep_thm) prems); - val comms = List.concat (map (comm_filter o #prop o rep_thm) prems); - val non_comm_rings = rings \\ comms; - val comm_rings = rings inter_string comms; + val non_comm_rings = List.concat (map (filter "CRing.ring" o #prop o rep_thm) prems); + val comm_rings = List.concat (map (filter "CRing.cring" o #prop o rep_thm) prems) @ + List.concat (map (filter "CRing.domain" o #prop o rep_thm) prems) @ + List.concat (map (filter21 "Module.module" o #prop o rep_thm) prems) @ + List.concat (map (filter21 "Module.algebra" o #prop o rep_thm) prems) @ + List.concat (map (filter22 "Module.algebra" o #prop o rep_thm) prems) @ + List.concat (map (filter "UnivPoly.UP_cring" o #prop o rep_thm) prems) @ + List.concat (map (filter "UnivPoly.UP_domain" o #prop o rep_thm) prems) @ + List.concat (map (filter31 "CRing.ring_hom_cring" o #prop o rep_thm) prems) @ + List.concat (map (filter32 "CRing.ring_hom_cring" o #prop o rep_thm) prems); val _ = tracing ("Non-commutative rings in proof context: " ^ commas non_comm_rings ^ "\nCommutative rings in proof context: " ^ commas comm_rings);
--- a/src/HOL/Finite_Set.thy Tue Jun 20 14:51:59 2006 +0200 +++ b/src/HOL/Finite_Set.thy Tue Jun 20 15:53:44 2006 +0200 @@ -502,13 +502,10 @@ text{* Interpretation of locales: *} interpretation AC_add: ACe ["op +" "0::'a::comm_monoid_add"] - by(auto intro: ACf.intro ACe_axioms.intro add_assoc add_commute) + by intro_locales (auto intro: add_assoc add_commute) interpretation AC_mult: ACe ["op *" "1::'a::comm_monoid_mult"] - apply (fast intro: ACf.intro mult_assoc mult_commute) - apply (fastsimp intro: ACe_axioms.intro mult_assoc mult_commute) - done - + by intro_locales (auto intro: mult_assoc mult_commute) subsubsection{*From @{term foldSet} to @{term fold}*} @@ -1312,7 +1309,7 @@ lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==> setprod f (insert a A) = f a * setprod f A" -by (simp add: setprod_def) + by (simp add: setprod_def) lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1" by (simp add: setprod_def) @@ -1983,7 +1980,7 @@ declare empty_foldSetE [rule del] foldSet.intros [rule del] empty_fold1SetE [rule del] insert_fold1SetE [rule del] - -- {* No more proves involve these relations. *} + -- {* No more proofs involve these relations. *} subsubsection{* Semi-Lattices *} @@ -2061,7 +2058,7 @@ lemma (in ACIfSLlin) strict_above_f_conv: - "x \<cdot> y \<sqsubset> z = (x \<sqsubset> z \<or> y \<sqsubset> z)" + "x \<cdot> y \<sqsubset> z = (x \<sqsubset> z \<or> y \<sqsubset> z)" apply(simp add: strict_below_def above_f_conv) using lin[of y z] lin[of x z] by (auto simp:below_def ACI) @@ -2206,6 +2203,7 @@ lemma (in Lattice) ACIfSL_inf: "ACIfSL inf (op \<sqsubseteq>)" apply(rule ACIfSL.intro) +apply(rule ACIf.intro) apply(rule ACf_inf) apply(rule ACIf.axioms[OF ACIf_inf]) apply(rule ACIfSL_axioms.intro) @@ -2216,7 +2214,9 @@ done lemma (in Lattice) ACIfSL_sup: "ACIfSL sup (%x y. y \<sqsubseteq> x)" +(* FIXME: insert ACf_sup and use intro_locales *) apply(rule ACIfSL.intro) +apply(rule ACIf.intro) apply(rule ACf_sup) apply(rule ACIf.axioms[OF ACIf_sup]) apply(rule ACIfSL_axioms.intro) @@ -2370,43 +2370,43 @@ done interpretation min: ACIf ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"] -apply(rule ACIf_axioms.intro) +apply intro_locales apply(auto simp:min_def) done interpretation max: ACf ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"] -apply(rule ACf.intro) +apply intro_locales apply(auto simp:max_def) done interpretation max: ACIf ["max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"] -apply(rule ACIf_axioms.intro) +apply intro_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(rule ACIfSL_axioms.intro) +apply intro_locales apply(auto simp:min_def) done interpretation min: ACIfSLlin ["min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>" "op <"] -apply(rule ACIfSLlin_axioms.intro) +apply intro_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(rule ACIfSL_axioms.intro) +apply intro_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(rule ACIfSLlin_axioms.intro) +apply intro_locales apply(auto simp:max_def) done @@ -2415,12 +2415,14 @@ apply - apply(rule Min_def) apply(rule Max_def) +apply intro_locales done interpretation min_max: Distrib_Lattice ["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max" "Min" "Max"] -. + by intro_locales + text{* Now we instantiate the recursion equations and declare them simplification rules: *}
--- a/src/HOL/Hyperreal/Filter.thy Tue Jun 20 14:51:59 2006 +0200 +++ b/src/HOL/Hyperreal/Filter.thy Tue Jun 20 15:53:44 2006 +0200 @@ -68,10 +68,11 @@ lemma (in freeultrafilter) finite: "finite A \<Longrightarrow> A \<notin> F" by (erule contrapos_pn, erule infinite) -lemma (in freeultrafilter) filter: "filter F" . +lemma (in freeultrafilter) filter: "filter F" by intro_locales lemma (in freeultrafilter) ultrafilter: "ultrafilter F" -by (rule ultrafilter.intro) + by intro_locales + subsection {* Collect properties *} @@ -385,7 +386,8 @@ with U show "infinite A" by (rule mem_superfrechet_all_infinite) qed from fil ultra free have "freeultrafilter U" - by (rule freeultrafilter.intro) + by (rule freeultrafilter.intro [OF ultrafilter.intro]) + (* FIXME: intro_locales should use chained facts *) thus ?thesis .. qed
--- a/src/HOL/Hyperreal/HyperDef.thy Tue Jun 20 14:51:59 2006 +0200 +++ b/src/HOL/Hyperreal/HyperDef.thy Tue Jun 20 15:53:44 2006 +0200 @@ -58,6 +58,9 @@ by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.finite]) lemma FreeUltrafilterNat_not_finite: "x \<in> FreeUltrafilterNat ==> ~ finite x" +thm FreeUltrafilterNat_mem +thm freeultrafilter.infinite +thm FreeUltrafilterNat_mem [THEN freeultrafilter.infinite] by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.infinite]) lemma FreeUltrafilterNat_empty [simp]: "{} \<notin> FreeUltrafilterNat"
--- a/src/HOL/Orderings.thy Tue Jun 20 14:51:59 2006 +0200 +++ b/src/HOL/Orderings.thy Tue Jun 20 15:53:44 2006 +0200 @@ -388,7 +388,7 @@ interpretation min_max: lower_semilattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"] -apply(rule lower_semilattice_axioms.intro) +apply intro_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,8 +396,7 @@ interpretation min_max: upper_semilattice["op \<le>" "max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"] -apply - -apply(rule upper_semilattice_axioms.intro) +apply intro_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) @@ -405,11 +404,11 @@ interpretation min_max: lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"] -. + by intro_locales interpretation min_max: distrib_lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"] -apply(rule distrib_lattice_axioms.intro) +apply intro_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 Jun 20 14:51:59 2006 +0200 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Tue Jun 20 15:53:44 2006 +0200 @@ -164,7 +164,7 @@ shows "b \<le> \<parallel>f\<parallel>\<hyphen>V" proof - have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" - by (unfold B_def fn_norm_def) (rule fn_norm_works [OF continuous.intro]) + by (unfold B_def fn_norm_def) (rule fn_norm_works) from this and b show ?thesis .. qed @@ -174,7 +174,7 @@ shows "\<parallel>f\<parallel>\<hyphen>V \<le> y" proof - have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" - by (unfold B_def fn_norm_def) (rule fn_norm_works [OF continuous.intro]) + by (unfold B_def fn_norm_def) (rule fn_norm_works) from this and b show ?thesis .. qed @@ -188,7 +188,7 @@ So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge> 0"}, provided the supremum exists and @{text B} is not empty. *} have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" - by (unfold B_def fn_norm_def) (rule fn_norm_works [OF continuous.intro]) + by (unfold B_def fn_norm_def) (rule fn_norm_works) moreover have "0 \<in> B V f" .. ultimately show ?thesis .. qed @@ -207,11 +207,10 @@ proof cases assume "x = 0" then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp - also have "f 0 = 0" .. + also have "f 0 = 0" by rule intro_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 [OF continuous.intro]) + by (unfold B_def fn_norm_def) (rule fn_norm_ge_zero) have "0 \<le> norm x" .. with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff) finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" . @@ -225,7 +224,7 @@ from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f" by (auto simp add: B_def real_divide_def) then show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V" - by (unfold B_def fn_norm_def) (rule fn_norm_ub [OF continuous.intro]) + by (unfold B_def fn_norm_def) (rule fn_norm_ub) qed finally show ?thesis . qed
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Tue Jun 20 14:51:59 2006 +0200 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Tue Jun 20 15:53:44 2006 +0200 @@ -334,17 +334,16 @@ \<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" . - have E_norm: "normed_vectorspace E norm" .. + have E: "vectorspace E" by intro_locales + have E_norm: "normed_vectorspace E norm" by rule intro_locales have FE: "F \<unlhd> E" . - have F: "vectorspace F" .. + have F: "vectorspace F" by rule intro_locales have linearform: "linearform F f" . have F_norm: "normed_vectorspace F norm" - by (rule subspace_normed_vs [OF E_norm]) + by (rule subspace_normed_vs) have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule normed_vectorspace.fn_norm_ge_zero - [OF F_norm continuous.intro, folded B_def fn_norm_def]) - + [OF F_norm (* continuous.intro*), folded B_def fn_norm_def]) txt {* We define a function @{text p} on @{text E} as follows: @{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} *} def p \<equiv> "\<lambda>x. \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>" @@ -393,7 +392,7 @@ fix x assume "x \<in> F" show "\<bar>f x\<bar> \<le> p x" by (unfold p_def) (rule normed_vectorspace.fn_norm_le_cong - [OF F_norm continuous.intro, folded B_def fn_norm_def]) + [OF F_norm, folded B_def fn_norm_def]) qed txt {* Using the fact that @{text p} is a seminorm and @{text f} is bounded @@ -466,7 +465,7 @@ using g_cont by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def]) next - show "continuous F norm f" by (rule continuous.intro) + show "continuous F norm f" . qed qed with linearformE a g_cont show ?thesis by blast
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy Tue Jun 20 14:51:59 2006 +0200 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Tue Jun 20 15:53:44 2006 +0200 @@ -97,11 +97,11 @@ includes subspace F E + normed_vectorspace E shows "normed_vectorspace F norm" proof - show "vectorspace F" by (rule vectorspace) - have "seminorm E norm" . with subset show "seminorm F norm" - by (simp add: seminorm_def) - have "norm_axioms E norm" . with subset show "norm_axioms F norm" - by (simp add: norm_axioms_def) + show "vectorspace F" by (rule vectorspace) intro_locales +next + have "NormedSpace.norm E norm" by intro_locales + with subset show "NormedSpace.norm F norm" + by (simp add: norm_def seminorm_def norm_axioms_def) qed end
--- a/src/HOL/ex/Locales.thy Tue Jun 20 14:51:59 2006 +0200 +++ b/src/HOL/ex/Locales.thy Tue Jun 20 15:53:44 2006 +0200 @@ -481,7 +481,7 @@ semigroup_product_def semigroup.defs) moreover have "semigroup ?G'" and "semigroup ?H'" - using prems by (simp_all add: semigroup_def semigroup.defs) + using prems by (simp_all add: semigroup_def semigroup.defs G.assoc H.assoc) then have "semigroup (semigroup_product ?G' ?H')" .. ultimately show ?thesis by (simp add: I_def semigroup_def) qed
--- a/src/Pure/Isar/element.ML Tue Jun 20 14:51:59 2006 +0200 +++ b/src/Pure/Isar/element.ML Tue Jun 20 15:53:44 2006 +0200 @@ -42,6 +42,7 @@ val conclude_witness: witness -> thm val mark_witness: term -> term val make_witness: term -> thm -> witness + val dest_witness: witness -> term * thm val refine_witness: Proof.state -> Proof.state Seq.seq val rename: (string * (string * mixfix option)) list -> string -> string val rename_var: (string * (string * mixfix option)) list -> string * mixfix -> string * mixfix @@ -283,6 +284,8 @@ fun make_witness t th = Witness (t, th); +fun dest_witness (Witness w) = w; + val refine_witness = Proof.refine (Method.Basic (K (Method.RAW_METHOD (K (ALLGOALS
--- a/src/Pure/Isar/locale.ML Tue Jun 20 14:51:59 2006 +0200 +++ b/src/Pure/Isar/locale.ML Tue Jun 20 15:53:44 2006 +0200 @@ -121,6 +121,18 @@ structure Locale: LOCALE = struct +fun legacy_unvarifyT thm = + let + val cT = Thm.ctyp_of (Thm.theory_of_thm thm); + val tfrees = map (fn ((x, _), S) => SOME (cT (TFree (x, S)))) (Drule.tvars_of thm); + in Drule.instantiate' tfrees [] thm end; + +fun legacy_unvarify raw_thm = + let + val thm = legacy_unvarifyT raw_thm; + val ct = Thm.cterm_of (Thm.theory_of_thm thm); + val frees = map (fn ((x, _), T) => SOME (ct (Free (x, T)))) (Drule.vars_of thm); + in Drule.instantiate' [] frees thm end; (** locale elements and expressions **) @@ -140,25 +152,19 @@ | map_elem _ (Expr e) = Expr e; type locale = - {predicate: cterm list * Element.witness list, - (* CB: For locales with "(open)" this entry is ([], []). - For new-style locales, which declare predicates, if the locale declares - no predicates, this is also ([], []). - If the locale declares predicates, the record field is - ([statement], axioms), where statement is the locale predicate applied - to the (assumed) locale parameters. Axioms contains the projections - from the locale predicate to the normalised assumptions of the locale - (cf. [1], normalisation of locale expressions.) - *) + {axiom: Element.witness list, + (* For locales that define predicates this is [A [A]], where a is the locale + specification. Otherwise []. *) import: expr, (*dynamic import*) elems: (Element.context_i * stamp) list, (* Static content, neither Fixes nor Constrains elements *) params: ((string * typ) * mixfix) list, (*all params*) - lparams: string list, (*local parmas*) + lparams: string list, (*local params*) term_syntax: ((Proof.context -> Proof.context) * stamp) list, (* FIXME depend on morphism *) - regs: ((string * string list) * Element.witness list) list} + regs: ((string * string list) * Element.witness list) list, (* Registrations: indentifiers and witnesses of locales interpreted in the locale. *) - + intros: thm list * thm list} + (* Introduction rules: of delta predicate and locale predicate. *) (* CB: an internal (Int) locale element was either imported or included, an external (Ext) element appears directly in the locale text. *) @@ -268,15 +274,16 @@ val copy = I; val extend = I; - fun join_locs _ ({predicate, import, elems, params, lparams, term_syntax, regs}: locale, + fun join_locs _ ({axiom, import, elems, params, lparams, term_syntax, regs, intros}: locale, {elems = elems', term_syntax = term_syntax', regs = regs', ...}: locale) = - {predicate = predicate, + {axiom = axiom, import = import, elems = gen_merge_lists (eq_snd (op =)) elems elems', params = params, lparams = lparams, term_syntax = Library.merge (eq_snd (op =)) (term_syntax, term_syntax'), - regs = merge_alists regs regs'}; + regs = merge_alists regs regs', + intros = intros}; fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) = (NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2), Symtab.join (K Registrations.join) (regs1, regs2)); @@ -328,12 +335,14 @@ fun change_locale name f thy = let - val {predicate, import, elems, params, lparams, term_syntax, regs} = the_locale thy name; - val (predicate', import', elems', params', lparams', term_syntax', regs') = - f (predicate, import, elems, params, lparams, term_syntax, regs); + val {axiom, import, elems, params, lparams, term_syntax, regs, intros} = + the_locale thy name; + val (axiom', import', elems', params', lparams', term_syntax', regs', intros') = + f (axiom, import, elems, params, lparams, term_syntax, regs, intros); in - put_locale name {predicate = predicate', import = import', elems = elems', - params = params', lparams = lparams', term_syntax = term_syntax', regs = regs'} thy + put_locale name {axiom = axiom', import = import', elems = elems', + params = params', lparams = lparams', term_syntax = term_syntax', regs = regs', + intros = intros'} thy end; @@ -398,8 +407,8 @@ gen_put_registration LocalLocalesData.map ProofContext.theory_of; fun put_registration_in_locale name id = - change_locale name (fn (predicate, import, elems, params, lparams, term_syntax, regs) => - (predicate, import, elems, params, lparams, term_syntax, regs @ [(id, [])])); + change_locale name (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) => + (axiom, import, elems, params, lparams, term_syntax, regs @ [(id, [])], intros)); (* add witness theorem to registration in theory or context, @@ -414,11 +423,11 @@ val add_local_witness = LocalLocalesData.map oo add_witness; fun add_witness_in_locale name id thm = - change_locale name (fn (predicate, import, elems, params, lparams, term_syntax, regs) => + change_locale name (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) => let fun add (id', thms) = if id = id' then (id', thm :: thms) else (id', thms); - in (predicate, import, elems, params, lparams, term_syntax, map add regs) end); + in (axiom, import, elems, params, lparams, term_syntax, map add regs, intros) end); (* printing of registrations *) @@ -790,17 +799,17 @@ identify at top level (top = true); parms is accumulated list of parameters *) let - val {predicate = (_, axioms), import, params, ...} = + val {axiom, import, params, ...} = the_locale thy name; val ps = map (#1 o #1) params; val (ids', parms', _) = identify false import; (* acyclic import dependencies *) + val ids'' = ids' @ [((name, ps), ([], Assumed []))]; val (_, ids''') = add_regs (name, map #1 params) ([], ids''); - - val ids_ax = if top then fst - (fold_map (axiomify ps) ids''' axioms) - else ids'''; + val (_, ids4) = chop (length ids' + 1) ids'''; + val ids5 = ids' @ ids4 @ [((name, ps), ([], Assumed []))]; + val ids_ax = if top then fst (fold_map (axiomify ps) ids5 axiom) else ids5; val syn = Symtab.make (map (apfst fst) params); in (ids_ax, merge_lists parms' ps, syn) end | identify top (Rename (e, xs)) = @@ -837,8 +846,8 @@ fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE | opt => opt); val ren = map #1 ps' ~~ map (fn x => (x, lookup_syn x)) xs; val (params', elems') = - if null ren then ((ps'(*, qs*)), map #1 elems) - else ((map (apfst (Element.rename ren)) ps'(*, map (Element.rename ren) qs*)), + if null ren then (ps', map #1 elems) + else (map (apfst (Element.rename ren)) ps', map (Element.rename_ctxt ren o #1) elems); val elems'' = elems' |> map (Element.map_ctxt {var = I, typ = I, term = I, fact = I, attrib = I, @@ -854,7 +863,7 @@ val idents = gen_rems (eq_fst (op =)) (ids, prev_idents); val syntax = merge_syntax ctxt ids (syn, prev_syntax); (* add types to params and unify them *) - val raw_elemss = (*unique_parms ctxt*) (map (eval syntax) idents); + val raw_elemss = map (eval syntax) idents; val elemss = unify_elemss' ctxt [] raw_elemss (map (apsnd mixfix_type) (Symtab.dest syntax)); (* replace params in ids by params from axioms, adjust types in mode *) @@ -890,22 +899,22 @@ (* NB: derived ids contain only facts at this stage *) -fun activate_elem _ ((ctxt, mode), Fixes fixes) = +fun activate_elem _ _ ((ctxt, mode), Fixes fixes) = ((ctxt |> ProofContext.add_fixes_i fixes |> snd, mode), []) - | activate_elem _ ((ctxt, mode), Constrains _) = + | activate_elem _ _ ((ctxt, mode), Constrains _) = ((ctxt, mode), []) - | activate_elem _ ((ctxt, Assumed axs), Assumes asms) = + | activate_elem ax_in_ctxt _ ((ctxt, Assumed axs), Assumes asms) = let val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms; val ts = maps (map #1 o #2) asms'; val (ps, qs) = chop (length ts) axs; val (_, ctxt') = ctxt |> fold ProofContext.fix_frees ts - |> ProofContext.add_assms_i (axioms_export ps) asms'; + |> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms'; in ((ctxt', Assumed qs), []) end - | activate_elem _ ((ctxt, Derived ths), Assumes asms) = + | activate_elem _ _ ((ctxt, Derived ths), Assumes asms) = ((ctxt, Derived ths), []) - | activate_elem _ ((ctxt, Assumed axs), Defines defs) = + | activate_elem _ _ ((ctxt, Assumed axs), Defines defs) = let val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs; val asms = defs' |> map (fn ((name, atts), (t, ps)) => @@ -915,19 +924,19 @@ ctxt |> fold (ProofContext.fix_frees o #1) asms |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms); in ((ctxt', Assumed axs), []) end - | activate_elem _ ((ctxt, Derived ths), Defines defs) = + | activate_elem _ _ ((ctxt, Derived ths), Defines defs) = ((ctxt, Derived ths), []) - | activate_elem is_ext ((ctxt, mode), Notes facts) = + | activate_elem _ is_ext ((ctxt, mode), Notes facts) = let val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts; val (res, ctxt') = ctxt |> ProofContext.note_thmss_i facts'; in ((ctxt', mode), if is_ext then res else []) end; -fun activate_elems (((name, ps), mode), elems) ctxt = +fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt = let val thy = ProofContext.theory_of ctxt; val ((ctxt', _), res) = - foldl_map (activate_elem (name = "")) ((ProofContext.qualified_names ctxt, mode), elems) + foldl_map (activate_elem ax_in_ctxt (name = "")) ((ProofContext.qualified_names ctxt, mode), elems) handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)] val ctxt'' = if name = "" then ctxt' else let @@ -941,15 +950,15 @@ end in (ProofContext.restore_naming ctxt ctxt'', res) end; -fun activate_elemss prep_facts = +fun activate_elemss ax_in_ctxt prep_facts = fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt => let val elems = map (prep_facts ctxt) raw_elems; val (ctxt', res) = apsnd flat - (activate_elems (((name, ps), mode), elems) ctxt); + (activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt); val elems' = elems |> map (Element.map_ctxt {name = I, var = I, typ = I, term = I, fact = I, attrib = Args.closure}); - in ((((name, ps), elems'), res), ctxt') end); + in (((((name, ps), mode), elems'), res), ctxt') end); in @@ -964,8 +973,8 @@ If read_facts or cert_facts is used for prep_facts, these also remove the internal/external markers from elemss. *) -fun activate_facts prep_facts (ctxt, args) = - let val ((elemss, factss), ctxt') = activate_elemss prep_facts args ctxt |>> split_list +fun activate_facts ax_in_ctxt prep_facts (ctxt, args) = + let val ((elemss, factss), ctxt') = activate_elemss ax_in_ctxt prep_facts args ctxt |>> split_list in (ctxt', (elemss, flat factss)) end; end; @@ -1010,7 +1019,7 @@ merge_syntax ctxt ids' (syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes)) handle Symtab.DUPS xs => err_in_locale ctxt - ("Conflicting syntax (3) for parameters: " ^ commas_quote xs) + ("Conflicting syntax for parameters: " ^ commas_quote xs) (map #1 ids')), [((("", map (rpair NONE o #1) fixes), Assumed []), Ext (Fixes fixes))]) end @@ -1301,7 +1310,7 @@ end; -(* specification of a locale *) +(* Get the specification of a locale *) (*The global specification is made from the parameters and global assumptions, the local specification from the parameters and the @@ -1394,32 +1403,30 @@ val (ps, qs) = chop (length raw_import_params_elemss + length raw_import_elemss) all_elemss'; val (import_ctxt, (import_elemss, _)) = - activate_facts prep_facts (context, ps); + activate_facts false prep_facts (context, ps); val (ctxt, (elemss, _)) = - activate_facts prep_facts (import_ctxt, qs); - val stmt = distinct Term.aconv - (maps (fn ((_, Assumed axs), _) => maps Element.witness_hyps axs - | ((_, Derived _), _) => []) qs); - val cstmt = map (cterm_of thy) stmt; + activate_facts false prep_facts (import_ctxt, qs); in ((((import_ctxt, import_elemss), (ctxt, elemss, syn)), - (parms, spec, defs)), (cstmt, concl)) + (parms, spec, defs)), ([], concl)) +(* FIXME: change signature, remove [] *) end; fun prep_statement prep_locale prep_ctxt raw_locale elems concl ctxt = let val thy = ProofContext.theory_of ctxt; val locale = Option.map (prep_locale thy) raw_locale; - val (locale_stmt, fixed_params, import) = + val (fixed_params, import) = (case locale of - NONE => ([], [], empty) + NONE => ([], empty) | SOME name => - let val {predicate = (stmt, _), params = ps, ...} = the_locale thy name - in (stmt, map fst ps, Locale name) end); - val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), (elems_stmt, concl')) = + let val {params = ps, ...} = the_locale thy name + in (map fst ps, Locale name) end); + val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), ([], concl')) = prep_ctxt false fixed_params import elems concl ctxt; - in (locale, (locale_stmt, locale_ctxt), (elems_stmt, elems_ctxt), concl') end; + in (locale, ([], locale_ctxt), ([], elems_ctxt), concl') end; + (* FIXME: change signatures, remove empty statement lists *) fun prep_expr prep import body ctxt = let @@ -1530,8 +1537,8 @@ fun add_term_syntax loc syn = snd #> syn #> ProofContext.map_theory (change_locale loc - (fn (predicate, import, elems, params, lparams, term_syntax, regs) => - (predicate, import, elems, params, lparams, (syn, stamp ()) :: term_syntax, regs))); + (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) => + (axiom, import, elems, params, lparams, (syn, stamp ()) :: term_syntax, regs, intros))); fun init_term_syntax loc ctxt = fold_rev (fn (f, _) => fn ctxt' => f ctxt') @@ -1557,11 +1564,11 @@ fun gen_thmss prep_facts global_results kind loc args (view, ctxt) thy = let val (ctxt', ([(_, [Notes args'])], facts)) = - activate_facts prep_facts (ctxt, [((("", []), Assumed []), [Ext (Notes args)])]); + activate_facts true prep_facts (ctxt, [((("", []), Assumed []), [Ext (Notes args)])]); val (facts', thy') = thy - |> change_locale loc (fn (predicate, import, elems, params, lparams, term_syntax, regs) => - (predicate, import, elems @ [(Notes args', stamp ())], params, lparams, term_syntax, regs)) + |> change_locale loc (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) => + (axiom, import, elems @ [(Notes args', stamp ())], params, lparams, term_syntax, regs, intros)) |> note_thmss_registrations kind loc args' |> global_results (map (#1 o #1) args' ~~ map #2 facts) (view, ctxt); in ((facts, facts'), (ProofContext.transfer thy' ctxt', thy')) end; @@ -1670,18 +1677,19 @@ in ((statement, intro, axioms), defs_thy) end; fun assumes_to_notes (Assumes asms) axms = - axms - |> fold_map (fn (a, spec) => fn axs => - let val (ps, qs) = chop (length spec) axs - in ((a, [(ps, [])]), qs) end) asms - |-> (pair o Notes) + fold_map (fn (a, spec) => fn axs => + let val (ps, qs) = chop (length spec) axs + in ((a, [(ps, [])]), qs) end) asms axms + |> apfst Notes | assumes_to_notes e axms = (e, axms); -(* CB: changes only "new" elems, these have identifier ("", _). *) +(* CB: the following two change only "new" elems, these have identifier ("", _). *) + +(* turn Assumes into Notes elements *) -fun change_elemss axioms elemss = +fun change_assumes_elemss axioms elemss = let - fun change (id as ("", _), es)= + fun change (id as ("", _), es) = fold_map assumes_to_notes (map (Element.map_ctxt_values I I (Element.satisfy_thm axioms)) es) #-> (fn es' => pair (id, es')) @@ -1690,44 +1698,53 @@ fst (fold_map change elemss (map Element.conclude_witness axioms)) end; +(* adjust hyps of Notes elements *) + +fun change_elemss_hyps axioms elemss = + let + fun change (id as ("", _), es) = + (id, map (fn e as (Notes _) => Element.map_ctxt_values I I (Element.satisfy_thm axioms) e + | e => e) es) + | change e = e; + in map change elemss end; + in (* CB: main predicate definition function *) fun define_preds bname (parms, ((exts, exts'), (ints, ints')), defs) elemss thy = let - val ((elemss', more_ts), thy') = - if null exts then ((elemss, []), thy) + val ((elemss', more_ts), a_elem, a_intro, thy') = + if null exts then ((elemss, []), [], [], thy) else let val aname = if null ints then bname else bname ^ "_" ^ axiomsN; val ((statement, intro, axioms), def_thy) = thy |> def_pred aname parms defs exts exts'; - val elemss' = - change_elemss axioms elemss - @ [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, [])])]])]; - in - def_thy - |> PureThy.note_thmss_qualified "" aname [((introN, []), [([intro], [])])] - |> snd - |> pair (elemss', [statement]) - end; - val (predicate, thy'') = - if null ints then (([], []), thy') + val elemss' = change_assumes_elemss axioms elemss; + val def_thy' = def_thy + |> PureThy.note_thmss_qualified "" aname [((introN, []), [([intro], [])])] + |> snd + val a_elem = [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, [])])]])]; + in ((elemss', [statement]), a_elem, [intro], def_thy') end; + val (predicate, stmt', elemss'', b_intro, thy'') = + if null ints then (([], []), more_ts, elemss' @ a_elem, [], thy') else let val ((statement, intro, axioms), def_thy) = thy' |> def_pred bname parms defs (ints @ more_ts) (ints' @ more_ts); val cstatement = Thm.cterm_of def_thy statement; - in + val elemss'' = change_elemss_hyps axioms elemss'; + val def_thy' = def_thy |> PureThy.note_thmss_qualified "" bname [((introN, []), [([intro], [])]), ((axiomsN, []), [(map (Drule.standard o Element.conclude_witness) axioms, [])])] - |> snd - |> pair ([cstatement], axioms) - end; - in ((elemss', predicate), thy'') end; + |> snd; + val b_elem = [(("", []), + [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, [])])]])]; + in (([cstatement], axioms), [statement], elemss'' @ b_elem, [intro], def_thy') end; + in (((elemss'', predicate, stmt'), (a_intro, b_intro)), thy'') end; end; @@ -1736,6 +1753,24 @@ local +(* turn Defines into Notes elements, accumulate definition terms *) + +fun defines_to_notes true thy (Defines defs) ts = + fold_map (fn (a, (def, _)) => fn ts => + ((a, [([assume (cterm_of thy def)], [])]), ts @ [def])) defs ts + |> apfst (SOME o Notes) + | defines_to_notes false _ (Defines defs) ts = + fold (fn (_, (def, _)) => fn ts => ts @ [def]) defs ts |> pair NONE + | defines_to_notes _ _ e ts = (SOME e, ts); + +fun change_defines_elemss thy elemss ts = + let + fun change (id as (n, _), es) ts = + let + val (es', ts') = fold_map (defines_to_notes (n="") thy) es ts + in ((id, map_filter I es'), ts') end + in fold_map change elemss ts end; + fun gen_add_locale prep_ctxt prep_expr do_predicate bname raw_import raw_body thy = let @@ -1745,9 +1780,10 @@ val thy_ctxt = ProofContext.init thy; val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)), - text as (parms, ((_, exts'), _), _)) = + text as (parms, ((_, exts'), _), defs)) = prep_ctxt raw_import raw_body thy_ctxt; - val elemss = import_elemss @ body_elemss; + val elemss = import_elemss @ body_elemss |> + map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE); val import = prep_expr thy raw_import; val extraTs = foldr Term.add_term_tfrees [] exts' \\ @@ -1755,9 +1791,25 @@ val _ = if null extraTs then () else warning ("Additional type variable(s) in locale specification " ^ quote bname); - val ((elemss', predicate as (predicate_statement, predicate_axioms)), pred_thy) = - if do_predicate then thy |> define_preds bname text elemss - else ((elemss, ([], [])), thy); + val ((((elemss', predicate as (predicate_statement, predicate_axioms), stmt'), intros), + pred_thy), (import, regs)) = + if do_predicate then + let + val (elemss', defs) = change_defines_elemss thy elemss []; + val elemss'' = elemss' @ + [(("", []), [Defines (map (fn t => (("", []), (t, []))) defs)])]; + val (((elemss''', predicate as (_, axioms), stmt'), intros), thy') = + define_preds bname text elemss'' thy; + fun mk_regs elemss wits = + fold_map (fn (id, elems) => fn wts => let + val ts = List.concat (List.mapPartial (fn (Assumes asms) => + SOME (List.concat (map (map #1 o #2) asms)) | _ => NONE) elems); + val (wts1, wts2) = chop (length ts) wts + in ((apsnd (map fst) id, wts1), wts2) end) elemss wits |> fst; + val regs = mk_regs elemss''' axioms |> + map_filter (fn (("", _), _) => NONE | e => SOME e); + in ((((elemss''', predicate, stmt'), intros), thy'), (empty, regs)) end + else ((((elemss, ([], []), []), ([], [])), thy), (import, [])); fun axiomify axioms elemss = (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let @@ -1767,23 +1819,25 @@ in (axs2, ((id, Assumed axs1), elems)) end) |> snd; val pred_ctxt = ProofContext.init pred_thy; - val (ctxt, (_, facts)) = activate_facts (K I) + val (ctxt, (_, facts)) = activate_facts true (K I) (pred_ctxt, axiomify predicate_axioms elemss'); val export = ProofContext.export_view predicate_statement ctxt thy_ctxt; val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])])); val elems' = maps #2 (filter (equal "" o #1 o #1) elemss'); val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems'; + val axs' = map (Element.assume_witness pred_thy) stmt'; val thy' = pred_thy |> PureThy.note_thmss_qualified "" bname facts' |> snd |> declare_locale name |> put_locale name - {predicate = predicate, + {axiom = axs', import = import, elems = map (fn e => (e, stamp ())) elems'', params = params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))), - lparams = map #1 (params_of body_elemss), + lparams = map #1 (params_of' body_elemss), term_syntax = [], - regs = []}; + regs = regs, + intros = intros}; in ((name, ProofContext.transfer thy' body_ctxt), thy') end; in @@ -1891,6 +1945,51 @@ end; +(** Normalisation of locale statements --- + discharges goals implied by interpretations **) + +local + +fun locale_assm_intros thy = + Symtab.fold (fn (_, {intros = (a, _), ...}) => fn intros => (a @ intros)) + (#2 (GlobalLocalesData.get thy)) []; +fun locale_base_intros thy = + Symtab.fold (fn (_, {intros = (_, b), ...}) => fn intros => (b @ intros)) + (#2 (GlobalLocalesData.get thy)) []; + +fun all_witnesses ctxt = + let + val thy = ProofContext.theory_of ctxt; + fun get registrations = Symtab.fold (fn (_, regs) => fn thms => + (Registrations.dest regs |> map (fn (_, (_, wits)) => + map Element.conclude_witness wits) |> flat) @ thms) + registrations []; + val globals = get (#3 (GlobalLocalesData.get thy)); + val locals = get (LocalLocalesData.get ctxt); + in globals @ locals end; +(* FIXME: proper varification *) + +in + +fun intro_locales_tac (ctxt, eager) facts st = + let + val wits = all_witnesses ctxt |> map Thm.varifyT; + val thy = ProofContext.theory_of ctxt; + val intros = locale_base_intros thy @ (if eager then locale_assm_intros thy else []); + in + (ALLGOALS (Method.insert_tac facts THEN' + REPEAT_ALL_NEW (resolve_tac (wits @ intros))) + THEN Tactic.distinct_subgoals_tac) st + end; + +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")]); + +end; + (** Interpretation commands **) @@ -1941,7 +2040,7 @@ (* add witnesses of Derived elements *) |> fold (fn (id, thms) => fold (add_wit id o Element.satisfy_witness prems) thms) (map_filter (fn ((_, Assumed _), _) => NONE - | ((id, Derived thms), _) => SOME (id, thms)) all_elemss) + | ((id, Derived thms), _) => SOME (id, thms)) new_elemss) val disch' = std o Element.satisfy_thm prems; (* FIXME *) in @@ -1957,7 +2056,7 @@ Attrib.attribute_i Drule.standard (fn (name, ps) => put_global_registration (name, map Logic.varify ps)) (fn (n, ps) => add_global_witness (n, map Logic.varify ps) o - Element.map_witness (fn (t, th) => (Logic.legacy_unvarify t, Drule.unvarify th)) + Element.map_witness (fn (t, th) => (Logic.legacy_unvarify t, legacy_unvarify th)) (* FIXME *)) x; fun local_activate_facts_elemss x = gen_activate_facts_elemss @@ -2041,9 +2140,10 @@ (* restore "small" ids *) val ids' = map (fn ((n, ps), (_, mode)) => ((n, map (fn p => Free (p, (the o AList.lookup (op =) parms) p)) ps), mode)) - (params_ids @ ids); + ids; + val (_, all_elemss') = chop (length raw_params_elemss) all_elemss (* instantiate ids and elements *) - val inst_elemss = (ids' ~~ all_elemss) |> map (fn (((n, ps), _), ((_, mode), elems)) => + val inst_elemss = (ids' ~~ all_elemss') |> map (fn (((n, ps), _), ((_, mode), elems)) => ((n, map (Element.inst_term insts) ps), map (fn Int e => Element.inst_ctxt thy insts e) elems) |> apfst (fn id => (id, map_mode (map (Element.inst_witness thy insts)) mode)));
--- a/src/ZF/Constructible/DPow_absolute.thy Tue Jun 20 14:51:59 2006 +0200 +++ b/src/ZF/Constructible/DPow_absolute.thy Tue Jun 20 15:53:44 2006 +0200 @@ -294,7 +294,7 @@ theorem M_DPow_L: "PROP M_DPow(L)" apply (rule M_DPow.intro) - apply (rule M_satisfies.axioms [OF M_satisfies_L])+ + apply (rule M_satisfies_L) apply (rule M_DPow_axioms_L) done @@ -596,10 +596,10 @@ done theorem M_Lset_L: "PROP M_Lset(L)" -apply (rule M_Lset.intro) - apply (rule M_DPow.axioms [OF M_DPow_L])+ -apply (rule M_Lset_axioms_L) -done + apply (rule M_Lset.intro) + apply (rule M_DPow_L) + apply (rule M_Lset_axioms_L) + done text{*Finally: the point of the whole theory!*} lemmas Lset_closed = M_Lset.Lset_closed [OF M_Lset_L]
--- a/src/ZF/Constructible/Rank_Separation.thy Tue Jun 20 14:51:59 2006 +0200 +++ b/src/ZF/Constructible/Rank_Separation.thy Tue Jun 20 15:53:44 2006 +0200 @@ -122,10 +122,10 @@ done theorem M_ordertype_L: "PROP M_ordertype(L)" -apply (rule M_ordertype.intro) - apply (rule M_basic.axioms [OF M_basic_L])+ -apply (rule M_ordertype_axioms_L) -done + apply (rule M_ordertype.intro) + apply (rule M_basic_L) + apply (rule M_ordertype_axioms_L) + done subsection{*The Locale @{text "M_wfrank"}*} @@ -224,7 +224,7 @@ theorem M_wfrank_L: "PROP M_wfrank(L)" apply (rule M_wfrank.intro) - apply (rule M_trancl.axioms [OF M_trancl_L])+ + apply (rule M_trancl_L) apply (rule M_wfrank_axioms_L) done
--- a/src/ZF/Constructible/Rec_Separation.thy Tue Jun 20 14:51:59 2006 +0200 +++ b/src/ZF/Constructible/Rec_Separation.thy Tue Jun 20 15:53:44 2006 +0200 @@ -181,10 +181,9 @@ done theorem M_trancl_L: "PROP M_trancl(L)" -by (rule M_trancl.intro - [OF M_trivial_L M_basic_axioms_L M_trancl_axioms_L]) +by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L]) -interpretation M_trancl [L] by (rule M_trancl_axioms_L) +interpretation M_trancl [L] by (rule M_trancl_L) subsection{*@{term L} is Closed Under the Operator @{term list}*} @@ -366,11 +365,11 @@ theorem M_datatypes_L: "PROP M_datatypes(L)" apply (rule M_datatypes.intro) - apply (rule M_trancl.axioms [OF M_trancl_L])+ - apply (rule M_datatypes_axioms_L) - done + apply (rule M_trancl_L) + apply (rule M_datatypes_axioms_L) + done -interpretation M_datatypes [L] by (rule M_datatypes_axioms_L) +interpretation M_datatypes [L] by (rule M_datatypes_L) subsection{*@{term L} is Closed Under the Operator @{term eclose}*} @@ -429,11 +428,11 @@ theorem M_eclose_L: "PROP M_eclose(L)" apply (rule M_eclose.intro) - apply (rule M_datatypes.axioms [OF M_datatypes_L])+ + apply (rule M_datatypes_L) apply (rule M_eclose_axioms_L) done -interpretation M_eclose [L] by (rule M_eclose_axioms_L) +interpretation M_eclose [L] by (rule M_eclose_L) end
--- a/src/ZF/Constructible/Satisfies_absolute.thy Tue Jun 20 14:51:59 2006 +0200 +++ b/src/ZF/Constructible/Satisfies_absolute.thy Tue Jun 20 15:53:44 2006 +0200 @@ -473,9 +473,10 @@ satisfies_b(A), satisfies_is_b(M,A), satisfies_c(A), satisfies_is_c(M,A), satisfies_d(A), satisfies_is_d(M,A))" -apply (rule Formula_Rec.intro, assumption+) -apply (erule Formula_Rec_axioms_M) -done + apply (rule Formula_Rec.intro) + apply (rule M_satisfies.axioms) apply assumption + apply (erule Formula_Rec_axioms_M) + done lemmas (in M_satisfies) satisfies_closed' = Formula_Rec.formula_rec_closed [OF Formula_Rec_M] @@ -1010,10 +1011,10 @@ done theorem M_satisfies_L: "PROP M_satisfies(L)" -apply (rule M_satisfies.intro) - apply (rule M_eclose.axioms [OF M_eclose_L])+ -apply (rule M_satisfies_axioms_L) -done + apply (rule M_satisfies.intro) + apply (rule M_eclose_L) + apply (rule M_satisfies_axioms_L) + done text{*Finally: the point of the whole theory!*} lemmas satisfies_closed = M_satisfies.satisfies_closed [OF M_satisfies_L]
--- a/src/ZF/Constructible/Separation.thy Tue Jun 20 14:51:59 2006 +0200 +++ b/src/ZF/Constructible/Separation.thy Tue Jun 20 15:53:44 2006 +0200 @@ -305,7 +305,7 @@ theorem M_basic_L: "PROP M_basic(L)" by (rule M_basic.intro [OF M_trivial_L M_basic_axioms_L]) -interpretation M_basic [L] by (rule M_basic_axioms_L) +interpretation M_basic [L] by (rule M_basic_L) end
--- a/src/ZF/ex/Group.thy Tue Jun 20 14:51:59 2006 +0200 +++ b/src/ZF/ex/Group.thy Tue Jun 20 15:53:44 2006 +0200 @@ -89,8 +89,7 @@ assumes inv_ex: "\<And>x. x \<in> carrier(G) \<Longrightarrow> \<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>" -lemma (in group) is_group [simp]: "group(G)" - by (rule group.intro [OF prems]) +lemma (in group) is_group [simp]: "group(G)" . theorem groupI: includes struct G @@ -328,7 +327,7 @@ and h: "h \<in> carrier(H)" shows "inv \<^bsub>G \<Otimes> H\<^esub> <g, h> = <inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h>" apply (rule group.inv_equality [OF DirProdGroup_group]) - apply (simp_all add: prems group_def group.l_inv) + apply (simp_all add: prems group.l_inv) done subsection {* Isomorphisms *} @@ -636,8 +635,7 @@ lemma (in group) normalI: "subgroup(H,G) \<Longrightarrow> (\<forall>x \<in> carrier(G). H #> x = x <# H) \<Longrightarrow> H \<lhd> G"; -apply (simp add: normal_def normal_axioms_def, auto) - by (blast intro: prems) + by (simp add: normal_def normal_axioms_def) lemma (in normal) inv_op_closed1: "\<lbrakk>x \<in> carrier(G); h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<cdot> h \<cdot> x \<in> H" @@ -822,8 +820,8 @@ lemma (in normal) rcos_mult_step3: "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<cdot> y)" -by (simp add: setmult_rcos_assoc coset_mult_assoc - subgroup_mult_id subset prems) + by (simp add: setmult_rcos_assoc coset_mult_assoc + subgroup_mult_id subset prems normal.axioms) lemma (in normal) rcos_sum: "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> @@ -833,7 +831,7 @@ lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M" -- {* generalizes @{text subgroup_mult_id} *} by (auto simp add: RCOSETS_def subset - setmult_rcos_assoc subgroup_mult_id prems) + setmult_rcos_assoc subgroup_mult_id prems normal.axioms) subsubsection{*Two distinct right cosets are disjoint*} @@ -1008,7 +1006,7 @@ lemma (in normal) rcosets_inv_mult_group_eq: "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H" -by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset prems) +by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset prems normal.axioms) theorem (in normal) factorgroup_is_group: "group (G Mod H)"