# HG changeset patch # User ballarin # Date 1153329958 -7200 # Node ID ed7bced29e1bd4972d34e14a09e63465196baa4b # Parent fe5fd4fd41148090b84a65960308d33d837a975a Reimplemented algebra method; now controlled by attribute. diff -r fe5fd4fd4114 -r ed7bced29e1b src/HOL/Algebra/CRing.thy --- a/src/HOL/Algebra/CRing.thy Wed Jul 19 19:24:02 2006 +0200 +++ b/src/HOL/Algebra/CRing.thy Wed Jul 19 19:25:58 2006 +0200 @@ -446,23 +446,31 @@ "[| x \ carrier R; y \ carrier R |] ==> x \ y = x \ \ y" by (simp only: a_minus_def) -lemmas (in ring) ring_simprules = +text {* Setup algebra method: + compute distributive normal form in locale contexts *} + +use "ringsimp.ML" + +setup Algebra.setup + +lemmas (in ring) ring_simprules + [algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] = a_closed zero_closed a_inv_closed minus_closed m_closed one_closed a_assoc l_zero l_neg a_comm m_assoc l_one l_distr minus_eq r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero a_lcomm r_distr l_null r_null l_minus r_minus -lemmas (in cring) cring_simprules = +lemmas (in cring) + [algebra del: ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] = + _ + +lemmas (in cring) cring_simprules + [algebra add: cring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] = a_closed zero_closed a_inv_closed minus_closed m_closed one_closed a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_eq r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus -use "ringsimp.ML" - -method_setup algebra = - {* Method.ctxt_args cring_normalise *} - {* computes distributive normal form in locale context cring *} lemma (in cring) nat_pow_zero: "(n::nat) ~= 0 ==> \ (^) n = \" diff -r fe5fd4fd4114 -r ed7bced29e1b src/HOL/Algebra/Module.thy --- a/src/HOL/Algebra/Module.thy Wed Jul 19 19:24:02 2006 +0200 +++ b/src/HOL/Algebra/Module.thy Wed Jul 19 19:25:58 2006 +0200 @@ -106,11 +106,11 @@ "x \ carrier M ==> \ \\<^bsub>M\<^esub> x = \\<^bsub>M\<^esub>" proof - assume M: "x \ carrier M" - note facts = M smult_closed + note facts = M smult_closed [OF R.zero_closed] from facts have "\ \\<^bsub>M\<^esub> x = (\ \\<^bsub>M\<^esub> x \\<^bsub>M\<^esub> \ \\<^bsub>M\<^esub> x) \\<^bsub>M\<^esub> \\<^bsub>M\<^esub> (\ \\<^bsub>M\<^esub> x)" by algebra also from M have "... = (\ \ \) \\<^bsub>M\<^esub> x \\<^bsub>M\<^esub> \\<^bsub>M\<^esub> (\ \\<^bsub>M\<^esub> x)" by (simp add: smult_l_distr del: R.l_zero R.r_zero) - also from facts have "... = \\<^bsub>M\<^esub>" by algebra + also from facts have "... = \\<^bsub>M\<^esub>" apply algebra apply algebra done finally show ?thesis . qed @@ -131,12 +131,15 @@ "[| a \ carrier R; x \ carrier M |] ==> (\a) \\<^bsub>M\<^esub> x = \\<^bsub>M\<^esub> (a \\<^bsub>M\<^esub> x)" proof - assume RM: "a \ carrier R" "x \ carrier M" - note facts = RM smult_closed + from RM have a_smult: "a \\<^bsub>M\<^esub> x \ carrier M" by simp + from RM have ma_smult: "\a \\<^bsub>M\<^esub> x \ carrier M" by simp + note facts = RM a_smult ma_smult from facts have "(\a) \\<^bsub>M\<^esub> x = (\a \\<^bsub>M\<^esub> x \\<^bsub>M\<^esub> a \\<^bsub>M\<^esub> x) \\<^bsub>M\<^esub> \\<^bsub>M\<^esub>(a \\<^bsub>M\<^esub> x)" by algebra also from RM have "... = (\a \ a) \\<^bsub>M\<^esub> x \\<^bsub>M\<^esub> \\<^bsub>M\<^esub>(a \\<^bsub>M\<^esub> x)" by (simp add: smult_l_distr) - also from facts smult_l_null have "... = \\<^bsub>M\<^esub>(a \\<^bsub>M\<^esub> x)" by algebra + also from facts smult_l_null have "... = \\<^bsub>M\<^esub>(a \\<^bsub>M\<^esub> x)" + apply algebra apply algebra done finally show ?thesis . qed diff -r fe5fd4fd4114 -r ed7bced29e1b src/HOL/Algebra/ringsimp.ML --- a/src/HOL/Algebra/ringsimp.ML Wed Jul 19 19:24:02 2006 +0200 +++ b/src/HOL/Algebra/ringsimp.ML Wed Jul 19 19:25:58 2006 +0200 @@ -1,68 +1,95 @@ (* - Title: Normalisation method for locale cring + Title: Normalisation method for locales ring and cring Id: $Id$ Author: Clemens Ballarin Copyright: TU Muenchen *) -(*** Term order for commutative rings ***) +signature ALGEBRA = +sig + val print_structures: Context.generic -> unit + val setup: Theory.theory -> Theory.theory +end; + +structure Algebra: ALGEBRA = +struct + + +(** Theory and context data **) + +fun struct_eq ((s1, ts1), (s2, ts2)) = + (s1 = s2) andalso equal_lists (op aconv) (ts1, ts2); -fun ring_ord (Const (a, _)) = - find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "CRing.a_inv", - "CRing.minus", "Group.monoid.one", "Group.monoid.mult"] - | ring_ord _ = ~1; +structure AlgebraData = GenericDataFun +(struct + val name = "Algebra/algebra"; + type T = ((string * term list) * thm list) list; + (* Algebraic structures: + identifier of the structure, list of operations and simp rules, + identifier and operations identify the structure uniquely. *) + val empty = []; + val extend = I; + fun merge _ (structs1, structs2) = gen_merge_lists + (fn ((s1, _), (s2, _)) => struct_eq (s1, s2)) structs1 structs2; + fun print generic structs = + let + val ctxt = Context.proof_of generic; + val pretty_term = Pretty.quote o ProofContext.pretty_term ctxt; + fun pretty_struct ((s, ts), _) = Pretty.block + [Pretty.str s, Pretty.str ":", Pretty.brk 1, + Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))]; + in + Pretty.big_list "Algebraic structures:" (map pretty_struct structs) |> + Pretty.writeln + end +end); -fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS); +val print_structures = AlgebraData.print; -val cring_ss = HOL_ss settermless termless_ring; + +(** Method **) -fun cring_normalise ctxt = let - 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 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 _ => []; +fun struct_tac ((s, ts), simps) = + let + val ops = map (fst o Term.strip_comb) ts; + fun ord (Const (a, _)) = find_index (fn (Const (b, _)) => a=b | _ => false) ops + | ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops; + fun less (a, b) = (Term.term_lpo ord (a, b) = LESS); + in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end; + +fun algebra_tac ctxt = + let val _ = print_structures (Context.Proof ctxt) + in EVERY' (map (fn s => TRY o struct_tac s) (AlgebraData.get (Context.Proof ctxt))) end; + +val method = + Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' HEADGOAL (algebra_tac ctxt)) + + +(** Attribute **) - val prems = ProofContext.prems_of ctxt; - 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); - val simps = - List.concat (map (fn s => ProofContext.get_thms ctxt (Name (s ^ ".ring_simprules"))) - non_comm_rings) @ - List.concat (map (fn s => ProofContext.get_thms ctxt (Name (s ^ ".cring_simprules"))) - comm_rings); - in Method.SIMPLE_METHOD' HEADGOAL (asm_full_simp_tac (cring_ss addsimps simps)) - end; +fun add_struct_thm s = + Thm.declaration_attribute (fn thm => fn ctxt => + AlgebraData.map (fn structs => + if AList.defined struct_eq structs s + then AList.map_entry struct_eq s (fn thms => thm :: thms) structs + else (s, [thm])::structs) ctxt); +fun del_struct s = + Thm.declaration_attribute (fn _ => fn ctxt => + AlgebraData.map (AList.delete struct_eq s) ctxt); -(* -val ring_ss = HOL_basic_ss settermless termless_ring addsimps - [a_assoc, l_zero, l_neg, a_comm, m_assoc, l_one, l_distr, m_comm, minus_def, - r_zero, r_neg, r_neg2, r_neg1, minus_add, minus_minus, minus0, - a_lcomm, m_lcomm, (*r_one,*) r_distr, l_null, r_null, l_minus, r_minus]; -*) +val attribute = Attrib.syntax + (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon || + Scan.succeed true) -- Scan.lift Args.name -- + Scan.repeat Args.term + >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts))); + + +(** Setup **) + +val setup = + AlgebraData.init #> + Method.add_methods [("algebra", method, "normalisation of algebraic structure")] #> + Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")]; + + +end; (* struct *)