Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Ex/NBE.thy
changeset 2956 7e1c309bf820
parent 2955 4049a2651dd9
child 2967 d7e8b9b78e28
equal deleted inserted replaced
2955:4049a2651dd9 2956:7e1c309bf820 
    11 | App "lam" "lam"
 
    11 | App "lam" "lam"
 
    12 | Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
 
    12 | Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
 
    13 
    13 
    14 
    14 
    15 nominal_datatype sem =
 
    15 nominal_datatype sem =
 
    16   L e::"env" x::"name" l::"lam" binds "bn e" x in l
 
    16   L e::"env" x::"name" l::"lam" binds x "bn e" in l
 
    17 | N "neu"
 
    17 | N "neu"
 
    18 and neu = 
    18 and neu = 
    19   V "name"
 
    19   V "name"
 
    20 | A "neu" "sem"
 
    20 | A "neu" "sem"
 
    21 and env =
 
    21 and env =
 
    23 | ECons "env" "name" "sem"
 
    23 | ECons "env" "name" "sem"
 
    24 binder
 
    24 binder
 
    25   bn
 
    25   bn
 
    26 where
 
    26 where
 
    27   "bn ENil = []"
 
    27   "bn ENil = []"
 
    28 | "bn (ECons env x v) = atom x # bn env" 
    28 | "bn (ECons env x v) = (atom x) # (bn env)" 
       
    29 
    29 
    30 
    30 nominal_primrec
 
    31 nominal_primrec
 
    31   evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and
 
    32   evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and
 
    32   evals_aux :: "sem \<Rightarrow> lam \<Rightarrow> env \<Rightarrow> sem"
 
    33   evals_aux :: "sem \<Rightarrow> lam \<Rightarrow> env \<Rightarrow> sem"
 
    33 where
 
    34 where
 
   119 apply(induct env rule: sem_neu_env.inducts(3))
 
   120 apply(induct env rule: sem_neu_env.inducts(3))
 
   120 apply(auto simp add: sem_neu_env.supp finite_supp)
 
   121 apply(auto simp add: sem_neu_env.supp finite_supp)
 
   121 done
 
   122 done
 
   122 
   123 
   123 lemma test:
 
   124 lemma test:
 
       
   125   fixes env::"env"
 
   124   shows "supp (evals env t) \<subseteq> (supp t - set (bn env)) \<union> (fv_bn env)"
 
   126   shows "supp (evals env t) \<subseteq> (supp t - set (bn env)) \<union> (fv_bn env)"
 
   125   and "supp (evals_aux s t env) \<subseteq> ((supp s) - set (bn cenv)) \<union> supp (fn cenv) \<union> supp (evals env t)"
 
   127   and "supp (evals_aux s t env) \<subseteq> (supp s) \<union> (fv_bn env) \<union> (supp (t) - set (bn env))"
 
   126 apply(induct rule: evals_evals_aux.induct)
 
   128 apply(induct env t and s t env rule: evals_evals_aux.induct)
 
   127 apply(simp add: sem_neu_env.supp lam.supp supp_Nil sem_neu_env.bn_defs)
 
   129 apply(simp add: sem_neu_env.supp lam.supp supp_Nil sem_neu_env.bn_defs)
 
   128 apply(simp add: sem_neu_env.supp lam.supp supp_Nil supp_Cons sem_neu_env.bn_defs)
 
   130 apply(simp add: sem_neu_env.supp lam.supp supp_Nil supp_Cons sem_neu_env.bn_defs)
 
   129 apply(rule conjI)
 
   131 apply(rule conjI)
 
   130 apply(auto)[1]
 
   132 apply(auto)[1]
 
   131 apply(rule impI)
 
   133 apply(rule impI)
 
   132 apply(simp)
 
   134 apply(simp)
 
   133 apply (metis (no_types) at_base_infinite finite_UNIV)
 
   135 apply(simp add: supp_at_base)
 
       
   136 apply(blast)
 
   134 apply(simp)
 
   137 apply(simp)
 
   135 apply(subst sem_neu_env.supp)
 
   138 apply(subst sem_neu_env.supp)
 
   136 apply(simp add: sem_neu_env.supp lam.supp)
 
   139 apply(simp add: sem_neu_env.supp lam.supp)
 
   137 apply(auto)[1]
 
   140 apply(auto)[1]
 
   138 apply(simp)
 
   141 apply(simp add: lam.supp sem_neu_env.supp)
 
   139 apply(metis)
 
   142 apply(blast)
 
   140 sorry
 
   143 apply(simp add: sem_neu_env.supp sem_neu_env.bn_defs)
 
       
   144 prefer 2
 
       
   145 apply(simp add: sem_neu_env.supp)
 
       
   146 apply(rule conjI)
 
       
   147 apply(blast)
 
       
   148 apply(blast)
 
       
   149 apply(blast)
 
       
   150 done
 
       
   151 
   141 
   152 
   142 nominal_primrec
 
   153 nominal_primrec
 
   143   reify :: "sem \<Rightarrow> lam" and
 
   154   reify :: "sem \<Rightarrow> lam" and
 
   144   reifyn :: "neu \<Rightarrow> lam"
 
   155   reifyn :: "neu \<Rightarrow> lam"
 
   145 where
 
   156 where
 
   195 apply(simp)
 
   206 apply(simp)
 
   196 apply(simp)
 
   207 apply(simp)
 
   197 apply(simp)
 
   208 apply(simp)
 
   198 apply(erule conjE)
 
   209 apply(erule conjE)
 
   199 apply (simp add: meta_eq_to_obj_eq[OF reify_def, symmetric, unfolded fun_eq_iff])
 
   210 apply (simp add: meta_eq_to_obj_eq[OF reify_def, symmetric, unfolded fun_eq_iff])
 
   200 apply (subgoal_tac "eqvt_at (\<lambda>t. reify t) (evals (ECons enva y (N (V x))) t)")
 
   211 apply (subgoal_tac "eqvt_at (\<lambda>t. reify t) (evals (ECons env y (N (V x))) t)")
 
   201 apply (subgoal_tac "eqvt_at (\<lambda>t. reify t) (evals (ECons enva ya (N (V xa))) ta)")
 
   212 apply (subgoal_tac "eqvt_at (\<lambda>t. reify t) (evals (ECons enva ya (N (V xa))) ta)")
 
   202 apply (thin_tac "eqvt_at reify_reifyn_sumC (Inl (evals (ECons enva y (N (V x))) t))")
 
   213 apply (thin_tac "eqvt_at reify_reifyn_sumC (Inl (evals (ECons env y (N (V x))) t))")
 
   203 apply (thin_tac "eqvt_at reify_reifyn_sumC (Inl (evals (ECons enva ya (N (V xa))) ta))")
 
   214 apply (thin_tac "eqvt_at reify_reifyn_sumC (Inl (evals (ECons enva ya (N (V xa))) ta))")
 
   204 defer
 
   215 defer
 
   205 apply (simp_all add: eqvt_at_def reify_def)[2]
 
   216 apply (simp_all add: eqvt_at_def reify_def)[2]
 
   206 apply(subgoal_tac "\<exists>c::name. atom c \<sharp> (x, xa, enva, y, ya, t, ta)")
 
   217 apply(subgoal_tac "\<exists>c::name. atom c \<sharp> (x, xa, env, enva, y, ya, t, ta)")
 
   207 prefer 2
 
   218 prefer 2
 
   208 apply(rule obtain_fresh)
 
   219 apply(rule obtain_fresh)
 
   209 apply(blast)
 
   220 apply(blast)
 
   210 apply(erule exE)
 
   221 apply(erule exE)
 
   211 apply(rule trans)
 
   222 apply(rule trans)
 
   216 apply(auto)[1]
 
   227 apply(auto)[1]
 
   217 apply(rule fresh_eqvt_at)
 
   228 apply(rule fresh_eqvt_at)
 
   218 back
 
   229 back
 
   219 apply(assumption)
 
   230 apply(assumption)
 
   220 apply(simp add: finite_supp)
 
   231 apply(simp add: finite_supp)
 
   221 apply(rule_tac S="supp (enva, y, x, t)" in supports_fresh)
 
   232 apply(rule_tac S="supp (env, y, x, t)" in supports_fresh)
 
   222 apply(simp add: supports_def fresh_def[symmetric])
 
   233 apply(simp add: supports_def fresh_def[symmetric])
 
   223 apply(perm_simp)
 
   234 apply(perm_simp)
 
   224 apply(simp add: swap_fresh_fresh fresh_Pair)
 
   235 apply(simp add: swap_fresh_fresh fresh_Pair)
 
   225 apply(simp add: finite_supp)
 
   236 apply(simp add: finite_supp)
 
   226 apply(simp add: fresh_def[symmetric])
 
   237 apply(simp add: fresh_def[symmetric])
 
   248 apply(simp add: eqvt_at_def)
 
   259 apply(simp add: eqvt_at_def)
 
   249 apply(simp add: eqvt_at_def[symmetric])
 
   260 apply(simp add: eqvt_at_def[symmetric])
 
   250 apply(perm_simp)
 
   261 apply(perm_simp)
 
   251 apply(simp add: flip_fresh_fresh)
 
   262 apply(simp add: flip_fresh_fresh)
 
   252 apply(simp (no_asm) add: Abs1_eq_iff)
 
   263 apply(simp (no_asm) add: Abs1_eq_iff)
 
       
   264 thm at_set_avoiding3
 
       
   265 using at_set_avoiding3
 
       
   266 apply -
 
       
   267 apply(drule_tac x="set (atom y # bn env)" in meta_spec)
 
       
   268 apply(drule_tac x="(env, enva)" in meta_spec)
 
       
   269 apply(drule_tac x="[atom y # bn env]lst. t" in meta_spec)
 
       
   270 apply(simp (no_asm_use) add: finite_supp)
 
       
   271 apply(drule meta_mp)
 
       
   272 apply(rule Abs_fresh_star)
 
       
   273 apply(auto)[1]
 
       
   274 apply(erule exE)
 
       
   275 apply(erule conjE)+
 
       
   276 apply(drule_tac q="(x \<leftrightarrow> c)" in eqvt_at_perm)
 
       
   277 apply(perm_simp)
 
       
   278 apply(simp add: flip_fresh_fresh fresh_Pair)
 
       
   279 apply(drule_tac q="(xa \<leftrightarrow> c)" in eqvt_at_perm)
 
       
   280 apply(perm_simp)
 
       
   281 apply(simp add: flip_fresh_fresh fresh_Pair)
 
       
   282 apply(drule sym)
 
       
   283 apply(rotate_tac 9)
 
       
   284 apply(drule trans)
 
       
   285 apply(rule sym)
 
       
   286 (* HERE *)
 
       
   287 
       
   288 apply(rule_tac p="p" in supp_perm_eq)
 
       
   289 apply(simp)
 
       
   290 apply(perm_simp)
 
       
   291 apply(simp add: Abs_eq_iff2 alphas)
 
       
   292 apply(clarify)
 
       
   293 apply(rule trans)
 
       
   294 apply(rule sym)
 
       
   295 apply(rule_tac p="pa" in perm_supp_eq)
 
       
   296 defer
 
       
   297 apply(rule sym)
 
       
   298 apply(rule trans)
 
       
   299 apply(rule sym)
 
       
   300 apply(rule_tac p="p" in perm_supp_eq)
 
       
   301 defer
 
       
   302 apply(simp add: atom_eqvt)
 
       
   303 apply(drule_tac q="(x \<leftrightarrow> c)" in eqvt_at_perm)
 
       
   304 apply(perm_simp)
 
       
   305 apply(simp add: flip_fresh_fresh fresh_Pair)
 
       
   306 
   253 apply(rule sym)
 
   307 apply(rule sym)
 
   254 apply(erule_tac Abs_lst1_fcb2')
 
   308 apply(erule_tac Abs_lst1_fcb2')
 
   255 apply(rule fresh_eqvt_at)
 
   309 apply(rule fresh_eqvt_at)
 
   256 back
 
   310 back
 
   257 apply(drule_tac q="(c \<leftrightarrow> x)" in eqvt_at_perm)
 
   311 apply(drule_tac q="(c \<leftrightarrow> x)" in eqvt_at_perm)
nominal2