src/HOL/Lifting.thy
author bulwahn
Thu Apr 12 11:01:15 2012 +0200 (2012-04-12)
changeset 47436 d8fad618a67a
parent 47376 776254f89a18
parent 47435 e1b761c216ac
child 47501 0b9294e093db
permissions -rw-r--r--
merged
     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 subsection {* Invariant *}
   222 
   223 definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
   224   where "invariant R = (\<lambda>x y. R x \<and> x = y)"
   225 
   226 lemma invariant_to_eq:
   227   assumes "invariant P x y"
   228   shows "x = y"
   229 using assms by (simp add: invariant_def)
   230 
   231 lemma fun_rel_eq_invariant:
   232   shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
   233 by (auto simp add: invariant_def fun_rel_def)
   234 
   235 lemma invariant_same_args:
   236   shows "invariant P x x \<equiv> P x"
   237 using assms by (auto simp add: invariant_def)
   238 
   239 lemma UNIV_typedef_to_Quotient:
   240   assumes "type_definition Rep Abs UNIV"
   241   and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   242   shows "Quotient (op =) Abs Rep T"
   243 proof -
   244   interpret type_definition Rep Abs UNIV by fact
   245   from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis 
   246     by (fastforce intro!: QuotientI fun_eq_iff)
   247 qed
   248 
   249 lemma UNIV_typedef_to_equivp:
   250   fixes Abs :: "'a \<Rightarrow> 'b"
   251   and Rep :: "'b \<Rightarrow> 'a"
   252   assumes "type_definition Rep Abs (UNIV::'a set)"
   253   shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)"
   254 by (rule identity_equivp)
   255 
   256 lemma typedef_to_Quotient:
   257   assumes "type_definition Rep Abs S"
   258   and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   259   shows "Quotient (Lifting.invariant (\<lambda>x. x \<in> S)) Abs Rep T"
   260 proof -
   261   interpret type_definition Rep Abs S by fact
   262   from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
   263     by (auto intro!: QuotientI simp: invariant_def fun_eq_iff)
   264 qed
   265 
   266 lemma typedef_to_part_equivp:
   267   assumes "type_definition Rep Abs S"
   268   shows "part_equivp (Lifting.invariant (\<lambda>x. x \<in> S))"
   269 proof (intro part_equivpI)
   270   interpret type_definition Rep Abs S by fact
   271   show "\<exists>x. Lifting.invariant (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: invariant_def)
   272 next
   273   show "symp (Lifting.invariant (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: invariant_def)
   274 next
   275   show "transp (Lifting.invariant (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: invariant_def)
   276 qed
   277 
   278 lemma open_typedef_to_Quotient:
   279   assumes "type_definition Rep Abs {x. P x}"
   280   and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   281   shows "Quotient (invariant P) Abs Rep T"
   282 proof -
   283   interpret type_definition Rep Abs "{x. P x}" by fact
   284   from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
   285     by (auto intro!: QuotientI simp: invariant_def fun_eq_iff)
   286 qed
   287 
   288 lemma open_typedef_to_part_equivp:
   289   assumes "type_definition Rep Abs {x. P x}"
   290   shows "part_equivp (invariant P)"
   291 proof (intro part_equivpI)
   292   interpret type_definition Rep Abs "{x. P x}" by fact
   293   show "\<exists>x. invariant P x x" using Rep by (auto simp: invariant_def)
   294 next
   295   show "symp (invariant P)" by (auto intro: sympI simp: invariant_def)
   296 next
   297   show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)
   298 qed
   299 
   300 text {* Generating transfer rules for quotients. *}
   301 
   302 lemma Quotient_right_unique:
   303   assumes "Quotient R Abs Rep T" shows "right_unique T"
   304   using assms unfolding Quotient_alt_def right_unique_def by metis
   305 
   306 lemma Quotient_right_total:
   307   assumes "Quotient R Abs Rep T" shows "right_total T"
   308   using assms unfolding Quotient_alt_def right_total_def by metis
   309 
   310 lemma Quotient_rel_eq_transfer:
   311   assumes "Quotient R Abs Rep T"
   312   shows "(T ===> T ===> op =) R (op =)"
   313   using assms unfolding Quotient_alt_def fun_rel_def by simp
   314 
   315 lemma Quotient_bi_total:
   316   assumes "Quotient R Abs Rep T" and "reflp R"
   317   shows "bi_total T"
   318   using assms unfolding Quotient_alt_def bi_total_def reflp_def by auto
   319 
   320 lemma Quotient_id_abs_transfer:
   321   assumes "Quotient R Abs Rep T" and "reflp R"
   322   shows "(op = ===> T) (\<lambda>x. x) Abs"
   323   using assms unfolding Quotient_alt_def reflp_def fun_rel_def by simp
   324 
   325 text {* Generating transfer rules for a type defined with @{text "typedef"}. *}
   326 
   327 lemma typedef_bi_unique:
   328   assumes type: "type_definition Rep Abs A"
   329   assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   330   shows "bi_unique T"
   331   unfolding bi_unique_def T_def
   332   by (simp add: type_definition.Rep_inject [OF type])
   333 
   334 lemma typedef_right_total:
   335   assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   336   shows "right_total T"
   337   unfolding right_total_def T_def by simp
   338 
   339 lemma copy_type_bi_total:
   340   assumes type: "type_definition Rep Abs UNIV"
   341   assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   342   shows "bi_total T"
   343   unfolding bi_total_def T_def
   344   by (metis type_definition.Abs_inverse [OF type] UNIV_I)
   345 
   346 lemma typedef_transfer_All:
   347   assumes type: "type_definition Rep Abs A"
   348   assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   349   shows "((T ===> op =) ===> op =) (Ball A) All"
   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_Ex:
   355   assumes type: "type_definition Rep Abs A"
   356   assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   357   shows "((T ===> op =) ===> op =) (Bex A) Ex"
   358   unfolding T_def fun_rel_def
   359   by (metis type_definition.Rep [OF type]
   360     type_definition.Abs_inverse [OF type])
   361 
   362 lemma typedef_transfer_bforall:
   363   assumes type: "type_definition Rep Abs A"
   364   assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   365   shows "((T ===> op =) ===> op =)
   366     (transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall"
   367   unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric]
   368   by (rule typedef_transfer_All [OF assms])
   369 
   370 text {* Generating the correspondence rule for a constant defined with
   371   @{text "lift_definition"}. *}
   372 
   373 lemma Quotient_to_transfer:
   374   assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c"
   375   shows "T c c'"
   376   using assms by (auto dest: Quotient_cr_rel)
   377 
   378 subsection {* ML setup *}
   379 
   380 text {* Auxiliary data for the lifting package *}
   381 
   382 use "Tools/Lifting/lifting_info.ML"
   383 setup Lifting_Info.setup
   384 
   385 declare [[map "fun" = (fun_rel, fun_quotient)]]
   386 
   387 use "Tools/Lifting/lifting_term.ML"
   388 
   389 use "Tools/Lifting/lifting_def.ML"
   390 
   391 use "Tools/Lifting/lifting_setup.ML"
   392 
   393 hide_const (open) invariant
   394 
   395 end