src/HOL/Quotient_Examples/Lift_Fun.thy
 author wenzelm Sun Nov 02 18:21:45 2014 +0100 (2014-11-02) changeset 58889 5b7a9633cfa8 parent 55941 a6a380edbec5 child 63167 0909deb8059b permissions -rw-r--r--
```     1 (*  Title:      HOL/Quotient_Examples/Lift_Fun.thy
```
```     2     Author:     Ondrej Kuncar
```
```     3 *)
```
```     4
```
```     5 section {* Example of lifting definitions with contravariant or co/contravariant type variables *}
```
```     6
```
```     7
```
```     8 theory Lift_Fun
```
```     9 imports Main "~~/src/HOL/Library/Quotient_Syntax"
```
```    10 begin
```
```    11
```
```    12 text {* This file is meant as a test case.
```
```    13   It contains examples of lifting definitions with quotients that have contravariant
```
```    14   type variables or type variables which are covariant and contravariant in the same time. *}
```
```    15
```
```    16 subsection {* Contravariant type variables *}
```
```    17
```
```    18 text {* 'a is a contravariant type variable and we are able to map over this variable
```
```    19   in the following four definitions. This example is based on HOL/Fun.thy. *}
```
```    20
```
```    21 quotient_type
```
```    22 ('a, 'b) fun' (infixr "\<rightarrow>" 55) = "'a \<Rightarrow> 'b" / "op ="
```
```    23   by (simp add: identity_equivp)
```
```    24
```
```    25 quotient_definition "comp' :: ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'c"  is
```
```    26   "comp :: ('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" done
```
```    27
```
```    28 quotient_definition "fcomp' :: ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" is
```
```    29   fcomp done
```
```    30
```
```    31 quotient_definition "map_fun' :: ('c \<rightarrow> 'a) \<rightarrow> ('b \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'c \<rightarrow> 'd"
```
```    32   is "map_fun::('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd" done
```
```    33
```
```    34 quotient_definition "inj_on' :: ('a \<rightarrow> 'b) \<rightarrow> 'a set \<rightarrow> bool" is inj_on done
```
```    35
```
```    36 quotient_definition "bij_betw' :: ('a \<rightarrow> 'b) \<rightarrow> 'a set \<rightarrow> 'b set \<rightarrow> bool" is bij_betw done
```
```    37
```
```    38
```
```    39 subsection {* Co/Contravariant type variables *}
```
```    40
```
```    41 text {* 'a is a covariant and contravariant type variable in the same time.
```
```    42   The following example is a bit artificial. We haven't had a natural one yet. *}
```
```    43
```
```    44 quotient_type 'a endofun = "'a \<Rightarrow> 'a" / "op =" by (simp add: identity_equivp)
```
```    45
```
```    46 definition map_endofun' :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> ('a => 'a) \<Rightarrow> ('b => 'b)"
```
```    47   where "map_endofun' f g e = map_fun g f e"
```
```    48
```
```    49 quotient_definition "map_endofun :: ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a endofun \<Rightarrow> 'b endofun" is
```
```    50   map_endofun' done
```
```    51
```
```    52 text {* Registration of the map function for 'a endofun. *}
```
```    53
```
```    54 functor map_endofun : map_endofun
```
```    55 proof -
```
```    56   have "\<forall> x. abs_endofun (rep_endofun x) = x" using Quotient3_endofun by (auto simp: Quotient3_def)
```
```    57   then show "map_endofun id id = id"
```
```    58     by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff)
```
```    59
```
```    60   have a:"\<forall> x. rep_endofun (abs_endofun x) = x" using Quotient3_endofun
```
```    61     Quotient3_rep_abs[of "(op =)" abs_endofun rep_endofun] by blast
```
```    62   show "\<And>f g h i. map_endofun f g \<circ> map_endofun h i = map_endofun (f \<circ> h) (i \<circ> g)"
```
```    63     by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff) (simp add: a o_assoc)
```
```    64 qed
```
```    65
```
```    66 text {* Relator for 'a endofun. *}
```
```    67
```
```    68 definition
```
```    69   rel_endofun' :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> bool"
```
```    70 where
```
```    71   "rel_endofun' R = (\<lambda>f g. (R ===> R) f g)"
```
```    72
```
```    73 quotient_definition "rel_endofun :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a endofun \<Rightarrow> 'b endofun \<Rightarrow> bool" is
```
```    74   rel_endofun' done
```
```    75
```
```    76 lemma endofun_quotient:
```
```    77 assumes a: "Quotient3 R Abs Rep"
```
```    78 shows "Quotient3 (rel_endofun R) (map_endofun Abs Rep) (map_endofun Rep Abs)"
```
```    79 proof (intro Quotient3I)
```
```    80   show "\<And>a. map_endofun Abs Rep (map_endofun Rep Abs a) = a"
```
```    81     by (metis (hide_lams, no_types) a abs_o_rep id_apply map_endofun.comp map_endofun.id o_eq_dest_lhs)
```
```    82 next
```
```    83   show "\<And>a. rel_endofun R (map_endofun Rep Abs a) (map_endofun Rep Abs a)"
```
```    84   using fun_quotient3[OF a a, THEN Quotient3_rep_reflp]
```
```    85   unfolding rel_endofun_def map_endofun_def map_fun_def o_def map_endofun'_def rel_endofun'_def id_def
```
```    86     by (metis (mono_tags) Quotient3_endofun rep_abs_rsp)
```
```    87 next
```
```    88   have abs_to_eq: "\<And> x y. abs_endofun x = abs_endofun y \<Longrightarrow> x = y"
```
```    89   by (drule arg_cong[where f=rep_endofun]) (simp add: Quotient3_rep_abs[OF Quotient3_endofun])
```
```    90   fix r s
```
```    91   show "rel_endofun R r s =
```
```    92           (rel_endofun R r r \<and>
```
```    93            rel_endofun R s s \<and> map_endofun Abs Rep r = map_endofun Abs Rep s)"
```
```    94     apply(auto simp add: rel_endofun_def rel_endofun'_def map_endofun_def map_endofun'_def)
```
```    95     using fun_quotient3[OF a a,THEN Quotient3_refl1]
```
```    96     apply metis
```
```    97     using fun_quotient3[OF a a,THEN Quotient3_refl2]
```
```    98     apply metis
```
```    99     using fun_quotient3[OF a a, THEN Quotient3_rel]
```
```   100     apply metis
```
```   101     by (auto intro: fun_quotient3[OF a a, THEN Quotient3_rel, THEN iffD1] simp add: abs_to_eq)
```
```   102 qed
```
```   103
```
```   104 declare [[mapQ3 endofun = (rel_endofun, endofun_quotient)]]
```
```   105
```
```   106 quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" done
```
```   107
```
```   108 term  endofun_id_id
```
```   109 thm  endofun_id_id_def
```
```   110
```
```   111 quotient_type 'a endofun' = "'a endofun" / "op =" by (simp add: identity_equivp)
```
```   112
```
```   113 text {* We have to map "'a endofun" to "('a endofun') endofun", i.e., mapping (lifting)
```
```   114   over a type variable which is a covariant and contravariant type variable. *}
```
```   115
```
```   116 quotient_definition "endofun'_id_id :: ('a endofun') endofun'" is endofun_id_id done
```
```   117
```
```   118 term  endofun'_id_id
```
```   119 thm  endofun'_id_id_def
```
```   120
```
```   121
```
```   122 end
```