isabelle: src/HOL/Nominal/Examples/Class.thy@87217764cec2 (annotated)

18395 87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	1	theory class = nominal:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	2
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	3	atom_decl name coname
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	4
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	5	section {* Term-Calculus from my PHD *}
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	6
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	7	nominal_datatype trm = Ax "name" "coname"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	8	\| ImpR "\<guillemotleft>name\<guillemotright>(\<guillemotleft>coname\<guillemotright>trm)" "coname"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	9	\| ImpL "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	10	\| Cut "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	11
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	12	consts
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	13	Ax :: "name \<Rightarrow> coname \<Rightarrow> trm"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	14	ImpR :: "name \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> coname \<Rightarrow> trm"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	15	("ImpR [_].[_]._ _" [100,100,100,100] 100)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	16	ImpL :: "coname \<Rightarrow> trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> name \<Rightarrow> trm"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	17	("ImpL [_]._ [_]._ _" [100,100,100,100,100] 100)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	18	Cut :: "coname \<Rightarrow> trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	19	("Cut [_]._ [_]._" [100,100,100,100] 100)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	20
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	21	defs
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	22	Ax_trm_def: "Ax x a
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	23	\<equiv> Abs_trm (trm_Rep.Ax x a)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	24	ImpR_trm_def: "ImpR [x].[a].t b
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	25	\<equiv> Abs_trm (trm_Rep.ImpR ([x].([a].(Rep_trm t))) b)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	26	ImpL_trm_def: "ImpL [a].t1 [x].t2 y
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	27	\<equiv> Abs_trm (trm_Rep.ImpL ([a].(Rep_trm t1)) ([x].(Rep_trm t2)) y)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	28	Cut_trm_def: "Cut [a].t1 [x].t2
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	29	\<equiv> Abs_trm (trm_Rep.Cut ([a].(Rep_trm t1)) ([x].(Rep_trm t2)))"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	30
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	31	lemma Ax_inject:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	32	shows "(Ax x a = Ax y b) = (x=y\<and>a=b)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	33	apply(subgoal_tac "trm_Rep.Ax x a \<in> trm_Rep_set")(A)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	34	apply(subgoal_tac "trm_Rep.Ax y b \<in> trm_Rep_set")(B)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	35	apply(simp add: Ax_trm_def Abs_trm_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	36	(A B)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	37	apply(rule trm_Rep_set.intros)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	38	apply(rule trm_Rep_set.intros)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	39	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	40
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	41	lemma permF_perm_name:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	42	fixes t :: "trm"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	43	and pi :: "name prm"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	44	shows "pi\<bullet>(Rep_trm t) = Rep_trm (pi\<bullet>t)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	45	apply(simp add: prm_trm_def)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	46	apply(subgoal_tac "pi\<bullet>(Rep_trm t)\<in>trm_Rep_set")(A)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	47	apply(simp add: Abs_trm_inverse)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	48	(A)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	49	apply(rule perm_closed)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	50	apply(rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	51	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	52
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	53	lemma permF_perm_coname:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	54	fixes t :: "trm"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	55	and pi :: "coname prm"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	56	shows "pi\<bullet>(Rep_trm t) = Rep_trm (pi\<bullet>t)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	57	apply(simp add: prm_trm_def)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	58	apply(subgoal_tac "pi\<bullet>(Rep_trm t)\<in>trm_Rep_set")(A)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	59	apply(simp add: Abs_trm_inverse)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	60	(A)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	61	apply(rule perm_closed)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	62	apply(rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	63	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	64
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	65	lemma freshF_fresh_name:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	66	fixes t :: "trm"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	67	and b :: "name"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	68	shows "b\<sharp>(Rep_trm t) = b\<sharp>t"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	69	apply(simp add: fresh_def supp_def)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	70	apply(simp add: permF_perm_name)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	71	apply(simp add: Rep_trm_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	72	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	73
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	74	lemma freshF_fresh_coname:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	75	fixes t :: "trm"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	76	and b :: "coname"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	77	shows "b\<sharp>(Rep_trm t) = b\<sharp>t"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	78	apply(simp add: fresh_def supp_def)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	79	apply(simp add: permF_perm_coname)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	80	apply(simp add: Rep_trm_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	81	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	82
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	83	lemma ImpR_inject:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	84	shows "((ImpR [x].[a].t1 b) = (ImpR [y].[c].t2 d)) = (([x].([a].t1) = [y].([c].t2)) \<and> b=d)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	85	apply(simp add: ImpR_trm_def)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	86	apply(subgoal_tac "trm_Rep.ImpR ([x].([a].(Rep_trm t1))) b \<in> trm_Rep_set")(A)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	87	apply(subgoal_tac "trm_Rep.ImpR ([y].([c].(Rep_trm t2))) d \<in> trm_Rep_set")(B)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	88	apply(simp add: Abs_trm_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	89	apply(simp add: alpha abs_perm perm_dj abs_fresh
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	90	permF_perm_name freshF_fresh_name
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	91	permF_perm_coname freshF_fresh_coname
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	92	Rep_trm_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	93	(* A B *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	94	apply(rule trm_Rep_set.intros, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	95	apply(rule trm_Rep_set.intros, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	96	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	97
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	98	lemma ImpL_inject:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	99	shows "((ImpL [a1].t1 [x1].s1 y1) = (ImpL [a2].t2 [x2].s2 y2)) =
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	100	([a1].t1 = [a2].t2 \<and> [x1].s1 = [x2].s2 \<and> y1=y2)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	101	apply(simp add: ImpL_trm_def)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	102	apply(subgoal_tac "(trm_Rep.ImpL ([a1].(Rep_trm t1)) ([x1].(Rep_trm s1)) y1) \<in> trm_Rep_set")(A)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	103	apply(subgoal_tac "(trm_Rep.ImpL ([a2].(Rep_trm t2)) ([x2].(Rep_trm s2)) y2) \<in> trm_Rep_set")(B)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	104	apply(simp add: Abs_trm_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	105	apply(simp add: alpha abs_perm perm_dj abs_fresh
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	106	permF_perm_name freshF_fresh_name
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	107	permF_perm_coname freshF_fresh_coname
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	108	Rep_trm_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	109	(* A B *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	110	apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	111	apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	112	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	113
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	114	lemma Cut_inject:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	115	shows "((Cut [a1].t1 [x1].s1) = (Cut [a2].t2 [x2].s2)) = ([a1].t1 = [a2].t2 \<and> [x1].s1 = [x2].s2)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	116	apply(simp add: Cut_trm_def)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	117	apply(subgoal_tac "trm_Rep.Cut ([a1].(Rep_trm t1)) ([x1].(Rep_trm s1)) \<in> trm_Rep_set")(A)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	118	apply(subgoal_tac "trm_Rep.Cut ([a2].(Rep_trm t2)) ([x2].(Rep_trm s2)) \<in> trm_Rep_set")(B)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	119	apply(simp add: Abs_trm_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	120	apply(simp add: alpha abs_perm perm_dj abs_fresh
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	121	permF_perm_name freshF_fresh_name
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	122	permF_perm_coname freshF_fresh_coname
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	123	Rep_trm_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	124	(* A B *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	125	apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	126	apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	127	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	128
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	129
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	130	lemma Ax_ineqs:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	131	shows "Ax x a \<noteq> ImpR [y].[b].t1 c"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	132	and "Ax x a \<noteq> ImpL [b].t1 [y].t2 z"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	133	and "Ax x a \<noteq> Cut [b].t1 [y].t2"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	134	apply(auto)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	135	(1)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	136	apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(A)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	137	apply(subgoal_tac "trm_Rep.ImpR ([y].([b].(Rep_trm t1))) c\<in>trm_Rep_set")(B)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	138	apply(simp add: Ax_trm_def ImpR_trm_def Abs_trm_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	139	(A B)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	140	apply(rule trm_Rep_set.intros, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	141	apply(rule trm_Rep_set.intros)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	142	(2)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	143	apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(C)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	144	apply(subgoal_tac "trm_Rep.ImpL ([b].(Rep_trm t1)) ([y].(Rep_trm t2)) z\<in>trm_Rep_set")(D)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	145	apply(simp add: Ax_trm_def ImpL_trm_def Abs_trm_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	146	(* C D *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	147	apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	148	apply(rule trm_Rep_set.intros)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	149	(3)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	150	apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(E)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	151	apply(subgoal_tac "trm_Rep.Cut ([b].(Rep_trm t1)) ([y].(Rep_trm t2))\<in>trm_Rep_set")(F)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	152	apply(simp add: Ax_trm_def Cut_trm_def Abs_trm_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	153	(* E F *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	154	apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	155	apply(rule trm_Rep_set.intros)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	156	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	157
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	158	lemma ImpR_ineqs:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	159	shows "ImpR [y].[b].t c \<noteq> Ax x a"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	160	and "ImpR [y].[b].t c \<noteq> ImpL [a].t1 [x].t2 z"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	161	and "ImpR [y].[b].t c \<noteq> Cut [a].t1 [x].t2"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	162	apply(auto)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	163	(1)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	164	apply(subgoal_tac "trm_Rep.ImpR ([y].([b].(Rep_trm t))) c\<in>trm_Rep_set")(B)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	165	apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(A)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	166	apply(simp add: Ax_trm_def ImpR_trm_def Abs_trm_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	167	(A B)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	168	apply(rule trm_Rep_set.intros)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	169	apply(rule trm_Rep_set.intros, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	170	(2)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	171	apply(subgoal_tac "trm_Rep.ImpR ([y].([b].(Rep_trm t))) c\<in>trm_Rep_set")(C)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	172	apply(subgoal_tac "trm_Rep.ImpL ([a].(Rep_trm t1)) ([x].(Rep_trm t2)) z\<in>trm_Rep_set")(D)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	173	apply(simp add: ImpR_trm_def ImpL_trm_def Abs_trm_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	174	(* C D *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	175	apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	176	apply(rule trm_Rep_set.intros, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	177	(3)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	178	apply(subgoal_tac "trm_Rep.ImpR ([y].([b].(Rep_trm t))) c\<in>trm_Rep_set")(E)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	179	apply(subgoal_tac "trm_Rep.Cut ([a].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(F)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	180	apply(simp add: ImpR_trm_def Cut_trm_def Abs_trm_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	181	(* E F *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	182	apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	183	apply(rule trm_Rep_set.intros, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	184	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	185
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	186	lemma ImpL_ineqs:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	187	shows "ImpL [b].t1 [x].t2 y \<noteq> Ax z a"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	188	and "ImpL [b].t1 [x].t2 y \<noteq> ImpR [z].[a].s1 c"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	189	and "ImpL [b].t1 [x].t2 y \<noteq> Cut [a].s1 [z].s2"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	190	apply(auto)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	191	(1)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	192	apply(subgoal_tac "trm_Rep.ImpL ([b].(Rep_trm t1)) ([x].(Rep_trm t2)) y\<in>trm_Rep_set")(B)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	193	apply(subgoal_tac "trm_Rep.Ax z a\<in>trm_Rep_set")(A)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	194	apply(simp add: Ax_trm_def ImpL_trm_def Abs_trm_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	195	(A B)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	196	apply(rule trm_Rep_set.intros)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	197	apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	198	(2)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	199	apply(subgoal_tac "trm_Rep.ImpL ([b].(Rep_trm t1)) ([x].(Rep_trm t2)) y\<in>trm_Rep_set")(D)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	200	apply(subgoal_tac "trm_Rep.ImpR ([z].([a].(Rep_trm s1))) c\<in>trm_Rep_set")(C)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	201	apply(simp add: ImpR_trm_def ImpL_trm_def Abs_trm_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	202	(* C D *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	203	apply(rule trm_Rep_set.intros, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	204	apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	205	(3)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	206	apply(subgoal_tac "trm_Rep.ImpL ([b].(Rep_trm t1)) ([x].(Rep_trm t2)) y\<in>trm_Rep_set")(E)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	207	apply(subgoal_tac "trm_Rep.Cut ([a].(Rep_trm s1)) ([z].(Rep_trm s2))\<in>trm_Rep_set")(F)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	208	apply(simp add: ImpL_trm_def Cut_trm_def Abs_trm_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	209	(* E F *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	210	apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	211	apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	212	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	213
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	214	lemma Cut_ineqs:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	215	shows "Cut [b].t1 [x].t2 \<noteq> Ax z a"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	216	and "Cut [b].t1 [x].t2 \<noteq> ImpR [z].[a].s1 c"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	217	and "Cut [b].t1 [x].t2 \<noteq> ImpL [a].s1 [z].s2 y"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	218	apply(auto)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	219	(1)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	220	apply(subgoal_tac "trm_Rep.Cut ([b].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(B)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	221	apply(subgoal_tac "trm_Rep.Ax z a\<in>trm_Rep_set")(A)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	222	apply(simp add: Ax_trm_def Cut_trm_def Abs_trm_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	223	(A B)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	224	apply(rule trm_Rep_set.intros)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	225	apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	226	(2)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	227	apply(subgoal_tac "trm_Rep.Cut ([b].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(D)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	228	apply(subgoal_tac "trm_Rep.ImpR ([z].([a].(Rep_trm s1))) c\<in>trm_Rep_set")(C)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	229	apply(simp add: ImpR_trm_def Cut_trm_def Abs_trm_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	230	(* C D *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	231	apply(rule trm_Rep_set.intros, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	232	apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	233	(3)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	234	apply(subgoal_tac "trm_Rep.Cut ([b].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(E)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	235	apply(subgoal_tac "trm_Rep.ImpL ([a].(Rep_trm s1)) ([z].(Rep_trm s2)) y\<in>trm_Rep_set")(F)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	236	apply(simp add: ImpL_trm_def Cut_trm_def Abs_trm_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	237	(* E F *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	238	apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	239	apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	240	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	241
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	242	lemma pi_Ax[simp]:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	243	fixes pi1 :: "name prm"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	244	and pi2 :: "coname prm"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	245	shows "pi1\<bullet>(Ax x a) = Ax (pi1\<bullet>x) a"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	246	and "pi2\<bullet>(Ax x a) = Ax x (pi2\<bullet>a)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	247	apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(A)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	248	apply(simp add: prm_trm_def Ax_trm_def Abs_trm_inverse perm_dj)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	249	(A)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	250	apply(rule trm_Rep_set.intros)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	251	apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(B)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	252	apply(simp add: prm_trm_def Ax_trm_def Abs_trm_inverse perm_dj)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	253	(B)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	254	apply(rule trm_Rep_set.intros)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	255	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	256
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	257	lemma pi_ImpR[simp]:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	258	fixes pi1 :: "name prm"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	259	and pi2 :: "coname prm"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	260	shows "pi1\<bullet>(ImpR [x].[a].t b) = ImpR [(pi1\<bullet>x)].[a].(pi1\<bullet>t) b"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	261	and "pi2\<bullet>(ImpR [x].[a].t b) = ImpR [x].[(pi2\<bullet>a)].(pi2\<bullet>t) (pi2\<bullet>b)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	262	apply(subgoal_tac "trm_Rep.ImpR ([x].([a].(Rep_trm t))) b\<in>trm_Rep_set")(A)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	263	apply(subgoal_tac "pi1\<bullet>(Rep_trm t)\<in>trm_Rep_set")(B)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	264	apply(simp add: prm_trm_def ImpR_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	265	apply(simp add: perm_dj)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	266	(* A B *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	267	apply(rule perm_closed, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	268	apply(rule trm_Rep_set.intros, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	269	apply(subgoal_tac "trm_Rep.ImpR ([x].([a].(Rep_trm t))) b\<in>trm_Rep_set")(C)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	270	apply(subgoal_tac "pi2\<bullet>(Rep_trm t)\<in>trm_Rep_set")(D)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	271	apply(simp add: prm_trm_def ImpR_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	272	apply(simp add: perm_dj)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	273	(* C D *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	274	apply(rule perm_closed, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	275	apply(rule trm_Rep_set.intros, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	276	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	277
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	278	lemma pi_ImpL[simp]:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	279	fixes pi1 :: "name prm"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	280	and pi2 :: "coname prm"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	281	shows "pi1\<bullet>(ImpL [a].t1 [x].t2 y) = ImpL [a].(pi1\<bullet>t1) [(pi1\<bullet>x)].(pi1\<bullet>t2) (pi1\<bullet>y)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	282	and "pi2\<bullet>(ImpL [a].t1 [x].t2 y) = ImpL [(pi2\<bullet>a)].(pi2\<bullet>t1) [x].(pi2\<bullet>t2) y"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	283	apply(subgoal_tac "trm_Rep.ImpL ([a].(Rep_trm t1)) ([x].(Rep_trm t2)) y\<in>trm_Rep_set")(A)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	284	apply(subgoal_tac "pi1\<bullet>(Rep_trm t1)\<in>trm_Rep_set")(B)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	285	apply(subgoal_tac "pi1\<bullet>(Rep_trm t2)\<in>trm_Rep_set")(C)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	286	apply(simp add: prm_trm_def ImpL_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	287	apply(simp add: perm_dj)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	288	(* A B C *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	289	apply(rule perm_closed, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	290	apply(rule perm_closed, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	291	apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	292	apply(subgoal_tac "trm_Rep.ImpL ([a].(Rep_trm t1)) ([x].(Rep_trm t2)) y\<in>trm_Rep_set")(E)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	293	apply(subgoal_tac "pi2\<bullet>(Rep_trm t1)\<in>trm_Rep_set")(D)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	294	apply(subgoal_tac "pi2\<bullet>(Rep_trm t2)\<in>trm_Rep_set")(F)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	295	apply(simp add: prm_trm_def ImpL_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	296	apply(simp add: perm_dj)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	297	(* C D *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	298	apply(rule perm_closed, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	299	apply(rule perm_closed, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	300	apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	301	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	302
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	303	lemma pi_Cut[simp]:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	304	fixes pi1 :: "name prm"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	305	and pi2 :: "coname prm"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	306	shows "pi1\<bullet>(Cut [a].t1 [x].t2) = Cut [a].(pi1\<bullet>t1) [(pi1\<bullet>x)].(pi1\<bullet>t2)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	307	and "pi2\<bullet>(Cut [a].t1 [x].t2) = Cut [(pi2\<bullet>a)].(pi2\<bullet>t1) [x].(pi2\<bullet>t2)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	308	apply(subgoal_tac "trm_Rep.Cut ([a].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(A)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	309	apply(subgoal_tac "pi1\<bullet>(Rep_trm t1)\<in>trm_Rep_set")(B)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	310	apply(subgoal_tac "pi1\<bullet>(Rep_trm t2)\<in>trm_Rep_set")(C)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	311	apply(simp add: prm_trm_def Cut_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	312	apply(simp add: perm_dj)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	313	(* A B C *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	314	apply(rule perm_closed, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	315	apply(rule perm_closed, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	316	apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	317	apply(subgoal_tac "trm_Rep.Cut ([a].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(E)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	318	apply(subgoal_tac "pi2\<bullet>(Rep_trm t1)\<in>trm_Rep_set")(D)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	319	apply(subgoal_tac "pi2\<bullet>(Rep_trm t2)\<in>trm_Rep_set")(F)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	320	apply(simp add: prm_trm_def Cut_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	321	apply(simp add: perm_dj)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	322	(* C D *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	323	apply(rule perm_closed, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	324	apply(rule perm_closed, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	325	apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	326	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	327
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	328	lemma supp_Ax:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	329	shows "((supp (Ax x a))::name set) = (supp x)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	330	and "((supp (Ax x a))::coname set) = (supp a)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	331	apply(simp add: supp_def Ax_inject)+
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	332	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	333
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	334	lemma supp_ImpR:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	335	shows "((supp (ImpR [x].[a].t b))::name set) = (supp ([x].t))"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	336	and "((supp (ImpR [x].[a].t b))::coname set) = (supp ([a].t,b))"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	337	apply(simp add: supp_def ImpR_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	338	apply(simp add: abs_perm alpha perm_dj abs_fresh)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	339	apply(simp add: supp_def ImpR_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	340	apply(simp add: abs_perm alpha perm_dj abs_fresh)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	341	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	342
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	343	lemma supp_ImpL:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	344	shows "((supp (ImpL [a].t1 [x].t2 y))::name set) = (supp (t1,[x].t2,y))"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	345	and "((supp (ImpL [a].t1 [x].t2 y))::coname set) = (supp ([a].t1,t2))"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	346	apply(simp add: supp_def ImpL_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	347	apply(simp add: abs_perm alpha perm_dj abs_fresh)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	348	apply(simp add: supp_def ImpL_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	349	apply(simp add: abs_perm alpha perm_dj abs_fresh)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	350	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	351
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	352	lemma supp_Cut:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	353	shows "((supp (Cut [a].t1 [x].t2))::name set) = (supp (t1,[x].t2))"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	354	and "((supp (Cut [a].t1 [x].t2))::coname set) = (supp ([a].t1,t2))"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	355	apply(simp add: supp_def Cut_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	356	apply(simp add: abs_perm alpha perm_dj abs_fresh)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	357	apply(simp add: supp_def Cut_inject)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	358	apply(simp add: abs_perm alpha perm_dj abs_fresh)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	359	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	360
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	361	lemma fresh_Ax[simp]:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	362	fixes x :: "name"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	363	and a :: "coname"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	364	shows "x\<sharp>(Ax y b) = x\<sharp>y"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	365	and "a\<sharp>(Ax y b) = a\<sharp>b"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	366	by (simp_all add: fresh_def supp_Ax)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	367
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	368	lemma fresh_ImpR[simp]:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	369	fixes x :: "name"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	370	and a :: "coname"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	371	shows "x\<sharp>(ImpR [y].[b].t c) = x\<sharp>([y].t)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	372	and "a\<sharp>(ImpR [y].[b].t c) = a\<sharp>([b].t,c)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	373	by (simp_all add: fresh_def supp_ImpR)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	374
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	375	lemma fresh_ImpL[simp]:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	376	fixes x :: "name"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	377	and a :: "coname"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	378	shows "x\<sharp>(ImpL [b].t1 [y].t2 z) = x\<sharp>(t1,[y].t2,z)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	379	and "a\<sharp>(ImpL [b].t1 [y].t2 z) = a\<sharp>([b].t1,t2)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	380	by (simp_all add: fresh_def supp_ImpL)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	381
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	382	lemma fresh_Cut[simp]:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	383	fixes x :: "name"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	384	and a :: "coname"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	385	shows "x\<sharp>(Cut [b].t1 [y].t2) = x\<sharp>(t1,[y].t2)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	386	and "a\<sharp>(Cut [b].t1 [y].t2) = a\<sharp>([b].t1,t2)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	387	by (simp_all add: fresh_def supp_Cut)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	388
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	389	lemma trm_inverses:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	390	shows "Abs_trm (trm_Rep.Ax x a) = (Ax x a)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	391	and "\<lbrakk>t1\<in>trm_Rep_set;t2\<in>trm_Rep_set\<rbrakk>
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	392	\<Longrightarrow> Abs_trm (trm_Rep.ImpL ([a].t1) ([x].t2) y) = ImpL [a].(Abs_trm t1) [x].(Abs_trm t2) y"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	393	and "\<lbrakk>t1\<in>trm_Rep_set;t2\<in>trm_Rep_set\<rbrakk>
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	394	\<Longrightarrow> Abs_trm (trm_Rep.Cut ([a].t1) ([x].t2)) = Cut [a].(Abs_trm t1) [x].(Abs_trm t2)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	395	and "\<lbrakk>t1\<in>trm_Rep_set\<rbrakk>
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	396	\<Longrightarrow> Abs_trm (trm_Rep.ImpR ([y].([a].t1)) b) = (ImpR [y].[a].(Abs_trm t1) b)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	397	(1)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	398	apply(simp add: Ax_trm_def)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	399	(2)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	400	apply(simp add: ImpL_trm_def Abs_trm_inverse)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	401	(3)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	402	apply(simp add: Cut_trm_def Abs_trm_inverse)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	403	(4)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	404	apply(simp add: ImpR_trm_def Abs_trm_inverse)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	405	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	406
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	407	lemma trm_Rep_set_fsupp_name:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	408	fixes t :: "trm_Rep"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	409	shows "t\<in>trm_Rep_set \<Longrightarrow> finite ((supp (Abs_trm t))::name set)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	410	apply(erule trm_Rep_set.induct)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	411	(* Ax_Rep *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	412	apply(simp add: trm_inverses supp_Ax at_supp[OF at_name_inst])
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	413	(* ImpR_Rep *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	414	apply(simp add: trm_inverses supp_ImpR abs_fun_supp[OF pt_name_inst, OF at_name_inst])
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	415	(* ImpL_Rep *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	416	apply(simp add: trm_inverses supp_prod supp_ImpL abs_fun_supp[OF pt_name_inst, OF at_name_inst]
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	417	at_supp[OF at_name_inst])
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	418	(* Cut_Rep *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	419	apply(simp add: trm_inverses supp_prod supp_Cut abs_fun_supp[OF pt_name_inst, OF at_name_inst])
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	420	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	421
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	422	instance trm :: fs_name
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	423	apply(intro_classes)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	424	apply(rule Abs_trm_induct)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	425	apply(simp add: trm_Rep_set_fsupp_name)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	426	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	427
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	428	lemma trm_Rep_set_fsupp_coname:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	429	fixes t :: "trm_Rep"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	430	shows "t\<in>trm_Rep_set \<Longrightarrow> finite ((supp (Abs_trm t))::coname set)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	431	apply(erule trm_Rep_set.induct)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	432	(* Ax_Rep *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	433	apply(simp add: trm_inverses supp_Ax at_supp[OF at_coname_inst])
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	434	(* ImpR_Rep *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	435	apply(simp add: trm_inverses supp_prod supp_ImpR abs_fun_supp[OF pt_coname_inst, OF at_coname_inst]
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	436	at_supp[OF at_coname_inst])
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	437	(* ImpL_Rep *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	438	apply(simp add: trm_inverses supp_prod supp_ImpL abs_fun_supp[OF pt_coname_inst, OF at_coname_inst]
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	439	at_supp[OF at_coname_inst])
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	440	(* Cut_Rep *)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	441	apply(simp add: trm_inverses supp_prod supp_Cut abs_fun_supp[OF pt_coname_inst, OF at_coname_inst])
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	442	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	443
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	444	instance trm :: fs_coname
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	445	apply(intro_classes)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	446	apply(rule Abs_trm_induct)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	447	apply(simp add: trm_Rep_set_fsupp_coname)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	448	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	449
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	450
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	451	section {* strong induction principle for lam *}
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	452
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	453	lemma trm_induct_weak:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	454	fixes P :: "trm \<Rightarrow> bool"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	455	assumes h1: "\<And>x a. P (Ax x a)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	456	and h2: "\<And>x a t b. P t \<Longrightarrow> P (ImpR [x].[a].t b)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	457	and h3: "\<And>a t1 x t2 y. P t1 \<Longrightarrow> P t2 \<Longrightarrow> P (ImpL [a].t1 [x].t2 y)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	458	and h4: "\<And>a t1 x t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> P (Cut [a].t1 [x].t2)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	459	shows "P t"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	460	apply(rule Abs_trm_induct)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	461	apply(erule trm_Rep_set.induct)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	462	apply(fold Ax_trm_def)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	463	apply(rule h1)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	464	apply(drule h2)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	465	apply(unfold ImpR_trm_def)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	466	apply(simp add: Abs_trm_inverse)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	467	apply(drule h3)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	468	apply(simp)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	469	apply(unfold ImpL_trm_def)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	470	apply(simp add: Abs_trm_inverse)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	471	apply(drule h4)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	472	apply(simp)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	473	apply(unfold Cut_trm_def)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	474	apply(simp add: Abs_trm_inverse)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	475	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	476
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	477	lemma trm_induct_aux:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	478	fixes P :: "trm \<Rightarrow> 'a \<Rightarrow> bool"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	479	and f1 :: "'a \<Rightarrow> name set"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	480	and f2 :: "'a \<Rightarrow> coname set"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	481	assumes fs1: "\<And>x. finite (f1 x)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	482	and fs2: "\<And>x. finite (f2 x)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	483	and h1: "\<And>k x a. P (Ax x a) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	484	and h2: "\<And>k x a t b. x\<notin>f1 k \<Longrightarrow> a\<notin>f2 k \<Longrightarrow> (\<forall>l. P t l) \<Longrightarrow> P (ImpR [x].[a].t b) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	485	and h3: "\<And>k a t1 x t2 y. a\<notin>f2 k \<Longrightarrow> x\<notin>f1 k \<Longrightarrow> (\<forall>l. P t1 l) \<Longrightarrow> (\<forall>l. P t2 l)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	486	\<Longrightarrow> P (ImpL [a].t1 [x].t2 y) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	487	and h4: "\<And>k a t1 x t2. a\<notin>f2 k \<Longrightarrow> x\<notin>f1 k \<Longrightarrow> (\<forall>l. P t1 l) \<Longrightarrow> (\<forall>l. P t2 l)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	488	\<Longrightarrow> P (Cut [a].t1 [x].t2) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	489	shows "\<forall>(pi1::name prm) (pi2::coname prm) k. P (pi1\<bullet>(pi2\<bullet>t)) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	490	proof (induct rule: trm_induct_weak)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	491	case (goal1 a)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	492	show ?case using h1 by simp
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	493	next
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	494	case (goal2 x a t b)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	495	assume i1: "\<forall>(pi1::name prm)(pi2::coname prm) k. P (pi1\<bullet>(pi2\<bullet>t)) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	496	show ?case
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	497	proof (intro strip, simp add: abs_perm perm_dj)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	498	fix pi1::"name prm" and pi2::"coname prm" and k::"'a"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	499	have "\<exists>u::name. u\<sharp>(f1 k,pi1\<bullet>x,pi1\<bullet>(pi2\<bullet>t))"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	500	by (rule at_exists_fresh[OF at_name_inst], simp add: supp_prod fs_name1
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	501	at_fin_set_supp[OF at_name_inst, OF fs1] fs1)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	502	then obtain u::"name"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	503	where f1: "u\<noteq>(pi1\<bullet>x)" and f2: "u\<sharp>(f1 k)" and f3: "u\<sharp>(pi1\<bullet>(pi2\<bullet>t))"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	504	by (auto simp add: fresh_prod at_fresh[OF at_name_inst])
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	505	have "\<exists>c::coname. c\<sharp>(f2 k,pi2\<bullet>a,pi1\<bullet>(pi2\<bullet>t))"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	506	by (rule at_exists_fresh[OF at_coname_inst], simp add: supp_prod fs_coname1
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	507	at_fin_set_supp[OF at_coname_inst, OF fs2] fs2)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	508	then obtain c::"coname"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	509	where e1: "c\<noteq>(pi2\<bullet>a)" and e2: "c\<sharp>(f2 k)" and e3: "c\<sharp>(pi1\<bullet>(pi2\<bullet>t))"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	510	by (auto simp add: fresh_prod at_fresh[OF at_coname_inst])
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	511	have g: "ImpR [u].[c].([(u,pi1\<bullet>x)]\<bullet>(pi1\<bullet>([(c,pi2\<bullet>a)]\<bullet>(pi2\<bullet>t)))) (pi2\<bullet>b)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	512	=ImpR [(pi1\<bullet>x)].[(pi2\<bullet>a)].(pi1\<bullet>(pi2\<bullet>t)) (pi2\<bullet>b)" using f1 f3 e1 e3
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	513	apply (auto simp add: ImpR_inject alpha abs_fresh abs_perm perm_dj,
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	514	simp add: dj_cp[OF cp_name_coname_inst, OF dj_coname_name])
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	515	apply(simp add: pt_fresh_left_ineq[OF pt_name_inst, OF pt_name_inst,
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	516	OF at_name_inst, OF cp_name_coname_inst] perm_dj)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	517	done
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	518	from i1 have "\<forall>k. P (([(u,pi1\<bullet>x)]@pi1)\<bullet>(([(c,pi2\<bullet>a)]@pi2)\<bullet>t)) k" by force
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	519	hence i1b: "\<forall>k. P ([(u,pi1\<bullet>x)]\<bullet>(pi1\<bullet>([(c,pi2\<bullet>a)]\<bullet>(pi2\<bullet>t)))) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	520	by (simp add: pt_name2[symmetric] pt_coname2[symmetric])
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	521	with h2 f2 e2 have "P (ImpR [u].[c].([(u,pi1\<bullet>x)]\<bullet>(pi1\<bullet>([(c,pi2\<bullet>a)]\<bullet>(pi2\<bullet>t)))) (pi2\<bullet>b)) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	522	by (simp add: fresh_def at_fin_set_supp[OF at_name_inst, OF fs1]
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	523	at_fin_set_supp[OF at_coname_inst, OF fs2])
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	524	with g show "P (ImpR [(pi1\<bullet>x)].[(pi2\<bullet>a)].(pi1\<bullet>(pi2\<bullet>t)) (pi2\<bullet>b)) k" by simp
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	525	qed
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	526	next
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	527	case (goal3 a t1 x t2 y)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	528	assume i1: "\<forall>(pi1::name prm)(pi2::coname prm) k. P (pi1\<bullet>(pi2\<bullet>t1)) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	529	and i2: "\<forall>(pi1::name prm)(pi2::coname prm) k. P (pi1\<bullet>(pi2\<bullet>t2)) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	530	show ?case
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	531	proof (intro strip, simp add: abs_perm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	532	fix pi1::"name prm" and pi2::"coname prm" and k::"'a"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	533	have "\<exists>u::name. u\<sharp>(f1 k,pi1\<bullet>x,pi1\<bullet>(pi2\<bullet>t2))"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	534	by (rule at_exists_fresh[OF at_name_inst], simp add: supp_prod fs_name1
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	535	at_fin_set_supp[OF at_name_inst, OF fs1] fs1)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	536	then obtain u::"name"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	537	where f1: "u\<noteq>(pi1\<bullet>x)" and f2: "u\<sharp>(f1 k)" and f3: "u\<sharp>(pi1\<bullet>(pi2\<bullet>t2))"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	538	by (auto simp add: fresh_prod at_fresh[OF at_name_inst])
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	539	have "\<exists>c::coname. c\<sharp>(f2 k,pi2\<bullet>a,pi1\<bullet>(pi2\<bullet>t1))"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	540	by (rule at_exists_fresh[OF at_coname_inst], simp add: supp_prod fs_coname1
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	541	at_fin_set_supp[OF at_coname_inst, OF fs2] fs2)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	542	then obtain c::"coname"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	543	where e1: "c\<noteq>(pi2\<bullet>a)" and e2: "c\<sharp>(f2 k)" and e3: "c\<sharp>(pi1\<bullet>(pi2\<bullet>t1))"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	544	by (auto simp add: fresh_prod at_fresh[OF at_coname_inst])
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	545	have g: "ImpL [c].([(c,pi2\<bullet>a)]\<bullet>(pi1\<bullet>(pi2\<bullet>t1))) [u].([(u,pi1\<bullet>x)]\<bullet>(pi1\<bullet>(pi2\<bullet>t2))) (pi1\<bullet>y)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	546	=ImpL [(pi2\<bullet>a)].(pi1\<bullet>(pi2\<bullet>t1)) [(pi1\<bullet>x)].(pi1\<bullet>(pi2\<bullet>t2)) (pi1\<bullet>y)" using f1 f3 e1 e3
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	547	by (simp add: ImpL_inject alpha abs_fresh abs_perm perm_dj)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	548	from i2 have "\<forall>k. P (([(u,pi1\<bullet>x)]@pi1)\<bullet>(pi2\<bullet>t2)) k" by force
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	549	hence i2b: "\<forall>k. P ([(u,pi1\<bullet>x)]\<bullet>(pi1\<bullet>(pi2\<bullet>t2))) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	550	by (simp add: pt_name2[symmetric])
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	551	from i1 have "\<forall>k. P (pi1\<bullet>(([(c,pi2\<bullet>a)]@pi2)\<bullet>t1)) k" by force
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	552	hence i1b: "\<forall>k. P ([(c,pi2\<bullet>a)]\<bullet>(pi1\<bullet>(pi2\<bullet>t1))) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	553	by (simp add: pt_coname2[symmetric] dj_cp[OF cp_name_coname_inst, OF dj_coname_name])
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	554	from h3 f2 e2 i1b i2b
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	555	have "P (ImpL [c].([(c,pi2\<bullet>a)]\<bullet>(pi1\<bullet>(pi2\<bullet>t1))) [u].([(u,pi1\<bullet>x)]\<bullet>(pi1\<bullet>(pi2\<bullet>t2))) (pi1\<bullet>y)) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	556	by (simp add: fresh_def at_fin_set_supp[OF at_name_inst, OF fs1]
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	557	at_fin_set_supp[OF at_coname_inst, OF fs2])
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	558	with g show "P (ImpL [(pi2\<bullet>a)].(pi1\<bullet>(pi2\<bullet>t1)) [(pi1\<bullet>x)].(pi1\<bullet>(pi2\<bullet>t2)) (pi1\<bullet>y)) k" by simp
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	559	qed
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	560	next
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	561	case (goal4 a t1 x t2)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	562	assume i1: "\<forall>(pi1::name prm)(pi2::coname prm) k. P (pi1\<bullet>(pi2\<bullet>t1)) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	563	and i2: "\<forall>(pi1::name prm)(pi2::coname prm) k. P (pi1\<bullet>(pi2\<bullet>t2)) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	564	show ?case
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	565	proof (intro strip, simp add: abs_perm)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	566	fix pi1::"name prm" and pi2::"coname prm" and k::"'a"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	567	have "\<exists>u::name. u\<sharp>(f1 k,pi1\<bullet>x,pi1\<bullet>(pi2\<bullet>t2))"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	568	by (rule at_exists_fresh[OF at_name_inst], simp add: supp_prod fs_name1
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	569	at_fin_set_supp[OF at_name_inst, OF fs1] fs1)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	570	then obtain u::"name"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	571	where f1: "u\<noteq>(pi1\<bullet>x)" and f2: "u\<sharp>(f1 k)" and f3: "u\<sharp>(pi1\<bullet>(pi2\<bullet>t2))"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	572	by (auto simp add: fresh_prod at_fresh[OF at_name_inst])
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	573	have "\<exists>c::coname. c\<sharp>(f2 k,pi2\<bullet>a,pi1\<bullet>(pi2\<bullet>t1))"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	574	by (rule at_exists_fresh[OF at_coname_inst], simp add: supp_prod fs_coname1
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	575	at_fin_set_supp[OF at_coname_inst, OF fs2] fs2)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	576	then obtain c::"coname"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	577	where e1: "c\<noteq>(pi2\<bullet>a)" and e2: "c\<sharp>(f2 k)" and e3: "c\<sharp>(pi1\<bullet>(pi2\<bullet>t1))"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	578	by (auto simp add: fresh_prod at_fresh[OF at_coname_inst])
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	579	have g: "Cut [c].([(c,pi2\<bullet>a)]\<bullet>(pi1\<bullet>(pi2\<bullet>t1))) [u].([(u,pi1\<bullet>x)]\<bullet>(pi1\<bullet>(pi2\<bullet>t2)))
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	580	=Cut [(pi2\<bullet>a)].(pi1\<bullet>(pi2\<bullet>t1)) [(pi1\<bullet>x)].(pi1\<bullet>(pi2\<bullet>t2))" using f1 f3 e1 e3
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	581	by (simp add: Cut_inject alpha abs_fresh abs_perm perm_dj)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	582	from i2 have "\<forall>k. P (([(u,pi1\<bullet>x)]@pi1)\<bullet>(pi2\<bullet>t2)) k" by force
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	583	hence i2b: "\<forall>k. P ([(u,pi1\<bullet>x)]\<bullet>(pi1\<bullet>(pi2\<bullet>t2))) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	584	by (simp add: pt_name2[symmetric])
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	585	from i1 have "\<forall>k. P (pi1\<bullet>(([(c,pi2\<bullet>a)]@pi2)\<bullet>t1)) k" by force
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	586	hence i1b: "\<forall>k. P ([(c,pi2\<bullet>a)]\<bullet>(pi1\<bullet>(pi2\<bullet>t1))) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	587	by (simp add: pt_coname2[symmetric] dj_cp[OF cp_name_coname_inst, OF dj_coname_name])
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	588	from h3 f2 e2 i1b i2b
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	589	have "P (Cut [c].([(c,pi2\<bullet>a)]\<bullet>(pi1\<bullet>(pi2\<bullet>t1))) [u].([(u,pi1\<bullet>x)]\<bullet>(pi1\<bullet>(pi2\<bullet>t2)))) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	590	by (simp add: fresh_def at_fin_set_supp[OF at_name_inst, OF fs1]
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	591	at_fin_set_supp[OF at_coname_inst, OF fs2])
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	592	with g show "P (Cut [(pi2\<bullet>a)].(pi1\<bullet>(pi2\<bullet>t1)) [(pi1\<bullet>x)].(pi1\<bullet>(pi2\<bullet>t2))) k" by simp
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	593	qed
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	594	qed
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	595
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	596	lemma trm_induct'[case_names Ax ImpR ImpL Cut]:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	597	fixes P :: "trm \<Rightarrow> 'a \<Rightarrow> bool"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	598	and f1 :: "'a \<Rightarrow> name set"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	599	and f2 :: "'a \<Rightarrow> coname set"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	600	assumes fs1: "\<And>x. finite (f1 x)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	601	and fs2: "\<And>x. finite (f2 x)"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	602	and h1: "\<And>k x a. P (Ax x a) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	603	and h2: "\<And>k x a t b. x\<notin>f1 k \<Longrightarrow> a\<notin>f2 k \<Longrightarrow> (\<forall>l. P t l) \<Longrightarrow> P (ImpR [x].[a].t b) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	604	and h3: "\<And>k a t1 x t2 y. a\<notin>f2 k \<Longrightarrow> x\<notin>f1 k \<Longrightarrow> (\<forall>l. P t1 l) \<Longrightarrow> (\<forall>l. P t2 l)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	605	\<Longrightarrow> P (ImpL [a].t1 [x].t2 y) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	606	and h4: "\<And>k a t1 x t2. a\<notin>f2 k \<Longrightarrow> x\<notin>f1 k \<Longrightarrow> (\<forall>l. P t1 l) \<Longrightarrow> (\<forall>l. P t2 l)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	607	\<Longrightarrow> P (Cut [a].t1 [x].t2) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	608	shows "P t k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	609	proof -
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	610	have "\<forall>(pi1::name prm)(pi2::coname prm) k. P (pi1\<bullet>(pi2\<bullet>t)) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	611	using fs1 fs2 h1 h2 h3 h4 by (rule trm_induct_aux, auto)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	612	hence "P (([]::name prm)\<bullet>(([]::coname prm)\<bullet>t)) k" by blast
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	613	thus "P t k" by simp
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	614	qed
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	615
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	616	lemma trm_induct[case_names Ax ImpR ImpL Cut]:
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	617	fixes P :: "trm \<Rightarrow> ('a::{fs_name,fs_coname}) \<Rightarrow> bool"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	618	assumes h1: "\<And>k x a. P (Ax x a) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	619	and h2: "\<And>k x a t b. x\<sharp>k \<Longrightarrow> a\<sharp>k \<Longrightarrow> (\<forall>l. P t l) \<Longrightarrow> P (ImpR [x].[a].t b) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	620	and h3: "\<And>k a t1 x t2 y. a\<sharp>k \<Longrightarrow> x\<sharp>k \<Longrightarrow> (\<forall>l. P t1 l) \<Longrightarrow> (\<forall>l. P t2 l)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	621	\<Longrightarrow> P (ImpL [a].t1 [x].t2 y) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	622	and h4: "\<And>k a t1 x t2. a\<sharp>k \<Longrightarrow> x\<sharp>k \<Longrightarrow> (\<forall>l. P t1 l) \<Longrightarrow> (\<forall>l. P t2 l)
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	623	\<Longrightarrow> P (Cut [a].t1 [x].t2) k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	624	shows "P t k"
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	625	by (rule trm_induct'[of "\<lambda>x. ((supp x)::name set)" "\<lambda>x. ((supp x)::coname set)" "P"],
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	626	simp_all add: fs_name1 fs_coname1 fresh_def[symmetric], auto intro: h1 h2 h3 h4)

author	urbanc
	Tue, 13 Dec 2005 16:30:50 +0100
changeset 18395	87217764cec2
child 18425	bcf13dbaa339
permissions	-rw-r--r--