--- a/Nominal/Ex/Lambda.thy	Tue Jan 25 02:51:44 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Tue Jan 25 18:58:26 2011 +0100
@@ -17,6 +17,7 @@
   "height (Var x) = 1"
 | "height (App t1 t2) = max (height t1) (height t2) + 1"
 | "height (Lam [x].t) = height t + 1"
+defer
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto simp add: lam.distinct lam.eq_iff)
 apply(simp add: Abs_eq_iff alphas)
@@ -24,11 +25,39 @@
 apply(subst (4) supp_perm_eq[where p="p", symmetric])
 apply(simp add: pure_supp fresh_star_def)
 apply(simp add: eqvt_at_def)
+apply(subgoal_tac "\<And>p x r. height_graph x r \<Longrightarrow> height_graph (p \<bullet> x) (p \<bullet> r)") 
+unfolding eqvt_def
+apply(rule allI)
+apply(simp add: permute_fun_def)
+apply(rule ext)
+apply(rule ext)
+apply(simp add: permute_bool_def)
+apply(rule iffI)
+apply(drule_tac x="p" in meta_spec)
+apply(drule_tac x="- p \<bullet> x" in meta_spec)
+apply(drule_tac x="- p \<bullet> xa" in meta_spec)
+apply(simp)
+apply(drule_tac x="-p" in meta_spec)
+apply(drule_tac x="x" in meta_spec)
+apply(drule_tac x="xa" in meta_spec)
+apply(simp)
+apply(erule height_graph.induct)
+apply(perm_simp)
+apply(rule height_graph.intros)
+apply(perm_simp)
+apply(rule height_graph.intros)
+apply(assumption)
+apply(assumption)
+apply(perm_simp)
+apply(rule height_graph.intros)
+apply(assumption)
 done
 
 termination
   by (relation "measure size") (simp_all add: lam.size)
   
+thm height.simps
+
   
 text {* free name function - returns atom lists *}
 
@@ -38,6 +67,7 @@
   "frees_lst (Var x) = [atom x]"
 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2"
 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)"
+defer
 apply(rule_tac y="x" in lam.exhaust)
 apply(simp_all)[3]
 apply(simp_all only: lam.distinct)
@@ -57,6 +87,32 @@
 apply(auto simp add: fresh_star_def)[1]
 unfolding eqvt_at_def
 apply(simp only: removeAll_eqvt atom_eqvt)
+apply(subgoal_tac "\<And>p x r. frees_lst_graph x r \<Longrightarrow> frees_lst_graph (p \<bullet> x) (p \<bullet> r)") 
+unfolding eqvt_def
+apply(rule allI)
+apply(simp add: permute_fun_def)
+apply(rule ext)
+apply(rule ext)
+apply(simp add: permute_bool_def)
+apply(rule iffI)
+apply(drule_tac x="p" in meta_spec)
+apply(drule_tac x="- p \<bullet> x" in meta_spec)
+apply(drule_tac x="- p \<bullet> xa" in meta_spec)
+apply(simp)
+apply(drule_tac x="-p" in meta_spec)
+apply(drule_tac x="x" in meta_spec)
+apply(drule_tac x="xa" in meta_spec)
+apply(simp)
+apply(erule frees_lst_graph.induct)
+apply(perm_simp)
+apply(rule frees_lst_graph.intros)
+apply(perm_simp)
+apply(rule frees_lst_graph.intros)
+apply(assumption)
+apply(assumption)
+apply(perm_simp)
+apply(rule frees_lst_graph.intros)
+apply(assumption)
 done
 
 termination
@@ -79,6 +135,7 @@
   "(Var x)[y ::= s] = (if x = y then s else (Var x))"
 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
+defer
 apply(auto simp add: lam.distinct lam.eq_iff)
 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
 apply(blast)+
@@ -115,6 +172,33 @@
 apply(simp add: Abs_fresh_iff)
 apply(drule sym)
 apply(simp add: Abs_fresh_iff)
+apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)") 
+unfolding eqvt_def
+apply(rule allI)
+apply(simp add: permute_fun_def)
+apply(rule ext)
+apply(rule ext)
+apply(simp add: permute_bool_def)
+apply(rule iffI)
+apply(drule_tac x="p" in meta_spec)
+apply(drule_tac x="- p \<bullet> x" in meta_spec)
+apply(drule_tac x="- p \<bullet> xa" in meta_spec)
+apply(simp)
+apply(drule_tac x="-p" in meta_spec)
+apply(drule_tac x="x" in meta_spec)
+apply(drule_tac x="xa" in meta_spec)
+apply(simp)
+apply(erule subst_graph.induct)
+apply(perm_simp)
+apply(rule subst_graph.intros)
+apply(perm_simp)
+apply(rule subst_graph.intros)
+apply(assumption)
+apply(assumption)
+apply(perm_simp)
+apply(rule subst_graph.intros)
+apply(simp add: fresh_Pair)
+apply(assumption)
 done
 
 termination
@@ -249,6 +333,7 @@
   "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))"
+defer
 apply(case_tac x)
 apply(simp)
 apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
@@ -335,53 +420,13 @@
 apply(simp_all add: permute_pure)
 done
 
-ML {*
-Nominal_Function_Core.trace := true
-*}
-
 (*
-inductive
-  trans_graph
-where
-  "trans_graph (Var x, xs) (index xs 0 (atom x) \<guillemotright>= (\<lambda>v. Some (DBVar v)))" 
-| "\<lbrakk>trans_graph (t1, xs) (trans_sum (t1, xs)); 
-    \<And>a. trans_sum (t1, xs) = Some a \<Longrightarrow> trans_graph (t2, xs) (trans_sum (t2, xs))\<rbrakk>
-    \<Longrightarrow> trans_graph (App t1 t2, xs) 
-       (trans_sum (t1, xs) \<guillemotright>= (\<lambda>v. trans_sum (t2, xs) \<guillemotright>= (\<lambda>va. Some (DBApp v va))))"
-| "trans_graph (t, atom x # xs) (trans_sum (t, atom x # xs)) \<Longrightarrow>
-    trans_graph (Lam x t, xs) (trans_sum (t, atom x # xs) \<guillemotright>= (\<lambda>v. Some (DBLam v)))"
-
-lemma
-  assumes a: "trans_graph x t"
-  shows "trans_graph (p \<bullet> x) (p \<bullet> t)"
-using a
-apply(induct)
-apply(perm_simp)
-apply(rule trans_graph.intros)
-apply(perm_simp)
-apply(rule trans_graph.intros)
-apply(simp)
-apply(simp)
-defer
-apply(perm_simp)
-apply(rule trans_graph.intros)
-apply(simp)
-apply(rotate_tac 3)
-apply(drule_tac x="FOO" in meta_spec)
-apply(drule meta_mp)
-prefer 2
-apply(simp)
-
-equivariance trans_graph
-*)
-
-(* equivariance fails at the moment
 nominal_primrec
   trans :: "lam \<Rightarrow> atom list \<Rightarrow> db option"
 where
   "trans (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))"
-| "trans (App t1 t2) xs = (trans t1 xs \<guillemotright>= (\<lambda>db1. trans t2 xs \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))"
-| "trans (Lam x t) xs = (trans t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))"
+| "trans (App t1 t2) xs = ((trans t1 xs) \<guillemotright>= (\<lambda>db1. (trans t2 xs) \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))"
+| "trans (Lam [x].t) xs = (trans t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))"
 *)
 
 

--- a/Nominal/Ex/TypeSchemes.thy	Tue Jan 25 02:51:44 2011 +0900
+++ b/Nominal/Ex/TypeSchemes.thy	Tue Jan 25 18:58:26 2011 +0100
@@ -28,6 +28,60 @@
 thm ty_tys.supp
 thm ty_tys.fresh
 
+fun
+  lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty"
+where
+  "lookup [] Y = Var Y"
+| "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)"
+
+lemma lookup_eqvt[eqvt]:
+  shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)"
+apply(induct Ts T rule: lookup.induct)
+apply(simp_all)
+done
+
+nominal_primrec
+    subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
+and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
+where
+  "subst \<theta> (Var X) = lookup \<theta> X"
+| "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)"
+| "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)"
+term subst_substs_sumC
+term Inl
+thm subst_substs_graph.induct
+thm subst_substs_graph.intros
+thm Projl.simps
+apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)")
+apply(simp add: eqvt_def)
+apply(rule allI)
+apply(simp add: permute_fun_def permute_bool_def)
+apply(rule ext)
+apply(rule ext)
+apply(rule iffI)
+apply(drule_tac x="p" in meta_spec)
+apply(drule_tac x="- p \<bullet> x" in meta_spec)
+apply(drule_tac x="- p \<bullet> xa" in meta_spec)
+apply(simp)
+apply(drule_tac x="-p" in meta_spec)
+apply(drule_tac x="x" in meta_spec)
+apply(drule_tac x="xa" in meta_spec)
+apply(simp)
+thm subst_substs_graph.induct
+thm subst_substs_graph.intros
+thm Projl.simps
+apply(erule subst_substs_graph.induct)
+apply(perm_simp)
+apply(rule subst_substs_graph.intros)
+apply(simp only: eqvts)
+thm Projl.simps
+term Inl
+term Inr
+apply(perm_simp)
+thm subst_substs_graph.intros
+thm Projl.simps
+oops
+
 
 section {* defined as two separate nominal datatypes *}
 
