--- 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