extension of lift_bnf to support quotient types

more specific keyword kinds;

isabelle update -u path_cartouches;

ran isabelle update_op on all sources

tuned op's

bundle lifting_syntax;

eliminated use of empty "assms";

isabelle update_cartouches -c -t;

add various lemmas

isabelle update_cartouches;

BNF relators preserve reflexivity

Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype

modernized header uniformly as section;

modernized setup;

named interpretations

introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales

updated to named_theorems;

merged two small theory files

setup for Transfer and Lifting from BNF; tuned thm names

--HG--
rename : src/HOL/Tools/transfer.ML => src/HOL/Tools/Transfer/transfer.ML

more appropriate name (Lifting.invariant -> eq_onp)

left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)

tuned

renamed 'fun_rel' to 'rel_fun'

new rule for making rsp theorem more readable

rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user

refactoring; generate rep_eq always, not only when it would be accepted by the code generator

less flex-flex pairs

implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules

move BNF_LFP up the dependency chain

new parametricity rules and useful lemmas

add lemmas

add lemmas

restoring Transfer/Lifting context

use only one data slot; rename print_quotmaps to print_quot_maps; tuned

remove OP

introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local

more reflexivity rules (for OO)

reflexivity rules for the function type and equality

stronger reflexivity prover

better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal

lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided

abandoned theory Plain

--HG--
extra : rebase_source : 6f5a395a55e8879386d1f79ab252c6fc2aca7dc5

prefer ML_file over old uses;

prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule

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

infrastructure that makes possible to prove that a relation is reflexive

lifting package produces abs_eq_iff rules for total quotients

use a quot_map theorem attribute instead of the complicated map attribute

move MRSL to a separate file

move alternative definition lemmas into Lifting.thy;
simplify proof of Quotient_compose

tuned proofs

generate abs_induct rules for quotient types

--HG--
extra : rebase_source : 9656ecaf26f12a5d2b81ce9d2d260be2c75c910b

Lifting: generate more thms & note them & tuned

move constant 'Respects' into Lifting.thy;
add quantifier transfer rules for quotients

add lemma Quotient_abs_induct

more usage of context blocks

use context block

lifting_setup generates transfer rule for rep of typedefs

--HG--
extra : rebase_source : d0ceef760c5bb5d2f87dc38f6f2426ef0ce511f1

use context block to organize typedef lifting theorems

--HG--
extra : rebase_source : eb93bd18a5176c8cde5ba30ac6f536d2644e011c

tuned the setup of lifting; generate transfer rules for typedef and Quotient thms

leave Lifting prefix

add transfer lemmas for quotients

support non-open typedefs; define cr_rel in terms of a rep function for typedefs

add lemmas for generating transfer rules for typedefs

update keywords file

lift_definition command generates transfer rule

new transfer proof method

new package Lifting - initial commit