# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1281952749 -28800
# Node ID 80db544a37ea43d54bf5855acdc7a9e68fb4994f
# Parent  7645e18e8b1970df84bc258583105ab05d0dbe3e
pinpointed the problem

diff -r 7645e18e8b19 -r 80db544a37ea Nominal/Abs.thy
--- a/Nominal/Abs.thy	Mon Aug 16 17:39:16 2010 +0800
+++ b/Nominal/Abs.thy	Mon Aug 16 17:59:09 2010 +0800
@@ -533,7 +533,6 @@
 where
  "prod_alpha = prod_rel"
 
-
 lemma [quot_respect]:
   shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"
   by auto
@@ -563,14 +562,6 @@
 
 
 
-
-
-
-
-
-
-
-
 section {* BELOW is stuff that may or may not be needed *}
 
 lemma supp_atom_image:
diff -r 7645e18e8b19 -r 80db544a37ea Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Mon Aug 16 17:39:16 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Mon Aug 16 17:59:09 2010 +0800
@@ -58,47 +58,46 @@
   val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_laws}
 *}
 
-ML {*
-  Local_Theory.exit_global;
-  Class.instantiation;
-  Class.prove_instantiation_exit_result;
-  Named_Target.theory_init;
-  op |->
-*}
-  
-done
-|> ...
-  |-> (fn x => Class.prove_instantiation_exit_result phi tac x)
-  |-> (fn y => ...)
-
-
 
 section {* NOT *} 
 
+lemma [quot_respect]:
+  "(alpha_assg_raw ===> alpha_assg_raw ===> op =) alpha_bn_raw alpha_bn_raw"
+  "(op = ===> (alpha_trm_raw ===> op =) ===> prod_rel op = alpha_trm_raw ===> op =) prod_fv prod_fv"
+  "((prod_rel op = alpha_trm_raw ===> prod_rel op = alpha_trm_raw ===> op =) ===>
+         (alpha_trm_raw ===> alpha_trm_raw ===> op =) ===>
+            prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw ===>
+            prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw ===> op =)
+            prod_alpha prod_alpha" 
+  "(op = ===>
+         (alpha_trm_raw ===> alpha_trm_raw ===> op =) ===>
+            prod_rel op = alpha_trm_raw ===> prod_rel op = alpha_trm_raw ===> op =)
+            prod_alpha prod_alpha"
+  "((prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw ===>
+             prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw ===> op =) ===>
+            (alpha_trm_raw ===> alpha_trm_raw ===> op =) ===>
+            prod_rel (prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw) alpha_trm_raw ===>
+            prod_rel (prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw) alpha_trm_raw ===>
+            op =)
+            prod_alpha prod_alpha"
+sorry
+
+thm eq_iff(5)
+thm eq_iff(5)[unfolded alphas permute_prod.simps]
+ML {*
+  val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) 
+   @{thms eq_iff(5)[unfolded alphas permute_prod.simps]}
+*}
 
 ML {*
   val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolded alphas prod_fv.simps prod_rel.simps prod_alpha_def]}
 *}
 
 ML {*
-  val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolding alphas]}
+  val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolded alphas]}
 *}
 
 
-(*
-instance trm :: size ..
-instance assg :: size ..
-
-lemma "(size (Var x)) = 0"
-apply(descending)
-apply(rule trm_raw_assg_raw.size(9 - 16))
-apply(simp)
-*)
-
-ML {*
-  val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolding alphas]}
-*}
-
 
 thm perm_defs
 thm perm_simps