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