theory Ex2+
−
imports "../NewParser"+
−
begin+
−
+
−
text {* example 2 *}+
−
+
−
atom_decl name+
−
+
−
nominal_datatype trm =+
−
  Var "name"+
−
| App "trm" "trm"+
−
| Lam x::"name" t::"trm"          bind_set x in t+
−
| Let p::"pat" "trm" t::"trm"     bind "f p" in t+
−
and pat =+
−
  PN+
−
| PS "name"+
−
| PD "name" "name"+
−
binder+
−
  f::"pat \<Rightarrow> atom list"+
−
where+
−
  "f PN = []"+
−
| "f (PS x) = [atom x]"+
−
| "f (PD x y) = [atom x, atom y]"+
−
+
−
thm trm_pat.bn+
−
thm trm_pat.perm+
−
thm trm_pat.induct+
−
thm trm_pat.distinct+
−
thm trm_pat.fv[simplified trm_pat.supp(1-2)]+
−
+
−
lemma lets_overlap1:+
−
  "atom a \<noteq> atom b \<Longrightarrow> Let (PD a a) x y \<noteq> Let (PD a b) x y"+
−
  by (simp add: trm_pat.eq_iff alphas)+
−
+
−
lemma lets_overlap2:+
−
  "atom a \<notin> supp y \<Longrightarrow> atom b \<notin> supp y \<Longrightarrow> Let (PD a a) x y = Let (PD b b) x y"+
−
  apply (simp add: trm_pat.eq_iff alphas trm_pat.supp)+
−
  apply (rule_tac x="(a\<leftrightarrow>b)" in exI)+
−
  apply (simp add: eqvts)+
−
  apply (rule conjI)+
−
  prefer 2+
−
  apply (rule Nominal2_Supp.supp_perm_eq)+
−
  apply (unfold fresh_star_def)+
−
  apply (unfold fresh_def)+
−
  apply (unfold flip_def)+
−
  apply (simp_all add: supp_swap)+
−
  apply auto+
−
  done+
−
+
−
end+
−
+
−
+
−
+
−