Reimplemented algebra method; now controlled by attribute.
authorballarin
Wed Jul 19 19:25:58 2006 +0200 (2006-07-19)
changeset 20168ed7bced29e1b
parent 20167 fe5fd4fd4114
child 20169 52173f7687fd
Reimplemented algebra method; now controlled by attribute.
src/HOL/Algebra/CRing.thy
src/HOL/Algebra/Module.thy
src/HOL/Algebra/ringsimp.ML
     1.1 --- a/src/HOL/Algebra/CRing.thy	Wed Jul 19 19:24:02 2006 +0200
     1.2 +++ b/src/HOL/Algebra/CRing.thy	Wed Jul 19 19:25:58 2006 +0200
     1.3 @@ -446,23 +446,31 @@
     1.4    "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
     1.5    by (simp only: a_minus_def)
     1.6  
     1.7 -lemmas (in ring) ring_simprules =
     1.8 +text {* Setup algebra method:
     1.9 +  compute distributive normal form in locale contexts *}
    1.10 +
    1.11 +use "ringsimp.ML"
    1.12 +
    1.13 +setup Algebra.setup
    1.14 +
    1.15 +lemmas (in ring) ring_simprules
    1.16 +  [algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
    1.17    a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
    1.18    a_assoc l_zero l_neg a_comm m_assoc l_one l_distr minus_eq
    1.19    r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
    1.20    a_lcomm r_distr l_null r_null l_minus r_minus
    1.21  
    1.22 -lemmas (in cring) cring_simprules =
    1.23 +lemmas (in cring)
    1.24 +  [algebra del: ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
    1.25 +  _
    1.26 +
    1.27 +lemmas (in cring) cring_simprules
    1.28 +  [algebra add: cring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
    1.29    a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
    1.30    a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_eq
    1.31    r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
    1.32    a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus
    1.33  
    1.34 -use "ringsimp.ML"
    1.35 -
    1.36 -method_setup algebra =
    1.37 -  {* Method.ctxt_args cring_normalise *}
    1.38 -  {* computes distributive normal form in locale context cring *}
    1.39  
    1.40  lemma (in cring) nat_pow_zero:
    1.41    "(n::nat) ~= 0 ==> \<zero> (^) n = \<zero>"
     2.1 --- a/src/HOL/Algebra/Module.thy	Wed Jul 19 19:24:02 2006 +0200
     2.2 +++ b/src/HOL/Algebra/Module.thy	Wed Jul 19 19:25:58 2006 +0200
     2.3 @@ -106,11 +106,11 @@
     2.4    "x \<in> carrier M ==> \<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>"
     2.5  proof -
     2.6    assume M: "x \<in> carrier M"
     2.7 -  note facts = M smult_closed
     2.8 +  note facts = M smult_closed [OF R.zero_closed]
     2.9    from facts have "\<zero> \<odot>\<^bsub>M\<^esub> x = (\<zero> \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> \<zero> \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub> (\<zero> \<odot>\<^bsub>M\<^esub> x)" by algebra
    2.10    also from M have "... = (\<zero> \<oplus> \<zero>) \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub> (\<zero> \<odot>\<^bsub>M\<^esub> x)"
    2.11      by (simp add: smult_l_distr del: R.l_zero R.r_zero)
    2.12 -  also from facts have "... = \<zero>\<^bsub>M\<^esub>" by algebra
    2.13 +  also from facts have "... = \<zero>\<^bsub>M\<^esub>" apply algebra apply algebra done
    2.14    finally show ?thesis .
    2.15  qed
    2.16  
    2.17 @@ -131,12 +131,15 @@
    2.18    "[| a \<in> carrier R; x \<in> carrier M |] ==> (\<ominus>a) \<odot>\<^bsub>M\<^esub> x = \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> x)"
    2.19  proof -
    2.20    assume RM: "a \<in> carrier R" "x \<in> carrier M"
    2.21 -  note facts = RM smult_closed
    2.22 +  from RM have a_smult: "a \<odot>\<^bsub>M\<^esub> x \<in> carrier M" by simp
    2.23 +  from RM have ma_smult: "\<ominus>a \<odot>\<^bsub>M\<^esub> x \<in> carrier M" by simp
    2.24 +  note facts = RM a_smult ma_smult
    2.25    from facts have "(\<ominus>a) \<odot>\<^bsub>M\<^esub> x = (\<ominus>a \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
    2.26      by algebra
    2.27    also from RM have "... = (\<ominus>a \<oplus> a) \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
    2.28      by (simp add: smult_l_distr)
    2.29 -  also from facts smult_l_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)" by algebra
    2.30 +  also from facts smult_l_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
    2.31 +    apply algebra apply algebra done
    2.32    finally show ?thesis .
    2.33  qed
    2.34  
     3.1 --- a/src/HOL/Algebra/ringsimp.ML	Wed Jul 19 19:24:02 2006 +0200
     3.2 +++ b/src/HOL/Algebra/ringsimp.ML	Wed Jul 19 19:25:58 2006 +0200
     3.3 @@ -1,68 +1,95 @@
     3.4  (*
     3.5 -  Title:     Normalisation method for locale cring
     3.6 +  Title:     Normalisation method for locales ring and cring
     3.7    Id:        $Id$
     3.8    Author:    Clemens Ballarin
     3.9    Copyright: TU Muenchen
    3.10  *)
    3.11  
    3.12 -(*** Term order for commutative rings ***)
    3.13 +signature ALGEBRA =
    3.14 +sig
    3.15 +  val print_structures: Context.generic -> unit
    3.16 +  val setup: Theory.theory -> Theory.theory
    3.17 +end;
    3.18 +
    3.19 +structure Algebra: ALGEBRA =
    3.20 +struct
    3.21 +
    3.22 +
    3.23 +(** Theory and context data **)
    3.24 +
    3.25 +fun struct_eq ((s1, ts1), (s2, ts2)) =
    3.26 +  (s1 = s2) andalso equal_lists (op aconv) (ts1, ts2);
    3.27  
    3.28 -fun ring_ord (Const (a, _)) =
    3.29 -    find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "CRing.a_inv",
    3.30 -      "CRing.minus", "Group.monoid.one", "Group.monoid.mult"]
    3.31 -  | ring_ord _ = ~1;
    3.32 +structure AlgebraData = GenericDataFun
    3.33 +(struct
    3.34 +  val name = "Algebra/algebra";
    3.35 +  type T = ((string * term list) * thm list) list;
    3.36 +    (* Algebraic structures:
    3.37 +       identifier of the structure, list of operations and simp rules,
    3.38 +       identifier and operations identify the structure uniquely. *)
    3.39 +  val empty = [];
    3.40 +  val extend = I;
    3.41 +  fun merge _ (structs1, structs2) = gen_merge_lists
    3.42 +    (fn ((s1, _), (s2, _)) => struct_eq (s1, s2)) structs1 structs2;
    3.43 +  fun print generic structs =
    3.44 +    let
    3.45 +      val ctxt = Context.proof_of generic;
    3.46 +      val pretty_term = Pretty.quote o ProofContext.pretty_term ctxt;
    3.47 +      fun pretty_struct ((s, ts), _) = Pretty.block
    3.48 +        [Pretty.str s, Pretty.str ":", Pretty.brk 1,
    3.49 +         Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
    3.50 +    in
    3.51 +      Pretty.big_list "Algebraic structures:" (map pretty_struct structs) |>
    3.52 +        Pretty.writeln
    3.53 +    end
    3.54 +end);
    3.55  
    3.56 -fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS);
    3.57 +val print_structures = AlgebraData.print;
    3.58  
    3.59 -val cring_ss = HOL_ss settermless termless_ring;
    3.60 +
    3.61 +(** Method **)
    3.62  
    3.63 -fun cring_normalise ctxt = let
    3.64 -    fun filter p t = (case HOLogic.dest_Trueprop t of
    3.65 -        Const (p', _) $ Free (s, _) => if p = p' then [s] else []
    3.66 -      | _ => [])
    3.67 -      handle TERM _ => [];
    3.68 -    fun filter21 p t = (case HOLogic.dest_Trueprop t of
    3.69 -        Const (p', _) $ Free (s, _) $ _ => if p = p' then [s] else []
    3.70 -      | _ => [])
    3.71 -      handle TERM _ => [];
    3.72 -    fun filter22 p t = (case HOLogic.dest_Trueprop t of
    3.73 -        Const (p', _) $ _ $ Free (s, _) => if p = p' then [s] else []
    3.74 -      | _ => [])
    3.75 -      handle TERM _ => [];
    3.76 -    fun filter31 p t = (case HOLogic.dest_Trueprop t of
    3.77 -        Const (p', _) $ Free (s, _) $ _ $ _ => if p = p' then [s] else []
    3.78 -      | _ => [])
    3.79 -      handle TERM _ => [];
    3.80 -    fun filter32 p t = (case HOLogic.dest_Trueprop t of
    3.81 -        Const (p', _) $ _ $ Free (s, _) $ _ => if p = p' then [s] else []
    3.82 -      | _ => [])
    3.83 -      handle TERM _ => [];
    3.84 +fun struct_tac ((s, ts), simps) =
    3.85 +  let
    3.86 +    val ops = map (fst o Term.strip_comb) ts;
    3.87 +    fun ord (Const (a, _)) = find_index (fn (Const (b, _)) => a=b | _ => false) ops
    3.88 +      | ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops;
    3.89 +    fun less (a, b) = (Term.term_lpo ord (a, b) = LESS);
    3.90 +  in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end;
    3.91 +
    3.92 +fun algebra_tac ctxt =
    3.93 +  let val _ = print_structures (Context.Proof ctxt)
    3.94 +  in EVERY' (map (fn s => TRY o struct_tac s) (AlgebraData.get (Context.Proof ctxt))) end;
    3.95 +
    3.96 +val method =
    3.97 +  Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' HEADGOAL (algebra_tac ctxt))
    3.98 +
    3.99 +
   3.100 +(** Attribute **)
   3.101  
   3.102 -    val prems = ProofContext.prems_of ctxt;
   3.103 -    val non_comm_rings = List.concat (map (filter "CRing.ring" o #prop o rep_thm) prems);
   3.104 -    val comm_rings = List.concat (map (filter "CRing.cring" o #prop o rep_thm) prems) @
   3.105 -        List.concat (map (filter "CRing.domain" o #prop o rep_thm) prems) @
   3.106 -        List.concat (map (filter21 "Module.module" o #prop o rep_thm) prems) @
   3.107 -        List.concat (map (filter21 "Module.algebra" o #prop o rep_thm) prems) @
   3.108 -        List.concat (map (filter22 "Module.algebra" o #prop o rep_thm) prems) @
   3.109 -        List.concat (map (filter "UnivPoly.UP_cring" o #prop o rep_thm) prems) @
   3.110 -        List.concat (map (filter "UnivPoly.UP_domain" o #prop o rep_thm) prems) @
   3.111 -        List.concat (map (filter31 "CRing.ring_hom_cring" o #prop o rep_thm) prems) @
   3.112 -        List.concat (map (filter32 "CRing.ring_hom_cring" o #prop o rep_thm) prems);
   3.113 -    val _ = tracing
   3.114 -      ("Non-commutative rings in proof context: " ^ commas non_comm_rings ^
   3.115 -       "\nCommutative rings in proof context: " ^ commas comm_rings);
   3.116 -    val simps =
   3.117 -      List.concat (map (fn s => ProofContext.get_thms ctxt (Name (s ^ ".ring_simprules")))
   3.118 -        non_comm_rings) @
   3.119 -      List.concat (map (fn s => ProofContext.get_thms ctxt (Name (s ^ ".cring_simprules")))
   3.120 -        comm_rings);
   3.121 -  in Method.SIMPLE_METHOD' HEADGOAL (asm_full_simp_tac (cring_ss addsimps simps))
   3.122 -  end;
   3.123 +fun add_struct_thm s =
   3.124 +  Thm.declaration_attribute (fn thm => fn ctxt =>
   3.125 +    AlgebraData.map (fn structs => 
   3.126 +      if AList.defined struct_eq structs s
   3.127 +      then AList.map_entry struct_eq s (fn thms => thm :: thms) structs
   3.128 +      else (s, [thm])::structs) ctxt);
   3.129 +fun del_struct s =
   3.130 +  Thm.declaration_attribute (fn _ => fn ctxt =>
   3.131 +    AlgebraData.map (AList.delete struct_eq s) ctxt);
   3.132  
   3.133 -(*
   3.134 -val ring_ss = HOL_basic_ss settermless termless_ring addsimps
   3.135 -  [a_assoc, l_zero, l_neg, a_comm, m_assoc, l_one, l_distr, m_comm, minus_def,
   3.136 -   r_zero, r_neg, r_neg2, r_neg1, minus_add, minus_minus, minus0,
   3.137 -   a_lcomm, m_lcomm, (*r_one,*) r_distr, l_null, r_null, l_minus, r_minus];
   3.138 -*)
   3.139 +val attribute = Attrib.syntax
   3.140 +     (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||
   3.141 +        Scan.succeed true) -- Scan.lift Args.name -- 
   3.142 +      Scan.repeat Args.term
   3.143 +      >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts)));
   3.144 +
   3.145 +
   3.146 +(** Setup **)
   3.147 +
   3.148 +val setup =
   3.149 +  AlgebraData.init #>
   3.150 +  Method.add_methods [("algebra", method, "normalisation of algebraic structure")] #>
   3.151 +  Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")];
   3.152 +
   3.153 +
   3.154 +end;  (* struct *)