# HG changeset patch # User Cezary Kaliszyk # Date 1266946052 -3600 # Node ID a41c3a1051044a8c52de96dbb2c9638c2c81d3ea # Parent ec2e0116779e2197175a93813bd88366ab9f90e1 rsp for bv; the only issue is that it requires an appropriate induction principle. diff -r ec2e0116779e -r a41c3a105104 Quot/Nominal/Rsp.thy --- a/Quot/Nominal/Rsp.thy Tue Feb 23 16:12:30 2010 +0100 +++ b/Quot/Nominal/Rsp.thy Tue Feb 23 18:27: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 diff -r ec2e0116779e -r a41c3a105104 Quot/Nominal/Terms.thy --- a/Quot/Nominal/Terms.thy Tue Feb 23 16:12:30 2010 +0100 +++ b/Quot/Nominal/Terms.thy Tue Feb 23 18:27: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 \ rtrm1 \ rtrm1"} +local_setup {* prove_const_rsp @{binding permute_rtrm1_rsp} [@{term "permute :: perm \ rtrm1 \ 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 \2 y \ fv_rtrm2 x = fv_rtrm2 y" sorry -lemma bv2_rsp: "x \2b y \ 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 \ rtrm2 \ 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 \ rtrm2 \ rtrm2"}] (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha2_eqvt}) 1) *}