nominal2: Nominal/Ex/NBE.thy@80f01215d1a6 (annotated)

2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory Lambda
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	imports
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	"../Nominal2"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	4	begin
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	5
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	6
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	atom_decl name
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	8
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	9	nominal_datatype lam =
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	Var "name"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	\| App "lam" "lam"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	12	\| Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	13
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	14
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	15	nominal_datatype sem =
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	L "env" x::"name" l::"lam" binds x in l
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	17	\| N "neu"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	18	and neu =
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	19	V "name"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	20	\| A "neu" "sem"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	and env =
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	22	ENil
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	\| ECons "env" "name" "sem"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	24
2953 80f01215d1a6 Setup eqvt_at for first goal Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2952 diff changeset	25	nominal_primrec
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	26	evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	27	evals_aux :: "sem \<Rightarrow> lam \<Rightarrow> env \<Rightarrow> sem"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	where
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	29	"evals ENil (Var x) = N (V x)"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	30	\| "evals (ECons tail y v) (Var x) = (if x = y then v else evals tail (Var x))"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	31	\| "evals env (Lam [x]. t) = L env x t"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	32	\| "evals env (App t1 t2) = evals_aux (evals env t1) t2 env"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	33	\| "evals_aux (L cenv x t) t2 env = evals (ECons cenv x (evals env t2)) t"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	34	\| "evals_aux (N n) t2 env = N (A n (evals env t2))"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	35	defer
2953 80f01215d1a6 Setup eqvt_at for first goal Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2952 diff changeset	36	apply (rule TrueI)
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	37	--"completeness"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	38	apply(case_tac x)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	39	apply(simp)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	40	apply(case_tac a)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	41	apply(simp)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	42	apply(case_tac aa rule: sem_neu_env.exhaust(3))
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	43	apply(simp)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	44	apply(case_tac b rule: lam.exhaust)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	45	apply(metis)+
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	46	apply(case_tac b rule: lam.exhaust)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	47	apply(metis)+
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	48	apply(simp)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	49	apply(case_tac b)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	50	apply(simp)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	51	apply(case_tac a rule: sem_neu_env.exhaust(1))
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	52	apply(metis)+
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	53	--"compatibility"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	54	apply(all_trivials)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	55	apply(simp)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	56	apply(simp)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	57	apply(simp)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	58	apply(simp)
2953 80f01215d1a6 Setup eqvt_at for first goal Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2952 diff changeset	59	apply (simp add: meta_eq_to_obj_eq[OF evals_def, symmetric, unfolded fun_eq_iff])
80f01215d1a6 Setup eqvt_at for first goal Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2952 diff changeset	60	apply (subgoal_tac "eqvt_at (\<lambda>(a,b). evals a b) (ECons cenva x (evals enva t2a), t)")
80f01215d1a6 Setup eqvt_at for first goal Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2952 diff changeset	61	apply (subgoal_tac "eqvt_at (\<lambda>(a,b). evals a b) (enva, t2a)")
80f01215d1a6 Setup eqvt_at for first goal Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2952 diff changeset	62	apply (subgoal_tac "eqvt_at (\<lambda>(a,b). evals a b) (ECons cenva xa (evals enva t2a), ta)")
80f01215d1a6 Setup eqvt_at for first goal Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2952 diff changeset	63	apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva x (evals enva t2a), t))")
80f01215d1a6 Setup eqvt_at for first goal Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2952 diff changeset	64	apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (enva, t2a))")
80f01215d1a6 Setup eqvt_at for first goal Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2952 diff changeset	65	apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva xa (evals enva t2a), ta))")
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	66	defer
2953 80f01215d1a6 Setup eqvt_at for first goal Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2952 diff changeset	67	apply (simp_all add: eqvt_at_def evals_def)[3]
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	68	sorry
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	69
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	70	(* can probably not proved by a trivial size argument *)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	71	termination sorry
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	72
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	73

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Wed, 06 Jul 2011 07:42:12 +0900
changeset 2953	80f01215d1a6
parent 2952	e4c2854833ad
child 2954	dc6007dd9c30
permissions	-rw-r--r--