src/HOL/Lifting.thy
author huffman
Wed Apr 18 15:48:32 2012 +0200 (2012-04-18)
changeset 47544 e455cdaac479
parent 47538 1f0ec5b8135a
child 47545 a2850a16e30f
permissions -rw-r--r--
move constant 'Respects' into Lifting.thy;
add quantifier transfer rules for quotients
     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 proof -
   274   interpret type_definition Rep Abs "{x. P x}" by fact
   275   from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
   276     by (auto intro!: QuotientI simp: invariant_def fun_eq_iff)
   277 qed
   278 
   279 lemma open_typedef_to_part_equivp:
   280   assumes "type_definition Rep Abs {x. P x}"
   281   shows "part_equivp (invariant P)"
   282 proof (intro part_equivpI)
   283   interpret type_definition Rep Abs "{x. P x}" by fact
   284   show "\<exists>x. invariant P x x" using Rep by (auto simp: invariant_def)
   285 next
   286   show "symp (invariant P)" by (auto intro: sympI simp: invariant_def)
   287 next
   288   show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)
   289 qed
   290 
   291 text {* Generating transfer rules for quotients. *}
   292 
   293 context
   294   fixes R Abs Rep T
   295   assumes 1: "Quotient R Abs Rep T"
   296 begin
   297 
   298 lemma Quotient_right_unique: "right_unique T"
   299   using 1 unfolding Quotient_alt_def right_unique_def by metis
   300 
   301 lemma Quotient_right_total: "right_total T"
   302   using 1 unfolding Quotient_alt_def right_total_def by metis
   303 
   304 lemma Quotient_rel_eq_transfer: "(T ===> T ===> op =) R (op =)"
   305   using 1 unfolding Quotient_alt_def fun_rel_def by simp
   306 
   307 lemma Quotient_abs_induct:
   308   assumes "\<And>y. R y y \<Longrightarrow> P (Abs y)" shows "P x"
   309   using 1 assms unfolding Quotient_def by metis
   310 
   311 lemma Quotient_All_transfer:
   312   "((T ===> op =) ===> op =) (Ball (Respects R)) All"
   313   unfolding fun_rel_def Respects_def Quotient_cr_rel [OF 1]
   314   by (auto, metis Quotient_abs_induct)
   315 
   316 lemma Quotient_Ex_transfer:
   317   "((T ===> op =) ===> op =) (Bex (Respects R)) Ex"
   318   unfolding fun_rel_def Respects_def Quotient_cr_rel [OF 1]
   319   by (auto, metis Quotient_rep_reflp [OF 1] Quotient_abs_rep [OF 1])
   320 
   321 lemma Quotient_forall_transfer:
   322   "((T ===> op =) ===> op =) (transfer_bforall (\<lambda>x. R x x)) transfer_forall"
   323   using Quotient_All_transfer
   324   unfolding transfer_forall_def transfer_bforall_def
   325     Ball_def [abs_def] in_respects .
   326 
   327 end
   328 
   329 text {* Generating transfer rules for total quotients. *}
   330 
   331 context
   332   fixes R Abs Rep T
   333   assumes 1: "Quotient R Abs Rep T" and 2: "reflp R"
   334 begin
   335 
   336 lemma Quotient_bi_total: "bi_total T"
   337   using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto
   338 
   339 lemma Quotient_id_abs_transfer: "(op = ===> T) (\<lambda>x. x) Abs"
   340   using 1 2 unfolding Quotient_alt_def reflp_def fun_rel_def by simp
   341 
   342 end
   343 
   344 text {* Generating transfer rules for a type defined with @{text "typedef"}. *}
   345 
   346 context
   347   fixes Rep Abs A T
   348   assumes type: "type_definition Rep Abs A"
   349   assumes T_def: "T \<equiv> (\<lambda>(x::'a) (y::'b). x = Rep y)"
   350 begin
   351 
   352 lemma typedef_bi_unique: "bi_unique T"
   353   unfolding bi_unique_def T_def
   354   by (simp add: type_definition.Rep_inject [OF type])
   355 
   356 lemma typedef_right_total: "right_total T"
   357   unfolding right_total_def T_def by simp
   358 
   359 lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep"
   360   unfolding fun_rel_def T_def by simp
   361 
   362 lemma typedef_transfer_All: "((T ===> op =) ===> op =) (Ball A) All"
   363   unfolding T_def fun_rel_def
   364   by (metis type_definition.Rep [OF type]
   365     type_definition.Abs_inverse [OF type])
   366 
   367 lemma typedef_transfer_Ex: "((T ===> op =) ===> op =) (Bex A) Ex"
   368   unfolding T_def fun_rel_def
   369   by (metis type_definition.Rep [OF type]
   370     type_definition.Abs_inverse [OF type])
   371 
   372 lemma typedef_transfer_bforall:
   373   "((T ===> op =) ===> op =)
   374     (transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall"
   375   unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric]
   376   by (rule typedef_transfer_All)
   377 
   378 end
   379 
   380 text {* Generating transfer rules for a type copy. *}
   381 
   382 lemma copy_type_bi_total:
   383   assumes type: "type_definition Rep Abs UNIV"
   384   assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   385   shows "bi_total T"
   386   unfolding bi_total_def T_def
   387   by (metis type_definition.Abs_inverse [OF type] UNIV_I)
   388 
   389 text {* Generating the correspondence rule for a constant defined with
   390   @{text "lift_definition"}. *}
   391 
   392 lemma Quotient_to_transfer:
   393   assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c"
   394   shows "T c c'"
   395   using assms by (auto dest: Quotient_cr_rel)
   396 
   397 subsection {* ML setup *}
   398 
   399 text {* Auxiliary data for the lifting package *}
   400 
   401 use "Tools/Lifting/lifting_info.ML"
   402 setup Lifting_Info.setup
   403 
   404 declare [[map "fun" = (fun_rel, fun_quotient)]]
   405 
   406 use "Tools/Lifting/lifting_term.ML"
   407 
   408 use "Tools/Lifting/lifting_def.ML"
   409 
   410 use "Tools/Lifting/lifting_setup.ML"
   411 
   412 hide_const (open) invariant
   413 
   414 end