--- a/src/HOL/Int.thy Thu Apr 10 17:48:18 2014 +0200
+++ b/src/HOL/Int.thy Thu Apr 10 17:48:32 2014 +0200
@@ -78,8 +78,8 @@
simp add: one_int.abs_eq plus_int.abs_eq)
lemma int_transfer [transfer_rule]:
- "(rel_fun (op =) cr_int) (\<lambda>n. (n, 0)) int"
- unfolding rel_fun_def cr_int_def int_def by simp
+ "(rel_fun (op =) pcr_int) (\<lambda>n. (n, 0)) int"
+ unfolding rel_fun_def int.pcr_cr_eq cr_int_def int_def by simp
lemma int_diff_cases:
obtains (diff) m n where "z = int m - int n"
--- a/src/HOL/Library/FSet.thy Thu Apr 10 17:48:18 2014 +0200
+++ b/src/HOL/Library/FSet.thy Thu Apr 10 17:48:32 2014 +0200
@@ -772,14 +772,6 @@
apply (subst rel_set_def[unfolded fun_eq_iff])
by blast
-lemma rel_fset_conversep: "rel_fset (conversep R) = conversep (rel_fset R)"
- unfolding rel_fset_alt_def by auto
-
-lemmas rel_fset_eq [relator_eq] = rel_set_eq[Transfer.transferred]
-
-lemma rel_fset_mono[relator_mono]: "A \<le> B \<Longrightarrow> rel_fset A \<le> rel_fset B"
-unfolding rel_fset_alt_def by blast
-
lemma finite_rel_set:
assumes fin: "finite X" "finite Z"
assumes R_S: "rel_set (R OO S) X Z"
@@ -806,63 +798,6 @@
ultimately show ?thesis by metis
qed
-lemma rel_fset_OO[relator_distr]: "rel_fset R OO rel_fset S = rel_fset (R OO S)"
-apply (rule ext)+
-by transfer (auto intro: finite_rel_set rel_set_OO[unfolded fun_eq_iff, rule_format, THEN iffD1])
-
-lemma Domainp_fset[relator_domain]: "Domainp (rel_fset T) = (\<lambda>A. fBall A (Domainp T))"
-proof -
- obtain f where f: "\<forall>x\<in>Collect (Domainp T). T x (f x)"
- unfolding Domainp_iff[abs_def]
- apply atomize_elim
- by (subst bchoice_iff[symmetric]) (auto iff: bchoice_iff[symmetric])
- from f show ?thesis
- unfolding fun_eq_iff rel_fset_alt_def Domainp_iff
- apply clarify
- apply (rule iffI)
- apply blast
- by (rename_tac A, rule_tac x="f |`| A" in exI, blast)
-qed
-
-lemma right_total_rel_fset[transfer_rule]: "right_total A \<Longrightarrow> right_total (rel_fset A)"
-unfolding right_total_def
-apply transfer
-apply (subst(asm) choice_iff)
-apply clarsimp
-apply (rename_tac A f y, rule_tac x = "f ` y" in exI)
-by (auto simp add: rel_set_def)
-
-lemma left_total_rel_fset[transfer_rule]: "left_total A \<Longrightarrow> left_total (rel_fset A)"
-unfolding left_total_def
-apply transfer
-apply (subst(asm) choice_iff)
-apply clarsimp
-apply (rename_tac A f y, rule_tac x = "f ` y" in exI)
-by (auto simp add: rel_set_def)
-
-lemmas right_unique_rel_fset[transfer_rule] = right_unique_rel_set[Transfer.transferred]
-lemmas left_unique_rel_fset[transfer_rule] = left_unique_rel_set[Transfer.transferred]
-
-thm right_unique_rel_fset left_unique_rel_fset
-
-lemma bi_unique_rel_fset[transfer_rule]: "bi_unique A \<Longrightarrow> bi_unique (rel_fset A)"
-by (auto intro: right_unique_rel_fset left_unique_rel_fset iff: bi_unique_alt_def)
-
-lemma bi_total_rel_fset[transfer_rule]: "bi_total A \<Longrightarrow> bi_total (rel_fset A)"
-by (auto intro: right_total_rel_fset left_total_rel_fset iff: bi_total_alt_def)
-
-lemmas fset_relator_eq_onp [relator_eq_onp] = set_relator_eq_onp[Transfer.transferred]
-
-
-subsubsection {* Quotient theorem for the Lifting package *}
-
-lemma Quotient_fset_map[quot_map]:
- assumes "Quotient R Abs Rep T"
- shows "Quotient (rel_fset R) (fimage Abs) (fimage Rep) (rel_fset T)"
- using assms unfolding Quotient_alt_def4
- by (simp add: rel_fset_OO[symmetric] rel_fset_conversep) (simp add: rel_fset_alt_def, blast)
-
-
subsubsection {* Transfer rules for the Transfer package *}
text {* Unconditional transfer rules *}
--- a/src/HOL/Library/Quotient_Option.thy Thu Apr 10 17:48:18 2014 +0200
+++ b/src/HOL/Library/Quotient_Option.thy Thu Apr 10 17:48:32 2014 +0200
@@ -20,7 +20,7 @@
declare
map_option.id [id_simps]
- rel_option_eq [id_simps]
+ option.rel_eq [id_simps]
lemma reflp_rel_option:
"reflp R \<Longrightarrow> reflp (rel_option R)"
@@ -44,7 +44,7 @@
assumes "Quotient3 R Abs Rep"
shows "Quotient3 (rel_option R) (map_option Abs) (map_option Rep)"
apply (rule Quotient3I)
- 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])
+ 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])
using Quotient3_rel [OF assms]
apply (simp add: rel_option_iff split: option.split)
done
--- a/src/HOL/Lifting_Option.thy Thu Apr 10 17:48:18 2014 +0200
+++ b/src/HOL/Lifting_Option.thy Thu Apr 10 17:48:32 2014 +0200
@@ -6,7 +6,7 @@
header {* Setup for Lifting/Transfer for the option type *}
theory Lifting_Option
-imports Lifting Partial_Function
+imports Lifting Option
begin
subsection {* Relator and predicator properties *}
@@ -17,64 +17,6 @@
| _ \<Rightarrow> False)"
by (auto split: prod.split option.split)
-abbreviation (input) pred_option :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" where
- "pred_option \<equiv> case_option True"
-
-lemma rel_option_eq [relator_eq]:
- "rel_option (op =) = (op =)"
- by (simp add: rel_option_iff fun_eq_iff split: option.split)
-
-lemma rel_option_mono[relator_mono]:
- assumes "A \<le> B"
- shows "(rel_option A) \<le> (rel_option B)"
-using assms by (auto simp: rel_option_iff split: option.splits)
-
-lemma rel_option_OO[relator_distr]:
- "(rel_option A) OO (rel_option B) = rel_option (A OO B)"
-by (rule ext)+ (auto simp: rel_option_iff OO_def split: option.split)
-
-lemma Domainp_option[relator_domain]:
- "Domainp (rel_option A) = (pred_option (Domainp A))"
-unfolding Domainp_iff[abs_def] rel_option_iff[abs_def]
-by (auto iff: fun_eq_iff split: option.split)
-
-lemma left_total_rel_option[transfer_rule]:
- "left_total R \<Longrightarrow> left_total (rel_option R)"
- unfolding left_total_def split_option_all split_option_ex by simp
-
-lemma left_unique_rel_option [transfer_rule]:
- "left_unique R \<Longrightarrow> left_unique (rel_option R)"
- unfolding left_unique_def split_option_all by simp
-
-lemma right_total_rel_option [transfer_rule]:
- "right_total R \<Longrightarrow> right_total (rel_option R)"
- unfolding right_total_def split_option_all split_option_ex by simp
-
-lemma right_unique_rel_option [transfer_rule]:
- "right_unique R \<Longrightarrow> right_unique (rel_option R)"
- unfolding right_unique_def split_option_all by simp
-
-lemma bi_total_rel_option [transfer_rule]:
- "bi_total R \<Longrightarrow> bi_total (rel_option R)"
- unfolding bi_total_def split_option_all split_option_ex by simp
-
-lemma bi_unique_rel_option [transfer_rule]:
- "bi_unique R \<Longrightarrow> bi_unique (rel_option R)"
- unfolding bi_unique_def split_option_all by simp
-
-lemma option_relator_eq_onp [relator_eq_onp]:
- "rel_option (eq_onp P) = eq_onp (pred_option P)"
- by (auto simp add: fun_eq_iff eq_onp_def split_option_all)
-
-subsection {* Quotient theorem for the Lifting package *}
-
-lemma Quotient_option[quot_map]:
- assumes "Quotient R Abs Rep T"
- shows "Quotient (rel_option R) (map_option Abs)
- (map_option Rep) (rel_option T)"
- using assms unfolding Quotient_alt_def rel_option_iff
- by (simp split: option.split)
-
subsection {* Transfer rules for the Transfer package *}
context
--- a/src/HOL/Lifting_Product.thy Thu Apr 10 17:48:18 2014 +0200
+++ b/src/HOL/Lifting_Product.thy Thu Apr 10 17:48:32 2014 +0200
@@ -8,69 +8,6 @@
imports Lifting Basic_BNFs
begin
-subsection {* Relator and predicator properties *}
-
-definition pred_prod :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
-where "pred_prod R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
-
-lemma pred_prod_apply [simp]:
- "pred_prod P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
- by (simp add: pred_prod_def)
-
-lemmas rel_prod_eq[relator_eq] = prod.rel_eq
-lemmas rel_prod_mono[relator_mono] = prod.rel_mono
-
-lemma rel_prod_OO[relator_distr]:
- "(rel_prod A B) OO (rel_prod C D) = rel_prod (A OO C) (B OO D)"
-by (rule ext)+ (auto simp: rel_prod_def OO_def)
-
-lemma Domainp_prod[relator_domain]:
- "Domainp (rel_prod T1 T2) = (pred_prod (Domainp T1) (Domainp T2))"
-unfolding rel_prod_def pred_prod_def by blast
-
-lemma left_total_rel_prod [transfer_rule]:
- assumes "left_total R1"
- assumes "left_total R2"
- shows "left_total (rel_prod R1 R2)"
- using assms unfolding left_total_def rel_prod_def by auto
-
-lemma left_unique_rel_prod [transfer_rule]:
- assumes "left_unique R1" and "left_unique R2"
- shows "left_unique (rel_prod R1 R2)"
- using assms unfolding left_unique_def rel_prod_def by auto
-
-lemma right_total_rel_prod [transfer_rule]:
- assumes "right_total R1" and "right_total R2"
- shows "right_total (rel_prod R1 R2)"
- using assms unfolding right_total_def rel_prod_def by auto
-
-lemma right_unique_rel_prod [transfer_rule]:
- assumes "right_unique R1" and "right_unique R2"
- shows "right_unique (rel_prod R1 R2)"
- using assms unfolding right_unique_def rel_prod_def by auto
-
-lemma bi_total_rel_prod [transfer_rule]:
- assumes "bi_total R1" and "bi_total R2"
- shows "bi_total (rel_prod R1 R2)"
- using assms unfolding bi_total_def rel_prod_def by auto
-
-lemma bi_unique_rel_prod [transfer_rule]:
- assumes "bi_unique R1" and "bi_unique R2"
- shows "bi_unique (rel_prod R1 R2)"
- using assms unfolding bi_unique_def rel_prod_def by auto
-
-lemma prod_relator_eq_onp [relator_eq_onp]:
- "rel_prod (eq_onp P1) (eq_onp P2) = eq_onp (pred_prod P1 P2)"
- by (simp add: fun_eq_iff rel_prod_def pred_prod_def eq_onp_def) blast
-
-subsection {* Quotient theorem for the Lifting package *}
-
-lemma Quotient_prod[quot_map]:
- assumes "Quotient R1 Abs1 Rep1 T1"
- assumes "Quotient R2 Abs2 Rep2 T2"
- shows "Quotient (rel_prod R1 R2) (map_prod Abs1 Abs2) (map_prod Rep1 Rep2) (rel_prod T1 T2)"
- using assms unfolding Quotient_alt_def by auto
-
subsection {* Transfer rules for the Transfer package *}
context
--- a/src/HOL/Lifting_Sum.thy Thu Apr 10 17:48:18 2014 +0200
+++ b/src/HOL/Lifting_Sum.thy Thu Apr 10 17:48:32 2014 +0200
@@ -8,58 +8,6 @@
imports Lifting Basic_BNFs
begin
-subsection {* Relator and predicator properties *}
-
-abbreviation (input) "sum_pred \<equiv> case_sum"
-
-lemmas rel_sum_eq[relator_eq] = sum.rel_eq
-lemmas rel_sum_mono[relator_mono] = sum.rel_mono
-
-lemma rel_sum_OO[relator_distr]:
- "(rel_sum A B) OO (rel_sum C D) = rel_sum (A OO C) (B OO D)"
- by (rule ext)+ (auto simp add: rel_sum_def OO_def split_sum_ex split: sum.split)
-
-lemma Domainp_sum[relator_domain]:
- "Domainp (rel_sum R1 R2) = (sum_pred (Domainp R1) (Domainp R2))"
-by (auto simp add: Domainp_iff split_sum_ex iff: fun_eq_iff split: sum.split)
-
-lemma left_total_rel_sum[transfer_rule]:
- "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (rel_sum R1 R2)"
- using assms unfolding left_total_def split_sum_all split_sum_ex by simp
-
-lemma left_unique_rel_sum [transfer_rule]:
- "left_unique R1 \<Longrightarrow> left_unique R2 \<Longrightarrow> left_unique (rel_sum R1 R2)"
- using assms unfolding left_unique_def split_sum_all by simp
-
-lemma right_total_rel_sum [transfer_rule]:
- "right_total R1 \<Longrightarrow> right_total R2 \<Longrightarrow> right_total (rel_sum R1 R2)"
- unfolding right_total_def split_sum_all split_sum_ex by simp
-
-lemma right_unique_rel_sum [transfer_rule]:
- "right_unique R1 \<Longrightarrow> right_unique R2 \<Longrightarrow> right_unique (rel_sum R1 R2)"
- unfolding right_unique_def split_sum_all by simp
-
-lemma bi_total_rel_sum [transfer_rule]:
- "bi_total R1 \<Longrightarrow> bi_total R2 \<Longrightarrow> bi_total (rel_sum R1 R2)"
- using assms unfolding bi_total_def split_sum_all split_sum_ex by simp
-
-lemma bi_unique_rel_sum [transfer_rule]:
- "bi_unique R1 \<Longrightarrow> bi_unique R2 \<Longrightarrow> bi_unique (rel_sum R1 R2)"
- using assms unfolding bi_unique_def split_sum_all by simp
-
-lemma sum_relator_eq_onp [relator_eq_onp]:
- "rel_sum (eq_onp P1) (eq_onp P2) = eq_onp (sum_pred P1 P2)"
- by (auto simp add: fun_eq_iff eq_onp_def rel_sum_def split: sum.split)
-
-subsection {* Quotient theorem for the Lifting package *}
-
-lemma Quotient_sum[quot_map]:
- assumes "Quotient R1 Abs1 Rep1 T1"
- assumes "Quotient R2 Abs2 Rep2 T2"
- shows "Quotient (rel_sum R1 R2) (map_sum Abs1 Abs2) (map_sum Rep1 Rep2) (rel_sum T1 T2)"
- using assms unfolding Quotient_alt_def
- by (simp add: split_sum_all)
-
subsection {* Transfer rules for the Transfer package *}
context
--- 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