Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)

--HG--
extra : amend_source : fa78190ac2ee02ba33d22a4ee58362bc893ff097

Changes to complete distributive lattices due to Viorel Preoteasa

ran isabelle update_op on all sources

more symbols;

proper concept of code declaration wrt. atomicity and Isar declarations

--HG--
extra : rebase_source : adb08da85e01b6c9c81d471a0d8e7ebb68d7e472

modernized (code) setup for enumeration predicates

--HG--
extra : rebase_source : c008a78e07363775bc83ca26917eb8074426038e

more canonical names

more symbols;

isabelle update_cartouches;

tuned spelling;

modernized header uniformly as section;

added 'extraction' plugins -- this might help 'HOL-Proofs'

disable datatype 'plugins' for internal types

updated news

use 'datatype_new' in 'Main'

renamed 'xxx_size' to 'size_xxx' for old datatype package

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

consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly

normalising simp rules for compound operators

more complete set of lemmas wrt. image and composition

renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)

--HG--
rename : src/HOL/Tools/enriched_type.ML => src/HOL/Tools/functor.ML

adapted theories to 'xxx_case' to 'case_xxx'
* * *
'char_case' -> 'case_char' and same for 'rec'
* * *
compile
* * *
renamed 'xxx_case' to 'case_xxx'

prefer Code.abort over code_abort

tuned proofs -- clarified flow of facts wrt. calculation;

two target language numeral types: integer and natural, as replacement for code_numeral;
former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral;
refined stack of theories implementing int and/or nat by target language numerals;
reduced number of target language numeral types to exactly one

--HG--
extra : rebase_source : ffa0242ad108fe680ff144a716257c0784285d17

reform of predicate compiler / quickcheck theories:
implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers!
avoid odd New_ prefix by joining related theories;
avoid overcompact name DSequence;
separated predicate inside random monad into separate theory;
consolidated name of theory Quickcheck

--HG--
rename : src/HOL/DSequence.thy => src/HOL/Limited_Sequence.thy
rename : src/HOL/Quickcheck.thy => src/HOL/Quickcheck_Random.thy
extra : rebase_source : b6adaac1637d6d1cc809d2f937ae890fcc21969c

abandoned theory Plain

--HG--
extra : rebase_source : 6f5a395a55e8879386d1f79ab252c6fc2aca7dc5

abandoned almost redundant *_foldr lemmas

tuned proofs

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

moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax

reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems

distributed lattice properties of predicates to places of instantiation

--HG--
extra : rebase_source : f060e45b06e82cc14c73eba231a21e4636bbe179

Added inf_Int_eq to pred_set_conv database as well

Declared pred_equals/subset_eq, sup_Un_eq and SUP_UN_eq(2) as pred_set_conv rules

conversions from sets to predicates and vice versa; extensionality on predicates

--HG--
extra : rebase_source : 6fc7a7680a74eeca1858d9007acfdfb9aff426b6

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

proper intro? declarations -- NB: elim? indexes on major premise, which is too flexible here and easily leads to inefficiences (cf. a0336f8b6558);

renamed Complete_Lattices lemmas, removed legacy names

tuned specifications, syntax and proofs

tuned specifications and syntax

avoid pred/set mixture

more fine-granular instantiation

more specific instantiation

tuned proofs

eliminated global prems;
tuned proofs;

"enriched_type" replaces less specific "type_lifting"

--HG--
rename : src/HOL/Tools/type_lifting.ML => src/HOL/Tools/enriched_type.ML

tuned type_lifting declarations

type_lifting for predicates

bot comes before top, inf before sup etc.

nice syntax for lattice INFI, SUPR;
various *_apply rules for lattice operations on fun;
more default simplification rules

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

moved generic definitions about relations from Quotient.thy to Predicate;
more natural deduction rules

adhere established Collect/mem convention more closely

eval simp rules for predicate type, simplify primitive proofs

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

renamed class/constant eq to equal; tuned some instantiations

"no_atp" fact that leads to unsound Sledgehammer proofs

dropped superfluous [code del]s

yields ill-typed ATP/metis proofs -- raus!

code_reflect: specify module name directly after keyword

avoid code_datatype antiquotation

replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;

add/change some lemmas about lattices

moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)

tuned lattices theory fragements; generlized some lemmas from sets to lattices

tuned code setup

adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler

removed dummy setup for predicate compiler commands as the compiler is now part of HOL-Main

tuned

developing an executable the operator

generalizing singleton with a default value

moved meta_fun_cong lemma into ML-file; tuned

inf/sup1/2_iff are mere duplicates of underlying definitions: dropped

moved lemmas about sup on bool to Lattices.thy

tuned headings

removed potentially dangerous rules from pred_set_conv

added first prototype of the extended predicate compiler

be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default

hide new constants

added emptiness check predicate and singleton projection

formally stylized

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

avoid useless code equations

added Predicate.map in SML environment

added Predicate.map

dropped sort constraint on predicate equality

added dummy values keyword

avoid latex output problem

Added pred_code command

fixed compilation of predicate types in ML environment

added general preprocessing of equality in predicates for code generation

static compilation of enumeration type

explicit code equations for some rarely used pred operations

dropped eq_pred

refined enumeration implementation

added enumeration of predicates

- Added mem_def and predicate1I in some of the proofs
- pred_equals_eq and pred_subset_eq are no longer used in the conversion
between sets and predicates, because sets and predicates can no longer
be distinguished

Sup now explicit parameter of complete_lattice

- Moved infrastructure for converting between sets and predicates
to Tools/inductive_set_package.ML
- Adapted conversion rules to new format (now use standard op :
and Collect operators rather than Collect2 and member(2))
- Removed bounded quantifiers for predicates

clarified import

tuned proofs: avoid implicit prems;

simplified DataFun interfaces;

Generalized version of SUP and INF (with index set).

stepping towards uniform lattice theory development in HOL

New theory for converting between predicates and sets.