# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269263255 -3600
# Node ID 69c9d53fb8173a8ad5ba7d7c809eaa87bbc8f0ac
# Parent  b39108f42638a3a3245784a2b7416e534a08c5c0# Parent  0368aef38e6a710c74c242ba0f3544402b669465
merge

diff -r 0368aef38e6a -r 69c9d53fb817 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Mon Mar 22 11:55:29 2010 +0100
+++ b/Nominal/Parser.thy	Mon Mar 22 14:07:35 2010 +0100
@@ -265,13 +265,11 @@
 end
 *}
 
-(* These 2 are critical, we don't know how to do it in term5 *)
-ML {* val cheat_fv_rsp = Unsynchronized.ref true *}
 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref true *}
-
 ML {* val cheat_equivp = Unsynchronized.ref true *}
 
-(* These 2 are not needed any more *)
+(* These 3 are not needed any more *)
+ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
 ML {* val cheat_fv_eqvt = Unsynchronized.ref false *}
 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
 
@@ -332,7 +330,8 @@
     else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff @ raw_fv_bv_eqvt) lthy6a 1
   val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6a;
   val _ = tracing "Proving equivalence";
-  val fv_alpha_all = combine_fv_alpha_bns (fv_ts_nobn, fv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
+  val (rfv_ts_nobn, rfv_ts_bn) = chop (length perms) ordered_fv_ts;
+  val fv_alpha_all = combine_fv_alpha_bns (rfv_ts_nobn, rfv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
   val reflps = build_alpha_refl fv_alpha_all induct alpha_eq_iff lthy6a;
   val alpha_equivp =
     if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn
@@ -356,11 +355,15 @@
   val _ = tracing "Proving respects";
   val (bns_rsp_pre, lthy9) = fold_map (
     fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t]
-      (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs 1)) bns lthy8;
+      (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs lthy8 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 1;
-  val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts fv_rsp_tac lthy9
+    else fvbv_rsp_tac alpha_induct fv_def lthy8 1;
+  val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9;
+  val (fv_rsp_pre, lthy10) = fold_map
+    (fn fv => fn ctxt => prove_const_rsp Binding.empty [fv]
+    (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) fv_ts lthy9;
+  val fv_rsp = flat (map snd fv_rsp_pre);
   val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
   val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11;
diff -r 0368aef38e6a -r 69c9d53fb817 Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Mon Mar 22 11:55:29 2010 +0100
+++ b/Nominal/Rsp.thy	Mon Mar 22 14:07:35 2010 +0100
@@ -73,20 +73,21 @@
 end
 *}
 
-
+ML {*
+fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct
+*}
 
 ML {*
-fun fvbv_rsp_tac induct fvbv_simps =
-  ((((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
-  (TRY o rtac @{thm TrueI})) THEN_ALL_NEW
-  asm_full_simp_tac
-  (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps))
-  THEN_ALL_NEW (REPEAT o eresolve_tac [conjE, exE] THEN'
-  asm_full_simp_tac
-  (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps))))
+fun fvbv_rsp_tac induct fvbv_simps ctxt =
+  ind_tac induct THEN_ALL_NEW
+  (TRY o rtac @{thm TrueI}) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)) THEN_ALL_NEW
+  REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW
+  TRY o blast_tac (claset_of ctxt)
 *}
 
