9 imports |
9 imports |
10 Predicate_Compile |
10 Predicate_Compile |
11 Quickcheck_Narrowing |
11 Quickcheck_Narrowing |
12 Extraction |
12 Extraction |
13 Nunchaku |
13 Nunchaku |
14 BNF_Greatest_Fixpoint Filter |
14 BNF_Greatest_Fixpoint |
|
15 Filter |
15 Conditionally_Complete_Lattices |
16 Conditionally_Complete_Lattices |
16 Binomial |
17 Binomial |
17 GCD |
18 GCD |
18 begin |
19 begin |
|
20 |
|
21 text \<open>Legacy\<close> |
|
22 |
|
23 context Inf |
|
24 begin |
|
25 |
|
26 abbreviation (input) INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" |
|
27 where "INFIMUM A f \<equiv> \<Sqinter>(f ` A)" |
|
28 |
|
29 end |
|
30 |
|
31 context Sup |
|
32 begin |
|
33 |
|
34 abbreviation (input) SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" |
|
35 where "SUPREMUM A f \<equiv> \<Squnion>(f ` A)" |
|
36 |
|
37 end |
|
38 |
|
39 abbreviation (input) INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" |
|
40 where "INTER \<equiv> INFIMUM" |
|
41 |
|
42 abbreviation (input) UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" |
|
43 where "UNION \<equiv> SUPREMUM" |
|
44 |
|
45 |
|
46 text \<open>Namespace cleanup\<close> |
|
47 |
|
48 hide_const (open) |
|
49 czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect |
|
50 fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift |
|
51 shift proj id_bnf |
|
52 |
|
53 hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV |
|
54 |
|
55 |
|
56 text \<open>Syntax cleanup\<close> |
19 |
57 |
20 no_notation |
58 no_notation |
21 bot ("\<bottom>") and |
59 bot ("\<bottom>") and |
22 top ("\<top>") and |
60 top ("\<top>") and |
23 inf (infixl "\<sqinter>" 70) and |
61 inf (infixl "\<sqinter>" 70) and |
27 ordLeq2 (infix "<=o" 50) and |
65 ordLeq2 (infix "<=o" 50) and |
28 ordLeq3 (infix "\<le>o" 50) and |
66 ordLeq3 (infix "\<le>o" 50) and |
29 ordLess2 (infix "<o" 50) and |
67 ordLess2 (infix "<o" 50) and |
30 ordIso2 (infix "=o" 50) and |
68 ordIso2 (infix "=o" 50) and |
31 card_of ("|_|") and |
69 card_of ("|_|") and |
32 csum (infixr "+c" 65) and |
70 BNF_Cardinal_Arithmetic.csum (infixr "+c" 65) and |
33 cprod (infixr "*c" 80) and |
71 BNF_Cardinal_Arithmetic.cprod (infixr "*c" 80) and |
34 cexp (infixr "^c" 90) and |
72 BNF_Cardinal_Arithmetic.cexp (infixr "^c" 90) and |
35 convol ("\<langle>(_,/ _)\<rangle>") |
73 BNF_Def.convol ("\<langle>(_,/ _)\<rangle>") |
36 |
|
37 hide_const (open) |
|
38 czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect |
|
39 fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift |
|
40 shift proj id_bnf |
|
41 |
|
42 hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV |
|
43 |
74 |
44 no_syntax |
75 no_syntax |
45 "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10) |
76 "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10) |
46 "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10) |
77 "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10) |
47 "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10) |
78 "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10) |