isabelle-common.gen 7.35 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4
(* driver for Isabelle/HOL *)
(* main author: Stefan Berghofer <stefan.berghofer@secunet.com> *)


5 6 7 8
valid "Finished Why3 theory"
fail "\\*\\*\\* \\(.*\\)$" "\\1"
time "why3cpulimit time : %s s"

9
transformation "eliminate_negative_constants"
10
transformation "eliminate_if_fmla"
Quentin Garchery's avatar
Quentin Garchery committed
11
transformation "eliminate_epsilon"
12
transformation "eliminate_let_fmla"
13 14 15 16 17 18 19 20 21
transformation "simplify_formula"

theory BuiltIn
  syntax type int "<type name=\"Int.int\"/>"
  syntax type real "<type name=\"Real.real\"/>"

  syntax predicate  (=)   "<app><const name=\"HOL.eq\"/>%1%2</app>"
end

22 23 24 25 26
theory HighOrd
  syntax type (->) "<fun>%1%2</fun>"
  syntax function (@) "<app>%1%2</app>"
end

27 28 29 30 31 32 33 34 35 36
theory Bool
  syntax type bool   "<type name=\"HOL.bool\"/>"

  syntax function True  "<const name=\"HOL.True\"/>"
  syntax function False "<const name=\"HOL.False\"/>"
end

theory bool.Bool
  syntax function andb  "<app><const name=\"HOL.conj\"/>%1%2</app>"
  syntax function orb   "<app><const name=\"HOL.disj\"/>%1%2</app>"
37
  syntax function xorb  "<app><const name=\"HOL.Not\"/><app><const name=\"HOL.eq\"/>%1%2</app></app>"
38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55
  syntax function notb  "<app><const name=\"HOL.Not\"/>%1</app>"
  syntax function implb "<app><const name=\"HOL.implies\"/>%1%2</app>"
end

theory int.Int
  syntax function zero "<number val=\"0\"><type name=\"Int.int\"/></number>"
  syntax function one  "<number val=\"1\"><type name=\"Int.int\"/></number>"

  syntax function (+)  "<app><const name=\"Groups.plus_class.plus\"/>%1%2</app>"
  syntax function (-)  "<app><const name=\"Groups.minus_class.minus\"/>%1%2</app>"
  syntax function (*)  "<app><const name=\"Groups.times_class.times\"/>%1%2</app>"
  syntax function (-_) "<app><const name=\"Groups.uminus_class.uminus\"/>%1</app>"

  syntax predicate (<=) "<app><const name=\"Orderings.ord_class.less_eq\"/>%1%2</app>"
  syntax predicate (<)  "<app><const name=\"Orderings.ord_class.less\"/>%1%2</app>"
  syntax predicate (>=) "<app><const name=\"Orderings.ord_class.less_eq\"/>%2%1</app>"
  syntax predicate (>)  "<app><const name=\"Orderings.ord_class.less\"/>%2%1</app>"

56 57 58 59 60 61 62
  remove prop MulComm.Comm
  remove prop MulAssoc.Assoc
  remove prop Unit_def_l
  remove prop Unit_def_r
  remove prop Inv_def_l
  remove prop Inv_def_r
  remove prop Assoc
63 64
  remove prop Mul_distr_l
  remove prop Mul_distr_r
65
  remove prop Comm
66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop CompatOrderMult
  remove prop ZeroLessOne
end

theory int.Abs
  syntax function abs "<app><const name=\"Groups.abs_class.abs\"/>%1</app>"

  remove prop Abs_pos
end

theory int.MinMax
  syntax function min "<app><const name=\"Orderings.ord_class.min\"/>%1%2</app>"
  syntax function max "<app><const name=\"Orderings.ord_class.max\"/>%1%2</app>"
end

Stefan Berghofer's avatar
Stefan Berghofer committed
88 89
theory int.Exponentiation
  syntax function power "<app><const name=\"Power.power_class.power\"/>%1<app><const name=\"Int.nat\"/>%2</app></app>"
90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111
end

theory list.List
  syntax type list "<type name=\"List.list\">%1</type>"

  syntax function Nil "<const name=\"List.list.Nil\">%t0</const>"
  syntax function Cons "<app><const name=\"List.list.Cons\"/>%1%2</app>"
end

theory list.Length
  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>"
end

theory list.Append
  syntax function (++) "<app><const name=\"List.append\"/>%1%2</app>"
end

theory list.Reverse
  syntax function reverse "<app><const name=\"List.rev\"/>%1</app>"
end

theory list.Mem
Stefan Berghofer's avatar
Stefan Berghofer committed
112
  syntax predicate mem "<app><const name=\"Set.member\"/>%1<app><const name=\"List.list.set\"/>%2</app></app>"
113 114 115 116 117 118
end

