nominal2: Nominal/Ex/Lambda.thy@e3f8673085b1 (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
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	105	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	106	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	107	\| 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	108	\| 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	109
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	110	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	111	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	112	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	113	"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	114
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	115
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	116	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	117	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	118	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	119	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	120	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	121	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	122	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	123	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	124
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	125	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	126	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	127	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	128	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	129	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	130	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	131	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	132	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	133	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	134	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	135	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	136	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	137	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	138
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	139	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	140	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	141	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	142	"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	143	\| "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	144
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	145	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	146	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	147	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	148	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	149	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	150
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	151	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	152	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	153	*}
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	154
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	155	(*
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	156	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	157	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	158	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	159	"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	160	\| "\<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	161	\<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	162	\<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	163	(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	164	\| "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	165	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	166
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	167	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	168	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	169	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	170	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	171	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	172	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	173	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	174	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	175	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	176	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	177	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	178	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	179	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	180	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	181	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	182	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	183	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	184	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	185	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	186	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	187
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	188	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	189	*)
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	190
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	191	(* 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	192	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	193	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	194	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	195	"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	196	\| "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	197	\| "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	198	*)
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	199
2666 324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	200	nominal_primrec
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	201	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	202	where
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	203	"(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	204	\| "(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	205	\| "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	206	apply(case_tac x)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	207	apply(simp)
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	208	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	209	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	210	apply(auto)[1]
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	211	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	212	apply(auto)[1]
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	213	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	214	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	215	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	216	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	217	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	218	apply(erule conjE)+
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	219	oops
324a5d1289a3 added a few examples of functions to Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2664 diff changeset	220
2654 0f0335d91456 solved subgoals for depth and subst function Christian Urban <urbanc@in.tum.de> parents: 2649 diff changeset	221
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	222	end
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	223
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	224
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	225

author	Christian Urban <urbanc@in.tum.de>
	Mon, 17 Jan 2011 17:20:21 +0100
changeset 2667	e3f8673085b1
parent 2666	324a5d1289a3
child 2669	1d1772a89026
permissions	-rw-r--r--