diff -r 4b0563bc4b03 -r 7d8949da7d99 Quot/Nominal/Rsp.thy
--- a/Quot/Nominal/Rsp.thy	Wed Feb 24 17:32:43 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,118 +0,0 @@
-theory Rsp
-imports Abs
-begin
-
-ML {*
-fun define_quotient_type args tac ctxt =
-let
-  val mthd = Method.SIMPLE_METHOD tac
-  val mthdt = Method.Basic (fn _ => mthd)
-  val bymt = Proof.global_terminal_proof (mthdt, NONE)
-in
-  bymt (Quotient_Type.quotient_type args ctxt)
-end
-*}
-
-ML {*
-fun const_rsp lthy const =
-let
-  val nty = fastype_of (Quotient_Term.quotient_lift_const ("", const) lthy)
-  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_rel_id};
-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 repeat_mp thm = repeat_mp (mp OF [thm]) handle THM _ => thm
-*}
-
-ML {*
-fun prove_const_rsp bind consts tac ctxt =
-let
-  val rsp_goals = map (const_rsp 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_rel_id} 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)
-|> snd o Local_Theory.note ((bind, []), user_thms)
-end
-*}
-
-
-
-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)))
-*}
-
-ML {*
-fun constr_rsp_tac inj rsp equivps =
-let
-  val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps
-in
-  REPEAT o rtac impI THEN'
-  simp_tac (HOL_ss addsimps inj) THEN'
-  (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)) THEN_ALL_NEW
-  (asm_simp_tac HOL_ss THEN_ALL_NEW (
-   rtac @{thm exI[of _ "0 :: perm"]} THEN'
-   asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @
-     @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv}))
-  ))
-end
-*}
-
-(* Testing code
-local_setup {* prove_const_rsp @{binding fv_rtrm2_rsp} [@{term rbv2}]
-  (fn _ => fv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms fv_rtrm2_fv_rassign.simps} 1) *}*)
-
-(*ML {*
-  val rsp_goals = map (const_rsp @{context}) [@{term rbv2}]
-  val (fixed, user_goals) = split_list (map (get_rsp_goal @{theory}) rsp_goals)
-  val fixed' = distinct (op =) (flat fixed)
-  val user_goal = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj user_goals)
-*}
-prove ug: {* user_goal *}
-ML_prf {*
-val induct = @{thm alpha_rtrm2_alpha_rassign.inducts(2)}
-val fv_simps = @{thms rbv2.simps}
-*} 
-*)
-
-end