theory list.NthNoOpt
  syntax function nth "<app><const name=\"List.nth\"/>%2<app><const name=\"Int.nat\"/>%1</app></app>"
end

119
theory list.HdTlNoOpt
Stefan Berghofer's avatar
Stefan Berghofer committed
120 121
  syntax function hd "<app><const name=\"List.list.hd\"/>%1</app>"
  syntax function tl "<app><const name=\"List.list.tl\"/>%1</app>"
122 123 124 125 126 127
end

theory list.Distinct
  syntax predicate distinct "<app><const name=\"List.distinct\"/>%1</app>"
end

128 129 130 131 132 133 134 135 136 137 138 139
theory option.Option
  syntax type option "<type name=\"Option.option\">%1</type>"

  syntax function None "<const name=\"Option.option.None\">%t0</const>"
  syntax function Some "<app><const name=\"Option.option.Some\"/>%1</app>"
end

theory map.Map
  syntax function get "<app>%1%2</app>"
  syntax function ([]) "<app>%1%2</app>"
  syntax function set "<app><const name=\"Fun.fun_upd\"/>%1%2%3</app>"
  syntax function ([<-]) "<app><const name=\"Fun.fun_upd\"/>%1%2%3</app>"
140 141
end

142 143 144 145
theory set.Fset
  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>"
end

Stefan Berghofer's avatar
Stefan Berghofer committed
146 147 148 149 150
theory number.Parity
  syntax predicate even "<app><const name=\"Parity.semiring_parity_class.even\"/>%1</app>"
  syntax predicate odd  "<app><const name=\"Parity.semiring_parity_class.odd\"/>%1</app>"
end

151 152 153 154 155 156 157 158
theory number.Divisibility
  syntax predicate divides "<app><const name=\"Rings.dvd_class.dvd\"/>%1%2</app>"
end

theory number.Gcd
  syntax function gcd "<app><const name=\"GCD.gcd_class.gcd\"/>%1%2</app>"
end

Stefan Berghofer's avatar
Stefan Berghofer committed
159 160 161 162
theory number.Prime
  syntax predicate prime "<app><const name=\"Factorial_Ring.normalization_semidom_class.prime\"/>%1</app>"
end

163 164 165 166 167
theory algebra.Field
  syntax function inv "<app><const name=\"Fields.inverse_class.inverse\"/>%1</app>"
  syntax function (/) "<app><const name=\"Rings.divide_class.divide\"/>%1%2</app>"
end

168 169 170 171 172 173 174 175 176 177 178 179 180 181
theory real.Real
  syntax function zero "<number val=\"0\"><type name=\"Real.real\"/></number>"
  syntax function one  "<number val=\"1\"><type name=\"Real.real\"/></number>"

  syntax function (+)  "<app><const name=\"Groups.plus_class.plus\"/>%1%2</app>"
  syntax function (-)  "<app><const name=\"Groups.minus_class.minus\"/>%1%2</app>"
  syntax function (*)  "<app><const name=\"Groups.times_class.times\"/>%1%2</app>"
  syntax function (-_) "<app><const name=\"Groups.uminus_class.uminus\"/>%1</app>"

  syntax predicate (<=) "<app><const name=\"Orderings.ord_class.less_eq\"/>%1%2</app>"
  syntax predicate (<)  "<app><const name=\"Orderings.ord_class.less\"/>%1%2</app>"
  syntax predicate (>=) "<app><const name=\"Orderings.ord_class.less_eq\"/>%2%1</app>"
  syntax predicate (>)  "<app><const name=\"Orderings.ord_class.less\"/>%2%1</app>"

182 183 184 185 186 187 188
  remove prop MulComm.Comm
  remove prop MulAssoc.Assoc
  remove prop Unit_def_l
  remove prop Unit_def_r
  remove prop Inv_def_l
  remove prop Inv_def_r
  remove prop Assoc
189 190
  remove prop Mul_distr_l
  remove prop Mul_distr_r
191
  remove prop Comm
192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop CompatOrderMult
  remove prop ZeroLessOne
end

theory real.Abs
  syntax function abs "<app><const name=\"Groups.abs_class.abs\"/>%1</app>"

  remove prop Abs_pos
end

theory real.MinMax
  syntax function min "<app><const name=\"Orderings.ord_class.min\"/>%1%2</app>"
  syntax function max "<app><const name=\"Orderings.ord_class.max\"/>%1%2</app>"
end

theory real.Trigonometry
  syntax function tan "<app><const name=\"Transcendental.tan\"/>%1</app>"
end

218 219 220 221
theory bv.BV_Gen
  syntax function to_int "<app><const name=\"Word.sint\"/>%1</app>"
end

222 223
(* this file has an extension .aux rather than .gen since it should not be distributed *)
import "isabelle-realizations.aux"