src/HOL/Nominal/Examples/Compile.thy

 (* $Id$ *)
 
 (* A challenge suggested by Adam Chlipala *)
 
 theory Compile
-imports "Nominal"
+imports "../Nominal"
 begin
 
 atom_decl name 
 
 nominal_datatype data = DNat

 | t7[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : DataI(NatI); \<Gamma> I\<turnstile> e2 : DataI(NatI)\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> e1\<mapsto>e2 : DataI(OneI)"
 | t8[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : DataI(NatI); \<Gamma> I\<turnstile> e2 : \<tau>\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> e1;;e2 : \<tau>"
 | t9[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e: DataI(NatI); \<Gamma> I\<turnstile> e1 : \<tau>; \<Gamma> I\<turnstile> e2 : \<tau>\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> Iif e e1 e2 : \<tau>"
 
 text {* capture-avoiding substitution *}
-
-lemma perm_if:
-  fixes pi::"'a prm"
-  shows "pi\<bullet>(if b then c1 else c2) = (if (pi\<bullet>b) then (pi\<bullet>c1) else (pi\<bullet>c2))"
-apply(simp add: perm_fun_def)
-done
-
-lemma eq_eqvt:
-  fixes pi::"name prm"
-  and   x::"'a::pt_name"
-  shows "pi\<bullet>(x=y) = ((pi\<bullet>x)=(pi\<bullet>y))"
-  apply(simp add: perm_bool perm_bij)
-  done
 
 consts
   subst :: "'a \<Rightarrow> name \<Rightarrow> 'a \<Rightarrow> 'a"  ("_[_::=_]" [100,100,100] 100)
 
 nominal_primrec

   "(InL e)[y::=t'] = InL (e[y::=t'])"
   "(InR e)[y::=t'] = InR (e[y::=t'])"
   "\<lbrakk>z\<noteq>x; x\<sharp>y; x\<sharp>e; x\<sharp>e2; z\<sharp>y; z\<sharp>e; z\<sharp>e1; x\<sharp>t'; z\<sharp>t'\<rbrakk> \<Longrightarrow>
      (Case e of inl x \<rightarrow> e1 | inr z \<rightarrow> e2)[y::=t'] =
        (Case (e[y::=t']) of inl x \<rightarrow> (e1[y::=t']) | inr z \<rightarrow> (e2[y::=t']))"
-  apply (finite_guess add: fs_name1 perm_if eq_eqvt)
-  apply (finite_guess add: fs_name1)
-  apply (finite_guess add: fs_name1)
-  apply (finite_guess add: fs_name1)
-  apply (finite_guess add: fs_name1)
-  apply (finite_guess add: fs_name1)
-  apply (finite_guess add: fs_name1)
-  apply (finite_guess add: fs_name1)
-  apply (finite_guess add: fs_name1)
-  apply (finite_guess only: fs_name1)
-  apply perm_simp
-  apply (simp add: supp_unit)
-  apply (rule TrueI)+
-  apply (simp add: abs_fresh)
-  apply (simp_all add: abs_fresh)
-  apply (fresh_guess add: fs_name1 perm_if eq_eqvt)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess only: fs_name1)
-  apply perm_simp
-  apply (fresh_guess add: fs_name1 perm_if eq_eqvt)
-  apply (fresh_guess add: fs_name1 perm_if eq_eqvt)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess only: fs_name1)
-  apply perm_simp
-  apply (fresh_guess only: fs_name1)
-  apply perm_simp
+  apply(finite_guess)+
+  apply(rule TrueI)+
+  apply(simp add: abs_fresh)+
+  apply(fresh_guess)+
   done
 
 nominal_primrec (Isubst)
   "(IVar x)[y::=t'] = (if x=y then t' else (IVar x))"
   "(IApp t1 t2)[y::=t'] = IApp (t1[y::=t']) (t2[y::=t'])"

   "(ISucc e)[y::=t'] = ISucc (e[y::=t'])"
   "(IAss e1 e2)[y::=t'] = IAss (e1[y::=t']) (e2[y::=t'])"
   "(IRef e)[y::=t'] = IRef (e[y::=t'])"
   "(ISeq e1 e2)[y::=t'] = ISeq (e1[y::=t']) (e2[y::=t'])"
   "(Iif e e1 e2)[y::=t'] = Iif (e[y::=t']) (e1[y::=t']) (e2[y::=t'])"
-  apply (finite_guess add: fs_name1 perm_if eq_eqvt)
-  apply (finite_guess add: fs_name1)
-  apply (finite_guess add: fs_name1)
-  apply (finite_guess add: fs_name1)
-  apply (finite_guess add: fs_name1)
-  apply (finite_guess add: fs_name1)
-  apply (finite_guess add: fs_name1)
-  apply (finite_guess add: fs_name1)
-  apply (finite_guess add: fs_name1)
-  apply (finite_guess only: fs_name1)
-  apply perm_simp
-  apply (simp add: supp_unit)
-  apply (rule TrueI)+
-  apply (simp add: abs_fresh)
-  apply (fresh_guess add: fs_name1 perm_if eq_eqvt)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess only: fs_name1)
-  apply perm_simp
-  done
-
-lemma Isubst_eqvt:
+  apply(finite_guess)+
+  apply(rule TrueI)+
+  apply(simp add: abs_fresh)+
+  apply(fresh_guess)+
+  done
+
+lemma Isubst_eqvt[eqvt]:
   fixes pi::"name prm"
   and   t1::"trmI"
   and   t2::"trmI"
   and   x::"name"
   shows "pi\<bullet>(t1[x::=t2]) = ((pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)])"
   apply (nominal_induct t1 avoiding: x t2 rule: trmI.induct)
-  apply (simp_all add: Isubst.simps perm_if eq_eqvt fresh_bij)
+  apply (simp_all add: Isubst.simps eqvt fresh_bij)
   done
 
 lemma Isubst_supp:
   fixes t1::"trmI"
   and   t2::"trmI"

    trans (Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2) =
        (let v = (trans e) in
         let v1 = (trans e1) in
         let v2 = (trans e2) in 
         Iif (IRef (ISucc v)) (v2[x2::=IRef (ISucc (ISucc v))]) (v1[x1::=IRef (ISucc (ISucc v))]))"
-  apply (finite_guess add: fs_name1)
-  apply (finite_guess add: fs_name1)
-  apply (finite_guess add: fs_name1)
-  apply (finite_guess add: fs_name1)
-  apply (finite_guess add: fs_name1 Let_def perm_nat_def)
-  apply (finite_guess add: fs_name1)
-  apply (finite_guess add: fs_name1)
-  apply (finite_guess add: fs_name1 Let_def perm_nat_def)
-  apply (finite_guess add: fs_name1 Let_def perm_nat_def)
-  apply (finite_guess add: fs_name1 Let_def Isubst_eqvt)
-  apply (simp add: supp_unit)
-  apply (rule TrueI)+
-  apply (simp add: abs_fresh)
-  apply (simp_all add: abs_fresh Isubst_fresh)
-  apply (fresh_guess add: fs_name1 perm_if eq_eqvt)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1 Let_def perm_nat_def)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1 Let_def perm_nat_def)
-  apply (fresh_guess add: fs_name1 Let_def perm_nat_def)
-  apply (fresh_guess add: fs_name1 Let_def Isubst_eqvt)
-  apply (fresh_guess add: fs_name1 perm_if eq_eqvt)
-  apply (fresh_guess add: fs_name1 perm_if eq_eqvt)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1 Let_def perm_nat_def)
-  apply (fresh_guess add: fs_name1 Let_def perm_nat_def)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1)
-  apply (fresh_guess add: fs_name1 Let_def perm_nat_def)
-  apply (fresh_guess add: fs_name1 Let_def perm_nat_def)
-  apply (fresh_guess add: fs_name1 Let_def perm_nat_def)
-  apply (fresh_guess add: fs_name1 Let_def perm_nat_def)
-  apply (fresh_guess add: fs_name1 Let_def Isubst_eqvt)
-  apply (fresh_guess add: fs_name1 Let_def Isubst_eqvt)
+  apply(finite_guess add: Let_def)+
+  apply(rule TrueI)+
+  apply(simp add: abs_fresh Isubst_fresh)+
+  apply(fresh_guess add: Let_def)+
   done
 
 consts trans_type :: "ty \<Rightarrow> tyI"
 
 nominal_primrec