nominal2: Nominal/Ex/Pi.thy@a44479bde681 (annotated)

3244 a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	1	(* Theory be Kirstin Peters *)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	2
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	3	theory Pi
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	4	imports "../Nominal2"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	5	begin
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	6
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	7	atom_decl name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	8
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	9	subsection {* Capture-Avoiding Substitution of Names *}
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	10
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	11	definition
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	12	subst_name :: "name \<Rightarrow> name \<Rightarrow> name \<Rightarrow> name" ("_[_:::=_]" [110, 110, 110] 110)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	13	where
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	14	"a[b:::=c] \<equiv> if (a = b) then c else a"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	15
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	16	declare subst_name_def[simp]
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	17
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	18	lemma subst_name_mix_eqvt[eqvt]:
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	19	fixes p :: perm
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	20	and a :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	21	and b :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	22	and c :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	23
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	24	shows "p \<bullet> (a[b:::=c]) = (p \<bullet> a)[(p \<bullet> b):::=(p \<bullet> c)]"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	25	proof -
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	26	show ?thesis
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	27	by(auto)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	28	qed
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	29
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	30	nominal_function
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	31	subst_name_list :: "name \<Rightarrow> (name \<times> name) list \<Rightarrow> name"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	32	where
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	33	"subst_name_list a [] = a"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	34	\| "subst_name_list a ((b, c)#xs) = (if (a = b) then c else (subst_name_list a xs))"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	35	apply(simp add: eqvt_def subst_name_list_graph_aux_def)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	36	apply(simp)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	37	apply(auto)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	38	apply(rule_tac y="b" in list.exhaust)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	39	by(auto)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	40
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	41	nominal_termination (eqvt)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	42	by (lexicographic_order)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	43
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	44
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	45	section {* The Synchronous Pi-Calculus *}
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	46
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	47	subsection {* Syntax: Synchronous, Monadic Pi-Calculus with n-ary, Mixed Choice *}
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	48
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	49	nominal_datatype
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	50	guardedTerm_mix = Output name name piMix ("_!<_>\<onesuperior>._" [120, 120, 110] 110)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	51	\| Input name b::name P::piMix binds b in P ("_?<_>\<onesuperior>._" [120, 120, 110] 110)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	52	\| Tau piMix ("<\<tau>\<onesuperior>>._" [110] 110)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	53	and sumList_mix = SumNil ("\<zero>\<onesuperior>")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	54	\| AddSummand guardedTerm_mix sumList_mix (infixr "\<oplus>\<onesuperior>" 65)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	55	and piMix = Res a::name P::piMix binds a in P ("<\<nu>_>\<onesuperior>_" [100, 100] 100)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	56	\| Par piMix piMix (infixr "\<parallel>\<onesuperior>" 85)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	57	\| Match name name piMix ("[_\<frown>\<onesuperior>_]_" [120, 120, 110] 110)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	58	\| Sum sumList_mix ("\<oplus>\<onesuperior>{_}" 90)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	59	\| Rep name b::name P::piMix binds b in P ("\<infinity>_?<_>\<onesuperior>._" [120, 120, 110] 110)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	60	\| Succ ("succ\<onesuperior>")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	61
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	62	lemmas piMix_strong_induct = guardedTerm_mix_sumList_mix_piMix.strong_induct
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	63	lemmas piMix_fresh = guardedTerm_mix_sumList_mix_piMix.fresh
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	64	lemmas piMix_eq_iff = guardedTerm_mix_sumList_mix_piMix.eq_iff
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	65	lemmas piMix_distinct = guardedTerm_mix_sumList_mix_piMix.distinct
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	66	lemmas piMix_size = guardedTerm_mix_sumList_mix_piMix.size
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	67
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	68	subsection {* Alpha-Conversion Lemmata *}
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	69
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	70	lemma alphaRes_mix:
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	71	fixes a :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	72	and P :: piMix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	73	and z :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	74
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	75	assumes "atom z \<sharp> P"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	76
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	77	shows "<\<nu>a>\<onesuperior>P = <\<nu>z>\<onesuperior>((atom a \<rightleftharpoons> atom z) \<bullet> P)"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	78	proof(cases "a = z")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	79	assume "a = z"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	80	thus ?thesis
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	81	by(simp)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	82	next
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	83	assume "a \<noteq> z"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	84	thus ?thesis
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	85	using assms
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	86	by (simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	87	qed
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	88
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	89	lemma alphaInput_mix:
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	90	fixes a :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	91	and b :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	92	and P :: piMix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	93	and z :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	94
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	95	assumes "atom z \<sharp> P"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	96
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	97	shows "a?<b>\<onesuperior>.P = a?<z>\<onesuperior>.((atom b \<rightleftharpoons> atom z) \<bullet> P)"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	98	proof(cases "b = z")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	99	assume "b = z"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	100	thus ?thesis
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	101	by(simp)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	102	next
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	103	assume "b \<noteq> z"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	104	thus ?thesis
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	105	using assms
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	106	by(simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	107	qed
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	108
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	109	lemma alphaRep_mix:
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	110	fixes a :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	111	and b :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	112	and P :: piMix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	113	and z :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	114
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	115	assumes "atom z \<sharp> P"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	116
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	117	shows "\<infinity>a?<b>\<onesuperior>.P = \<infinity>a?<z>\<onesuperior>.((atom b \<rightleftharpoons> atom z) \<bullet> P)"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	118	proof(cases "b = z")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	119	assume "b = z"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	120	thus ?thesis
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	121	by(simp)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	122	next
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	123	assume "b \<noteq> z"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	124	thus ?thesis
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	125	using assms
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	126	by(simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	127	qed
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	128
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	129	subsection {* Capture-Avoiding Substitution of Names *}
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	130
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	131	lemma testl:
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	132	assumes a: "\<exists>y. f = Inl y"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	133	shows "(p \<bullet> (Sum_Type.projl f)) = Sum_Type.projl (p \<bullet> f)"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	134	using a by auto
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	135
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	136	lemma testrr:
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	137	assumes a: "\<exists>y. f = Inr (Inr y)"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	138	shows "(p \<bullet> (Sum_Type.projr (Sum_Type.projr f))) = Sum_Type.projr (Sum_Type.projr (p \<bullet> f))"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	139	using a by auto
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	140
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	141	lemma testlr:
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	142	assumes a: "\<exists>y. f = Inr (Inl y)"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	143	shows "(p \<bullet> (Sum_Type.projl (Sum_Type.projr f))) = Sum_Type.projl (Sum_Type.projr (p \<bullet> f))"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	144	using a by auto
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	145
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	146	nominal_function (default "case_sum (\<lambda>x. Inl undefined) (case_sum (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	147	subsGuard_mix :: "guardedTerm_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> guardedTerm_mix" ("_[_::=\<onesuperior>\<onesuperior>_]" [100, 100, 100] 100) and
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	148	subsList_mix :: "sumList_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> sumList_mix" ("_[_::=\<onesuperior>\<twosuperior>_]" [100, 100, 100] 100) and
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	149	subs_mix :: "piMix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> piMix" ("_[_::=\<onesuperior>_]" [100, 100, 100] 100)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	150	where
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	151	"(a!<b>\<onesuperior>.P)[x::=\<onesuperior>\<onesuperior>y] = (a[x:::=y])!<(b[x:::=y])>\<onesuperior>.(P[x::=\<onesuperior>y])"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	152	\| "\<lbrakk>atom b \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (a?<b>\<onesuperior>.P)[x::=\<onesuperior>\<onesuperior>y] = (a[x:::=y])?<b>\<onesuperior>.(P[x::=\<onesuperior>y])"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	153	\| "(<\<tau>\<onesuperior>>.P)[x::=\<onesuperior>\<onesuperior>y] = <\<tau>\<onesuperior>>.(P[x::=\<onesuperior>y])"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	154	\| "(\<zero>\<onesuperior>)[x::=\<onesuperior>\<twosuperior>y] = \<zero>\<onesuperior>"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	155	\| "(g \<oplus>\<onesuperior> xg)[x::=\<onesuperior>\<twosuperior>y] = (g[x::=\<onesuperior>\<onesuperior>y]) \<oplus>\<onesuperior> (xg[x::=\<onesuperior>\<twosuperior>y])"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	156	\| "\<lbrakk>atom a \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (<\<nu>a>\<onesuperior>P)[x::=\<onesuperior>y] = <\<nu>a>\<onesuperior>(P[x::=\<onesuperior>y])"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	157	\| "(P \<parallel>\<onesuperior> Q)[x::=\<onesuperior>y] = (P[x::=\<onesuperior>y]) \<parallel>\<onesuperior> (Q[x::=\<onesuperior>y])"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	158	\| "([a\<frown>\<onesuperior>b]P)[x::=\<onesuperior>y] = ([(a[x:::=y])\<frown>\<onesuperior>(b[x:::=y])](P[x::=\<onesuperior>y]))"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	159	\| "(\<oplus>\<onesuperior>{xg})[x::=\<onesuperior>y] = \<oplus>\<onesuperior>{(xg[x::=\<onesuperior>\<twosuperior>y])}"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	160	\| "\<lbrakk>atom b \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (\<infinity>a?<b>\<onesuperior>.P)[x::=\<onesuperior>y] = \<infinity>(a[x:::=y])?<b>\<onesuperior>.(P[x::=\<onesuperior>y])"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	161	\| "(succ\<onesuperior>)[x::=\<onesuperior>y] = succ\<onesuperior>"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	162	using [[simproc del: alpha_lst]]
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	163	apply(auto simp add: piMix_distinct piMix_eq_iff)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	164	apply(simp add: eqvt_def subsGuard_mix_subsList_mix_subs_mix_graph_aux_def)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	165	--"Covered all cases"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	166	apply(case_tac x)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	167	apply(simp)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	168	apply(case_tac a)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	169	apply(simp)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	170	apply (rule_tac y="aa" and c="(b, c)" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(1))
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	171	apply(blast)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	172	apply(auto simp add: fresh_star_def)[1]
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	173	apply(blast)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	174	apply(simp)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	175	apply(case_tac b)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	176	apply(simp)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	177	apply(case_tac a)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	178	apply(simp)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	179	apply (rule_tac ya="aa" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(2))
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	180	apply(blast)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	181	apply(blast)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	182	apply(simp)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	183	apply(case_tac ba)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	184	apply(simp)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	185	apply (rule_tac yb="a" and c="(bb,c)" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(3))
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	186	using [[simproc del: alpha_lst]]
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	187	apply(auto simp add: fresh_star_def)[1]
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	188	apply(blast)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	189	apply(blast)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	190	apply(blast)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	191	using [[simproc del: alpha_lst]]
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	192	apply(auto simp add: fresh_star_def)[1]
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	193	apply(simp)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	194	--"compatibility"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	195	apply (simp only: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff])
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	196	apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	197	apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (P, xa, ya)))")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	198	apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (Pa, xa, ya)))")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	199	prefer 2
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	200	apply (simp only: eqvt_at_def subs_mix_def)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	201	apply rule
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	202	apply(simp (no_asm))
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	203	apply (subst testrr)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	204	apply (simp add: subsGuard_mix_subsList_mix_subs_mix_sumC_def)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	205	apply (simp add: THE_default_def)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	206	apply (case_tac "Ex1 (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya))))")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	207	apply simp_all[2]
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	208	apply auto[1]
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	209	apply (erule_tac x="x" in allE)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	210	apply simp
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	211	apply(thin_tac "\<forall>p. p \<bullet> The (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya)))) =
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	212	(if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	213	then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	214	else Inr (Inr undefined))")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	215	apply(thin_tac "\<forall>p. p \<bullet> (if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	216	then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	217	else Inr (Inr undefined)) =
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	218	(if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	219	then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	220	else Inr (Inr undefined))")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	221	apply (thin_tac "atom b \<sharp> (xa, ya)")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	222	apply (thin_tac "atom ba \<sharp> (xa, ya)")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	223	apply (thin_tac "[[atom b]]lst. P = [[atom ba]]lst. Pa")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	224	apply(cases rule: subsGuard_mix_subsList_mix_subs_mix_graph.cases)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	225	apply assumption
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	226	apply (metis Inr_not_Inl)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	227	apply (metis Inr_not_Inl)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	228	apply (metis Inr_not_Inl)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	229	apply (metis Inr_inject Inr_not_Inl)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	230	apply (metis Inr_inject Inr_not_Inl)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	231	apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.projr
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	232	(Sum_Type.projr
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	233	(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	234	apply clarify
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	235	apply (rule the1_equality)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	236	apply blast apply assumption
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	237	apply (rule_tac x="Sum_Type.projr
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	238	(Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	239	Sum_Type.projr
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	240	(Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	241	apply clarify
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	242	apply (rule the1_equality)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	243	apply blast apply assumption
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	244	apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.projr
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	245	(Sum_Type.projr
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	246	(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	247	apply clarify
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	248	apply (rule the1_equality)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	249	apply blast apply assumption
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	250	apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.projl
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	251	(Sum_Type.projr
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	252	(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	253	apply clarify
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	254	apply (rule the1_equality)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	255	apply blast apply assumption
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	256	apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.projr
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	257	(Sum_Type.projr
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	258	(subsGuard_mix_subsList_mix_subs_mix_sum
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	259	(Inr (Inr (Pb, xb, y)))))" in exI)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	260	apply clarify
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	261	apply (rule the1_equality)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	262	apply blast apply assumption
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	263	apply (rule_tac x="succ\<onesuperior>" in exI)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	264	apply clarify
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	265	apply (rule the1_equality)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	266	apply blast apply assumption
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	267	apply simp
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	268	(* Here the only real goal compatibility is left *)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	269	apply (erule Abs_lst1_fcb)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	270	apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	271	apply (subgoal_tac "atom ba \<sharp> (\<lambda>(a, x, y). subs_mix a x y) (P, xa, ya)")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	272	apply simp
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	273	apply (erule fresh_eqvt_at)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	274	apply(simp add: finite_supp)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	275	apply(simp)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	276	apply(simp add: eqvt_at_def)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	277	apply(drule_tac x="(b \<leftrightarrow> ba)" in spec)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	278	apply(simp)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	279	apply (simp only: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff])
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	280	apply(rename_tac b P ba xa ya Pa)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	281	apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	282	apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (P, xa, ya)))")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	283	apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (Pa, xa, ya)))")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	284	prefer 2
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	285	apply (simp only: eqvt_at_def subs_mix_def)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	286	apply rule
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	287	apply(simp (no_asm))
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	288	apply (subst testrr)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	289	apply (simp add: subsGuard_mix_subsList_mix_subs_mix_sumC_def)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	290	apply (simp add: THE_default_def)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	291	apply (case_tac "Ex1 (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya))))")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	292	apply simp_all[2]
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	293	apply auto[1]
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	294	apply (erule_tac x="x" in allE)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	295	apply simp
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	296	apply(thin_tac "\<forall>p. p \<bullet> The (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya)))) =
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	297	(if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	298	then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	299	else Inr (Inr undefined))")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	300	apply(thin_tac "\<forall>p. p \<bullet> (if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	301	then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	302	else Inr (Inr undefined)) =
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	303	(if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	304	then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	305	else Inr (Inr undefined))")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	306	apply (thin_tac "atom b \<sharp> (xa, ya)")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	307	apply (thin_tac "atom ba \<sharp> (xa, ya)")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	308	apply (thin_tac "[[atom b]]lst. P = [[atom ba]]lst. Pa")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	309	apply(cases rule: subsGuard_mix_subsList_mix_subs_mix_graph.cases)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	310	apply assumption
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	311	apply (metis Inr_not_Inl)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	312	apply (metis Inr_not_Inl)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	313	apply (metis Inr_not_Inl)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	314	apply (metis Inr_inject Inr_not_Inl)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	315	apply (metis Inr_inject Inr_not_Inl)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	316	apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.projr
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	317	(Sum_Type.projr
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	318	(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	319	apply clarify
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	320	apply (rule the1_equality)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	321	apply blast apply assumption
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	322	apply (rule_tac x="Sum_Type.projr
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	323	(Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	324	Sum_Type.projr
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	325	(Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	326	apply clarify
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	327	apply (rule the1_equality)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	328	apply blast apply assumption
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	329	apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.projr
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	330	(Sum_Type.projr
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	331	(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	332	apply clarify
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	333	apply (rule the1_equality)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	334	apply blast apply assumption
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	335	apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.projl
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	336	(Sum_Type.projr
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	337	(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	338	apply clarify
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	339	apply (rule the1_equality)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	340	apply blast apply assumption
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	341	apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.projr
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	342	(Sum_Type.projr
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	343	(subsGuard_mix_subsList_mix_subs_mix_sum
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	344	(Inr (Inr (Pb, xb, y)))))" in exI)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	345	apply clarify
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	346	apply (rule the1_equality)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	347	apply blast apply assumption
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	348	apply (rule_tac x="succ\<onesuperior>" in exI)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	349	apply clarify
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	350	apply (rule the1_equality)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	351	apply blast apply assumption
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	352	apply simp
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	353	(* Here the only real goal compatibility is left *)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	354	apply (erule Abs_lst1_fcb)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	355	apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	356	apply (subgoal_tac "atom ba \<sharp> (\<lambda>(a, x, y). subs_mix a x y) (P, xa, ya)")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	357	apply simp
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	358	apply (erule fresh_eqvt_at)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	359	apply(simp add: finite_supp)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	360	apply(simp)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	361	apply(simp add: eqvt_at_def)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	362	apply(drule_tac x="(b \<leftrightarrow> ba)" in spec)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	363	apply(simp)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	364	done
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	365
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	366	nominal_termination (eqvt)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	367	by (lexicographic_order)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	368
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	369	lemma forget_mix:
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	370	fixes g :: guardedTerm_mix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	371	and xg :: sumList_mix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	372	and P :: piMix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	373	and x :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	374	and y :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	375
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	376	shows "atom x \<sharp> g \<longrightarrow> g[x::=\<onesuperior>\<onesuperior>y] = g"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	377	and "atom x \<sharp> xg \<longrightarrow> xg[x::=\<onesuperior>\<twosuperior>y] = xg"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	378	and "atom x \<sharp> P \<longrightarrow> P[x::=\<onesuperior>y] = P"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	379	proof -
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	380	show "atom x \<sharp> g \<longrightarrow> g[x::=\<onesuperior>\<onesuperior>y] = g"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	381	and "atom x \<sharp> xg \<longrightarrow> xg[x::=\<onesuperior>\<twosuperior>y] = xg"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	382	and "atom x \<sharp> P \<longrightarrow> P[x::=\<onesuperior>y] = P"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	383	using assms
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	384	apply(nominal_induct g and xg and P avoiding: x y rule: piMix_strong_induct)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	385	by(auto simp add: piMix_eq_iff piMix_fresh fresh_at_base)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	386	qed
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	387
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	388	lemma fresh_fact_mix:
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	389	fixes g :: guardedTerm_mix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	390	and xg :: sumList_mix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	391	and P :: piMix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	392	and x :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	393	and y :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	394	and z :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	395
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	396	assumes "atom z \<sharp> y"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	397
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	398	shows "(z = x \<or> atom z \<sharp> g) \<longrightarrow> atom z \<sharp> g[x::=\<onesuperior>\<onesuperior>y]"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	399	and "(z = x \<or> atom z \<sharp> xg) \<longrightarrow> atom z \<sharp> xg[x::=\<onesuperior>\<twosuperior>y]"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	400	and "(z = x \<or> atom z \<sharp> P) \<longrightarrow> atom z \<sharp> P[x::=\<onesuperior>y]"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	401	proof -
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	402	show "(z = x \<or> atom z \<sharp> g) \<longrightarrow> atom z \<sharp> g[x::=\<onesuperior>\<onesuperior>y]"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	403	and "(z = x \<or> atom z \<sharp> xg) \<longrightarrow> atom z \<sharp> xg[x::=\<onesuperior>\<twosuperior>y]"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	404	and "(z = x \<or> atom z \<sharp> P) \<longrightarrow> atom z \<sharp> P[x::=\<onesuperior>y]"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	405	using assms
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	406	apply(nominal_induct g and xg and P avoiding: x y z rule: piMix_strong_induct)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	407	by(auto simp add: piMix_fresh fresh_at_base)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	408	qed
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	409
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	410	lemma substitution_lemma_mix:
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	411	fixes g :: guardedTerm_mix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	412	and xg :: sumList_mix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	413	and P :: piMix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	414	and s :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	415	and u :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	416	and x :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	417	and y :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	418
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	419	assumes "x \<noteq> y"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	420	and "atom x \<sharp> u"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	421
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	422	shows "g[x::=\<onesuperior>\<onesuperior>s][y::=\<onesuperior>\<onesuperior>u] = g[y::=\<onesuperior>\<onesuperior>u][x::=\<onesuperior>\<onesuperior>s[y:::=u]]"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	423	and "xg[x::=\<onesuperior>\<twosuperior>s][y::=\<onesuperior>\<twosuperior>u] = xg[y::=\<onesuperior>\<twosuperior>u][x::=\<onesuperior>\<twosuperior>s[y:::=u]]"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	424	and "P[x::=\<onesuperior>s][y::=\<onesuperior>u] = P[y::=\<onesuperior>u][x::=\<onesuperior>s[y:::=u]]"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	425	proof -
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	426	show "g[x::=\<onesuperior>\<onesuperior>s][y::=\<onesuperior>\<onesuperior>u] = g[y::=\<onesuperior>\<onesuperior>u][x::=\<onesuperior>\<onesuperior>s[y:::=u]]"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	427	and "xg[x::=\<onesuperior>\<twosuperior>s][y::=\<onesuperior>\<twosuperior>u] = xg[y::=\<onesuperior>\<twosuperior>u][x::=\<onesuperior>\<twosuperior>s[y:::=u]]"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	428	and "P[x::=\<onesuperior>s][y::=\<onesuperior>u] = P[y::=\<onesuperior>u][x::=\<onesuperior>s[y:::=u]]"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	429	using assms
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	430	apply(nominal_induct g and xg and P avoiding: x y s u rule: piMix_strong_induct)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	431	apply(simp_all add: fresh_fact_mix forget_mix)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	432	by(auto simp add: fresh_at_base)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	433	qed
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	434
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	435	lemma perm_eq_subst_mix:
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	436	fixes g :: guardedTerm_mix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	437	and xg :: sumList_mix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	438	and P :: piMix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	439	and x :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	440	and y :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	441
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	442	shows "atom y \<sharp> g \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> g = g[x::=\<onesuperior>\<onesuperior>y]"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	443	and "atom y \<sharp> xg \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> xg = xg[x::=\<onesuperior>\<twosuperior>y]"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	444	and "atom y \<sharp> P \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> P = P[x::=\<onesuperior>y]"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	445	proof -
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	446	show "atom y \<sharp> g \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> g = g[x::=\<onesuperior>\<onesuperior>y]"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	447	and "atom y \<sharp> xg \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> xg = xg[x::=\<onesuperior>\<twosuperior>y]"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	448	and "atom y \<sharp> P \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> P = P[x::=\<onesuperior>y]"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	449	apply(nominal_induct g and xg and P avoiding: x y rule: piMix_strong_induct)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	450	by(auto simp add: piMix_fresh fresh_at_base)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	451	qed
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	452
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	453	lemma subst_id_mix:
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	454	fixes g :: guardedTerm_mix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	455	and xg :: sumList_mix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	456	and P :: piMix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	457	and x :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	458
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	459	shows "g[x::=\<onesuperior>\<onesuperior>x] = g" and "xg[x::=\<onesuperior>\<twosuperior>x] = xg" and "P[x::=\<onesuperior>x] = P"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	460	proof -
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	461	show "g[x::=\<onesuperior>\<onesuperior>x] = g" and "xg[x::=\<onesuperior>\<twosuperior>x] = xg" and "P[x::=\<onesuperior>x] = P"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	462	apply(nominal_induct g and xg and P avoiding: x rule: piMix_strong_induct)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	463	by(auto)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	464	qed
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	465
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	466	lemma alphaRes_subst_mix:
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	467	fixes a :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	468	and P :: piMix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	469	and z :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	470
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	471	assumes "atom z \<sharp> P"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	472
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	473	shows "<\<nu>a>\<onesuperior>P = <\<nu>z>\<onesuperior>(P[a::=\<onesuperior>z])"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	474	proof(cases "a = z")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	475	assume "a = z"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	476	thus ?thesis
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	477	by(simp add: subst_id_mix)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	478	next
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	479	assume "a \<noteq> z"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	480	thus ?thesis
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	481	using assms
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	482	by(simp add: alphaRes_mix perm_eq_subst_mix)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	483	qed
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	484
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	485	lemma alphaInput_subst_mix:
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	486	fixes a :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	487	and b :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	488	and P :: piMix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	489	and z :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	490
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	491	assumes "atom z \<sharp> P"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	492
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	493	shows "a?<b>\<onesuperior>.P = a?<z>\<onesuperior>.(P[b::=\<onesuperior>z])"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	494	proof(cases "b = z")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	495	assume "b = z"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	496	thus ?thesis
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	497	by(simp add: subst_id_mix)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	498	next
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	499	assume "b \<noteq> z"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	500	thus ?thesis
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	501	using assms
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	502	by(simp add: alphaInput_mix perm_eq_subst_mix)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	503	qed
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	504
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	505	lemma alphaRep_subst_mix:
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	506	fixes a :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	507	and b :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	508	and P :: piMix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	509	and z :: name
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	510
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	511	assumes "atom z \<sharp> P"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	512
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	513	shows "\<infinity>a?<b>\<onesuperior>.P = \<infinity>a?<z>\<onesuperior>.(P[b::=\<onesuperior>z])"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	514	proof(cases "b = z")
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	515	assume "b = z"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	516	thus ?thesis
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	517	by(simp add: subst_id_mix)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	518	next
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	519	assume "b \<noteq> z"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	520	thus ?thesis
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	521	using assms
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	522	by(simp add: alphaRep_mix perm_eq_subst_mix)
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	523	qed
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	524
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	525	inductive
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	526	fresh_list_guard_mix :: "name list \<Rightarrow> guardedTerm_mix \<Rightarrow> bool"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	527	where
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	528	"fresh_list_guard_mix [] g"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	529	\| "\<lbrakk>atom n \<sharp> g; fresh_list_guard_mix xn g\<rbrakk> \<Longrightarrow> fresh_list_guard_mix (n#xn) g"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	530
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	531	equivariance fresh_list_guard_mix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	532	nominal_inductive fresh_list_guard_mix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	533	done
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	534
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	535	inductive
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	536	fresh_list_sumList_mix :: "name list \<Rightarrow> sumList_mix \<Rightarrow> bool"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	537	where
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	538	"fresh_list_sumList_mix [] xg"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	539	\| "\<lbrakk>atom n \<sharp> xg; fresh_list_sumList_mix xn xg\<rbrakk> \<Longrightarrow> fresh_list_sumList_mix (n#xn) xg"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	540
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	541	equivariance fresh_list_sumList_mix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	542	nominal_inductive fresh_list_sumList_mix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	543	done
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	544
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	545	inductive
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	546	fresh_list_mix :: "name list \<Rightarrow> piMix \<Rightarrow> bool"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	547	where
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	548	"fresh_list_mix [] P"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	549	\| "\<lbrakk>atom n \<sharp> P; fresh_list_mix xn P\<rbrakk> \<Longrightarrow> fresh_list_mix (n#xn) P"
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	550
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	551	equivariance fresh_list_mix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	552	nominal_inductive fresh_list_mix
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	553	done
a44479bde681 fixed a problem with two example theories Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3236 diff changeset	554
3235 5ebd327ffb96 changed nominal_primrec into the more appropriate nominal_function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3231 diff changeset	555	end

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Tue, 22 Mar 2016 12:18:30 +0000
changeset 3244	a44479bde681
parent 3236	e2da10806a34
child 3245	017e33849f4d
permissions	-rw-r--r--