1 theory SingleLet

     1 theory SingleLet

     3 begin

     3 begin

     4 

     4 

     5 atom_decl name

     5 atom_decl name

     6 

     6 

     7 declare [[STEPS = 100]]

     7 declare [[STEPS = 100]]

    36 thm single_let.fsupp

    36 thm single_let.fsupp

    37 

    37 

    38 

    38 

    39 

    39 

    40 

    40 

    42 lemma test: 

    42 lemma test: 

    43   "(\<exists>p. (bs, x) \<approx>lst (op=) f p (cs, y)) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>lst (op=) supp p (cs, y))"

    43   "(\<exists>p. (bs, x) \<approx>lst (op=) f p (cs, y)) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>lst (op=) supp p (cs, y))"

    45 

    45 

    46 lemma Abs_eq_iff:

    46 lemma Abs_eq_iff:

    47   shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"

    47   shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"

    48   and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"

    48   and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"

    49   and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"

    49   and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"

    50   by (lifting alphas_abs)

    50   by (lifting alphas_abs)

    51 

    52 

    52 lemma supp_fv:

    54 lemma supp_fv:

    53   "supp t = fv_trm t \<and> supp b = fv_bn b"

    55   "supp t = fv_trm t \<and> supp b = fv_bn b"

    54 apply(rule single_let.induct)

    56 apply(rule single_let.induct)

    55 apply(simp_all only: single_let.fv_defs)[2]

    57 apply(simp_all only: single_let.fv_defs)[2]

    56 apply(simp_all only: supp_def)[2]

    58 apply(simp_all only: supp_def)[2]

    71 apply(simp only: permute_abs atom_eqvt permute_list.simps)

    73 apply(simp only: permute_abs atom_eqvt permute_list.simps)

    72 apply(simp only: Abs_eq_iff)

    74 apply(simp only: Abs_eq_iff)

    73 apply(subst test)

    75 apply(subst test)

    74 apply(rule refl)

    76 apply(rule refl)

    75 sorry

    77 sorry

    77 (*

    79 (*

    78 consts perm_bn_trm :: "perm \<Rightarrow> trm \<Rightarrow> trm"

    80 consts perm_bn_trm :: "perm \<Rightarrow> trm \<Rightarrow> trm"

    79 consts perm_bn_assg :: "perm \<Rightarrow> assg \<Rightarrow> assg"

    81 consts perm_bn_assg :: "perm \<Rightarrow> assg \<Rightarrow> assg"

    80 

    82 

    81 lemma y:

    83 lemma y: