src/HOL/List.thy
changeset 56525 b5b6ad5dc2ae
parent 56520 3373f5d1e074
child 56527 907f04603177
--- a/src/HOL/List.thy	Thu Apr 10 17:48:18 2014 +0200
+++ b/src/HOL/List.thy	Thu Apr 10 17:48:32 2014 +0200
@@ -6578,124 +6578,6 @@
 
 subsection {* Setup for Lifting/Transfer *}
 
-subsubsection {* Relator and predicator properties *}
-
-lemma list_all2_eq'[relator_eq]:
-  "list_all2 (op =) = (op =)"
-by (rule ext)+ (simp add: list_all2_eq)
-
-lemma list_all2_mono'[relator_mono]:
-  assumes "A \<le> B"
-  shows "(list_all2 A) \<le> (list_all2 B)"
-using assms by (auto intro: list_all2_mono)
-
-lemma list_all2_OO[relator_distr]: "list_all2 A OO list_all2 B = list_all2 (A OO B)"
-proof (intro ext iffI)
-  fix xs ys
-  assume "list_all2 (A OO B) xs ys"
-  thus "(list_all2 A OO list_all2 B) xs ys"
-    unfolding OO_def
-    by (induct, simp, simp add: list_all2_Cons1 list_all2_Cons2, fast)
-next
-  fix xs ys
-  assume "(list_all2 A OO list_all2 B) xs ys"
-  then obtain zs where "list_all2 A xs zs" and "list_all2 B zs ys" ..
-  thus "list_all2 (A OO B) xs ys"
-    by (induct arbitrary: ys, simp, clarsimp simp add: list_all2_Cons1, fast)
-qed
-
-lemma Domainp_list[relator_domain]:
-  "Domainp (list_all2 A) = (list_all (Domainp A))"
-proof -
-  {
-    fix x
-    have *: "\<And>x. (\<exists>y. A x y) = Domainp A x" unfolding Domainp_iff by blast
-    have "(\<exists>y. (list_all2 A x y)) = list_all (Domainp A) x"
-    by (induction x) (simp_all add: * list_all2_Cons1)
-  }
-  then show ?thesis
-  unfolding Domainp_iff[abs_def]
-  by (auto iff: fun_eq_iff)
-qed 
-
-lemma left_total_list_all2[transfer_rule]:
-  "left_total R \<Longrightarrow> left_total (list_all2 R)"
-  unfolding left_total_def
-  apply safe
-  apply (rename_tac xs, induct_tac xs, simp, simp add: list_all2_Cons1)
-done
-
-lemma left_unique_list_all2 [transfer_rule]:
-  "left_unique R \<Longrightarrow> left_unique (list_all2 R)"
-  unfolding left_unique_def
-  apply (subst (2) all_comm, subst (1) all_comm)
-  apply (rule allI, rename_tac zs, induct_tac zs)
-  apply (auto simp add: list_all2_Cons2)
-  done
-
-lemma right_total_list_all2 [transfer_rule]:
-  "right_total R \<Longrightarrow> right_total (list_all2 R)"
-  unfolding right_total_def
-  by (rule allI, induct_tac y, simp, simp add: list_all2_Cons2)
-
-lemma right_unique_list_all2 [transfer_rule]:
-  "right_unique R \<Longrightarrow> right_unique (list_all2 R)"
-  unfolding right_unique_def
-  apply (rule allI, rename_tac xs, induct_tac xs)
-  apply (auto simp add: list_all2_Cons1)
-  done
-
-lemma bi_total_list_all2 [transfer_rule]:
-  "bi_total A \<Longrightarrow> bi_total (list_all2 A)"
-  unfolding bi_total_def
-  apply safe
-  apply (rename_tac xs, induct_tac xs, simp, simp add: list_all2_Cons1)
-  apply (rename_tac ys, induct_tac ys, simp, simp add: list_all2_Cons2)
-  done
-
-lemma bi_unique_list_all2 [transfer_rule]:
-  "bi_unique A \<Longrightarrow> bi_unique (list_all2 A)"
-  unfolding bi_unique_def
-  apply (rule conjI)
-  apply (rule allI, rename_tac xs, induct_tac xs)
-  apply (simp, force simp add: list_all2_Cons1)
-  apply (subst (2) all_comm, subst (1) all_comm)
-  apply (rule allI, rename_tac xs, induct_tac xs)
-  apply (simp, force simp add: list_all2_Cons2)
-  done
-
-lemma list_relator_eq_onp [relator_eq_onp]:
-  "list_all2 (eq_onp P) = eq_onp (list_all P)"
-  apply (simp add: fun_eq_iff list_all2_iff list_all_iff eq_onp_def Ball_def) 
-  apply (intro allI) 
-  apply (induct_tac rule: list_induct2') 
-  apply simp_all 
-  apply fastforce
-done
-
-subsubsection {* Quotient theorem for the Lifting package *}
-
-lemma Quotient_list[quot_map]:
-  assumes "Quotient R Abs Rep T"
-  shows "Quotient (list_all2 R) (map Abs) (map Rep) (list_all2 T)"
-proof (unfold Quotient_alt_def, intro conjI allI impI)
-  from assms have 1: "\<And>x y. T x y \<Longrightarrow> Abs x = y"
-    unfolding Quotient_alt_def by simp
-  fix xs ys assume "list_all2 T xs ys" thus "map Abs xs = ys"
-    by (induct, simp, simp add: 1)
-next
-  from assms have 2: "\<And>x. T (Rep x) x"
-    unfolding Quotient_alt_def by simp
-  fix xs show "list_all2 T (map Rep xs) xs"
-    by (induct xs, simp, simp add: 2)
-next
-  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"
-    unfolding Quotient_alt_def by simp
-  fix xs ys show "list_all2 R xs ys \<longleftrightarrow> list_all2 T xs (map Abs xs) \<and>
-    list_all2 T ys (map Abs ys) \<and> map Abs xs = map Abs ys"
-    by (induct xs ys rule: list_induct2', simp_all, metis 3)
-qed
-
 subsubsection {* Transfer rules for the Transfer package *}
 
 context