--- 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")
--- 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: "\<phi> tr1 tr2" and
Lift: "\<And> tr1 tr2. \<phi> tr1 tr2 \<Longrightarrow>
- root tr1 = root tr2 \<and> rel_set (sum_rel op = \<phi>) (cont tr1) (cont tr2)"
+ root tr1 = root tr2 \<and> rel_set (rel_sum op = \<phi>) (cont tr1) (cont tr2)"
shows "tr1 = tr2"
using phi apply(elim dtree.coinduct)
apply(rule Lift[unfolded rel_set_cont]) .
--- 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 =) \<phi>) A1 A2 \<longleftrightarrow>
+lemma rel_set_rel_sum_eq[simp]:
+"rel_set (rel_sum (op =) \<phi>) A1 A2 \<longleftrightarrow>
Inl -` A1 = Inl -` A2 \<and> rel_set \<phi> (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 \<parallel> tr2 = tr2 \<parallel> tr1"
@@ -79,7 +79,7 @@
{fix trA trB
assume "?\<theta> 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 \<parallel> tr2) = root (tr2 \<parallel> tr1)"
unfolding root_par by (rule Nplus_comm)
next
@@ -114,7 +114,7 @@
{fix trA trB
assume "?\<theta> 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 \<parallel> tr2) \<parallel> tr3) = root (tr1 \<parallel> (tr2 \<parallel> tr3))"
unfolding root_par by (rule Nplus_assoc)
next
--- 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 *)
--- 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 \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
+ rel_sum :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
where
- "sum_rel R1 R2 x y =
+ "rel_sum R1 R2 x y =
(case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
| (Inr x, Inr y) \<Rightarrow> R2 x y
| _ \<Rightarrow> 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 \<le> 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 \<le> 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 \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum fst fst))\<inverse>\<inverse> OO
Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> 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)
--- 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 \<chi> \<phi>) A1 A2 \<longleftrightarrow>
+lemma rel_set_rel_sum[simp]:
+"rel_set (rel_sum \<chi> \<phi>) A1 A2 \<longleftrightarrow>
rel_set \<chi> (Inl -` A1) (Inl -` A2) \<and> rel_set \<phi> (Inr -` A1) (Inr -` A2)"
(is "?L \<longleftrightarrow> ?Rl \<and> ?Rr")
proof safe
assume L: "?L"
show ?Rl unfolding rel_set_def Bex_def vimage_eq proof safe
fix l1 assume "Inl l1 \<in> A1"
- then obtain a2 where a2: "a2 \<in> A2" and "sum_rel \<chi> \<phi> (Inl l1) a2"
+ then obtain a2 where a2: "a2 \<in> A2" and "rel_sum \<chi> \<phi> (Inl l1) a2"
using L unfolding rel_set_def by auto
then obtain l2 where "a2 = Inl l2 \<and> \<chi> l1 l2" by (cases a2, auto)
thus "\<exists> l2. Inl l2 \<in> A2 \<and> \<chi> l1 l2" using a2 by auto
next
fix l2 assume "Inl l2 \<in> A2"
- then obtain a1 where a1: "a1 \<in> A1" and "sum_rel \<chi> \<phi> a1 (Inl l2)"
+ then obtain a1 where a1: "a1 \<in> A1" and "rel_sum \<chi> \<phi> a1 (Inl l2)"
using L unfolding rel_set_def by auto
then obtain l1 where "a1 = Inl l1 \<and> \<chi> l1 l2" by (cases a1, auto)
thus "\<exists> l1. Inl l1 \<in> A1 \<and> \<chi> l1 l2" using a1 by auto
qed
show ?Rr unfolding rel_set_def Bex_def vimage_eq proof safe
fix r1 assume "Inr r1 \<in> A1"
- then obtain a2 where a2: "a2 \<in> A2" and "sum_rel \<chi> \<phi> (Inr r1) a2"
+ then obtain a2 where a2: "a2 \<in> A2" and "rel_sum \<chi> \<phi> (Inr r1) a2"
using L unfolding rel_set_def by auto
then obtain r2 where "a2 = Inr r2 \<and> \<phi> r1 r2" by (cases a2, auto)
thus "\<exists> r2. Inr r2 \<in> A2 \<and> \<phi> r1 r2" using a2 by auto
next
fix r2 assume "Inr r2 \<in> A2"
- then obtain a1 where a1: "a1 \<in> A1" and "sum_rel \<chi> \<phi> a1 (Inr r2)"
+ then obtain a1 where a1: "a1 \<in> A1" and "rel_sum \<chi> \<phi> a1 (Inr r2)"
using L unfolding rel_set_def by auto
then obtain r1 where "a1 = Inr r1 \<and> \<phi> r1 r2" by (cases a1, auto)
thus "\<exists> r1. Inr r1 \<in> A1 \<and> \<phi> 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 \<in> A1"
- show "\<exists> a2. a2 \<in> A2 \<and> sum_rel \<chi> \<phi> a1 a2"
+ show "\<exists> a2. a2 \<in> A2 \<and> rel_sum \<chi> \<phi> a1 a2"
proof(cases a1)
case (Inl l1) then obtain l2 where "Inl l2 \<in> A2 \<and> \<chi> l1 l2"
using Rl a1 unfolding rel_set_def by blast
@@ -1097,7 +1097,7 @@
qed
next
fix a2 assume a2: "a2 \<in> A2"
- show "\<exists> a1. a1 \<in> A1 \<and> sum_rel \<chi> \<phi> a1 a2"
+ show "\<exists> a1. a1 \<in> A1 \<and> rel_sum \<chi> \<phi> a1 a2"
proof(cases a2)
case (Inl l2) then obtain l1 where "Inl l1 \<in> A1 \<and> \<chi> l1 l2"
using Rl a2 unfolding rel_set_def by blast
--- 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 \<longleftrightarrow> sum_rel (\<lambda>x. R1 (f1 x)) (\<lambda>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 \<longleftrightarrow> rel_sum (\<lambda>x. R1 (f1 x)) (\<lambda>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) \<longleftrightarrow> sum_rel (\<lambda>x y. R1 x (f1 y)) (\<lambda>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) \<longleftrightarrow> rel_sum (\<lambda>x y. R1 x (f1 y)) (\<lambda>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 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
- unfolding reflp_def split_sum_all sum_rel_simps by fast
+lemma reflp_rel_sum:
+ "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (rel_sum R1 R2)"
+ unfolding reflp_def split_sum_all rel_sum_simps by fast
lemma sum_symp:
- "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
- unfolding symp_def split_sum_all sum_rel_simps by fast
+ "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (rel_sum R1 R2)"
+ unfolding symp_def split_sum_all rel_sum_simps by fast
lemma sum_transp:
- "transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (sum_rel R1 R2)"
- unfolding transp_def split_sum_all sum_rel_simps by fast
+ "transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (rel_sum R1 R2)"
+ unfolding transp_def split_sum_all rel_sum_simps by fast
lemma sum_equivp [quot_equiv]:
- "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)"
- by (blast intro: equivpI reflp_sum_rel sum_symp sum_transp elim: equivpE)
+ "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> 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]:
--- 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 \<equiv> 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 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)"
+lemma left_total_rel_sum[reflexivity_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_sum_rel [reflexivity_rule]:
- "left_unique R1 \<Longrightarrow> left_unique R2 \<Longrightarrow> left_unique (sum_rel R1 R2)"
+lemma left_unique_rel_sum [reflexivity_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_sum_rel [transfer_rule]:
- "right_total R1 \<Longrightarrow> right_total R2 \<Longrightarrow> right_total (sum_rel R1 R2)"
+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_sum_rel [transfer_rule]:
- "right_unique R1 \<Longrightarrow> right_unique R2 \<Longrightarrow> right_unique (sum_rel R1 R2)"
+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_sum_rel [transfer_rule]:
- "bi_total R1 \<Longrightarrow> bi_total R2 \<Longrightarrow> bi_total (sum_rel R1 R2)"
+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_sum_rel [transfer_rule]:
- "bi_unique R1 \<Longrightarrow> bi_unique R2 \<Longrightarrow> bi_unique (sum_rel R1 R2)"
+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_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
--- 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