# HG changeset patch # User blanchet # Date 1394115921 -3600 # Node ID 5c2df04e97d11015b516fab0be25ee94ec348863 # Parent c2d96043de4b0d594094f8b6d703f35a5c792cfa renamed 'sum_rel' to 'rel_sum' diff -r c2d96043de4b -r 5c2df04e97d1 NEWS --- a/NEWS Thu Mar 06 15:14:09 2014 +0100 +++ b/NEWS Thu Mar 06 15:25:21 2014 +0100 @@ -193,6 +193,7 @@ * The following map functions and relators have been renamed: sum_map ~> map_sum map_pair ~> map_prod + sum_rel ~> rel_sum set_rel ~> rel_set filter_rel ~> rel_filter fset_rel ~> rel_fset (in "Library/FSet.thy") diff -r c2d96043de4b -r 5c2df04e97d1 src/HOL/BNF_Examples/Derivation_Trees/DTree.thy --- a/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy Thu Mar 06 15:14:09 2014 +0100 +++ b/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy Thu Mar 06 15:25:21 2014 +0100 @@ -67,7 +67,7 @@ lemma dtree_coinduct[elim, consumes 1, case_names Lift, induct pred: "HOL.eq"]: assumes phi: "\ tr1 tr2" and Lift: "\ tr1 tr2. \ tr1 tr2 \ - root tr1 = root tr2 \ rel_set (sum_rel op = \) (cont tr1) (cont tr2)" + root tr1 = root tr2 \ rel_set (rel_sum op = \) (cont tr1) (cont tr2)" shows "tr1 = tr2" using phi apply(elim dtree.coinduct) apply(rule Lift[unfolded rel_set_cont]) . diff -r c2d96043de4b -r 5c2df04e97d1 src/HOL/BNF_Examples/Derivation_Trees/Parallel.thy --- a/src/HOL/BNF_Examples/Derivation_Trees/Parallel.thy Thu Mar 06 15:14:09 2014 +0100 +++ b/src/HOL/BNF_Examples/Derivation_Trees/Parallel.thy Thu Mar 06 15:25:21 2014 +0100 @@ -67,10 +67,10 @@ subsection{* Structural Coinduction Proofs *} -lemma rel_set_sum_rel_eq[simp]: -"rel_set (sum_rel (op =) \) A1 A2 \ +lemma rel_set_rel_sum_eq[simp]: +"rel_set (rel_sum (op =) \) A1 A2 \ Inl -` A1 = Inl -` A2 \ rel_set \ (Inr -` A1) (Inr -` A2)" -unfolding rel_set_sum_rel rel_set_eq .. +unfolding rel_set_rel_sum rel_set_eq .. (* Detailed proofs of commutativity and associativity: *) theorem par_com: "tr1 \ tr2 = tr2 \ tr1" @@ -79,7 +79,7 @@ {fix trA trB assume "?\ trA trB" hence "trA = trB" apply (induct rule: dtree_coinduct) - unfolding rel_set_sum_rel rel_set_eq unfolding rel_set_def proof safe + unfolding rel_set_rel_sum rel_set_eq unfolding rel_set_def proof safe fix tr1 tr2 show "root (tr1 \ tr2) = root (tr2 \ tr1)" unfolding root_par by (rule Nplus_comm) next @@ -114,7 +114,7 @@ {fix trA trB assume "?\ trA trB" hence "trA = trB" apply (induct rule: dtree_coinduct) - unfolding rel_set_sum_rel rel_set_eq unfolding rel_set_def proof safe + unfolding rel_set_rel_sum rel_set_eq unfolding rel_set_def proof safe fix tr1 tr2 tr3 show "root ((tr1 \ tr2) \ tr3) = root (tr1 \ (tr2 \ tr3))" unfolding root_par by (rule Nplus_assoc) next diff -r c2d96043de4b -r 5c2df04e97d1 src/HOL/BNF_Examples/Process.thy --- a/src/HOL/BNF_Examples/Process.thy Thu Mar 06 15:14:09 2014 +0100 +++ b/src/HOL/BNF_Examples/Process.thy Thu Mar 06 15:25:21 2014 +0100 @@ -23,7 +23,7 @@ declare rel_pre_process_def[simp] - sum_rel_def[simp] + rel_sum_def[simp] prod_rel_def[simp] (* Constructors versus discriminators *) diff -r c2d96043de4b -r 5c2df04e97d1 src/HOL/Basic_BNFs.thy --- a/src/HOL/Basic_BNFs.thy Thu Mar 06 15:14:09 2014 +0100 +++ b/src/HOL/Basic_BNFs.thy Thu Mar 06 15:25:21 2014 +0100 @@ -22,26 +22,26 @@ lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def] definition - sum_rel :: "('a \ 'c \ bool) \ ('b \ 'd \ bool) \ 'a + 'b \ 'c + 'd \ bool" + rel_sum :: "('a \ 'c \ bool) \ ('b \ 'd \ bool) \ 'a + 'b \ 'c + 'd \ bool" where - "sum_rel R1 R2 x y = + "rel_sum R1 R2 x y = (case (x, y) of (Inl x, Inl y) \ R1 x y | (Inr x, Inr y) \ R2 x y | _ \ False)" -lemma sum_rel_simps[simp]: - "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" - "sum_rel R1 R2 (Inl a1) (Inr b2) = False" - "sum_rel R1 R2 (Inr a2) (Inl b1) = False" - "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" - unfolding sum_rel_def by simp_all +lemma rel_sum_simps[simp]: + "rel_sum R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" + "rel_sum R1 R2 (Inl a1) (Inr b2) = False" + "rel_sum R1 R2 (Inr a2) (Inl b1) = False" + "rel_sum R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" + unfolding rel_sum_def by simp_all bnf "'a + 'b" map: map_sum sets: setl setr bd: natLeq wits: Inl Inr - rel: sum_rel + rel: rel_sum proof - show "map_sum id id = id" by (rule map_sum.id) next @@ -84,14 +84,14 @@ by (simp add: setr_def split: sum.split) next fix R1 R2 S1 S2 - show "sum_rel R1 R2 OO sum_rel S1 S2 \ sum_rel (R1 OO S1) (R2 OO S2)" - by (auto simp: sum_rel_def split: sum.splits) + show "rel_sum R1 R2 OO rel_sum S1 S2 \ rel_sum (R1 OO S1) (R2 OO S2)" + by (auto simp: rel_sum_def split: sum.splits) next fix R S - show "sum_rel R S = + show "rel_sum R S = (Grp {x. setl x \ Collect (split R) \ setr x \ Collect (split S)} (map_sum fst fst))\\ OO Grp {x. setl x \ Collect (split R) \ setr x \ Collect (split S)} (map_sum snd snd)" - unfolding setl_def setr_def sum_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff + unfolding setl_def setr_def rel_sum_def Grp_def relcompp.simps conversep.simps fun_eq_iff by (fastforce split: sum.splits) qed (auto simp: sum_set_defs) diff -r c2d96043de4b -r 5c2df04e97d1 src/HOL/Library/FSet.thy --- a/src/HOL/Library/FSet.thy Thu Mar 06 15:14:09 2014 +0100 +++ b/src/HOL/Library/FSet.thy Thu Mar 06 15:25:21 2014 +0100 @@ -1049,34 +1049,34 @@ (* Set vs. sum relators: *) -lemma rel_set_sum_rel[simp]: -"rel_set (sum_rel \ \) A1 A2 \ +lemma rel_set_rel_sum[simp]: +"rel_set (rel_sum \ \) A1 A2 \ rel_set \ (Inl -` A1) (Inl -` A2) \ rel_set \ (Inr -` A1) (Inr -` A2)" (is "?L \ ?Rl \ ?Rr") proof safe assume L: "?L" show ?Rl unfolding rel_set_def Bex_def vimage_eq proof safe fix l1 assume "Inl l1 \ A1" - then obtain a2 where a2: "a2 \ A2" and "sum_rel \ \ (Inl l1) a2" + then obtain a2 where a2: "a2 \ A2" and "rel_sum \ \ (Inl l1) a2" using L unfolding rel_set_def by auto then obtain l2 where "a2 = Inl l2 \ \ l1 l2" by (cases a2, auto) thus "\ l2. Inl l2 \ A2 \ \ l1 l2" using a2 by auto next fix l2 assume "Inl l2 \ A2" - then obtain a1 where a1: "a1 \ A1" and "sum_rel \ \ a1 (Inl l2)" + then obtain a1 where a1: "a1 \ A1" and "rel_sum \ \ a1 (Inl l2)" using L unfolding rel_set_def by auto then obtain l1 where "a1 = Inl l1 \ \ l1 l2" by (cases a1, auto) thus "\ l1. Inl l1 \ A1 \ \ l1 l2" using a1 by auto qed show ?Rr unfolding rel_set_def Bex_def vimage_eq proof safe fix r1 assume "Inr r1 \ A1" - then obtain a2 where a2: "a2 \ A2" and "sum_rel \ \ (Inr r1) a2" + then obtain a2 where a2: "a2 \ A2" and "rel_sum \ \ (Inr r1) a2" using L unfolding rel_set_def by auto then obtain r2 where "a2 = Inr r2 \ \ r1 r2" by (cases a2, auto) thus "\ r2. Inr r2 \ A2 \ \ r1 r2" using a2 by auto next fix r2 assume "Inr r2 \ A2" - then obtain a1 where a1: "a1 \ A1" and "sum_rel \ \ a1 (Inr r2)" + then obtain a1 where a1: "a1 \ A1" and "rel_sum \ \ a1 (Inr r2)" using L unfolding rel_set_def by auto then obtain r1 where "a1 = Inr r1 \ \ r1 r2" by (cases a1, auto) thus "\ r1. Inr r1 \ A1 \ \ r1 r2" using a1 by auto @@ -1085,7 +1085,7 @@ assume Rl: "?Rl" and Rr: "?Rr" show ?L unfolding rel_set_def Bex_def vimage_eq proof safe fix a1 assume a1: "a1 \ A1" - show "\ a2. a2 \ A2 \ sum_rel \ \ a1 a2" + show "\ a2. a2 \ A2 \ rel_sum \ \ a1 a2" proof(cases a1) case (Inl l1) then obtain l2 where "Inl l2 \ A2 \ \ l1 l2" using Rl a1 unfolding rel_set_def by blast @@ -1097,7 +1097,7 @@ qed next fix a2 assume a2: "a2 \ A2" - show "\ a1. a1 \ A1 \ sum_rel \ \ a1 a2" + show "\ a1. a1 \ A1 \ rel_sum \ \ a1 a2" proof(cases a2) case (Inl l2) then obtain l1 where "Inl l1 \ A1 \ \ l1 l2" using Rl a2 unfolding rel_set_def by blast diff -r c2d96043de4b -r 5c2df04e97d1 src/HOL/Library/Quotient_Sum.thy --- a/src/HOL/Library/Quotient_Sum.thy Thu Mar 06 15:14:09 2014 +0100 +++ b/src/HOL/Library/Quotient_Sum.thy Thu Mar 06 15:25:21 2014 +0100 @@ -10,61 +10,61 @@ subsection {* Rules for the Quotient package *} -lemma sum_rel_map1: - "sum_rel R1 R2 (map_sum f1 f2 x) y \ sum_rel (\x. R1 (f1 x)) (\x. R2 (f2 x)) x y" - by (simp add: sum_rel_def split: sum.split) +lemma rel_sum_map1: + "rel_sum R1 R2 (map_sum f1 f2 x) y \ rel_sum (\x. R1 (f1 x)) (\x. R2 (f2 x)) x y" + by (simp add: rel_sum_def split: sum.split) -lemma sum_rel_map2: - "sum_rel R1 R2 x (map_sum f1 f2 y) \ sum_rel (\x y. R1 x (f1 y)) (\x y. R2 x (f2 y)) x y" - by (simp add: sum_rel_def split: sum.split) +lemma rel_sum_map2: + "rel_sum R1 R2 x (map_sum f1 f2 y) \ rel_sum (\x y. R1 x (f1 y)) (\x y. R2 x (f2 y)) x y" + by (simp add: rel_sum_def split: sum.split) lemma map_sum_id [id_simps]: "map_sum id id = id" by (simp add: id_def map_sum.identity fun_eq_iff) -lemma sum_rel_eq [id_simps]: - "sum_rel (op =) (op =) = (op =)" - by (simp add: sum_rel_def fun_eq_iff split: sum.split) +lemma rel_sum_eq [id_simps]: + "rel_sum (op =) (op =) = (op =)" + by (simp add: rel_sum_def fun_eq_iff split: sum.split) -lemma reflp_sum_rel: - "reflp R1 \ reflp R2 \ reflp (sum_rel R1 R2)" - unfolding reflp_def split_sum_all sum_rel_simps by fast +lemma reflp_rel_sum: + "reflp R1 \ reflp R2 \ reflp (rel_sum R1 R2)" + unfolding reflp_def split_sum_all rel_sum_simps by fast lemma sum_symp: - "symp R1 \ symp R2 \ symp (sum_rel R1 R2)" - unfolding symp_def split_sum_all sum_rel_simps by fast + "symp R1 \ symp R2 \ symp (rel_sum R1 R2)" + unfolding symp_def split_sum_all rel_sum_simps by fast lemma sum_transp: - "transp R1 \ transp R2 \ transp (sum_rel R1 R2)" - unfolding transp_def split_sum_all sum_rel_simps by fast + "transp R1 \ transp R2 \ transp (rel_sum R1 R2)" + unfolding transp_def split_sum_all rel_sum_simps by fast lemma sum_equivp [quot_equiv]: - "equivp R1 \ equivp R2 \ equivp (sum_rel R1 R2)" - by (blast intro: equivpI reflp_sum_rel sum_symp sum_transp elim: equivpE) + "equivp R1 \ equivp R2 \ equivp (rel_sum R1 R2)" + by (blast intro: equivpI reflp_rel_sum sum_symp sum_transp elim: equivpE) lemma sum_quotient [quot_thm]: assumes q1: "Quotient3 R1 Abs1 Rep1" assumes q2: "Quotient3 R2 Abs2 Rep2" - shows "Quotient3 (sum_rel R1 R2) (map_sum Abs1 Abs2) (map_sum Rep1 Rep2)" + shows "Quotient3 (rel_sum R1 R2) (map_sum Abs1 Abs2) (map_sum Rep1 Rep2)" apply (rule Quotient3I) - apply (simp_all add: map_sum.compositionality comp_def map_sum.identity sum_rel_eq sum_rel_map1 sum_rel_map2 + apply (simp_all add: map_sum.compositionality comp_def map_sum.identity rel_sum_eq rel_sum_map1 rel_sum_map2 Quotient3_abs_rep [OF q1] Quotient3_rel_rep [OF q1] Quotient3_abs_rep [OF q2] Quotient3_rel_rep [OF q2]) using Quotient3_rel [OF q1] Quotient3_rel [OF q2] - apply (simp add: sum_rel_def comp_def split: sum.split) + apply (simp add: rel_sum_def comp_def split: sum.split) done -declare [[mapQ3 sum = (sum_rel, sum_quotient)]] +declare [[mapQ3 sum = (rel_sum, sum_quotient)]] lemma sum_Inl_rsp [quot_respect]: assumes q1: "Quotient3 R1 Abs1 Rep1" assumes q2: "Quotient3 R2 Abs2 Rep2" - shows "(R1 ===> sum_rel R1 R2) Inl Inl" + shows "(R1 ===> rel_sum R1 R2) Inl Inl" by auto lemma sum_Inr_rsp [quot_respect]: assumes q1: "Quotient3 R1 Abs1 Rep1" assumes q2: "Quotient3 R2 Abs2 Rep2" - shows "(R2 ===> sum_rel R1 R2) Inr Inr" + shows "(R2 ===> rel_sum R1 R2) Inr Inr" by auto lemma sum_Inl_prs [quot_preserve]: diff -r c2d96043de4b -r 5c2df04e97d1 src/HOL/Lifting_Sum.thy --- a/src/HOL/Lifting_Sum.thy Thu Mar 06 15:14:09 2014 +0100 +++ b/src/HOL/Lifting_Sum.thy Thu Mar 06 15:25:21 2014 +0100 @@ -12,54 +12,54 @@ abbreviation (input) "sum_pred \ case_sum" -lemmas sum_rel_eq[relator_eq] = sum.rel_eq -lemmas sum_rel_mono[relator_mono] = sum.rel_mono +lemmas rel_sum_eq[relator_eq] = sum.rel_eq +lemmas rel_sum_mono[relator_mono] = sum.rel_mono -lemma sum_rel_OO[relator_distr]: - "(sum_rel A B) OO (sum_rel C D) = sum_rel (A OO C) (B OO D)" - by (rule ext)+ (auto simp add: sum_rel_def OO_def split_sum_ex split: sum.split) +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]: assumes "Domainp R1 = P1" assumes "Domainp R2 = P2" - shows "Domainp (sum_rel R1 R2) = (sum_pred P1 P2)" + shows "Domainp (rel_sum R1 R2) = (sum_pred P1 P2)" using assms by (auto simp add: Domainp_iff split_sum_ex iff: fun_eq_iff split: sum.split) -lemma left_total_sum_rel[reflexivity_rule]: - "left_total R1 \ left_total R2 \ left_total (sum_rel R1 R2)" +lemma left_total_rel_sum[reflexivity_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_sum_rel [reflexivity_rule]: - "left_unique R1 \ left_unique R2 \ left_unique (sum_rel R1 R2)" +lemma left_unique_rel_sum [reflexivity_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_sum_rel [transfer_rule]: - "right_total R1 \ right_total R2 \ right_total (sum_rel R1 R2)" +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_sum_rel [transfer_rule]: - "right_unique R1 \ right_unique R2 \ right_unique (sum_rel R1 R2)" +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_sum_rel [transfer_rule]: - "bi_total R1 \ bi_total R2 \ bi_total (sum_rel R1 R2)" +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_sum_rel [transfer_rule]: - "bi_unique R1 \ bi_unique R2 \ bi_unique (sum_rel R1 R2)" +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_invariant_commute [invariant_commute]: - "sum_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)" - by (auto simp add: fun_eq_iff Lifting.invariant_def sum_rel_def split: sum.split) + "rel_sum (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)" + by (auto simp add: fun_eq_iff Lifting.invariant_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 (sum_rel R1 R2) (map_sum Abs1 Abs2) (map_sum Rep1 Rep2) (sum_rel T1 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) @@ -69,15 +69,15 @@ begin interpretation lifting_syntax . -lemma Inl_transfer [transfer_rule]: "(A ===> sum_rel A B) Inl Inl" +lemma Inl_transfer [transfer_rule]: "(A ===> rel_sum A B) Inl Inl" unfolding fun_rel_def by simp -lemma Inr_transfer [transfer_rule]: "(B ===> sum_rel A B) Inr Inr" +lemma Inr_transfer [transfer_rule]: "(B ===> rel_sum A B) Inr Inr" unfolding fun_rel_def by simp lemma case_sum_transfer [transfer_rule]: - "((A ===> C) ===> (B ===> C) ===> sum_rel A B ===> C) case_sum case_sum" - unfolding fun_rel_def sum_rel_def by (simp split: sum.split) + "((A ===> C) ===> (B ===> C) ===> rel_sum A B ===> C) case_sum case_sum" + unfolding fun_rel_def rel_sum_def by (simp split: sum.split) end diff -r c2d96043de4b -r 5c2df04e97d1 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Mar 06 15:14:09 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Mar 06 15:25:21 2014 +0100 @@ -42,7 +42,7 @@ @{thms UN_empty UN_insert Un_empty_left Un_empty_right Un_iff UN_simps(10) UN_iff Union_Un_distrib image_iff o_apply map_prod_simp mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps}; -val sum_prod_thms_rel = @{thms prod_rel_apply sum_rel_simps id_apply}; +val sum_prod_thms_rel = @{thms prod_rel_apply rel_sum_simps id_apply}; fun hhf_concl_conv cv ctxt ct = (case Thm.term_of ct of