
diff -r 0f0335d91456 -r 1c3ad1256f16 Nominal/Ex/LamTest.thy
--- a/Nominal/Ex/LamTest.thy	Sun Jan 09 04:28:24 2011 +0000
+++ b/Nominal/Ex/LamTest.thy	Sun Jan 09 05:38:53 2011 +0000
@@ -35,8 +35,8 @@
 lemma fundef_ex1_eqvt:
   fixes x::"'a::pt"
   assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
+  assumes eqvt: "eqvt G"
   assumes ex1: "\<exists>!y. G x y"
-  assumes eqvt: "eqvt G"
   shows "(p \<bullet> (f x)) = f (p \<bullet> x)"
   apply (simp only: f_def)
   apply(subst the_default_eqvt)
@@ -46,7 +46,16 @@
   apply(simp add: eqvt_def)
   done
 
-
+lemma fundef_ex1_eqvt_at:
+  fixes x::"'a::pt"
+  assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
+  assumes eqvt: "eqvt G"
+  assumes ex1: "\<exists>!y. G x y"
+  shows "eqvt_at f x"
+  unfolding eqvt_at_def
+  using assms
+  apply(auto intro: fundef_ex1_eqvt)
+  done
 
 ML {*
 
@@ -161,11 +170,13 @@
 
 fun mk_compat_proof_obligations domT ranT fvar f glrs =
   let
+    (*
     val _ = tracing ("domT: " ^ @{make_string} domT)
     val _ = tracing ("ranT: " ^ @{make_string} ranT)
     val _ = tracing ("fvar: " ^ @{make_string} fvar)
     val _ = tracing ("f: " ^ @{make_string} f)
-
+    *)
+ 
     fun mk_impl ((qs, gs, lhs, rhs), (qs', gs', lhs', rhs')) =
       let
         val shift = incr_boundvars (length qs')
@@ -186,7 +197,8 @@
       end
   in
     map mk_impl (unordered_pairs glrs)
-    |> tap (fn ts => tracing ("compat_trms:\n" ^ cat_lines (map (Syntax.string_of_term @{context}) ts)))
+    (*|> tap (fn ts => tracing ("compat_trms:\n" ^ cat_lines (map (Syntax.string_of_term @{context}) ts)))
+    *)
   end
 *}
 
@@ -296,9 +308,6 @@
 
 ML {*
 fun eqvt_at_elim thm =
-  let
-    val _ = tracing ("term\n" ^ @{make_string} (prop_of thm))
-  in
   case (prop_of thm) of
     Const ("==>", _) $ (t as (@{term Trueprop} $ (Const (@{const_name eqvt_at}, _) $ _ $ _))) $ _ => 
       let
@@ -308,7 +317,6 @@
         |> eqvt_at_elim
       end
   | _ => thm
-  end
 *}
 
 ML {*
@@ -330,10 +338,10 @@
     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))
+      (*|> tap (fn th => tracing ("NEED TO PROVE " ^ @{make_string} th))*)
       (*|> Thm.elim_implies @{thm TrueI}*) (* THERE *)
       |> eqvt_at_elim 
-      |> tap (fn th => tracing ("AFTER " ^ @{make_string} th))
+      (*|> tap (fn th => tracing ("AFTER " ^ @{make_string} th))*)
       |> fold Thm.elim_implies agsj
       |> fold Thm.elim_implies agsi
       |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
@@ -344,10 +352,10 @@
     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)) 
+      (*|> tap (fn th => tracing ("NEED TO PROVE " ^ @{make_string} th))*) 
       (*|> Thm.elim_implies @{thm TrueI}*)
       |> eqvt_at_elim 
-      |> tap (fn th => tracing ("AFTER " ^ @{make_string} th))
+      (*|> tap (fn th => tracing ("AFTER " ^ @{make_string} th))*)
       |> fold Thm.elim_implies agsi
       |> fold Thm.elim_implies agsj
       |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj)
@@ -491,10 +499,13 @@
   end
 *}
 
-(* AAA *)
+ML Thm.forall_elim_vars
+
+ML {* (ex1_implies_ex, ex1_implies_un) *}
+thm fundef_ex1_eqvt_at
 
 ML {*
-fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim f_def =
+fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim G_eqvt f_def =
   let
     val Globals {h, domT, ranT, x, ...} = globals
     val thy = ProofContext.theory_of ctxt
@@ -510,40 +521,45 @@
     val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
     val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
       |> instantiate' [] [NONE, SOME (cterm_of thy h)]
+    val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at}))
 
-    (*
-    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 _ = tracing ("ih_eqvt\n" ^ @{make_string} ih_eqvt)
 
     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
+      |> tap (fn th => tracing ("A\n" ^ @{make_string} th))
       |> Thm.forall_elim_vars 0
+      |> tap (fn th => tracing ("B\n" ^ @{make_string} th))
       |> fold (curry op COMP) ex1s
+      |> tap (fn th => tracing ("C\n" ^ @{make_string} th))
       |> Thm.implies_intr (ihyp)
+      |> tap (fn th => tracing ("D\n" ^ @{make_string} th))
       |> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
+      |> tap (fn th => tracing ("E\n" ^ @{make_string} th))
       |> Thm.forall_intr (cterm_of thy x)
+      |> tap (fn th => tracing ("F\n" ^ @{make_string} th))
       |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
+      |> tap (fn th => tracing ("G\n" ^ @{make_string} th))
       |> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
+      |> tap (fn th => tracing ("H\n" ^ @{make_string} th))
+
 
     val goalstate =  Conjunction.intr graph_is_function complete
       |> Thm.close_derivation
@@ -1055,7 +1071,9 @@
     val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
     val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
 
+    (*
     val _ = tracing ("recursive calls:\n" ^ cat_lines (map @{make_string} RCss))
+    *)
 
     val ((R, RIntro_thmss, R_elim, R_eqvt), lthy) =
       PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
@@ -1096,9 +1114,10 @@
 
     val (goalstate, values) = PROFILE "prove_stuff"
       (prove_stuff lthy globals G f R xclauses complete compat
-         compat_store G_elim) f_defthm
+         compat_store G_elim G_eqvt) f_defthm
      
     val _ = tracing ("goalstate prove_stuff thm:\n" ^ @{make_string} goalstate)
+    val _ = tracing ("values prove_stuff thms:\n" ^ cat_lines (map @{make_string} values))
 
     val mk_trsimps =
       mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses




