# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1309902440 -7200
# Node ID d75b3d8529e7691e91466b91c36a8a12adec1f07
# Parent  0911cb7bf696b703ae8121e295b5cd83bed1802a
added some relatively simple examples from paper by Norrish

diff -r 0911cb7bf696 -r d75b3d8529e7 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Tue Jul 05 18:42:34 2011 +0200
+++ b/Nominal/Ex/Lambda.thy	Tue Jul 05 23:47:20 2011 +0200
@@ -27,12 +27,181 @@
 
 method_setup test = {* test *} {* test *}
 
+section {* Simple examples from Norrish 2004 *}
+
+nominal_primrec 
+  is_app :: "lam \<Rightarrow> bool"
+where
+  "is_app (Var x) = False"
+| "is_app (App t1 t2) = True"
+| "is_app (Lam [x]. t) = False"
+apply(simp add: eqvt_def is_app_graph_def)
+apply (rule, perm_simp, rule)
+apply(rule TrueI)
+apply(rule_tac y="x" in lam.exhaust)
+apply(auto)[3]
+apply(all_trivials)
+done
+
+termination by lexicographic_order
+
+lemma [eqvt]:
+  shows "(p \<bullet> (is_app t)) = is_app (p \<bullet> t)"
+apply(induct t rule: lam.induct)
+apply(simp_all add: permute_bool_def)
+done
+
+nominal_primrec 
+  rator :: "lam \<Rightarrow> lam option"
+where
+  "rator (Var x) = None"
+| "rator (App t1 t2) = Some t1"
+| "rator (Lam [x]. t) = None"
+apply(simp add: eqvt_def rator_graph_def)
+apply (rule, perm_simp, rule)
+apply(rule TrueI)
+apply(rule_tac y="x" in lam.exhaust)
+apply(auto)[3]
+apply(simp_all)
+done
+
+termination by lexicographic_order
+
+lemma [eqvt]:
+  shows "(p \<bullet> (rator t)) = rator (p \<bullet> t)"
+apply(induct t rule: lam.induct)
+apply(simp_all)
+done
+
+nominal_primrec 
+  rand :: "lam \<Rightarrow> lam option"
+where
+  "rand (Var x) = None"
+| "rand (App t1 t2) = Some t2"
+| "rand (Lam [x]. t) = None"
+apply(simp add: eqvt_def rand_graph_def)
+apply (rule, perm_simp, rule)
+apply(rule TrueI)
+apply(rule_tac y="x" in lam.exhaust)
+apply(auto)[3]
+apply(simp_all)
+done
+
+termination by lexicographic_order
+
+lemma [eqvt]:
+  shows "(p \<bullet> (rand t)) = rand (p \<bullet> t)"
+apply(induct t rule: lam.induct)
+apply(simp_all)
+done
+
+nominal_primrec 
+  is_eta_nf :: "lam \<Rightarrow> bool"
+where
+  "is_eta_nf (Var x) = True"
+| "is_eta_nf (App t1 t2) = (is_eta_nf t1 \<and> is_eta_nf t2)"
+| "is_eta_nf (Lam [x]. t) = (is_eta_nf t \<and> 
+                             ((is_app t \<and> rand t = Some (Var x)) \<longrightarrow> atom x \<in> supp (rator t)))"
+apply(simp add: eqvt_def is_eta_nf_graph_def)
+apply (rule, perm_simp, rule)
+apply(rule TrueI)
+apply(rule_tac y="x" in lam.exhaust)
+apply(auto)[3]
+apply(simp_all)
+apply(erule_tac c="()" in Abs_lst1_fcb2')
+apply(simp_all add: pure_fresh fresh_star_def)[3]
+apply(simp add: eqvt_at_def conj_eqvt)
+apply(perm_simp)
+apply(rule refl)
+apply(simp add: eqvt_at_def conj_eqvt)
+apply(perm_simp)
+apply(rule refl)
+done
+
+termination by lexicographic_order
+
+nominal_datatype path = Left | Right | In
+
+section {* Paths to a free variables *} 
+
+instance path :: pure
+apply(default)
+apply(induct_tac "x::path" rule: path.induct)
+apply(simp_all)
+done
+
+nominal_primrec 
+  var_pos :: "name \<Rightarrow> lam \<Rightarrow> (path list) set"
+where
+  "var_pos y (Var x) = (if y = x then {[]} else {})"
+| "var_pos y (App t1 t2) = (Cons Left ` (var_pos y t1)) \<union> (Cons Right ` (var_pos y t2))"
+| "atom x \<sharp> y \<Longrightarrow> var_pos y (Lam [x]. t) = (Cons In ` (var_pos y t))"
+apply(simp add: eqvt_def var_pos_graph_def)
+apply (rule, perm_simp, rule)
+apply(rule TrueI)
+apply(case_tac x)
+apply(rule_tac y="b" and c="a" in lam.strong_exhaust)
+apply(auto simp add: fresh_star_def)[3]
+apply(simp_all)
+apply(erule conjE)+
+apply(erule_tac Abs_lst1_fcb2)
+apply(simp add: pure_fresh)
+apply(simp add: fresh_star_def)
+apply(simp add: eqvt_at_def image_eqvt perm_supp_eq)
+apply(perm_simp)
+apply(rule refl)
+apply(simp add: eqvt_at_def image_eqvt perm_supp_eq)
+apply(perm_simp)
+apply(rule refl)
+done
+
+termination by lexicographic_order
+
+lemma var_pos1:
+  assumes "atom y \<notin> supp t"
+  shows "var_pos y t = {}"
+using assms
+apply(induct t rule: var_pos.induct)
+apply(simp_all add: lam.supp supp_at_base fresh_at_base)
+done
+
+lemma var_pos2:
+  shows "var_pos y (Lam [y].t) = {}"
+apply(rule var_pos1)
+apply(simp add: lam.supp)
+done
+
+
+text {* strange substitution operation *}
+
+nominal_primrec
+  subst' :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::== _]" [90, 90, 90] 90)
+where
+  "(Var x)[y ::== s] = (if x = y then s else (Var x))"
+| "(App t1 t2)[y ::== s] = App (t1[y ::== s]) (t2[y ::== s])"
+| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::== s] = Lam [x].(t[y ::== (App (Var y) s)])"
+  apply(simp add: eqvt_def subst'_graph_def)
+  apply (rule, perm_simp, rule)
+  apply(rule TrueI)
+  apply(case_tac x)
+  apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
+  apply(auto simp add: fresh_star_def)[3]
+  apply(simp_all)
+  apply(erule conjE)+
+  apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
+  apply(simp_all add: Abs_fresh_iff)
+  apply(simp add: fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+done
+
+termination by lexicographic_order
+
+
 section {* free name function *}
 
 text {* first returns an atom list *}
 
-ML Thm.implies_intr
-
 nominal_primrec 
   frees_lst :: "lam \<Rightarrow> atom list"
 where