# HG changeset patch # User kuncar # Date 1397144912 -7200 # Node ID b5b6ad5dc2aea0cfbdc9b511a42dc8df789d6f87 # Parent f4ba736040faae691835a321f0e049a11e4255a2 simplify and fix theories thanks to 356a5efdb278 diff -r f4ba736040fa -r b5b6ad5dc2ae src/HOL/Int.thy --- 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) (\n. (n, 0)) int" - unfolding rel_fun_def cr_int_def int_def by simp + "(rel_fun (op =) pcr_int) (\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" diff -r f4ba736040fa -r b5b6ad5dc2ae src/HOL/Library/FSet.thy --- 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 \ B \ rel_fset A \ 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) = (\A. fBall A (Domainp T))" -proof - - obtain f where f: "\x\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 \ 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 \ 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 \ 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 \ 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 *} diff -r f4ba736040fa -r b5b6ad5dc2ae src/HOL/Library/Quotient_Option.thy --- 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 \ 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 diff -r f4ba736040fa -r b5b6ad5dc2ae src/HOL/Lifting_Option.thy --- 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 @@ | _ \ False)" by (auto split: prod.split option.split) -abbreviation (input) pred_option :: "('a \ bool) \ 'a option \ bool" where - "pred_option \ 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 \ B" - shows "(rel_option A) \ (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 \ 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 \ left_unique (rel_option R)" - unfolding left_unique_def split_option_all by simp - -lemma right_total_rel_option [transfer_rule]: - "right_total R \ 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 \ right_unique (rel_option R)" - unfolding right_unique_def split_option_all by simp - -lemma bi_total_rel_option [transfer_rule]: - "bi_total R \ 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 \ 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 diff -r f4ba736040fa -r b5b6ad5dc2ae src/HOL/Lifting_Product.thy --- 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 \ bool) \ ('b \ bool) \ 'a \ 'b \ bool" -where "pred_prod R1 R2 = (\(a, b). R1 a \ R2 b)" - -lemma pred_prod_apply [simp]: - "pred_prod P1 P2 (a, b) \ P1 a \ 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 diff -r f4ba736040fa -r b5b6ad5dc2ae src/HOL/Lifting_Sum.thy --- 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 \ 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 \ left_total R2 \ 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 \ left_unique R2 \ 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 \ right_total R2 \ 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 \ right_unique R2 \ 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 \ bi_total R2 \ 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 \ bi_unique R2 \ 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 diff -r f4ba736040fa -r b5b6ad5dc2ae src/HOL/List.thy --- 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 \ B" - shows "(list_all2 A) \ (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 *: "\x. (\y. A x y) = Domainp A x" unfolding Domainp_iff by blast - have "(\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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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: "\x y. T x y \ 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: "\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: "\x y. R x y \ T x (Abs x) \ T y (Abs y) \ Abs x = Abs y" - unfolding Quotient_alt_def by simp - fix xs ys show "list_all2 R xs ys \ list_all2 T xs (map Abs xs) \ - list_all2 T ys (map Abs ys) \ 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