714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory FSet3
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
2 |
imports "../QuotMain" List
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
begin
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
|
722
|
5 |
fun
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
where
|
722
|
8 |
"list_eq xs ys = (\<forall>e. (e \<in> set xs) = (e \<in> set ys))"
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
9 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
10 |
lemma list_eq_equivp:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
11 |
shows "equivp list_eq"
|
722
|
12 |
unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
|
|
13 |
by auto
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
14 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
15 |
quotient fset = "'a list" / "list_eq"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
16 |
by (rule list_eq_equivp)
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
17 |
|
722
|
18 |
lemma not_nil_equiv_cons:
|
|
19 |
"\<not>[] \<approx> a # A"
|
|
20 |
by auto
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
21 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
22 |
lemma nil_rsp[quot_respect]:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
23 |
shows "[] \<approx> []"
|
722
|
24 |
by simp
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
25 |
|
722
|
26 |
lemma cons_rsp[quot_respect]:
|
|
27 |
shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"
|
|
28 |
by simp
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
29 |
|
722
|
30 |
(*
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
31 |
lemma mem_rsp[quot_respect]:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
32 |
"(op = ===> op \<approx> ===> op =) (op mem) (op mem)"
|
722
|
33 |
*)
|
|
34 |
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
35 |
|
722
|
36 |
lemma no_mem_nil:
|
|
37 |
"(\<forall>a. \<not>(a \<in> set A)) = (A = [])"
|
|
38 |
by (induct A) (auto)
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
39 |
|
722
|
40 |
lemma none_mem_nil:
|
|
41 |
"(\<forall>a. \<not>(a \<in> set A)) = (A \<approx> [])"
|
|
42 |
by simp
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
43 |
|
722
|
44 |
lemma mem_cons:
|
|
45 |
"a \<in> set A \<Longrightarrow> a # A \<approx> A"
|
|
46 |
by auto
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
47 |
|
722
|
48 |
lemma cons_left_comm:
|
|
49 |
"x #y # A \<approx> y # x # A"
|
|
50 |
by auto
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
51 |
|
722
|
52 |
lemma cons_left_idem:
|
|
53 |
"x # x # A \<approx> x # A"
|
|
54 |
by auto
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
55 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
56 |
lemma finite_set_raw_strong_cases:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
57 |
"(X = []) \<or> (\<exists>a. \<exists> Y. (~(a mem Y) \<and> (X \<approx> a # Y)))"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
58 |
apply (induct X)
|
722
|
59 |
apply (auto)
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
60 |
sorry
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
61 |
|
722
|
62 |
fun
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
63 |
delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
64 |
where
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
65 |
"delete_raw [] x = []"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
66 |
| "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
67 |
|
722
|
68 |
(* definitely FALSE
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
69 |
lemma mem_delete_raw:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
70 |
"x mem (delete_raw A a) = x mem A \<and> \<not>(x = a)"
|
722
|
71 |
apply(induct A arbitrary: x a)
|
|
72 |
apply(auto)
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
73 |
sorry
|
722
|
74 |
*)
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
75 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
76 |
lemma mem_delete_raw_ident:
|
722
|
77 |
"\<not>(a \<in> set (delete_raw A a))"
|
|
78 |
by (induct A) (auto)
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
79 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
80 |
lemma not_mem_delete_raw_ident:
|
722
|
81 |
"b \<notin> set A \<Longrightarrow> (delete_raw A b = A)"
|
|
82 |
by (induct A) (auto)
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
83 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
84 |
lemma delete_raw_RSP:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
85 |
"A \<approx> B \<Longrightarrow> delete_raw A a \<approx> delete_raw B a"
|
722
|
86 |
apply(induct A arbitrary: B a)
|
|
87 |
apply(auto)
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
88 |
sorry
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
89 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
90 |
lemma cons_delete_raw:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
91 |
"a # (delete_raw A a) \<approx> (if a mem A then A else (a # A))"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
92 |
sorry
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
93 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
94 |
lemma mem_cons_delete_raw:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
95 |
"a mem A \<Longrightarrow> a # (delete_raw A a) \<approx> A"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
96 |
sorry
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
97 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
98 |
lemma finite_set_raw_delete_raw_cases1:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
99 |
"X = [] \<or> (\<exists>a. X \<approx> a # delete_raw X a)"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
100 |
sorry
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
101 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
102 |
lemma finite_set_raw_delete_raw_cases:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
103 |
"X = [] \<or> (\<exists>a. a mem X \<and> X \<approx> a # delete_raw X a)"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
104 |
sorry
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
105 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
106 |
fun
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
107 |
card_raw :: "'a list \<Rightarrow> nat"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
108 |
where
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
109 |
card_raw_nil: "card_raw [] = 0"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
110 |
| card_raw_cons: "card_raw (x # xs) = (if x mem xs then card_raw xs else Suc (card_raw xs))"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
111 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
112 |
lemma not_mem_card_raw:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
113 |
fixes x :: "'a"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
114 |
fixes xs :: "'a list"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
115 |
shows "(\<not>(x mem xs)) = (card_raw (x # xs) = Suc (card_raw xs))"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
116 |
sorry
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
117 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
118 |
lemma card_raw_suc:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
119 |
fixes xs :: "'a list"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
120 |
fixes n :: "nat"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
121 |
assumes c: "card_raw xs = Suc n"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
122 |
shows "\<exists>a ys. \<not>(a mem ys) \<and> xs \<approx> (a # ys)"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
123 |
using c
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
124 |
apply(induct xs)
|
722
|
125 |
(*apply(metis mem_delete_raw)
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
126 |
apply(metis mem_delete_raw)
|
722
|
127 |
done*)
|
|
128 |
sorry
|
|
129 |
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
130 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
131 |
lemma mem_card_raw_not_0:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
132 |
"a mem A \<Longrightarrow> \<not>(card_raw A = 0)"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
133 |
sorry
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
134 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
135 |
lemma card_raw_cons_gt_0:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
136 |
"0 < card_raw (a # A)"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
137 |
sorry
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
138 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
139 |
lemma card_raw_delete_raw:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
140 |
"card_raw (delete_raw A a) = (if a mem A then card_raw A - 1 else card_raw A)"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
141 |
sorry
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
142 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
143 |
lemma card_raw_rsp_aux:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
144 |
assumes e: "a \<approx> b"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
145 |
shows "card_raw a = card_raw b"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
146 |
using e sorry
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
147 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
148 |
lemma card_raw_rsp[quot_respect]:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
149 |
"(op \<approx> ===> op =) card_raw card_raw"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
150 |
by (simp add: card_raw_rsp_aux)
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
151 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
152 |
lemma card_raw_0:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
153 |
"(card_raw A = 0) = (A = [])"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
154 |
sorry
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
155 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
156 |
lemma list2set_thm:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
157 |
shows "set [] = {}"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
158 |
and "set (h # t) = insert h (set t)"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
159 |
sorry
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
160 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
161 |
lemma list2set_RSP:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
162 |
"A \<approx> B \<Longrightarrow> set A = set B"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
163 |
sorry
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
164 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
165 |
definition
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
166 |
rsp_fold
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
167 |
where
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
168 |
"rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
169 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
170 |
primrec
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
171 |
fold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
172 |
where
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
173 |
"fold_raw f z [] = z"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
174 |
| "fold_raw f z (a # A) =
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
175 |
(if (rsp_fold f) then
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
176 |
if a mem A then fold_raw f z A
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
177 |
else f a (fold_raw f z A)
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
178 |
else z)"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
179 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
180 |
lemma mem_lcommuting_fold_raw:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
181 |
"rsp_fold f \<Longrightarrow> h mem B \<Longrightarrow> fold_raw f z B = f h (fold_raw f z (delete_raw B h))"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
182 |
sorry
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
183 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
184 |
lemma fold_rsp[quot_respect]:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
185 |
"(op = ===> op = ===> op \<approx> ===> op =) fold_raw fold_raw"
|
722
|
186 |
apply(auto)
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
187 |
sorry
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
188 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
189 |
lemma append_rsp[quot_respect]:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
190 |
"(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
|
722
|
191 |
by auto
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
192 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
193 |
primrec
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
194 |
inter_raw
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
195 |
where
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
196 |
"inter_raw [] B = []"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
197 |
| "inter_raw (a # A) B = (if a mem B then a # inter_raw A B else inter_raw A B)"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
198 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
199 |
lemma mem_inter_raw:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
200 |
"x mem (inter_raw A B) = x mem A \<and> x mem B"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
201 |
sorry
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
202 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
203 |
lemma inter_raw_RSP:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
204 |
"A1 \<approx> A2 \<and> B1 \<approx> B2 \<Longrightarrow> (inter_raw A1 B1) \<approx> (inter_raw A2 B2)"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
205 |
sorry
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
206 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
207 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
208 |
(* LIFTING DEFS *)
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
209 |
|
722
|
210 |
|
|
211 |
section {* Constants on the Quotient Type *}
|
|
212 |
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
213 |
quotient_def
|
722
|
214 |
"fempty :: 'a fset"
|
|
215 |
as "[]::'a list"
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
216 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
217 |
quotient_def
|
722
|
218 |
"finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
|
|
219 |
as "op #"
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
220 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
221 |
quotient_def
|
722
|
222 |
"fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)
|
|
223 |
as "\<lambda>x X. x \<in> set X"
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
224 |
|
722
|
225 |
abbreviation
|
|
226 |
fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<notin>f _" [50, 51] 50)
|
|
227 |
where
|
|
228 |
"a \<notin>f S \<equiv> \<not>(a \<in>f S)"
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
229 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
230 |
quotient_def
|
722
|
231 |
"fcard :: 'a fset \<Rightarrow> nat"
|
|
232 |
as "card_raw"
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
233 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
234 |
quotient_def
|
722
|
235 |
"fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset"
|
|
236 |
as "delete_raw"
|
|
237 |
|
|
238 |
quotient_def
|
|
239 |
"funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<in>f _" [50, 51] 50)
|
|
240 |
as "op @"
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
241 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
242 |
quotient_def
|
722
|
243 |
"finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
|
|
244 |
as "inter_raw"
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
245 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
246 |
quotient_def
|
722
|
247 |
"ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
|
|
248 |
as "fold_raw"
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
249 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
250 |
quotient_def
|
722
|
251 |
"fset_to_set :: 'a fset \<Rightarrow> 'a set"
|
|
252 |
as "set"
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
253 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
254 |
|
722
|
255 |
section {* Lifted Theorems *}
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
256 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
257 |
thm list.cases (* ??? *)
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
258 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
259 |
thm cons_left_comm
|
722
|
260 |
lemma "finsert a (finsert b S) = finsert b (finsert a S)"
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
261 |
by (lifting cons_left_comm)
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
262 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
263 |
thm cons_left_idem
|
722
|
264 |
lemma "finsert a (finsert a S) = finsert a S"
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
265 |
by (lifting cons_left_idem)
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
266 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
267 |
(* thm MEM:
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
268 |
MEM x [] = F
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
269 |
MEM x (h::t) = (x=h) \/ MEM x t *)
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
270 |
thm none_mem_nil
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
271 |
thm mem_cons
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
272 |
thm finite_set_raw_strong_cases
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
273 |
thm card_raw.simps
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
274 |
thm not_mem_card_raw
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
275 |
thm card_raw_suc
|
722
|
276 |
|
|
277 |
lemma "fcard X = Suc n \<Longrightarrow> (\<exists>a S. a \<notin>f S & X = finsert a S)"
|
|
278 |
(*by (lifting card_raw_suc)*)
|
|
279 |
sorry
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
280 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
281 |
thm card_raw_cons_gt_0
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
282 |
thm mem_card_raw_not_0
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
283 |
thm not_nil_equiv_cons
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
284 |
thm delete_raw.simps
|
722
|
285 |
(*thm mem_delete_raw*)
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
286 |
thm card_raw_delete_raw
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
287 |
thm cons_delete_raw
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
288 |
thm mem_cons_delete_raw
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
289 |
thm finite_set_raw_delete_raw_cases
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
290 |
thm append.simps
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
291 |
(* MEM_APPEND: MEM e (APPEND l1 l2) = MEM e l1 \/ MEM e l2 *)
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
292 |
thm inter_raw.simps
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
293 |
thm mem_inter_raw
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
294 |
thm fold_raw.simps
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
295 |
thm list2set_thm
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
296 |
thm list_eq_def
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
297 |
thm list.induct
|
722
|
298 |
lemma "\<lbrakk>P fempty; \<And>a x. P x \<Longrightarrow> P (finsert a x)\<rbrakk> \<Longrightarrow> P l"
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
299 |
by (lifting list.induct)
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
300 |
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
301 |
(* We also have map and some properties of it in FSet *)
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
302 |
(* and the following which still lifts ok *)
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
303 |
lemma "funion (funion x xa) xb = funion x (funion xa xb)"
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
304 |
by (lifting append_assoc)
|
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
305 |
|
716
|
306 |
quotient_def
|
|
307 |
"fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
|
|
308 |
as
|
|
309 |
"list_case"
|
|
310 |
|
|
311 |
(* NOT SURE IF TRUE *)
|
|
312 |
lemma list_case_rsp[quot_respect]:
|
|
313 |
"(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
|
|
314 |
apply (auto)
|
|
315 |
sorry
|
|
316 |
|
722
|
317 |
lemma "fset_case (f1::'t) f2 (finsert a xa) = f2 a xa"
|
716
|
318 |
apply (lifting list.cases(2))
|
|
319 |
done
|
|
320 |
|
|
321 |
|
714
37f7dc85b61b
Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
322 |
end
|