# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1308881698 -32400
# Node ID 59be22e05a0ac7b4013cf07e63f9e48223d68160
# Parent  65efa1c7563cbeaeb2ba3fc008e44ca2c0c06d2b
The examples in Lambda_add can be defined by nominal_function directly

diff -r 65efa1c7563c -r 59be22e05a0a Nominal/Ex/Lambda_add.thy
--- a/Nominal/Ex/Lambda_add.thy	Fri Jun 24 11:03:53 2011 +0900
+++ b/Nominal/Ex/Lambda_add.thy	Fri Jun 24 11:14:58 2011 +0900
@@ -8,155 +8,16 @@
   "fv \<noteq> x \<Longrightarrow> addlam (Var x) = Lam [fv]. App (Var fv) (Var x)"
 | "addlam (App t1 t2) = App t1 t2"
 | "addlam (Lam [x]. t) = Lam [x].t"
-oops
-
-
-nominal_primrec
-  addlam_pre :: "lam \<Rightarrow> lam \<Rightarrow> lam"
-where
-  "fv \<noteq> x \<Longrightarrow> addlam_pre (Var x) (Lam [fv].it) = Lam [fv]. App (Var fv) (Var x)"
-| "addlam_pre (Var x) (App t1 t2) = Var x"
-| "addlam_pre (Var x) (Var v) = Var x"
-| "addlam_pre (App t1 t2) it = App t1 t2"
-| "addlam_pre (Lam [x]. t) it = Lam [x].t"
-apply (subgoal_tac "\<And>p a x. addlam_pre_graph a x \<Longrightarrow> addlam_pre_graph (p \<bullet> a) (p \<bullet> x)")
-apply (simp add: eqvt_def)
-apply (intro allI)
-apply(simp add: permute_fun_def)
-apply(rule ext)
-apply(rule ext)
-apply(simp add: permute_bool_def)
-apply rule
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="- p \<bullet> x" in meta_spec)
-apply(drule_tac x="- p \<bullet> xa" in meta_spec)
-apply simp
-apply(drule_tac x="-p" in meta_spec)
-apply(drule_tac x="x" in meta_spec)
-apply(drule_tac x="xa" in meta_spec)
-apply simp
-apply (erule addlam_pre_graph.induct)
-apply (simp_all add: addlam_pre_graph.intros)
-apply (simp_all add:lam.distinct)
-apply clarify
-apply simp
-apply (rule_tac y="a" in lam.exhaust)
-apply(auto simp add: lam.distinct lam.eq_iff)
-prefer 2 apply blast
-prefer 2 apply blast
-apply (rule_tac y="b" and c="name" in lam.strong_exhaust)
-apply(auto simp add: lam.distinct lam.eq_iff)[3]
-apply blast
-apply(drule_tac x="namea" in meta_spec)
-apply(drule_tac x="name" in meta_spec)
-apply(drule_tac x="lam" in meta_spec)
-apply (auto simp add: fresh_star_def atom_name_def fresh_at_base)[1]
-apply (auto simp add: lam.eq_iff Abs1_eq_iff fresh_def lam.supp supp_at_base)
-done
-
-termination
-  by (relation "measure (\<lambda>(t,_). size t)")
-     (simp_all add: lam.size)
-
-function
-  addlam :: "lam \<Rightarrow> lam"
-where
-  "addlam (Var x) = addlam_pre (Var x) (Lam [x]. (Var x))"
-| "addlam (App t1 t2) = App t1 t2"
-| "addlam (Lam [x]. t) = Lam [x].t"
-apply (simp_all add:lam.distinct)
-apply (rule_tac y="x" in lam.exhaust)
-apply auto
-apply (simp add:lam.eq_iff)
-done
-
-termination
-  by (relation "measure (\<lambda>(t). size t)")
-     (simp_all add: lam.size)
-
-lemma addlam':
-  "fv \<noteq> x \<Longrightarrow> addlam (Var x) = Lam [fv]. App (Var fv) (Var x)"
-  apply simp
-  apply (subgoal_tac "Lam [x]. Var x = Lam [fv]. Var fv")
-  apply simp
-  apply (simp add: lam.eq_iff Abs1_eq_iff lam.supp fresh_def supp_at_base)
+  unfolding addlam_graph_def eqvt_def
+  apply perm_simp
+  apply auto
+  apply (case_tac x rule: lam.exhaust)
+  apply auto
+  apply (rule_tac x="name" and ?'a="name" in obtain_fresh)
+  apply (simp add: fresh_at_base)
+  apply (simp add: Abs1_eq_iff lam.fresh fresh_at_base)
   done
 
-nominal_primrec
-  Pair_pre
-where
-  "atom z \<sharp> (M, N) \<Longrightarrow> (Pair_pre M N) (Lam [z]. _) = (Lam [z]. App (App (Var z) M) N)"
-| "(Pair_pre M N) (App l r) = (App l r)"
-| "(Pair_pre M N) (Var v) = (Var v)"
-apply (subgoal_tac "\<And>p a x. Pair_pre_graph a x \<Longrightarrow> Pair_pre_graph (p \<bullet> a) (p \<bullet> x)")
-apply (simp add: eqvt_def)
-apply (intro allI)
-apply(simp add: permute_fun_def)
-apply(rule ext)
-apply(rule ext)
-apply(simp add: permute_bool_def)
-apply rule
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="- p \<bullet> x" in meta_spec)
-apply(drule_tac x="- p \<bullet> xa" in meta_spec)
-apply simp
-apply(drule_tac x="-p" in meta_spec)
-apply(drule_tac x="x" in meta_spec)
-apply(drule_tac x="xa" in meta_spec)
-apply simp
-apply (erule Pair_pre_graph.induct)
-apply (simp_all add: Pair_pre_graph.intros)[3]
-  apply (case_tac x)
-  apply clarify
-  apply (simp add: symmetric[OF atomize_conjL])
-  apply (rule_tac y="c" and c="(ab, ba)" in lam.strong_exhaust)
-  apply (simp_all add: lam.distinct symmetric[OF atomize_conjL] lam.eq_iff Abs1_eq_iff fresh_star_def)
-  apply auto[1]
-  apply (simp_all add: fresh_Pair lam.fresh fresh_at_base)
-  apply (rule swap_fresh_fresh[symmetric])
-  prefer 3
-  apply (rule swap_fresh_fresh[symmetric])
-  apply simp_all
-  done
-
-termination
-  by (relation "measure (\<lambda>(t,_). size t)")
-     (simp_all add: lam.size)
-
-consts cx :: name
-
-fun
-  Pair where
-  "(Pair M N) = (Pair_pre M N (Lam [cx]. Var cx))"
-
-lemma Pair : "atom z \<sharp> (M, N) \<Longrightarrow> Pair M N = (Lam [z]. App (App (Var z) M) N)"
-  apply simp
-  apply (subgoal_tac "Lam [cx]. Var cx = Lam[z]. Var z")
-  apply simp
-  apply (auto simp add: lam.eq_iff Abs1_eq_iff)
-  by (metis Rep_name_inject atom_name_def fresh_at_base lam.fresh(1))
-
-
-definition Lam_I_pre : "\<II> \<equiv> Lam[cx]. Var cx"
-
-lemma Lam_I : "\<II> = Lam[x]. Var x"
-  by (simp add: Lam_I_pre lam.eq_iff Abs1_eq_iff lam.fresh supp_at_base)
-     (metis Rep_name_inverse atom_name_def fresh_at_base)
-
-definition c1 :: name where "c1 \<equiv> Abs_name (Atom (Sort ''Lambda.name'' []) 1)"
-definition c2 :: name where "c2 \<equiv> Abs_name (Atom (Sort ''Lambda.name'' []) 2)"
-
-lemma c1_c2[simp]:
-  "c1 \<noteq> c2"
-  unfolding c1_def c2_def
-  by (simp add: Abs_name_inject)
-
-definition Lam_F_pre : "\<FF> \<equiv> Lam[c1]. Lam[c2]. Var c2"
-lemma Lam_F : "\<FF> = Lam[x]. Lam[y]. Var y"
-  by (simp add: Lam_F_pre lam.eq_iff Abs1_eq_iff lam.fresh supp_at_base)
-     (metis Rep_name_inverse atom_name_def fresh_at_base)
+termination by lexicographic_order
 
 end
-
-
-