de-applying (mostly Quotient)

de-applying

ran isabelle update_op on all sources

more symbols;

bundle lifting_syntax;

isabelle update_cartouches -c -t;

isabelle update_cartouches;

named_theorems: multiple args;

modernized header uniformly as section;

updated to named_theorems;
modernized setup;

enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions

--HG--
extra : rebase_source : 4103bf02b2df95e1e84808f766f131292beef893

renamed 'fun_rel' to 'rel_fun'

prefer ephemeral interpretation over interpretation in proof contexts;
prefer context begin ... end blocks for often-occuring assumptions;
slightly more complete interpretations into abstract algebraic structures for gcd/lcm

rationalize imports

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

abandoned theory Plain

--HG--
extra : rebase_source : 6f5a395a55e8879386d1f79ab252c6fc2aca7dc5

prefer ML_file over old uses;

move definition of set_rel into Library/Quotient_Set.thy

tuned lemmas (v)image_id;
removed duplicate of vimage_id

--HG--
extra : rebase_source : 9178db2e0f900cdeab723f13b8c0d5fc45786a95

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

centralized enriched_type declaration, thanks to in-situ available Isar commands

--HG--
extra : rebase_source : ea8947ffa8bb301d674c472c3427994b31c4c458

connect the Quotient package to the Lifting package

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

new package Lifting - initial commit

dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"

hide invariant constant

declare command keywords via theory header, including strict checking outside Pure;

declare minor keywords via theory header;

simplified use of tacticals;

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

store the relational theorem for every relator

respectfulness theorem has to be proved if a new constant is lifted by quotient_definition

treatment of type constructor `set`

Quotient_Info stores only relation maps

added a specific tactic and method that deal with partial equivalence relations

more conventional file name;

--HG--
rename : src/HOL/Tools/Quotient/quotient_typ.ML => src/HOL/Tools/Quotient/quotient_type.ML

tuned proofs

avoid intermixing set and predicates; dropped lemmas mem_rsp and mem_prs (now in Quotient_Set.thy)

Quotient Package: some infrastructure for lifting inside sets

avoid Collect_def in proof

Quotient Package: make quotient_type work with separate set type

simplified/unified method_setup/attribute_setup;

use old Skolemizer for Metis call that requires high unification bound (around 100) with the new Skolemizer

tuned headers;

more standard package setup;

reorienting iff in Quotient_rel prevents simplifier looping;
lemma QuotientI;
tuned theory text

moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
moved generic definitions about relations from Quotient.thy to Predicate;
consistent use of R rather than E for relations;
more natural deduction rules

generalized type

map_fun combinator in theory Fun

type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions

Quotient package: partial equivalence introduction

remove needless Metis facts

move Metis into Plain

--HG--
rename : src/HOL/Tools/Sledgehammer/metis_reconstruct.ML => src/HOL/Tools/Metis/metis_reconstruct.ML
rename : src/HOL/Tools/Sledgehammer/metis_tactics.ML => src/HOL/Tools/Metis/metis_tactics.ML
rename : src/HOL/Tools/Sledgehammer/metis_translate.ML => src/HOL/Tools/Metis/metis_translate.ML

quotient package: respectfulness and preservation of identity.

renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI

expand_fun_eq -> ext_iff
expand_set_eq -> set_ext_iff
Naming in line now with multisets

Quotient Package: added respectfulness and preservation lemmas for mem.

quotient package: lemmas to be lifted and descended can be pre-simplified

Quotient Package / lemma for regularization of bex1_rel for equivalence relations

deleted duplicate lemma

use file names relative to master directory of theory source -- Proof General can now handle that due to the ThyLoad.add_path deception (cf. 3ceccd415145);

separated the lifting and descending procedures in the quotient package

Quotient package reverse lifting

Quotient package now uses Partial Equivalence instead place of equivalence

Let rsp and prs in fun_rel/fun_map format

fun_rel introduction and list_rel elimination for quotient package

respectfullness and preservation of function composition

add If respectfullness and preservation to Quotient package database

Changed the type of Quot_True, so that it is an HOL constant.

renamed "ATP_Linkup" theory to "Sledgehammer"

--HG--
rename : src/HOL/ATP_Linkup.thy => src/HOL/Sledgehammer.thy

proper header and subsection headings

quote the constant and theorem name with @{text}

Initial version of HOL quotient package.