src/HOL/Lifting.thy
author huffman
Wed Apr 18 15:09:07 2012 +0200 (2012-04-18)
changeset 47538 1f0ec5b8135a
parent 47537 b06be48923a4
child 47544 e455cdaac479
permissions -rw-r--r--
add lemma Quotient_abs_induct
     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 context
   286   fixes R Abs Rep T
   287   assumes 1: "Quotient R Abs Rep T"
   288 begin
   289 
   290 lemma Quotient_right_unique: "right_unique T"
   291   using 1 unfolding Quotient_alt_def right_unique_def by metis
   292 
   293 lemma Quotient_right_total: "right_total T"
   294   using 1 unfolding Quotient_alt_def right_total_def by metis
   295 
   296 lemma Quotient_rel_eq_transfer: "(T ===> T ===> op =) R (op =)"
   297   using 1 unfolding Quotient_alt_def fun_rel_def by simp
   298 
   299 lemma Quotient_abs_induct:
   300   assumes "\<And>y. R y y \<Longrightarrow> P (Abs y)" shows "P x"
   301   using 1 assms unfolding Quotient_def by metis
   302 
   303 end
   304 
   305 text {* Generating transfer rules for total quotients. *}
   306 
   307 context
   308   fixes R Abs Rep T
   309   assumes 1: "Quotient R Abs Rep T" and 2: "reflp R"
   310 begin
   311 
   312 lemma Quotient_bi_total: "bi_total T"
   313   using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto
   314 
   315 lemma Quotient_id_abs_transfer: "(op = ===> T) (\<lambda>x. x) Abs"
   316   using 1 2 unfolding Quotient_alt_def reflp_def fun_rel_def by simp
   317 
   318 end
   319 
   320 text {* Generating transfer rules for a type defined with @{text "typedef"}. *}
   321 
   322 context
   323   fixes Rep Abs A T
   324   assumes type: "type_definition Rep Abs A"
   325   assumes T_def: "T \<equiv> (\<lambda>(x::'a) (y::'b). x = Rep y)"
   326 begin
   327 
   328 lemma typedef_bi_unique: "bi_unique T"
   329   unfolding bi_unique_def T_def
   330   by (simp add: type_definition.Rep_inject [OF type])
   331 
   332 lemma typedef_right_total: "right_total T"
   333   unfolding right_total_def T_def by simp
   334 
   335 lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep"
   336   unfolding fun_rel_def T_def by simp
   337 
   338 lemma typedef_transfer_All: "((T ===> op =) ===> op =) (Ball A) All"
   339   unfolding T_def fun_rel_def
   340   by (metis type_definition.Rep [OF type]
   341     type_definition.Abs_inverse [OF type])
   342 
   343 lemma typedef_transfer_Ex: "((T ===> op =) ===> op =) (Bex A) Ex"
   344   unfolding T_def fun_rel_def
   345   by (metis type_definition.Rep [OF type]
   346     type_definition.Abs_inverse [OF type])
   347 
   348 lemma typedef_transfer_bforall:
   349   "((T ===> op =) ===> op =)
   350     (transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall"
   351   unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric]
   352   by (rule typedef_transfer_All)
   353 
   354 end
   355 
   356 text {* Generating transfer rules for a type copy. *}
   357 
   358 lemma copy_type_bi_total:
   359   assumes type: "type_definition Rep Abs UNIV"
   360   assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   361   shows "bi_total T"
   362   unfolding bi_total_def T_def
   363   by (metis type_definition.Abs_inverse [OF type] UNIV_I)
   364 
   365 text {* Generating the correspondence rule for a constant defined with
   366   @{text "lift_definition"}. *}
   367 
   368 lemma Quotient_to_transfer:
   369   assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c"
   370   shows "T c c'"
   371   using assms by (auto dest: Quotient_cr_rel)
   372 
   373 subsection {* ML setup *}
   374 
   375 text {* Auxiliary data for the lifting package *}
   376 
   377 use "Tools/Lifting/lifting_info.ML"
   378 setup Lifting_Info.setup
   379 
   380 declare [[map "fun" = (fun_rel, fun_quotient)]]
   381 
   382 use "Tools/Lifting/lifting_term.ML"
   383 
   384 use "Tools/Lifting/lifting_def.ML"
   385 
   386 use "Tools/Lifting/lifting_setup.ML"
   387 
   388 hide_const (open) invariant
   389 
   390 end