
diff -r fd5eec72c3f5 -r 477293d841e8 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Fri May 21 11:55:22 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Fri May 21 17:17:51 2010 +0200
@@ -474,9 +474,6 @@
 
 (* Substitution *)
 
-definition new where
-  "new s = (THE x. \<forall>a \<in> s. atom x \<noteq> a)"
-
 primrec match_Var_raw where
   "match_Var_raw (Var_raw x) = Some x"
 | "match_Var_raw (App_raw x y) = None"
@@ -512,7 +509,41 @@
 
 lemmas match_App_simps = match_App_raw.simps[quot_lifted]
 
-primrec match_Lam_raw where
+definition new where
+  "new (s :: 'a :: fs) = (THE x. \<forall>a \<in> supp s. atom x \<noteq> a)"
+
+definition
+  "match_Lam (S :: 'a :: fs) t = (if (\<exists>n s. (t = Lam n s)) then
+    (let z = new (S, t) in Some (z, THE s. t = Lam z s)) else None)"
+
+lemma lam_half_inj: "(Lam z s = Lam z sa) = (s = sa)"
+  apply auto
+  apply (simp only: lam.eq_iff alphas)
+  apply clarify
+  apply (simp add: eqvts)
+  sorry
+
+lemma match_Lam_simps:
+  "match_Lam S (Var n) = None"
+  "match_Lam S (App l r) = None"
+  "z = new (S, (Lam z s)) \<Longrightarrow> match_Lam S (Lam z s) = Some (z, s)"
+  apply (simp_all add: match_Lam_def)
+  apply (simp add: lam_half_inj)
+  apply auto
+  done
+
+(*
+lemma match_Lam_simps2:
+  "atom n \<sharp> ((S :: 'a :: fs), Lam n s) \<Longrightarrow> match_Lam S (Lam n s) = Some (n, s)"
+  apply (rule_tac t="Lam n s"
+              and s="Lam (new (S, (Lam n s))) ((n \<leftrightarrow> (new (S, (Lam n s)))) \<bullet> s)" in subst)
+  defer
+  apply (subst match_Lam_simps(3))
+  defer
+  apply simp
+*)
+
+(*primrec match_Lam_raw where
   "match_Lam_raw (S :: atom set) (Var_raw x) = None"
 | "match_Lam_raw S (App_raw x y) = None"
 | "match_Lam_raw S (Lam_raw n t) = (let z = new (S \<union> (fv_lam_raw t - {atom n})) in Some (z, (n \<leftrightarrow> z) \<bullet> t))"
@@ -579,6 +610,7 @@
   qed
 
 lemmas match_Lam_simps = match_Lam_raw.simps[quot_lifted]
+*)
 
 lemma app_some: "match_App x = Some (a, b) \<Longrightarrow> x = App a b"
 by (induct x rule: lam.induct) (simp_all add: match_App_simps)
@@ -586,30 +618,30 @@
 lemma lam_some: "match_Lam S x = Some (z, s) \<Longrightarrow> x = Lam z s \<and> atom z \<sharp> S"
   apply (induct x rule: lam.induct)
   apply (simp_all add: match_Lam_simps)
+  apply (thin_tac "match_Lam S lam = Some (z, s) \<Longrightarrow> lam = Lam z s \<and> atom z \<sharp> S")
+  apply (simp add: match_Lam_def)
+  apply (subgoal_tac "\<exists>n s. Lam name lam = Lam n s")
+  prefer 2
+  apply auto[1]
   apply (simp add: Let_def)
-  apply (erule conjE)
-  apply (thin_tac "match_Lam S lam = Some (z, s) \<Longrightarrow> lam = Lam z s \<and> atom z \<sharp> S")
+  apply (thin_tac "\<exists>n s. Lam name lam = Lam n s")
+  apply clarify
   apply (rule conjI)
+  apply (rule_tac t="THE s. Lam name lam = Lam (new (S, Lam name lam)) s" and
+                  s="(name \<leftrightarrow> (new (S, Lam name lam))) \<bullet> lam" in subst)
+  defer
   apply (simp add: lam.eq_iff)
