--- a/src/HOL/BNF_Composition.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/BNF_Composition.thy Thu Aug 27 21:19:48 2015 +0200
@@ -82,7 +82,7 @@
"\<lbrakk>A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\<rbrakk> \<Longrightarrow> wpull A' B1' B2' f1 f2 p1 p2"
by simp
-lemma Grp_fst_snd: "(Grp (Collect (split R)) fst)^--1 OO Grp (Collect (split R)) snd = R"
+lemma Grp_fst_snd: "(Grp (Collect (case_prod R)) fst)^--1 OO Grp (Collect (case_prod R)) snd = R"
unfolding Grp_def fun_eq_iff relcompp.simps by auto
lemma OO_Grp_cong: "A = B \<Longrightarrow> (Grp A f)^--1 OO Grp A g = (Grp B f)^--1 OO Grp B g"
--- a/src/HOL/BNF_Def.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/BNF_Def.thy Thu Aug 27 21:19:48 2015 +0200
@@ -15,7 +15,7 @@
"bnf" :: thy_goal
begin
-lemma Collect_splitD: "x \<in> Collect (split A) \<Longrightarrow> A (fst x) (snd x)"
+lemma Collect_splitD: "x \<in> Collect (case_prod A) \<Longrightarrow> A (fst x) (snd x)"
by auto
inductive
@@ -98,7 +98,7 @@
unfolding convol_def by simp
lemma convol_mem_GrpI:
- "x \<in> A \<Longrightarrow> \<langle>id, g\<rangle> x \<in> (Collect (split (Grp A g)))"
+ "x \<in> A \<Longrightarrow> \<langle>id, g\<rangle> x \<in> (Collect (case_prod (Grp A g)))"
unfolding convol_def Grp_def by auto
definition csquare where
@@ -131,10 +131,10 @@
lemma GrpE: "Grp A f x y \<Longrightarrow> (\<lbrakk>f x = y; x \<in> A\<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
unfolding Grp_def by auto
-lemma Collect_split_Grp_eqD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> (f \<circ> fst) z = snd z"
+lemma Collect_split_Grp_eqD: "z \<in> Collect (case_prod (Grp A f)) \<Longrightarrow> (f \<circ> fst) z = snd z"
unfolding Grp_def comp_def by auto
-lemma Collect_split_Grp_inD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> fst z \<in> A"
+lemma Collect_split_Grp_inD: "z \<in> Collect (case_prod (Grp A f)) \<Longrightarrow> fst z \<in> A"
unfolding Grp_def comp_def by auto
definition "pick_middlep P Q a c = (SOME b. P a b \<and> Q b c)"
@@ -149,7 +149,7 @@
definition sndOp where
"sndOp P Q ac = (pick_middlep P Q (fst ac) (snd ac), (snd ac))"
-lemma fstOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> fstOp P Q ac \<in> Collect (split P)"
+lemma fstOp_in: "ac \<in> Collect (case_prod (P OO Q)) \<Longrightarrow> fstOp P Q ac \<in> Collect (case_prod P)"
unfolding fstOp_def mem_Collect_eq
by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct1])
@@ -159,7 +159,7 @@
lemma snd_sndOp: "snd bc = (snd \<circ> sndOp P Q) bc"
unfolding comp_def sndOp_def by simp
-lemma sndOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> sndOp P Q ac \<in> Collect (split Q)"
+lemma sndOp_in: "ac \<in> Collect (case_prod (P OO Q)) \<Longrightarrow> sndOp P Q ac \<in> Collect (case_prod Q)"
unfolding sndOp_def mem_Collect_eq
by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct2])
@@ -173,15 +173,15 @@
lemma fst_snd_flip: "fst xy = (snd \<circ> (%(x, y). (y, x))) xy"
by (simp split: prod.split)
-lemma flip_pred: "A \<subseteq> Collect (split (R ^--1)) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> Collect (split R)"
+lemma flip_pred: "A \<subseteq> Collect (case_prod (R ^--1)) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> Collect (case_prod R)"
by auto
-lemma Collect_split_mono: "A \<le> B \<Longrightarrow> Collect (split A) \<subseteq> Collect (split B)"
+lemma Collect_split_mono: "A \<le> B \<Longrightarrow> Collect (case_prod A) \<subseteq> Collect (case_prod B)"
by auto
lemma Collect_split_mono_strong:
- "\<lbrakk>X = fst ` A; Y = snd ` A; \<forall>a\<in>X. \<forall>b \<in> Y. P a b \<longrightarrow> Q a b; A \<subseteq> Collect (split P)\<rbrakk> \<Longrightarrow>
- A \<subseteq> Collect (split Q)"
+ "\<lbrakk>X = fst ` A; Y = snd ` A; \<forall>a\<in>X. \<forall>b \<in> Y. P a b \<longrightarrow> Q a b; A \<subseteq> Collect (case_prod P)\<rbrakk> \<Longrightarrow>
+ A \<subseteq> Collect (case_prod Q)"
by fastforce
@@ -216,7 +216,7 @@
lemma rel_fun_iff_leq_vimage2p: "(rel_fun R S) f g = (R \<le> vimage2p f g S)"
unfolding rel_fun_def vimage2p_def by auto
-lemma convol_image_vimage2p: "\<langle>f \<circ> fst, g \<circ> snd\<rangle> ` Collect (split (vimage2p f g R)) \<subseteq> Collect (split R)"
+lemma convol_image_vimage2p: "\<langle>f \<circ> fst, g \<circ> snd\<rangle> ` Collect (case_prod (vimage2p f g R)) \<subseteq> Collect (case_prod R)"
unfolding vimage2p_def convol_def by auto
lemma vimage2p_Grp: "vimage2p f g P = Grp UNIV f OO P OO (Grp UNIV g)\<inverse>\<inverse>"
--- a/src/HOL/BNF_Greatest_Fixpoint.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/BNF_Greatest_Fixpoint.thy Thu Aug 27 21:19:48 2015 +0200
@@ -82,13 +82,13 @@
lemma subset_CollectI: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> Q x \<Longrightarrow> P x) \<Longrightarrow> ({x \<in> B. Q x} \<subseteq> {x \<in> A. P x})"
by blast
-lemma in_rel_Collect_split_eq: "in_rel (Collect (split X)) = X"
+lemma in_rel_Collect_split_eq: "in_rel (Collect (case_prod X)) = X"
unfolding fun_eq_iff by auto
-lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (split (in_rel Y))"
+lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (case_prod (in_rel Y))"
by auto
-lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
+lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (case_prod (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
by force
lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
--- a/src/HOL/Basic_BNFs.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/Basic_BNFs.thy Thu Aug 27 21:19:48 2015 +0200
@@ -83,8 +83,8 @@
next
fix 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)"
+ (Grp {x. setl x \<subseteq> Collect (case_prod R) \<and> setr x \<subseteq> Collect (case_prod S)} (map_sum fst fst))\<inverse>\<inverse> OO
+ Grp {x. setl x \<subseteq> Collect (case_prod R) \<and> setr x \<subseteq> Collect (case_prod S)} (map_sum snd snd)"
unfolding sum_set_defs Grp_def relcompp.simps conversep.simps fun_eq_iff
by (fastforce elim: rel_sum.cases split: sum.splits)
qed (auto simp: sum_set_defs)
@@ -153,8 +153,8 @@
next
fix R S
show "rel_prod R S =
- (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod fst fst))\<inverse>\<inverse> OO
- Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod snd snd)"
+ (Grp {x. {fst x} \<subseteq> Collect (case_prod R) \<and> {snd x} \<subseteq> Collect (case_prod S)} (map_prod fst fst))\<inverse>\<inverse> OO
+ Grp {x. {fst x} \<subseteq> Collect (case_prod R) \<and> {snd x} \<subseteq> Collect (case_prod S)} (map_prod snd snd)"
unfolding prod_set_defs rel_prod_apply Grp_def relcompp.simps conversep.simps fun_eq_iff
by auto
qed
@@ -197,8 +197,8 @@
next
fix R
show "rel_fun op = R =
- (Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> fst))\<inverse>\<inverse> OO
- Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> snd)"
+ (Grp {x. range x \<subseteq> Collect (case_prod R)} (op \<circ> fst))\<inverse>\<inverse> OO
+ Grp {x. range x \<subseteq> Collect (case_prod R)} (op \<circ> snd)"
unfolding rel_fun_def Grp_def fun_eq_iff relcompp.simps conversep.simps subset_iff image_iff
comp_apply mem_Collect_eq split_beta bex_UNIV
proof (safe, unfold fun_eq_iff[symmetric])
--- a/src/HOL/Fun_Def.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/Fun_Def.thy Thu Aug 27 21:19:48 2015 +0200
@@ -143,7 +143,7 @@
lemma split_cong [fundef_cong]:
"(\<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y) \<Longrightarrow> p = q
- \<Longrightarrow> split f p = split g q"
+ \<Longrightarrow> case_prod f p = case_prod g q"
by (auto simp: split_def)
lemma comp_cong [fundef_cong]:
--- a/src/HOL/Groups_Big.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/Groups_Big.thy Thu Aug 27 21:19:48 2015 +0200
@@ -184,7 +184,7 @@
using assms by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute)
lemma Sigma:
- "finite A \<Longrightarrow> \<forall>x\<in>A. finite (B x) \<Longrightarrow> F (\<lambda>x. F (g x) (B x)) A = F (split g) (SIGMA x:A. B x)"
+ "finite A \<Longrightarrow> \<forall>x\<in>A. finite (B x) \<Longrightarrow> F (\<lambda>x. F (g x) (B x)) A = F (case_prod g) (SIGMA x:A. B x)"
apply (subst Sigma_def)
apply (subst UNION_disjoint, assumption, simp)
apply blast
@@ -350,7 +350,7 @@
qed
lemma cartesian_product:
- "F (\<lambda>x. F (g x) B) A = F (split g) (A <*> B)"
+ "F (\<lambda>x. F (g x) B) A = F (case_prod g) (A <*> B)"
apply (rule sym)
apply (cases "finite A")
apply (cases "finite B")
--- a/src/HOL/HOLCF/IOA/ABP/Abschannel.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel.thy Thu Aug 27 21:19:48 2015 +0200
@@ -5,7 +5,7 @@
section {* The transmission channel *}
theory Abschannel
-imports IOA Action Lemmas
+imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action Lemmas
begin
datatype 'a abs_action = S 'a | R 'a
--- a/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy Thu Aug 27 21:19:48 2015 +0200
@@ -5,7 +5,7 @@
section {* The transmission channel -- finite version *}
theory Abschannel_finite
-imports Abschannel IOA Action Lemmas
+imports Abschannel "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action Lemmas
begin
primrec reverse :: "'a list => 'a list"
--- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy Thu Aug 27 21:19:48 2015 +0200
@@ -5,7 +5,7 @@
section {* The main correctness proof: System_fin implements System *}
theory Correctness
-imports IOA Env Impl Impl_finite
+imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Env Impl Impl_finite
begin
ML_file "Check.ML"
--- a/src/HOL/HOLCF/IOA/ABP/Env.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Env.thy Thu Aug 27 21:19:48 2015 +0200
@@ -5,7 +5,7 @@
section {* The environment *}
theory Env
-imports IOA Action
+imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
begin
type_synonym
--- a/src/HOL/HOLCF/IOA/ABP/Receiver.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Receiver.thy Thu Aug 27 21:19:48 2015 +0200
@@ -5,7 +5,7 @@
section {* The implementation: receiver *}
theory Receiver
-imports IOA Action Lemmas
+imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action Lemmas
begin
type_synonym
--- a/src/HOL/HOLCF/IOA/ABP/Sender.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Sender.thy Thu Aug 27 21:19:48 2015 +0200
@@ -5,7 +5,7 @@
section {* The implementation: sender *}
theory Sender
-imports IOA Action Lemmas
+imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action Lemmas
begin
type_synonym
--- a/src/HOL/HOLCF/IOA/NTP/Abschannel.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Abschannel.thy Thu Aug 27 21:19:48 2015 +0200
@@ -5,7 +5,7 @@
section {* The (faulty) transmission channel (both directions) *}
theory Abschannel
-imports IOA Action
+imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
begin
datatype 'a abs_action = S 'a | R 'a
--- a/src/HOL/HOLCF/IOA/NTP/Receiver.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Receiver.thy Thu Aug 27 21:19:48 2015 +0200
@@ -5,7 +5,7 @@
section {* The implementation: receiver *}
theory Receiver
-imports IOA Action
+imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
begin
type_synonym
--- a/src/HOL/HOLCF/IOA/NTP/Sender.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Sender.thy Thu Aug 27 21:19:48 2015 +0200
@@ -5,7 +5,7 @@
section {* The implementation: sender *}
theory Sender
-imports IOA Action
+imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
begin
type_synonym
--- a/src/HOL/HOLCF/IOA/NTP/Spec.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Spec.thy Thu Aug 27 21:19:48 2015 +0200
@@ -5,7 +5,7 @@
section {* The specification of reliable transmission *}
theory Spec
-imports IOA Action
+imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
begin
definition
--- a/src/HOL/HOLCF/IOA/Storage/Spec.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/Storage/Spec.thy Thu Aug 27 21:19:48 2015 +0200
@@ -5,7 +5,7 @@
section {* The specification of a memory *}
theory Spec
-imports IOA Action
+imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
begin
definition
--- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy Thu Aug 27 21:19:48 2015 +0200
@@ -364,7 +364,7 @@
(* main case *)
apply clarify
apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
(* UU case *)
apply (simp add: nil_is_Conc)
(* nil case *)
@@ -431,7 +431,7 @@
temp_sat_def satisfies_def Init_def unlift_def)
apply auto
apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
apply (tactic {* pair_tac @{context} "a" 1 *})
done
@@ -441,7 +441,7 @@
lemma TL_ex2seq_UU:
"(TL$(ex2seq (cex_abs h ex))=UU) = (TL$(ex2seq ex)=UU)"
apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
apply (tactic {* pair_tac @{context} "a" 1 *})
apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
apply (tactic {* pair_tac @{context} "a" 1 *})
@@ -450,7 +450,7 @@
lemma TL_ex2seq_nil:
"(TL$(ex2seq (cex_abs h ex))=nil) = (TL$(ex2seq ex)=nil)"
apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
apply (tactic {* pair_tac @{context} "a" 1 *})
apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
apply (tactic {* pair_tac @{context} "a" 1 *})
@@ -474,7 +474,7 @@
lemma TLex2seq: "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL$(ex2seq ex) = ex2seq ex')"
apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
apply (tactic {* pair_tac @{context} "a" 1 *})
apply auto
done
@@ -482,7 +482,7 @@
lemma ex2seqnilTL: "(TL$(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)"
apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
apply (tactic {* pair_tac @{context} "a" 1 *})
apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
apply (tactic {* pair_tac @{context} "a" 1 *})
@@ -517,7 +517,7 @@
temp_sat_def satisfies_def Init_def unlift_def)
apply auto
apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
apply (tactic {* pair_tac @{context} "a" 1 *})
done
--- a/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy Thu Aug 27 21:19:48 2015 +0200
@@ -185,8 +185,7 @@
apply (auto simp add: mk_traceConc)
apply (frule reachable.reachable_n)
apply assumption
-apply (erule_tac x = "y" in allE)
-apply (simp add: move_subprop4 split add: split_if)
+apply (auto simp add: move_subprop4 split add: split_if)
done
declare split_if [split]
@@ -232,7 +231,7 @@
apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
(* main case *)
apply auto
-apply (rule_tac t = "f y" in lemma_2_1)
+apply (rule_tac t = "f x2" in lemma_2_1)
(* Finite *)
apply (erule move_subprop2)
@@ -246,7 +245,7 @@
(* Induction hypothesis *)
(* reachable_n looping, therefore apply it manually *)
-apply (erule_tac x = "y" in allE)
+apply (erule_tac x = "x2" in allE)
apply simp
apply (frule reachable.reachable_n)
apply assumption
--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Thu Aug 27 21:19:48 2015 +0200
@@ -1102,7 +1102,7 @@
THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt i)));
fun pair_tac ctxt s =
- Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), s)] [] @{thm PairE}
+ Rule_Insts.res_inst_tac ctxt [((("y", 0), Position.none), s)] [] @{thm PairE}
THEN' hyp_subst_tac ctxt THEN' asm_full_simp_tac ctxt;
(* induction on a sequence of pairs with pairsplitting and simplification *)
--- a/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy Thu Aug 27 21:19:48 2015 +0200
@@ -227,7 +227,7 @@
apply (simp add: executions_def)
apply (tactic {* pair_tac @{context} "ex" 1 *})
apply auto
-apply (rule_tac x = " (x,Cut (%a. fst a:ext A) y) " in exI)
+apply (rule_tac x = " (x1,Cut (%a. fst a:ext A) x2) " in exI)
apply (simp (no_asm_simp))
(* Subgoal 1: Lemma: propagation of execution through Cut *)
@@ -237,7 +237,7 @@
(* Subgoal 2: Lemma: Filter P s = Filter P (Cut P s) *)
apply (simp (no_asm) add: filter_act_def)
-apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) y) = Cut (%a. a:ext A) (Map fst$y) ")
+apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) x2) = Cut (%a. a:ext A) (Map fst$x2) ")
apply (rule_tac [2] MapCut [unfolded o_def])
apply (simp add: FilterCut [symmetric])
@@ -245,7 +245,7 @@
(* Subgoal 3: Lemma: Cut idempotent *)
apply (simp (no_asm) add: LastActExtsch_def filter_act_def)
-apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) y) = Cut (%a. a:ext A) (Map fst$y) ")
+apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) x2) = Cut (%a. a:ext A) (Map fst$x2) ")
apply (rule_tac [2] MapCut [unfolded o_def])
apply (simp add: Cut_idemp)
done
--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Thu Aug 27 21:19:48 2015 +0200
@@ -152,7 +152,7 @@
lemma ex2seq_nUUnnil: "ex2seq exec ~= UU & ex2seq exec ~= nil"
apply (tactic {* pair_tac @{context} "exec" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
apply (tactic {* pair_tac @{context} "a" 1 *})
done
@@ -173,14 +173,14 @@
(* TL = UU *)
apply (rule conjI)
apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
apply (tactic {* pair_tac @{context} "a" 1 *})
apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
apply (tactic {* pair_tac @{context} "a" 1 *})
(* TL = nil *)
apply (rule conjI)
apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_tac @{context} "x2" 1 *})
apply (simp add: unlift_def)
apply fast
apply (simp add: unlift_def)
@@ -193,7 +193,7 @@
apply (simp add: unlift_def)
apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
apply (tactic {* pair_tac @{context} "a" 1 *})
apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
apply (tactic {* pair_tac @{context} "a" 1 *})
--- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy Thu Aug 27 21:19:48 2015 +0200
@@ -396,7 +396,7 @@
lemma execfrag_prefixclosed: "!x s. is_exec_frag A (s,x) & y<<x --> is_exec_frag A (s,y)"
apply (tactic {* pair_induct_tac @{context} "y" [@{thm is_exec_frag_def}] 1 *})
apply (intro strip)
-apply (tactic {* Seq_case_simp_tac @{context} "xa" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x" 1 *})
apply (tactic {* pair_tac @{context} "a" 1 *})
apply auto
done
--- a/src/HOL/Hilbert_Choice.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/Hilbert_Choice.thy Thu Aug 27 21:19:48 2015 +0200
@@ -546,7 +546,7 @@
lemma split_paired_Eps: "(SOME x. P x) = (SOME (a,b). P(a,b))"
by simp
-lemma Eps_split: "Eps (split P) = (SOME xy. P (fst xy) (snd xy))"
+lemma Eps_split: "Eps (case_prod P) = (SOME xy. P (fst xy) (snd xy))"
by (simp add: split_def)
lemma Eps_split_eq [simp]: "(@(x',y'). x = x' & y = y') = (x,y)"
--- a/src/HOL/List.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/List.thy Thu Aug 27 21:19:48 2015 +0200
@@ -2664,7 +2664,7 @@
by (simp add: list_all2_conv_all_nth)
lemma list_all2I:
- "\<forall>x \<in> set (zip a b). split P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
+ "\<forall>x \<in> set (zip a b). case_prod P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
by (simp add: list_all2_iff)
lemma list_all2_nthD:
--- a/src/HOL/Map.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/Map.thy Thu Aug 27 21:19:48 2015 +0200
@@ -227,14 +227,14 @@
lemma map_of_mapk_SomeI:
"inj f \<Longrightarrow> map_of t k = Some x \<Longrightarrow>
- map_of (map (split (\<lambda>k. Pair (f k))) t) (f k) = Some x"
+ map_of (map (case_prod (\<lambda>k. Pair (f k))) t) (f k) = Some x"
by (induct t) (auto simp: inj_eq)
lemma weak_map_of_SomeI: "(k, x) \<in> set l \<Longrightarrow> \<exists>x. map_of l k = Some x"
by (induct l) auto
lemma map_of_filter_in:
- "map_of xs k = Some z \<Longrightarrow> P k z \<Longrightarrow> map_of (filter (split P) xs) k = Some z"
+ "map_of xs k = Some z \<Longrightarrow> P k z \<Longrightarrow> map_of (filter (case_prod P) xs) k = Some z"
by (induct xs) auto
lemma map_of_map:
--- a/src/HOL/Probability/Caratheodory.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/Probability/Caratheodory.thy Thu Aug 27 21:19:48 2015 +0200
@@ -516,11 +516,10 @@
finally show ?thesis .
qed
def C \<equiv> "(split BB) o prod_decode"
- have C: "!!n. C n \<in> M"
- apply (rule_tac p="prod_decode n" in PairE)
- apply (simp add: C_def)
- apply (metis BB subsetD rangeI)
- done
+ from BB have "\<And>i j. BB i j \<in> M"
+ by (rule range_subsetD)
+ then have C: "\<And>n. C n \<in> M"
+ by (simp add: C_def split_def)
have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
proof (auto simp add: C_def)
fix x i
--- a/src/HOL/Product_Type.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/Product_Type.thy Thu Aug 27 21:19:48 2015 +0200
@@ -284,9 +284,6 @@
subsubsection \<open>Tuple syntax\<close>
-abbreviation (input) split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
- "split \<equiv> case_prod"
-
text \<open>
Patterns -- extends pre-defined type @{typ pttrn} used in
abstractions.
@@ -310,6 +307,11 @@
"%(x, y, zs). b" == "CONST case_prod (%x (y, zs). b)"
"%(x, y). b" == "CONST case_prod (%x y. b)"
"_abs (CONST Pair x y) t" => "%(x, y). t"
+
+
+
+
+
-- \<open>The last rule accommodates tuples in `case C ... (x,y) ... => ...'
The (x,y) is parsed as `Pair x y' because it is logic, not pttrn\<close>
@@ -435,13 +437,13 @@
lemma prod_eqI [intro?]: "fst p = fst q \<Longrightarrow> snd p = snd q \<Longrightarrow> p = q"
by (simp add: prod_eq_iff)
-lemma split_conv [simp, code]: "split f (a, b) = f a b"
+lemma split_conv [simp, code]: "case_prod f (a, b) = f a b"
by (fact prod.case)
-lemma splitI: "f a b \<Longrightarrow> split f (a, b)"
+lemma splitI: "f a b \<Longrightarrow> case_prod f (a, b)"
by (rule split_conv [THEN iffD2])
-lemma splitD: "split f (a, b) \<Longrightarrow> f a b"
+lemma splitD: "case_prod f (a, b) \<Longrightarrow> f a b"
by (rule split_conv [THEN iffD1])
lemma split_Pair [simp]: "(\<lambda>(x, y). (x, y)) = id"
@@ -451,13 +453,13 @@
-- \<open>Subsumes the old @{text split_Pair} when @{term f} is the identity function.\<close>
by (simp add: fun_eq_iff split: prod.split)
-lemma split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)"
+lemma split_comp: "case_prod (f \<circ> g) x = f (g (fst x)) (snd x)"
by (cases x) simp
-lemma split_twice: "split f (split g p) = split (\<lambda>x y. split f (g x y)) p"
- by (cases p) simp
+lemma split_twice: "case_prod f (case_prod g p) = case_prod (\<lambda>x y. case_prod f (g x y)) p"
+ by (fact prod.case_distrib)
-lemma The_split: "The (split P) = (THE xy. P (fst xy) (snd xy))"
+lemma The_split: "The (case_prod P) = (THE xy. P (fst xy) (snd xy))"
by (simp add: case_prod_unfold)
lemmas split_weak_cong = prod.case_cong_weak
@@ -602,31 +604,31 @@
lemmas split_split_asm [no_atp] = prod.split_asm
text \<open>
- \medskip @{term split} used as a logical connective or set former.
+ \medskip @{const case_prod} used as a logical connective or set former.
\medskip These rules are for use with @{text blast}; could instead
call @{text simp} using @{thm [source] prod.split} as rewrite.\<close>
-lemma splitI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> split c p"
+lemma splitI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> case_prod c p"
apply (simp only: split_tupled_all)
apply (simp (no_asm_simp))
done
-lemma splitI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> split c p x"
+lemma splitI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> case_prod c p x"
apply (simp only: split_tupled_all)
apply (simp (no_asm_simp))
done
-lemma splitE: "split c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
+lemma splitE: "case_prod c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
by (induct p) auto
-lemma splitE': "split c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
+lemma splitE': "case_prod c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
by (induct p) auto
lemma splitE2:
- "[| Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R"
+ "[| Q (case_prod P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R"
proof -
- assume q: "Q (split P z)"
+ assume q: "Q (case_prod P z)"
assume r: "!!x y. [|z = (x, y); Q (P x y)|] ==> R"
show R
apply (rule r surjective_pairing)+
@@ -634,17 +636,17 @@
done
qed
-lemma splitD': "split R (a,b) c ==> R a b c"
+lemma splitD': "case_prod R (a,b) c ==> R a b c"
by simp
-lemma mem_splitI: "z: c a b ==> z: split c (a, b)"
+lemma mem_splitI: "z: c a b ==> z: case_prod c (a, b)"
by simp
-lemma mem_splitI2: "!!p. [| !!a b. p = (a, b) ==> z: c a b |] ==> z: split c p"
+lemma mem_splitI2: "!!p. [| !!a b. p = (a, b) ==> z: c a b |] ==> z: case_prod c p"
by (simp only: split_tupled_all, simp)
lemma mem_splitE:
- assumes "z \<in> split c p"
+ assumes "z \<in> case_prod c p"
obtains x y where "p = (x, y)" and "z \<in> c x y"
using assms by (rule splitE2)
@@ -672,10 +674,10 @@
lemma split_eta_SetCompr [simp, no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
by (rule ext) fast
-lemma split_eta_SetCompr2 [simp, no_atp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
+lemma split_eta_SetCompr2 [simp, no_atp]: "(%u. EX x y. u = (x, y) & P x y) = case_prod P"
by (rule ext) fast
-lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"
+lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & case_prod Q ab)"
-- \<open>Allows simplifications of nested splits in case of independent predicates.\<close>
by (rule ext) blast
@@ -685,7 +687,7 @@
*)
lemma split_comp_eq:
fixes f :: "'a => 'b => 'c" and g :: "'d => 'a"
- shows "(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))"
+ shows "(%u. f (g (fst u)) (snd u)) = (case_prod (%x. f (g x)))"
by (rule ext) auto
lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A"
@@ -773,12 +775,8 @@
"(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
by (cases x) blast
-lemma split_def:
- "split = (\<lambda>c p. c (fst p) (snd p))"
- by (fact case_prod_unfold)
-
definition internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
- "internal_split == split"
+ "internal_split == case_prod"
lemma internal_split_conv: "internal_split c (a, b) = c a b"
by (simp only: internal_split_def split_conv)
@@ -805,11 +803,11 @@
lemma curryE: "curry f a b \<Longrightarrow> (f (a, b) \<Longrightarrow> Q) \<Longrightarrow> Q"
by (simp add: curry_def)
-lemma curry_split [simp]: "curry (split f) = f"
- by (simp add: curry_def split_def)
+lemma curry_split [simp]: "curry (case_prod f) = f"
+ by (simp add: curry_def case_prod_unfold)
-lemma split_curry [simp]: "split (curry f) = f"
- by (simp add: curry_def split_def)
+lemma split_curry [simp]: "case_prod (curry f) = f"
+ by (simp add: curry_def case_prod_unfold)
lemma curry_K: "curry (\<lambda>x. c) = (\<lambda>x y. c)"
by(simp add: fun_eq_iff)
@@ -1120,11 +1118,11 @@
by (blast elim: equalityE)
lemma SetCompr_Sigma_eq:
- "Collect (split (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))"
+ "Collect (case_prod (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))"
by blast
lemma Collect_split [simp]: "{(a,b). P a & Q b} = Collect P <*> Collect Q"
- by blast
+ by (fact SetCompr_Sigma_eq)
lemma UN_Times_distrib:
"(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)"
@@ -1357,16 +1355,17 @@
subsection \<open>Legacy theorem bindings and duplicates\<close>
-lemma PairE:
- obtains x y where "p = (x, y)"
- by (fact prod.exhaust)
+abbreviation (input) split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
+ "split \<equiv> case_prod"
+lemmas PairE = prod.exhaust
lemmas Pair_eq = prod.inject
lemmas fst_conv = prod.sel(1)
lemmas snd_conv = prod.sel(2)
lemmas pair_collapse = prod.collapse
lemmas split = split_conv
lemmas Pair_fst_snd_eq = prod_eq_iff
+lemmas split_def = case_prod_unfold
hide_const (open) prod
--- a/src/HOL/String.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/String.thy Thu Aug 27 21:19:48 2015 +0200
@@ -128,9 +128,9 @@
ML_file "Tools/string_syntax.ML"
lemma UNIV_char:
- "UNIV = image (split Char) (UNIV \<times> UNIV)"
+ "UNIV = image (case_prod Char) (UNIV \<times> UNIV)"
proof (rule UNIV_eq_I)
- fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
+ fix x show "x \<in> image (case_prod Char) (UNIV \<times> UNIV)" by (cases x) auto
qed
lemma size_char [code, simp]:
@@ -218,7 +218,7 @@
"Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
lemma enum_char_product_enum_nibble:
- "(Enum.enum :: char list) = map (split Char) (List.product Enum.enum Enum.enum)"
+ "(Enum.enum :: char list) = map (case_prod Char) (List.product Enum.enum Enum.enum)"
by (simp add: enum_char_def enum_nibble_def)
instance proof
--- a/src/HOL/Transitive_Closure.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/Transitive_Closure.thy Thu Aug 27 21:19:48 2015 +0200
@@ -169,8 +169,9 @@
lemma rtrancl_Int_subset: "[| Id \<subseteq> s; (r^* \<inter> s) O r \<subseteq> s|] ==> r^* \<subseteq> s"
apply (rule subsetI)
- apply (rule_tac p="x" in PairE, clarify)
- apply (erule rtrancl_induct, auto)
+ apply auto
+ apply (erule rtrancl_induct)
+ apply auto
done
lemma converse_rtranclp_into_rtranclp:
@@ -409,10 +410,9 @@
lemma trancl_Int_subset: "[| r \<subseteq> s; (r^+ \<inter> s) O r \<subseteq> s|] ==> r^+ \<subseteq> s"
apply (rule subsetI)
- apply (rule_tac p = x in PairE)
- apply clarify
+ apply auto
apply (erule trancl_induct)
- apply auto
+ apply auto
done
lemma trancl_unfold: "r^+ = r Un r^+ O r"