@@ -52,22 +106,23 @@
 thm tys2.fresh
 
 fun
-  lookup :: "(name \<times> ty2) list \<Rightarrow> name \<Rightarrow> ty2"
+  lookup2 :: "(name \<times> ty2) list \<Rightarrow> name \<Rightarrow> ty2"
 where
-  "lookup [] Y = Var2 Y"
-| "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)"
+  "lookup2 [] Y = Var2 Y"
+| "lookup2 ((X, T) # Ts) Y = (if X = Y then T else lookup2 Ts Y)"
 
-lemma lookup_eqvt[eqvt]:
-  shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)"
-apply(induct Ts T rule: lookup.induct)
+lemma lookup2_eqvt[eqvt]:
+  shows "(p \<bullet> lookup2 Ts T) = lookup2 (p \<bullet> Ts) (p \<bullet> T)"
+apply(induct Ts T rule: lookup2.induct)
 apply(simp_all)
 done
 
-function
+nominal_primrec
   subst  :: "(name \<times> ty2) list \<Rightarrow> ty2 \<Rightarrow> ty2"
 where
-  "subst \<theta> (Var2 X) = lookup \<theta> X"
+  "subst \<theta> (Var2 X) = lookup2 \<theta> X"
 | "subst \<theta> (Fun2 T1 T2) = Fun2 (subst \<theta> T1) (subst \<theta> T2)"
+defer
 apply(case_tac x)
 apply(simp)
 apply(rule_tac y="b" in ty2.exhaust)
@@ -76,6 +131,28 @@
 apply(simp_all add: ty2.distinct)
 apply(simp add: ty2.eq_iff)
 apply(simp add: ty2.eq_iff)
+apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)")
+apply(simp add: eqvt_def)
+apply(rule allI)
+apply(simp add: permute_fun_def permute_bool_def)
+apply(rule ext)
+apply(rule ext)
+apply(rule iffI)
+apply(drule_tac x="p" in meta_spec)
+apply(drule_tac x="- p \<bullet> x" in meta_spec)
+apply(drule_tac x="- p \<bullet> xa" in meta_spec)
+apply(simp)
+apply(drule_tac x="-p" in meta_spec)
+apply(drule_tac x="x" in meta_spec)
+apply(drule_tac x="xa" in meta_spec)
+apply(simp)
+apply(erule subst_graph.induct)
+apply(perm_simp)
+apply(rule subst_graph.intros)
+apply(perm_simp)
+apply(rule subst_graph.intros)
+apply(assumption)
+apply(assumption)
 done
 
 termination
@@ -86,14 +163,14 @@
 lemma subst_eqvt[eqvt]:
   shows "(p \<bullet> subst \<theta> T) = subst (p \<bullet> \<theta>) (p \<bullet> T)"
 apply(induct \<theta> T rule: subst.induct)
-apply(simp_all add: lookup_eqvt)
+apply(simp_all add: lookup2_eqvt)
 done
 
 lemma j:
   assumes "a \<sharp> Ts" " a \<sharp> X"
-  shows "a \<sharp> lookup Ts X"
+  shows "a \<sharp> lookup2 Ts X"
 using assms
-apply(induct Ts X rule: lookup.induct)
+apply(induct Ts X rule: lookup2.induct)
 apply(auto simp add: ty2.fresh fresh_Cons fresh_Pair)
 done
 

