Added instantiation of algebra method to fields
authorchaieb
Mon Jun 11 16:23:17 2007 +0200 (2007-06-11)
changeset 233271654013ec97c
parent 23326 71e99443e17d
child 23328 405a28da4bf3
Added instantiation of algebra method to fields
src/HOL/Groebner_Basis.thy
src/HOL/NatSimprocs.thy
     1.1 --- a/src/HOL/Groebner_Basis.thy	Mon Jun 11 16:21:03 2007 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Mon Jun 11 16:23:17 2007 +0200
     1.3 @@ -260,6 +260,22 @@
     1.4  *} "Semiring_normalizer"
     1.5  
     1.6  
     1.7 +locale gb_field = gb_ring +
     1.8 +  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
     1.9 +    and inverse:: "'a \<Rightarrow> 'a"
    1.10 +  assumes divide: "divide x y = mul x (inverse y)"
    1.11 +     and inverse: "inverse x = divide r1 x"
    1.12 +begin
    1.13 +
    1.14 +lemma "axioms" [normalizer
    1.15 +  semiring ops: semiring_ops
    1.16 +  semiring rules: semiring_rules
    1.17 +  ring ops: ring_ops
    1.18 +  ring rules: ring_rules]:
    1.19 +  "gb_field add mul pwr r0 r1 sub neg divide inverse" .
    1.20 +
    1.21 +end
    1.22 +
    1.23  subsection {* Groebner Bases *}
    1.24  
    1.25  locale semiringb = gb_semiring +
    1.26 @@ -384,6 +400,21 @@
    1.27      conv = fn phi => numeral_conv}
    1.28  *}
    1.29  
    1.30 +locale fieldgb = ringb + gb_field
    1.31 +begin
    1.32 +
    1.33 +declare "axioms" [normalizer del]
    1.34 +
    1.35 +lemma "axioms" [normalizer
    1.36 +  semiring ops: semiring_ops
    1.37 +  semiring rules: semiring_rules
    1.38 +  ring ops: ring_ops
    1.39 +  ring rules: ring_rules
    1.40 +  idom rules: noteq_reduce add_scale_eq_noteq]:
    1.41 +  "fieldgb add mul pwr r0 r1 sub neg divide inverse" by unfold_locales
    1.42 +end
    1.43 +
    1.44 +
    1.45  
    1.46  lemmas bool_simps = simp_thms(1-34)
    1.47  lemma dnf:
    1.48 @@ -414,4 +445,6 @@
    1.49    Method.ctxt_args (Method.SIMPLE_METHOD' o algebra_tac)
    1.50  *} ""
    1.51  
    1.52 +
    1.53 +
    1.54  end
     2.1 --- a/src/HOL/NatSimprocs.thy	Mon Jun 11 16:21:03 2007 +0200
     2.2 +++ b/src/HOL/NatSimprocs.thy	Mon Jun 11 16:23:17 2007 +0200
     2.3 @@ -392,4 +392,209 @@
     2.4  val minus1_divide = @{thm minus1_divide};
     2.5  *}
     2.6  
     2.7 +section{* Installing Groebner Bases for Fields *}
     2.8 +
     2.9 +
    2.10 +interpretation class_fieldgb: 
    2.11 +  fieldgb["op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse"] apply (unfold_locales) by (simp_all add: divide_inverse)
    2.12 +
    2.13 +lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
    2.14 +lemma divide_Numeral0: "(x::'a::{field,number_ring, division_by_zero}) / Numeral0 = 0" 
    2.15 +  by simp
    2.16 +lemma mult_frac_frac: "((x::'a::{field,division_by_zero}) / y) * (z / w) = (x*z) / (y*w)" 
    2.17 +  by simp
    2.18 +lemma mult_frac_num: "((x::'a::{field, division_by_zero}) / y) * z  = (x*z) / y" 
    2.19 +  by simp
    2.20 +lemma mult_num_frac: "((x::'a::{field, division_by_zero}) / y) * z  = (x*z) / y" 
    2.21 +  by simp
    2.22 +
    2.23 +lemma Numeral1_eq1_nat: "(1::nat) = Numeral1" by simp
    2.24 +
    2.25 +lemma add_frac_num: "y\<noteq> 0 \<Longrightarrow> (x::'a::{field, division_by_zero}) / y + z = (x + z*y) / y" 
    2.26 +  by (simp add: add_divide_distrib)
    2.27 +lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y" 
    2.28 +  by (simp add: add_divide_distrib)
    2.29 +
    2.30 +declaration{*
    2.31 +let
    2.32 + val zr = @{cpat "0"}
    2.33 + val zT = ctyp_of_term zr
    2.34 + val geq = @{cpat "op ="}
    2.35 + val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd
    2.36 + val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"} 
    2.37 + val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
    2.38 + val add_num_frac = mk_meta_eq @{thm "add_num_frac"}
    2.39 +
    2.40 + fun prove_nz ss T t = 
    2.41 +    let 
    2.42 +      val z = instantiate_cterm ([(zT,T)],[]) zr 
    2.43 +      val eq = instantiate_cterm ([(eqT,T)],[]) geq
    2.44 +      val th = Simplifier.rewrite (ss addsimps simp_thms) 
    2.45 +           (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"} 
    2.46 +                  (Thm.capply (Thm.capply eq t) z)))
    2.47 +    in equal_elim (symmetric th) TrueI
    2.48 +    end
    2.49 +
    2.50 + fun proc phi ss ct = 
    2.51 +  let 
    2.52 +    val ((x,y),(w,z)) = 
    2.53 +         (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct
    2.54 +    val _ = map (HOLogic.dest_number o term_of) [x,y,z,w] 
    2.55 +    val T = ctyp_of_term x
    2.56 +    val [y_nz, z_nz] = map (prove_nz ss T) [y, z]
    2.57 +    val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
    2.58 +  in SOME (implies_elim (implies_elim th y_nz) z_nz)
    2.59 +  end
    2.60 +  handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
    2.61 +
    2.62 + fun proc2 phi ss ct = 
    2.63 +  let 
    2.64 +    val (l,r) = Thm.dest_binop ct
    2.65 +    val T = ctyp_of_term l
    2.66 +  in (case (term_of l, term_of r) of
    2.67 +      (Const(@{const_name "HOL.divide"},_)$_$_, _) => 
    2.68 +        let val (x,y) = Thm.dest_binop l val z = r
    2.69 +            val _ = map (HOLogic.dest_number o term_of) [x,y,z]
    2.70 +            val ynz = prove_nz ss T y
    2.71 +        in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
    2.72 +        end
    2.73 +     | (_, Const (@{const_name "HOL.divide"},_)$_$_) => 
    2.74 +        let val (x,y) = Thm.dest_binop r val z = l
    2.75 +            val _ = map (HOLogic.dest_number o term_of) [x,y,z]
    2.76 +            val ynz = prove_nz ss T y
    2.77 +        in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
    2.78 +        end
    2.79 +     | _ => NONE)
    2.80 +  end
    2.81 +  handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
    2.82 +
    2.83 + fun is_number (Const(@{const_name "HOL.divide"},_)$a$b) = is_number a andalso is_number b
    2.84 +   | is_number t = can HOLogic.dest_number t
    2.85 +
    2.86 + val is_number = is_number o term_of
    2.87 +
    2.88 + fun proc3 phi ss ct =
    2.89 +  (case term_of ct of
    2.90 +    Const(@{const_name "Orderings.less"},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ => 
    2.91 +      let 
    2.92 +        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    2.93 +        val _ = map is_number [a,b,c]
    2.94 +        val T = ctyp_of_term c
    2.95 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
    2.96 +      in SOME (mk_meta_eq th) end
    2.97 +  | Const(@{const_name "Orderings.less_eq"},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ => 
    2.98 +      let 
    2.99 +        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   2.100 +        val _ = map is_number [a,b,c]
   2.101 +        val T = ctyp_of_term c
   2.102 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
   2.103 +      in SOME (mk_meta_eq th) end
   2.104 +  | Const("op =",_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ => 
   2.105 +      let 
   2.106 +        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   2.107 +        val _ = map is_number [a,b,c]
   2.108 +        val T = ctyp_of_term c
   2.109 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
   2.110 +      in SOME (mk_meta_eq th) end
   2.111 +  | Const(@{const_name "Orderings.less"},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) => 
   2.112 +    let 
   2.113 +      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   2.114 +        val _ = map is_number [a,b,c]
   2.115 +        val T = ctyp_of_term c
   2.116 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
   2.117 +      in SOME (mk_meta_eq th) end
   2.118 +  | Const(@{const_name "Orderings.less_eq"},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) => 
   2.119 +    let 
   2.120 +      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   2.121 +        val _ = map is_number [a,b,c]
   2.122 +        val T = ctyp_of_term c
   2.123 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
   2.124 +      in SOME (mk_meta_eq th) end
   2.125 +  | Const("op =",_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) => 
   2.126 +    let 
   2.127 +      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   2.128 +        val _ = map is_number [a,b,c]
   2.129 +        val T = ctyp_of_term c
   2.130 +        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"}
   2.131 +      in SOME (mk_meta_eq th) end
   2.132 +  | _ => NONE)
   2.133 +  handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE
   2.134 +
   2.135 +val add_frac_frac_simproc = 
   2.136 +       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}], 
   2.137 +                     name = "add_frac_frac_simproc",
   2.138 +                     proc = proc, identifier = []}
   2.139 +
   2.140 +val add_frac_num_simproc = 
   2.141 +       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}], 
   2.142 +                     name = "add_frac_num_simproc",
   2.143 +                     proc = proc2, identifier = []}
   2.144 +
   2.145 +val ord_frac_simproc = 
   2.146 +  make_simproc 
   2.147 +    {lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"}, 
   2.148 +             @{cpat "(?a::(?'a::{field, ord}))/?b \<le> ?c"}, 
   2.149 +             @{cpat "?c < (?a::(?'a::{field, ord}))/?b"}, 
   2.150 +             @{cpat "?c \<le> (?a::(?'a::{field, ord}))/?b"},
   2.151 +             @{cpat "?c = ((?a::(?'a::{field, ord}))/?b)"},
   2.152 +             @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}],
   2.153 +             name = "ord_frac_simproc", proc = proc3, identifier = []}
   2.154 +
   2.155 +val nat_arith = map thm ["add_nat_number_of", "diff_nat_number_of", 
   2.156 +               "mult_nat_number_of", "eq_nat_number_of", "less_nat_number_of"]
   2.157 +
   2.158 +val comp_arith = (map thm ["Let_def", "if_False", "if_True", "add_0", 
   2.159 +                 "add_Suc", "add_number_of_left", "mult_number_of_left", 
   2.160 +                 "Suc_eq_add_numeral_1"])@
   2.161 +                 (map (fn s => thm s RS sym) ["numeral_1_eq_1", "numeral_0_eq_0"])
   2.162 +                 @ arith_simps@ nat_arith @ rel_simps 
   2.163 +val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, 
   2.164 +           @{thm "divide_Numeral1"}, 
   2.165 +           @{thm "Ring_and_Field.divide_zero"}, @{thm "divide_Numeral0"},
   2.166 +           @{thm "divide_divide_eq_left"}, @{thm "mult_frac_frac"},
   2.167 +           @{thm "mult_num_frac"}, @{thm "mult_frac_num"}, 
   2.168 +           @{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"}, 
   2.169 +           @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
   2.170 +           @{thm "diff_def"}, @{thm "minus_divide_left"}, 
   2.171 +           @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym]
   2.172 +
   2.173 +val ss = HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"} 
   2.174 +                 addsimps ths addsimps comp_arith addsimps simp_thms
   2.175 +                 addsimprocs field_cancel_numeral_factors
   2.176 +                 addsimprocs [add_frac_frac_simproc, add_frac_num_simproc,
   2.177 +                              ord_frac_simproc]
   2.178 +                 addcongs [@{thm "if_weak_cong"}]
   2.179 +
   2.180 +val comp_conv = Simplifier.rewrite ss
   2.181 +
   2.182 +fun numeral_is_const ct = 
   2.183 +  case term_of ct of 
   2.184 +   Const (@{const_name "HOL.divide"},_) $ a $ b => 
   2.185 +     can HOLogic.dest_number a andalso can HOLogic.dest_number b
   2.186 + | t => can HOLogic.dest_number t
   2.187 +
   2.188 +fun dest_const ct = case term_of ct of
   2.189 +   Const (@{const_name "HOL.divide"},_) $ a $ b=>
   2.190 +    Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
   2.191 + | t => Rat.rat_of_int (snd (HOLogic.dest_number t))
   2.192 +
   2.193 +fun mk_const phi cT x = 
   2.194 + let val (a, b) = Rat.quotient_of_rat x
   2.195 + in if b = 1 then Normalizer.mk_cnumber cT a
   2.196 +    else Thm.capply 
   2.197 +         (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"}) 
   2.198 +                     (Normalizer.mk_cnumber cT a))
   2.199 +         (Normalizer.mk_cnumber cT b)
   2.200 +  end
   2.201 +
   2.202 +in 
   2.203 + NormalizerData.funs @{thm class_fieldgb.axioms}
   2.204 +   {is_const = K numeral_is_const,
   2.205 +    dest_const = K dest_const,
   2.206 +    mk_const = mk_const,
   2.207 +    conv = K comp_conv}
   2.208  end
   2.209 +
   2.210 +*}
   2.211 +
   2.212 +end