equal
deleted
inserted
replaced
12 |
12 |
13 typedef (open) 'a set = "set :: ('a \<Rightarrow> bool) set" |
13 typedef (open) 'a set = "set :: ('a \<Rightarrow> bool) set" |
14 morphisms member Set |
14 morphisms member Set |
15 unfolding set_def by auto |
15 unfolding set_def by auto |
16 |
16 |
17 text {* Here is some ML setup that should eventually be incorporated in the typedef command. *} |
17 setup_lifting type_definition_set[unfolded set_def] |
18 |
|
19 local_setup {* fn lthy => |
|
20 let |
|
21 val quotients = |
|
22 {qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"}, |
|
23 equiv_rel = @{term "op ="}, equiv_thm = @{thm refl}} |
|
24 val qty_full_name = @{type_name "set"} |
|
25 |
|
26 fun qinfo phi = Quotient_Info.transform_quotients phi quotients |
|
27 in |
|
28 lthy |
|
29 |> Local_Theory.declaration {syntax = false, pervasive = true} |
|
30 (fn phi => |
|
31 Quotient_Info.update_quotients qty_full_name (qinfo phi) #> |
|
32 Quotient_Info.update_abs_rep qty_full_name |
|
33 (Quotient_Info.transform_abs_rep phi {abs = @{term "Set"}, rep = @{term "member"}})) |
|
34 end |
|
35 *} |
|
36 |
18 |
37 text {* Now, we can employ quotient_definition to lift definitions. *} |
19 text {* Now, we can employ quotient_definition to lift definitions. *} |
38 |
20 |
39 quotient_definition empty where "empty :: 'a set" |
21 quotient_definition empty where "empty :: 'a set" |
40 is "bot :: 'a \<Rightarrow> bool" done |
22 is "bot :: 'a \<Rightarrow> bool" done |
49 is insertp done |
31 is insertp done |
50 |
32 |
51 term "Lift_Set.insert" |
33 term "Lift_Set.insert" |
52 thm Lift_Set.insert_def |
34 thm Lift_Set.insert_def |
53 |
35 |
|
36 export_code empty insert in SML |
|
37 |
54 end |
38 end |
55 |
39 |