# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1274435722 -7200
# Node ID fd5eec72c3f5b095e4053709d3808650431e5969
# Parent  9697bbf713eccdd60ac062e099a94638a649c896
More on Function-defined subst.

diff -r 9697bbf713ec -r fd5eec72c3f5 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Fri May 21 11:46:47 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Fri May 21 11:55:22 2010 +0200
@@ -521,6 +521,23 @@
   "match_Lam :: (atom set) \<Rightarrow> lam \<Rightarrow> (name \<times> lam) option"
 is match_Lam_raw
 
+lemma swap_fresh:
+  assumes a: "fv_lam_raw t \<sharp>* p"
+  shows "alpha_lam_raw (p \<bullet> t) t"
+  using a apply (induct t)
+  apply (simp add: supp_at_base fresh_star_def)
+  apply (rule alpha_lam_raw.intros)
+  apply (metis Rep_name_inverse atom_eqvt atom_name_def fresh_perm)
+  apply (simp)
+  apply (simp only: fresh_star_union)
+  apply clarify
+  apply (rule alpha_lam_raw.intros)
+  apply simp
+  apply simp
+  apply simp
+  apply (rule alpha_lam_raw.intros)
+  sorry
+
 lemma [quot_respect]:
   "(op = ===> alpha_lam_raw ===> option_rel (prod_rel op = alpha_lam_raw)) match_Lam_raw match_Lam_raw"
   proof (intro fun_relI, clarify)
@@ -551,8 +568,8 @@
       next
         have "atom y \<sharp> p" sorry
         have "fv_lam_raw t \<sharp>* ((x \<leftrightarrow> y) \<bullet> p)" sorry
-        then have "alpha_lam_raw (((x \<leftrightarrow> y) \<bullet> p) \<bullet> t) t" sorry
-        have "alpha_lam_raw (p \<bullet> t) ((x \<leftrightarrow> y) \<bullet> t)" sorry
+        then have "alpha_lam_raw (((x \<leftrightarrow> y) \<bullet> p) \<bullet> t) t" using swap_fresh by auto
+        then have "alpha_lam_raw (p \<bullet> t) ((x \<leftrightarrow> y) \<bullet> t)" sorry
         have "alpha_lam_raw t ((x \<leftrightarrow> y) \<bullet> s)" sorry
         then have "alpha_lam_raw ((x \<leftrightarrow> ?z) \<bullet> t) ((y \<leftrightarrow> ?z) \<bullet> s)" using eqvts(15) sorry
         then show "alpha_lam_raw ((x \<leftrightarrow> new (S \<union> (fv_lam_raw t - {atom x}))) \<bullet> t)
@@ -585,10 +602,8 @@
   apply (simp only: new_def)
   apply (subgoal_tac "\<forall>a \<in> S. atom z \<noteq> a")
   apply (simp only: fresh_def)
-  
-  thm new_def
-  apply simp
-
+  (*thm supp_finite_atom_fset*)
+  sorry
 
 function subst where
 "subst v s t = (
@@ -598,15 +613,13 @@
 by pat_completeness auto
 
 termination apply (relation "measure (\<lambda>(_, _, t). size t)")
-apply auto[1]
-defer
-apply (case_tac a) apply simp
-apply (frule app_some) apply simp
-apply (case_tac a) apply simp
-apply (frule app_some) apply simp
-apply (case_tac a) apply simp
-apply (frule lam_some)
- apply simp
+  apply auto[1]
+  apply (case_tac a) apply simp
+  apply (frule lam_some) apply simp
+  apply (case_tac a) apply simp
+  apply (frule app_some) apply simp
+  apply (case_tac a) apply simp
+  apply (frule app_some) apply simp
 done
 
 lemmas lam_exhaust = lam_raw.exhaust[quot_lifted]
@@ -677,117 +690,30 @@
     qed
   qed
 
-lemma size_no_change: "size (p \<bullet> (t :: lam_raw)) = size t"
-  by (induct t) simp_all
 
-function
-  subst_raw :: "lam_raw \<Rightarrow> name \<Rightarrow> lam_raw \<Rightarrow> lam_raw"
-where
-  "subst_raw (Var_raw x) y s = (if x=y then s else (Var_raw x))"
-| "subst_raw (App_raw l r) y s = App_raw (subst_raw l y s) (subst_raw r y s)"
-| "subst_raw (Lam_raw x t) y s =
-      Lam_raw (new ({atom y} \<union> fv_lam_raw s \<union> fv_lam_raw t - {atom x}))
-       (subst_raw ((x \<leftrightarrow> (new ({atom y} \<union> fv_lam_raw s \<union> fv_lam_raw t - {atom x}))) \<bullet> t) y s)"
-  by (pat_completeness, auto)
-termination
-  apply (relation "measure (\<lambda>(t, y, s). (size t))")
-  apply (auto simp add: size_no_change)
-  done
-
-lemma fv_subst[simp]: "fv_lam_raw (subst_raw t y s) =
-  (if (atom y \<in> fv_lam_raw t) then fv_lam_raw s \<union> (fv_lam_raw t - {atom y}) else fv_lam_raw t)"
-  apply (induct t arbitrary: s)
-  apply (auto simp add: supp_at_base)[1]
-  apply (auto simp add: supp_at_base)[1]
-  apply (simp only: fv_lam_raw.simps)
-  apply simp
-  apply (rule conjI)
-  apply clarify
-  oops
-
-lemma new_eqvt[eqvt]: "p \<bullet> (new s) = new (p \<bullet> s)"
-  oops
-
-lemma subst_var_raw_eqvt[eqvt]: "p \<bullet> (subst_raw t y s) = subst_raw (p \<bullet> t) (p \<bullet> y) (p \<bullet> s)"
-  apply (induct t arbitrary: p y s)
-  apply simp_all
-  apply(perm_simp)
-  oops
-
-lemma subst_id: "alpha_lam_raw (subst_raw x d (Var_raw d)) x"
-  apply (induct x arbitrary: d)
-  apply (simp_all add: alpha_lam_raw.intros)
-  apply (rule alpha_lam_raw.intros)
-  apply (rule_tac x="(name \<leftrightarrow> new (insert (atom d) (supp d)))" in exI)
-  apply (simp add: alphas)
-  oops
-
-quotient_definition
-  subst2 ("_ [ _ ::= _ ]" [100,100,100] 100)
-where
-  "subst2 :: lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" is "subst_raw"
-
-lemmas fv_rsp = quot_respect(10)[simplified]
-
-lemma subst_rsp_pre1:
-  assumes a: "alpha_lam_raw a b"
-  shows "alpha_lam_raw (subst_raw a y c) (subst_raw b y c)"
-  using a
-  apply (induct a b arbitrary: c y rule: alpha_lam_raw.induct)
-  apply (simp add: equivp_reflp[OF lam_equivp])
-  apply (simp add: alpha_lam_raw.intros)
-  apply (simp only: alphas)
-  apply clarify
-  apply (simp only: subst_raw.simps)
-  apply (rule alpha_lam_raw.intros)
-  apply (simp only: alphas)
+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)"
+  "atom x \<sharp> (t, s) \<Longrightarrow> subst y s (Lam x t) = Lam x (subst y s t)"
+  apply (subst subst.simps)
+  apply (simp only: match_Var_simps)
+  apply (simp only: option.simps)
+  apply (subst subst.simps)
+  apply (simp only: match_App_simps)
+  apply (simp only: option.simps)
+  apply (simp only: prod.simps)
+  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: match_App_simps)
+  apply (simp only: option.simps)
+  apply (simp only: Let_def)
+  apply (simp only: option.simps)
+  apply (simp only: prod.simps)
   sorry
 
-lemma subst_rsp_pre2:
-  assumes a: "alpha_lam_raw a b"
-  shows "alpha_lam_raw (subst_raw c y a) (subst_raw c y b)"
-  using a
-  apply (induct c arbitrary: a b y)
-  apply (simp add: equivp_reflp[OF lam_equivp])
-  apply (simp add: alpha_lam_raw.intros)
-  apply simp
-  apply (rule alpha_lam_raw.intros)
-  apply (rule_tac x="((new (insert (atom y) (fv_lam_raw a \<union> fv_lam_raw c) -
-                       {atom name}))\<leftrightarrow>(new (insert (atom y) (fv_lam_raw b \<union> fv_lam_raw c) -
-                        {atom name})))" in exI)
-  apply (simp only: alphas)
-  apply (tactic {* split_conj_tac 1 *})
-  prefer 3
-  sorry
-
-lemma [quot_respect]:
-  "(alpha_lam_raw ===> op = ===> alpha_lam_raw ===> alpha_lam_raw) subst_raw subst_raw"
-  proof (intro fun_relI, simp)
-    fix a b c d :: lam_raw
-    fix y :: name
-    assume a: "alpha_lam_raw a b"
-    assume b: "alpha_lam_raw c d"
-    have c: "alpha_lam_raw (subst_raw a y c) (subst_raw b y c)" using subst_rsp_pre1 a by simp
-    then have d: "alpha_lam_raw (subst_raw b y c) (subst_raw b y d)" using subst_rsp_pre2 b by simp
-    show "alpha_lam_raw (subst_raw a y c) (subst_raw b y d)"
-      using c d equivp_transp[OF lam_equivp] by blast
-  qed
-
-lemma simp3:
-  "x \<noteq> y \<Longrightarrow> atom x \<notin> fv_lam_raw s \<Longrightarrow> alpha_lam_raw (subst_raw (Lam_raw x t) y s) (Lam_raw x (subst_raw t y s))"
-  apply simp
-  apply (rule alpha_lam_raw.intros)
-  apply (rule_tac x ="(x \<leftrightarrow> (new (insert (atom y) (fv_lam_raw s \<union> fv_lam_raw t) -
-                    {atom x})))" in exI)
-  apply (simp only: alphas)
-  sorry
-
-lemmas subst_simps = subst_raw.simps(1-2)[quot_lifted,no_vars]
-  simp3[quot_lifted,simplified lam.supp,simplified fresh_def[symmetric], no_vars]
-
-
-thm subst_raw.simps(3)[quot_lifted,no_vars]
-
 end