-
 ML {*
 fun sym_eqvts ctxt = map (fn x => sym OF [x]) (Nominal_ThmDecls.get_eqvts_thms ctxt)
 fun all_eqvts ctxt =
@@ -124,10 +125,6 @@
 *)
 
 ML {*
-fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct
-*}
-
-ML {*
 fun build_eqvts_tac induct simps ctxt inds _ = (Datatype_Aux.indtac induct inds THEN_ALL_NEW
     (asm_full_simp_tac (HOL_ss addsimps
       (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1
@@ -219,4 +216,48 @@
   build_eqvts Binding.empty [t] (build_eqvts_tac (nth inducts n) simps ctxt) ctxt
 *}
 
+ML {*
+fun prove_fv_rsp fv_alphas_lst all_alphas tac ctxt =
+let
+  val (fvs_alphas, ls) = split_list fv_alphas_lst;
+  val (fv_ts, alpha_ts) = split_list fvs_alphas;
+  val tys = map (domain_type o fastype_of) alpha_ts;
+  val names = Datatype_Prop.make_tnames tys;
+  val names2 = Name.variant_list names names;
+  val args = map Free (names ~~ tys);
+  val args2 = map Free (names2 ~~ tys);
+  fun mk_fv_rsp arg arg2 (fv, alpha) = HOLogic.mk_eq ((fv $ arg), (fv $ arg2));
+  fun fv_rsp_arg (((fv, alpha), (arg, arg2)), l) =
+    HOLogic.mk_imp (
+     (alpha $ arg $ arg2),
+     (foldr1 HOLogic.mk_conj
+       (HOLogic.mk_eq (fv $ arg, fv $ arg2) ::
+       (map (mk_fv_rsp arg arg2) l))));
+  val nobn_eqs = map fv_rsp_arg (((fv_ts ~~ alpha_ts) ~~ (args ~~ args2)) ~~ ls);
+  fun mk_fv_rsp_bn arg arg2 (fv, alpha) =
+    HOLogic.mk_imp (
+      (alpha $ arg $ arg2),
+      HOLogic.mk_eq ((fv $ arg), (fv $ arg2)));
+  fun fv_rsp_arg_bn ((arg, arg2), l) =
+    map (mk_fv_rsp_bn arg arg2) l;
+  val bn_eqs = flat (map fv_rsp_arg_bn ((args ~~ args2) ~~ ls));
+  val (_, add_alphas) = chop (length (nobn_eqs @ bn_eqs)) all_alphas;
+  val atys = map (domain_type o fastype_of) add_alphas;
+  val anames = Name.variant_list (names @ names2) (Datatype_Prop.make_tnames atys);
+  val aargs = map Free (anames ~~ atys);
+  val aeqs = map2 (fn alpha => fn arg => HOLogic.mk_imp (alpha $ arg $ arg, @{term True}))
+    add_alphas aargs;
+  val eq = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (nobn_eqs @ bn_eqs @ aeqs));
+  val th = Goal.prove ctxt (names @ names2) [] eq tac;
+  val ths = HOLogic.conj_elims th;
+  val (ths_nobn, ths_bn) = chop (length ls) ths;
+  fun project (th, l) =
+    Project_Rule.projects ctxt (1 upto (length l + 1)) (hd (Project_Rule.projections ctxt th))
+  val ths_nobn_pr = map project (ths_nobn ~~ ls);
+in
+  (flat ths_nobn_pr @ ths_bn)
 end
+*}
+
+
+end
diff -r 0368aef38e6a -r 69c9d53fb817 TODO
--- a/TODO	Mon Mar 22 11:55:29 2010 +0100
+++ b/TODO	Mon Mar 22 14:07:35 2010 +0100
@@ -8,7 +8,7 @@
   ty1_tyn.induct
   ty1_tyn.inducts
   instance ty1 and tyn :: fs
-  ty1_tyn.supp            for too many bindings empty
+  ty1_tyn.supp            empty when for too many bindings
 
 Smaller things:
 
@@ -27,14 +27,17 @@
 - check support equations for more bindings per constructor
 
 - automate the proofs that are currently proved with sorry:
-  alpha_equivp, fv_rsp, alpha_bn_rsp
+  alpha_equivp, alpha_bn_rsp
 
 - store information about defined nominal datatypes, so that
   it can be used to define new types that depend on these
 
-- make 3 versions of Abs
-
 - make parser aware of bn functions that call other bn functions
   and reflect it in the datastructure passed to Fv/Alpha generation
 
 - make parser aware of recursive and of different versions of abs
+
+Less important:
+
+- fv_rsp uses 'blast' to show goals of the type:
+  a u b = c u d   ==>  a u x u b = c u x u d