# HG changeset patch # User kuncar # Date 1380285806 -7200 # Node ID b2781a3ce95831c6b57e71e199cccca456b56733 # Parent 03b74ef6d7c637ee0f7887f831e1bd7bdee348f7 new parametricity rules and useful lemmas diff -r 03b74ef6d7c6 -r b2781a3ce958 src/HOL/Lifting.thy --- a/src/HOL/Lifting.thy Fri Sep 27 14:43:26 2013 +0200 +++ b/src/HOL/Lifting.thy Fri Sep 27 14:43:26 2013 +0200 @@ -38,12 +38,26 @@ obtains "(\x. \y. R x y)" using assms unfolding left_total_def by blast +lemma bi_total_iff: "bi_total A = (right_total A \ left_total A)" +unfolding left_total_def right_total_def bi_total_def by blast + lemma bi_total_conv_left_right: "bi_total R \ left_total R \ right_total R" by(simp add: left_total_def right_total_def bi_total_def) definition left_unique :: "('a \ 'b \ bool) \ bool" where "left_unique R \ (\x y z. R x z \ R y z \ x = y)" +lemma left_unique_transfer [transfer_rule]: + assumes [transfer_rule]: "right_total A" + assumes [transfer_rule]: "right_total B" + assumes [transfer_rule]: "bi_unique A" + shows "((A ===> B ===> op=) ===> implies) left_unique left_unique" +using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def fun_rel_def +by metis + +lemma bi_unique_iff: "bi_unique A = (right_unique A \ left_unique A)" +unfolding left_unique_def right_unique_def bi_unique_def by blast + lemma bi_unique_conv_left_right: "bi_unique R \ left_unique R \ right_unique R" by(auto simp add: left_unique_def right_unique_def bi_unique_def) @@ -286,6 +300,11 @@ shows "invariant P x x \ P x" using assms by (auto simp add: invariant_def) +lemma invariant_transfer [transfer_rule]: + assumes [transfer_rule]: "bi_unique A" + shows "((A ===> op=) ===> A ===> A ===> op=) Lifting.invariant Lifting.invariant" +unfolding invariant_def[abs_def] by transfer_prover + lemma UNIV_typedef_to_Quotient: assumes "type_definition Rep Abs UNIV" and T_def: "T \ (\x y. x = Rep y)" diff -r 03b74ef6d7c6 -r b2781a3ce958 src/HOL/Lifting_Set.thy --- a/src/HOL/Lifting_Set.thy Fri Sep 27 14:43:26 2013 +0200 +++ b/src/HOL/Lifting_Set.thy Fri Sep 27 14:43:26 2013 +0200 @@ -162,6 +162,10 @@ by(rule SUPR_eq)(auto 4 4 dest: set_relD1[OF AB] set_relD2[OF AB] fun_relD[OF fg] intro: rev_bexI) qed +lemma bind_transfer [transfer_rule]: + "(set_rel A ===> (A ===> set_rel B) ===> set_rel B) Set.bind Set.bind" +unfolding bind_UNION[abs_def] by transfer_prover + subsubsection {* Rules requiring bi-unique, bi-total or right-total relations *} lemma member_transfer [transfer_rule]: diff -r 03b74ef6d7c6 -r b2781a3ce958 src/HOL/Transfer.thy --- a/src/HOL/Transfer.thy Fri Sep 27 14:43:26 2013 +0200 +++ b/src/HOL/Transfer.thy Fri Sep 27 14:43:26 2013 +0200 @@ -292,6 +292,17 @@ subsection {* Transfer rules *} +lemma Domainp_iff: "Domainp T x \ (\y. T x y)" + by auto + +lemma Domainp_forall_transfer [transfer_rule]: + assumes "right_total A" + shows "((A ===> op =) ===> op =) + (transfer_bforall (Domainp A)) transfer_forall" + using assms unfolding right_total_def + unfolding transfer_forall_def transfer_bforall_def fun_rel_def Domainp_iff + by metis + text {* Transfer rules using implication instead of equality on booleans. *} lemma transfer_forall_transfer [transfer_rule]: @@ -324,9 +335,6 @@ shows "(A ===> A ===> op =) (op =) (op =)" using assms unfolding bi_unique_def fun_rel_def by auto -lemma Domainp_iff: "Domainp T x \ (\y. T x y)" - by auto - lemma right_total_Ex_transfer[transfer_rule]: assumes "right_total A" shows "((A ===> op=) ===> op=) (Bex (Collect (Domainp A))) Ex" @@ -379,17 +387,50 @@ "(op = ===> (A ===> A) ===> (A ===> A)) compow compow" unfolding funpow_def by transfer_prover -lemma Domainp_forall_transfer [transfer_rule]: - assumes "right_total A" - shows "((A ===> op =) ===> op =) - (transfer_bforall (Domainp A)) transfer_forall" - using assms unfolding right_total_def - unfolding transfer_forall_def transfer_bforall_def fun_rel_def Domainp_iff - by metis +lemma mono_transfer[transfer_rule]: + assumes [transfer_rule]: "bi_total A" + assumes [transfer_rule]: "(A ===> A ===> op=) op\ op\" + assumes [transfer_rule]: "(B ===> B ===> op=) op\ op\" + shows "((A ===> B) ===> op=) mono mono" +unfolding mono_def[abs_def] by transfer_prover + +lemma right_total_relcompp_transfer[transfer_rule]: + assumes [transfer_rule]: "right_total B" + shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=) + (\R S x z. \y\Collect (Domainp B). R x y \ S y z) op OO" +unfolding OO_def[abs_def] by transfer_prover + +lemma relcompp_transfer[transfer_rule]: + assumes [transfer_rule]: "bi_total B" + shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=) op OO op OO" +unfolding OO_def[abs_def] by transfer_prover -lemma forall_transfer [transfer_rule]: - "bi_total A \ ((A ===> op =) ===> op =) transfer_forall transfer_forall" - unfolding transfer_forall_def by (rule All_transfer) +lemma right_total_Domainp_transfer[transfer_rule]: + assumes [transfer_rule]: "right_total B" + shows "((A ===> B ===> op=) ===> A ===> op=) (\T x. \y\Collect(Domainp B). T x y) Domainp" +apply(subst(2) Domainp_iff[abs_def]) by transfer_prover + +lemma Domainp_transfer[transfer_rule]: + assumes [transfer_rule]: "bi_total B" + shows "((A ===> B ===> op=) ===> A ===> op=) Domainp Domainp" +unfolding Domainp_iff[abs_def] by transfer_prover + +lemma reflp_transfer[transfer_rule]: + "bi_total A \ ((A ===> A ===> op=) ===> op=) reflp reflp" + "right_total A \ ((A ===> A ===> implies) ===> implies) reflp reflp" + "right_total A \ ((A ===> A ===> op=) ===> implies) reflp reflp" + "bi_total A \ ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp" + "bi_total A \ ((A ===> A ===> op=) ===> rev_implies) reflp reflp" +using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def fun_rel_def +by fast+ + +lemma right_unique_transfer [transfer_rule]: + assumes [transfer_rule]: "right_total A" + assumes [transfer_rule]: "right_total B" + assumes [transfer_rule]: "bi_unique B" + shows "((A ===> B ===> op=) ===> implies) right_unique right_unique" +using assms unfolding right_unique_def[abs_def] right_total_def bi_unique_def fun_rel_def +by metis end