--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Nominal/Rsp.thy	Tue Feb 23 16:32:04 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

--- a/Quot/Nominal/Terms.thy	Tue Feb 23 16:31:40 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Tue Feb 23 16:32:04 2010 +0100
@@ -1,5 +1,5 @@
 theory Terms
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "../../Attic/Prove"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../../Attic/Prove"
 begin
 
 atom_decl name
@@ -32,7 +32,7 @@
 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *}
 thm permute_rtrm1_permute_bp.simps
 
-local_setup {* 
+local_setup {*
   snd o define_fv_alpha "Terms.rtrm1"
   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
   [[], [[]], [[], []]]] *}
@@ -120,20 +120,8 @@
   (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *}
 thm alpha1_equivp
 
-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
-*}
-
-local_setup  {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))] 
-  (rtac @{thm alpha1_equivp(1)} 1)
-*}
+local_setup  {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))]
+  (rtac @{thm alpha1_equivp(1)} 1) *}
 
 local_setup {*
 (fn ctxt => ctxt
@@ -145,44 +133,18 @@
 *}
 print_theorems
 
-prove fv_rtrm1_rsp': {*
- (@{term Trueprop} $ (Quotient_Term.equiv_relation_chk @{context} (fastype_of @{term fv_rtrm1}, fastype_of @{term fv_trm1}) $ @{term fv_rtrm1} $ @{term fv_rtrm1})) *}
-by (tactic {*
-  (rtac @{thm fun_rel_id} THEN'
-  eresolve_tac @{thms alpha_rtrm1_alpha_bp.inducts} THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps @{thms alpha_gen fv_rtrm1_fv_bp.simps})) 1 *})
-
-
-lemmas fv_rtrm1_rsp = apply_rsp'[OF fv_rtrm1_rsp']
-
-(* We need this since 'prove' doesn't support attributes *)
-lemma [quot_respect]: "(alpha_rtrm1 ===> op =) fv_rtrm1 fv_rtrm1"
-  by (rule fv_rtrm1_rsp')
-
-ML {*
-fun contr_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
-*}
-
-lemma [quot_respect]:
- "(op = ===> alpha_rtrm1) rVr1 rVr1"
- "(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1"
- "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) rLm1 rLm1"
- "(op = ===> alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rLt1 rLt1"
-apply (tactic {* contr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1 *})+
-done
-
+local_setup {* prove_const_rsp @{binding fv_rtrm1_rsp} @{term fv_rtrm1}
+  (fn _ => fv_rsp_tac @{thms alpha_rtrm1_alpha_bp.inducts} @{thms fv_rtrm1_fv_bp.simps} 1) *}
+local_setup {* prove_const_rsp @{binding rVr1_rsp} @{term rVr1}
+  (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
+local_setup {* prove_const_rsp @{binding rAp1_rsp} @{term rAp1}
+  (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
+local_setup {* prove_const_rsp @{binding rLm1_rsp} @{term rLm1}
+  (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
+local_setup {* prove_const_rsp @{binding rLt1_rsp} @{term rLt1}
+  (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
+local_setup {* prove_const_rsp @{binding permute_rtrm1_rsp} @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"}
+  (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) 1) *}
 
 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]
 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted]
@@ -195,10 +157,6 @@
 is
   "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"
 
-lemma [quot_respect]:
-  "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) permute permute"
-  by (simp add: alpha1_eqvt)
-
 lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted]
 
 instance
@@ -209,11 +167,10 @@
 
 end
 
-lemmas fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted]
-
-lemmas fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted]
-
-lemmas alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+lemmas
+    fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted]
+and fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted]
+and alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
 lemma lm1_supp_pre:
   shows "(supp (atom x, t)) supports (Lm1 x t) "
@@ -352,12 +309,10 @@
   (build_equivps [@{term alpha_rtrm2}, @{term alpha_rassign}] @{thm rtrm2_rassign.induct} @{thm alpha_rtrm2_alpha_rassign.induct} @{thms rtrm2.inject rassign.inject} @{thms alpha2_inj} @{thms rtrm2.distinct rassign.distinct} @{thms alpha_rtrm2.cases alpha_rassign.cases} @{thms alpha2_eqvt} ctxt)) ctxt)) *}
 thm alpha2_equivp
 
-
-quotient_type
-  trm2 = rtrm2 / alpha_rtrm2
-and
-  assign = rassign / alpha_rassign
-  by (rule alpha2_equivp(1)) (rule alpha2_equivp(2))
+local_setup  {* define_quotient_type 
+  [(([], @{binding trm2}, NoSyn), (@{typ rtrm2}, @{term alpha_rtrm2})),
+   (([], @{binding assign}, NoSyn), (@{typ rassign}, @{term alpha_rassign}))]
+  ((rtac @{thm alpha2_equivp(1)} 1) THEN (rtac @{thm alpha2_equivp(2)}) 1) *}
 
 local_setup {*
 (fn ctxt => ctxt
@@ -371,6 +326,22 @@
 *}
 print_theorems
 
+(*local_setup {* prove_const_rsp @{binding fv_rtrm2_rsp} @{term fv_rtrm2}
+  (fn _ => fv_rsp_tac @{thms alpha_rtrm2_alpha_rassign.inducts} @{thms fv_rtrm2_fv_rassign.simps} 1) *} *)
+lemma fv_rtrm2_rsp: "x \<approx>2 y \<Longrightarrow> fv_rtrm2 x = fv_rtrm2 y" sorry
+lemma bv2_rsp: "x \<approx>2b y \<Longrightarrow> rbv2 x = rbv2 y" sorry
+
+local_setup {* prove_const_rsp @{binding rVr2_rsp} @{term rVr2}
+  (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}
+local_setup {* prove_const_rsp @{binding rAp2_rsp} @{term rAp2}
+  (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}
+local_setup {* prove_const_rsp @{binding rLm2_rsp} @{term rLm2}
+  (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}
+local_setup {* prove_const_rsp @{binding rLt2_rsp} @{term rLt2}
+  (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp bv2_rsp} @{thms alpha2_equivp} 1) *}
+local_setup {* prove_const_rsp @{binding permute_rtrm2_rsp} @{term "permute :: perm \<Rightarrow> rtrm2 \<Rightarrow> rtrm2"}
+  (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha2_eqvt}) 1) *}
+
 
 section {*** lets with many assignments ***}