--- a/Quot/Nominal/Rsp.thy Wed Feb 24 09:56:12 2010 +0100
+++ b/Quot/Nominal/Rsp.thy Wed Feb 24 09:56:32 2010 +0100
@@ -14,7 +14,7 @@
*}
ML {*
-fun const_rsp const lthy =
+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);
@@ -23,13 +23,17 @@
end
*}
+(* Replaces bounds by frees and meta implications by implications *)
ML {*
-fun remove_alls trm =
+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
- ((map fst vars), subst_bounds (fs, (strip_all_body trm)))
+ (fixes, fold (curry HOLogic.mk_imp) prems concl)
end
*}
@@ -41,31 +45,41 @@
in
case (SINGLE (tac 1) goalstate) of
NONE => error "rsp_goal failed"
- | SOME th => remove_alls (term_of (cprem_of th 1))
+ | SOME th => prepare_goal (term_of (cprem_of th 1))
end
*}
ML {*
-fun prove_const_rsp bind const tac ctxt =
+fun repeat_mp thm = repeat_mp (mp OF [thm]) handle THM _ => thm
+*}
+
+ML {*
+fun prove_const_rsp bind consts tac ctxt =
let
- val rsp_goal = const_rsp const ctxt
+ val rsp_goals = map (const_rsp ctxt) consts
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
+ 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_thm])
-|> snd o Local_Theory.note ((bind, []), [user_thm])
+ ((Binding.empty, [Attrib.internal (fn _ => Quotient_Info.rsp_rules_add)]), rsp_thms)
+|> snd o Local_Theory.note ((bind, []), user_thms)
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))
+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 {*
@@ -73,7 +87,7 @@
let
val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps
in
- REPEAT o rtac @{thm fun_rel_id} THEN'
+ 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 (
@@ -84,5 +98,21 @@
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
--- a/Quot/Nominal/Terms.thy Wed Feb 24 09:56:12 2010 +0100
+++ b/Quot/Nominal/Terms.thy Wed Feb 24 09:56:32 2010 +0100
@@ -133,17 +133,18 @@
*}
print_theorems
-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}
+thm alpha_rtrm1_alpha_bp.induct
+local_setup {* prove_const_rsp @{binding fv_rtrm1_rsp} [@{term fv_rtrm1}]
+ (fn _ => fvbv_rsp_tac @{thm alpha_rtrm1_alpha_bp.inducts(1)} @{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 rLm1_rsp} @{term rLm1}
+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}
+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"}
+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]
@@ -326,20 +327,19 @@
*}
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}
+local_setup {* prove_const_rsp @{binding fv_rtrm2_rsp} [@{term fv_rtrm2}, @{term fv_rassign}]
+ (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.induct} @{thms fv_rtrm2_fv_rassign.simps} 1) *}
+local_setup {* prove_const_rsp @{binding rbv2_rsp} [@{term rbv2}]
+ (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms rbv2.simps} 1) *}
+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}
+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}
+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"}
+local_setup {* prove_const_rsp @{binding rLt2_rsp} [@{term rLt2}]
+ (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp rbv2_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) *}