added lemmas and transfer rules

ran isabelle update_op on all sources

a more general relator domain rule for the function type

more lemmas

--HG--
extra : rebase_source : f52072de0fdc0fac0b2505569668d385d1ffe93d

bundle lifting_syntax;

eliminated use of empty "assms";

make predicator a first-class bnf citizen

add various lemmas

isabelle update_cartouches;

more transfer rules

add parametricity rule for Ex1

add intro and elim rules for right_total

tuning

Add plugin to generate transfer theorem for primrec and primcorec

renamed theory file

--HG--
rename : src/HOL/Basic_BNF_Least_Fixpoints.thy => src/HOL/Basic_BNF_LFPs.thy

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

more complete fp_sugars for sum and prod;
tuned;
removed theorem duplicates;
removed obsolete Lifting_{Option,Product,Sum} theories

modernized header uniformly as section;

modernized setup;

generate 'corec_transfer' for codatatypes

generate 'ctor_rec_transfer' for datatypes

typo

tweaked setup for datatype realizer

renamed BNF theories

--HG--
rename : src/HOL/BNF_Comp.thy => src/HOL/BNF_Composition.thy
rename : src/HOL/BNF_FP_Base.thy => src/HOL/BNF_Fixpoint_Base.thy
rename : src/HOL/BNF_GFP.thy => src/HOL/BNF_Greatest_Fixpoint.thy
rename : src/HOL/BNF_LFP.thy => src/HOL/BNF_Least_Fixpoint.thy

add parametricity lemmas

merged two small theory files

fixed postprocessing of 'coinduct' formula to obtain right property format (without needless hypotheses)

predicator simplification rules: support also partially specialized types e.g. 'a * nat

qualify name

bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced

setup for Transfer and Lifting from BNF; tuned thm names

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

abstract Domainp in relator_domain rules => more natural statement of the rule

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

killed a few 'metis' calls

renamed 'fun_rel' to 'rel_fun'

load Metis a little later

transfer domain rule for special case of functions - was missing

renamed 'nat_{case,rec}' to '{case,rec}_nat'

rationalized lemmas

new parametricity rules and useful lemmas

add lemmas

add lemmas

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

implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction

implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>

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

try to detect assumptions of transfer rules that are in a shape of a transfer rule

fixing transfer tactic - unfold fully identity relation by using relator_eq

abandoned theory Plain

--HG--
extra : rebase_source : 6f5a395a55e8879386d1f79ab252c6fc2aca7dc5

transfer package: more flexible handling of equality relations using is_equality predicate

prefer ML_file over old uses;

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

add transfer rules for nat_rec and funpow

implement transfer tactic with more scalable forward proof methods

tuned precedence order of transfer rules

--HG--
extra : rebase_source : fac335be28930b101ac84bd8fb7f88f98bdc10f5

new example theory for quotient/transfer

enable variant of transfer method that proves an implication instead of an equivalence

add transfer rule for nat_case

--HG--
extra : transplant_source : %26%5B%3A%D7%9B%FA%D9%B6%E95C%04%0E%83%9C%A5%8C%DC8%E2

uniform naming scheme for transfer rules

rename 'correspondence' method to 'transfer_prover'

add secondary transfer rule for universal quantifiers on non-bi-total relations

add transfer rule for 'id'

make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules

add transfer rule for Let

make transfer method more deterministic by using SOLVED' on some subgoals

--HG--
extra : rebase_source : 3ed8e05dc4c7ebb812ea7cdcdd0b9bbe2de94ebd

add theory data for relator identity rules;
preprocess transfer rules generated by lift_definition using relator rules

--HG--
extra : transplant_source : %0C%BB%B3H%AB%A7%25/H%DF%AE%0E%AF%8B%F83-%9AK%06

add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer

new transfer proof method