more de-applying

tuned

By Andrei Popescu based on an initial version by Kasper F. Brandt

ran isabelle update_op on all sources

added 'mlex_iff' lemma and simplified proof

dropped aliasses

tuned;

tuned proofs;

misc tuning and modernization;

misc tuning and modernization;

proper document source;
tuned proofs;

misc tuning and modernization;

Moved material from AFP/Randomised_Social_Choice to distribution

a quasi-recursive characterization of the multiset order (by Christian Sternagel)

--HG--
extra : rebase_source : ea7549c1d4957cffe917d57e17b983992bba0524

prefer symbols for "Union", "Inter";

discontinued ASCII replacement syntax <*>;

isabelle update_cartouches -c -t;

prod_case as canonical name for product type eliminator

fewer aliases for toplevel theorem statements;

isabelle update_cartouches;

New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.

new lemma

prefer local fixes;

modernized header uniformly as section;

more bibtex entries;
more antiquotations;

move size hooks together, with new one preceding old one and sharing same theory data

use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges

elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION

normalising simp rules for compound operators

renamed 'map_pair' to 'map_prod'

folded 'Wellfounded_More_FP' into 'Wellfounded'

qualifed popular user space names

adjusting proofs

prefer ML_file over old uses;

renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")

tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set

tuned simpset

moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy

--HG--
extra : rebase_source : ed15629634477aff0a8efea30547f496c70907ad

moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy

adding code_unfold to make measure executable

reverting 46c2c96f5d92 as it only provides mostly non-terminating executions for generated code

adding very basic code generation to Wellfounded theory

pred_subset_eq and SUP_UN_eq2 are now standard pred_set_conv rules

adjusted to set/pred distinction by means of type constructor `set`

moved acyclic predicate up in hierarchy

--HG--
extra : rebase_source : 4c9a0c3c1dd3de32826493a20016e209648a4e47

modernized definitions

--HG--
extra : rebase_source : d50ecbd4a46b11ec1f49c3eb54ad2ee86a8981ce

tuned specification and lemma distribution among theories; tuned proofs

removed further legacy rules from Complete_Lattices

tuned proofs

removed unused material, which does not really belong here

tuned lemmas

new lemmas

added termination lemmas

primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`

map_pair replaces prod_fun

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

dropped superfluous [code del]s

declare lex_prod_def [code del]

repaired comments where SOMEthing went utterly wrong (cf. 2b04504fcb69)

locale predicates of classes carry a mandatory "class" prefix

now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"

Big_Operators now in Main rather than Plain

split off theory Big_Operators from theory Finite_Set

--HG--
rename : src/HOL/Finite_Set.thy => src/HOL/Big_Operators.thy

get rid of many duplicate simp rule warnings

authentic constants; moved "acyclic" further down

point-free characterization of well-foundedness

replaced (outdated) comments by explicit statements

eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;

simplified proof

moved lemma Wellfounded.in_inv_image to Relation.thy

moved wfrec to Recdef.thy

no consts_code for wfrec, as it violates the "code generation = equational reasoning" principle

explicit is better than implicit

moved obsolete same_fst to Recdef.thy

"more standard" argument order of relation composition (op O)

explicit is better than implicit

uniformly capitialized names for subdirectories

--HG--
rename : src/HOL/Tools/datatype_package/datatype.ML => src/HOL/Tools/Datatype/datatype.ML
rename : src/HOL/Tools/datatype_package/datatype_abs_proofs.ML => src/HOL/Tools/Datatype/datatype_abs_proofs.ML
rename : src/HOL/Tools/datatype_package/datatype_aux.ML => src/HOL/Tools/Datatype/datatype_aux.ML
rename : src/HOL/Tools/datatype_package/datatype_case.ML => src/HOL/Tools/Datatype/datatype_case.ML
rename : src/HOL/Tools/datatype_package/datatype_codegen.ML => src/HOL/Tools/Datatype/datatype_codegen.ML
rename : src/HOL/Tools/datatype_package/datatype_prop.ML => src/HOL/Tools/Datatype/datatype_prop.ML
rename : src/HOL/Tools/datatype_package/datatype_realizer.ML => src/HOL/Tools/Datatype/datatype_realizer.ML
rename : src/HOL/Tools/datatype_package/datatype_rep_proofs.ML => src/HOL/Tools/Datatype/datatype_rep_proofs.ML
rename : src/HOL/Tools/function_package/auto_term.ML => src/HOL/Tools/Function/auto_term.ML
rename : src/HOL/Tools/function_package/context_tree.ML => src/HOL/Tools/Function/context_tree.ML
rename : src/HOL/Tools/function_package/decompose.ML => src/HOL/Tools/Function/decompose.ML
rename : src/HOL/Tools/function_package/descent.ML => src/HOL/Tools/Function/descent.ML
rename : src/HOL/Tools/function_package/fundef.ML => src/HOL/Tools/Function/fundef.ML
rename : src/HOL/Tools/function_package/fundef_common.ML => src/HOL/Tools/Function/fundef_common.ML
rename : src/HOL/Tools/function_package/fundef_core.ML => src/HOL/Tools/Function/fundef_core.ML
rename : src/HOL/Tools/function_package/fundef_datatype.ML => src/HOL/Tools/Function/fundef_datatype.ML
rename : src/HOL/Tools/function_package/fundef_lib.ML => src/HOL/Tools/Function/fundef_lib.ML
rename : src/HOL/Tools/function_package/induction_scheme.ML => src/HOL/Tools/Function/induction_scheme.ML
rename : src/HOL/Tools/function_package/inductive_wrap.ML => src/HOL/Tools/Function/inductive_wrap.ML
rename : src/HOL/Tools/function_package/lexicographic_order.ML => src/HOL/Tools/Function/lexicographic_order.ML
rename : src/HOL/Tools/function_package/measure_functions.ML => src/HOL/Tools/Function/measure_functions.ML
rename : src/HOL/Tools/function_package/mutual.ML => src/HOL/Tools/Function/mutual.ML
rename : src/HOL/Tools/function_package/pattern_split.ML => src/HOL/Tools/Function/pattern_split.ML
rename : src/HOL/Tools/function_package/scnp_reconstruct.ML => src/HOL/Tools/Function/scnp_reconstruct.ML
rename : src/HOL/Tools/function_package/scnp_solve.ML => src/HOL/Tools/Function/scnp_solve.ML
rename : src/HOL/Tools/function_package/size.ML => src/HOL/Tools/Function/size.ML
rename : src/HOL/Tools/function_package/sum_tree.ML => src/HOL/Tools/Function/sum_tree.ML
rename : src/HOL/Tools/function_package/termination.ML => src/HOL/Tools/Function/termination.ML
rename : src/Tools/code/code_haskell.ML => src/Tools/Code/code_haskell.ML
rename : src/Tools/code/code_ml.ML => src/Tools/Code/code_ml.ML
rename : src/Tools/code/code_preproc.ML => src/Tools/Code/code_preproc.ML
rename : src/Tools/code/code_printer.ML => src/Tools/Code/code_printer.ML
rename : src/Tools/code/code_target.ML => src/Tools/Code/code_target.ML
rename : src/Tools/code/code_thingol.ML => src/Tools/Code/code_thingol.ML

reverted slip in theory imports

adjusted to changes in power syntax

explicit code equations for some rarely used pred operations

changed import hierarchy

dropped ID

method "sizechange" proves termination of functions; added more infrastructure for termination proofs

removed lemmas called lemma1 and lemma2

min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf

`code func` now just `code`

arbitrary is undefined

wf_finite_psubset[simp], in_finite_psubset[simp]

moved class wellorder to theory Orderings

rearranged subsections

- Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the
to_set and to_pred attributes, because it is no longer applied automatically
- Manually applied predicate1I in proof of accp_subset, because it is no longer
part of the claset
- Replaced psubset_def by less_le

Merged theories about wellfoundedness into one: Wellfounded.thy