--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Nominal/Rsp.thy	Tue Feb 23 16:12:30 2010 +0100
@@ -0,0 +1,88 @@
+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 const lthy =
+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
+*}
+
+ML {*
+fun remove_alls trm =
+let
+  val vars = strip_all_vars trm
+  val fs = rev (map Free vars)
+in
+  ((map fst vars), subst_bounds (fs, (strip_all_body trm)))
+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 => remove_alls (term_of (cprem_of th 1))
+end
+*}
+
+ML {*
+fun prove_const_rsp bind const tac ctxt =
+let
+  val rsp_goal = const_rsp const ctxt
+  val thy = ProofContext.theory_of ctxt
+  val (fixed, user_goal) = get_rsp_goal thy rsp_goal
+  val user_thm = Goal.prove ctxt fixed [] user_goal tac
+  fun tac _ = (REPEAT o rtac @{thm fun_rel_id} THEN' rtac user_thm THEN_ALL_NEW atac) 1
+  val rsp_thm = Goal.prove ctxt [] [] rsp_goal tac
+in
+   ctxt
+|> snd o Local_Theory.note 
+  ((Binding.empty, [Attrib.internal (fn _ => Quotient_Info.rsp_rules_add)]), [rsp_thm])
+|> snd o Local_Theory.note ((bind, []), [user_thm])
+end
+*}
+
+ML {*
+fun fv_rsp_tac induct fv_simps =
+  eresolve_tac induct THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: fv_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 @{thm fun_rel_id} 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
+*}
+
+
+end