--- a/Nominal/Ex/Pi.thy Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/Ex/Pi.thy Thu Mar 13 09:21:31 2014 +0000
@@ -130,20 +130,20 @@
lemma testl:
assumes a: "\<exists>y. f = Inl y"
- shows "(p \<bullet> (Sum_Type.Projl f)) = Sum_Type.Projl (p \<bullet> f)"
+ shows "(p \<bullet> (Sum_Type.projl f)) = Sum_Type.projl (p \<bullet> f)"
using a by auto
lemma testrr:
assumes a: "\<exists>y. f = Inr (Inr y)"
- shows "(p \<bullet> (Sum_Type.Projr (Sum_Type.Projr f))) = Sum_Type.Projr (Sum_Type.Projr (p \<bullet> f))"
+ shows "(p \<bullet> (Sum_Type.projr (Sum_Type.projr f))) = Sum_Type.projr (Sum_Type.projr (p \<bullet> f))"
using a by auto
lemma testlr:
assumes a: "\<exists>y. f = Inr (Inl y)"
- shows "(p \<bullet> (Sum_Type.Projl (Sum_Type.Projr f))) = Sum_Type.Projl (Sum_Type.Projr (p \<bullet> f))"
+ shows "(p \<bullet> (Sum_Type.projl (Sum_Type.projr f))) = Sum_Type.projl (Sum_Type.projr (p \<bullet> f))"
using a by auto
-nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (sum_case (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))")
+nominal_primrec (default "case_sum (\<lambda>x. Inl undefined) (case_sum (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))")
subsGuard_mix :: "guardedTerm_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> guardedTerm_mix" ("_[_::=\<onesuperior>\<onesuperior>_]" [100, 100, 100] 100) and
subsList_mix :: "sumList_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> sumList_mix" ("_[_::=\<onesuperior>\<twosuperior>_]" [100, 100, 100] 100) and
subs_mix :: "piMix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> piMix" ("_[_::=\<onesuperior>_]" [100, 100, 100] 100)
@@ -240,33 +240,33 @@
apply (metis Inr_not_Inl)
apply (metis Inr_inject Inr_not_Inl)
apply (metis Inr_inject Inr_not_Inl)
-apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.Projr
- (Sum_Type.Projr
+apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.projr
+ (Sum_Type.projr
(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
apply clarify
apply (rule the1_equality)
apply blast apply assumption
-apply (rule_tac x="Sum_Type.Projr
- (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
- Sum_Type.Projr
- (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
+apply (rule_tac x="Sum_Type.projr
+ (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
+ Sum_Type.projr
+ (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
apply clarify
apply (rule the1_equality)
apply blast apply assumption
-apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.Projr
- (Sum_Type.Projr
+apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.projr
+ (Sum_Type.projr
(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
apply clarify
apply (rule the1_equality)
apply blast apply assumption
-apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.Projl
- (Sum_Type.Projr
+apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.projl
+ (Sum_Type.projr
(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI)
apply clarify
apply (rule the1_equality)
apply blast apply assumption
-apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.Projr
- (Sum_Type.Projr
+apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.projr
+ (Sum_Type.projr
(subsGuard_mix_subsList_mix_subs_mix_sum
(Inr (Inr (Pb, xb, y)))))" in exI)
apply clarify
@@ -333,33 +333,33 @@
apply (metis Inr_not_Inl)
apply (metis Inr_inject Inr_not_Inl)
apply (metis Inr_inject Inr_not_Inl)
-apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.Projr
- (Sum_Type.Projr
+apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.projr
+ (Sum_Type.projr
(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
apply clarify
apply (rule the1_equality)
apply blast apply assumption
-apply (rule_tac x="Sum_Type.Projr
- (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
- Sum_Type.Projr
- (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
+apply (rule_tac x="Sum_Type.projr
+ (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
+ Sum_Type.projr
+ (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
apply clarify
apply (rule the1_equality)
apply blast apply assumption
-apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.Projr
- (Sum_Type.Projr
+apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.projr
+ (Sum_Type.projr
(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
apply clarify
apply (rule the1_equality)
apply blast apply assumption
-apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.Projl
- (Sum_Type.Projr
+apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.projl
+ (Sum_Type.projr
(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI)
apply clarify
apply (rule the1_equality)
apply blast apply assumption
-apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.Projr
- (Sum_Type.Projr
+apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.projr
+ (Sum_Type.projr
(subsGuard_mix_subsList_mix_subs_mix_sum
(Inr (Inr (Pb, xb, y)))))" in exI)
apply clarify