misspelled name
alternative names of morphisms in the definition of a quotient type can be specified
merged
updated documentation for the quotient package
removed outdated comment
removed outdated comment moved back and updated (at the direct request of Christian Urban)
the note about morphisms moved in the description part
merged
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
context/theory parametres tuned
make ctxt the first parameter
merged
added an example file with lifting of constants with contravariant and co/contravariant types
added dependencies
Quotient_Info stores only relation maps
support phantom types as quotient types
fix Quotient_Examples
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
store the quotient theorem for every quotient
store the relational theorem for every relator
simplified code of generation of aggregate relations
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
fix example files
update etc/isar-keywords.el
resolve invariant constant name clash
updated comment
hide invariant constant
use Thm.transfer for thms stored in generic context data storage
merged
tuned proof - no smt call
merged
merged
tuned comment
note a code eqn in quotient_def
merged
use qualified names for rsp and rep_eq theorems in quotient_def
new package Lifting - initial commit
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
connect the Quotient package to the Lifting package
make Quotient_Def.lift_raw_const working again
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
leave Lifting prefix
note the Quotient theorem in quotient_type
go back to the explicit compisition of quotient theorems
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
Lifting: generate more thms & note them & tuned
setup_lifting: no_code switch and supoport for quotient theorems
create thm names correctly
use tnames for bound variables in rsp thms
rename no_code to no_abs_code - more appropriate name
hide the invariant constant for relators: invariant_commute infrastracture
move MRSL to a separate file
added useful Trueprop_conv
CONTRIBUTORS
use a quot_map theorem attribute instead of the complicated map attribute
support Quotient map theorems with invariant parameters
tuned; don't generate abs code if quotient_type is used
added a basic sanity check for quot_map
documentation for the Lifting package in Isar-ref
documentation of the Lifting package on the ML level & tuned
resolved maxidx bug
infrastructure that makes possible to prove that a relation is reflexive
remove the generation of a code certificate from the Quotient package (mainly from quotient_def), because it's in lift_definition now
don't generate code in Word because it breaks the current code setup
note Quotient theorem for typedefs in setup_lifting
quot_del attribute, it allows us to deregister quotient types
use quot_del instead of ML code in Rat.thy
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
drop the feature that more than one quotient type can be defined by quotient_type -> it causes problems
merged
don't be so aggressive during unfolding id and o
more relation operations expressed by Finite_Set.fold
more set operations expressed by Finite_Set.fold
a couple of additions to RBT formalization to allow us to implement RBT_Set
use lifting/transfer formalization of RBT from Lift_RBT
implementation of sets by RBT trees for the code generator
add testing file for RBT_Set
Remove Lift_RBT.thy, it's in HOL/Library/RBT.thy now
new get function for non-symmetric relator_eq & tuned
mk_readable_rsp_thm_eq is more robust now
rename Set.project to Set.filter - more appropriate name
use Set.filter instead of Finite_Set.filter, which is removed then
don't be so aggressive when expanding a transfer rule relation; rewrite only the relational part of the rule
new theorem
tuned proofs
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
don't include Quotient_Option - workaround to a transfer bug
new theorems
generate correct correspondence relation name
simplified code
generate correct names
add option_fold
quot_thm_crel
generate a parameterized correspondence relation
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
NEWS
update isar-ref for Quotient and Lifting package
more update on Lifting in isar-ref
restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
delete also predicates on relations when hiding an implementation of an abstract type