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