| Fri, 10 Jan 2014 15:22:23 +0100 |
blanchet |
repair 'exhaustive' feature for one-constructor types
|
file |
diff |
annotate
|
| Fri, 10 Jan 2014 15:11:00 +0100 |
blanchet |
pass right rhs as code rhs
|
file |
diff |
annotate
|
| Fri, 10 Jan 2014 14:58:31 +0100 |
blanchet |
use correct default for exclude rules to avoid weird tactic failures
|
file |
diff |
annotate
|
| Fri, 10 Jan 2014 14:47:26 +0100 |
blanchet |
tuning (no need for |-> here)
|
file |
diff |
annotate
|
| Fri, 10 Jan 2014 14:39:37 +0100 |
blanchet |
fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
|
file |
diff |
annotate
|
| Fri, 10 Jan 2014 14:39:37 +0100 |
blanchet |
only destruct cases equipped with the right stuff (in particular, 'sel_split')
|
file |
diff |
annotate
|
| Fri, 10 Jan 2014 14:39:37 +0100 |
blanchet |
generate 'disc_iff' for all discriminators
|
file |
diff |
annotate
|
| Fri, 10 Jan 2014 14:39:37 +0100 |
blanchet |
use 'disc_iff' as simp rules whenever possible + clean up '= True', '= False', etc.
|
file |
diff |
annotate
|
| Fri, 10 Jan 2014 14:39:37 +0100 |
blanchet |
exhaustive rules like '(False ==> P) ==> P ==> P' are now filtered out as trivial
|
file |
diff |
annotate
|
| Fri, 10 Jan 2014 09:48:11 +0100 |
blanchet |
fixed 'disc_iff' tactic in the case where different equations use different variable names for the function arguments
|
file |
diff |
annotate
|
| Thu, 09 Jan 2014 19:10:35 +0100 |
panny |
do not use wrong constructor in auto-generated proof goal
|
file |
diff |
annotate
|
| Thu, 09 Jan 2014 17:13:05 +0100 |
blanchet |
tuned error message
|
file |
diff |
annotate
|
| Thu, 09 Jan 2014 16:40:50 +0100 |
blanchet |
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
|
file |
diff |
annotate
|
| Thu, 09 Jan 2014 15:49:19 +0100 |
blanchet |
strengthened tactics w.r.t. 'lets' and tuples
|
file |
diff |
annotate
|
| Thu, 09 Jan 2014 15:07:25 +0100 |
blanchet |
for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
|
file |
diff |
annotate
|
| Wed, 08 Jan 2014 17:26:42 +0100 |
panny |
match order of generated theorems to user input;
|
file |
diff |
annotate
|
| Fri, 03 Jan 2014 14:38:13 +0100 |
blanchet |
proper name generation to avoid clash with 'P' in user specification
|
file |
diff |
annotate
|
| Fri, 03 Jan 2014 14:14:16 +0100 |
blanchet |
more SML-ish (less Haskell-ish) naming convention
|
file |
diff |
annotate
|
| Fri, 03 Jan 2014 14:04:37 +0100 |
blanchet |
strengthened tactic
|
file |
diff |
annotate
|
| Fri, 03 Jan 2014 13:55:34 +0100 |
blanchet |
refactoring
|
file |
diff |
annotate
|
| Fri, 03 Jan 2014 11:26:44 +0100 |
blanchet |
instantiate schematics as projections to avoid HOU trouble
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 23:44:31 +0100 |
blanchet |
avoid schematic variable in goal, which sometimes gets instantiated by tactic
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 20:51:09 +0100 |
blanchet |
made tactic handle corner cases, where some of the 'disc' properties are missing, correctly
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 09:50:22 +0100 |
blanchet |
consider code as exhaustive
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 09:50:22 +0100 |
blanchet |
proper handling of corner case, take 2
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 09:50:22 +0100 |
blanchet |
robustness
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 09:50:22 +0100 |
blanchet |
properly synchronize parallel lists
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 09:50:22 +0100 |
blanchet |
graceful handling of one-constructor case
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 09:50:22 +0100 |
blanchet |
made tactic handle gracefully the case of missing constructors
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 09:50:22 +0100 |
blanchet |
removed 'nchotomy' property
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 09:50:22 +0100 |
blanchet |
don't generate any proof obligation for implicit (de facto) exclusiveness
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 09:50:22 +0100 |
blanchet |
detect syntactic exhaustiveness
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 09:50:22 +0100 |
blanchet |
internally allow different values for 'exhaustive' for different constructors
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 09:50:22 +0100 |
blanchet |
internally allow different values for 'sequential' for different constructors
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 09:50:22 +0100 |
blanchet |
use same name for feature internally as in user interface, to facilitate grepping
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 09:50:22 +0100 |
blanchet |
generate 'disc_iff' property in 'primcorec'
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 09:50:22 +0100 |
blanchet |
added tactic to prove 'disc_iff' properties in 'primcorec'
|
file |
diff |
annotate
|
| Tue, 31 Dec 2013 14:29:16 +0100 |
wenzelm |
proper context for norm_hhf and derived operations;
|
file |
diff |
annotate
|
| Sat, 21 Dec 2013 09:44:30 +0100 |
blanchet |
generate exhaust from nchotomy
|
file |
diff |
annotate
|
| Sat, 21 Dec 2013 09:44:28 +0100 |
blanchet |
renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package)
|
file |
diff |
annotate
|
| Fri, 20 Dec 2013 11:34:07 +0100 |
blanchet |
note manually proved exclusiveness property
|
file |
diff |
annotate
|
| Fri, 20 Dec 2013 11:12:51 +0100 |
blanchet |
note exhaust proof obligation
|
file |
diff |
annotate
|
| Thu, 19 Dec 2013 21:49:30 +0100 |
blanchet |
implemented 'exhaustive' option in tactic
|
file |
diff |
annotate
|
| Wed, 18 Dec 2013 14:50:25 +0100 |
panny |
pass down user input in more cases in order to preserve "let"s etc.
|
file |
diff |
annotate
|
| Wed, 18 Dec 2013 14:06:34 +0100 |
panny |
pass auto-proved exhaustiveness properties to tactic;
|
file |
diff |
annotate
|
| Mon, 02 Dec 2013 19:49:34 +0100 |
panny |
generate "code" theorems for incomplete definitions
|
file |
diff |
annotate
|
| Sun, 01 Dec 2013 19:32:57 +0100 |
panny |
more work towards "exhaustive"
|
file |
diff |
annotate
|
| Mon, 25 Nov 2013 20:25:22 +0100 |
panny |
prevent exception when equations for a function are missing;
|
file |
diff |
annotate
|
| Wed, 06 Nov 2013 13:00:45 +0100 |
blanchet |
removed dead code
|
file |
diff |
annotate
|
| Wed, 06 Nov 2013 12:47:50 +0100 |
blanchet |
take out possibility of moving corecursive calls past constructors -- this doesn't work in the general case
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 16:53:40 +0100 |
blanchet |
avoid subtle failure in the presence of top sort
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 16:47:10 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 04 Nov 2013 16:53:43 +0100 |
blanchet |
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
|
file |
diff |
annotate
| base
|