| Wed, 31 Jan 2024 21:10:52 +0100 |
wenzelm |
tuned proof: avoid z3;
|
file |
diff |
annotate
|
| Wed, 28 Dec 2022 12:15:16 +0000 |
paulson |
Tidied some messy proofs
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 08:42:36 +0200 |
desharna |
added opaque_combs and renamed hide_lams to opaque_lifting
|
file |
diff |
annotate
|
| Mon, 10 May 2021 16:14:34 +0200 |
wenzelm |
tuned proofs --- avoid z3, which is absent on arm64-linux;
|
file |
diff |
annotate
|
| Sun, 15 Nov 2020 07:17:06 +0000 |
haftmann |
bundles for reflected term syntax
|
file |
diff |
annotate
|
| Sun, 03 Nov 2019 19:58:02 -0500 |
immler |
moved theory Interval_Approximation from the AFP
|
file |
diff |
annotate
|
| Wed, 09 Oct 2019 14:51:54 +0000 |
haftmann |
dedicated fact collections for algebraic simplification rules potentially splitting goals
|
file |
diff |
annotate
|
| Sat, 22 Jun 2019 06:25:34 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 14 Jun 2019 08:34:28 +0000 |
haftmann |
official fact collection sign_simps
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 14:30:09 +0200 |
nipkow |
Prefix form of infix with * on either side no longer needs special treatment
|
file |
diff |
annotate
|
| Thu, 07 Jun 2018 19:36:12 +0200 |
nipkow |
utilize 'flip'
|
file |
diff |
annotate
|
| Mon, 05 Feb 2018 08:30:19 +0100 |
immler |
added lemmas, avoid 'float_of 0'
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Sat, 02 Dec 2017 16:50:53 +0000 |
haftmann |
more simplification rules
|
file |
diff |
annotate
|
| Tue, 24 Oct 2017 18:48:21 +0200 |
immler |
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
|
file |
diff |
annotate
|
| Wed, 26 Apr 2017 15:53:35 +0100 |
paulson |
Further new material. The simprule status of some exp and ln identities was reverted.
|
file |
diff |
annotate
|
| Sun, 05 Mar 2017 10:57:51 +0100 |
nipkow |
added numeral_powr_numeral
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:06 +0200 |
haftmann |
eliminated irregular aliasses
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:04 +0200 |
haftmann |
more standardized names
|
file |
diff |
annotate
|
| Fri, 12 Aug 2016 09:57:09 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Fri, 12 Aug 2016 08:20:17 +0200 |
nipkow |
Extracted floorlog and bitlen to separate theory Log_Nat
|
file |
diff |
annotate
|
| Fri, 05 Aug 2016 12:27:51 +0200 |
nipkow |
fixed floor proofs
|
file |
diff |
annotate
|
| Fri, 05 Aug 2016 09:05:03 +0200 |
nipkow |
more lemmas
|
file |
diff |
annotate
|
| Fri, 24 Jun 2016 20:27:57 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2016 16:46:48 +0200 |
immler |
generalized bitlen to floor of log
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| Fri, 26 Feb 2016 11:53:45 +0100 |
immler |
finite precision computation to determine sign for comparison
|
file |
diff |
annotate
|
| Fri, 26 Feb 2016 11:53:45 +0100 |
immler |
positive precision for truncate; fixed precision for approximation of rationals; code for truncate
|
file |
diff |
annotate
|
| Fri, 26 Feb 2016 11:53:42 +0100 |
immler |
compute_real_of_float has not been used as code equation
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
dropped various legacy fact bindings
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 01:28:28 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sun, 27 Dec 2015 21:46:36 +0100 |
wenzelm |
prefer symbols for "floor", "ceiling";
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Tue, 01 Dec 2015 14:09:10 +0000 |
paulson |
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
|
file |
diff |
annotate
|
| Fri, 13 Nov 2015 12:27:13 +0000 |
paulson |
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
|
file |
diff |
annotate
|
| Wed, 11 Nov 2015 17:11:50 +0000 |
paulson |
new conversion theorems for int, nat to float
|
file |
diff |
annotate
|
| Tue, 10 Nov 2015 14:18:41 +0000 |
paulson |
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
|
file |
diff |
annotate
|
| Sat, 08 Aug 2015 10:51:33 +0200 |
haftmann |
direct bootstrap of integer division from natural division
|
file |
diff |
annotate
|
| Thu, 09 Jul 2015 00:40:57 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2015 22:57:34 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 11:03:05 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 14:36:36 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 11 Apr 2015 11:56:40 +0100 |
paulson |
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
|
file |
diff |
annotate
|
| Thu, 09 Apr 2015 09:12:47 +0200 |
haftmann |
conversion between division on nat/int and division in archmedean fields
|
file |
diff |
annotate
|
| Wed, 18 Feb 2015 22:46:47 +0100 |
haftmann |
inlined rules to free user-space from technical names
|
file |
diff |
annotate
|
| Fri, 06 Feb 2015 17:57:03 +0100 |
haftmann |
default abstypes and default abstract equations make technical (no_code) annotation superfluous
|
file |
diff |
annotate
|
| Wed, 12 Nov 2014 17:37:43 +0100 |
immler |
tuned proofs
|
file |
diff |
annotate
|
| Wed, 12 Nov 2014 17:37:43 +0100 |
immler |
quickcheck setup for float, inspired by rat::{exhaustive,full_exhaustive,random}
|
file |
diff |
annotate
|
| Wed, 12 Nov 2014 17:37:43 +0100 |
immler |
truncate intermediate results in horner to improve performance of approximate;
|
file |
diff |
annotate
|
| Wed, 12 Nov 2014 17:36:29 +0100 |
immler |
simplified computations based on round_up by reducing to round_down;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:20:45 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Thu, 30 Oct 2014 21:02:01 +0100 |
haftmann |
more simp rules concerning dvd and even/odd
|
file |
diff |
annotate
|
| Sun, 21 Sep 2014 16:56:11 +0200 |
haftmann |
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
|
file |
diff |
annotate
|
| Mon, 25 Aug 2014 14:24:05 +0200 |
hoelzl |
introduce real_of typeclass for real :: 'a => real
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 12:56:15 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Wed, 11 Jun 2014 14:24:23 +1000 |
Thomas Sewell |
Hypsubst preserves equality hypotheses
|
file |
diff |
annotate
|
| Mon, 28 Apr 2014 17:50:03 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 14 Apr 2014 13:08:17 +0200 |
hoelzl |
added divide_nonneg_nonneg and co; made it a simp rule
|
file |
diff |
annotate
|
| Sat, 12 Apr 2014 17:26:27 +0200 |
nipkow |
made mult_pos_pos a simp rule
|
file |
diff |
annotate
|
| Fri, 11 Apr 2014 13:36:57 +0200 |
nipkow |
made mult_nonneg_nonneg a simp rule
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 09:37:47 +0200 |
hoelzl |
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
|
file |
diff |
annotate
|
| Fri, 04 Apr 2014 17:58:25 +0100 |
paulson |
divide_minus_left divide_minus_right are in field_simps but are not default simprules
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:40:33 +0100 |
blanchet |
renamed 'fun_rel' to 'rel_fun'
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 23:03:50 +0100 |
kuncar |
simplify proofs because of the stronger reflexivity prover
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
monotonicity of rounding and truncating float
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
Float: prevent unnecessary large numbers when adding 0
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
additional definitions and lemmas for Float
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 22:04:23 +0200 |
wenzelm |
tuned proofs -- less guessing;
|
file |
diff |
annotate
|
| Tue, 27 Aug 2013 14:37:56 +0200 |
hoelzl |
renamed typeclass dense_linorder to unbounded_dense_linorder
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 20:02:02 +0100 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
| Fri, 08 Mar 2013 13:21:06 +0100 |
kuncar |
patch Isabelle ditribution to conform to changes regarding the parametricity
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 18:58:20 +0200 |
wenzelm |
discontinued obsolete typedef (open) syntax;
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 17:43:23 +0200 |
wenzelm |
eliminated some remaining uses of typedef with implicit set definition;
|
file |
diff |
annotate
|
| Wed, 16 May 2012 19:17:20 +0200 |
kuncar |
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
|
file |
diff |
annotate
|
| Thu, 26 Apr 2012 14:42:50 +0200 |
hoelzl |
add code equation for real_of_float
|
file |
diff |
annotate
|
| Fri, 20 Apr 2012 11:14:39 +0200 |
hoelzl |
hide code generation facts in the Float theory, they are only exported for Approximation
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 22:13:46 +0200 |
hoelzl |
transfer now handles Let
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 18:24:40 +0200 |
kuncar |
rename no_code to no_abs_code - more appropriate name
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 11:55:30 +0200 |
hoelzl |
use real :: float => real as lifting-morphism so we can directlry use the rep_eq theorems
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 14:29:22 +0200 |
hoelzl |
use lifting to introduce floating point numbers
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 14:29:21 +0200 |
hoelzl |
replace the float datatype by a type with unique representation
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 17:22:17 +0200 |
wenzelm |
tuned proofs, less guesswork;
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 19:21:05 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Sat, 25 Feb 2012 09:07:39 +0100 |
bulwahn |
removing unnecessary assumptions in RealDef;
|
file |
diff |
annotate
|
| Tue, 21 Feb 2012 16:28:18 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 10:47:55 +0100 |
haftmann |
attribute code_abbrev superseedes code_unfold_post
|
file |
diff |
annotate
|
| Tue, 06 Dec 2011 14:29:37 +0100 |
hoelzl |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 14 Nov 2011 18:36:31 +0100 |
hoelzl |
cleaned up float theories; removed duplicate definitions and theorems
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 19:03:41 -0700 |
huffman |
avoid using legacy theorem names
|
file |
diff |
annotate
|
| Wed, 04 May 2011 15:37:39 +0200 |
wenzelm |
proper case_names for int_cases, int_of_nat_induct;
|
file |
diff |
annotate
|
| Wed, 12 Jan 2011 17:14:27 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 19:54:48 +0100 |
hoelzl |
move coercions to appropriate places
|
file |
diff |
annotate
|
| Mon, 06 Sep 2010 15:01:37 +0200 |
hoelzl |
When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
|
file |
diff |
annotate
|
| Sun, 09 May 2010 22:51:11 -0700 |
huffman |
avoid using real-specific versions of generic lemmas
|
file |
diff |
annotate
|
| Tue, 23 Feb 2010 10:37:25 -0800 |
huffman |
moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 14:06:41 +0100 |
haftmann |
separate library theory for type classes combining lattices with various algebraic structures
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 18:29:07 +0100 |
wenzelm |
eliminated some old uses of cumulative prems (!) in proof methods;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 16:27:32 +0200 |
haftmann |
prefer code_inline over code_unfold; use code_unfold_post where appropriate
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 10:54:04 +0200 |
haftmann |
code attributes use common underscore convention
|
file |
diff |
annotate
|
| Mon, 29 Jun 2009 23:29:11 +0200 |
hoelzl |
Implemented taylor series expansion for approximation
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 17:55:47 +0200 |
hoelzl |
Approximation: Implemented argument reduction for cosine. Sinus is now implemented in terms of cosine. Sqrt computes on the entire real numbers
|
file |
diff |
annotate
|
| Wed, 29 Apr 2009 20:19:50 +0200 |
hoelzl |
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
|
file |
diff |
annotate
|
| Wed, 29 Apr 2009 14:20:26 +0200 |
haftmann |
farewell to class recpower
|
file |
diff |
annotate
|
| Wed, 22 Apr 2009 19:09:21 +0200 |
haftmann |
power operation defined generic
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 12:01:57 +0100 |
nipkow |
removed redundant lemmas
|
file |
diff |
annotate
|
| Thu, 26 Feb 2009 20:56:59 +0100 |
wenzelm |
standard headers;
|
file |
diff |
annotate
|
| Sat, 21 Feb 2009 09:58:26 +0100 |
nipkow |
removed redundant thms
|
file |
diff |
annotate
|
| Wed, 18 Feb 2009 20:53:58 -0800 |
huffman |
add header
|
file |
diff |
annotate
|
| Thu, 05 Feb 2009 11:45:15 +0100 |
hoelzl |
Added new Float theory and moved old Library/Float.thy to ComputeFloat
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:29:16 +0100 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
file |
diff |
annotate
|
| Tue, 09 Dec 2008 22:13:16 -0800 |
huffman |
move all neg-related lemmas to NatBin; make type of neg specific to int
|
file |
diff |
annotate
|