Fix lemma names for ring.

lordqwerty · Jan 22, 2014 · 72cea5a · 72cea5a
1 parent 2ced384
commit 72cea5a
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 17 deletions.
diff --git a/src/ecAlgTactic.ml b/src/ecAlgTactic.ml
@@ -22,17 +22,17 @@ module Axioms = struct
   let expr  = "expr"
   let embed = "ofint"
 
-  let core_add = ["oner_neq0"; "addr0"; "addrA"; "addrC";]
-  let core_mul = [ "mulr1"; "mulrA"; "mulrC"; "mulrDl"]
-  let core   = core_add @ "addrN" :: core_mul
-  let core_bool = core_add @ "addrrN" :: "bmulrI" :: core_mul
-
-  let ofoppbool = ["oppE"] 
-  let intpow = ["expr0"; "exprS"]
-  let ofint  = ["ofint0"; "ofint1"; "ofintS"; "ofintN"]
-  let ofsub  = ["subrE"]
-  let field  = ["mulrV"; "exprN"]
-  let ofdiv  = ["divrE"]
+  let core_add  = ["oner_neq0"; "addr0"; "addrA"; "addrC";]
+  let core_mul  = [ "mulr1"; "mulrA"; "mulrC"; "mulrDl"]
+  let core      = core_add @ "addrN" :: core_mul
+  let core_bool = core_add @ "addrK" :: "mulrK" :: core_mul
+
+  let ofoppbool = ["oppr_id"]
+  let intpow    = ["expr0"; "exprS"]
+  let ofint     = ["ofint0"; "ofint1"; "ofintS"; "ofintN"]
+  let ofsub     = ["subrE"]
+  let field     = ["mulrV"; "exprN"]
+  let ofdiv     = ["divrE"]
 
   let ty0 ty = ty
   let ty1 ty = tfun ty (ty0 ty)

diff --git a/theories/AWord.ec b/theories/AWord.ec
@@ -68,13 +68,13 @@ instance boolean_ring with word
   proof addr0     by smt
   proof addrA     by smt
   proof addrC     by smt
-  proof addrrN    by smt
+  proof addrK     by smt
   proof mulr1     by smt
   proof mulrA     by smt
   proof mulrC     by smt
   proof mulrDl    by smt
-  proof oppE      by smt 
-  proof bmulrI    by smt.
+  proof oppr_id   by smt 
+  proof mulrK     by smt.
 
 require export ABitstring.
 op to_bits: word -> bitstring.

diff --git a/theories/AlgTactic.ec b/theories/AlgTactic.ec
@@ -71,10 +71,10 @@ theory Requires.
     forall (x : domain), add x (opp x) = rzero.
 
   (* For boolean ring *)
-  axiom nosmt addrrN:
+  axiom nosmt addrK:
     forall (x : domain), add x x = rzero.
 
-  axiom nosmt oppE:
+  axiom nosmt oppr_id:
     forall (x : domain), opp x = x.
 
   axiom nosmt mulr1:
@@ -90,7 +90,7 @@ theory Requires.
     forall (x y z: domain), mul x (add y z) = add (mul x y) (mul x z).
 
   (* For boolean ring *)
-  axiom nosmt bmulrI :
+  axiom nosmt mulrK:
     forall (x:domain), mul x x = x.
 
   axiom nosmt expr0: