1 theory Rsp

     2 imports Abs

     3 begin

     4 

     5 ML {*

     6 fun define_quotient_type args tac ctxt =

     7 let

     8   val mthd = Method.SIMPLE_METHOD tac

     9   val mthdt = Method.Basic (fn _ => mthd)

    10   val bymt = Proof.global_terminal_proof (mthdt, NONE)

    11 in

    12   bymt (Quotient_Type.quotient_type args ctxt)

    13 end

    14 *}

    15 

    16 ML {*

    17 fun const_rsp lthy const =

    18 let

    19   val nty = fastype_of (Quotient_Term.quotient_lift_const ("", const) lthy)

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

    21 in

    22   HOLogic.mk_Trueprop (rel $ const $ const)

    23 end

    24 *}

    25 

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

    27 ML {*

    28 fun prepare_goal trm =

    29 let

    30   val vars = strip_all_vars trm

    31   val fs = rev (map Free vars)

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

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

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

    35 in

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

    37 end

    38 *}

    39 

    40 ML {*

    41 fun get_rsp_goal thy trm =

    42 let

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

    44   val tac = REPEAT o rtac @{thm fun_rel_id};

    45 in

    46   case (SINGLE (tac 1) goalstate) of

    47     NONE => error "rsp_goal failed"

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

    49 end

    50 *}

    51 

    52 ML {*

    53 fun repeat_mp thm = repeat_mp (mp OF [thm]) handle THM _ => thm

    54 *}

    55 

    56 ML {*

    57 fun prove_const_rsp bind consts tac ctxt =

    58 let

    59   val rsp_goals = map (const_rsp ctxt) consts

    60   val thy = ProofContext.theory_of ctxt

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

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

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

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

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

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

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

    68 in

    69    ctxt

    70 |> snd o Local_Theory.note 

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

    72 |> snd o Local_Theory.note ((bind, []), user_thms)

    73 end

    74 *}

    75 

    76 

    77 

    78 ML {*

    79 fun fvbv_rsp_tac induct fvbv_simps =

    80   ((((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW

    81   (TRY o rtac @{thm TrueI})) THEN_ALL_NEW asm_full_simp_tac

    82   (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)))

    83 *}

    84 

    85 ML {*

    86 fun constr_rsp_tac inj rsp equivps =

    87 let

    88   val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps

    89 in

    90   REPEAT o rtac impI THEN'

    91   simp_tac (HOL_ss addsimps inj) THEN'

    92   (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)) THEN_ALL_NEW

    93   (asm_simp_tac HOL_ss THEN_ALL_NEW (

    94    rtac @{thm exI[of _ "0 :: perm"]} THEN'

    95    asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @

    96      @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv}))

    97   ))

    98 end

    99 *}

   100 

   101 (* Testing code

   102 local_setup {* prove_const_rsp @{binding fv_rtrm2_rsp} [@{term rbv2}]

   103   (fn _ => fv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms fv_rtrm2_fv_rassign.simps} 1) *}*)

   104 

   105 (*ML {*

   106   val rsp_goals = map (const_rsp @{context}) [@{term rbv2}]

   107   val (fixed, user_goals) = split_list (map (get_rsp_goal @{theory}) rsp_goals)

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

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

   110 *}

   111 prove ug: {* user_goal *}

   112 ML_prf {*

   113 val induct = @{thm alpha_rtrm2_alpha_rassign.inducts(2)}

   114 val fv_simps = @{thms rbv2.simps}

   115 *} 

   116 *)

   117 

   118 end