drivers/isabelle-common.gen

   1 (* driver for Isabelle/HOL *)
   2 (* main author: Stefan Berghofer <stefan.berghofer@secunet.com> *)
   3
   4
   5 valid "Finished Why3 theory"
   6 valid "All verification conditions have been proved"
   7 unknown "The following verification conditions remain to be proved" "incomplete proof"
   8 (* fail "\\*\\*\\* \\(.*\\)$" "\\1" *)
   9 time "why3cpulimit time : %s s"
  10
  11 transformation "eliminate_negative_constants"
  12 transformation "eliminate_literal"
  13 transformation "eliminate_if_fmla"
  14 transformation "eliminate_epsilon"
  15 transformation "eliminate_let_fmla"
  16 transformation "simplify_formula"
  17
  18 theory BuiltIn
  19   syntax type int "<type name=\"Int.int\"/>"
  20   syntax type real "<type name=\"Real.real\"/>"
  21
  22   syntax predicate  (=)   "<app><const name=\"HOL.eq\"/>%1%2</app>"
  23 end
  24
  25 theory Ignore
  26   syntax predicate ignore'term  "<const name=\"HOL.True\"/>"
  27 end
  28
  29 theory HighOrd
  30   syntax type (->) "<fun>%1%2</fun>"
  31   syntax function (@) "<app>%1%2</app>"
  32 end
  33
  34 theory Bool
  35   syntax type bool   "<type name=\"HOL.bool\"/>"
  36
  37   syntax function True  "<const name=\"HOL.True\"/>"
  38   syntax function False "<const name=\"HOL.False\"/>"
  39 end
  40
  41 theory bool.Bool
  42   syntax function andb  "<app><const name=\"HOL.conj\"/>%1%2</app>"
  43   syntax function orb   "<app><const name=\"HOL.disj\"/>%1%2</app>"
  44   syntax function xorb  "<app><const name=\"HOL.Not\"/><app><const name=\"HOL.eq\"/>%1%2</app></app>"
  45   syntax function notb  "<app><const name=\"HOL.Not\"/>%1</app>"
  46   syntax function implb "<app><const name=\"HOL.implies\"/>%1%2</app>"
  47 end
  48
  49 theory int.Int
  50   syntax function zero "<number val=\"0\"><type name=\"Int.int\"/></number>"
  51   syntax function one  "<number val=\"1\"><type name=\"Int.int\"/></number>"
  52
  53   syntax function (+)  "<app><const name=\"Groups.plus_class.plus\"/>%1%2</app>"
  54   syntax function (-)  "<app><const name=\"Groups.minus_class.minus\"/>%1%2</app>"
  55   syntax function (*)  "<app><const name=\"Groups.times_class.times\"/>%1%2</app>"
  56   syntax function (-_) "<app><const name=\"Groups.uminus_class.uminus\"/>%1</app>"
  57
  58   syntax predicate (<=) "<app><const name=\"Orderings.ord_class.less_eq\"/>%1%2</app>"
  59   syntax predicate (<)  "<app><const name=\"Orderings.ord_class.less\"/>%1%2</app>"
  60   syntax predicate (>=) "<app><const name=\"Orderings.ord_class.less_eq\"/>%2%1</app>"
  61   syntax predicate (>)  "<app><const name=\"Orderings.ord_class.less\"/>%2%1</app>"
  62
  63   remove prop MulComm.Comm
  64   remove prop MulAssoc.Assoc
  65   remove prop Unit_def_l
  66   remove prop Unit_def_r
  67   remove prop Inv_def_l
  68   remove prop Inv_def_r
  69   remove prop Assoc
  70   remove prop Mul_distr_l
  71   remove prop Mul_distr_r
  72   remove prop Comm
  73   remove prop Unitary
  74   remove prop Refl
  75   remove prop Trans
  76   remove prop Antisymm
  77   remove prop Total
  78   remove prop NonTrivialRing
  79   remove prop CompatOrderAdd
  80   remove prop CompatOrderMult
  81   remove prop ZeroLessOne
  82 end
  83
  84 theory int.Abs
  85   syntax function abs "<app><const name=\"Groups.abs_class.abs\"/>%1</app>"
  86
  87   remove prop Abs_pos
  88 end
  89
  90 theory int.MinMax
  91   syntax function min "<app><const name=\"Orderings.ord_class.min\"/>%1%2</app>"
  92   syntax function max "<app><const name=\"Orderings.ord_class.max\"/>%1%2</app>"
  93 end
  94
  95 theory int.Exponentiation
  96   syntax function power "<app><const name=\"Power.power_class.power\"/>%1<app><const name=\"Int.nat\"/>%2</app></app>"
  97 end
  98
  99 theory list.List
 100   syntax type list "<type name=\"List.list\">%1</type>"
 101
 102   syntax function Nil "<const name=\"List.list.Nil\">%t0</const>"
 103   syntax function Cons "<app><const name=\"List.list.Cons\"/>%1%2</app>"
 104 end
 105
 106 theory list.Length
 107   syntax function length "<app><const name=\"Nat.semiring_1_class.of_nat\"><fun><type name=\"Nat.nat\"/><type name=\"Int.int\"/></fun></const><app><const name=\"List.length\"/>%1</app></app>"
 108 end
 109
 110 theory list.Append
 111   syntax function (++) "<app><const name=\"List.append\"/>%1%2</app>"
 112 end
 113
 114 theory list.Reverse
 115   syntax function reverse "<app><const name=\"List.rev\"/>%1</app>"
 116 end
 117
 118 theory list.Mem
 119   syntax predicate mem "<app><const name=\"Set.member\"/>%1<app><const name=\"List.list.set\"/>%2</app></app>"
 120 end
 121
 122 theory list.NthNoOpt
 123   syntax function nth "<app><const name=\"List.nth\"/>%2<app><const name=\"Int.nat\"/>%1</app></app>"
 124 end
 125
 126 theory list.HdTlNoOpt
 127   syntax function hd "<app><const name=\"List.list.hd\"/>%1</app>"
 128   syntax function tl "<app><const name=\"List.list.tl\"/>%1</app>"
 129 end
 130
 131 theory list.Distinct
 132   syntax predicate distinct "<app><const name=\"List.distinct\"/>%1</app>"
 133 end
 134
 135 theory option.Option
 136   syntax type option "<type name=\"Option.option\">%1</type>"
 137
 138   syntax function None "<const name=\"Option.option.None\">%t0</const>"
 139   syntax function Some "<app><const name=\"Option.option.Some\"/>%1</app>"
 140 end
 141
 142 theory map.Map
 143   syntax function get "<app>%1%2</app>"
 144   syntax function ([]) "<app>%1%2</app>"
 145   syntax function set "<app><const name=\"Fun.fun_upd\"/>%1%2%3</app>"
 146   syntax function ([<-]) "<app><const name=\"Fun.fun_upd\"/>%1%2%3</app>"
 147 end
 148
 149 theory set.Fset
 150   syntax function cardinal "<app><const name=\"Nat.semiring_1_class.of_nat\"><fun><type name=\"Nat.nat\"/><type name=\"Int.int\"/></fun></const><app><const name=\"FSet.fcard\"/>%1</app></app>"
 151 end
 152
 153 theory number.Parity
 154   syntax predicate even "<app><const name=\"Parity.semiring_parity_class.even\"/>%1</app>"
 155   syntax predicate odd  "<app><const name=\"Parity.semiring_parity_class.odd\"/>%1</app>"
 156 end
 157
 158 theory number.Divisibility
 159   syntax predicate divides "<app><const name=\"Rings.dvd_class.dvd\"/>%1%2</app>"
 160 end
 161
 162 theory number.Gcd
 163   syntax function gcd "<app><const name=\"GCD.gcd_class.gcd\"/>%1%2</app>"
 164 end
 165
 166 theory number.Prime
 167   syntax predicate prime "<app><const name=\"Factorial_Ring.normalization_semidom_class.prime\"/>%1</app>"
 168 end
 169
 170 theory number.Coprime
 171   syntax predicate coprime "<app><const name=\"Rings.algebraic_semidom_class.coprime\"/>%1%2</app>"
 172 end
 173
 174 theory algebra.Field
 175   syntax function inv "<app><const name=\"Fields.inverse_class.inverse\"/>%1</app>"
 176   syntax function (/) "<app><const name=\"Rings.divide_class.divide\"/>%1%2</app>"
 177 end
 178
 179 theory real.Real
 180   syntax function zero "<number val=\"0\"><type name=\"Real.real\"/></number>"
 181   syntax function one  "<number val=\"1\"><type name=\"Real.real\"/></number>"
 182
 183   syntax function (+)  "<app><const name=\"Groups.plus_class.plus\"/>%1%2</app>"
 184   syntax function (-)  "<app><const name=\"Groups.minus_class.minus\"/>%1%2</app>"
 185   syntax function (*)  "<app><const name=\"Groups.times_class.times\"/>%1%2</app>"
 186   syntax function (-_) "<app><const name=\"Groups.uminus_class.uminus\"/>%1</app>"
 187
 188   syntax predicate (<=) "<app><const name=\"Orderings.ord_class.less_eq\"/>%1%2</app>"
 189   syntax predicate (<)  "<app><const name=\"Orderings.ord_class.less\"/>%1%2</app>"
 190   syntax predicate (>=) "<app><const name=\"Orderings.ord_class.less_eq\"/>%2%1</app>"
 191   syntax predicate (>)  "<app><const name=\"Orderings.ord_class.less\"/>%2%1</app>"
 192
 193   remove prop MulComm.Comm
 194   remove prop MulAssoc.Assoc
 195   remove prop Unit_def_l
 196   remove prop Unit_def_r
 197   remove prop Inv_def_l
 198   remove prop Inv_def_r
 199   remove prop Assoc
 200   remove prop Mul_distr_l
 201   remove prop Mul_distr_r
 202   remove prop Comm
 203   remove prop Unitary
 204   remove prop Refl
 205   remove prop Trans
 206   remove prop Antisymm
 207   remove prop Total
 208   remove prop NonTrivialRing
 209   remove prop CompatOrderAdd
 210   remove prop CompatOrderMult
 211   remove prop ZeroLessOne
 212 end
 213
 214 theory real.Abs
 215   syntax function abs "<app><const name=\"Groups.abs_class.abs\"/>%1</app>"
 216
 217   remove prop Abs_pos
 218 end
 219
 220 theory real.MinMax
 221   syntax function min "<app><const name=\"Orderings.ord_class.min\"/>%1%2</app>"
 222   syntax function max "<app><const name=\"Orderings.ord_class.max\"/>%1%2</app>"
 223 end
 224
 225 theory real.Trigonometry
 226   syntax function tan "<app><const name=\"Transcendental.tan\"/>%1</app>"
 227 end
 228
 229 theory bv.BV_Gen
 230   meta "literal:keep" type t
 231   syntax function to_int "<app><const name=\"Word.sint\"/>%1</app>"
 232 end
 233
 234 theory bv.BV64
 235   meta "literal:keep" type t
 236 end
 237
 238 theory bv.BV32
 239   meta "literal:keep" type t
 240 end
 241
 242 theory bv.BV16
 243   meta "literal:keep" type t
 244 end
 245
 246 theory bv.BV8
 247   meta "literal:keep" type t
 248 end
 249
 250 (* this file has an extension .aux rather than .gen since it should not be distributed *)
 251 import "isabelle-realizations.aux"