--- a/Nominal/nominal_function_core.ML	Tue Jan 25 02:51:44 2011 +0900
+++ b/Nominal/nominal_function_core.ML	Tue Jan 25 18:58:26 2011 +0100
@@ -115,6 +115,14 @@
     |> HOLogic.mk_Trueprop
   end
 
+fun mk_eqvt trm =
+  let
+    val ty = fastype_of trm
+  in
+    Const (@{const_name eqvt}, ty --> @{typ bool}) $ trm
+    |> HOLogic.mk_Trueprop
+  end
+
 (* nominal *)
 fun find_calls2 f t = 
   let
@@ -496,18 +504,19 @@
       |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
       |> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
 
-    val goalstate =  Conjunction.intr graph_is_function complete
+    val goalstate =  
+         Conjunction.intr (Conjunction.intr graph_is_function complete) G_eqvt 
       |> Thm.close_derivation
       |> Goal.protect
       |> fold_rev (Thm.implies_intr o cprop_of) compat
       |> Thm.implies_intr (cprop_of complete)
+      |> Thm.implies_intr (cprop_of G_eqvt)
   in
     (goalstate, values)
   end
 
-(* nominal *) 
 (* wrapper -- restores quantifiers in rule specifications *)
-fun inductive_def eqvt_flag (binding as ((R, T), _)) intrs lthy =
+fun inductive_def (binding as ((R, T), _)) intrs lthy =
   let
     val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) =
       lthy
@@ -527,16 +536,6 @@
           [] (* no special monos *)
       ||> Local_Theory.restore_naming lthy
 
-    val eqvt_thm' = 
-      if eqvt_flag = false then NONE
-      else 
-        let
-          (* val _ = tracing ("intrs:\n" ^ cat_lines (map @{make_string} intrs_gen)) *)
-          val ([eqvt_thm], lthy) = Nominal_Eqvt.raw_equivariance false [Rdef] raw_induct intrs_gen lthy
-        in
-          SOME ((Nominal_ThmDecls.eqvt_transform lthy eqvt_thm) RS @{thm eqvtI})
-        end
-
     val cert = cterm_of (ProofContext.theory_of lthy)
     fun requantify orig_intro thm =
       let
@@ -550,7 +549,7 @@
           forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm
       end
   in
-    ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct, eqvt_thm'), lthy)
+    ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy)
   end
 
 (* nominal *)
@@ -574,7 +573,7 @@
 
     val G_intros = map2 mk_GIntro clauses RCss
   in
-    inductive_def true ((Binding.name n, T), NoSyn) G_intros lthy
+    inductive_def ((Binding.name n, T), NoSyn) G_intros lthy
   end
 
 fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
@@ -605,8 +604,8 @@
 
     val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
 
-    val ((R, RIntro_thms, R_elim, _, _), lthy) =
-      inductive_def false ((Binding.name n, T), NoSyn) (flat R_intross) lthy
+    val ((R, RIntro_thms, R_elim, _), lthy) =
+      inductive_def ((Binding.name n, T), NoSyn) (flat R_intross) lthy
   in
     ((R, Library.unflat R_intross RIntro_thms, R_elim), lthy)
   end
@@ -988,7 +987,7 @@
     val trees = map build_tree clauses
     val RCss = map find_calls trees
 
-    val ((G, GIntro_thms, G_elim, G_induct, SOME G_eqvt), lthy) =
+    val ((G, GIntro_thms, G_elim, G_induct), lthy) =
       PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
 
     val ((f, (_, f_defthm)), lthy) =
@@ -1019,6 +1018,8 @@
       mk_compat_proof_obligations domT ranT fvar f abstract_qglrs 
       |> map (cert #> Thm.assume)
 
+    val G_eqvt = mk_eqvt G |> cert |> Thm.assume
+ 
     val compat_store = store_compat_thms n compat
 
     val (goalstate, values) = PROFILE "prove_stuff"
@@ -1032,10 +1033,11 @@
       let
         val newthy = theory_of_thm provedgoal (*FIXME*)
 
-        val (graph_is_function, complete_thm) =
+        val ((graph_is_function, complete_thm), _) =
           provedgoal
           |> Conjunction.elim
-          |> apfst (Thm.forall_elim_vars 0)
+          |>> Conjunction.elim
+          |>> apfst (Thm.forall_elim_vars 0)
 
         val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)