src/HOL/Lifting.thy
author huffman
Wed Apr 04 20:45:19 2012 +0200 (2012-04-04)
changeset 47369 f483be2fecb9
parent 47368 4c522dff1f4d
parent 47361 87c0eaf04bad
child 47376 776254f89a18
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 pred_compI)
   203     apply (rule Rep1)
   204     apply (rule Rep2)
   205     apply (rule pred_compI, assumption)
   206     apply (drule Abs1, simp)
   207     apply (clarsimp simp add: R2)
   208     apply (rule pred_compI, 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 pred_compI, assumption)
   214     apply (rule pred_compI [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 a type defined with @{text "typedef"}. *}
   301 
   302 lemma typedef_bi_unique:
   303   assumes type: "type_definition Rep Abs A"
   304   assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   305   shows "bi_unique T"
   306   unfolding bi_unique_def T_def
   307   by (simp add: type_definition.Rep_inject [OF type])
   308 
   309 lemma typedef_right_total:
   310   assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   311   shows "right_total T"
   312   unfolding right_total_def T_def by simp
   313 
   314 lemma copy_type_bi_total:
   315   assumes type: "type_definition Rep Abs UNIV"
   316   assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   317   shows "bi_total T"
   318   unfolding bi_total_def T_def
   319   by (metis type_definition.Abs_inverse [OF type] UNIV_I)
   320 
   321 lemma typedef_transfer_All:
   322   assumes type: "type_definition Rep Abs A"
   323   assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   324   shows "((T ===> op =) ===> op =) (Ball A) All"
   325   unfolding T_def fun_rel_def
   326   by (metis type_definition.Rep [OF type]
   327     type_definition.Abs_inverse [OF type])
   328 
   329 lemma typedef_transfer_Ex:
   330   assumes type: "type_definition Rep Abs A"
   331   assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   332   shows "((T ===> op =) ===> op =) (Bex A) Ex"
   333   unfolding T_def fun_rel_def
   334   by (metis type_definition.Rep [OF type]
   335     type_definition.Abs_inverse [OF type])
   336 
   337 lemma typedef_transfer_bforall:
   338   assumes type: "type_definition Rep Abs A"
   339   assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   340   shows "((T ===> op =) ===> op =)
   341     (transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall"
   342   unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric]
   343   by (rule typedef_transfer_All [OF assms])
   344 
   345 text {* Generating the correspondence rule for a constant defined with
   346   @{text "lift_definition"}. *}
   347 
   348 lemma Quotient_to_transfer:
   349   assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c"
   350   shows "T c c'"
   351   using assms by (auto dest: Quotient_cr_rel)
   352 
   353 subsection {* ML setup *}
   354 
   355 text {* Auxiliary data for the lifting package *}
   356 
   357 use "Tools/Lifting/lifting_info.ML"
   358 setup Lifting_Info.setup
   359 
   360 declare [[map "fun" = (fun_rel, fun_quotient)]]
   361 
   362 use "Tools/Lifting/lifting_term.ML"
   363 
   364 use "Tools/Lifting/lifting_def.ML"
   365 
   366 use "Tools/Lifting/lifting_setup.ML"
   367 
   368 hide_const (open) invariant
   369 
   370 end