#
a794106c |
|
09-Dec-2019 |
traytel <none@none> |
extension of lift_bnf to support quotient types
|
#
6ce8882b |
|
14-Mar-2019 |
wenzelm <none@none> |
more specific keyword kinds;
|
#
e60cf64d |
|
06-Jan-2019 |
wenzelm <none@none> |
isabelle update -u path_cartouches;
|
#
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
#
e329cd69 |
|
20-Dec-2017 |
nipkow <none@none> |
tuned op's
|
#
48473ab7 |
|
22-Jun-2016 |
wenzelm <none@none> |
bundle lifting_syntax;
|
#
1daf8189 |
|
13-May-2016 |
wenzelm <none@none> |
eliminated use of empty "assms";
|
#
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
3487f527 |
|
11-Nov-2015 |
Andreas Lochbihler <none@none> |
add various lemmas
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
99c387f7 |
|
16-Mar-2015 |
traytel <none@none> |
BNF relators preserve reflexivity
|
#
75b699bc |
|
05-Dec-2014 |
kuncar <none@none> |
Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
8049c47b |
|
29-Oct-2014 |
wenzelm <none@none> |
modernized setup;
|
#
625d35eb |
|
04-Sep-2014 |
blanchet <none@none> |
named interpretations
|
#
3a5bbb8e |
|
03-Sep-2014 |
blanchet <none@none> |
introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
|
#
9fb2f336 |
|
16-Aug-2014 |
wenzelm <none@none> |
updated to named_theorems;
|
#
3816e708 |
|
27-Jun-2014 |
blanchet <none@none> |
merged two small theory files
|
#
e9e8c934 |
|
10-Apr-2014 |
kuncar <none@none> |
setup for Transfer and Lifting from BNF; tuned thm names --HG-- rename : src/HOL/Tools/transfer.ML => src/HOL/Tools/Transfer/transfer.ML
|
#
128e121b |
|
10-Apr-2014 |
kuncar <none@none> |
more appropriate name (Lifting.invariant -> eq_onp)
|
#
845456ae |
|
10-Apr-2014 |
kuncar <none@none> |
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
|
#
2a4f822d |
|
10-Apr-2014 |
kuncar <none@none> |
tuned
|
#
b9ba5739 |
|
06-Mar-2014 |
blanchet <none@none> |
renamed 'fun_rel' to 'rel_fun'
|
#
8a230f2e |
|
25-Feb-2014 |
kuncar <none@none> |
new rule for making rsp theorem more readable
|
#
1247c4d5 |
|
25-Feb-2014 |
kuncar <none@none> |
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
|
#
e7724912 |
|
20-Feb-2014 |
kuncar <none@none> |
refactoring; generate rep_eq always, not only when it would be accepted by the code generator
|
#
d149e4f0 |
|
20-Feb-2014 |
noschinl <none@none> |
less flex-flex pairs
|
#
93867854 |
|
18-Feb-2014 |
kuncar <none@none> |
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
|
#
e3355c3e |
|
20-Jan-2014 |
blanchet <none@none> |
move BNF_LFP up the dependency chain
|
#
17f4af0c |
|
27-Sep-2013 |
kuncar <none@none> |
new parametricity rules and useful lemmas
|
#
d20e79f0 |
|
27-Sep-2013 |
Andreas Lochbihler <none@none> |
add lemmas
|
#
8c550eac |
|
26-Sep-2013 |
Andreas Lochbihler <none@none> |
add lemmas
|
#
308ade1d |
|
16-Sep-2013 |
kuncar <none@none> |
restoring Transfer/Lifting context
|
#
9e756f50 |
|
28-Aug-2013 |
kuncar <none@none> |
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
|
#
3ffa26d0 |
|
22-Aug-2013 |
kuncar <none@none> |
remove OP
|
#
a265459b |
|
13-Aug-2013 |
kuncar <none@none> |
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
|
#
3f8f4f71 |
|
05-Jun-2013 |
kuncar <none@none> |
more reflexivity rules (for OO)
|
#
d23678bc |
|
16-May-2013 |
kuncar <none@none> |
reflexivity rules for the function type and equality
|
#
01e7a4f2 |
|
14-May-2013 |
kuncar <none@none> |
stronger reflexivity prover
|
#
8c36fedb |
|
13-May-2013 |
kuncar <none@none> |
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
|
#
f2065d73 |
|
08-Mar-2013 |
kuncar <none@none> |
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
|
#
fa22b8b3 |
|
13-Feb-2013 |
haftmann <none@none> |
abandoned theory Plain --HG-- extra : rebase_source : 6f5a395a55e8879386d1f79ab252c6fc2aca7dc5
|
#
e3227796 |
|
22-Aug-2012 |
wenzelm <none@none> |
prefer ML_file over old uses;
|
#
dd23141d |
|
24-May-2012 |
kuncar <none@none> |
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
|
#
7bae30d6 |
|
16-May-2012 |
kuncar <none@none> |
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
|
#
7e12d58a |
|
16-May-2012 |
kuncar <none@none> |
infrastructure that makes possible to prove that a relation is reflexive
|
#
4ede7bb5 |
|
04-May-2012 |
huffman <none@none> |
lifting package produces abs_eq_iff rules for total quotients
|
#
09bb30ca |
|
25-Apr-2012 |
kuncar <none@none> |
use a quot_map theorem attribute instead of the complicated map attribute
|
#
a7ace5a5 |
|
23-Apr-2012 |
kuncar <none@none> |
move MRSL to a separate file
|
#
efec17bb |
|
21-Apr-2012 |
huffman <none@none> |
move alternative definition lemmas into Lifting.thy; simplify proof of Quotient_compose
|
#
b4156774 |
|
21-Apr-2012 |
huffman <none@none> |
tuned proofs
|
#
4a7f2f4a |
|
19-Apr-2012 |
huffman <none@none> |
generate abs_induct rules for quotient types --HG-- extra : rebase_source : 9656ecaf26f12a5d2b81ce9d2d260be2c75c910b
|
#
3e3d1772 |
|
18-Apr-2012 |
kuncar <none@none> |
Lifting: generate more thms & note them & tuned
|
#
b5a49119 |
|
18-Apr-2012 |
huffman <none@none> |
move constant 'Respects' into Lifting.thy; add quantifier transfer rules for quotients
|
#
329d643a |
|
18-Apr-2012 |
huffman <none@none> |
add lemma Quotient_abs_induct
|
#
2235729e |
|
18-Apr-2012 |
huffman <none@none> |
more usage of context blocks
|
#
8923a585 |
|
18-Apr-2012 |
huffman <none@none> |
use context block
|
#
f8111acb |
|
17-Apr-2012 |
huffman <none@none> |
lifting_setup generates transfer rule for rep of typedefs --HG-- extra : rebase_source : d0ceef760c5bb5d2f87dc38f6f2426ef0ce511f1
|
#
6b43d349 |
|
18-Apr-2012 |
huffman <none@none> |
use context block to organize typedef lifting theorems --HG-- extra : rebase_source : eb93bd18a5176c8cde5ba30ac6f536d2644e011c
|
#
b07286d9 |
|
17-Apr-2012 |
kuncar <none@none> |
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
|
#
84bbd105 |
|
16-Apr-2012 |
kuncar <none@none> |
leave Lifting prefix
|
#
2a412f5e |
|
05-Apr-2012 |
huffman <none@none> |
add transfer lemmas for quotients
|
#
fe6190cb |
|
04-Apr-2012 |
kuncar <none@none> |
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
|
#
5f6482df |
|
04-Apr-2012 |
huffman <none@none> |
add lemmas for generating transfer rules for typedefs
|
#
e7cfcd64 |
|
03-Apr-2012 |
huffman <none@none> |
update keywords file
|
#
d5289941 |
|
04-Apr-2012 |
huffman <none@none> |
lift_definition command generates transfer rule
|
#
f0c3385b |
|
03-Apr-2012 |
huffman <none@none> |
new transfer proof method
|
#
a2076df5 |
|
03-Apr-2012 |
kuncar <none@none> |
new package Lifting - initial commit
|