nominal2: Nominal/Ex/Lambda_add.thy@13af2c8d7329 (annotated)

2726 bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	1	theory Lambda_add
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	2	imports "Lambda"
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5	nominal_primrec
2752 9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right Christian Urban <urbanc@in.tum.de> parents: 2739 diff changeset	6	addlam :: "lam \<Rightarrow> lam"
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right Christian Urban <urbanc@in.tum.de> parents: 2739 diff changeset	7	where
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right Christian Urban <urbanc@in.tum.de> parents: 2739 diff changeset	8	"fv \<noteq> x \<Longrightarrow> addlam (Var x) = Lam [fv]. App (Var fv) (Var x)"
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right Christian Urban <urbanc@in.tum.de> parents: 2739 diff changeset	9	\| "addlam (App t1 t2) = App t1 t2"
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right Christian Urban <urbanc@in.tum.de> parents: 2739 diff changeset	10	\| "addlam (Lam [x]. t) = Lam [x].t"
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right Christian Urban <urbanc@in.tum.de> parents: 2739 diff changeset	11	oops
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right Christian Urban <urbanc@in.tum.de> parents: 2739 diff changeset	12
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right Christian Urban <urbanc@in.tum.de> parents: 2739 diff changeset	13
9f44608ea28d changed default preprocessor that does not catch variables only occuring on the right Christian Urban <urbanc@in.tum.de> parents: 2739 diff changeset	14	nominal_primrec
2726 bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	15	addlam_pre :: "lam \<Rightarrow> lam \<Rightarrow> lam"
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	16	where
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	17	"fv \<noteq> x \<Longrightarrow> addlam_pre (Var x) (Lam [fv].it) = Lam [fv]. App (Var fv) (Var x)"
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	18	\| "addlam_pre (Var x) (App t1 t2) = Var x"
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	19	\| "addlam_pre (Var x) (Var v) = Var x"
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	20	\| "addlam_pre (App t1 t2) it = App t1 t2"
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	21	\| "addlam_pre (Lam [x]. t) it = Lam [x].t"
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	22	apply (subgoal_tac "\<And>p a x. addlam_pre_graph a x \<Longrightarrow> addlam_pre_graph (p \<bullet> a) (p \<bullet> x)")
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	23	apply (simp add: eqvt_def)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	24	apply (intro allI)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	25	apply(simp add: permute_fun_def)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	26	apply(rule ext)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	27	apply(rule ext)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	28	apply(simp add: permute_bool_def)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	29	apply rule
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	30	apply(drule_tac x="p" in meta_spec)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	31	apply(drule_tac x="- p \<bullet> x" in meta_spec)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	32	apply(drule_tac x="- p \<bullet> xa" in meta_spec)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	33	apply simp
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	34	apply(drule_tac x="-p" in meta_spec)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	35	apply(drule_tac x="x" in meta_spec)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	36	apply(drule_tac x="xa" in meta_spec)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	37	apply simp
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	38	apply (erule addlam_pre_graph.induct)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	39	apply (simp_all add: addlam_pre_graph.intros)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	40	apply (simp_all add:lam.distinct)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	41	apply clarify
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	42	apply simp
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	43	apply (rule_tac y="a" in lam.exhaust)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	44	apply(auto simp add: lam.distinct lam.eq_iff)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	45	prefer 2 apply blast
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	46	prefer 2 apply blast
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	47	apply (rule_tac y="b" and c="name" in lam.strong_exhaust)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	48	apply(auto simp add: lam.distinct lam.eq_iff)[3]
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	49	apply blast
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	50	apply(drule_tac x="namea" in meta_spec)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	51	apply(drule_tac x="name" in meta_spec)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	52	apply(drule_tac x="lam" in meta_spec)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	53	apply (auto simp add: fresh_star_def atom_name_def fresh_at_base)[1]
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	54	apply (auto simp add: lam.eq_iff Abs1_eq_iff fresh_def lam.supp supp_at_base)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	55	done
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	56
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	57	termination
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	58	by (relation "measure (\<lambda>(t,_). size t)")
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	59	(simp_all add: lam.size)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	60
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	61	function
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	62	addlam :: "lam \<Rightarrow> lam"
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	63	where
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	64	"addlam (Var x) = addlam_pre (Var x) (Lam [x]. (Var x))"
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	65	\| "addlam (App t1 t2) = App t1 t2"
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	66	\| "addlam (Lam [x]. t) = Lam [x].t"
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	67	apply (simp_all add:lam.distinct)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	68	apply (rule_tac y="x" in lam.exhaust)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	69	apply auto
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	70	apply (simp add:lam.eq_iff)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	71	done
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	72
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	73	termination
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	74	by (relation "measure (\<lambda>(t). size t)")
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	75	(simp_all add: lam.size)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	76
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	77	lemma addlam':
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	78	"fv \<noteq> x \<Longrightarrow> addlam (Var x) = Lam [fv]. App (Var fv) (Var x)"
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	79	apply simp
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	80	apply (subgoal_tac "Lam [x]. Var x = Lam [fv]. Var fv")
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	81	apply simp
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	82	apply (simp add: lam.eq_iff Abs1_eq_iff lam.supp fresh_def supp_at_base)
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	83	done
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	84
2737 ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	85	nominal_primrec
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	86	Pair_pre
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	87	where
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	88	"atom z \<sharp> (M, N) \<Longrightarrow> (Pair_pre M N) (Lam [z]. _) = (Lam [z]. App (App (Var z) M) N)"
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	89	\| "(Pair_pre M N) (App l r) = (App l r)"
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	90	\| "(Pair_pre M N) (Var v) = (Var v)"
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	91	apply (subgoal_tac "\<And>p a x. Pair_pre_graph a x \<Longrightarrow> Pair_pre_graph (p \<bullet> a) (p \<bullet> x)")
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	92	apply (simp add: eqvt_def)
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	93	apply (intro allI)
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	94	apply(simp add: permute_fun_def)
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	95	apply(rule ext)
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	96	apply(rule ext)
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	97	apply(simp add: permute_bool_def)
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	98	apply rule
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	99	apply(drule_tac x="p" in meta_spec)
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	100	apply(drule_tac x="- p \<bullet> x" in meta_spec)
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	101	apply(drule_tac x="- p \<bullet> xa" in meta_spec)
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	102	apply simp
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	103	apply(drule_tac x="-p" in meta_spec)
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	104	apply(drule_tac x="x" in meta_spec)
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	105	apply(drule_tac x="xa" in meta_spec)
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	106	apply simp
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	107	apply (erule Pair_pre_graph.induct)
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	108	apply (simp_all add: Pair_pre_graph.intros)[3]
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	109	apply (case_tac x)
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	110	apply clarify
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	111	apply (simp add: symmetric[OF atomize_conjL])
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	112	apply (rule_tac y="c" and c="(ab, ba)" in lam.strong_exhaust)
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	113	apply (simp_all add: lam.distinct symmetric[OF atomize_conjL] lam.eq_iff Abs1_eq_iff fresh_star_def)
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	114	apply auto[1]
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	115	apply (simp_all add: fresh_Pair lam.fresh fresh_at_base)
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	116	apply (rule swap_fresh_fresh[symmetric])
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	117	prefer 3
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	118	apply (rule swap_fresh_fresh[symmetric])
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	119	apply simp_all
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	120	done
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	121
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	122	termination
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	123	by (relation "measure (\<lambda>(t,_). size t)")
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	124	(simp_all add: lam.size)
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	125
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	126	consts cx :: name
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	127
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	128	fun
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	129	Pair where
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	130	"(Pair M N) = (Pair_pre M N (Lam [cx]. Var cx))"
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	131
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	132	lemma Pair : "atom z \<sharp> (M, N) \<Longrightarrow> Pair M N = (Lam [z]. App (App (Var z) M) N)"
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	133	apply simp
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	134	apply (subgoal_tac "Lam [cx]. Var cx = Lam[z]. Var z")
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	135	apply simp
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	136	apply (auto simp add: lam.eq_iff Abs1_eq_iff)
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	137	by (metis Rep_name_inject atom_name_def fresh_at_base lam.fresh(1))
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	138
ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	139
2739 b5ffcb30b6d0 distinct names at toplevel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2737 diff changeset	140	definition Lam_I_pre : "\<II> \<equiv> Lam[cx]. Var cx"
b5ffcb30b6d0 distinct names at toplevel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2737 diff changeset	141
b5ffcb30b6d0 distinct names at toplevel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2737 diff changeset	142	lemma Lam_I : "\<II> = Lam[x]. Var x"
b5ffcb30b6d0 distinct names at toplevel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2737 diff changeset	143	by (simp add: Lam_I_pre lam.eq_iff Abs1_eq_iff lam.fresh supp_at_base)
b5ffcb30b6d0 distinct names at toplevel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2737 diff changeset	144	(metis Rep_name_inverse atom_name_def fresh_at_base)
b5ffcb30b6d0 distinct names at toplevel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2737 diff changeset	145
b5ffcb30b6d0 distinct names at toplevel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2737 diff changeset	146	definition c1 :: name where "c1 \<equiv> Abs_name (Atom (Sort ''Lambda.name'' []) 1)"
b5ffcb30b6d0 distinct names at toplevel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2737 diff changeset	147	definition c2 :: name where "c2 \<equiv> Abs_name (Atom (Sort ''Lambda.name'' []) 2)"
b5ffcb30b6d0 distinct names at toplevel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2737 diff changeset	148
b5ffcb30b6d0 distinct names at toplevel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2737 diff changeset	149	lemma c1_c2[simp]:
b5ffcb30b6d0 distinct names at toplevel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2737 diff changeset	150	"c1 \<noteq> c2"
b5ffcb30b6d0 distinct names at toplevel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2737 diff changeset	151	unfolding c1_def c2_def
b5ffcb30b6d0 distinct names at toplevel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2737 diff changeset	152	by (simp add: Abs_name_inject)
b5ffcb30b6d0 distinct names at toplevel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2737 diff changeset	153
b5ffcb30b6d0 distinct names at toplevel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2737 diff changeset	154	definition Lam_F_pre : "\<FF> \<equiv> Lam[c1]. Lam[c2]. Var c2"
b5ffcb30b6d0 distinct names at toplevel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2737 diff changeset	155	lemma Lam_F : "\<FF> = Lam[x]. Lam[y]. Var y"
b5ffcb30b6d0 distinct names at toplevel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2737 diff changeset	156	by (simp add: Lam_F_pre lam.eq_iff Abs1_eq_iff lam.fresh supp_at_base)
b5ffcb30b6d0 distinct names at toplevel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2737 diff changeset	157	(metis Rep_name_inverse atom_name_def fresh_at_base)
2737 ff22039df778 Pairing function Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2726 diff changeset	158
2726 bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	159	end
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	160
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	161
bc2c1ab01422 Finished the proof of a function that invents fresh variable names. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	162

author	Christian Urban <urbanc@in.tum.de>
	Thu, 02 Jun 2011 12:09:31 +0100 (2011-06-02)
changeset 2807	13af2c8d7329
parent 2752	9f44608ea28d
child 2896	59be22e05a0a
permissions	-rw-r--r--