diff -r 92dc6cfa3a95 -r 3772bb3bd7ce Nominal/Rsp.thy --- a/Nominal/Rsp.thy Wed Aug 25 22:55:42 2010 +0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,224 +0,0 @@ -theory Rsp -imports Abs Tacs -begin - -ML {* -fun const_rsp qtys lthy const = -let - val nty = Quotient_Term.derive_qtyp lthy qtys (fastype_of const) - val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty); -in - HOLogic.mk_Trueprop (rel $ const $ const) -end -*} - -(* Replaces bounds by frees and meta implications by implications *) -ML {* -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 - (fixes, fold (curry HOLogic.mk_imp) prems concl) -end -*} - -ML {* -fun get_rsp_goal thy trm = -let - val goalstate = Goal.init (cterm_of thy trm); - val tac = REPEAT o rtac @{thm fun_relI}; -in - case (SINGLE (tac 1) goalstate) of - NONE => error "rsp_goal failed" - | SOME th => prepare_goal (term_of (cprem_of th 1)) -end -*} - -ML {* -fun prove_const_rsp qtys bind consts tac ctxt = -let - val rsp_goals = map (const_rsp qtys ctxt) consts - val thy = ProofContext.theory_of ctxt - 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_relI} 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_thms) -|> Local_Theory.note ((bind, []), user_thms) -end -*} - -ML {* -fun fvbv_rsp_tac induct fvbv_simps ctxt = - rtac induct THEN_ALL_NEW - (TRY o rtac @{thm TrueI}) THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps (@{thms prod_fv.simps prod_rel.simps set.simps append.simps alphas} @ fvbv_simps)) THEN_ALL_NEW - REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW - TRY o blast_tac (claset_of ctxt) -*} - -ML {* -fun sym_eqvts ctxt = maps (fn x => [sym OF [x]] handle _ => []) (Nominal_ThmDecls.get_eqvts_thms ctxt) -fun all_eqvts ctxt = - Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt -*} - -ML {* -fun constr_rsp_tac inj rsp = - REPEAT o rtac impI THEN' - simp_tac (HOL_ss addsimps inj) THEN' split_conj_tac THEN_ALL_NEW - (asm_simp_tac HOL_ss THEN_ALL_NEW ( - REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps (rsp @ - @{thms split_conv alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left prod_rel.simps prod_fv.simps})) - )) -*} - -ML {* -fun prove_fv_rsp fv_alphas_lst all_alphas tac ctxt = -let - val (fvs_alphas, ls) = split_list fv_alphas_lst; - val (fv_ts, alpha_ts) = split_list fvs_alphas; - val tys = map (domain_type o fastype_of) alpha_ts; - val names = Datatype_Prop.make_tnames tys; - val names2 = Name.variant_list names names; - val args = map Free (names ~~ tys); - val args2 = map Free (names2 ~~ tys); - fun mk_fv_rsp arg arg2 (fv, alpha) = HOLogic.mk_eq ((fv $ arg), (fv $ arg2)); - fun fv_rsp_arg (((fv, alpha), (arg, arg2)), l) = - HOLogic.mk_imp ( - (alpha $ arg $ arg2), - (foldr1 HOLogic.mk_conj - (HOLogic.mk_eq (fv $ arg, fv $ arg2) :: - (map (mk_fv_rsp arg arg2) l)))); - val nobn_eqs = map fv_rsp_arg (((fv_ts ~~ alpha_ts) ~~ (args ~~ args2)) ~~ ls); - fun mk_fv_rsp_bn arg arg2 (fv, alpha) = - HOLogic.mk_imp ( - (alpha $ arg $ arg2), - HOLogic.mk_eq ((fv $ arg), (fv $ arg2))); - fun fv_rsp_arg_bn ((arg, arg2), l) = - map (mk_fv_rsp_bn arg arg2) l; - val bn_eqs = flat (map fv_rsp_arg_bn ((args ~~ args2) ~~ ls)); - val (_, add_alphas) = chop (length (nobn_eqs @ bn_eqs)) all_alphas; - val atys = map (domain_type o fastype_of) add_alphas; - val anames = Name.variant_list (names @ names2) (Datatype_Prop.make_tnames atys); - val aargs = map Free (anames ~~ atys); - val aeqs = map2 (fn alpha => fn arg => HOLogic.mk_imp (alpha $ arg $ arg, @{term True})) - add_alphas aargs; - val eq = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (nobn_eqs @ bn_eqs @ aeqs)); - val th = Goal.prove ctxt (names @ names2) [] eq tac; - val ths = HOLogic.conj_elims th; - val (ths_nobn, ths_bn) = chop (length ls) ths; - fun project (th, l) = - Project_Rule.projects ctxt (1 upto (length l + 1)) (hd (Project_Rule.projections ctxt th)) - val ths_nobn_pr = map project (ths_nobn ~~ ls); -in - (flat ths_nobn_pr @ ths_bn) -end -*} - -(** alpha_bn_rsp **) - -lemma equivp_rspl: - "equivp r \ r a b \ r a c = r b c" - unfolding equivp_reflp_symp_transp symp_def transp_def - by blast - -lemma equivp_rspr: - "equivp r \ r a b \ r c a = r c b" - unfolding equivp_reflp_symp_transp symp_def transp_def - by blast - -ML {* -fun alpha_bn_rsp_tac simps res exhausts a ctxt = - rtac allI THEN_ALL_NEW - case_rules_tac ctxt a exhausts THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps simps addsimps @{thms alphas}) THEN_ALL_NEW - TRY o REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \"]}) THEN_ALL_NEW - TRY o eresolve_tac res THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps simps) -*} - - -ML {* -fun build_alpha_bn_rsp_gl a alphas alpha_bn ctxt = -let - val ty = domain_type (fastype_of alpha_bn); - val (l, r) = the (AList.lookup (op=) alphas ty); -in - ([HOLogic.mk_all (a, ty, HOLogic.mk_eq (alpha_bn $ l $ Bound 0, alpha_bn $ r $ Bound 0)), - HOLogic.mk_all (a, ty, HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r))], ctxt) -end -*} - -ML {* -fun prove_alpha_bn_rsp alphas ind simps equivps exhausts alpha_bns ctxt = -let - val ([a], ctxt') = Variable.variant_fixes ["a"] ctxt; - val resl = map (fn x => @{thm equivp_rspl} OF [x]) equivps; - val resr = map (fn x => @{thm equivp_rspr} OF [x]) equivps; - val ths_loc = prove_by_rel_induct alphas (build_alpha_bn_rsp_gl a) ind - (alpha_bn_rsp_tac simps (resl @ resr) exhausts a) alpha_bns ctxt -in - Variable.export ctxt' ctxt ths_loc -end -*} - -ML {* -fun build_alpha_alpha_bn_gl alphas alpha_bn ctxt = -let - val ty = domain_type (fastype_of alpha_bn); - val (l, r) = the (AList.lookup (op=) alphas ty); -in - ([alpha_bn $ l $ r], ctxt) -end -*} - -lemma exi_same: "\(pi :: perm). P pi \ (\(p :: perm). P p \ Q p) \ \pi. Q pi" - by auto - -ML {* -fun prove_alpha_alphabn alphas ind simps alpha_bns ctxt = - prove_by_rel_induct alphas build_alpha_alpha_bn_gl ind - (fn _ => asm_full_simp_tac (HOL_ss addsimps simps addsimps @{thms alphas}) - THEN_ALL_NEW split_conj_tac THEN_ALL_NEW (TRY o etac @{thm exi_same}) - THEN_ALL_NEW asm_full_simp_tac HOL_ss) alpha_bns ctxt -*} - -ML {* -fun build_rsp_gl alphas fnctn ctxt = -let - val typ = domain_type (fastype_of fnctn); - val (argl, argr) = the (AList.lookup (op=) alphas typ); -in - ([HOLogic.mk_eq (fnctn $ argl, fnctn $ argr)], ctxt) -end -*} - -ML {* -fun fvbv_rsp_tac' simps ctxt = - asm_full_simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps (@{thms alphas} @ simps)) THEN_ALL_NEW - REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW - TRY o blast_tac (claset_of ctxt) -*} - -ML {* -fun build_fvbv_rsps alphas ind simps fnctns ctxt = - prove_by_rel_induct alphas build_rsp_gl ind (fvbv_rsp_tac' simps) fnctns ctxt -*} - -end