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