# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269544377 -3600
# Node ID f731e9aff8664b34468979735529824036f2d30f
# Parent  4b949985cf5771f91b2915c83f9a25294a060474
Proper bn_rsp, for bn functions calling each other.

diff -r 4b949985cf57 -r f731e9aff866 Nominal/ExCoreHaskell.thy
--- a/Nominal/ExCoreHaskell.thy	Thu Mar 25 17:30:46 2010 +0100
+++ b/Nominal/ExCoreHaskell.thy	Thu Mar 25 20:12:57 2010 +0100
@@ -5,7 +5,6 @@
 (* core haskell *)
 
 ML {* val _ = recursive := false *}
-ML {* val _ = cheat_bn_rsp := true *}
 ML {* val _ = cheat_const_rsp := true *}
 ML {* val _ = cheat_alpha_bn_rsp := true *}
 atom_decl var
diff -r 4b949985cf57 -r f731e9aff866 Nominal/ExLet.thy
--- a/Nominal/ExLet.thy	Thu Mar 25 17:30:46 2010 +0100
+++ b/Nominal/ExLet.thy	Thu Mar 25 20:12:57 2010 +0100
@@ -1,5 +1,5 @@
 theory ExLet
-imports "Parser"
+imports "Parser" "../Attic/Prove"
 begin
 
 text {* example 3 or example 5 from Terms.thy *}
@@ -8,7 +8,6 @@
 
 ML {* val _ = recursive := false  *}
 
-
 nominal_datatype trm =
   Vr "name"
 | Ap "trm" "trm"
@@ -23,6 +22,8 @@
   "bn Lnil = {}"
 | "bn (Lcons x t l) = {atom x} \<union> (bn l)"
 
+
+
 thm trm_lts.fv
 thm trm_lts.eq_iff
 thm trm_lts.bn
diff -r 4b949985cf57 -r f731e9aff866 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Thu Mar 25 17:30:46 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 25 20:12:57 2010 +0100
@@ -1150,4 +1150,56 @@
 end
 *}
 
+ML {*
+fun prove_by_alpha_induct alphas build_goal ind utac inputs ctxt =
+let
+  val tys = map (domain_type o fastype_of) alphas;
+  val names = Datatype_Prop.make_tnames tys;
+  val (namesl, ctxt') = Variable.variant_fixes names ctxt;
+  val (namesr, ctxt'') = Variable.variant_fixes names ctxt';
+  val freesl = map Free (namesl ~~ tys);
+  val freesr = map Free (namesr ~~ tys);
+  val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ (freesl ~~ freesr))) inputs ctxt'';
+  val gls = flat gls_lists;
+  fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls;
+  val trm_gl_lists = map trm_gls_map freesl;
+  val trm_gls = map mk_conjl trm_gl_lists;
+  val pgls = map
+    (fn ((alpha, gl), (l, r)) => HOLogic.mk_imp (alpha $ l $ r, gl)) 
+    ((alphas ~~ trm_gls) ~~ (freesl ~~ freesr))
+  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj pgls);
+(*  val _ = tracing (PolyML.makestring gl); *)
+  fun tac {context,...} = (ind_tac ind THEN_ALL_NEW split_conjs THEN_ALL_NEW utac) 1
+  val th_loc = Goal.prove ctxt'' [] [] gl tac
+  val ths_loc = HOLogic.conj_elims th_loc
+  val ths = Variable.export ctxt'' ctxt ths_loc
+in
+  filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths
 end
+*}
+
+ML {*
+fun build_rsp_gl alphas fnctn ctxt =
+let
+  val typ = domain_type (fastype_of fnctn);
+  val (argl, argr) = the (AList.lookup (op=) alphas typ);
+in
+  ([HOLogic.mk_eq (fnctn $ argl, fnctn $ argr)], ctxt)
+end
+*}
+
+ML {*
+fun fvbv_rsp_tac' simps ctxt =
+  asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: simps)) THEN_ALL_NEW
+  REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW
+  TRY o blast_tac (claset_of ctxt)
+*}
+
+ML {*
+fun build_fvbv_rsps alphas ind simps fnctns ctxt =
+  prove_by_alpha_induct alphas build_rsp_gl ind (fvbv_rsp_tac' simps ctxt) fnctns ctxt
+*}
+
+end
diff -r 4b949985cf57 -r f731e9aff866 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Thu Mar 25 17:30:46 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 25 20:12:57 2010 +0100
@@ -374,10 +374,10 @@
   (* Could be done nicer *)
   val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts);
   val _ = tracing "Proving respects";
+  val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;
   val (bns_rsp_pre, lthy9) = fold_map (
     fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] (fn _ =>
-       if !cheat_bn_rsp then (Skip_Proof.cheat_tac thy) else
-       fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs lthy8 1)) bns lthy8;
+       resolve_tac bns_rsp_pre' 1)) bns lthy8;
   val bns_rsp = flat (map snd bns_rsp_pre);
   fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
     else fvbv_rsp_tac alpha_induct fv_def lthy8 1;