swh:1:snp:a009335c9ad61a15b4ffe398f445dd601942b68c
Tip revision: e422fcb07e3f2b54871c7686ce0c329db5b01397 authored by Pierre-Yves Strub on 24 July 2021, 17:58:50 UTC
Improve search command
Improve search command
Tip revision: e422fcb
StdRing.ec
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-B-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
require import Bool Int Real.
require (*--*) Ring.
(* -------------------------------------------------------------------- *)
instance ring with int
op rzero = CoreInt.zero
op rone = CoreInt.one
op add = CoreInt.add
op opp = CoreInt.opp
op mul = CoreInt.mul
op expr = Ring.IntID.exp
proof oner_neq0 by smt()
proof addr0 by smt()
proof addrA by smt()
proof addrC by smt()
proof addrN by smt()
proof mulr1 by smt()
proof mulrA by smt()
proof mulrC by smt()
proof mulrDl by smt()
proof expr0 by smt(Ring.IntID.expr0)
proof exprS by smt(Ring.IntID.exprS).
op bid (b:bool) = b.
instance bring with bool
op rzero = false
op rone = true
op add = Bool.( ^^ )
op mul = (/\)
op opp = bid
proof oner_neq0 by smt()
proof addr0 by smt()
proof addrA by smt()
proof addrC by smt()
proof addrK by smt()
proof mulr1 by smt()
proof mulrA by smt()
proof mulrC by smt()
proof mulrDl by smt()
proof mulrK by smt()
proof oppr_id by smt().