simplify and fix theories thanks to 356a5efdb278
authorkuncar
Thu Apr 10 17:48:32 2014 +0200 (2014-04-10)
changeset 56525b5b6ad5dc2ae
parent 56524 f4ba736040fa
child 56526 58ac520db7ae
simplify and fix theories thanks to 356a5efdb278
src/HOL/Int.thy
src/HOL/Library/FSet.thy
src/HOL/Library/Quotient_Option.thy
src/HOL/Lifting_Option.thy
src/HOL/Lifting_Product.thy
src/HOL/Lifting_Sum.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/Int.thy	Thu Apr 10 17:48:18 2014 +0200
     1.2 +++ b/src/HOL/Int.thy	Thu Apr 10 17:48:32 2014 +0200
     1.3 @@ -78,8 +78,8 @@
     1.4      simp add: one_int.abs_eq plus_int.abs_eq)
     1.5  
     1.6  lemma int_transfer [transfer_rule]:
     1.7 -  "(rel_fun (op =) cr_int) (\<lambda>n. (n, 0)) int"
     1.8 -  unfolding rel_fun_def cr_int_def int_def by simp
     1.9 +  "(rel_fun (op =) pcr_int) (\<lambda>n. (n, 0)) int"
    1.10 +  unfolding rel_fun_def int.pcr_cr_eq cr_int_def int_def by simp
    1.11  
    1.12  lemma int_diff_cases:
    1.13    obtains (diff) m n where "z = int m - int n"
     2.1 --- a/src/HOL/Library/FSet.thy	Thu Apr 10 17:48:18 2014 +0200
     2.2 +++ b/src/HOL/Library/FSet.thy	Thu Apr 10 17:48:32 2014 +0200
     2.3 @@ -772,14 +772,6 @@
     2.4  apply (subst rel_set_def[unfolded fun_eq_iff]) 
     2.5  by blast
     2.6  
     2.7 -lemma rel_fset_conversep: "rel_fset (conversep R) = conversep (rel_fset R)"
     2.8 -  unfolding rel_fset_alt_def by auto
     2.9 -
    2.10 -lemmas rel_fset_eq [relator_eq] = rel_set_eq[Transfer.transferred]
    2.11 -
    2.12 -lemma rel_fset_mono[relator_mono]: "A \<le> B \<Longrightarrow> rel_fset A \<le> rel_fset B"
    2.13 -unfolding rel_fset_alt_def by blast
    2.14 -
    2.15  lemma finite_rel_set:
    2.16    assumes fin: "finite X" "finite Z"
    2.17    assumes R_S: "rel_set (R OO S) X Z"
    2.18 @@ -806,63 +798,6 @@
    2.19    ultimately show ?thesis by metis
    2.20  qed
    2.21  
    2.22 -lemma rel_fset_OO[relator_distr]: "rel_fset R OO rel_fset S = rel_fset (R OO S)"
    2.23 -apply (rule ext)+
    2.24 -by transfer (auto intro: finite_rel_set rel_set_OO[unfolded fun_eq_iff, rule_format, THEN iffD1])
    2.25 -
    2.26 -lemma Domainp_fset[relator_domain]: "Domainp (rel_fset T) = (\<lambda>A. fBall A (Domainp T))"
    2.27 -proof -
    2.28 -  obtain f where f: "\<forall>x\<in>Collect (Domainp T). T x (f x)"
    2.29 -    unfolding Domainp_iff[abs_def]
    2.30 -    apply atomize_elim
    2.31 -    by (subst bchoice_iff[symmetric]) (auto iff: bchoice_iff[symmetric])
    2.32 -  from f show ?thesis
    2.33 -    unfolding fun_eq_iff rel_fset_alt_def Domainp_iff
    2.34 -    apply clarify
    2.35 -    apply (rule iffI)
    2.36 -      apply blast
    2.37 -    by (rename_tac A, rule_tac x="f |`| A" in exI, blast)
    2.38 -qed
    2.39 -
    2.40 -lemma right_total_rel_fset[transfer_rule]: "right_total A \<Longrightarrow> right_total (rel_fset A)"
    2.41 -unfolding right_total_def 
    2.42 -apply transfer
    2.43 -apply (subst(asm) choice_iff)
    2.44 -apply clarsimp
    2.45 -apply (rename_tac A f y, rule_tac x = "f ` y" in exI)
    2.46 -by (auto simp add: rel_set_def)
    2.47 -
    2.48 -lemma left_total_rel_fset[transfer_rule]: "left_total A \<Longrightarrow> left_total (rel_fset A)"
    2.49 -unfolding left_total_def 
    2.50 -apply transfer
    2.51 -apply (subst(asm) choice_iff)
    2.52 -apply clarsimp
    2.53 -apply (rename_tac A f y, rule_tac x = "f ` y" in exI)
    2.54 -by (auto simp add: rel_set_def)
    2.55 -
    2.56 -lemmas right_unique_rel_fset[transfer_rule] = right_unique_rel_set[Transfer.transferred]
    2.57 -lemmas left_unique_rel_fset[transfer_rule] = left_unique_rel_set[Transfer.transferred]
    2.58 -
    2.59 -thm right_unique_rel_fset left_unique_rel_fset
    2.60 -
    2.61 -lemma bi_unique_rel_fset[transfer_rule]: "bi_unique A \<Longrightarrow> bi_unique (rel_fset A)"
    2.62 -by (auto intro: right_unique_rel_fset left_unique_rel_fset iff: bi_unique_alt_def)
    2.63 -
    2.64 -lemma bi_total_rel_fset[transfer_rule]: "bi_total A \<Longrightarrow> bi_total (rel_fset A)"
    2.65 -by (auto intro: right_total_rel_fset left_total_rel_fset iff: bi_total_alt_def)
    2.66 -
    2.67 -lemmas fset_relator_eq_onp [relator_eq_onp] = set_relator_eq_onp[Transfer.transferred]
    2.68 -
    2.69 -
    2.70 -subsubsection {* Quotient theorem for the Lifting package *}
    2.71 -
    2.72 -lemma Quotient_fset_map[quot_map]:
    2.73 -  assumes "Quotient R Abs Rep T"
    2.74 -  shows "Quotient (rel_fset R) (fimage Abs) (fimage Rep) (rel_fset T)"
    2.75 -  using assms unfolding Quotient_alt_def4
    2.76 -  by (simp add: rel_fset_OO[symmetric] rel_fset_conversep) (simp add: rel_fset_alt_def, blast)
    2.77 -
    2.78 -
    2.79  subsubsection {* Transfer rules for the Transfer package *}
    2.80  
    2.81  text {* Unconditional transfer rules *}
     3.1 --- a/src/HOL/Library/Quotient_Option.thy	Thu Apr 10 17:48:18 2014 +0200
     3.2 +++ b/src/HOL/Library/Quotient_Option.thy	Thu Apr 10 17:48:32 2014 +0200
     3.3 @@ -20,7 +20,7 @@
     3.4  
     3.5  declare
     3.6    map_option.id [id_simps]
     3.7 -  rel_option_eq [id_simps]
     3.8 +  option.rel_eq [id_simps]
     3.9  
    3.10  lemma reflp_rel_option:
    3.11    "reflp R \<Longrightarrow> reflp (rel_option R)"
    3.12 @@ -44,7 +44,7 @@
    3.13    assumes "Quotient3 R Abs Rep"
    3.14    shows "Quotient3 (rel_option R) (map_option Abs) (map_option Rep)"
    3.15    apply (rule Quotient3I)
    3.16 -  apply (simp_all add: option.map_comp comp_def option.map_id[unfolded id_def] rel_option_eq rel_option_map1 rel_option_map2 Quotient3_abs_rep [OF assms] Quotient3_rel_rep [OF assms])
    3.17 +  apply (simp_all add: option.map_comp comp_def option.map_id[unfolded id_def] option.rel_eq rel_option_map1 rel_option_map2 Quotient3_abs_rep [OF assms] Quotient3_rel_rep [OF assms])
    3.18    using Quotient3_rel [OF assms]
    3.19    apply (simp add: rel_option_iff split: option.split)
    3.20    done
     4.1 --- a/src/HOL/Lifting_Option.thy	Thu Apr 10 17:48:18 2014 +0200
     4.2 +++ b/src/HOL/Lifting_Option.thy	Thu Apr 10 17:48:32 2014 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  header {* Setup for Lifting/Transfer for the option type *}
     4.5  
     4.6  theory Lifting_Option
     4.7 -imports Lifting Partial_Function
     4.8 +imports Lifting Option
     4.9  begin
    4.10  
    4.11  subsection {* Relator and predicator properties *}
    4.12 @@ -17,64 +17,6 @@
    4.13      | _ \<Rightarrow> False)"
    4.14  by (auto split: prod.split option.split)
    4.15  
    4.16 -abbreviation (input) pred_option :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" where
    4.17 -  "pred_option \<equiv> case_option True"
    4.18 -
    4.19 -lemma rel_option_eq [relator_eq]:
    4.20 -  "rel_option (op =) = (op =)"
    4.21 -  by (simp add: rel_option_iff fun_eq_iff split: option.split)
    4.22 -
    4.23 -lemma rel_option_mono[relator_mono]:
    4.24 -  assumes "A \<le> B"
    4.25 -  shows "(rel_option A) \<le> (rel_option B)"
    4.26 -using assms by (auto simp: rel_option_iff split: option.splits)
    4.27 -
    4.28 -lemma rel_option_OO[relator_distr]:
    4.29 -  "(rel_option A) OO (rel_option B) = rel_option (A OO B)"
    4.30 -by (rule ext)+ (auto simp: rel_option_iff OO_def split: option.split)
    4.31 -
    4.32 -lemma Domainp_option[relator_domain]: 
    4.33 -  "Domainp (rel_option A) = (pred_option (Domainp A))"
    4.34 -unfolding Domainp_iff[abs_def] rel_option_iff[abs_def]
    4.35 -by (auto iff: fun_eq_iff split: option.split)
    4.36 -
    4.37 -lemma left_total_rel_option[transfer_rule]:
    4.38 -  "left_total R \<Longrightarrow> left_total (rel_option R)"
    4.39 -  unfolding left_total_def split_option_all split_option_ex by simp
    4.40 -
    4.41 -lemma left_unique_rel_option [transfer_rule]:
    4.42 -  "left_unique R \<Longrightarrow> left_unique (rel_option R)"
    4.43 -  unfolding left_unique_def split_option_all by simp
    4.44 -
    4.45 -lemma right_total_rel_option [transfer_rule]:
    4.46 -  "right_total R \<Longrightarrow> right_total (rel_option R)"
    4.47 -  unfolding right_total_def split_option_all split_option_ex by simp
    4.48 -
    4.49 -lemma right_unique_rel_option [transfer_rule]:
    4.50 -  "right_unique R \<Longrightarrow> right_unique (rel_option R)"
    4.51 -  unfolding right_unique_def split_option_all by simp
    4.52 -
    4.53 -lemma bi_total_rel_option [transfer_rule]:
    4.54 -  "bi_total R \<Longrightarrow> bi_total (rel_option R)"
    4.55 -  unfolding bi_total_def split_option_all split_option_ex by simp
    4.56 -
    4.57 -lemma bi_unique_rel_option [transfer_rule]:
    4.58 -  "bi_unique R \<Longrightarrow> bi_unique (rel_option R)"
    4.59 -  unfolding bi_unique_def split_option_all by simp
    4.60 -
    4.61 -lemma option_relator_eq_onp [relator_eq_onp]:
    4.62 -  "rel_option (eq_onp P) = eq_onp (pred_option P)"
    4.63 -  by (auto simp add: fun_eq_iff eq_onp_def split_option_all)
    4.64 -
    4.65 -subsection {* Quotient theorem for the Lifting package *}
    4.66 -
    4.67 -lemma Quotient_option[quot_map]:
    4.68 -  assumes "Quotient R Abs Rep T"
    4.69 -  shows "Quotient (rel_option R) (map_option Abs)
    4.70 -    (map_option Rep) (rel_option T)"
    4.71 -  using assms unfolding Quotient_alt_def rel_option_iff
    4.72 -  by (simp split: option.split)
    4.73 -
    4.74  subsection {* Transfer rules for the Transfer package *}
    4.75  
    4.76  context
     5.1 --- a/src/HOL/Lifting_Product.thy	Thu Apr 10 17:48:18 2014 +0200
     5.2 +++ b/src/HOL/Lifting_Product.thy	Thu Apr 10 17:48:32 2014 +0200
     5.3 @@ -8,69 +8,6 @@
     5.4  imports Lifting Basic_BNFs
     5.5  begin
     5.6  
     5.7 -subsection {* Relator and predicator properties *}
     5.8 -
     5.9 -definition pred_prod :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    5.10 -where "pred_prod R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
    5.11 -
    5.12 -lemma pred_prod_apply [simp]:
    5.13 -  "pred_prod P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
    5.14 -  by (simp add: pred_prod_def)
    5.15 -
    5.16 -lemmas rel_prod_eq[relator_eq] = prod.rel_eq
    5.17 -lemmas rel_prod_mono[relator_mono] = prod.rel_mono
    5.18 -
    5.19 -lemma rel_prod_OO[relator_distr]:
    5.20 -  "(rel_prod A B) OO (rel_prod C D) = rel_prod (A OO C) (B OO D)"
    5.21 -by (rule ext)+ (auto simp: rel_prod_def OO_def)
    5.22 -
    5.23 -lemma Domainp_prod[relator_domain]: 
    5.24 -  "Domainp (rel_prod T1 T2) = (pred_prod (Domainp T1) (Domainp T2))"
    5.25 -unfolding rel_prod_def pred_prod_def by blast
    5.26 -
    5.27 -lemma left_total_rel_prod [transfer_rule]:
    5.28 -  assumes "left_total R1"
    5.29 -  assumes "left_total R2"
    5.30 -  shows "left_total (rel_prod R1 R2)"
    5.31 -  using assms unfolding left_total_def rel_prod_def by auto
    5.32 -
    5.33 -lemma left_unique_rel_prod [transfer_rule]:
    5.34 -  assumes "left_unique R1" and "left_unique R2"
    5.35 -  shows "left_unique (rel_prod R1 R2)"
    5.36 -  using assms unfolding left_unique_def rel_prod_def by auto
    5.37 -
    5.38 -lemma right_total_rel_prod [transfer_rule]:
    5.39 -  assumes "right_total R1" and "right_total R2"
    5.40 -  shows "right_total (rel_prod R1 R2)"
    5.41 -  using assms unfolding right_total_def rel_prod_def by auto
    5.42 -
    5.43 -lemma right_unique_rel_prod [transfer_rule]:
    5.44 -  assumes "right_unique R1" and "right_unique R2"
    5.45 -  shows "right_unique (rel_prod R1 R2)"
    5.46 -  using assms unfolding right_unique_def rel_prod_def by auto
    5.47 -
    5.48 -lemma bi_total_rel_prod [transfer_rule]:
    5.49 -  assumes "bi_total R1" and "bi_total R2"
    5.50 -  shows "bi_total (rel_prod R1 R2)"
    5.51 -  using assms unfolding bi_total_def rel_prod_def by auto
    5.52 -
    5.53 -lemma bi_unique_rel_prod [transfer_rule]:
    5.54 -  assumes "bi_unique R1" and "bi_unique R2"
    5.55 -  shows "bi_unique (rel_prod R1 R2)"
    5.56 -  using assms unfolding bi_unique_def rel_prod_def by auto
    5.57 -
    5.58 -lemma prod_relator_eq_onp [relator_eq_onp]: 
    5.59 -  "rel_prod (eq_onp P1) (eq_onp P2) = eq_onp (pred_prod P1 P2)"
    5.60 -  by (simp add: fun_eq_iff rel_prod_def pred_prod_def eq_onp_def) blast
    5.61 -
    5.62 -subsection {* Quotient theorem for the Lifting package *}
    5.63 -
    5.64 -lemma Quotient_prod[quot_map]:
    5.65 -  assumes "Quotient R1 Abs1 Rep1 T1"
    5.66 -  assumes "Quotient R2 Abs2 Rep2 T2"
    5.67 -  shows "Quotient (rel_prod R1 R2) (map_prod Abs1 Abs2) (map_prod Rep1 Rep2) (rel_prod T1 T2)"
    5.68 -  using assms unfolding Quotient_alt_def by auto
    5.69 -
    5.70  subsection {* Transfer rules for the Transfer package *}
    5.71  
    5.72  context
     6.1 --- a/src/HOL/Lifting_Sum.thy	Thu Apr 10 17:48:18 2014 +0200
     6.2 +++ b/src/HOL/Lifting_Sum.thy	Thu Apr 10 17:48:32 2014 +0200
     6.3 @@ -8,58 +8,6 @@
     6.4  imports Lifting Basic_BNFs
     6.5  begin
     6.6  
     6.7 -subsection {* Relator and predicator properties *}
     6.8 -
     6.9 -abbreviation (input) "sum_pred \<equiv> case_sum"
    6.10 -
    6.11 -lemmas rel_sum_eq[relator_eq] = sum.rel_eq
    6.12 -lemmas rel_sum_mono[relator_mono] = sum.rel_mono
    6.13 -
    6.14 -lemma rel_sum_OO[relator_distr]:
    6.15 -  "(rel_sum A B) OO (rel_sum C D) = rel_sum (A OO C) (B OO D)"
    6.16 -  by (rule ext)+ (auto simp add: rel_sum_def OO_def split_sum_ex split: sum.split)
    6.17 -
    6.18 -lemma Domainp_sum[relator_domain]:
    6.19 -  "Domainp (rel_sum R1 R2) = (sum_pred (Domainp R1) (Domainp R2))"
    6.20 -by (auto simp add: Domainp_iff split_sum_ex iff: fun_eq_iff split: sum.split)
    6.21 -
    6.22 -lemma left_total_rel_sum[transfer_rule]:
    6.23 -  "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (rel_sum R1 R2)"
    6.24 -  using assms unfolding left_total_def split_sum_all split_sum_ex by simp
    6.25 -
    6.26 -lemma left_unique_rel_sum [transfer_rule]:
    6.27 -  "left_unique R1 \<Longrightarrow> left_unique R2 \<Longrightarrow> left_unique (rel_sum R1 R2)"
    6.28 -  using assms unfolding left_unique_def split_sum_all by simp
    6.29 -
    6.30 -lemma right_total_rel_sum [transfer_rule]:
    6.31 -  "right_total R1 \<Longrightarrow> right_total R2 \<Longrightarrow> right_total (rel_sum R1 R2)"
    6.32 -  unfolding right_total_def split_sum_all split_sum_ex by simp
    6.33 -
    6.34 -lemma right_unique_rel_sum [transfer_rule]:
    6.35 -  "right_unique R1 \<Longrightarrow> right_unique R2 \<Longrightarrow> right_unique (rel_sum R1 R2)"
    6.36 -  unfolding right_unique_def split_sum_all by simp
    6.37 -
    6.38 -lemma bi_total_rel_sum [transfer_rule]:
    6.39 -  "bi_total R1 \<Longrightarrow> bi_total R2 \<Longrightarrow> bi_total (rel_sum R1 R2)"
    6.40 -  using assms unfolding bi_total_def split_sum_all split_sum_ex by simp
    6.41 -
    6.42 -lemma bi_unique_rel_sum [transfer_rule]:
    6.43 -  "bi_unique R1 \<Longrightarrow> bi_unique R2 \<Longrightarrow> bi_unique (rel_sum R1 R2)"
    6.44 -  using assms unfolding bi_unique_def split_sum_all by simp
    6.45 -
    6.46 -lemma sum_relator_eq_onp [relator_eq_onp]: 
    6.47 -  "rel_sum (eq_onp P1) (eq_onp P2) = eq_onp (sum_pred P1 P2)"
    6.48 -  by (auto simp add: fun_eq_iff eq_onp_def rel_sum_def split: sum.split)
    6.49 -
    6.50 -subsection {* Quotient theorem for the Lifting package *}
    6.51 -
    6.52 -lemma Quotient_sum[quot_map]:
    6.53 -  assumes "Quotient R1 Abs1 Rep1 T1"
    6.54 -  assumes "Quotient R2 Abs2 Rep2 T2"
    6.55 -  shows "Quotient (rel_sum R1 R2) (map_sum Abs1 Abs2) (map_sum Rep1 Rep2) (rel_sum T1 T2)"
    6.56 -  using assms unfolding Quotient_alt_def
    6.57 -  by (simp add: split_sum_all)
    6.58 -
    6.59  subsection {* Transfer rules for the Transfer package *}
    6.60  
    6.61  context
     7.1 --- a/src/HOL/List.thy	Thu Apr 10 17:48:18 2014 +0200
     7.2 +++ b/src/HOL/List.thy	Thu Apr 10 17:48:32 2014 +0200
     7.3 @@ -6578,124 +6578,6 @@
     7.4  
     7.5  subsection {* Setup for Lifting/Transfer *}
     7.6  
     7.7 -subsubsection {* Relator and predicator properties *}
     7.8 -
     7.9 -lemma list_all2_eq'[relator_eq]:
    7.10 -  "list_all2 (op =) = (op =)"
    7.11 -by (rule ext)+ (simp add: list_all2_eq)
    7.12 -
    7.13 -lemma list_all2_mono'[relator_mono]:
    7.14 -  assumes "A \<le> B"
    7.15 -  shows "(list_all2 A) \<le> (list_all2 B)"
    7.16 -using assms by (auto intro: list_all2_mono)
    7.17 -
    7.18 -lemma list_all2_OO[relator_distr]: "list_all2 A OO list_all2 B = list_all2 (A OO B)"
    7.19 -proof (intro ext iffI)
    7.20 -  fix xs ys
    7.21 -  assume "list_all2 (A OO B) xs ys"
    7.22 -  thus "(list_all2 A OO list_all2 B) xs ys"
    7.23 -    unfolding OO_def
    7.24 -    by (induct, simp, simp add: list_all2_Cons1 list_all2_Cons2, fast)
    7.25 -next
    7.26 -  fix xs ys
    7.27 -  assume "(list_all2 A OO list_all2 B) xs ys"
    7.28 -  then obtain zs where "list_all2 A xs zs" and "list_all2 B zs ys" ..
    7.29 -  thus "list_all2 (A OO B) xs ys"
    7.30 -    by (induct arbitrary: ys, simp, clarsimp simp add: list_all2_Cons1, fast)
    7.31 -qed
    7.32 -
    7.33 -lemma Domainp_list[relator_domain]:
    7.34 -  "Domainp (list_all2 A) = (list_all (Domainp A))"
    7.35 -proof -
    7.36 -  {
    7.37 -    fix x
    7.38 -    have *: "\<And>x. (\<exists>y. A x y) = Domainp A x" unfolding Domainp_iff by blast
    7.39 -    have "(\<exists>y. (list_all2 A x y)) = list_all (Domainp A) x"
    7.40 -    by (induction x) (simp_all add: * list_all2_Cons1)
    7.41 -  }
    7.42 -  then show ?thesis
    7.43 -  unfolding Domainp_iff[abs_def]
    7.44 -  by (auto iff: fun_eq_iff)
    7.45 -qed 
    7.46 -
    7.47 -lemma left_total_list_all2[transfer_rule]:
    7.48 -  "left_total R \<Longrightarrow> left_total (list_all2 R)"
    7.49 -  unfolding left_total_def
    7.50 -  apply safe
    7.51 -  apply (rename_tac xs, induct_tac xs, simp, simp add: list_all2_Cons1)
    7.52 -done
    7.53 -
    7.54 -lemma left_unique_list_all2 [transfer_rule]:
    7.55 -  "left_unique R \<Longrightarrow> left_unique (list_all2 R)"
    7.56 -  unfolding left_unique_def
    7.57 -  apply (subst (2) all_comm, subst (1) all_comm)
    7.58 -  apply (rule allI, rename_tac zs, induct_tac zs)
    7.59 -  apply (auto simp add: list_all2_Cons2)
    7.60 -  done
    7.61 -
    7.62 -lemma right_total_list_all2 [transfer_rule]:
    7.63 -  "right_total R \<Longrightarrow> right_total (list_all2 R)"
    7.64 -  unfolding right_total_def
    7.65 -  by (rule allI, induct_tac y, simp, simp add: list_all2_Cons2)
    7.66 -
    7.67 -lemma right_unique_list_all2 [transfer_rule]:
    7.68 -  "right_unique R \<Longrightarrow> right_unique (list_all2 R)"
    7.69 -  unfolding right_unique_def
    7.70 -  apply (rule allI, rename_tac xs, induct_tac xs)
    7.71 -  apply (auto simp add: list_all2_Cons1)
    7.72 -  done
    7.73 -
    7.74 -lemma bi_total_list_all2 [transfer_rule]:
    7.75 -  "bi_total A \<Longrightarrow> bi_total (list_all2 A)"
    7.76 -  unfolding bi_total_def
    7.77 -  apply safe
    7.78 -  apply (rename_tac xs, induct_tac xs, simp, simp add: list_all2_Cons1)
    7.79 -  apply (rename_tac ys, induct_tac ys, simp, simp add: list_all2_Cons2)
    7.80 -  done
    7.81 -
    7.82 -lemma bi_unique_list_all2 [transfer_rule]:
    7.83 -  "bi_unique A \<Longrightarrow> bi_unique (list_all2 A)"
    7.84 -  unfolding bi_unique_def
    7.85 -  apply (rule conjI)
    7.86 -  apply (rule allI, rename_tac xs, induct_tac xs)
    7.87 -  apply (simp, force simp add: list_all2_Cons1)
    7.88 -  apply (subst (2) all_comm, subst (1) all_comm)
    7.89 -  apply (rule allI, rename_tac xs, induct_tac xs)
    7.90 -  apply (simp, force simp add: list_all2_Cons2)
    7.91 -  done
    7.92 -
    7.93 -lemma list_relator_eq_onp [relator_eq_onp]:
    7.94 -  "list_all2 (eq_onp P) = eq_onp (list_all P)"
    7.95 -  apply (simp add: fun_eq_iff list_all2_iff list_all_iff eq_onp_def Ball_def) 
    7.96 -  apply (intro allI) 
    7.97 -  apply (induct_tac rule: list_induct2') 
    7.98 -  apply simp_all 
    7.99 -  apply fastforce
   7.100 -done
   7.101 -
   7.102 -subsubsection {* Quotient theorem for the Lifting package *}
   7.103 -
   7.104 -lemma Quotient_list[quot_map]:
   7.105 -  assumes "Quotient R Abs Rep T"
   7.106 -  shows "Quotient (list_all2 R) (map Abs) (map Rep) (list_all2 T)"
   7.107 -proof (unfold Quotient_alt_def, intro conjI allI impI)
   7.108 -  from assms have 1: "\<And>x y. T x y \<Longrightarrow> Abs x = y"
   7.109 -    unfolding Quotient_alt_def by simp
   7.110 -  fix xs ys assume "list_all2 T xs ys" thus "map Abs xs = ys"
   7.111 -    by (induct, simp, simp add: 1)
   7.112 -next
   7.113 -  from assms have 2: "\<And>x. T (Rep x) x"
   7.114 -    unfolding Quotient_alt_def by simp
   7.115 -  fix xs show "list_all2 T (map Rep xs) xs"
   7.116 -    by (induct xs, simp, simp add: 2)
   7.117 -next
   7.118 -  from assms have 3: "\<And>x y. R x y \<longleftrightarrow> T x (Abs x) \<and> T y (Abs y) \<and> Abs x = Abs y"
   7.119 -    unfolding Quotient_alt_def by simp
   7.120 -  fix xs ys show "list_all2 R xs ys \<longleftrightarrow> list_all2 T xs (map Abs xs) \<and>
   7.121 -    list_all2 T ys (map Abs ys) \<and> map Abs xs = map Abs ys"
   7.122 -    by (induct xs ys rule: list_induct2', simp_all, metis 3)
   7.123 -qed
   7.124 -
   7.125  subsubsection {* Transfer rules for the Transfer package *}
   7.126  
   7.127  context