moved constants inverse and divide to Ring.thy
authorhaftmann
Wed Feb 10 08:49:26 2010 +0100 (2010-02-10)
changeset 35084e25eedfc15ce
parent 35083 3246e66b0874
child 35085 22bdb7f86a1e
moved constants inverse and divide to Ring.thy
NEWS
src/HOL/Algebras.thy
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Fields.thy
src/HOL/Groebner_Basis.thy
src/HOL/Import/HOL/realax.imp
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/numeral_simprocs.ML
src/HOL/ex/SVC_Oracle.thy
src/HOL/ex/svc_funcs.ML
     1.1 --- a/NEWS	Wed Feb 10 08:49:26 2010 +0100
     1.2 +++ b/NEWS	Wed Feb 10 08:49:26 2010 +0100
     1.3 @@ -20,6 +20,15 @@
     1.4  consistent names suitable for name prefixes within the HOL theories.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Some generic constants have been put to appropriate theories:
     1.8 +
     1.9 +    inverse, divide: Rings
    1.10 +
    1.11 +INCOMPATIBILITY.
    1.12 +
    1.13 +* Class division ring also requires proof of fact divide_inverse.  However instantiation
    1.14 +of parameter divide has also been required previously.  INCOMPATIBILITY.
    1.15 +
    1.16  * More consistent naming of type classes involving orderings (and lattices):
    1.17  
    1.18      lower_semilattice                   ~> semilattice_inf
    1.19 @@ -76,7 +85,7 @@
    1.20  
    1.21  * New theory Algebras contains generic algebraic structures and
    1.22  generic algebraic operations.  INCOMPATIBILTY: constants zero, one,
    1.23 -plus, minus, uminus, times, inverse, divide, abs, sgn, less_eq and
    1.24 +plus, minus, uminus, times, abs, sgn, less_eq and
    1.25  less have been moved from HOL.thy to Algebras.thy.
    1.26  
    1.27  * HOLogic.strip_psplit: types are returned in syntactic order, similar
     2.1 --- a/src/HOL/Algebras.thy	Wed Feb 10 08:49:26 2010 +0100
     2.2 +++ b/src/HOL/Algebras.thy	Wed Feb 10 08:49:26 2010 +0100
     2.3 @@ -103,10 +103,6 @@
     2.4  class times =
     2.5    fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
     2.6  
     2.7 -class inverse =
     2.8 -  fixes inverse :: "'a \<Rightarrow> 'a"
     2.9 -    and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
    2.10 -
    2.11  class abs =
    2.12    fixes abs :: "'a \<Rightarrow> 'a"
    2.13  begin
     3.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Feb 10 08:49:26 2010 +0100
     3.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Feb 10 08:49:26 2010 +0100
     3.3 @@ -655,7 +655,7 @@
     3.4      if h aconvc y then false else if h aconvc x then true else earlier t x y;
     3.5  
     3.6  fun dest_frac ct = case term_of ct of
     3.7 -   Const (@{const_name Algebras.divide},_) $ a $ b=>
     3.8 +   Const (@{const_name Rings.divide},_) $ a $ b=>
     3.9      Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
    3.10   | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
    3.11   | t => Rat.rat_of_int (snd (HOLogic.dest_number t))
     4.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 10 08:49:26 2010 +0100
     4.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 10 08:49:26 2010 +0100
     4.3 @@ -2946,7 +2946,7 @@
     4.4  fun num rT x = HOLogic.mk_number rT x;
     4.5  fun rrelT rT = [rT,rT] ---> rT;
     4.6  fun rrT rT = [rT, rT] ---> bT;
     4.7 -fun divt rT = Const(@{const_name Algebras.divide},rrelT rT);
     4.8 +fun divt rT = Const(@{const_name Rings.divide},rrelT rT);
     4.9  fun timest rT = Const(@{const_name Algebras.times},rrelT rT);
    4.10  fun plust rT = Const(@{const_name Algebras.plus},rrelT rT);
    4.11  fun minust rT = Const(@{const_name Algebras.minus},rrelT rT);
    4.12 @@ -2974,7 +2974,7 @@
    4.13   | Const(@{const_name Algebras.minus},_)$a$b => @{code poly.Sub} (num_of_term m a, num_of_term m b)
    4.14   | Const(@{const_name Algebras.times},_)$a$b => @{code poly.Mul} (num_of_term m a, num_of_term m b)
    4.15   | Const(@{const_name Power.power},_)$a$n => @{code poly.Pw} (num_of_term m a, dest_nat n)
    4.16 - | Const(@{const_name Algebras.divide},_)$a$b => @{code poly.C} (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    4.17 + | Const(@{const_name Rings.divide},_)$a$b => @{code poly.C} (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    4.18   | _ => (@{code poly.C} (HOLogic.dest_number t |> snd,1) 
    4.19           handle TERM _ => @{code poly.Bound} (AList.lookup (op aconv) m t |> the));
    4.20  
     5.1 --- a/src/HOL/Fields.thy	Wed Feb 10 08:49:26 2010 +0100
     5.2 +++ b/src/HOL/Fields.thy	Wed Feb 10 08:49:26 2010 +0100
     5.3 @@ -14,8 +14,8 @@
     5.4  begin
     5.5  
     5.6  class field = comm_ring_1 + inverse +
     5.7 -  assumes field_inverse:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
     5.8 -  assumes divide_inverse: "a / b = a * inverse b"
     5.9 +  assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
    5.10 +  assumes field_divide_inverse: "a / b = a * inverse b"
    5.11  begin
    5.12  
    5.13  subclass division_ring
    5.14 @@ -24,6 +24,9 @@
    5.15    assume "a \<noteq> 0"
    5.16    thus "inverse a * a = 1" by (rule field_inverse)
    5.17    thus "a * inverse a = 1" by (simp only: mult_commute)
    5.18 +next
    5.19 +  fix a b :: 'a
    5.20 +  show "a / b = a * inverse b" by (rule field_divide_inverse)
    5.21  qed
    5.22  
    5.23  subclass idom ..
     6.1 --- a/src/HOL/Groebner_Basis.thy	Wed Feb 10 08:49:26 2010 +0100
     6.2 +++ b/src/HOL/Groebner_Basis.thy	Wed Feb 10 08:49:26 2010 +0100
     6.3 @@ -489,7 +489,13 @@
     6.4    by (simp add: add_divide_distrib)
     6.5  lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y"
     6.6    by (simp add: add_divide_distrib)
     6.7 -ML{* let open Conv in fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute}))))   (@{thm divide_inverse} RS sym)end*}
     6.8 +
     6.9 +ML {*
    6.10 +let open Conv
    6.11 +in fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute})))) (@{thm field_divide_inverse} RS sym)
    6.12 +end
    6.13 +*}
    6.14 +
    6.15  ML{* 
    6.16  local
    6.17   val zr = @{cpat "0"}
    6.18 @@ -527,13 +533,13 @@
    6.19      val (l,r) = Thm.dest_binop ct
    6.20      val T = ctyp_of_term l
    6.21    in (case (term_of l, term_of r) of
    6.22 -      (Const(@{const_name Algebras.divide},_)$_$_, _) =>
    6.23 +      (Const(@{const_name Rings.divide},_)$_$_, _) =>
    6.24          let val (x,y) = Thm.dest_binop l val z = r
    6.25              val _ = map (HOLogic.dest_number o term_of) [x,y,z]
    6.26              val ynz = prove_nz ss T y
    6.27          in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
    6.28          end
    6.29 -     | (_, Const (@{const_name Algebras.divide},_)$_$_) =>
    6.30 +     | (_, Const (@{const_name Rings.divide},_)$_$_) =>
    6.31          let val (x,y) = Thm.dest_binop r val z = l
    6.32              val _ = map (HOLogic.dest_number o term_of) [x,y,z]
    6.33              val ynz = prove_nz ss T y
    6.34 @@ -543,49 +549,49 @@
    6.35    end
    6.36    handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
    6.37  
    6.38 - fun is_number (Const(@{const_name Algebras.divide},_)$a$b) = is_number a andalso is_number b
    6.39 + fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b
    6.40     | is_number t = can HOLogic.dest_number t
    6.41  
    6.42   val is_number = is_number o term_of
    6.43  
    6.44   fun proc3 phi ss ct =
    6.45    (case term_of ct of
    6.46 -    Const(@{const_name Algebras.less},_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ =>
    6.47 +    Const(@{const_name Algebras.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
    6.48        let
    6.49          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    6.50          val _ = map is_number [a,b,c]
    6.51          val T = ctyp_of_term c
    6.52          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
    6.53        in SOME (mk_meta_eq th) end
    6.54 -  | Const(@{const_name Algebras.less_eq},_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ =>
    6.55 +  | Const(@{const_name Algebras.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
    6.56        let
    6.57          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    6.58          val _ = map is_number [a,b,c]
    6.59          val T = ctyp_of_term c
    6.60          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
    6.61        in SOME (mk_meta_eq th) end
    6.62 -  | Const("op =",_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ =>
    6.63 +  | Const("op =",_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
    6.64        let
    6.65          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    6.66          val _ = map is_number [a,b,c]
    6.67          val T = ctyp_of_term c
    6.68          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
    6.69        in SOME (mk_meta_eq th) end
    6.70 -  | Const(@{const_name Algebras.less},_)$_$(Const(@{const_name Algebras.divide},_)$_$_) =>
    6.71 +  | Const(@{const_name Algebras.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
    6.72      let
    6.73        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
    6.74          val _ = map is_number [a,b,c]
    6.75          val T = ctyp_of_term c
    6.76          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
    6.77        in SOME (mk_meta_eq th) end
    6.78 -  | Const(@{const_name Algebras.less_eq},_)$_$(Const(@{const_name Algebras.divide},_)$_$_) =>
    6.79 +  | Const(@{const_name Algebras.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
    6.80      let
    6.81        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
    6.82          val _ = map is_number [a,b,c]
    6.83          val T = ctyp_of_term c
    6.84          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
    6.85        in SOME (mk_meta_eq th) end
    6.86 -  | Const("op =",_)$_$(Const(@{const_name Algebras.divide},_)$_$_) =>
    6.87 +  | Const("op =",_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
    6.88      let
    6.89        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
    6.90          val _ = map is_number [a,b,c]
    6.91 @@ -628,9 +634,9 @@
    6.92             @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
    6.93             @{thm "diff_def"}, @{thm "minus_divide_left"},
    6.94             @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym,
    6.95 -           @{thm divide_inverse} RS sym, @{thm inverse_divide}, 
    6.96 +           @{thm field_divide_inverse} RS sym, @{thm inverse_divide}, 
    6.97             fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute}))))   
    6.98 -           (@{thm divide_inverse} RS sym)]
    6.99 +           (@{thm field_divide_inverse} RS sym)]
   6.100  
   6.101  val comp_conv = (Simplifier.rewrite
   6.102  (HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
   6.103 @@ -645,15 +651,15 @@
   6.104  
   6.105  fun numeral_is_const ct =
   6.106    case term_of ct of
   6.107 -   Const (@{const_name Algebras.divide},_) $ a $ b =>
   6.108 +   Const (@{const_name Rings.divide},_) $ a $ b =>
   6.109       can HOLogic.dest_number a andalso can HOLogic.dest_number b
   6.110 - | Const (@{const_name Algebras.inverse},_)$t => can HOLogic.dest_number t
   6.111 + | Const (@{const_name Rings.inverse},_)$t => can HOLogic.dest_number t
   6.112   | t => can HOLogic.dest_number t
   6.113  
   6.114  fun dest_const ct = ((case term_of ct of
   6.115 -   Const (@{const_name Algebras.divide},_) $ a $ b=>
   6.116 +   Const (@{const_name Rings.divide},_) $ a $ b=>
   6.117      Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
   6.118 - | Const (@{const_name Algebras.inverse},_)$t => 
   6.119 + | Const (@{const_name Rings.inverse},_)$t => 
   6.120                 Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
   6.121   | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) 
   6.122     handle TERM _ => error "ring_dest_const")
     7.1 --- a/src/HOL/Import/HOL/realax.imp	Wed Feb 10 08:49:26 2010 +0100
     7.2 +++ b/src/HOL/Import/HOL/realax.imp	Wed Feb 10 08:49:26 2010 +0100
     7.3 @@ -33,7 +33,7 @@
     7.4    "real_add" > "Algebras.plus_class.plus" :: "real => real => real"
     7.5    "real_1" > "Algebras.one_class.one" :: "real"
     7.6    "real_0" > "Algebras.zero_class.zero" :: "real"
     7.7 -  "inv" > "Algebras.divide_class.inverse" :: "real => real"
     7.8 +  "inv" > "Ring.inverse" :: "real => real"
     7.9    "hreal_of_treal" > "HOL4Real.realax.hreal_of_treal"
    7.10  
    7.11  thm_maps
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Feb 10 08:49:26 2010 +0100
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Feb 10 08:49:26 2010 +0100
     8.3 @@ -78,7 +78,7 @@
     8.4      Const (atom_name "" T j, T)
     8.5  
     8.6  (* term -> real *)
     8.7 -fun extract_real_number (Const (@{const_name Algebras.divide}, _) $ t1 $ t2) =
     8.8 +fun extract_real_number (Const (@{const_name Rings.divide}, _) $ t1 $ t2) =
     8.9      real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
    8.10    | extract_real_number t = real (snd (HOLogic.dest_number t))
    8.11  (* term * term -> order *)
    8.12 @@ -446,7 +446,7 @@
    8.13                             0 => mk_num 0
    8.14                           | n1 => case HOLogic.dest_number t2 |> snd of
    8.15                                     1 => mk_num n1
    8.16 -                                 | n2 => Const (@{const_name Algebras.divide},
    8.17 +                                 | n2 => Const (@{const_name Rings.divide},
    8.18                                                  num_T --> num_T --> num_T)
    8.19                                           $ mk_num n1 $ mk_num n2)
    8.20                        | _ => raise TERM ("Nitpick_Model.reconstruct_term.\
     9.1 --- a/src/HOL/Tools/lin_arith.ML	Wed Feb 10 08:49:26 2010 +0100
     9.2 +++ b/src/HOL/Tools/lin_arith.ML	Wed Feb 10 08:49:26 2010 +0100
     9.3 @@ -150,7 +150,7 @@
     9.4                (SOME t', m'') => (SOME (mC $ s' $ t'), m'')
     9.5              | (NONE,    m'') => (SOME s', m''))
     9.6          | (NONE,    m') => demult (t, m')))
     9.7 -    | demult ((mC as Const (@{const_name Algebras.divide}, _)) $ s $ t, m) =
     9.8 +    | demult ((mC as Const (@{const_name Rings.divide}, _)) $ s $ t, m) =
     9.9        (* FIXME: Shouldn't we simplify nested quotients, e.g. '(s/t)/u' could
    9.10           become 's/(t*u)', and '(s*t)/u' could become 's*(t/u)' ?   Note that
    9.11           if we choose to do so here, the simpset used by arith must be able to
    9.12 @@ -212,7 +212,7 @@
    9.13          (case demult inj_consts (all, m) of
    9.14             (NONE,   m') => (p, Rat.add i m')
    9.15           | (SOME u, m') => add_atom u m' pi)
    9.16 -    | poly (all as Const (@{const_name Algebras.divide}, _) $ _ $ _, m, pi as (p, i)) =
    9.17 +    | poly (all as Const (@{const_name Rings.divide}, _) $ _ $ _, m, pi as (p, i)) =
    9.18          (case demult inj_consts (all, m) of
    9.19             (NONE,   m') => (p, Rat.add i m')
    9.20           | (SOME u, m') => add_atom u m' pi)
    10.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Wed Feb 10 08:49:26 2010 +0100
    10.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Wed Feb 10 08:49:26 2010 +0100
    10.3 @@ -96,7 +96,7 @@
    10.4    Fractions are reduced later by the cancel_numeral_factor simproc.*)
    10.5  fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
    10.6  
    10.7 -val mk_divide = HOLogic.mk_binop @{const_name Algebras.divide};
    10.8 +val mk_divide = HOLogic.mk_binop @{const_name Rings.divide};
    10.9  
   10.10  (*Build term (p / q) * t*)
   10.11  fun mk_fcoeff ((p, q), t) =
   10.12 @@ -105,7 +105,7 @@
   10.13  
   10.14  (*Express t as a product of a fraction with other sorted terms*)
   10.15  fun dest_fcoeff sign (Const (@{const_name Algebras.uminus}, _) $ t) = dest_fcoeff (~sign) t
   10.16 -  | dest_fcoeff sign (Const (@{const_name Algebras.divide}, _) $ t $ u) =
   10.17 +  | dest_fcoeff sign (Const (@{const_name Rings.divide}, _) $ t $ u) =
   10.18      let val (p, t') = dest_coeff sign t
   10.19          val (q, u') = dest_coeff 1 u
   10.20      in (mk_frac (p, q), mk_divide (t', u')) end
   10.21 @@ -391,8 +391,8 @@
   10.22  structure DivideCancelNumeralFactor = CancelNumeralFactorFun
   10.23   (open CancelNumeralFactorCommon
   10.24    val prove_conv = Arith_Data.prove_conv
   10.25 -  val mk_bal   = HOLogic.mk_binop @{const_name Algebras.divide}
   10.26 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.divide} Term.dummyT
   10.27 +  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
   10.28 +  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} Term.dummyT
   10.29    val cancel = @{thm mult_divide_mult_cancel_left} RS trans
   10.30    val neg_exchanges = false
   10.31  )
   10.32 @@ -570,8 +570,8 @@
   10.33  structure DivideCancelFactor = ExtractCommonTermFun
   10.34   (open CancelFactorCommon
   10.35    val prove_conv = Arith_Data.prove_conv
   10.36 -  val mk_bal   = HOLogic.mk_binop @{const_name Algebras.divide}
   10.37 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.divide} Term.dummyT
   10.38 +  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
   10.39 +  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} Term.dummyT
   10.40    fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
   10.41  );
   10.42  
    11.1 --- a/src/HOL/ex/SVC_Oracle.thy	Wed Feb 10 08:49:26 2010 +0100
    11.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Wed Feb 10 08:49:26 2010 +0100
    11.3 @@ -65,7 +65,7 @@
    11.4      (*abstraction of a real/rational expression*)
    11.5      fun rat ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    11.6        | rat ((c as Const(@{const_name Algebras.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    11.7 -      | rat ((c as Const(@{const_name Algebras.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    11.8 +      | rat ((c as Const(@{const_name Rings.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    11.9        | rat ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
   11.10        | rat ((c as Const(@{const_name Algebras.uminus}, _)) $ x) = c $ (rat x)
   11.11        | rat t = lit t
    12.1 --- a/src/HOL/ex/svc_funcs.ML	Wed Feb 10 08:49:26 2010 +0100
    12.2 +++ b/src/HOL/ex/svc_funcs.ML	Wed Feb 10 08:49:26 2010 +0100
    12.3 @@ -173,7 +173,7 @@
    12.4        | tm (Const(@{const_name Algebras.times}, T) $ x $ y) =
    12.5            if is_numeric_op T then Interp("*", [tm x, tm y])
    12.6            else fail t
    12.7 -      | tm (Const(@{const_name Algebras.inverse}, T) $ x) =
    12.8 +      | tm (Const(@{const_name Rings.inverse}, T) $ x) =
    12.9            if domain_type T = HOLogic.realT then
   12.10                Rat(1, litExp x)
   12.11            else fail t