Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei:   Sprache: HTML

Original von: Isabelle©

(*  Title:      HOL/Tools/BNF/bnf_fp_n2m_tactics.ML
    Author:     Dmitriy Traytel, TU Muenchen
    Copyright   2013

Tactics for mutualization of nested (co)datatypes.
*)


signature BNF_FP_N2M_TACTICS =
sig
  val mk_rel_xtor_co_induct_tac: BNF_Util.fp_kind -> thm list -> thm list -> thm list ->
    thm list -> thm list -> thm list -> {prems: thm list, context: Proof.context} -> tactic
  val mk_xtor_un_fold_unique_tac: BNF_Util.fp_kind -> thm list -> thm list -> thm list ->
    thm list -> thm list -> thm list -> thm list -> thm list -> thm list ->
    {context: Proof.context, prems: thm list} -> tactic
  val mk_xtor_un_fold_tac: Proof.context -> int -> thm list -> thm list -> tactic
  val mk_xtor_un_fold_transfer_tac: Proof.context -> int -> thm list -> thm list -> thm list ->
    thm list -> thm list -> thm list -> thm list -> tactic
end;

structure BNF_FP_N2M_Tactics : BNF_FP_N2M_TACTICS =
struct

open BNF_Util
open BNF_Tactics
open BNF_FP_Util

val vimage2p_unfolds = o_apply :: @{thms vimage2p_def};

fun unfold_at_most_once_tac ctxt thms =
  CONVERSION (Conv.top_sweep_conv (K (Conv.rewrs_conv thms)) ctxt);
val unfold_once_tac = CHANGED ooo unfold_at_most_once_tac;

fun mk_rel_xtor_co_induct_tac fp abs_inverses co_inducts0 rel_defs rel_monos nesting_rel_eqs0
  nesting_rel_monos0 {context = ctxt, prems = raw_C_IHs} =
  let
    val nesting_rel_eqs = @{thms prod.rel_eq sum.rel_eq} @ nesting_rel_eqs0;
    val nesting_rel_monos = map (fn thm => rotate_prems ~1 (thm RS @{thm predicate2D}))
      (@{thms prod.rel_mono sum.rel_mono} @ nesting_rel_monos0);
    val co_inducts = map (unfold_thms ctxt (vimage2p_unfolds @ nesting_rel_eqs)) co_inducts0;
    val unfolds = map (fn def =>
      unfold_thms ctxt (id_apply :: vimage2p_unfolds @ abs_inverses @ no_reflexive [def])) rel_defs;
    val folded_C_IHs = map (fn thm => thm RS @{thm spec2} RS mp) raw_C_IHs;
    val C_IHs = map2 (curry op |>) folded_C_IHs unfolds;
    val C_IH_monos =
      @{map 3} (fn C_IH => fn mono => fn unfold =>
        (mono RSN (2, @{thm vimage2p_mono}), C_IH)
        |> fp = Greatest_FP ? swap
        |> op RS
        |> unfold)
      folded_C_IHs rel_monos unfolds;

    val sym_nested_rel_eqs = map mk_sym nesting_rel_eqs;
  in
    unfold_thms_tac ctxt vimage2p_unfolds THEN
    HEADGOAL (CONJ_WRAP_GEN' (rtac ctxt @{thm context_conjI})
      (fn thm => rtac ctxt thm THEN_ALL_NEW (rotate_tac ~1 THEN'
         REPEAT_ALL_NEW (FIRST' [eresolve_tac ctxt C_IHs, eresolve_tac ctxt C_IH_monos,
           SELECT_GOAL (unfold_thms_tac ctxt nesting_rel_eqs) THEN' rtac ctxt @{thm order_refl},
           assume_tac ctxt, resolve_tac ctxt co_inducts,
           resolve_tac ctxt C_IH_monos THEN_ALL_NEW (TRY o FIRST'
             [SELECT_GOAL (unfold_thms_tac ctxt sym_nested_rel_eqs) THEN' assume_tac ctxt,
              rtac ctxt @{thm order_refl},
              REPEAT_ALL_NEW (eresolve_tac ctxt nesting_rel_monos)])])))
    co_inducts)
  end;

fun mk_xtor_un_fold_unique_tac fp xtor_un_fold_defs map_arg_congs xtor_un_fold_o_maps
   Rep_o_Abss fp_un_fold_uniques simp_thms map_thms map_defs cache_defs {context = ctxt, prems} =
  unfold_thms_tac ctxt xtor_un_fold_defs THEN
  HEADGOAL (REPEAT_DETERM o FIRST' [hyp_subst_tac_thin true ctxt, rtac ctxt refl,
    rtac ctxt conjI,
    rtac ctxt @{thm arg_cong2[of _ _ _ _ "(\)"OF refl]},
    rtac ctxt @{thm arg_cong2[of _ _ _ _ "(\)"OF _ refl]},
    resolve_tac ctxt map_arg_congs,
    resolve_tac ctxt fp_un_fold_uniques THEN_ALL_NEW case_fp fp (K all_tac) (rtac ctxt sym),
    SELECT_GOAL (CHANGED (unfold_thms_tac ctxt (flat [simp_thms, map_thms, map_defs,
      xtor_un_fold_defs, xtor_un_fold_o_maps, Rep_o_Abss, prems]))),
    unfold_once_tac ctxt cache_defs]);

fun mk_xtor_un_fold_tac ctxt n simps cache_defs =
  REPEAT_DETERM (CHANGED (unfold_thms_tac ctxt simps) ORELSE
    CHANGED (ALLGOALS (unfold_at_most_once_tac ctxt cache_defs))) THEN
  CONJ_WRAP (K (HEADGOAL (rtac ctxt refl))) (1 upto n);

fun mk_xtor_un_fold_transfer_tac ctxt n xtor_un_fold_defs rel_defs fp_un_fold_transfers
    map_transfers Abs_transfers fp_or_nesting_rel_eqs cache_defs =
  let
    val unfold = SELECT_GOAL (unfold_thms_tac ctxt fp_or_nesting_rel_eqs);
  in
    unfold_thms_tac ctxt (xtor_un_fold_defs @ rel_defs) THEN
    HEADGOAL (CONJ_WRAP'
      (fn thm => EVERY' [REPEAT_DETERM_N n o rtac ctxt rel_funI, rtac ctxt thm THEN_ALL_NEW
        REPEAT_DETERM o (FIRST' [assume_tac ctxt, rtac ctxt @{thm id_transfer},
            rtac ctxt @{thm rel_funD[OF rel_funD[OF comp_transfer]]},
            resolve_tac ctxt fp_un_fold_transfers, resolve_tac ctxt map_transfers,
            unfold_once_tac ctxt cache_defs,
            resolve_tac ctxt Abs_transfers, rtac ctxt @{thm vimage2p_rel_fun},
            unfold THEN' rtac ctxt @{thm vimage2p_rel_fun}])])
      fp_un_fold_transfers)
  end;

end;

¤ Dauer der Verarbeitung: 0.20 Sekunden  (vorverarbeitet)  ¤





Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik