src/HOL/Lifting.thy
author huffman
Sat Apr 21 13:06:22 2012 +0200 (2012-04-21)
changeset 47651 8e4f50afd21a
parent 47575 b90cd7016d4f
child 47652 1b722b100301
permissions -rw-r--r--
tuned proofs
     1 (*  Title:      HOL/Lifting.thy
     2     Author:     Brian Huffman and Ondrej Kuncar
     3     Author:     Cezary Kaliszyk and Christian Urban
     4 *)
     5 
     6 header {* Lifting package *}
     7 
     8 theory Lifting
     9 imports Plain Equiv_Relations Transfer
    10 keywords
    11   "print_quotmaps" "print_quotients" :: diag and
    12   "lift_definition" :: thy_goal and
    13   "setup_lifting" :: thy_decl
    14 uses
    15   ("Tools/Lifting/lifting_info.ML")
    16   ("Tools/Lifting/lifting_term.ML")
    17   ("Tools/Lifting/lifting_def.ML")
    18   ("Tools/Lifting/lifting_setup.ML")
    19 begin
    20 
    21 subsection {* Function map *}
    22 
    23 notation map_fun (infixr "--->" 55)
    24 
    25 lemma map_fun_id:
    26   "(id ---> id) = id"
    27   by (simp add: fun_eq_iff)
    28 
    29 subsection {* Quotient Predicate *}
    30 
    31 definition
    32   "Quotient R Abs Rep T \<longleftrightarrow>
    33      (\<forall>a. Abs (Rep a) = a) \<and> 
    34      (\<forall>a. R (Rep a) (Rep a)) \<and>
    35      (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s) \<and>
    36      T = (\<lambda>x y. R x x \<and> Abs x = y)"
    37 
    38 lemma QuotientI:
    39   assumes "\<And>a. Abs (Rep a) = a"
    40     and "\<And>a. R (Rep a) (Rep a)"
    41     and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s"
    42     and "T = (\<lambda>x y. R x x \<and> Abs x = y)"
    43   shows "Quotient R Abs Rep T"
    44   using assms unfolding Quotient_def by blast
    45 
    46 context
    47   fixes R Abs Rep T
    48   assumes a: "Quotient R Abs Rep T"
    49 begin
    50 
    51 lemma Quotient_abs_rep: "Abs (Rep a) = a"
    52   using a unfolding Quotient_def
    53   by simp
    54 
    55 lemma Quotient_rep_reflp: "R (Rep a) (Rep a)"
    56   using a unfolding Quotient_def
    57   by blast
    58 
    59 lemma Quotient_rel:
    60   "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
    61   using a unfolding Quotient_def
    62   by blast
    63 
    64 lemma Quotient_cr_rel: "T = (\<lambda>x y. R x x \<and> Abs x = y)"
    65   using a unfolding Quotient_def
    66   by blast
    67 
    68 lemma Quotient_refl1: "R r s \<Longrightarrow> R r r"
    69   using a unfolding Quotient_def
    70   by fast
    71 
    72 lemma Quotient_refl2: "R r s \<Longrightarrow> R s s"
    73   using a unfolding Quotient_def
    74   by fast
    75 
    76 lemma Quotient_rel_rep: "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
    77   using a unfolding Quotient_def
    78   by metis
    79 
    80 lemma Quotient_rep_abs: "R r r \<Longrightarrow> R (Rep (Abs r)) r"
    81   using a unfolding Quotient_def
    82   by blast
    83 
    84 lemma Quotient_rel_abs: "R r s \<Longrightarrow> Abs r = Abs s"
    85   using a unfolding Quotient_def
    86   by blast
    87 
    88 lemma Quotient_symp: "symp R"
    89   using a unfolding Quotient_def using sympI by (metis (full_types))
    90 
    91 lemma Quotient_transp: "transp R"
    92   using a unfolding Quotient_def using transpI by (metis (full_types))
    93 
    94 lemma Quotient_part_equivp: "part_equivp R"
    95 by (metis Quotient_rep_reflp Quotient_symp Quotient_transp part_equivpI)
    96 
    97 end
    98 
    99 lemma identity_quotient: "Quotient (op =) id id (op =)"
   100 unfolding Quotient_def by simp 
   101 
   102 lemma Quotient_alt_def:
   103   "Quotient R Abs Rep T \<longleftrightarrow>
   104     (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and>
   105     (\<forall>b. T (Rep b) b) \<and>
   106     (\<forall>x y. R x y \<longleftrightarrow> T x (Abs x) \<and> T y (Abs y) \<and> Abs x = Abs y)"
   107 apply safe
   108 apply (simp (no_asm_use) only: Quotient_def, fast)
   109 apply (simp (no_asm_use) only: Quotient_def, fast)
   110 apply (simp (no_asm_use) only: Quotient_def, fast)
   111 apply (simp (no_asm_use) only: Quotient_def, fast)
   112 apply (simp (no_asm_use) only: Quotient_def, fast)
   113 apply (simp (no_asm_use) only: Quotient_def, fast)
   114 apply (rule QuotientI)
   115 apply simp
   116 apply metis
   117 apply simp
   118 apply (rule ext, rule ext, metis)
   119 done
   120 
   121 lemma Quotient_alt_def2:
   122   "Quotient R Abs Rep T \<longleftrightarrow>
   123     (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and>
   124     (\<forall>b. T (Rep b) b) \<and>
   125     (\<forall>x y. R x y \<longleftrightarrow> T x (Abs y) \<and> T y (Abs x))"
   126   unfolding Quotient_alt_def by (safe, metis+)
   127 
   128 lemma fun_quotient:
   129   assumes 1: "Quotient R1 abs1 rep1 T1"
   130   assumes 2: "Quotient R2 abs2 rep2 T2"
   131   shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2) (T1 ===> T2)"
   132   using assms unfolding Quotient_alt_def2
   133   unfolding fun_rel_def fun_eq_iff map_fun_apply
   134   by (safe, metis+)
   135 
   136 lemma apply_rsp:
   137   fixes f g::"'a \<Rightarrow> 'c"
   138   assumes q: "Quotient R1 Abs1 Rep1 T1"
   139   and     a: "(R1 ===> R2) f g" "R1 x y"
   140   shows "R2 (f x) (g y)"
   141   using a by (auto elim: fun_relE)
   142 
   143 lemma apply_rsp':
   144   assumes a: "(R1 ===> R2) f g" "R1 x y"
   145   shows "R2 (f x) (g y)"
   146   using a by (auto elim: fun_relE)
   147 
   148 lemma apply_rsp'':
   149   assumes "Quotient R Abs Rep T"
   150   and "(R ===> S) f f"
   151   shows "S (f (Rep x)) (f (Rep x))"
   152 proof -
   153   from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp)
   154   then show ?thesis using assms(2) by (auto intro: apply_rsp')
   155 qed
   156 
   157 subsection {* Quotient composition *}
   158 
   159 lemma Quotient_compose:
   160   assumes 1: "Quotient R1 Abs1 Rep1 T1"
   161   assumes 2: "Quotient R2 Abs2 Rep2 T2"
   162   shows "Quotient (T1 OO R2 OO conversep T1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2) (T1 OO T2)"
   163 proof -
   164   from 1 have Abs1: "\<And>a b. T1 a b \<Longrightarrow> Abs1 a = b"
   165     unfolding Quotient_alt_def by simp
   166   from 1 have Rep1: "\<And>b. T1 (Rep1 b) b"
   167     unfolding Quotient_alt_def by simp
   168   from 2 have Abs2: "\<And>a b. T2 a b \<Longrightarrow> Abs2 a = b"
   169     unfolding Quotient_alt_def by simp
   170   from 2 have Rep2: "\<And>b. T2 (Rep2 b) b"
   171     unfolding Quotient_alt_def by simp
   172   from 2 have R2:
   173     "\<And>x y. R2 x y \<longleftrightarrow> T2 x (Abs2 x) \<and> T2 y (Abs2 y) \<and> Abs2 x = Abs2 y"
   174     unfolding Quotient_alt_def by simp
   175   show ?thesis
   176     unfolding Quotient_alt_def
   177     apply simp
   178     apply safe
   179     apply (drule Abs1, simp)
   180     apply (erule Abs2)
   181     apply (rule relcomppI)
   182     apply (rule Rep1)
   183     apply (rule Rep2)
   184     apply (rule relcomppI, assumption)
   185     apply (drule Abs1, simp)
   186     apply (clarsimp simp add: R2)
   187     apply (rule relcomppI, assumption)
   188     apply (drule Abs1, simp)+
   189     apply (clarsimp simp add: R2)
   190     apply (drule Abs1, simp)+
   191     apply (clarsimp simp add: R2)
   192     apply (rule relcomppI, assumption)
   193     apply (rule relcomppI [rotated])
   194     apply (erule conversepI)
   195     apply (drule Abs1, simp)+
   196     apply (simp add: R2)
   197     done
   198 qed
   199 
   200 lemma equivp_reflp2:
   201   "equivp R \<Longrightarrow> reflp R"
   202   by (erule equivpE)
   203 
   204 subsection {* Respects predicate *}
   205 
   206 definition Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set"
   207   where "Respects R = {x. R x x}"
   208 
   209 lemma in_respects: "x \<in> Respects R \<longleftrightarrow> R x x"
   210   unfolding Respects_def by simp
   211 
   212 subsection {* Invariant *}
   213 
   214 definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
   215   where "invariant R = (\<lambda>x y. R x \<and> x = y)"
   216 
   217 lemma invariant_to_eq:
   218   assumes "invariant P x y"
   219   shows "x = y"
   220 using assms by (simp add: invariant_def)
   221 
   222 lemma fun_rel_eq_invariant:
   223   shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
   224 by (auto simp add: invariant_def fun_rel_def)
   225 
   226 lemma invariant_same_args:
   227   shows "invariant P x x \<equiv> P x"
   228 using assms by (auto simp add: invariant_def)
   229 
   230 lemma UNIV_typedef_to_Quotient:
   231   assumes "type_definition Rep Abs UNIV"
   232   and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   233   shows "Quotient (op =) Abs Rep T"
   234 proof -
   235   interpret type_definition Rep Abs UNIV by fact
   236   from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis 
   237     by (fastforce intro!: QuotientI fun_eq_iff)
   238 qed
   239 
   240 lemma UNIV_typedef_to_equivp:
   241   fixes Abs :: "'a \<Rightarrow> 'b"
   242   and Rep :: "'b \<Rightarrow> 'a"
   243   assumes "type_definition Rep Abs (UNIV::'a set)"
   244   shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)"
   245 by (rule identity_equivp)
   246 
   247 lemma typedef_to_Quotient:
   248   assumes "type_definition Rep Abs S"
   249   and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   250   shows "Quotient (invariant (\<lambda>x. x \<in> S)) Abs Rep T"
   251 proof -
   252   interpret type_definition Rep Abs S by fact
   253   from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
   254     by (auto intro!: QuotientI simp: invariant_def fun_eq_iff)
   255 qed
   256 
   257 lemma typedef_to_part_equivp:
   258   assumes "type_definition Rep Abs S"
   259   shows "part_equivp (invariant (\<lambda>x. x \<in> S))"
   260 proof (intro part_equivpI)
   261   interpret type_definition Rep Abs S by fact
   262   show "\<exists>x. invariant (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: invariant_def)
   263 next
   264   show "symp (invariant (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: invariant_def)
   265 next
   266   show "transp (invariant (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: invariant_def)
   267 qed
   268 
   269 lemma open_typedef_to_Quotient:
   270   assumes "type_definition Rep Abs {x. P x}"
   271   and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   272   shows "Quotient (invariant P) Abs Rep T"
   273   using typedef_to_Quotient [OF assms] by simp
   274 
   275 lemma open_typedef_to_part_equivp:
   276   assumes "type_definition Rep Abs {x. P x}"
   277   shows "part_equivp (invariant P)"
   278   using typedef_to_part_equivp [OF assms] by simp
   279 
   280 text {* Generating transfer rules for quotients. *}
   281 
   282 context
   283   fixes R Abs Rep T
   284   assumes 1: "Quotient R Abs Rep T"
   285 begin
   286 
   287 lemma Quotient_right_unique: "right_unique T"
   288   using 1 unfolding Quotient_alt_def right_unique_def by metis
   289 
   290 lemma Quotient_right_total: "right_total T"
   291   using 1 unfolding Quotient_alt_def right_total_def by metis
   292 
   293 lemma Quotient_rel_eq_transfer: "(T ===> T ===> op =) R (op =)"
   294   using 1 unfolding Quotient_alt_def fun_rel_def by simp
   295 
   296 lemma Quotient_abs_induct:
   297   assumes "\<And>y. R y y \<Longrightarrow> P (Abs y)" shows "P x"
   298   using 1 assms unfolding Quotient_def by metis
   299 
   300 lemma Quotient_All_transfer:
   301   "((T ===> op =) ===> op =) (Ball (Respects R)) All"
   302   unfolding fun_rel_def Respects_def Quotient_cr_rel [OF 1]
   303   by (auto, metis Quotient_abs_induct)
   304 
   305 lemma Quotient_Ex_transfer:
   306   "((T ===> op =) ===> op =) (Bex (Respects R)) Ex"
   307   unfolding fun_rel_def Respects_def Quotient_cr_rel [OF 1]
   308   by (auto, metis Quotient_rep_reflp [OF 1] Quotient_abs_rep [OF 1])
   309 
   310 lemma Quotient_forall_transfer:
   311   "((T ===> op =) ===> op =) (transfer_bforall (\<lambda>x. R x x)) transfer_forall"
   312   using Quotient_All_transfer
   313   unfolding transfer_forall_def transfer_bforall_def
   314     Ball_def [abs_def] in_respects .
   315 
   316 end
   317 
   318 text {* Generating transfer rules for total quotients. *}
   319 
   320 context
   321   fixes R Abs Rep T
   322   assumes 1: "Quotient R Abs Rep T" and 2: "reflp R"
   323 begin
   324 
   325 lemma Quotient_bi_total: "bi_total T"
   326   using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto
   327 
   328 lemma Quotient_id_abs_transfer: "(op = ===> T) (\<lambda>x. x) Abs"
   329   using 1 2 unfolding Quotient_alt_def reflp_def fun_rel_def by simp
   330 
   331 lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x"
   332   using 1 2 assms unfolding Quotient_alt_def reflp_def by metis
   333 
   334 end
   335 
   336 text {* Generating transfer rules for a type defined with @{text "typedef"}. *}
   337 
   338 context
   339   fixes Rep Abs A T
   340   assumes type: "type_definition Rep Abs A"
   341   assumes T_def: "T \<equiv> (\<lambda>(x::'a) (y::'b). x = Rep y)"
   342 begin
   343 
   344 lemma typedef_bi_unique: "bi_unique T"
   345   unfolding bi_unique_def T_def
   346   by (simp add: type_definition.Rep_inject [OF type])
   347 
   348 lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep"
   349   unfolding fun_rel_def T_def by simp
   350 
   351 lemma typedef_All_transfer: "((T ===> op =) ===> op =) (Ball A) All"
   352   unfolding T_def fun_rel_def
   353   by (metis type_definition.Rep [OF type]
   354     type_definition.Abs_inverse [OF type])
   355 
   356 lemma typedef_Ex_transfer: "((T ===> op =) ===> op =) (Bex A) Ex"
   357   unfolding T_def fun_rel_def
   358   by (metis type_definition.Rep [OF type]
   359     type_definition.Abs_inverse [OF type])
   360 
   361 lemma typedef_forall_transfer:
   362   "((T ===> op =) ===> op =)
   363     (transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall"
   364   unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric]
   365   by (rule typedef_All_transfer)
   366 
   367 end
   368 
   369 text {* Generating the correspondence rule for a constant defined with
   370   @{text "lift_definition"}. *}
   371 
   372 lemma Quotient_to_transfer:
   373   assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c"
   374   shows "T c c'"
   375   using assms by (auto dest: Quotient_cr_rel)
   376 
   377 subsection {* ML setup *}
   378 
   379 text {* Auxiliary data for the lifting package *}
   380 
   381 use "Tools/Lifting/lifting_info.ML"
   382 setup Lifting_Info.setup
   383 
   384 declare [[map "fun" = (fun_rel, fun_quotient)]]
   385 
   386 use "Tools/Lifting/lifting_term.ML"
   387 
   388 use "Tools/Lifting/lifting_def.ML"
   389 
   390 use "Tools/Lifting/lifting_setup.ML"
   391 
   392 hide_const (open) invariant
   393 
   394 end