| Thu, 10 Apr 2014 17:48:18 +0200 |
setup for Transfer and Lifting from BNF; tuned thm names
|
file | diff | annotate |
| Thu, 10 Apr 2014 17:48:15 +0200 |
more appropriate name (Lifting.invariant -> eq_onp)
|
file | diff | annotate |
| Thu, 10 Apr 2014 17:48:14 +0200 |
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
|
file | diff | annotate |
| Fri, 21 Mar 2014 20:33:56 +0100 |
more qualified names;
|
file | diff | annotate |
| Thu, 06 Mar 2014 15:40:33 +0100 |
renamed 'fun_rel' to 'rel_fun'
|
file | diff | annotate |
| Thu, 27 Feb 2014 13:52:33 +0100 |
hide Lifting.invariant from a user completely
|
file | diff | annotate |
| Tue, 25 Feb 2014 19:07:40 +0100 |
new rule for making rsp theorem more readable
|
file | diff | annotate |
| Tue, 25 Feb 2014 15:02:54 +0100 |
the rules are not needed due to 1726f46d2aa8
|
file | diff | annotate |
| Tue, 25 Feb 2014 15:02:19 +0100 |
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
|
file | diff | annotate |
| Mon, 24 Feb 2014 18:12:41 +0100 |
more robust registration of code equations
|
file | diff | annotate |
| Mon, 24 Feb 2014 18:12:40 +0100 |
be consistent and produce always rep_eq with =
|
file | diff | annotate |
| Thu, 20 Feb 2014 16:56:33 +0100 |
refactoring; generate rep_eq always, not only when it would be accepted by the code generator
|
file | diff | annotate |
| Thu, 20 Feb 2014 16:56:32 +0100 |
refactoring
|
file | diff | annotate |
| Thu, 20 Feb 2014 16:56:32 +0100 |
the rule is not needed due to 1726f46d2aa8
|
file | diff | annotate |
| Tue, 18 Feb 2014 23:03:47 +0100 |
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
|
file | diff | annotate |
| Sat, 11 Jan 2014 23:35:05 +0100 |
more accurate context;
|
file | diff | annotate |
| Wed, 08 Jan 2014 17:00:03 +0100 |
typo
|
file | diff | annotate |
| Sat, 14 Dec 2013 17:28:05 +0100 |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file | diff | annotate |
| Mon, 14 Oct 2013 15:01:41 +0200 |
update documentation of important public ML functions in Lifting
|
file | diff | annotate |
| Fri, 27 Sep 2013 14:43:26 +0200 |
allow to specify multiple parametricity transfer rules in lift_definition
|
file | diff | annotate |
| Mon, 16 Sep 2013 15:30:17 +0200 |
restoring Transfer/Lifting context
|
file | diff | annotate |
| Mon, 26 Aug 2013 16:13:20 +0200 |
prefer Binding.name_of over Binding.print -- the latter leads to funny quotes and markup within the constructed term;
|
file | diff | annotate |
| Mon, 26 Aug 2013 15:45:51 +0200 |
proper context;
|
file | diff | annotate |
| Wed, 15 May 2013 12:10:39 +0200 |
stronger reflexivity prover
|
file | diff | annotate |
| Mon, 13 May 2013 15:22:19 +0200 |
typo
|
file | diff | annotate |
| Fri, 10 May 2013 19:41:23 +0200 |
don't apply an unnecessary morphism
|
file | diff | annotate |
| Fri, 08 Mar 2013 13:14:23 +0100 |
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
|
file | diff | annotate |
| Thu, 28 Feb 2013 16:54:52 +0100 |
just one HOLogic.Trueprop_conv, with regular exception CTERM;
|
file | diff | annotate |
| Wed, 24 Oct 2012 18:43:25 +0200 |
transfer package: more flexible handling of equality relations using is_equality predicate
|
file | diff | annotate |
| Wed, 17 Oct 2012 00:16:31 +0200 |
don't be so aggressive when expanding a transfer rule relation; rewrite only the relational part of the rule
|
file | diff | annotate |
| Thu, 27 Sep 2012 20:30:32 +0200 |
mk_readable_rsp_thm_eq is more robust now
|
file | diff | annotate |
| Thu, 27 Sep 2012 20:30:30 +0200 |
new get function for non-symmetric relator_eq & tuned
|
file | diff | annotate |
| Tue, 29 May 2012 19:13:02 +0200 |
don't be so aggressive during unfolding id and o
|
file | diff | annotate |
| Thu, 24 May 2012 14:20:23 +0200 |
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
|
file | diff | annotate |
| Mon, 21 May 2012 16:36:48 +0200 |
quot_del attribute, it allows us to deregister quotient types
|
file | diff | annotate |
| Wed, 16 May 2012 19:17:20 +0200 |
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 |
| Wed, 02 May 2012 18:26:10 +0200 |
documentation of the Lifting package on the ML level & tuned
|
file | diff | annotate |
| Mon, 23 Apr 2012 18:42:03 +0200 |
added useful Trueprop_conv
|
file | diff | annotate |
| Mon, 23 Apr 2012 17:18:18 +0200 |
move MRSL to a separate file
|
file | diff | annotate |
| Sun, 22 Apr 2012 16:53:24 +0200 |
fix bug caused by misunderstanding of operator precedences (cf. cb44d09d9d22)
|
file | diff | annotate |
| Fri, 20 Apr 2012 18:29:21 +0200 |
hide the invariant constant for relators: invariant_commute infrastracture
|
file | diff | annotate |
| Thu, 19 Apr 2012 17:31:34 +0200 |
use tnames for bound variables in rsp thms
|
file | diff | annotate |
| Wed, 18 Apr 2012 23:57:44 +0200 |
setup_lifting: no_code switch and supoport for quotient theorems
|
file | diff | annotate |
| Wed, 18 Apr 2012 17:04:03 +0200 |
Lifting: generate more thms & note them & tuned
|
file | diff | annotate |
| Tue, 17 Apr 2012 14:56:38 +0200 |
go back to the explicit compisition of quotient theorems
|
file | diff | annotate |
| Tue, 17 Apr 2012 11:03:08 +0200 |
add theory data for relator identity rules;
|
file | diff | annotate |
| Fri, 06 Apr 2012 14:39:27 +0200 |
more robust generation of quotient rules using tactics
|
file | diff | annotate |
| Fri, 06 Apr 2012 09:35:47 +0200 |
correct plumbing of proof contexts, so that force_rty_type won't generalize more type variables than it should
|
file | diff | annotate |
| Thu, 05 Apr 2012 23:22:54 +0200 |
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
|
file | diff | annotate |
| Thu, 05 Apr 2012 12:18:06 +0200 |
lift_definition declares transfer_rule attribute
|
file | diff | annotate |
| Wed, 04 Apr 2012 17:51:12 +0200 |
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
|
file | diff | annotate |
| Wed, 04 Apr 2012 13:42:01 +0200 |
lift_definition command generates transfer rule
|
file | diff | annotate |
| Tue, 03 Apr 2012 16:26:48 +0200 |
new package Lifting - initial commit
|
file | diff | annotate |