1 theory Rsp

     2 imports Abs Tacs

     3 begin

     4 

     5 ML {*

     6 fun const_rsp qtys lthy const =

     7 let

     8   val nty = Quotient_Term.derive_qtyp lthy qtys (fastype_of const)

     9   val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty);

    10 in

    11   HOLogic.mk_Trueprop (rel $ const $ const)

    12 end

    13 *}

    14 

    15 (* Replaces bounds by frees and meta implications by implications *)

    16 ML {*

    17 fun prepare_goal trm =

    18 let

    19   val vars = strip_all_vars trm

    20   val fs = rev (map Free vars)

    21   val (fixes, no_alls) = ((map fst vars), subst_bounds (fs, (strip_all_body trm)))

    22   val prems = map HOLogic.dest_Trueprop (Logic.strip_imp_prems no_alls)

    23   val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl no_alls)

    24 in

    25   (fixes, fold (curry HOLogic.mk_imp) prems concl)

    26 end

    27 *}

    28 

    29 ML {*

    30 fun get_rsp_goal thy trm =

    31 let

    32   val goalstate = Goal.init (cterm_of thy trm);

    33   val tac = REPEAT o rtac @{thm fun_relI};

    34 in

    35   case (SINGLE (tac 1) goalstate) of

    36     NONE => error "rsp_goal failed"

    37   | SOME th => prepare_goal (term_of (cprem_of th 1))

    38 end

    39 *}

    40 

    41 ML {*

    42 fun prove_const_rsp qtys bind consts tac ctxt =

    43 let

    44   val rsp_goals = map (const_rsp qtys ctxt) consts

    45   val thy = ProofContext.theory_of ctxt

    46   val (fixed, user_goals) = split_list (map (get_rsp_goal thy) rsp_goals)

    47   val fixed' = distinct (op =) (flat fixed)

    48   val user_goal = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj user_goals)

    49   val user_thm = Goal.prove ctxt fixed' [] user_goal tac

    50   val user_thms = map repeat_mp (HOLogic.conj_elims user_thm)

    51   fun tac _ = (REPEAT o rtac @{thm fun_relI} THEN' resolve_tac user_thms THEN_ALL_NEW atac) 1

    52   val rsp_thms = map (fn gl => Goal.prove ctxt [] [] gl tac) rsp_goals

    53 in

    54    ctxt

    55 |> snd o Local_Theory.note 

    56   ((Binding.empty, [Attrib.internal (fn _ => Quotient_Info.rsp_rules_add)]), rsp_thms)

    57 |> Local_Theory.note ((bind, []), user_thms)

    58 end

    59 *}

    60 

    61 ML {*

    62 fun fvbv_rsp_tac induct fvbv_simps ctxt =

    63   rtac induct THEN_ALL_NEW

    64   (TRY o rtac @{thm TrueI}) THEN_ALL_NEW

    65   asm_full_simp_tac (HOL_ss addsimps (@{thms prod_fv.simps prod_rel.simps set.simps append.simps alphas} @ fvbv_simps)) THEN_ALL_NEW

    66   REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW

    67   asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW

    68   TRY o blast_tac (claset_of ctxt)

    69 *}

    70 

    71 ML {*

    72 fun sym_eqvts ctxt = maps (fn x => [sym OF [x]] handle _ => []) (Nominal_ThmDecls.get_eqvts_thms ctxt)

    73 fun all_eqvts ctxt =

    74   Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt

    75 *}

    76 

    77 ML {*

    78 fun constr_rsp_tac inj rsp =

    79   REPEAT o rtac impI THEN'

    80   simp_tac (HOL_ss addsimps inj) THEN' split_conj_tac THEN_ALL_NEW

    81   (asm_simp_tac HOL_ss THEN_ALL_NEW (

    82    REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW

    83    simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW

    84    asm_full_simp_tac (HOL_ss addsimps (rsp @

    85      @{thms split_conv alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left prod_rel.simps prod_fv.simps}))

    86   ))

    87 *}

    88 

    89 ML {*

    90 fun prove_fv_rsp fv_alphas_lst all_alphas tac ctxt =

    91 let

    92   val (fvs_alphas, ls) = split_list fv_alphas_lst;

    93   val (fv_ts, alpha_ts) = split_list fvs_alphas;

    94   val tys = map (domain_type o fastype_of) alpha_ts;

    95   val names = Datatype_Prop.make_tnames tys;

    96   val names2 = Name.variant_list names names;

    97   val args = map Free (names ~~ tys);

    98   val args2 = map Free (names2 ~~ tys);

    99   fun mk_fv_rsp arg arg2 (fv, alpha) = HOLogic.mk_eq ((fv $ arg), (fv $ arg2));

   100   fun fv_rsp_arg (((fv, alpha), (arg, arg2)), l) =

   101     HOLogic.mk_imp (

   102      (alpha $ arg $ arg2),

   103      (foldr1 HOLogic.mk_conj

   104        (HOLogic.mk_eq (fv $ arg, fv $ arg2) ::

   105        (map (mk_fv_rsp arg arg2) l))));

   106   val nobn_eqs = map fv_rsp_arg (((fv_ts ~~ alpha_ts) ~~ (args ~~ args2)) ~~ ls);

   107   fun mk_fv_rsp_bn arg arg2 (fv, alpha) =

   108     HOLogic.mk_imp (

   109       (alpha $ arg $ arg2),

   110       HOLogic.mk_eq ((fv $ arg), (fv $ arg2)));

   111   fun fv_rsp_arg_bn ((arg, arg2), l) =

   112     map (mk_fv_rsp_bn arg arg2) l;

   113   val bn_eqs = flat (map fv_rsp_arg_bn ((args ~~ args2) ~~ ls));

   114   val (_, add_alphas) = chop (length (nobn_eqs @ bn_eqs)) all_alphas;

   115   val atys = map (domain_type o fastype_of) add_alphas;

   116   val anames = Name.variant_list (names @ names2) (Datatype_Prop.make_tnames atys);

   117   val aargs = map Free (anames ~~ atys);

   118   val aeqs = map2 (fn alpha => fn arg => HOLogic.mk_imp (alpha $ arg $ arg, @{term True}))

   119     add_alphas aargs;

   120   val eq = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (nobn_eqs @ bn_eqs @ aeqs));

   121   val th = Goal.prove ctxt (names @ names2) [] eq tac;

   122   val ths = HOLogic.conj_elims th;

   123   val (ths_nobn, ths_bn) = chop (length ls) ths;

   124   fun project (th, l) =

   125     Project_Rule.projects ctxt (1 upto (length l + 1)) (hd (Project_Rule.projections ctxt th))

   126   val ths_nobn_pr = map project (ths_nobn ~~ ls);

   127 in

   128   (flat ths_nobn_pr @ ths_bn)

   129 end

   130 *}

   131 

   132 (** alpha_bn_rsp **)

   133 

   134 lemma equivp_rspl:

   135   "equivp r \<Longrightarrow> r a b \<Longrightarrow> r a c = r b c"

   136   unfolding equivp_reflp_symp_transp symp_def transp_def 

   137   by blast

   138 

   139 lemma equivp_rspr:

   140   "equivp r \<Longrightarrow> r a b \<Longrightarrow> r c a = r c b"

   141   unfolding equivp_reflp_symp_transp symp_def transp_def 

   142   by blast

   143 

   144 ML {*

   145 fun alpha_bn_rsp_tac simps res exhausts a ctxt =

   146   rtac allI THEN_ALL_NEW

   147   case_rules_tac ctxt a exhausts THEN_ALL_NEW

   148   asm_full_simp_tac (HOL_ss addsimps simps addsimps @{thms alphas}) THEN_ALL_NEW

   149   TRY o REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<and>"]}) THEN_ALL_NEW

   150   TRY o eresolve_tac res THEN_ALL_NEW

   151   asm_full_simp_tac (HOL_ss addsimps simps)

   152 *}

   153 

   154 

   155 ML {*

   156 fun build_alpha_bn_rsp_gl a alphas alpha_bn ctxt =

   157 let

   158   val ty = domain_type (fastype_of alpha_bn);

   159   val (l, r) = the (AList.lookup (op=) alphas ty);

   160 in

   161   ([HOLogic.mk_all (a, ty, HOLogic.mk_eq (alpha_bn $ l $ Bound 0, alpha_bn $ r $ Bound 0)),

   162     HOLogic.mk_all (a, ty, HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r))], ctxt)

   163 end

   164 *}

   165 

   166 ML {*

   167 fun prove_alpha_bn_rsp alphas ind simps equivps exhausts alpha_bns ctxt =

   168 let

   169   val ([a], ctxt') = Variable.variant_fixes ["a"] ctxt;

   170   val resl = map (fn x => @{thm equivp_rspl} OF [x]) equivps;

   171   val resr = map (fn x => @{thm equivp_rspr} OF [x]) equivps;

   172   val ths_loc = prove_by_rel_induct alphas (build_alpha_bn_rsp_gl a) ind

   173     (alpha_bn_rsp_tac simps (resl @ resr) exhausts a) alpha_bns ctxt

   174 in

   175   Variable.export ctxt' ctxt ths_loc

   176 end

   177 *}

   178 

   179 ML {*

   180 fun build_alpha_alpha_bn_gl alphas alpha_bn ctxt =

   181 let

   182   val ty = domain_type (fastype_of alpha_bn);

   183   val (l, r) = the (AList.lookup (op=) alphas ty);

   184 in

   185   ([alpha_bn $ l $ r], ctxt)

   186 end

   187 *}

   188 

   189 lemma exi_same: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q p) \<Longrightarrow> \<exists>pi. Q pi"

   190   by auto

   191 

   192 ML {*

   193 fun prove_alpha_alphabn alphas ind simps alpha_bns ctxt =

   194   prove_by_rel_induct alphas build_alpha_alpha_bn_gl ind

   195     (fn _ => asm_full_simp_tac (HOL_ss addsimps simps addsimps @{thms alphas})

   196      THEN_ALL_NEW split_conj_tac THEN_ALL_NEW (TRY o etac @{thm exi_same})

   197      THEN_ALL_NEW asm_full_simp_tac HOL_ss) alpha_bns ctxt

   198 *}

   199 

   200 ML {*

   201 fun build_rsp_gl alphas fnctn ctxt =

   202 let

   203   val typ = domain_type (fastype_of fnctn);

   204   val (argl, argr) = the (AList.lookup (op=) alphas typ);

   205 in

   206   ([HOLogic.mk_eq (fnctn $ argl, fnctn $ argr)], ctxt)

   207 end

   208 *}

   209 

   210 ML {*

   211 fun fvbv_rsp_tac' simps ctxt =

   212   asm_full_simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW

   213   asm_full_simp_tac (HOL_ss addsimps (@{thms alphas} @ simps)) THEN_ALL_NEW

   214   REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW

   215   asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW

   216   TRY o blast_tac (claset_of ctxt)

   217 *}

   218 

   219 ML {*

   220 fun build_fvbv_rsps alphas ind simps fnctns ctxt =

   221   prove_by_rel_induct alphas build_rsp_gl ind (fvbv_rsp_tac' simps) fnctns ctxt

   222 *}

   223 

   224 end