src/HOL/Quotient_Examples/Lift_Set.thy
 author blanchet Wed Feb 12 08:35:57 2014 +0100 (2014-02-12) changeset 55415 05f5fdb8d093 parent 49834 b27bbb021df1 child 55584 a879f14b6f95 permissions -rw-r--r--
renamed 'nat_{case,rec}' to '{case,rec}_nat'
```     1 (*  Title:      HOL/Quotient_Examples/Lift_Set.thy
```
```     2     Author:     Lukas Bulwahn and Ondrej Kuncar
```
```     3 *)
```
```     4
```
```     5 header {* Example of lifting definitions with the lifting infrastructure *}
```
```     6
```
```     7 theory Lift_Set
```
```     8 imports Main
```
```     9 begin
```
```    10
```
```    11 definition set where "set = (UNIV :: ('a \<Rightarrow> bool) set)"
```
```    12
```
```    13 typedef 'a set = "set :: ('a \<Rightarrow> bool) set"
```
```    14   morphisms member Set
```
```    15   unfolding set_def by auto
```
```    16
```
```    17 setup_lifting type_definition_set[unfolded set_def]
```
```    18
```
```    19 text {* Now, we can employ lift_definition to lift definitions. *}
```
```    20
```
```    21 lift_definition empty :: "'a set" is "bot :: 'a \<Rightarrow> bool" done
```
```    22
```
```    23 term "Lift_Set.empty"
```
```    24 thm Lift_Set.empty_def
```
```    25
```
```    26 lift_definition insert :: "'a => 'a set => 'a set" is "\<lambda> x P y. y = x \<or> P y" done
```
```    27
```
```    28 term "Lift_Set.insert"
```
```    29 thm Lift_Set.insert_def
```
```    30
```
```    31 export_code empty insert in SML
```
```    32
```
```    33 end
```
```    34
```