Nominal/Ex/SingleLetFoo.thy
changeset 2130 5111dadd1162
child 2132 d74e08799b63
equal deleted inserted replaced
2129:f38adea0591c 2130:5111dadd1162
       
     1 theory SingleLetFoo
       
     2 imports "../NewParser"
       
     3 begin
       
     4 
       
     5 
       
     6 declare [[STEPS = 4]]
       
     7 (* alpha does not work for this type *)
       
     8 
       
     9 atom_decl name
       
    10 
       
    11 nominal_datatype trm =
       
    12   Var "name"
       
    13 | App "trm" "trm"
       
    14 | Lam x::"name" t::"trm"  bind_set x in t
       
    15 | Let a::"assg" t::"trm"  bind_set "bn a" in t
       
    16 | Foo1 a1::"assg" a2::"assg" t::"trm" bind_set "bn a1" "bn a2" in t
       
    17 | Foo2 x::name a::"assg" t::"trm" bind_set x "bn a" in t
       
    18 and assg =
       
    19   As "name" "trm"
       
    20 binder
       
    21   bn::"assg \<Rightarrow> atom set"
       
    22 where
       
    23   "bn (As x t) = {atom x}"
       
    24 
       
    25 thm permute_trm_raw_permute_assg_raw.simps
       
    26 thm fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps[no_vars]
       
    27 
       
    28 (* there is something wrong with the free variables *)
       
    29 
       
    30 text {*
       
    31 thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]
       
    32 *}
       
    33 
       
    34 inductive 
       
    35   alpha_trm_raw and alpha_assg_raw and alpha_bn_raw
       
    36 where
       
    37   "name = namea \<Longrightarrow> alpha_trm_raw (Var_raw name) (Var_raw namea)"
       
    38 | "\<lbrakk>alpha_trm_raw trm_raw1 trm_raw1a; alpha_trm_raw trm_raw2 trm_raw2a\<rbrakk>
       
    39   \<Longrightarrow> alpha_trm_raw (App_raw trm_raw1 trm_raw2) (App_raw trm_raw1a trm_raw2a)"
       
    40 | "\<exists>p. ({atom name}, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p ({atom namea}, trm_rawa) \<Longrightarrow>
       
    41    alpha_trm_raw (Lam_raw name trm_raw) (Lam_raw namea trm_rawa)"
       
    42 | "\<lbrakk>\<exists>p. (bn_raw assg_raw, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p (bn_raw assg_rawa, trm_rawa);
       
    43     alpha_bn_raw assg_raw assg_rawa\<rbrakk>
       
    44     \<Longrightarrow> alpha_trm_raw (Let_raw assg_raw trm_raw) (Let_raw assg_rawa trm_rawa)"
       
    45 | "\<lbrakk>\<exists>p. (bn_raw assg_raw1 \<union> bn_raw ass_raw2, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p 
       
    46         (bn_raw assg_raw1a \<union> bn_raw ass_raw2a, trm_rawa);
       
    47    alpha_bn_raw assg_raw1 assg_raw1a; alpha_bn_raw assg_raw2 assg_raw2a\<rbrakk>
       
    48    \<Longrightarrow> alpha_trm_raw (Foo1_raw assg_raw1 assg_raw2 trm_raw) (Foo1_raw assg_raw1a assg_raw2a trm_rawa)"
       
    49 | "\<lbrakk>\<exists>p. ({atom name} \<union> bn_raw assg_raw, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p 
       
    50         ({atom namea} \<union> bn_raw assg_rawa, trm_rawa);
       
    51    alpha_bn_raw assg_raw assg_rawa\<rbrakk>
       
    52    \<Longrightarrow> alpha_trm_raw (Foo2_raw name assg_raw trm_raw) (Foo2_raw namea assg_rawa trm_rawa)"
       
    53 
       
    54 | "\<lbrakk>name = namea; alpha_trm_raw trm_raw trm_rawa\<rbrakk>
       
    55   \<Longrightarrow> alpha_assg_raw (As_raw name trm_raw) (As_raw namea trm_rawa)"
       
    56 | "alpha_trm_raw trm_raw trm_rawa \<Longrightarrow> alpha_bn_raw (As_raw name trm_raw) (As_raw namea trm_rawa)"
       
    57 
       
    58 lemmas all = alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros
       
    59 
       
    60 lemma test: "p \<bullet> bn_raw \<equiv> bn_raw" sorry
       
    61 
       
    62 lemma
       
    63   assumes "distinct [x,y, z, u]"
       
    64   shows "alpha_trm_raw (Foo2_raw z (As_raw x (Var_raw z)) (Var_raw z))
       
    65                        (Foo2_raw u (As_raw y (Var_raw z)) (Var_raw u))"
       
    66 using assms
       
    67 apply(rule_tac all)
       
    68 apply(rule_tac x="(z \<leftrightarrow> u) + (x \<leftrightarrow> y)" in exI)
       
    69 apply(simp only: alphas)
       
    70 apply(rule conjI)
       
    71 apply(simp)
       
    72 apply(simp add: supp_at_base fresh_star_def)
       
    73 apply(rule conjI)
       
    74 apply(simp add: supp_at_base fresh_star_def)
       
    75 apply(rule conjI)
       
    76 apply(simp)
       
    77 apply(rule all)
       
    78 apply(simp)
       
    79 unfolding flip_def
       
    80 apply(perm_simp add: test)
       
    81 unfolding flip_def[symmetric]
       
    82 apply(simp)
       
    83 apply(subst flip_at_base_simps(3))
       
    84 apply(auto)[2]
       
    85 apply(simp)
       
    86 apply(rule all)
       
    87 apply(rule all)
       
    88 apply(simp)
       
    89 done
       
    90 
       
    91 lemma
       
    92   assumes "distinct [x,y,z,u]"
       
    93   shows "fv_trm_raw (Foo2_raw z (As_raw x (Var_raw z)) (Var_raw z)) = {atom z}"
       
    94 using assms
       
    95 apply(simp add: supp_at_base)
       
    96 
       
    97 
       
    98 end
       
    99 
       
   100 
       
   101