39 primrec

    40   permute_bn_raw

    41 where

    42   "permute_bn_raw p (As_raw x y t) = As_raw (p \<bullet> x) y t"

    43 

    44 quotient_definition

    45   "permute_bn :: perm \<Rightarrow> assg \<Rightarrow> assg"

    46 is

    47   "permute_bn_raw"

    48 

    49 lemma [quot_respect]:

    50   shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn_raw permute_bn_raw"

    51   apply simp

    52   apply clarify

    53   apply (erule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts)

    54   apply (rule TrueI)+

    55   apply simp_all

    56   apply (rule_tac [!] alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)

    57   apply simp_all

    58   done

    59 

    60 lemmas permute_bn = permute_bn_raw.simps[quot_lifted]

    61 

    62 lemma uu:

    63   shows "alpha_bn as (permute_bn p as)"

    64 apply(induct as rule: single_let.inducts(2))

    65 apply(auto)[7]

    66 apply(simp add: permute_bn)

    67 apply(simp add: single_let.eq_iff)

    68 done

    69 

    70 lemma tt:

    71   shows "(p \<bullet> bn as) = bn (permute_bn p as)"

    72 apply(induct as rule: single_let.inducts(2))

    73 apply(auto)[7]

    74 apply(simp add: permute_bn single_let.bn_defs)

    75 apply(simp add: atom_eqvt)

    76 done

    77 

    78 lemma Abs_fresh_star':

    79   fixes x::"'a::fs"

    80   shows  "set bs = as \<Longrightarrow> as \<sharp>* Abs_lst bs x"

    81   unfolding fresh_star_def

    82   by(simp_all add: Abs_fresh_iff)

    83 

    84 lemma strong_exhaust:

    85   fixes c::"'a::fs"

    86   assumes "\<And>name. y = Var name \<Longrightarrow> P" 

    87   and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" 

    88   and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P"

    89   and "\<And>assg trm. \<lbrakk>set (bn assg) \<sharp>* c; y = Let assg trm\<rbrakk> \<Longrightarrow> P"

    90   and "\<And>name1 name2 trm1 trm2 trm3. \<lbrakk>{atom name1} \<sharp>* c; y = Foo name1 name2 trm1 trm2 trm3\<rbrakk> \<Longrightarrow> P"

    91   and "\<And>name1 name2 trm. \<lbrakk>{atom name1, atom name2} \<sharp>* c; y = Bar name1 name2 trm\<rbrakk> \<Longrightarrow> P" 

    92   and "\<And>name trm1 trm2. \<lbrakk>{atom name} \<sharp>* c; y = Baz name trm1 trm2\<rbrakk> \<Longrightarrow> P"

    93   shows "P"

    94   apply(rule_tac y="y" in single_let.exhaust(1))

    95   apply(rule assms(1))

    96   apply(assumption)

    97   apply(rule assms(2))

    98   apply(assumption)

    99   apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp ([[atom name]]lst.trm) \<sharp>* q")

   100   apply(erule exE)

   101   apply(erule conjE)

   102   apply(perm_simp)

   103   apply(rule assms(3))

   104   apply(assumption)

   105   apply(drule supp_perm_eq[symmetric])

   106   apply(simp add: single_let.eq_iff)

   107   apply(perm_simp)

   108   apply(rule refl)

   109   apply(rule at_set_avoiding2)

   110   apply(simp add: finite_supp)

   111   apply(simp add: finite_supp)

   112   apply(simp add: finite_supp)

   113   apply(simp add: Abs_fresh_star')

   114   apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assg))) \<sharp>* (c::'a::fs) \<and> supp ([bn assg]lst.trm) \<sharp>* q")

   115   apply(erule exE)

   116   apply(erule conjE)

   117   apply(perm_simp add: tt)

   118   apply(rule_tac assms(4))

   119   apply(assumption)

   120   apply(drule supp_perm_eq[symmetric])

   121   apply(simp add: single_let.eq_iff)

   122   apply(simp add: tt uu)

   123   apply(rule at_set_avoiding2)

   124   apply(simp add: finite_supp)

   125   apply(simp add: finite_supp)

   126   apply(simp add: finite_supp)

   127   apply(simp add: Abs_fresh_star)

   128   apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name1}) \<sharp>* (c::'a::fs) \<and> 

   129     supp ([{atom name1}]set.(((name2, trm1), trm2), trm3)) \<sharp>* q")

   130   apply(erule exE)

   131   apply(erule conjE)

   132   apply(perm_simp add: tt)

   133   apply(rule_tac assms(5))

   134   apply(assumption)

   135   apply(drule supp_perm_eq[symmetric])

   136   apply(simp add: single_let.eq_iff)

   137   apply(perm_simp)

   138   apply(rule refl)

   139   apply(rule at_set_avoiding2)

   140   apply(simp add: finite_supp)

   141   apply(simp add: finite_supp)

   142   apply(simp add: finite_supp)

   143   apply(simp add: Abs_fresh_star)

   144   apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name1, atom name2}) \<sharp>* (c::'a::fs) \<and> 

   145     supp ([[atom name2, atom name1]]lst.((trm, name1), name2)) \<sharp>* q")

   146   apply(erule exE)

   147   apply(erule conjE)

   148   apply(perm_simp add: tt)

   149   apply(rule_tac assms(6))

   150   apply(assumption)

   151   apply(drule supp_perm_eq[symmetric])

   152   apply(simp add: single_let.eq_iff)

   153   apply(perm_simp)

   154   apply(rule refl)

   155   apply(rule at_set_avoiding2)

   156   apply(simp add: finite_supp)

   157   apply(simp add: finite_supp)

   158   apply(simp add: finite_supp)

   159   oops

   160   (*apply(simp add: Abs_fresh_star)*)

   161 sorry

   162   

   163 done