24 |
24 |
25 quotient_type |
25 quotient_type |
26 fset = "'a list" / "list_eq" |
26 fset = "'a list" / "list_eq" |
27 by (rule equivp_list_eq) |
27 by (rule equivp_list_eq) |
28 |
28 |
|
29 |
|
30 fun |
|
31 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
|
32 where |
|
33 "intrel (x, y) (u, v) = (x + v = u + y)" |
|
34 |
|
35 quotient_type int = "nat \<times> nat" / intrel |
|
36 apply(unfold equivp_def) |
|
37 apply(auto simp add: mem_def expand_fun_eq) |
|
38 done |
|
39 |
|
40 |
|
41 ML {* |
|
42 open Quotient_Def; |
|
43 *} |
|
44 |
|
45 ML {* |
|
46 get_fun absF @{context} (@{typ "'a list"}, |
|
47 @{typ "'a fset"}) |
|
48 |> Syntax.check_term @{context} |
|
49 |> Syntax.string_of_term @{context} |
|
50 |> writeln |
|
51 *} |
|
52 |
|
53 term "map id" |
|
54 term "abs_fset o (map id)" |
|
55 |
|
56 ML {* |
|
57 get_fun absF @{context} (@{typ "(nat * nat) list"}, |
|
58 @{typ "int fset"}) |
|
59 |> Syntax.check_term @{context} |
|
60 |> Syntax.string_of_term @{context} |
|
61 |> writeln |
|
62 *} |
|
63 |
|
64 term "map abs_int" |
|
65 term "abs_fset o map abs_int" |
|
66 |
|
67 |
|
68 ML {* |
|
69 get_fun absF @{context} (@{typ "('a list) list"}, |
|
70 @{typ "('a fset) fset"}) |
|
71 |> Syntax.check_term @{context} |
|
72 |> Syntax.string_of_term @{context} |
|
73 |> writeln |
|
74 *} |
|
75 |
|
76 ML {* |
|
77 get_fun absF @{context} (@{typ "('a list) list \<Rightarrow> 'a"}, |
|
78 @{typ "('a fset) fset \<Rightarrow> 'a"}) |
|
79 |> Syntax.check_term @{context} |
|
80 |> Syntax.string_of_term @{context} |
|
81 |> writeln |
|
82 *} |
|
83 |
29 quotient_definition |
84 quotient_definition |
30 "EMPTY :: 'a fset" |
85 "EMPTY :: 'a fset" |
31 as |
86 as |
32 "[]::'a list" |
87 "[]::'a list" |
33 |
88 |
50 quotient_definition |
105 quotient_definition |
51 "CARD :: 'a fset \<Rightarrow> nat" |
106 "CARD :: 'a fset \<Rightarrow> nat" |
52 as |
107 as |
53 "card1" |
108 "card1" |
54 |
109 |
55 (* text {* |
110 quotient_definition |
|
111 "fconcat :: ('a fset) fset \<Rightarrow> 'a fset" |
|
112 as |
|
113 "concat" |
|
114 |
|
115 term concat |
|
116 term fconcat |
|
117 |
|
118 text {* |
56 Maybe make_const_def should require a theorem that says that the particular lifted function |
119 Maybe make_const_def should require a theorem that says that the particular lifted function |
57 respects the relation. With it such a definition would be impossible: |
120 respects the relation. With it such a definition would be impossible: |
58 make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
121 make_const_def CARD @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
59 *}*) |
122 *} |
60 |
123 |
61 lemma card1_0: |
124 lemma card1_0: |
62 fixes a :: "'a list" |
125 fixes a :: "'a list" |
63 shows "(card1 a = 0) = (a = [])" |
126 shows "(card1 a = 0) = (a = [])" |
64 by (induct a) auto |
127 by (induct a) auto |
211 lemma "IN x EMPTY = False" |
274 lemma "IN x EMPTY = False" |
212 apply(lifting member.simps(1)) |
275 apply(lifting member.simps(1)) |
213 done |
276 done |
214 |
277 |
215 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
278 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
216 by (lifting member.simps(2)) |
279 apply (lifting member.simps(2)) |
|
280 done |
217 |
281 |
218 lemma "INSERT a (INSERT a x) = INSERT a x" |
282 lemma "INSERT a (INSERT a x) = INSERT a x" |
219 apply (lifting list_eq.intros(4)) |
283 apply (lifting list_eq.intros(4)) |
220 done |
284 done |
221 |
285 |