-  apply (rule_tac x="(name \<leftrightarrow> z)" in exI)
+  apply (rule_tac x="(name \<leftrightarrow> (new (S, Lam name lam)))" in exI)
   apply (simp add: alphas)
   apply (simp add: eqvts)
-  apply (simp only: lam.fv(3)[symmetric])
-  apply (subgoal_tac "Lam name lam = Lam z s")
-  apply (simp del: lam.fv)
-  prefer 3
-  apply (thin_tac "(name \<leftrightarrow> new (S \<union> (fv_lam lam - {atom name}))) \<bullet> lam = s")
-  apply (simp only: new_def)
-  apply (subgoal_tac "\<forall>a \<in> S. atom z \<noteq> a")
-  apply (simp only: fresh_def)
-  (*thm supp_finite_atom_fset*)
+  apply (rule conjI)
   sorry
 
 function subst where
 "subst v s t = (
   case match_Var t of Some n \<Rightarrow> if n = v then s else Var n | None \<Rightarrow>
   case match_App t of Some (l, r) \<Rightarrow> App (subst v s l) (subst v s r) | None \<Rightarrow>
-  case match_Lam (supp (v,s)) t of Some (n, t) \<Rightarrow> Lam n (subst v s t) | None \<Rightarrow> undefined)"
+  case match_Lam (v,s) t of Some (n, t) \<Rightarrow> Lam n (subst v s t) | None \<Rightarrow> undefined)"
 by pat_completeness auto
 
 termination apply (relation "measure (\<lambda>(_, _, t). size t)")
@@ -646,7 +678,7 @@
         apply (simp only: lam.perm)
         apply (subst (3) subst.simps)
         apply (subst match_Var_simps)
-       apply (simp only: option.cases)
+        apply (simp only: option.cases)
         apply (subst match_App_simps)
         apply (simp only: option.cases)
         apply (simp only: prod.cases)
@@ -671,8 +703,10 @@
         apply (simp only: option.cases)
         apply (subst match_App_simps)
         apply (simp only: option.cases)
+        apply (rule_tac t="Lam n t'" and s="Lam (new ((v, s), Lam n t')) ((n \<leftrightarrow> new ((v, s), Lam n t')) \<bullet> t')" in subst)
+        defer
         apply (subst match_Lam_simps)
-        apply (simp only: Let_def)
+        defer
         apply (simp only: option.cases)
         apply (simp only: prod.cases)
         apply (subst (2) subst.simps)
@@ -680,17 +714,18 @@
         apply (simp only: option.cases)
         apply (subst match_App_simps)
         apply (simp only: option.cases)
+        apply (rule_tac t="Lam (p \<bullet> n) (p \<bullet> t')" and s="Lam (new ((p \<bullet> v, p \<bullet> s), Lam (p \<bullet> n) (p \<bullet> t'))) (((p \<bullet> n) \<leftrightarrow> new ((p \<bullet> v, p \<bullet> s), Lam (p \<bullet> n) (p \<bullet> t'))) \<bullet> t')" in subst)
+        defer
         apply (subst match_Lam_simps)
-        apply (simp only: Let_def)
+        defer
         apply (simp only: option.cases)
         apply (simp only: prod.cases)
         apply (simp only: lam.perm)
-        apply (simp only: lam.eq_iff)
+        thm 1(1)
         sorry
     qed
   qed
 
-
 lemma subst_proper_eqs:
   "subst y s (Var x) = (if x = y then s else (Var x))"
   "subst y s (App l r) = App (subst y s l) (subst y s r)"
@@ -705,11 +740,14 @@
   apply (simp only: match_Var_simps)
   apply (simp only: option.simps)
   apply (subst subst.simps)
-  apply (simp only: match_Lam_simps)
   apply (simp only: match_Var_simps)
+  apply (simp only: option.simps)
   apply (simp only: match_App_simps)
   apply (simp only: option.simps)
-  apply (simp only: Let_def)
+  apply (rule_tac t="Lam x t" and s="Lam (new ((y, s), Lam x t)) ((x \<leftrightarrow> new ((y, s), Lam x t)) \<bullet> t)" in subst)
+  defer
+  apply (subst match_Lam_simps)
+  defer
   apply (simp only: option.simps)
   apply (simp only: prod.simps)
   sorry




