# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1281514884 -28800
# Node ID d9a0cf26a88c584f755f5c616a4c6aa9442279c0
# Parent  9294d7cec5e27662fc1b298c5023af8f9aa8594a
added a function that transforms the helper-rsp lemmas into real rsp lemmas

diff -r 9294d7cec5e2 -r d9a0cf26a88c Nominal/Ex/CoreHaskell.thy
--- a/Nominal/Ex/CoreHaskell.thy	Sun Aug 08 10:12:38 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy	Wed Aug 11 16:21:24 2010 +0800
@@ -8,7 +8,7 @@
 atom_decl cvar
 atom_decl tvar
 
-declare [[STEPS = 16]]
+declare [[STEPS = 17]]
 
 nominal_datatype tkind =
   KStar
@@ -85,6 +85,9 @@
 | "bv_cvs CvsNil = []"
 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
 
+thm alpha_sym_thms
+thm funs_rsp
+thm distinct
 
 term TvsNil
 
diff -r 9294d7cec5e2 -r d9a0cf26a88c Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Sun Aug 08 10:12:38 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Wed Aug 11 16:21:24 2010 +0800
@@ -35,6 +35,8 @@
 thm perm_laws
 thm funs_rsp
 
+declare size_rsp[quot_respect]
+declare funs_rsp[quot_respect]
 
 typ trm
 typ assg
@@ -70,16 +72,11 @@
   "(op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) Baz_raw Baz_raw"
   "(op = ===> op = ===> alpha_trm_raw ===> alpha_assg_raw) As_raw As_raw"
 apply(tactic {* ALLGOALS tac *})
-done
+sorry
 
 lemma [quot_respect]:
-  "(alpha_trm_raw ===> op =) fv_trm_raw fv_trm_raw"
-  "(alpha_assg_raw ===> op =) fv_bn_raw fv_bn_raw"
-  "(alpha_assg_raw ===> op =) bn_raw bn_raw"
-  "(alpha_assg_raw ===> op =) fv_assg_raw fv_assg_raw"
   "(op = ===> alpha_trm_raw ===> alpha_trm_raw) permute permute"
-  "(alpha_trm_raw ===> op =) size size"
-apply(simp_all add: alpha_bn_imps funs_rsp size_rsp)
+apply(simp)
 sorry
 
 ML {*
diff -r 9294d7cec5e2 -r d9a0cf26a88c Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Sun Aug 08 10:12:38 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Wed Aug 11 16:21:24 2010 +0800
@@ -28,6 +28,8 @@
   val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> 
     term list -> thm -> thm list -> Proof.context -> thm list
   val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list
+
+  val resolve_fun_rel: thm -> thm
 end
 
 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =
@@ -604,7 +606,7 @@
 end
 
 
-(* helper lemmas for respectfulness for fv_raw / bn_raw *)
+(* respectfulness for fv_raw / bn_raw *)
 
 fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt =
 let
@@ -622,7 +624,7 @@
     (K (asm_full_simp_tac ss)) ctxt
 end
 
-(* helper lemmas for respectfulness for size *)
+(* respectfulness for size *)
 
 fun raw_size_rsp_aux all_alpha_trms alpha_induct simps ctxt =
 let
@@ -641,5 +643,19 @@
   alpha_prove all_alpha_trms props alpha_induct (K tac) ctxt
 end
 
+
+(* resolve with @{thm fun_relI} *)
+
+fun resolve_fun_rel thm =
+let 
+  val fun_rel = @{thm fun_relI}
+  val thm' = forall_intr_vars thm
+  val cinsts = Thm.match (cprem_of fun_rel 1, cprop_of thm')
+  val fun_rel' = Thm.instantiate cinsts fun_rel
+in
+  thm' COMP fun_rel'
+end 
+
+
 end (* structure *)