nominal2: Nominal/Ex/Lambda.thy@42c0d011a177 (annotated)

1797 fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	1	theory Lambda
2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2442 diff changeset	2	imports "../Nominal2"
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5	atom_decl name
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	7	nominal_datatype lam =
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	8	Var "name"
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	9	\| App "lam" "lam"
2683 42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	10	\| Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100)
2431 331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	11
2683 42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	12	text {* height function *}
2431 331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	13
2666 324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	14	nominal_primrec
2678 494b859bfc16 defined height as a function that returns an integer Christian Urban <urbanc@in.tum.de> parents: 2675 diff changeset	15	height :: "lam \<Rightarrow> int"
2666 324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	16	where
2678 494b859bfc16 defined height as a function that returns an integer Christian Urban <urbanc@in.tum.de> parents: 2675 diff changeset	17	"height (Var x) = 1"
2683 42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	18	\| "height (App t1 t2) = max (height t1) (height t2) + 1"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	19	\| "height (Lam [x].t) = height t + 1"
2666 324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	20	apply(rule_tac y="x" in lam.exhaust)
2683 42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	21	apply(auto simp add: lam.distinct lam.eq_iff)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	22	apply(simp add: Abs_eq_iff alphas)
2666 324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	23	apply(clarify)
2683 42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	24	apply(subst (4) supp_perm_eq[where p="p", symmetric])
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	25	apply(simp add: pure_supp fresh_star_def)
2666 324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	26	apply(simp add: eqvt_at_def)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	27	done
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	28
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	29	termination
2683 42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	30	by (relation "measure size") (simp_all add: lam.size)
2666 324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	31
2683 42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	32
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	33	text {* free name function - returns atom lists *}
2666 324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	34
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	35	nominal_primrec
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	36	frees_lst :: "lam \<Rightarrow> atom list"
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	37	where
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	38	"frees_lst (Var x) = [atom x]"
2683 42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	39	\| "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	40	\| "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)"
2666 324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	41	apply(rule_tac y="x" in lam.exhaust)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	42	apply(simp_all)[3]
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	43	apply(simp_all only: lam.distinct)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	44	apply(simp add: lam.eq_iff)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	45	apply(simp add: lam.eq_iff)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	46	apply(simp add: lam.eq_iff)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	47	apply(simp add: Abs_eq_iff)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	48	apply(erule exE)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	49	apply(simp add: alphas)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	50	apply(simp add: atom_eqvt)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	51	apply(clarify)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	52	apply(rule trans)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	53	apply(rule_tac p="p" in supp_perm_eq[symmetric])
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	54	apply(simp (no_asm) add: supp_removeAll)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	55	apply(drule supp_eqvt_at)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	56	apply(simp add: finite_supp)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	57	apply(auto simp add: fresh_star_def)[1]
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	58	unfolding eqvt_at_def
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	59	apply(simp only: removeAll_eqvt atom_eqvt)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	60	done
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	61
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	62	termination
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	63	apply(relation "measure size")
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	64	apply(simp_all add: lam.size)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	65	done
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	66
2683 42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	67	text {* a small test lemma *}
2666 324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	68	lemma
2683 42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	69	shows "supp t = set (frees_lst t)"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	70	apply(induct t rule: frees_lst.induct)
2666 324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	71	apply(simp_all add: lam.supp supp_at_base)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	72	done
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	73
2683 42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	74	text {* capture - avoiding substitution *}
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	75
2675 68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	76	nominal_primrec
2683 42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	77	subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90)
2675 68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	78	where
2683 42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	79	"(Var x)[y ::= s] = (if x = y then s else (Var x))"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	80	\| "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	81	\| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	82	apply(auto simp add: lam.distinct lam.eq_iff)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	83	apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	84	apply(blast)+
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	85	apply(simp add: fresh_star_def)
2675 68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	86	apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t \<and> atom x \<sharp> [[atom xa]]lst. ta")
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	87	apply(subst (asm) Abs_eq_iff2)
2683 42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	88	apply(simp add: alphas atom_eqvt)
2675 68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	89	apply(clarify)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	90	apply(rule trans)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	91	apply(rule_tac p="p" in supp_perm_eq[symmetric])
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	92	apply(rule fresh_star_supp_conv)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	93	apply(drule fresh_star_perm_set_conv)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	94	apply(simp add: finite_supp)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	95	apply(subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* ([[atom x]]lst. subst_sumC (t, ya, sa))")
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	96	apply(auto simp add: fresh_star_def)[1]
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	97	apply(simp (no_asm) add: fresh_star_def)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	98	apply(rule conjI)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	99	apply(simp (no_asm) add: Abs_fresh_iff)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	100	apply(clarify)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	101	apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	102	apply(simp add: finite_supp)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	103	apply(simp (no_asm_use) add: fresh_Pair)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	104	apply(simp add: Abs_fresh_iff)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	105	apply(simp)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	106	apply(simp add: Abs_fresh_iff)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	107	apply(subgoal_tac "p \<bullet> ya = ya")
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	108	apply(subgoal_tac "p \<bullet> sa = sa")
2683 42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	109	apply(simp add: atom_eqvt eqvt_at_def)
2675 68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	110	apply(rule perm_supp_eq)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	111	apply(auto simp add: fresh_star_def fresh_Pair)[1]
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	112	apply(rule perm_supp_eq)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	113	apply(auto simp add: fresh_star_def fresh_Pair)[1]
2683 42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	114	apply(rule conjI)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	115	apply(simp add: Abs_fresh_iff)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	116	apply(drule sym)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	117	apply(simp add: Abs_fresh_iff)
2675 68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	118	done
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	119
2678 494b859bfc16 defined height as a function that returns an integer Christian Urban <urbanc@in.tum.de> parents: 2675 diff changeset	120	termination
2683 42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	121	by (relation "measure (\<lambda>(t,_,_). size t)")
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	122	(simp_all add: lam.size)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	123
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	124	lemma subst_eqvt[eqvt]:
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	125	shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	126	by (induct t x s rule: subst.induct) (simp_all)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	127
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	128	lemma forget:
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	129	shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	130	apply(nominal_induct t avoiding: x s rule: lam.strong_induct)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	131	apply(auto simp add: lam.fresh fresh_at_base)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	132	done
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	133
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	134	text {* same lemma but with subst.induction *}
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	135	lemma forget2:
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	136	shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	137	apply(induct t x s rule: subst.induct)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	138	apply(auto simp add: lam.fresh fresh_at_base fresh_Pair)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	139	done
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	140
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	141	lemma fresh_fact:
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	142	fixes z::"name"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	143	assumes a: "atom z \<sharp> s"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	144	and b: "z = y \<or> atom z \<sharp> t"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	145	shows "atom z \<sharp> t[y ::= s]"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	146	using a b
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	147	apply (nominal_induct t avoiding: z y s rule: lam.strong_induct)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	148	apply (auto simp add: lam.fresh fresh_at_base)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	149	done
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	150
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	151	lemma substitution_lemma:
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	152	assumes a: "x \<noteq> y" "atom x \<sharp> u"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	153	shows "t[x ::= s][y ::= u] = t[y ::= u][x ::= s[y ::= u]]"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	154	using a
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	155	by (nominal_induct t avoiding: x y s u rule: lam.strong_induct)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	156	(auto simp add: fresh_fact forget)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	157
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	158	lemma subst_rename:
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	159	assumes a: "atom y \<sharp> t"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	160	shows "t[x ::= s] = ((y \<leftrightarrow> x) \<bullet>t)[y ::= s]"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	161	using a
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	162	apply (nominal_induct t avoiding: x y s rule: lam.strong_induct)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	163	apply (auto simp add: lam.fresh fresh_at_base)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	164	done
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	165
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	166
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	167	subsection {* single-step beta-reduction *}
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	168
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	169	inductive
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	170	beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b _" [80,80] 80)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	171	where
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	172	b1[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> App t1 s \<longrightarrow>b App t2 s"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	173	\| b2[intro]: "s1 \<longrightarrow>b s2 \<Longrightarrow> App t s1 \<longrightarrow>b App t s2"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	174	\| b3[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> Lam [x]. t1 \<longrightarrow>b Lam [x]. t2"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	175	\| b4[intro]: "atom x \<sharp> s \<Longrightarrow> App (Lam [x]. t) s \<longrightarrow>b t[x ::= s]"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	176
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	177	equivariance beta
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	178
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	179	nominal_inductive beta
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	180	avoids b4: "x"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	181	by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	182
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	183	text {* One-Reduction *}
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	184
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	185	inductive
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	186	One :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>1 _" [80,80] 80)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	187	where
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	188	o1[intro]: "Var x \<longrightarrow>1 Var x"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	189	\| o2[intro]: "\<lbrakk>t1 \<longrightarrow>1 t2; s1 \<longrightarrow>1 s2\<rbrakk> \<Longrightarrow> App t1 s1 \<longrightarrow>1 App t2 s2"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	190	\| o3[intro]: "t1 \<longrightarrow>1 t2 \<Longrightarrow> Lam [x].t1 \<longrightarrow>1 Lam [x].t2"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	191	\| o4[intro]: "\<lbrakk>atom x \<sharp> (s1, s2); t1 \<longrightarrow>1 t2; s1 \<longrightarrow>1 s2\<rbrakk> \<Longrightarrow> App (Lam [x].t1) s1 \<longrightarrow>1 t2[x ::= s2]"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	192
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	193	equivariance One
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	194
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	195	nominal_inductive One
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	196	avoids o3: "x"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	197	\| o4: "x"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	198	by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	199
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	200	lemma One_refl:
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	201	shows "t \<longrightarrow>1 t"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	202	by (nominal_induct t rule: lam.strong_induct) (auto)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	203
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	204	lemma One_subst:
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	205	assumes a: "t1 \<longrightarrow>1 t2" "s1 \<longrightarrow>1 s2"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	206	shows "t1[x ::= s1] \<longrightarrow>1 t2[x ::= s2]"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	207	using a
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	208	apply(nominal_induct t1 t2 avoiding: s1 s2 x rule: One.strong_induct)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	209	apply(auto simp add: substitution_lemma fresh_at_base fresh_fact fresh_Pair)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	210	done
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	211
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	212	lemma better_o4_intro:
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	213	assumes a: "t1 \<longrightarrow>1 t2" "s1 \<longrightarrow>1 s2"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	214	shows "App (Lam [x]. t1) s1 \<longrightarrow>1 t2[ x ::= s2]"
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	215	proof -
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	216	obtain y::"name" where fs: "atom y \<sharp> (x, t1, s1, t2, s2)" sorry
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	217	have "App (Lam [x]. t1) s1 = App (Lam [y]. ((y \<leftrightarrow> x) \<bullet> t1)) s1" using fs
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	218	by (auto simp add: lam.eq_iff Abs1_eq_iff' flip_def fresh_Pair fresh_at_base)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	219	also have "\<dots> \<longrightarrow>1 ((y \<leftrightarrow> x) \<bullet> t2)[y ::= s2]" using fs a by (auto simp add: One.eqvt)
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	220	also have "\<dots> = t2[x ::= s2]" using fs by (simp add: subst_rename[symmetric])
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	221	finally show "App (Lam [x].t1) s1 \<longrightarrow>1 t2[x ::= s2]" by simp
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	222	qed
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	223
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	224
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	225
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	226
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	227
42c0d011a177 ported some of the old proofs to serve as testcases Christian Urban <urbanc@in.tum.de> parents: 2678 diff changeset	228	section {* Locally Nameless Terms *}
2678 494b859bfc16 defined height as a function that returns an integer Christian Urban <urbanc@in.tum.de> parents: 2675 diff changeset	229
2669 1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	230	nominal_datatype ln =
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	231	LNBnd nat
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	232	\| LNVar name
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	233	\| LNApp ln ln
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	234	\| LNLam ln
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	235
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	236	fun
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	237	lookup :: "name list \<Rightarrow> nat \<Rightarrow> name \<Rightarrow> ln"
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	238	where
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	239	"lookup [] n x = LNVar x"
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	240	\| "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))"
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	241
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	242	lemma [eqvt]:
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	243	shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	244	apply(induct xs arbitrary: n)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	245	apply(simp_all add: permute_pure)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	246	done
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	247
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	248	nominal_primrec
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	249	trans :: "lam \<Rightarrow> name list \<Rightarrow> ln"
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	250	where
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	251	"trans (Var x) xs = lookup xs 0 x"
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	252	\| "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)"
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	253	\| "atom x \<sharp> xs \<Longrightarrow> trans (Lam x t) xs = LNLam (trans t (x # xs))"
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	254	apply(case_tac x)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	255	apply(simp)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	256	apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	257	apply(simp_all)[3]
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	258	apply(blast)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	259	apply(blast)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	260	apply(simp add: fresh_star_def)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	261	apply(simp_all add: lam.distinct)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	262	apply(simp add: lam.eq_iff)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	263	apply(simp add: lam.eq_iff)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	264	apply(simp add: lam.eq_iff)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	265	apply(erule conjE)
2675 68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	266	apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t \<and> atom x \<sharp> [[atom xa]]lst. ta")
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	267	prefer 2
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	268	apply(rule conjI)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	269	apply(simp add: Abs_fresh_iff)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	270	apply(drule sym)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	271	apply(simp add: Abs_fresh_iff)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	272	apply(subst (asm) Abs_eq_iff2)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	273	apply(auto)
2669 1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	274	apply(simp add: alphas)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	275	apply(simp add: atom_eqvt)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	276	apply(clarify)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	277	apply(rule trans)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	278	apply(rule_tac p="p" in supp_perm_eq[symmetric])
2675 68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	279	apply(rule fresh_star_supp_conv)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	280	apply(drule fresh_star_perm_set_conv)
2669 1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	281	apply(simp add: finite_supp)
2675 68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	282	apply(subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* LNLam (trans_sumC (t, x # xsa))")
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	283	apply(auto simp add: fresh_star_def)[1]
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	284	apply(simp (no_asm) add: fresh_star_def ln.fresh)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	285	apply(rule conjI)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	286	apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	287	apply(simp add: finite_supp)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	288	apply(simp (no_asm_use) add: fresh_Pair)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	289	apply(simp add: Abs_fresh_iff fresh_Cons)[1]
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	290	apply(erule disjE)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	291	apply(erule disjE)
68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	292	apply(simp)
2669 1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	293	oops
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions Christian Urban <urbanc@in.tum.de> parents: 2667 diff changeset	294
2667 e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	295	nominal_datatype db =
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	296	DBVar nat
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	297	\| DBApp db db
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	298	\| DBLam db
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	299
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	300	abbreviation
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	301	mbind :: "'a option => ('a => 'b option) => 'b option" ("_ \<guillemotright>= _" [65,65] 65)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	302	where
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	303	"c \<guillemotright>= f \<equiv> case c of None => None \| (Some v) => f v"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	304
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	305	lemma mbind_eqvt:
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	306	fixes c::"'a::pt option"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	307	shows "(p \<bullet> (c \<guillemotright>= f)) = ((p \<bullet> c) \<guillemotright>= (p \<bullet> f))"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	308	apply(cases c)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	309	apply(simp_all)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	310	apply(perm_simp)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	311	apply(rule refl)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	312	done
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	313
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	314	lemma mbind_eqvt_raw[eqvt_raw]:
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	315	shows "(p \<bullet> option_case) \<equiv> option_case"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	316	apply(rule eq_reflection)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	317	apply(rule ext)+
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	318	apply(case_tac xb)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	319	apply(simp_all)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	320	apply(rule_tac p="-p" in permute_boolE)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	321	apply(perm_simp add: permute_minus_cancel)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	322	apply(simp)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	323	apply(rule_tac p="-p" in permute_boolE)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	324	apply(perm_simp add: permute_minus_cancel)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	325	apply(simp)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	326	done
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	327
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	328	fun
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	329	index :: "atom list \<Rightarrow> nat \<Rightarrow> atom \<Rightarrow> nat option"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	330	where
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	331	"index [] n x = None"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	332	\| "index (y # ys) n x = (if x = y then (Some n) else (index ys (n + 1) x))"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	333
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	334	lemma [eqvt]:
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	335	shows "(p \<bullet> index xs n x) = index (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	336	apply(induct xs arbitrary: n)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	337	apply(simp_all add: permute_pure)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	338	done
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	339
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	340	ML {*
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	341	Nominal_Function_Core.trace := true
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	342	*}
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	343
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	344	(*
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	345	inductive
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	346	trans_graph
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	347	where
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	348	"trans_graph (Var x, xs) (index xs 0 (atom x) \<guillemotright>= (\<lambda>v. Some (DBVar v)))"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	349	\| "\<lbrakk>trans_graph (t1, xs) (trans_sum (t1, xs));
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	350	\<And>a. trans_sum (t1, xs) = Some a \<Longrightarrow> trans_graph (t2, xs) (trans_sum (t2, xs))\<rbrakk>
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	351	\<Longrightarrow> trans_graph (App t1 t2, xs)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	352	(trans_sum (t1, xs) \<guillemotright>= (\<lambda>v. trans_sum (t2, xs) \<guillemotright>= (\<lambda>va. Some (DBApp v va))))"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	353	\| "trans_graph (t, atom x # xs) (trans_sum (t, atom x # xs)) \<Longrightarrow>
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	354	trans_graph (Lam x t, xs) (trans_sum (t, atom x # xs) \<guillemotright>= (\<lambda>v. Some (DBLam v)))"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	355
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	356	lemma
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	357	assumes a: "trans_graph x t"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	358	shows "trans_graph (p \<bullet> x) (p \<bullet> t)"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	359	using a
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	360	apply(induct)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	361	apply(perm_simp)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	362	apply(rule trans_graph.intros)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	363	apply(perm_simp)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	364	apply(rule trans_graph.intros)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	365	apply(simp)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	366	apply(simp)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	367	defer
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	368	apply(perm_simp)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	369	apply(rule trans_graph.intros)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	370	apply(simp)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	371	apply(rotate_tac 3)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	372	apply(drule_tac x="FOO" in meta_spec)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	373	apply(drule meta_mp)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	374	prefer 2
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	375	apply(simp)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	376
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	377	equivariance trans_graph
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	378	*)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	379
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	380	(* equivariance fails at the moment
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	381	nominal_primrec
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	382	trans :: "lam \<Rightarrow> atom list \<Rightarrow> db option"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	383	where
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	384	"trans (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	385	\| "trans (App t1 t2) xs = (trans t1 xs \<guillemotright>= (\<lambda>db1. trans t2 xs \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	386	\| "trans (Lam x t) xs = (trans t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	387	*)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) Christian Urban <urbanc@in.tum.de> parents: 2666 diff changeset	388
2675 68ccf847507d defined properly substitution Christian Urban <urbanc@in.tum.de> parents: 2669 diff changeset	389
2666 324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	390
2654 0f0335d91456 solved subgoals for depth and subst function Christian Urban <urbanc@in.tum.de> parents: 2649 diff changeset	391
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	392	end
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	393
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	394
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	395

author	Christian Urban <urbanc@in.tum.de>
	Wed, 19 Jan 2011 18:56:28 +0100
changeset 2683	42c0d011a177
parent 2678	494b859bfc16
child 2685	1df873b63cb2
permissions	-rw-r--r--