src/HOL/Lifting.thy
 author huffman Wed Apr 18 10:52:49 2012 +0200 (2012-04-18) changeset 47534 06cc372a80ed parent 47521 69f95ac85c3d child 47535 0f94b02fda1c permissions -rw-r--r--
use context block to organize typedef lifting theorems
```     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 lemma Quotient_abs_rep:
```
```    47   assumes a: "Quotient R Abs Rep T"
```
```    48   shows "Abs (Rep a) = a"
```
```    49   using a
```
```    50   unfolding Quotient_def
```
```    51   by simp
```
```    52
```
```    53 lemma Quotient_rep_reflp:
```
```    54   assumes a: "Quotient R Abs Rep T"
```
```    55   shows "R (Rep a) (Rep a)"
```
```    56   using a
```
```    57   unfolding Quotient_def
```
```    58   by blast
```
```    59
```
```    60 lemma Quotient_rel:
```
```    61   assumes a: "Quotient R Abs Rep T"
```
```    62   shows "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
```
```    63   using a
```
```    64   unfolding Quotient_def
```
```    65   by blast
```
```    66
```
```    67 lemma Quotient_cr_rel:
```
```    68   assumes a: "Quotient R Abs Rep T"
```
```    69   shows "T = (\<lambda>x y. R x x \<and> Abs x = y)"
```
```    70   using a
```
```    71   unfolding Quotient_def
```
```    72   by blast
```
```    73
```
```    74 lemma Quotient_refl1:
```
```    75   assumes a: "Quotient R Abs Rep T"
```
```    76   shows "R r s \<Longrightarrow> R r r"
```
```    77   using a unfolding Quotient_def
```
```    78   by fast
```
```    79
```
```    80 lemma Quotient_refl2:
```
```    81   assumes a: "Quotient R Abs Rep T"
```
```    82   shows "R r s \<Longrightarrow> R s s"
```
```    83   using a unfolding Quotient_def
```
```    84   by fast
```
```    85
```
```    86 lemma Quotient_rel_rep:
```
```    87   assumes a: "Quotient R Abs Rep T"
```
```    88   shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
```
```    89   using a
```
```    90   unfolding Quotient_def
```
```    91   by metis
```
```    92
```
```    93 lemma Quotient_rep_abs:
```
```    94   assumes a: "Quotient R Abs Rep T"
```
```    95   shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
```
```    96   using a unfolding Quotient_def
```
```    97   by blast
```
```    98
```
```    99 lemma Quotient_rel_abs:
```
```   100   assumes a: "Quotient R Abs Rep T"
```
```   101   shows "R r s \<Longrightarrow> Abs r = Abs s"
```
```   102   using a unfolding Quotient_def
```
```   103   by blast
```
```   104
```
```   105 lemma Quotient_symp:
```
```   106   assumes a: "Quotient R Abs Rep T"
```
```   107   shows "symp R"
```
```   108   using a unfolding Quotient_def using sympI by (metis (full_types))
```
```   109
```
```   110 lemma Quotient_transp:
```
```   111   assumes a: "Quotient R Abs Rep T"
```
```   112   shows "transp R"
```
```   113   using a unfolding Quotient_def using transpI by (metis (full_types))
```
```   114
```
```   115 lemma Quotient_part_equivp:
```
```   116   assumes a: "Quotient R Abs Rep T"
```
```   117   shows "part_equivp R"
```
```   118 by (metis Quotient_rep_reflp Quotient_symp Quotient_transp a part_equivpI)
```
```   119
```
```   120 lemma identity_quotient: "Quotient (op =) id id (op =)"
```
```   121 unfolding Quotient_def by simp
```
```   122
```
```   123 lemma Quotient_alt_def:
```
```   124   "Quotient R Abs Rep T \<longleftrightarrow>
```
```   125     (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and>
```
```   126     (\<forall>b. T (Rep b) b) \<and>
```
```   127     (\<forall>x y. R x y \<longleftrightarrow> T x (Abs x) \<and> T y (Abs y) \<and> Abs x = Abs y)"
```
```   128 apply safe
```
```   129 apply (simp (no_asm_use) only: Quotient_def, fast)
```
```   130 apply (simp (no_asm_use) only: Quotient_def, fast)
```
```   131 apply (simp (no_asm_use) only: Quotient_def, fast)
```
```   132 apply (simp (no_asm_use) only: Quotient_def, fast)
```
```   133 apply (simp (no_asm_use) only: Quotient_def, fast)
```
```   134 apply (simp (no_asm_use) only: Quotient_def, fast)
```
```   135 apply (rule QuotientI)
```
```   136 apply simp
```
```   137 apply metis
```
```   138 apply simp
```
```   139 apply (rule ext, rule ext, metis)
```
```   140 done
```
```   141
```
```   142 lemma Quotient_alt_def2:
```
```   143   "Quotient R Abs Rep T \<longleftrightarrow>
```
```   144     (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and>
```
```   145     (\<forall>b. T (Rep b) b) \<and>
```
```   146     (\<forall>x y. R x y \<longleftrightarrow> T x (Abs y) \<and> T y (Abs x))"
```
```   147   unfolding Quotient_alt_def by (safe, metis+)
```
```   148
```
```   149 lemma fun_quotient:
```
```   150   assumes 1: "Quotient R1 abs1 rep1 T1"
```
```   151   assumes 2: "Quotient R2 abs2 rep2 T2"
```
```   152   shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2) (T1 ===> T2)"
```
```   153   using assms unfolding Quotient_alt_def2
```
```   154   unfolding fun_rel_def fun_eq_iff map_fun_apply
```
```   155   by (safe, metis+)
```
```   156
```
```   157 lemma apply_rsp:
```
```   158   fixes f g::"'a \<Rightarrow> 'c"
```
```   159   assumes q: "Quotient R1 Abs1 Rep1 T1"
```
```   160   and     a: "(R1 ===> R2) f g" "R1 x y"
```
```   161   shows "R2 (f x) (g y)"
```
```   162   using a by (auto elim: fun_relE)
```
```   163
```
```   164 lemma apply_rsp':
```
```   165   assumes a: "(R1 ===> R2) f g" "R1 x y"
```
```   166   shows "R2 (f x) (g y)"
```
```   167   using a by (auto elim: fun_relE)
```
```   168
```
```   169 lemma apply_rsp'':
```
```   170   assumes "Quotient R Abs Rep T"
```
```   171   and "(R ===> S) f f"
```
```   172   shows "S (f (Rep x)) (f (Rep x))"
```
```   173 proof -
```
```   174   from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp)
```
```   175   then show ?thesis using assms(2) by (auto intro: apply_rsp')
```
```   176 qed
```
```   177
```
```   178 subsection {* Quotient composition *}
```
```   179
```
```   180 lemma Quotient_compose:
```
```   181   assumes 1: "Quotient R1 Abs1 Rep1 T1"
```
```   182   assumes 2: "Quotient R2 Abs2 Rep2 T2"
```
```   183   shows "Quotient (T1 OO R2 OO conversep T1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2) (T1 OO T2)"
```
```   184 proof -
```
```   185   from 1 have Abs1: "\<And>a b. T1 a b \<Longrightarrow> Abs1 a = b"
```
```   186     unfolding Quotient_alt_def by simp
```
```   187   from 1 have Rep1: "\<And>b. T1 (Rep1 b) b"
```
```   188     unfolding Quotient_alt_def by simp
```
```   189   from 2 have Abs2: "\<And>a b. T2 a b \<Longrightarrow> Abs2 a = b"
```
```   190     unfolding Quotient_alt_def by simp
```
```   191   from 2 have Rep2: "\<And>b. T2 (Rep2 b) b"
```
```   192     unfolding Quotient_alt_def by simp
```
```   193   from 2 have R2:
```
```   194     "\<And>x y. R2 x y \<longleftrightarrow> T2 x (Abs2 x) \<and> T2 y (Abs2 y) \<and> Abs2 x = Abs2 y"
```
```   195     unfolding Quotient_alt_def by simp
```
```   196   show ?thesis
```
```   197     unfolding Quotient_alt_def
```
```   198     apply simp
```
```   199     apply safe
```
```   200     apply (drule Abs1, simp)
```
```   201     apply (erule Abs2)
```
```   202     apply (rule relcomppI)
```
```   203     apply (rule Rep1)
```
```   204     apply (rule Rep2)
```
```   205     apply (rule relcomppI, assumption)
```
```   206     apply (drule Abs1, simp)
```
```   207     apply (clarsimp simp add: R2)
```
```   208     apply (rule relcomppI, assumption)
```
```   209     apply (drule Abs1, simp)+
```
```   210     apply (clarsimp simp add: R2)
```
```   211     apply (drule Abs1, simp)+
```
```   212     apply (clarsimp simp add: R2)
```
```   213     apply (rule relcomppI, assumption)
```
```   214     apply (rule relcomppI [rotated])
```
```   215     apply (erule conversepI)
```
```   216     apply (drule Abs1, simp)+
```
```   217     apply (simp add: R2)
```
```   218     done
```
```   219 qed
```
```   220
```
```   221 lemma equivp_reflp2:
```
```   222   "equivp R \<Longrightarrow> reflp R"
```
```   223   by (erule equivpE)
```
```   224
```
```   225 subsection {* Invariant *}
```
```   226
```
```   227 definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
```
```   228   where "invariant R = (\<lambda>x y. R x \<and> x = y)"
```
```   229
```
```   230 lemma invariant_to_eq:
```
```   231   assumes "invariant P x y"
```
```   232   shows "x = y"
```
```   233 using assms by (simp add: invariant_def)
```
```   234
```
```   235 lemma fun_rel_eq_invariant:
```
```   236   shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
```
```   237 by (auto simp add: invariant_def fun_rel_def)
```
```   238
```
```   239 lemma invariant_same_args:
```
```   240   shows "invariant P x x \<equiv> P x"
```
```   241 using assms by (auto simp add: invariant_def)
```
```   242
```
```   243 lemma UNIV_typedef_to_Quotient:
```
```   244   assumes "type_definition Rep Abs UNIV"
```
```   245   and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
```
```   246   shows "Quotient (op =) Abs Rep T"
```
```   247 proof -
```
```   248   interpret type_definition Rep Abs UNIV by fact
```
```   249   from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
```
```   250     by (fastforce intro!: QuotientI fun_eq_iff)
```
```   251 qed
```
```   252
```
```   253 lemma UNIV_typedef_to_equivp:
```
```   254   fixes Abs :: "'a \<Rightarrow> 'b"
```
```   255   and Rep :: "'b \<Rightarrow> 'a"
```
```   256   assumes "type_definition Rep Abs (UNIV::'a set)"
```
```   257   shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)"
```
```   258 by (rule identity_equivp)
```
```   259
```
```   260 lemma typedef_to_Quotient:
```
```   261   assumes "type_definition Rep Abs S"
```
```   262   and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
```
```   263   shows "Quotient (invariant (\<lambda>x. x \<in> S)) Abs Rep T"
```
```   264 proof -
```
```   265   interpret type_definition Rep Abs S by fact
```
```   266   from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
```
```   267     by (auto intro!: QuotientI simp: invariant_def fun_eq_iff)
```
```   268 qed
```
```   269
```
```   270 lemma typedef_to_part_equivp:
```
```   271   assumes "type_definition Rep Abs S"
```
```   272   shows "part_equivp (invariant (\<lambda>x. x \<in> S))"
```
```   273 proof (intro part_equivpI)
```
```   274   interpret type_definition Rep Abs S by fact
```
```   275   show "\<exists>x. invariant (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: invariant_def)
```
```   276 next
```
```   277   show "symp (invariant (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: invariant_def)
```
```   278 next
```
```   279   show "transp (invariant (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: invariant_def)
```
```   280 qed
```
```   281
```
```   282 lemma open_typedef_to_Quotient:
```
```   283   assumes "type_definition Rep Abs {x. P x}"
```
```   284   and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
```
```   285   shows "Quotient (invariant P) Abs Rep T"
```
```   286 proof -
```
```   287   interpret type_definition Rep Abs "{x. P x}" by fact
```
```   288   from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
```
```   289     by (auto intro!: QuotientI simp: invariant_def fun_eq_iff)
```
```   290 qed
```
```   291
```
```   292 lemma open_typedef_to_part_equivp:
```
```   293   assumes "type_definition Rep Abs {x. P x}"
```
```   294   shows "part_equivp (invariant P)"
```
```   295 proof (intro part_equivpI)
```
```   296   interpret type_definition Rep Abs "{x. P x}" by fact
```
```   297   show "\<exists>x. invariant P x x" using Rep by (auto simp: invariant_def)
```
```   298 next
```
```   299   show "symp (invariant P)" by (auto intro: sympI simp: invariant_def)
```
```   300 next
```
```   301   show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)
```
```   302 qed
```
```   303
```
```   304 text {* Generating transfer rules for quotients. *}
```
```   305
```
```   306 lemma Quotient_right_unique:
```
```   307   assumes "Quotient R Abs Rep T" shows "right_unique T"
```
```   308   using assms unfolding Quotient_alt_def right_unique_def by metis
```
```   309
```
```   310 lemma Quotient_right_total:
```
```   311   assumes "Quotient R Abs Rep T" shows "right_total T"
```
```   312   using assms unfolding Quotient_alt_def right_total_def by metis
```
```   313
```
```   314 lemma Quotient_rel_eq_transfer:
```
```   315   assumes "Quotient R Abs Rep T"
```
```   316   shows "(T ===> T ===> op =) R (op =)"
```
```   317   using assms unfolding Quotient_alt_def fun_rel_def by simp
```
```   318
```
```   319 lemma Quotient_bi_total:
```
```   320   assumes "Quotient R Abs Rep T" and "reflp R"
```
```   321   shows "bi_total T"
```
```   322   using assms unfolding Quotient_alt_def bi_total_def reflp_def by auto
```
```   323
```
```   324 lemma Quotient_id_abs_transfer:
```
```   325   assumes "Quotient R Abs Rep T" and "reflp R"
```
```   326   shows "(op = ===> T) (\<lambda>x. x) Abs"
```
```   327   using assms unfolding Quotient_alt_def reflp_def fun_rel_def by simp
```
```   328
```
```   329 text {* Generating transfer rules for a type defined with @{text "typedef"}. *}
```
```   330
```
```   331 context
```
```   332   fixes Rep Abs A T
```
```   333   assumes type: "type_definition Rep Abs A"
```
```   334   assumes T_def: "T \<equiv> (\<lambda>(x::'a) (y::'b). x = Rep y)"
```
```   335 begin
```
```   336
```
```   337 lemma typedef_bi_unique: "bi_unique T"
```
```   338   unfolding bi_unique_def T_def
```
```   339   by (simp add: type_definition.Rep_inject [OF type])
```
```   340
```
```   341 lemma typedef_right_total: "right_total T"
```
```   342   unfolding right_total_def T_def by simp
```
```   343
```
```   344 lemma typedef_transfer_All: "((T ===> op =) ===> op =) (Ball A) All"
```
```   345   unfolding T_def fun_rel_def
```
```   346   by (metis type_definition.Rep [OF type]
```
```   347     type_definition.Abs_inverse [OF type])
```
```   348
```
```   349 lemma typedef_transfer_Ex: "((T ===> op =) ===> op =) (Bex A) Ex"
```
```   350   unfolding T_def fun_rel_def
```
```   351   by (metis type_definition.Rep [OF type]
```
```   352     type_definition.Abs_inverse [OF type])
```
```   353
```
```   354 lemma typedef_transfer_bforall:
```
```   355   "((T ===> op =) ===> op =)
```
```   356     (transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall"
```
```   357   unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric]
```
```   358   by (rule typedef_transfer_All [OF assms])
```
```   359
```
```   360 end
```
```   361
```
```   362 lemma copy_type_bi_total:
```
```   363   assumes type: "type_definition Rep Abs UNIV"
```
```   364   assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
```
```   365   shows "bi_total T"
```
```   366   unfolding bi_total_def T_def
```
```   367   by (metis type_definition.Abs_inverse [OF type] UNIV_I)
```
```   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
```