--- a/Nominal/Rsp.thy	Wed Aug 25 22:55:42 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,224 +0,0 @@
-theory Rsp
-imports Abs Tacs
-begin
-
-ML {*
-fun const_rsp qtys lthy const =
-let
-  val nty = Quotient_Term.derive_qtyp lthy qtys (fastype_of const)
-  val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty);
-in
-  HOLogic.mk_Trueprop (rel $ const $ const)
-end
-*}
-
-(* Replaces bounds by frees and meta implications by implications *)
-ML {*
-fun prepare_goal trm =
-let
-  val vars = strip_all_vars trm
-  val fs = rev (map Free vars)
-  val (fixes, no_alls) = ((map fst vars), subst_bounds (fs, (strip_all_body trm)))
-  val prems = map HOLogic.dest_Trueprop (Logic.strip_imp_prems no_alls)
-  val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl no_alls)
-in
-  (fixes, fold (curry HOLogic.mk_imp) prems concl)
-end
-*}
-
-ML {*
-fun get_rsp_goal thy trm =
-let
-  val goalstate = Goal.init (cterm_of thy trm);
-  val tac = REPEAT o rtac @{thm fun_relI};
-in
-  case (SINGLE (tac 1) goalstate) of
-    NONE => error "rsp_goal failed"
-  | SOME th => prepare_goal (term_of (cprem_of th 1))
-end
-*}
-
-ML {*
-fun prove_const_rsp qtys bind consts tac ctxt =
-let
-  val rsp_goals = map (const_rsp qtys ctxt) consts
-  val thy = ProofContext.theory_of ctxt
-  val (fixed, user_goals) = split_list (map (get_rsp_goal thy) rsp_goals)
-  val fixed' = distinct (op =) (flat fixed)
-  val user_goal = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj user_goals)
-  val user_thm = Goal.prove ctxt fixed' [] user_goal tac
-  val user_thms = map repeat_mp (HOLogic.conj_elims user_thm)
-  fun tac _ = (REPEAT o rtac @{thm fun_relI} THEN' resolve_tac user_thms THEN_ALL_NEW atac) 1
-  val rsp_thms = map (fn gl => Goal.prove ctxt [] [] gl tac) rsp_goals
-in
-   ctxt
-|> snd o Local_Theory.note 
-  ((Binding.empty, [Attrib.internal (fn _ => Quotient_Info.rsp_rules_add)]), rsp_thms)
-|> Local_Theory.note ((bind, []), user_thms)
-end
-*}
-
-ML {*
-fun fvbv_rsp_tac induct fvbv_simps ctxt =
-  rtac induct THEN_ALL_NEW
-  (TRY o rtac @{thm TrueI}) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps (@{thms prod_fv.simps prod_rel.simps set.simps append.simps alphas} @ 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 = maps (fn x => [sym OF [x]] handle _ => []) (Nominal_ThmDecls.get_eqvts_thms ctxt)
-fun all_eqvts ctxt =
-  Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt
-*}
-
-ML {*
-fun constr_rsp_tac inj rsp =
-  REPEAT o rtac impI THEN'
-  simp_tac (HOL_ss addsimps inj) THEN' split_conj_tac THEN_ALL_NEW
-  (asm_simp_tac HOL_ss THEN_ALL_NEW (
-   REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW
-   simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
-   asm_full_simp_tac (HOL_ss addsimps (rsp @
-     @{thms split_conv alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left prod_rel.simps prod_fv.simps}))
-  ))
-*}
-
-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
-*}
-
-(** alpha_bn_rsp **)
-
-lemma equivp_rspl:
-  "equivp r \<Longrightarrow> r a b \<Longrightarrow> r a c = r b c"
-  unfolding equivp_reflp_symp_transp symp_def transp_def 
-  by blast
-
-lemma equivp_rspr:
-  "equivp r \<Longrightarrow> r a b \<Longrightarrow> r c a = r c b"
-  unfolding equivp_reflp_symp_transp symp_def transp_def 
-  by blast
-
-ML {*
-fun alpha_bn_rsp_tac simps res exhausts a ctxt =
-  rtac allI THEN_ALL_NEW
-  case_rules_tac ctxt a exhausts THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps simps addsimps @{thms alphas}) THEN_ALL_NEW
-  TRY o REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<and>"]}) THEN_ALL_NEW
-  TRY o eresolve_tac res THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps simps)
-*}
-
-
-ML {*
-fun build_alpha_bn_rsp_gl a alphas alpha_bn ctxt =
-let
-  val ty = domain_type (fastype_of alpha_bn);
-  val (l, r) = the (AList.lookup (op=) alphas ty);
-in
-  ([HOLogic.mk_all (a, ty, HOLogic.mk_eq (alpha_bn $ l $ Bound 0, alpha_bn $ r $ Bound 0)),
-    HOLogic.mk_all (a, ty, HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r))], ctxt)
-end
-*}
-
-ML {*
-fun prove_alpha_bn_rsp alphas ind simps equivps exhausts alpha_bns ctxt =
-let
-  val ([a], ctxt') = Variable.variant_fixes ["a"] ctxt;
-  val resl = map (fn x => @{thm equivp_rspl} OF [x]) equivps;
-  val resr = map (fn x => @{thm equivp_rspr} OF [x]) equivps;
-  val ths_loc = prove_by_rel_induct alphas (build_alpha_bn_rsp_gl a) ind
-    (alpha_bn_rsp_tac simps (resl @ resr) exhausts a) alpha_bns ctxt
-in
-  Variable.export ctxt' ctxt ths_loc
-end
-*}
-
-ML {*
-fun build_alpha_alpha_bn_gl alphas alpha_bn ctxt =
-let
-  val ty = domain_type (fastype_of alpha_bn);
-  val (l, r) = the (AList.lookup (op=) alphas ty);
-in
-  ([alpha_bn $ l $ r], ctxt)
-end
-*}
-
-lemma exi_same: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q p) \<Longrightarrow> \<exists>pi. Q pi"
-  by auto
-
-ML {*
-fun prove_alpha_alphabn alphas ind simps alpha_bns ctxt =
-  prove_by_rel_induct alphas build_alpha_alpha_bn_gl ind
-    (fn _ => asm_full_simp_tac (HOL_ss addsimps simps addsimps @{thms alphas})
-     THEN_ALL_NEW split_conj_tac THEN_ALL_NEW (TRY o etac @{thm exi_same})
-     THEN_ALL_NEW asm_full_simp_tac HOL_ss) alpha_bns ctxt
-*}
-
-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 alphas2}) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps (@{thms alphas} @ 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_rel_induct alphas build_rsp_gl ind (fvbv_rsp_tac' simps) fnctns ctxt
-*}
-
-end