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. \a \ s. atom x \ 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. \a \ supp s. atom x \ a)" + +definition + "match_Lam (S :: 'a :: fs) t = (if (\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)) \ 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 \ ((S :: 'a :: fs), Lam n s) \ 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 \ (new (S, (Lam n s)))) \ 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 \ (fv_lam_raw t - {atom n})) in Some (z, (n \ z) \ 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) \ 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) \ x = Lam z s \ atom z \ S" apply (induct x rule: lam.induct) apply (simp_all add: match_Lam_simps) + apply (thin_tac "match_Lam S lam = Some (z, s) \ lam = Lam z s \ atom z \ S") + apply (simp add: match_Lam_def) + apply (subgoal_tac "\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) \ lam = Lam z s \ atom z \ S") + apply (thin_tac "\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 \ (new (S, Lam name lam))) \ lam" in subst) + defer apply (simp add: lam.eq_iff) - apply (rule_tac x="(name \ z)" in exI) + apply (rule_tac x="(name \ (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 \ new (S \ (fv_lam lam - {atom name}))) \ lam = s") - apply (simp only: new_def) - apply (subgoal_tac "\a \ S. atom z \ 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 \ if n = v then s else Var n | None \ case match_App t of Some (l, r) \ App (subst v s l) (subst v s r) | None \ - case match_Lam (supp (v,s)) t of Some (n, t) \ Lam n (subst v s t) | None \ undefined)" + case match_Lam (v,s) t of Some (n, t) \ Lam n (subst v s t) | None \ undefined)" by pat_completeness auto termination apply (relation "measure (\(_, _, 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 \ new ((v, s), Lam n t')) \ 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 \ n) (p \ t')" and s="Lam (new ((p \ v, p \ s), Lam (p \ n) (p \ t'))) (((p \ n) \ new ((p \ v, p \ s), Lam (p \ n) (p \ t'))) \ 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 \ new ((y, s), Lam x t)) \ t)" in subst) + defer + apply (subst match_Lam_simps) + defer apply (simp only: option.simps) apply (simp only: prod.simps) sorry