nominal2: Nominal/Ex/Lambda.thy@324a5d1289a3 (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"
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	10	\| Lam x::"name" l::"lam" bind x in l
2431 331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	11
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	12	thm lam.distinct
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	13	thm lam.induct
2617 e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2559 diff changeset	14	thm lam.exhaust lam.strong_exhaust
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	15	thm lam.fv_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	16	thm lam.bn_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	17	thm lam.perm_simps
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	18	thm lam.eq_iff
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	19	thm lam.fv_bn_eqvt
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	20	thm lam.size_eqvt
2431 331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	21
2666 324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	22	nominal_primrec
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	23	depth :: "lam \<Rightarrow> nat"
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	24	where
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	25	"depth (Var x) = 1"
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	26	\| "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1"
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	27	\| "depth (Lam x t) = (depth t) + 1"
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	28	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	29	apply(simp_all)[3]
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	30	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	31	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	32	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	33	apply(subst (asm) Abs_eq_iff)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	34	apply(erule exE)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	35	apply(simp add: alphas)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	36	apply(clarify)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	37	apply(rule trans)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	38	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	39	apply(simp add: pure_supp)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	40	apply(simp add: fresh_star_def)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	41	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	42	done
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	43
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	44	termination
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	45	apply(relation "measure size")
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	46	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	47	done
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	48
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	49	lemma removeAll_eqvt[eqvt]:
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	50	shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	51	by (induct xs) (auto)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	52
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	53	lemma supp_removeAll:
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	54	fixes x::"atom"
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	55	shows "supp (removeAll x xs) = (supp xs - {x})"
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	56	apply(induct xs)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	57	apply(simp_all add: supp_Nil supp_Cons)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	58	apply(rule conjI)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	59	apply(rule impI)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	60	apply(simp add: supp_atom)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	61	apply(rule impI)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	62	apply(simp add: supp_atom)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	63	apply(blast)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	64	done
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	65
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	66	nominal_primrec
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	67	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	68	where
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	69	"frees_lst (Var x) = [atom x]"
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	70	\| "frees_lst (App t1 t2) = (frees_lst t1) @ (frees_lst t2)"
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	71	\| "frees_lst (Lam x t) = removeAll (atom x) (frees_lst t)"
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	72	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	73	apply(simp_all)[3]
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	74	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	75	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	76	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	77	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	78	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	79	apply(erule exE)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	80	apply(simp add: alphas)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	81	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	82	apply(clarify)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	83	apply(rule trans)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	84	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	85	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	86	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	87	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	88	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	89	unfolding eqvt_at_def
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	90	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	91	done
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	92
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	93	termination
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	94	apply(relation "measure size")
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	95	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	96	done
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	97
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	98	(* a small lemma *)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	99	lemma
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	100	"supp t = set (frees_lst t)"
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	101	apply(induct t rule: lam.induct)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	102	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	103	done
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	104
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	105	nominal_primrec
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	106	subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [100,100,100] 100)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	107	where
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	108	"(Var x)[y ::= s] = (if x=y then s else (Var x))"
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	109	\| "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])"
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	110	\| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])"
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	111	apply(case_tac x)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	112	apply(simp)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	113	apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	114	apply(simp add: lam.eq_iff lam.distinct)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	115	apply(auto)[1]
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	116	apply(simp add: lam.eq_iff lam.distinct)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	117	apply(auto)[1]
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	118	apply(simp add: fresh_star_def lam.eq_iff lam.distinct)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	119	apply(simp_all add: lam.distinct)[5]
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	120	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	121	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	122	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	123	apply(erule conjE)+
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	124	oops
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	125
2654 0f0335d91456 solved subgoals for depth and subst function Christian Urban <urbanc@in.tum.de> parents: 2649 diff changeset	126
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	127	end
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	128
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	129
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	130

author	Christian Urban <urbanc@in.tum.de>
	Mon, 17 Jan 2011 15:12:03 +0100
changeset 2666	324a5d1289a3
parent 2664	a9a1ed3f5023
child 2667	e3f8673085b1
permissions	-rw-r--r--