# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1310766517 -3600
# Node ID d7e8b9b78e28021dcfed681eeac1528bf8ec66d8
# Parent  fa37c2a33812f52cb6a769b2be0217dee5debac5
some improvements to the NBE example

diff -r fa37c2a33812 -r d7e8b9b78e28 Nominal/Ex/NBE.thy
--- a/Nominal/Ex/NBE.thy	Wed Jul 13 09:47:58 2011 +0100
+++ b/Nominal/Ex/NBE.thy	Fri Jul 15 22:48:37 2011 +0100
@@ -30,44 +30,16 @@
 
 nominal_primrec
   evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and
-  evals_aux :: "sem \<Rightarrow> lam \<Rightarrow> env \<Rightarrow> sem"
+  evals_aux :: "sem \<Rightarrow> sem \<Rightarrow> sem"
 where
   "evals ENil (Var x) = N (V x)"
 | "evals (ECons tail y v) (Var x) = (if x = y then v else evals tail (Var x))" 
-| "evals env (Lam [x]. t) = L env x t"
-| "evals env (App t1 t2) = evals_aux (evals env t1) t2 env"
-| "evals_aux (L cenv x t) t2 env = evals (ECons cenv x (evals env t2)) t"
-| "evals_aux (N n) t2 env = N (A n (evals env t2))"
-apply(subgoal_tac "\<And>p x y. evals_evals_aux_graph x y \<Longrightarrow> evals_evals_aux_graph (p \<bullet> x) (p \<bullet> y)")
-apply(simp add: eqvt_def)
-apply(simp add: permute_fun_def)
-apply(rule allI)
-apply(rule ext)
-apply(rule ext)
-apply(rule iffI)
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="- p \<bullet> x" in meta_spec)
-apply(drule_tac x="- p \<bullet> xa" in meta_spec)
-apply(simp add: permute_bool_def)
-apply(simp add: permute_bool_def)
-apply(erule evals_evals_aux_graph.induct)
+| "atom x \<sharp> env \<Longrightarrow> evals env (Lam [x]. t) = L env x t"
+| "evals env (App t1 t2) = evals_aux (evals env t1) (evals env t2)"
+| "evals_aux (L cenv x t) t' = evals (ECons cenv x t') t"
+| "evals_aux (N n) t' = N (A n t')"
+apply(simp add: eqvt_def  evals_evals_aux_graph_def)
 apply(perm_simp)
-apply(rule evals_evals_aux_graph.intros)
-apply(perm_simp)
-apply(rule evals_evals_aux_graph.intros)
-apply(simp)
-apply(perm_simp)
-apply(rule evals_evals_aux_graph.intros)
-apply(perm_simp)
-apply(rule evals_evals_aux_graph.intros)
-apply(simp)
-apply(simp)
-apply(perm_simp)
-apply(rule evals_evals_aux_graph.intros)
-apply(simp)
-apply(simp)
-apply(perm_simp)
-apply(rule evals_evals_aux_graph.intros)
 apply(simp)
 apply (rule TrueI)
 --"completeness"
@@ -76,11 +48,17 @@
 apply(case_tac a)
 apply(simp)
 apply(case_tac aa rule: sem_neu_env.exhaust(3))
-apply(simp)
+apply(simp add: sem_neu_env.fresh)
 apply(case_tac b rule: lam.exhaust)
 apply(metis)+
-apply(case_tac b rule: lam.exhaust)
+apply(case_tac aa rule: sem_neu_env.exhaust(3))
+apply(rule_tac y="b" and c="env" in lam.strong_exhaust)
 apply(metis)+
+apply(simp add: fresh_star_def)
+apply(simp)
+apply(rule_tac y="b" and c="ECons env name sem" in lam.strong_exhaust)
+apply(metis)+
+apply(simp add: fresh_star_def)
 apply(simp)
 apply(case_tac b)
 apply(simp)
@@ -94,16 +72,23 @@
 apply(simp)
 apply(simp)
 apply (simp add: meta_eq_to_obj_eq[OF evals_def, symmetric, unfolded fun_eq_iff])
-apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenv x (evals enva t2a), t)")
-apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (enva, t2a)")
-apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenva xa (evals enva t2a), ta)")
-apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenv x (evals enva t2a), t))")
-apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (enva, t2a))")
-apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva xa (evals enva t2a), ta))")
+apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenv x t'a, t)")
+apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenva xa t'a, ta)")
+apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenv x t'a, t))")
+apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva xa t'a, ta))")
 apply(erule conjE)+
 defer
 apply (simp_all add: eqvt_at_def evals_def)[3]
-apply(simp)
+apply(simp add: sem_neu_env.alpha_refl)
+apply(erule conjE)+
+apply(erule_tac c="(env, enva)" in Abs_lst1_fcb2)
+apply(simp add: Abs_fresh_iff)
+apply(simp add: fresh_star_def)
+apply(perm_simp)
+apply(simp add: fresh_star_Pair perm_supp_eq)
+apply(perm_simp)
+apply(simp add: fresh_star_Pair perm_supp_eq)
+thm Abs_lst1_fcb2'
 sorry
 
 (* can probably not proved by a trivial size argument *)
@@ -111,7 +96,7 @@
 
 lemma [eqvt]:
   shows "(p \<bullet> evals env t) = evals (p \<bullet> env) (p \<bullet> t)"
-  and "(p \<bullet> evals_aux v t env) = evals_aux (p \<bullet> v) (p \<bullet> t) (p \<bullet> env)"
+  and "(p \<bullet> evals_aux v s) = evals_aux (p \<bullet> v) (p \<bullet> s)"
 sorry
 
 (* fixme: should be a provided lemma *)
@@ -124,8 +109,8 @@
 lemma test:
   fixes env::"env"
   shows "supp (evals env t) \<subseteq> (supp t - set (bn env)) \<union> (fv_bn env)"
-  and "supp (evals_aux s t env) \<subseteq> (supp s) \<union> (fv_bn env) \<union> (supp (t) - set (bn env))"
-apply(induct env t and s t env rule: evals_evals_aux.induct)
+  and "supp (evals_aux s v) \<subseteq> (supp s) \<union> (supp v)"
+apply(induct env t and s v rule: evals_evals_aux.induct)
 apply(simp add: sem_neu_env.supp lam.supp supp_Nil sem_neu_env.bn_defs)
 apply(simp add: sem_neu_env.supp lam.supp supp_Nil supp_Cons sem_neu_env.bn_defs)
 apply(rule conjI)
@@ -141,12 +126,8 @@
 apply(simp add: lam.supp sem_neu_env.supp)
 apply(blast)
 apply(simp add: sem_neu_env.supp sem_neu_env.bn_defs)
-prefer 2
+apply(blast)
 apply(simp add: sem_neu_env.supp)
-apply(rule conjI)
-apply(blast)
-apply(blast)
-apply(blast)
 done
 
 
@@ -280,15 +261,18 @@
 apply(perm_simp)
 apply(simp add: flip_fresh_fresh fresh_Pair)
 apply(drule sym)
+(* HERE *)
+apply(rotate_tac 9)
+apply(drule sym)
 apply(rotate_tac 9)
 apply(drule trans)
 apply(rule sym)
-(* HERE *)
-
 apply(rule_tac p="p" in supp_perm_eq)
+apply(assumption)
 apply(simp)
 apply(perm_simp)
-apply(simp add: Abs_eq_iff2 alphas)
+apply(simp (no_asm_use) add: Abs_eq_iff2 alphas)
+apply(erule conjE | erule exE)+
 apply(clarify)
 apply(rule trans)
 apply(rule sym)