--- a/Nominal/Ex/LamTest.thy	Fri Jan 07 02:30:00 2011 +0000
+++ b/Nominal/Ex/LamTest.thy	Fri Jan 07 05:06:25 2011 +0000
@@ -17,6 +17,20 @@
 apply(auto simp add: eqvt_def)
 done
 
+
+lemma the_default_eqvt:
+  assumes unique: "\<exists>!x. P x"
+  shows "(p \<bullet> (THE_default d P)) = (THE_default (p \<bullet> d) (p \<bullet> P))"
+  apply(rule THE_default1_equality [symmetric])
+  apply(rule_tac p="-p" in permute_boolE)
+  apply(perm_simp add: permute_minus_cancel)
+  apply(rule unique)
+  apply(rule_tac p="-p" in permute_boolE)
+  apply(perm_simp add: permute_minus_cancel)
+  apply(rule THE_defaultI'[OF unique])
+  done
+
+
 ML {*
 
 
@@ -73,8 +87,11 @@
   tree: Function_Ctx_Tree.ctx_tree,
   lGI: thm,
   RCs: rec_call_info list}
+*}
 
+thm accp_induct_rule
 
+ML {*
 (* Theory dependencies. *)
 val acc_induct_rule = @{thm accp_induct_rule}
 
@@ -128,8 +145,8 @@
           (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
             HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
         |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
-        (* HERE |> (curry Logic.mk_implies) (mk_eqvt fvar) *)
-        |> (curry Logic.mk_implies) @{term "Trueprop True"}
+        (*|> (curry Logic.mk_implies) (mk_eqvt fvar) *)
+        |> (curry Logic.mk_implies) @{term "Trueprop True"}  (* HERE *)
         |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
         |> curry abstract_over fvar
         |> curry subst_bound f
@@ -262,6 +279,7 @@
     in
       compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
       |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
+      (*|> tap (fn th => tracing ("NEED TO PROVE" ^ @{make_string} th)) *)
       |> Thm.elim_implies @{thm TrueI}
       |> fold Thm.elim_implies agsj
       |> fold Thm.elim_implies agsi
@@ -273,6 +291,7 @@
     in
       compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
       |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
+      (* |> tap (fn th => tracing ("NEED TO PROVE" ^ @{make_string} th)) *)
       |> Thm.elim_implies @{thm TrueI}
       |> fold Thm.elim_implies agsi
       |> fold Thm.elim_implies agsj
@@ -378,7 +397,9 @@
 
     val unique_clauses =
       map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas
-  
+     
+    val _ = tracing ("unique_clauses\n" ^ cat_lines (map @{make_string} unique_clauses))
+
     fun elim_implies_eta A AB =
       Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single
 
@@ -414,6 +435,8 @@
   end
 *}
 
+(* AAA *)
+
 ML {*
 fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim f_def =
   let
@@ -432,13 +455,23 @@
     val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
       |> instantiate' [] [NONE, SOME (cterm_of thy h)]
 
+    val _ = tracing ("ihyp\n" ^ @{make_string} ihyp)
+    val _ = tracing ("ihyp_thm\n" ^ @{make_string} ihyp_thm)
+    val _ = tracing ("ih_intro\n" ^ @{make_string} ih_intro)
+    val _ = tracing ("ih_elim\n" ^ @{make_string} ih_elim)
+
     val _ = trace_msg (K "Proving Replacement lemmas...")
     val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
 
+    val _ = tracing (cat_lines (map @{make_string} repLemmas))
+
     val _ = trace_msg (K "Proving cases for unique existence...")
     val (ex1s, values) =
       split_list (map (mk_uniqueness_case thy globals G f 
         ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
+    
+    val _ = tracing ("ex1s\n" ^ cat_lines (map @{make_string} ex1s))
+    val _ = tracing ("values\n" ^ cat_lines (map @{make_string} values)) 
 
     val _ = trace_msg (K "Proving: Graph is a function")
     val graph_is_function = complete
@@ -460,10 +493,7 @@
   end
 *}
 
-ML {* 
-Inductive.add_inductive_i;
-Local_Theory.conceal
-*}
+
 
 ML {*
 (* wrapper -- restores quantifiers in rule specifications *)
@@ -948,7 +978,7 @@
 
     val _ = tracing ("Graph - name: " ^ @{make_string} G)
     val _ = tracing ("Graph intros:\n" ^ cat_lines (map @{make_string} GIntro_thms))
-    val _ = tracing ("Graph Equivariance" ^ @{make_string} G_eqvt)
+    val _ = tracing ("Graph Equivariance " ^ @{make_string} G_eqvt)
     
 
     val ((f, (_, f_defthm)), lthy) =
@@ -965,7 +995,7 @@
 
     val _ = tracing ("Relation - name: " ^ @{make_string} R) 
     val _ = tracing ("Relation intros:\n" ^ cat_lines (map @{make_string} RIntro_thmss))
-    val _ = tracing ("Relation Equivariance" ^ @{make_string} R_eqvt)
+    val _ = tracing ("Relation Equivariance " ^ @{make_string} R_eqvt)
 
     val (_, lthy) =
       Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
@@ -1501,6 +1531,8 @@
 apply(simp add: lam.eq_iff)
 sorry
 
+thm depth.psimps
+
 nominal_primrec 
   frees :: "lam \<Rightarrow> name set"
 where

--- a/Nominal/Nominal2_Eqvt.thy	Fri Jan 07 02:30:00 2011 +0000
+++ b/Nominal/Nominal2_Eqvt.thy	Fri Jan 07 05:06:25 2011 +0000
@@ -124,6 +124,18 @@
 
 lemma the_eqvt:
   assumes unique: "\<exists>!x. P x"
+  shows "(p \<bullet> (THE x. P x)) = (THE x. (p \<bullet> P) x)"
+  apply(rule the1_equality [symmetric])
+  apply(rule_tac p="-p" in permute_boolE)
+  apply(perm_simp add: permute_minus_cancel)
+  apply(rule unique)
+  apply(rule_tac p="-p" in permute_boolE)
+  apply(perm_simp add: permute_minus_cancel)
+  apply(rule theI'[OF unique])
+  done
+
+lemma the_eqvt2:
+  assumes unique: "\<exists>!x. P x"
   shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))"
   apply(rule the1_equality [symmetric])
   apply(simp add: ex1_eqvt2[symmetric])