Commit d4f77f6f authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Merge remote-tracking branch 'berghofer/master'

parents 63ad8e88 edd35d17
......@@ -155,6 +155,7 @@ pvsbin/
ISABELLELIBS_INT_FILES = Exponentiation Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power
ISABELLELIBS_INT_FILES = Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power
ISABELLELIBS_INT = $(addsuffix .xml, $(addprefix lib/isabelle/int/, $(ISABELLELIBS_INT_FILES)))
ISABELLELIBS_BOOL = $(addsuffix .xml, $(addprefix lib/isabelle/bool/, $(ISABELLELIBS_BOOL_FILES)))
ISABELLELIBS_REAL_FILES = # not yet realized : Abs ExpLog FromInt MinMax PowerInt Real Square RealInfix
ISABELLELIBS_REAL_FILES = Real RealInfix Abs MinMax FromInt Truncate Square ExpLog Trigonometry PowerInt # not yet realized : PowerReal Hyperbolic Polar
ISABELLELIBS_REAL = $(addsuffix .xml, $(addprefix lib/isabelle/real/, $(ISABELLELIBS_REAL_FILES)))
ISABELLELIBS_NUMBER_FILES = Divisibility Gcd Parity Prime Coprime
......@@ -1178,6 +1178,9 @@ ISABELLELIBS_MAP = $(addsuffix .xml, $(addprefix lib/isabelle/map/, $(ISABELLELI
ISABELLELIBS_LIST_FILES = List Length Mem Nth NthNoOpt NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt RevAppend Combine Distinct NumOcc Permut
ISABELLELIBS_LIST = $(addsuffix .xml, $(addprefix lib/isabelle/list/, $(ISABELLELIBS_LIST_FILES)))
ISABELLELIBS_BV_FILES = Pow2int BV8 BV16 BV32 BV64 BVConverter_32_64 BVConverter_16_64 BVConverter_8_64 BVConverter_16_32 BVConverter_8_32 BVConverter_8_16
ISABELLELIBS_BV = $(addsuffix .xml, $(addprefix lib/isabelle/bv/, $(ISABELLELIBS_BV_FILES)))
drivers/isabelle-realizations.aux: Makefile
$(if $(QUIET),@echo 'Generate $@' &&) \
(echo "(* generated automatically at compilation time *)"; \
......@@ -1198,6 +1201,8 @@ drivers/isabelle-realizations.aux: Makefile
echo 'theory list.'"$$f"' meta "realized_theory" "list.'"$$f"'", "" end'; done; \
echo 'theory option.'"$$f"' meta "realized_theory" "option.'"$$f"'", "" end'; done; \
for f in $(ISABELLELIBS_BV_FILES); do \
echo 'theory bv.'"$$f"' meta "realized_theory" "bv.'"$$f"'", "" end'; done; \
) > $@
ifeq (@enable_local@,yes)
......@@ -1206,7 +1211,7 @@ else
ifneq (@enable_local@,yes)
cp -r lib/isabelle "$(LIBDIR)/why3"
......@@ -1227,7 +1232,7 @@ install_no_local:: lib/isabelle/last_build
install_local:: lib/isabelle/last_build
$(ISABELLELIBS_INT): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/int.why
......@@ -1269,6 +1274,11 @@ $(ISABELLELIBS_OPTION): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realization
mkdir -p lib/isabelle/option
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T option.$(notdir $(basename $@)) -o lib/isabelle/option/
$(ISABELLELIBS_BV): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/bv.why
mkdir -p lib/isabelle/bv
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bv.$(notdir $(basename $@)) -o lib/isabelle/bv/
# do not update isabelle realizations systematically
# opt byte: update-isabelle
......@@ -166,5 +166,60 @@ theory number.Coprime
syntax predicate coprime "<app><const name=\"GCD.gcd_class.coprime\"/>%1%2</app>"
theory algebra.Field
syntax function inv "<app><const name=\"Fields.inverse_class.inverse\"/>%1</app>"
syntax function (/) "<app><const name=\"Fields.inverse_class.divide\"/>%1%2</app>"
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=\"\"/>%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>"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
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
theory real.Abs
syntax function abs "<app><const name=\"Groups.abs_class.abs\"/>%1</app>"
remove prop Abs_pos
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>"
theory real.Trigonometry
syntax function tan "<app><const name=\"Transcendental.tan\"/>%1</app>"
(* this file has an extension .aux rather than .gen since it should not be distributed *)
import "isabelle-realizations.aux"
chapter Why3
session Why3 = HOL +
session Why3 = "HOL-Word" +
options [document = false]
theories Why3
......@@ -6,6 +6,8 @@ imports
This diff is collapsed.
theory Why3_Real
imports Complex_Main "~~/src/HOL/Decision_Procs/Approximation" Why3_Setup
section {* Real numbers and the basic unary and binary operators *}
why3_open "real/Real.xml"
why3_vc infix_lseq_def by auto
why3_vc Assoc by auto
why3_vc Unit_def_l by auto
why3_vc Unit_def_r by auto
why3_vc Inv_def_l by auto
why3_vc Inv_def_r by auto
why3_vc Comm by simp
why3_vc Assoc1 by simp
why3_vc Mul_distr_l by (simp add: Fields.linordered_field_class.sign_simps)
why3_vc Mul_distr_r by (simp add: Rings.comm_semiring_class.distrib)
why3_vc infix_mn_def by auto
why3_vc Comm1 by auto
why3_vc Unitary by auto
why3_vc NonTrivialRing by auto
why3_vc Inverse by (simp add: assms)
why3_vc add_div by (simp add: Fields.division_ring_class.add_divide_distrib)
why3_vc sub_div by (simp add: Fields.division_ring_class.diff_divide_distrib)
why3_vc neg_div by auto
why3_vc assoc_mul_div by auto
why3_vc assoc_div_mul by auto
why3_vc assoc_div_div by auto
why3_vc Refl by auto
why3_vc Trans
using assms
by auto
why3_vc Antisymm
using assms
by auto
why3_vc Total by auto
why3_vc ZeroLessOne by auto
why3_vc CompatOrderAdd
using assms
by auto
why3_vc CompatOrderMult
using assms
by (simp add: Rings.ordered_semiring_class.mult_right_mono)
why3_vc infix_sl_def by (simp add: Real.divide_real_def)
section {* Alternative Infix Operators *}
why3_open "real/RealInfix.xml"
section {* Absolute Value *}
why3_open "real/Abs.xml"
why3_vc Abs_le by auto
why3_vc Abs_pos by auto
why3_vc Abs_sum by auto
why3_vc abs_def by (simp add: Real.abs_real_def)
why3_vc Abs_prod by (simp add: Rings.linordered_idom_class.abs_mult)
why3_vc triangular_inequality by (simp add: Real.abs_real_def)
section {* Minimum and Maximum *}
why3_open "real/MinMax.xml"
why3_vc Max_l
using assms
by auto
why3_vc Min_r
using assms
by auto
why3_vc max_def by auto
why3_vc min_def by auto
why3_vc Max_comm by auto
why3_vc Min_comm by auto
why3_vc Max_assoc by auto
why3_vc Min_assoc by auto
section {* Injection of integers into reals *}
why3_open "real/FromInt.xml"
from_int = of_int
why3_vc Add by auto
why3_vc Mul by auto
why3_vc Neg by auto
why3_vc One by auto
why3_vc Sub by auto
why3_vc Zero by auto
section {* Various truncation functions *}
(* truncate: rounds towards zero *)
definition truncate :: "real \<Rightarrow> int" where
"truncate x = (if x \<ge> 0 then floor x else ceiling x)"
why3_open "real/Truncate.xml"
truncate = truncate
floor = floor
ceil = ceiling
subsection {* Roundings up and down *}
why3_vc Ceil_up
by (simp_all add: ceiling_correct)
why3_vc Ceil_int by auto
why3_vc Floor_int by auto
why3_vc Floor_down
by (simp_all add: floor_correct [simplified])
why3_vc Ceil_monotonic
using assms
by (simp add:ceiling_mono)
why3_vc Floor_monotonic
using assms
by (simp add:floor_mono)
subsection {* Rounding towards zero *}
why3_vc Real_of_truncate
using floor_correct [of x] ceiling_correct [of x]
by (simp_all add: truncate_def)
why3_vc Truncate_int by (simp add:truncate_def)
why3_vc Truncate_up_neg
using assms ceiling_correct [of x]
by (simp_all add: truncate_def)
why3_vc Truncate_down_pos
using assms floor_correct [of x]
by (simp_all add: truncate_def)
why3_vc Truncate_monotonic
using assms
unfolding truncate_def
by (simp add: floor_mono ceiling_mono order_trans [of "\<lceil>x\<rceil>" 0 "\<lfloor>y\<rfloor>"])
why3_vc Truncate_monotonic_int1
using assms
by (simp add: truncate_def floor_le_iff ceiling_le_iff)
why3_vc Truncate_monotonic_int2
using assms
by (simp add: truncate_def le_floor_iff le_ceiling_iff)
section {* Square and Square Root *}
why3_open "real/Square.xml"
sqrt = sqrt
why3_vc Sqrt_le
using assms
by auto
why3_vc Sqrt_mul by (simp add: NthRoot.real_sqrt_mult)
why3_vc Sqrt_square
using assms
by (simp add: sqr_def)
why3_vc Square_sqrt
using assms
by auto
why3_vc Sqrt_positive
using assms
by auto
section {* Exponential and Logarithm *}
why3_open "real/ExpLog.xml"
exp = exp
log = ln
why3_vc Exp_log
using assms
by auto
why3_vc Exp_sum by (simp add: Transcendental.exp_add)
why3_vc Log_exp by auto
why3_vc Log_mul
using assms
by (simp add: Transcendental.ln_mult)
why3_vc Log_one by auto
why3_vc Exp_zero by auto
section {* Power of a real to an integer *}
(* TODO: clones int.Exponentiation which is not yet realized *)
why3_open "real/PowerInt.xml"
why3_vc Power_0 by auto
why3_vc Power_1 by auto
why3_vc Power_s
using assms
by (simp add: nat_add_distrib)
why3_vc Power_sum
using assms
by (simp add: nat_add_distrib power_add)
why3_vc Pow_ge_one using assms by auto
why3_vc Power_mult
using assms
by (simp add: nat_mult_distrib power_mult)
why3_vc Power_mult2 by (simp only:Power.comm_monoid_mult_class.power_mult_distrib)
why3_vc Power_s_alt
proof -
have "nat n = Suc (nat (n - 1))" using assms by auto
then show ?thesis by simp
section {* Power of a real to a real exponent *}
(* TODO: no power to a real exponent in Isabelle? *)
section {* Trigonometric Functions *}
why3_open "real/Trigonometry.xml"
cos = cos
sin = sin
pi = pi
atan = arctan
why3_vc Cos_0 by auto
why3_vc Sin_0 by auto
why3_vc Cos_pi by auto
why3_vc Sin_pi by auto
why3_vc Cos_neg by auto
why3_vc Cos_pi2 by auto
why3_vc Cos_sum by (simp add: Transcendental.cos_add)
why3_vc Sin_neg by auto
why3_vc Sin_pi2 by auto
why3_vc Sin_sum by (simp add: Transcendental.sin_add)
why3_vc tan_def by (simp add: Transcendental.tan_def)
why3_vc Tan_atan by (simp add: Transcendental.tan_arctan)
why3_vc Cos_le_one by auto
why3_vc Sin_le_one by auto
why3_vc Cos_plus_pi by auto
why3_vc Pi_interval
proof -
have "3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196 < pi"
by (approximation 670)
then show ?C1 by simp
have "pi < 3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197"
by (approximation 670)
then show ?C2 by simp
why3_vc Sin_plus_pi by auto
why3_vc Cos_plus_pi2 by (simp add: Transcendental.minus_sin_cos_eq)
why3_vc Sin_plus_pi2 by (simp add: sin_add)
why3_vc Pythagorean_identity
by (simp add: sqr_def)
section {* Hyperbolic Functions *}
(* TODO: missing acosh *)
section {* Polar Coordinates *}
(* TODO: missing atan2 *)
theory Why3_Setup
imports "~~/src/HOL/Word/Word" "~~/src/HOL/Word/Bit_Comparison"
imports Main
"why3_open" :: thy_load and
"why3_end" "why3_consts" "why3_types" "why3_thms" "why3_defs" :: thy_decl and
......@@ -424,8 +424,8 @@ fun read_decl ctxt = variant
(get_name'' atts, expand_cases ctxt (read_prop ctxt t)))) xs))];
fun rename_const ps = map_aterms
(fn t as Const (s, T) => (case AList.lookup (op =) ps s of
SOME s' => Free (s', T)
(fn t as Const (p as (_, T)) => (case AList.lookup (op =) ps p of
SOME s => Free (s, T)
| NONE => t)
| t => t);
......@@ -490,10 +490,10 @@ fun mk_decl _ (Axiom ((s, id), ts)) thy =
add_const s,
| SOME [th] =>
let val (s', _) = head_of_eqn' (Thm.prop_of th)
let val p as (s', _) = head_of_eqn' (Thm.prop_of th)
handle TERM _ => error ("Bad equation for " ^ string_of_id id)
if Pattern.matches thy (rename_const [(s', s)] (Thm.prop_of th), eqn)
if Pattern.matches thy (rename_const [(p, s)] (Thm.prop_of th), eqn)
then (add_const_raw NONE (s, s') thy, false)
else error ("Failed to match definition " ^ string_of_id id)
......@@ -552,7 +552,7 @@ fun mk_decl _ (Axiom ((s, id), ts)) thy =
| SOME preds' =>
let val cmap = map (fn (((s, id), _, _), th :: _) =>
(th |> Thm.concl_of |> HOLogic.dest_Trueprop |> head_of |>
dest_Const |> fst handle TERM _ =>
dest_Const handle TERM _ =>
error ("Bad introduction rule for " ^ string_of_id id),
s)) preds'
......@@ -563,7 +563,7 @@ fun mk_decl _ (Axiom ((s, id), ts)) thy =
(intrs, intrs')
then ()
else error ("Failed to match predicate " ^ string_of_id id)) preds';
(fold (add_const_raw NONE o swap) cmap thy, false)
(fold (add_const_raw NONE o swap o apfst fst) cmap thy, false)
| mk_decl _ (Function eqnss) thy =
let val eqnss' = map (head_of_eqn o hd o snd) eqnss
......@@ -578,7 +578,7 @@ fun mk_decl _ (Axiom ((s, id), ts)) thy =
| SOME eqnss'' =>
let val cmap = map2 (fn ((id, _), th :: _) => fn (s, _) =>
(th |> Thm.prop_of |> head_of_eqn' |> fst handle TERM _ =>
(th |> Thm.prop_of |> head_of_eqn' handle TERM _ =>
error ("Bad equation for " ^ string_of_id id),
s)) eqnss'' eqnss'
......@@ -589,7 +589,7 @@ fun mk_decl _ (Axiom ((s, id), ts)) thy =
(eqns, eqns')
then ()
else error ("Failed to match function " ^ string_of_id id)) eqnss'';
(fold (add_const_raw NONE o swap) cmap thy, false)
(fold (add_const_raw NONE o swap o apfst fst) cmap thy, false)
| mk_decl _ _ thy = (thy, true);
......@@ -48,17 +48,16 @@ let opt_string_of_bool b = if b then Some "true" else None
let black_list =
["o"; "O"]
let isanitize = sanitizer' char_to_alpha char_to_alnumus char_to_alnum
let fresh_printer () =
let isanitize = sanitizer' char_to_alpha char_to_alnumus char_to_alnum in
create_ident_printer black_list ~sanitizer:isanitize
let iprinter = fresh_printer ()
let thprinter = fresh_printer ()
let forget_ids () = forget_all iprinter
let forget_ids () =
forget_all iprinter;
forget_all thprinter
let string_of_id id = isanitize id.id_string
(* type variables *)
......@@ -90,7 +89,7 @@ type info = {
let print_id fmt id = string fmt (id_unique iprinter id)
let print_altname_path info fmt id =
attribs "altname" string
attribs "altname" html_string
(print_option (attrib "path" string))
fmt (id.id_string, Mid.find_opt id info.theories)
......@@ -419,7 +418,7 @@ let print_decls info fmt dl =
print_list nothing (print_decl info) fmt dl
let make_thname th = String.concat "." (th.Theory.th_path @
[id_unique thprinter th.Theory.th_name])
[string_of_id th.Theory.th_name])
let print_task printer_args realize fmt task =
forget_ids ();
......@@ -439,11 +438,11 @@ let print_task printer_args realize fmt task =
let rec upd_realized_theories = function
| Some { Task.task_decl = { Theory.td_node =
Theory.Decl { Decl.d_node = Decl.Dprop (Decl.Pgoal, pr, _) }}} ->
id_unique thprinter pr.pr_name, realized_theories
string_of_id pr.pr_name, realized_theories
| Some { Task.task_decl = { Theory.td_node = Theory.Clone (th,_) }} ->
Sid.iter (fun id -> ignore (id_unique iprinter id)) th.Theory.th_local;
let id = th.Theory.th_name in
String.concat "." (th.Theory.th_path @ [id_unique thprinter id]),
String.concat "." (th.Theory.th_path @ [string_of_id id]),
Mid.remove id realized_theories
| Some { Task.task_decl = { Theory.td_node = Theory.Meta _ };
Task.task_prev = task } ->
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment