--- a/Nominal/Ex/Lambda_F_T.thy	Sat Jun 04 09:07:50 2011 +0900
+++ b/Nominal/Ex/Lambda_F_T.thy	Sat Jun 04 14:50:57 2011 +0900
@@ -44,58 +44,152 @@
   using fresh_fun_eqvt_app[OF a b(1)] a b
   by (metis fresh_fun_app)
 
+lemma the_default_pty:
+  assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
+  and unique: "\<exists>!y. G x y"
+  and pty: "\<And>x y. G x y \<Longrightarrow> P x y"
+  shows "P x (f x)"
+  apply(subst f_def)
+  apply (rule ex1E[OF unique])
+  apply (subst THE_default1_equality[OF unique])
+  apply assumption
+  apply (rule pty)
+  apply assumption
+  done
+
+locale test =
+  fixes f1::"name \<Rightarrow> name list \<Rightarrow> ('a::pt)"
+    and f2::"lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> name list \<Rightarrow> ('a::pt)"
+    and f3::"name \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> name list \<Rightarrow> ('a::pt)"
+  assumes fs: "finite (supp (f1, f2, f3))"
+    and eq: "eqvt f1" "eqvt f2" "eqvt f3"
+    and fcb1: "\<And>l n. atom ` set l \<sharp>* f1 n l"
+    and fcb2: "\<And>l t1 t2 r1 r2. atom ` set l \<sharp>* (r1, r2) \<Longrightarrow> atom ` set l \<sharp>* f2 t1 t2 r1 r2 l"
+    and fcb3: "\<And>t l r. atom ` set (x # l) \<sharp>* r \<Longrightarrow> atom ` set (x # l) \<sharp>* f3 x t r l"
+begin
+
 nominal_primrec
   f
 where
-  "f f1 f2 f3 (Var x) l = f1 x l"
-| "f f1 f2 f3 (App t1 t2) l = f2 t1 t2 (f f1 f2 f3 t1 l) (f f1 f2 f3 t2 l) l"
-| "(\<And>t l r. atom x \<sharp> r \<Longrightarrow> atom x \<sharp> f3 x t r l) \<Longrightarrow> (eqvt f1 \<and> eqvt f2 \<and> eqvt f3) \<Longrightarrow> atom x \<sharp> (f1,f2,f3,l) \<Longrightarrow> (f f1 f2 f3 (Lam [x].t) l) = f3 x t (f f1 f2 f3 t (x # l)) l"
+  "f (Var x) l = f1 x l"
+| "f (App t1 t2) l = f2 t1 t2 (f t1 l) (f t2 l) l"
+| "atom x \<sharp> l \<Longrightarrow> (f (Lam [x].t) l) = f3 x t (f t (x # l)) l"
   apply (simp add: eqvt_def f_graph_def)
-  apply (rule, perm_simp, rule)
+  apply (rule, perm_simp)
+  apply (simp only: eq[unfolded eqvt_def])
   apply(case_tac x)
-  apply(rule_tac y="d" and c="z" in lam.strong_exhaust)
+  apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
   apply(auto simp add: fresh_star_def)
-  apply(blast)
-  apply blast
-  defer
-  apply(simp add: fresh_Pair_elim)
   apply(erule Abs1_eq_fdest)
   defer
   apply simp_all
-  apply (rule_tac f="f3a" in fresh_fun_eqvt_app4)
-  apply assumption
+  apply (rule fresh_fun_eqvt_app4[OF eq(3)])
   apply (simp add: fresh_at_base)
   apply assumption
   apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Pair supp_fun_eqvt finite_supp)
-  apply (simp add: fresh_Pair)
-  apply (simp add: fresh_Cons)
-  apply (simp add: fresh_Cons fresh_at_base)
-  apply (assumption)
-  apply (subgoal_tac "\<And>p y r l. p \<bullet> (f3a x y r l) = f3a (p \<bullet> x) (p \<bullet> y) (p \<bullet> r) (p \<bullet> l)")
+  apply (simp add: finite_supp)
+  apply (simp add: fresh_Pair fresh_Cons fresh_at_base)
+  apply assumption
+  apply (subgoal_tac "\<And>p y r l. p \<bullet> (f3 x y r l) = f3 (p \<bullet> x) (p \<bullet> y) (p \<bullet> r) (p \<bullet> l)")
   apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> la = la")
-  apply (simp add: eqvt_at_def eqvt_def)
+  apply (simp add: eqvt_at_def)
   apply (simp add: swap_fresh_fresh)
-  apply (simp add: permute_fun_app_eq)
-  apply (simp add: eqvt_def)
+  apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def])
+  apply (subgoal_tac "atom ` set (x # la) \<sharp>* f3 x t (f_sumC (t, x # la)) la")
+  apply (simp add: fresh_star_def)
+  apply (rule fcb3)
+  apply (rule_tac x="x # la" in meta_spec)
+  apply (thin_tac "eqvt_at f_sumC (t, x # la)")
+  apply (thin_tac "atom x \<sharp> la")
+  apply (thin_tac "atom xa \<sharp> la")
+  apply (thin_tac "x \<noteq> xa")
+  apply (thin_tac "atom xa \<sharp> t")
+  apply (subgoal_tac "atom ` set (snd (t, xb)) \<sharp>* f_sumC (t, xb)")
+  apply simp
+  apply (rule_tac x="(t, xb)" in meta_spec)
+  apply (simp only: triv_forall_equality)
+--"We start induction on the graph. We need the 2nd subgoal in the first one"
+  apply (subgoal_tac "\<And>x y. f_graph x y \<Longrightarrow> atom ` set (snd x) \<sharp>* y")
+  apply (rule the_default_pty[OF f_sumC_def])
+  prefer 2
+  apply blast
   prefer 2
-  apply (subgoal_tac "atom x \<sharp> f_sumC (f1a, f2a, f3a, t, x # la)")
+  apply (erule f_graph.induct)
+  apply (simp add: fcb1)
+  apply (simp add: fcb2 fresh_star_Pair)
+  apply (simp only: snd_conv)
+  apply (subgoal_tac "atom ` set (xa # l) \<sharp>* f3 xa t (f_sum (t, xa # l)) l")
+  apply (simp add: fresh_star_def)
+  apply (rule fcb3)
+  apply assumption
+--"We'd like to do the proof with this property"
+  apply (case_tac xc)
   apply simp
---"I believe this holds by induction on the graph..."
-  unfolding f_sumC_def
-  apply (rule_tac y="t" in lam.exhaust)
-  apply (subgoal_tac "THE_default undefined (f_graph (f1a, f2a, f3a, t, x # la)) = f1a name (x # la)")
+  apply (rule_tac lam="a" and c="b" in lam.strong_induct)
+  apply (rule_tac a="f1 name c" in ex1I)
+  apply (rule f_graph.intros)
+  apply (erule f_graph.cases)
+  apply simp_all[3]
+  apply (drule_tac x="c" in meta_spec)+
+  apply (erule ex1E)+
+  apply (subgoal_tac "f_graph (lam1, c) (f_sumC (lam1, c))")
+  apply (subgoal_tac "f_graph (lam2, c) (f_sumC (lam2, c))")
+  apply (rule_tac a="f2 lam1 lam2 (f_sumC (lam1, c)) (f_sumC (lam2, c)) c" in ex1I)
+  apply (rule_tac f_graph.intros(2))
+  apply assumption+
+  apply (rotate_tac 8)
+  apply (erule f_graph.cases)
+  apply simp
+  apply auto[1]
+  apply metis
   apply simp
-  defer
-  apply (rule THE_default1_equality)
+  apply (simp add: f_sumC_def)
+  apply (rule THE_defaultI')
+  apply metis
+  apply (simp add: f_sumC_def)
+  apply (rule THE_defaultI')
+  apply metis
+--"Only the Lambda case left"
+  apply (subgoal_tac "f_graph (lam, (name # c)) (f_sumC (lam, (name # c)))")
+  prefer 2
+  apply (simp add: f_sumC_def)
+  apply (rule THE_defaultI')
+  apply assumption
+  apply (rule_tac a="f3 name lam (f_sumC (lam, name # c)) c" in ex1I)
+  apply (rule f_graph.intros(3))
+  apply (simp add: fresh_star_def)
+  apply assumption
+  apply (rotate_tac -1)
+  apply (erule f_graph.cases)
+  apply simp_all[2]
   apply simp
-  defer
+  apply auto[1]
+  apply (subgoal_tac "f_sumC (lam, name # l) = f_sum (lam, name # l)")
   apply simp
-  apply (rule_tac ?f1.0="f1a" in f_graph.intros(1))
-  sorry (*this could be defined? *)
+  apply (rule sym)
+  apply (erule Abs1_eq_fdest)
+  apply (subgoal_tac "atom ` set (name # l) \<sharp>* f3 name lam (f_sum (lam, name # l)) l")
+  apply (simp add: fresh_star_def)
+  apply (rule fcb3)
+  apply metis
+  apply (rule fresh_fun_eqvt_app4[OF eq(3)])
+  apply (simp add: fresh_at_base)
+  apply assumption
+defer --"eqvt_at f_sumC"
+  apply assumption
+  apply (subgoal_tac "\<And>p y r l. p \<bullet> (f3 name y r l) = f3 (p \<bullet> name) (p \<bullet> y) (p \<bullet> r) (p \<bullet> l)")
+  apply (subgoal_tac "(atom name \<rightleftharpoons> atom xa) \<bullet> l = l")
+  apply (simp add: eq[unfolded eqvt_def])
+defer --"eqvt_at f_sumC"
+  apply (metis fresh_star_insert swap_fresh_fresh)
+  apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def])
+  apply simp
+  sorry
 
 termination
-  by (relation "measure (\<lambda>(_,_,_,x,_). size x)") (auto simp add: lam.size)
+  by (relation "measure (\<lambda>(x,_). size x)") (auto simp add: lam.size)
+
+end
 
 section {* Locally Nameless Terms *}
 
@@ -111,31 +205,47 @@
   "lookup [] n x = LNVar x"
 | "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))"
 
-lemma [eqvt]:
+lemma lookup_eqvt[eqvt]:
   shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
   by (induct xs arbitrary: n) (simp_all add: permute_pure)
 
-definition
-  trans :: "lam \<Rightarrow> name list \<Rightarrow> ln"
-where
-  "trans t l = f (%x l. lookup l 0 x) (%t1 t2 r1 r2 l. LNApp r1 r2) (%n t r l. LNLam r) t l"
+lemma fresh_at_list: "atom x \<sharp> xs \<longleftrightarrow> x \<notin> set xs"
+  unfolding fresh_def supp_set[symmetric]
+  apply (induct xs)
+  apply (simp add: supp_set_empty)
+  apply simp
+  apply auto
+  apply (simp_all add: insert_absorb UnI2 finite_set supp_of_finite_insert supp_at_base)
+  done
 
-lemma
- "trans (Var x) xs = lookup xs 0 x"
-  "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)"
-  "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))"
-apply (simp_all add: trans_def)
-apply (subst f.simps)
-apply (simp add: ln.fresh)
-apply (simp add: eqvt_def)
-apply auto
-apply (perm_simp, rule)
-apply (perm_simp, rule)
-apply (perm_simp, rule)
-apply (auto simp add: fresh_Pair)[1]
-apply (simp_all add: fresh_def supp_def permute_fun_def)[3]
-apply (simp add: eqvts permute_pure)
-done
+interpretation trans: test
+  "%x l. lookup l 0 x"
+  "%t1 t2 r1 r2 l. LNApp r1 r2"
+  "%n t r l. LNLam r"
+  apply default
+  apply (auto simp add: pure_fresh supp_Pair)
+  apply (simp_all add: fresh_def supp_def permute_fun_def permute_pure lookup_eqvt)[3]
+  apply (simp_all add: eqvt_def permute_fun_def permute_pure lookup_eqvt)
+  apply (simp add: fresh_star_def)
+  apply (rule_tac x="0 :: nat" in spec)
+  apply (induct_tac l)
+  apply (simp add: ln.fresh pure_fresh)
+  apply (auto simp add: ln.fresh pure_fresh)[1]
+  apply (case_tac "a \<in> set list")
+  apply simp
+  apply (rule_tac f="lookup" in fresh_fun_eqvt_app3)
+  unfolding eqvt_def
+  apply rule
+  using eqvts_raw(35)
+  apply auto[1]
+  apply (simp add: fresh_at_list)
+  apply (simp add: pure_fresh)
+  apply (simp add: fresh_at_base)
+  apply (simp add: fresh_star_Pair fresh_star_def ln.fresh)
+  apply (simp add: fresh_star_def ln.fresh)
+  done
+
+thm trans.f.simps
 
 lemma lam_strong_exhaust2:
   "\<lbrakk>\<And>name. y = Var name \<Longrightarrow> P; 
@@ -154,9 +264,18 @@
 | "finite (supp (g1, g2, g3)) \<Longrightarrow> atom x \<sharp> (g1,g2,g3) \<Longrightarrow> (g g1 g2 g3 (Lam [x].t)) = g3 x t (g g1 g2 g3 t)"
   apply (simp add: eqvt_def g_graph_def)
   apply (rule, perm_simp, rule)
+  apply simp_all
   apply (case_tac x)
   apply (case_tac "finite (supp (a, b, c))")
   prefer 2
   apply simp
   apply(rule_tac y="d" and c="(a,b,c)" in lam_strong_exhaust2)
-  apply simp_all
+  apply auto
+  apply blast
+  apply (simp add: Abs1_eq_iff fresh_star_def)
+  sorry
+
+termination
+  by (relation "measure (\<lambda>(_,_,_,t). size t)") (simp_all add: lam.size)
+
+end