# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1281527637 -28800
# Node ID 79e4938808017acf11a947d3aa74cb84e6c3bb84
# Parent  e2759a4dad4b8a1a965405efc4e7bcd975807539
rsp for constructors

diff -r e2759a4dad4b -r 79e493880801 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Wed Aug 11 16:23:50 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Wed Aug 11 19:53:57 2010 +0800
@@ -21,6 +21,8 @@
 where
   "bn (As x y t) = {atom x}"
 
+
+
 thm alpha_sym_thms
 thm alpha_trans_thms
 thm size_eqvt
@@ -34,9 +36,10 @@
 thm perm_simps
 thm perm_laws
 thm funs_rsp
+thm constrs_rsp
 
-declare size_rsp[quot_respect]
-declare funs_rsp[quot_respect]
+declare constrs_rsp[quot_respect]
+(* declare funs_rsp[quot_respect] *)
 
 typ trm
 typ assg
@@ -47,33 +50,6 @@
 term fv_trm
 term alpha_bn
 
-lemma exi_zero: "P 0 \<Longrightarrow> \<exists>(x::perm). P x" by auto
-
-ML {* 
-  val pre_ss = @{thms fun_rel_def}
-  val post_ss = @{thms alphas prod_alpha_def prod_rel.simps 
-    prod_fv.simps fresh_star_zero permute_zero funs_rsp prod.cases alpha_bn_imps}
-
-  val tac = 
-    asm_full_simp_tac (HOL_ss addsimps pre_ss)
-    THEN' REPEAT o (resolve_tac @{thms allI impI})
-    THEN' resolve_tac @{thms alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros} 
-    THEN_ALL_NEW (TRY o (rtac @{thm exi_zero}) THEN' asm_full_simp_tac (HOL_ss addsimps post_ss))
-*}
-
-lemma [quot_respect]: 
-  "(op= ===> alpha_trm_raw) Var_raw Var_raw"
-  "(alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) App_raw App_raw"
-  "(op= ===> alpha_trm_raw ===> alpha_trm_raw) Lam_raw Lam_raw"
-  "(alpha_assg_raw ===> alpha_trm_raw ===> alpha_trm_raw) Let_raw Let_raw"
-  "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw)
-     Foo_raw Foo_raw"
-  "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw) Bar_raw Bar_raw"
-  "(op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) Baz_raw Baz_raw"
-  "(op = ===> op = ===> alpha_trm_raw ===> alpha_assg_raw) As_raw As_raw"
-apply(tactic {* ALLGOALS tac *})
-sorry
-
 lemma [quot_respect]:
   "(op = ===> alpha_trm_raw ===> alpha_trm_raw) permute permute"
 apply(simp)
diff -r e2759a4dad4b -r 79e493880801 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Wed Aug 11 16:23:50 2010 +0800
+++ b/Nominal/NewParser.thy	Wed Aug 11 19:53:57 2010 +0800
@@ -445,6 +445,8 @@
   val raw_size_rsp = raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct 
     (raw_size_thms @ raw_size_eqvt) lthy6
 
+  val raw_constrs_rsp = raw_constrs_rsp all_raw_constrs alpha_trms alpha_intros
+    (alpha_bn_imp_thms @ raw_funs_rsp) lthy6 
 
   (* defining the quotient type *)
   val _ = warning "Declaring the quotient types"
@@ -509,6 +511,7 @@
      ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), raw_size_eqvt)
      ||>> Local_Theory.note ((@{binding "size_simps"}, []), raw_size_thms)
      ||>> Local_Theory.note ((@{binding "size_rsp"}, []), raw_size_rsp)
+     ||>> Local_Theory.note ((@{binding "constrs_rsp"}, []), raw_constrs_rsp)
      ||>> Local_Theory.note ((@{binding "alpha_sym_thms"}, []), alpha_sym_thms)
      ||>> Local_Theory.note ((@{binding "alpha_trans_thms"}, []), alpha_trans_thms)
   
diff -r e2759a4dad4b -r 79e493880801 Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Wed Aug 11 16:23:50 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Wed Aug 11 19:53:57 2010 +0800
@@ -28,6 +28,7 @@
   val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> 
     term list -> thm -> thm list -> Proof.context -> thm list
   val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list
+  val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list
 
   val resolve_fun_rel: thm -> thm
 end
@@ -624,6 +625,7 @@
     (K (asm_full_simp_tac ss)) ctxt
 end
 
+
 (* respectfulness for size *)
 
 fun raw_size_rsp_aux all_alpha_trms alpha_induct simps ctxt =
@@ -644,6 +646,50 @@
 end
 
 
+(* respectfulness for constructors *)
+
+fun raw_constr_rsp_tac alpha_intros simps = 
+let
+  val pre_ss = HOL_ss addsimps @{thms fun_rel_def}
+  val post_ss = HOL_ss addsimps @{thms alphas prod_alpha_def prod_rel.simps 
+    prod_fv.simps fresh_star_zero permute_zero prod.cases} @ simps
+  (* funs_rsp alpha_bn_simps *)
+in
+  asm_full_simp_tac pre_ss
+  THEN' REPEAT o (resolve_tac @{thms allI impI})
+  THEN' resolve_tac alpha_intros
+  THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_ss)
+end
+
+
+fun raw_constrs_rsp constrs alpha_trms alpha_intros simps ctxt =
+let
+  val alpha_arg_tys = map (domain_type o fastype_of) alpha_trms
+  
+  fun lookup ty = 
+    case AList.lookup (op=) (alpha_arg_tys ~~ alpha_trms) ty of
+      NONE => HOLogic.eq_const ty
+    | SOME alpha => alpha 
+  
+  fun fun_rel_app t1 t2 = 
+    Const (@{const_name "fun_rel"}, dummyT) $ t1 $ t2
+
+  fun prep_goal trm =
+    trm
+    |> strip_type o fastype_of
+    |>> map lookup
+    ||> lookup
+    |> uncurry (fold_rev fun_rel_app)
+    |> (fn t => t $ trm $ trm)
+    |> Syntax.check_term ctxt
+    |> HOLogic.mk_Trueprop
+in
+  Goal.prove_multi ctxt [] [] (map prep_goal constrs)
+    (K (HEADGOAL 
+      (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac alpha_intros simps)))
+end
+
+
 (* resolve with @{thm fun_relI} *)
 
 fun resolve_fun_rel thm =