Isabelle realization for reals

Works both with Isabelle 2014 and 2015

.gitignore

@@ -155,6 +155,7 @@ pvsbin/
 /lib/isabelle/number/
 /lib/isabelle/list/
 /lib/isabelle/map/
+/lib/isabelle/real/
 /lib/isabelle/set/
 /lib/isabelle/Tools/why3
 /lib/isabelle/Why3_Number.thy

Makefile.in

@@ -1162,7 +1162,7 @@ ISABELLELIBS_INT = $(addsuffix .xml, $(addprefix lib/isabelle/int/, $(ISABELLELI
 ISABELLELIBS_BOOL_FILES = Bool
 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

drivers/isabelle-common.gen

@@ -166,5 +166,60 @@ theory number.Coprime
   syntax predicate coprime "<app><const name=\"GCD.gcd_class.coprime\"/>%1%2</app>"
 end
 
+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>"
+end
+
+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>"
+
+  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
+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
+
 (* this file has an extension .aux rather than .gen since it should not be distributed *)
 import "isabelle-realizations.aux"

lib/isabelle/Why3_Real.thy

+theory Why3_Real
+imports Complex_Main "~~/src/HOL/Decision_Procs/Approximation" Why3_Setup
+begin
+
+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)
+
+why3_end
+
+section {* Alternative Infix Operators *}
+
+why3_open "real/RealInfix.xml"
+
+why3_end
+
+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)
+
+why3_end
+
+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
+
+why3_end
+
+section {* Injection of integers into reals *}
+
+why3_open "real/FromInt.xml"
+  constants
+    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
+
+why3_end
+
+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"
+  constants
+  truncate = truncate
+  floor = floor
+  ceil = ceiling
+
+subsection {* Roundings up and down *}
+
+why3_vc Ceil_up
+proof -
+  show ?C1 by linarith
+  show ?C2 by (simp add:ceiling_def) (linarith)
+qed
+
+why3_vc Ceil_int by auto
+
+why3_vc Floor_int by auto
+
+why3_vc Floor_down
+proof -
+  show ?C1 by linarith
+  show ?C2 by linarith
+qed
+
+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
+proof -
+  show ?C1
+    apply (simp add:ceiling_def truncate_def)
+    apply (linarith)
+    done
+  show ?C2
+    apply (simp add:ceiling_def truncate_def)
+    apply (linarith)
+    done
+qed
+
+why3_vc Truncate_int by (simp add:truncate_def)
+
+why3_vc Truncate_up_neg
+proof -
+  show ?C1
+    apply (simp add:ceiling_def truncate_def)
+    apply (linarith)
+    done
+  show ?C2
+    using assms
+    unfolding truncate_def ceiling_def
+    apply (simp)
+    apply (linarith)
+    done
+qed
+
+why3_vc Truncate_down_pos
+proof -
+  show ?C1
+    using assms
+    apply (simp add:ceiling_def truncate_def)
+    apply (linarith)
+    done
+  show ?C2
+    apply (simp add:ceiling_def truncate_def)
+    apply (linarith)
+    done
+qed
+
+why3_vc Truncate_monotonic
+proof -
+  { fix a b
+    assume "\<not> a > (0::int)" and "(0::int) \<le> b"
+    from this have "a \<le> b" by arith
+  } note neg_lesseq_nonneg = this
+  show ?C1 using assms
+  unfolding truncate_def
+  apply (simp add:floor_mono ceiling_mono neg_lesseq_nonneg)
+  done
+qed
+
+why3_vc Truncate_monotonic_int1
+proof -
+  show ?C1 using assms
+  apply (simp add:truncate_def)
+  apply (linarith)
+  done
+qed
+
+why3_vc Truncate_monotonic_int2
+proof -
+  show ?C1 using assms
+  apply (simp add:truncate_def)
+  apply (linarith)
+  done
+qed
+
+why3_end
+
+section {* Square and Square Root *}
+
+why3_open "real/Square.xml"
+  constants
+    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
+
+why3_end
+
+section {* Exponential and Logarithm *}
+
+why3_open "real/ExpLog.xml"
+  constants
+    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
+
+why3_end
+
+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
+proof -
+  { have "nat (n + 1) = Suc (nat n)" using assms by auto
+  } note l1 = this
+  show ?C1
+  apply (simp add:l1)
+  done
+qed
+
+why3_vc Power_sum
+proof -
+  { have "nat (n + m) = nat n + nat m" using assms by auto
+  } note l2 = this
+  show ?C1
+  apply (simp add:l2 Power.monoid_mult_class.power_add)
+  done
+qed
+
+why3_vc Pow_ge_one using assms by auto
+
+why3_vc Power_mult
+proof -
+  { have "nat (n * m) = nat n * nat m"
+    using assms
+    by (simp add:Nat_Transfer.transfer_nat_int_functions)
+  } note l3 = this
+  show ?C1
+  apply (simp add:l3 Power.monoid_mult_class.power_mult)
+  done
+qed
+
+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
+  } note l4 = this
+  show ?C1
+  apply (simp add:l4)
+  done
+qed
+
+why3_end
+
+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"
+  constants
+    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)
+  } note pi_greater = this
+  { have "pi < 3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197
+" by (approximation 670)
+  } note pi_less = this
+  (* explicitly remove exponentiation from the above lemmas *)
+  have a: "10 ^ 200 = (100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000::real)" by simp
+  from pi_less have pi_less': "pi < 314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197 /
+         100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000"
+     by (simp only: a)
+  also from pi_greater have pi_greater': "314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196 /
+    100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
+    < pi" by (simp only: a)
+  (* the rest is easy *)
+  show ?C1 by (simp only: pi_greater')
+  show ?C2 by (simp only: pi_less')
+qed
+
+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)
+
+why3_end
+
+section {* Hyperbolic Functions *}
+
+(* TODO: missing acosh *)
+
+section {* Polar Coordinates *}
+
+(* TODO: missing atan2 *)
+
+end