author | desharna |
Mon, 13 Jun 2022 20:02:00 +0200 | |
changeset 75560 | aeb797356de0 |
parent 73886 | 93ba8e3fdcdf |
child 77811 | ae9e6218443d |
permissions | -rw-r--r-- |
73886
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
1 |
subsection \<open>Code setup for sets with cardinality type information\<close> |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
2 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
3 |
theory Code_Cardinality imports Cardinality begin |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
4 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
5 |
text \<open> |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
6 |
Implement \<^term>\<open>CARD('a)\<close> via \<^term>\<open>card_UNIV\<close> and provide |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
7 |
implementations for \<^term>\<open>finite\<close>, \<^term>\<open>card\<close>, \<^term>\<open>(\<subseteq>)\<close>, |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
8 |
and \<^term>\<open>(=)\<close>if the calling context already provides \<^class>\<open>finite_UNIV\<close> |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
9 |
and \<^class>\<open>card_UNIV\<close> instances. If we implemented the latter |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
10 |
always via \<^term>\<open>card_UNIV\<close>, we would require instances of essentially all |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
11 |
element types, i.e., a lot of instantiation proofs and -- at run time -- |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
12 |
possibly slow dictionary constructions. |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
13 |
\<close> |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
14 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
15 |
context |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
16 |
begin |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
17 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
18 |
qualified definition card_UNIV' :: "'a card_UNIV" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
19 |
where [code del]: "card_UNIV' = Phantom('a) CARD('a)" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
20 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
21 |
lemma CARD_code [code_unfold]: |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
22 |
"CARD('a) = of_phantom (card_UNIV' :: 'a card_UNIV)" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
23 |
by(simp add: card_UNIV'_def) |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
24 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
25 |
lemma card_UNIV'_code [code]: |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
26 |
"card_UNIV' = card_UNIV" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
27 |
by(simp add: card_UNIV card_UNIV'_def) |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
28 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
29 |
end |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
30 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
31 |
lemma card_Compl: |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
32 |
"finite A \<Longrightarrow> card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
33 |
by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest) |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
34 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
35 |
context fixes xs :: "'a :: finite_UNIV list" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
36 |
begin |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
37 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
38 |
qualified definition finite' :: "'a set \<Rightarrow> bool" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
39 |
where [simp, code del, code_abbrev]: "finite' = finite" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
40 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
41 |
lemma finite'_code [code]: |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
42 |
"finite' (set xs) \<longleftrightarrow> True" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
43 |
"finite' (List.coset xs) \<longleftrightarrow> of_phantom (finite_UNIV :: 'a finite_UNIV)" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
44 |
by(simp_all add: card_gt_0_iff finite_UNIV) |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
45 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
46 |
end |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
47 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
48 |
context fixes xs :: "'a :: card_UNIV list" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
49 |
begin |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
50 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
51 |
qualified definition card' :: "'a set \<Rightarrow> nat" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
52 |
where [simp, code del, code_abbrev]: "card' = card" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
53 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
54 |
lemma card'_code [code]: |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
55 |
"card' (set xs) = length (remdups xs)" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
56 |
"card' (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
57 |
by(simp_all add: List.card_set card_Compl card_UNIV) |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
58 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
59 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
60 |
qualified definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
61 |
where [simp, code del, code_abbrev]: "subset' = (\<subseteq>)" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
62 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
63 |
lemma subset'_code [code]: |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
64 |
"subset' A (List.coset ys) \<longleftrightarrow> (\<forall>y \<in> set ys. y \<notin> A)" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
65 |
"subset' (set ys) B \<longleftrightarrow> (\<forall>y \<in> set ys. y \<in> B)" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
66 |
"subset' (List.coset xs) (set ys) \<longleftrightarrow> (let n = CARD('a) in n > 0 \<and> card(set (xs @ ys)) = n)" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
67 |
by(auto simp add: Let_def card_gt_0_iff dest: card_eq_UNIV_imp_eq_UNIV intro: arg_cong[where f=card]) |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
68 |
(metis finite_compl finite_set rev_finite_subset) |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
69 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
70 |
qualified definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
71 |
where [simp, code del, code_abbrev]: "eq_set = (=)" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
72 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
73 |
lemma eq_set_code [code]: |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
74 |
fixes ys |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
75 |
defines "rhs \<equiv> |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
76 |
let n = CARD('a) |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
77 |
in if n = 0 then False else |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
78 |
let xs' = remdups xs; ys' = remdups ys |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
79 |
in length xs' + length ys' = n \<and> (\<forall>x \<in> set xs'. x \<notin> set ys') \<and> (\<forall>y \<in> set ys'. y \<notin> set xs')" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
80 |
shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
81 |
and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
82 |
and "eq_set (set xs) (set ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
83 |
and "eq_set (List.coset xs) (List.coset ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
84 |
proof goal_cases |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
85 |
{ |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
86 |
case 1 |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
87 |
show ?case (is "?lhs \<longleftrightarrow> ?rhs") |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
88 |
proof |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
89 |
show ?rhs if ?lhs |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
90 |
using that |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
91 |
by (auto simp add: rhs_def Let_def List.card_set[symmetric] |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
92 |
card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
93 |
Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set) |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
94 |
show ?lhs if ?rhs |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
95 |
proof - |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
96 |
have "\<lbrakk> \<forall>y\<in>set xs. y \<notin> set ys; \<forall>x\<in>set ys. x \<notin> set xs \<rbrakk> \<Longrightarrow> set xs \<inter> set ys = {}" by blast |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
97 |
with that show ?thesis |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
98 |
by (auto simp add: rhs_def Let_def List.card_set[symmetric] |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
99 |
card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"] |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
100 |
dest: card_eq_UNIV_imp_eq_UNIV split: if_split_asm) |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
101 |
qed |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
102 |
qed |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
103 |
} |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
104 |
moreover |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
105 |
case 2 |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
106 |
ultimately show ?case unfolding eq_set_def by blast |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
107 |
next |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
108 |
case 3 |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
109 |
show ?case unfolding eq_set_def List.coset_def by blast |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
110 |
next |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
111 |
case 4 |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
112 |
show ?case unfolding eq_set_def List.coset_def by blast |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
113 |
qed |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
114 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
115 |
end |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
116 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
117 |
text \<open> |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
118 |
Provide more informative exceptions than Match for non-rewritten cases. |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
119 |
If generated code raises one these exceptions, then a code equation calls |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
120 |
the mentioned operator for an element type that is not an instance of |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
121 |
\<^class>\<open>card_UNIV\<close> and is therefore not implemented via \<^term>\<open>card_UNIV\<close>. |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
122 |
Constrain the element type with sort \<^class>\<open>card_UNIV\<close> to change this. |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
123 |
\<close> |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
124 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
125 |
lemma card_coset_error [code]: |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
126 |
"card (List.coset xs) = |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
127 |
Code.abort (STR ''card (List.coset _) requires type class instance card_UNIV'') |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
128 |
(\<lambda>_. card (List.coset xs))" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
129 |
by(simp) |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
130 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
131 |
lemma coset_subseteq_set_code [code]: |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
132 |
"List.coset xs \<subseteq> set ys \<longleftrightarrow> |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
133 |
(if xs = [] \<and> ys = [] then False |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
134 |
else Code.abort |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
135 |
(STR ''subset_eq (List.coset _) (List.set _) requires type class instance card_UNIV'') |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
136 |
(\<lambda>_. List.coset xs \<subseteq> set ys))" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
137 |
by simp |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
138 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
139 |
notepad begin \<comment> \<open>test code setup\<close> |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
140 |
have "List.coset [True] = set [False] \<and> |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
141 |
List.coset [] \<subseteq> List.set [True, False] \<and> |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
142 |
finite (List.coset [True])" |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
143 |
by eval |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
144 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
145 |
end |
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
146 |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
diff
changeset
|
147 |
end |