11 oops

    11   unfolding addlam_graph_def eqvt_def

    12 

    12   apply perm_simp

    13 

    13   apply auto

    14 nominal_primrec

    14   apply (case_tac x rule: lam.exhaust)

    15   addlam_pre :: "lam \<Rightarrow> lam \<Rightarrow> lam"

    15   apply auto

    16 where

    16   apply (rule_tac x="name" and ?'a="name" in obtain_fresh)

    17   "fv \<noteq> x \<Longrightarrow> addlam_pre (Var x) (Lam [fv].it) = Lam [fv]. App (Var fv) (Var x)"

    17   apply (simp add: fresh_at_base)

    18 | "addlam_pre (Var x) (App t1 t2) = Var x"

    18   apply (simp add: Abs1_eq_iff lam.fresh fresh_at_base)

    19 | "addlam_pre (Var x) (Var v) = Var x"

    20 | "addlam_pre (App t1 t2) it = App t1 t2"

    21 | "addlam_pre (Lam [x]. t) it = Lam [x].t"

    22 apply (subgoal_tac "\<And>p a x. addlam_pre_graph a x \<Longrightarrow> addlam_pre_graph (p \<bullet> a) (p \<bullet> x)")

    23 apply (simp add: eqvt_def)

    24 apply (intro allI)

    25 apply(simp add: permute_fun_def)

    26 apply(rule ext)

    27 apply(rule ext)

    28 apply(simp add: permute_bool_def)

    29 apply rule

    30 apply(drule_tac x="p" in meta_spec)

    31 apply(drule_tac x="- p \<bullet> x" in meta_spec)

    32 apply(drule_tac x="- p \<bullet> xa" in meta_spec)

    33 apply simp

    34 apply(drule_tac x="-p" in meta_spec)

    35 apply(drule_tac x="x" in meta_spec)

    36 apply(drule_tac x="xa" in meta_spec)

    37 apply simp

    38 apply (erule addlam_pre_graph.induct)

    39 apply (simp_all add: addlam_pre_graph.intros)

    40 apply (simp_all add:lam.distinct)

    41 apply clarify

    42 apply simp

    43 apply (rule_tac y="a" in lam.exhaust)

    44 apply(auto simp add: lam.distinct lam.eq_iff)

    45 prefer 2 apply blast

    46 prefer 2 apply blast

    47 apply (rule_tac y="b" and c="name" in lam.strong_exhaust)

    48 apply(auto simp add: lam.distinct lam.eq_iff)[3]

    49 apply blast

    50 apply(drule_tac x="namea" in meta_spec)

    51 apply(drule_tac x="name" in meta_spec)

    52 apply(drule_tac x="lam" in meta_spec)

    53 apply (auto simp add: fresh_star_def atom_name_def fresh_at_base)[1]

    54 apply (auto simp add: lam.eq_iff Abs1_eq_iff fresh_def lam.supp supp_at_base)

    55 done

    56 

    57 termination

    58   by (relation "measure (\<lambda>(t,_). size t)")

    59      (simp_all add: lam.size)

    60 

    61 function

    62   addlam :: "lam \<Rightarrow> lam"

    63 where

    64   "addlam (Var x) = addlam_pre (Var x) (Lam [x]. (Var x))"

    65 | "addlam (App t1 t2) = App t1 t2"

    66 | "addlam (Lam [x]. t) = Lam [x].t"

    67 apply (simp_all add:lam.distinct)

    68 apply (rule_tac y="x" in lam.exhaust)

    69 apply auto

    70 apply (simp add:lam.eq_iff)

    71 done

    72 

    73 termination

    74   by (relation "measure (\<lambda>(t). size t)")

    75      (simp_all add: lam.size)

    76 

    77 lemma addlam':

    78   "fv \<noteq> x \<Longrightarrow> addlam (Var x) = Lam [fv]. App (Var fv) (Var x)"

    79   apply simp

    80   apply (subgoal_tac "Lam [x]. Var x = Lam [fv]. Var fv")

    81   apply simp

    82   apply (simp add: lam.eq_iff Abs1_eq_iff lam.supp fresh_def supp_at_base)

    85 nominal_primrec

    21 termination by lexicographic_order

    86   Pair_pre

    87 where

    88   "atom z \<sharp> (M, N) \<Longrightarrow> (Pair_pre M N) (Lam [z]. _) = (Lam [z]. App (App (Var z) M) N)"

    89 | "(Pair_pre M N) (App l r) = (App l r)"

    90 | "(Pair_pre M N) (Var v) = (Var v)"

    91 apply (subgoal_tac "\<And>p a x. Pair_pre_graph a x \<Longrightarrow> Pair_pre_graph (p \<bullet> a) (p \<bullet> x)")

    92 apply (simp add: eqvt_def)

    93 apply (intro allI)

    94 apply(simp add: permute_fun_def)

    95 apply(rule ext)

    96 apply(rule ext)

    97 apply(simp add: permute_bool_def)

    98 apply rule

    99 apply(drule_tac x="p" in meta_spec)

   100 apply(drule_tac x="- p \<bullet> x" in meta_spec)

   101 apply(drule_tac x="- p \<bullet> xa" in meta_spec)

   102 apply simp

   103 apply(drule_tac x="-p" in meta_spec)

   104 apply(drule_tac x="x" in meta_spec)

   105 apply(drule_tac x="xa" in meta_spec)

   106 apply simp

   107 apply (erule Pair_pre_graph.induct)

   108 apply (simp_all add: Pair_pre_graph.intros)[3]

   109   apply (case_tac x)

   110   apply clarify

   111   apply (simp add: symmetric[OF atomize_conjL])

   112   apply (rule_tac y="c" and c="(ab, ba)" in lam.strong_exhaust)

   113   apply (simp_all add: lam.distinct symmetric[OF atomize_conjL] lam.eq_iff Abs1_eq_iff fresh_star_def)

   114   apply auto[1]

   115   apply (simp_all add: fresh_Pair lam.fresh fresh_at_base)

   116   apply (rule swap_fresh_fresh[symmetric])

   117   prefer 3

   118   apply (rule swap_fresh_fresh[symmetric])

   119   apply simp_all

   120   done

   121 

   122 termination

   123   by (relation "measure (\<lambda>(t,_). size t)")

   124      (simp_all add: lam.size)

   125 

   126 consts cx :: name

   127 

   128 fun

   129   Pair where

   130   "(Pair M N) = (Pair_pre M N (Lam [cx]. Var cx))"

   131 

   132 lemma Pair : "atom z \<sharp> (M, N) \<Longrightarrow> Pair M N = (Lam [z]. App (App (Var z) M) N)"

   133   apply simp

   134   apply (subgoal_tac "Lam [cx]. Var cx = Lam[z]. Var z")

   135   apply simp

   136   apply (auto simp add: lam.eq_iff Abs1_eq_iff)

   137   by (metis Rep_name_inject atom_name_def fresh_at_base lam.fresh(1))

   138 

   139 

   140 definition Lam_I_pre : "\<II> \<equiv> Lam[cx]. Var cx"

   141 

   142 lemma Lam_I : "\<II> = Lam[x]. Var x"

   143   by (simp add: Lam_I_pre lam.eq_iff Abs1_eq_iff lam.fresh supp_at_base)

   144      (metis Rep_name_inverse atom_name_def fresh_at_base)

   145 

   146 definition c1 :: name where "c1 \<equiv> Abs_name (Atom (Sort ''Lambda.name'' []) 1)"

   147 definition c2 :: name where "c2 \<equiv> Abs_name (Atom (Sort ''Lambda.name'' []) 2)"

   148 

   149 lemma c1_c2[simp]:

   150   "c1 \<noteq> c2"

   151   unfolding c1_def c2_def

   152   by (simp add: Abs_name_inject)

   153 

   154 definition Lam_F_pre : "\<FF> \<equiv> Lam[c1]. Lam[c2]. Var c2"

   155 lemma Lam_F : "\<FF> = Lam[x]. Lam[y]. Var y"

   156   by (simp add: Lam_F_pre lam.eq_iff Abs1_eq_iff lam.fresh supp_at_base)

   157      (metis Rep_name_inverse atom_name_def fresh_at_base)