76 nominal_primrec

    77   Pair_pre

    78 where

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

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

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

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

    83 apply (simp add: eqvt_def)

    84 apply (intro allI)

    85 apply(simp add: permute_fun_def)

    86 apply(rule ext)

    87 apply(rule ext)

    88 apply(simp add: permute_bool_def)

    89 apply rule

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

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

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

    93 apply simp

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

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

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

    97 apply simp

    98 apply (erule Pair_pre_graph.induct)

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

   100   apply (case_tac x)

   101   apply clarify

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

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

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

   105   apply auto[1]

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

   107   apply (rule swap_fresh_fresh[symmetric])

   108   prefer 3

   109   apply (rule swap_fresh_fresh[symmetric])

   110   apply simp_all

   111   done

   112 

   113 termination

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

   115      (simp_all add: lam.size)

   116 

   117 consts cx :: name

   118 

   119 fun

   120   Pair where

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

   122 

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

   124   apply simp

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

   126   apply simp

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

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

   129 

   130 

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

   132 

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

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

   135      (metis Rep_name_inverse atom_name_def fresh_at_base)

   136 

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

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

   139 

   140 lemma c1_c2[simp]:

   141   "c1 \<noteq> c2"

   142   unfolding c1_def c2_def

   143   by (simp add: Abs_name_inject)

   144 

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

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

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

   148      (metis Rep_name_inverse atom_name_def fresh_at_base)

   149