products/sources/formale sprachen/Isabelle/HOL/Tools/BNF/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: bnf_gfp_grec_tactics.ML   Sprache: SML

Original von: Isabelle©
(*  Title:      HOL/Tools/BNF/bnf_gfp_grec_tactics.ML
    Author:     Jasmin Blanchette, Inria, LORIA, MPII
    Author:     Dmitriy Traytel, ETH Zurich
    Copyright   2015, 2016

Tactics for generalized corecursor construction.
*)

signature BNF_GFP_GREC_TACTICS =
sig
  val transfer_prover_eq_tac: Proof.context -> int -> tactic
  val transfer_prover_add_tac: Proof.context -> thm list -> thm list -> int -> tactic

  val mk_algLam_algLam_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm ->
    tactic
  val mk_algLam_algrho_tac: Proof.context -> thm -> thm -> tactic
  val mk_algLam_base_tac: Proof.context -> term -> thm -> thm -> thm -> thm -> thm -> thm -> thm ->
    thm list -> thm -> thm list -> thm list -> thm -> thm -> tactic
  val mk_algLam_step_tac: Proof.context -> thm -> thm -> thm -> tactic
  val mk_cong_locale_tac: Proof.context -> thm -> thm list -> thm -> thm -> thm list -> thm ->
    thm -> tactic
  val mk_corecU_pointfree_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm list -> thm ->
    thm list -> thm -> thm -> thm -> tactic
  val mk_corecUU_pointfree_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm ->
    thm -> thm -> thm -> thm -> thm -> thm -> tactic
  val mk_corecUU_unique_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm ->
    thm -> thm -> thm -> thm -> thm -> thm -> tactic
  val mk_corecUU_Inl_tac: Proof.context -> term -> thm -> thm -> thm -> thm -> thm list -> thm ->
    thm list -> thm -> thm -> thm -> thm -> tactic
  val mk_dtor_algLam_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
    thm -> thm -> thm list -> thm -> thm -> thm -> thm -> tactic
  val mk_dtor_algrho_tac: Proof.context -> thm -> thm -> thm -> thm -> tactic
  val mk_dtor_transfer_tac: Proof.context -> thm -> tactic
  val mk_equivp_Retr_tac: Proof.context -> thm -> thm -> thm -> thm -> tactic
  val mk_eval_core_embL_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm ->
    thm -> thm -> thm -> thm list -> thm list -> thm list -> thm -> tactic
  val mk_eval_core_flat_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm ->
    thm list -> thm -> thm list -> thm -> thm -> thm -> thm list -> tactic
  val mk_eval_core_k_as_ssig_tac: Proof.context -> thm -> thm -> thm -> thm list -> thm -> thm ->
    thm -> thm list -> tactic
  val mk_eval_embL_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> tactic
  val mk_eval_flat_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm ->
    tactic
  val mk_eval_sctr_tac: Proof.context -> thm -> thm -> thm -> thm -> tactic
  val mk_eval_Oper_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> thm -> thm list ->
    thm -> thm -> tactic
  val mk_eval_V_or_CLeaf_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm list -> thm ->
    tactic
  val mk_extdd_mor_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm ->
    thm -> thm -> thm -> tactic
  val mk_extdd_o_VLeaf_tac: Proof.context -> thm -> thm -> thm -> thm list -> thm list -> thm ->
    thm -> thm -> tactic
  val mk_flat_embL_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list ->
    thm list -> thm list -> tactic
  val mk_flat_VLeaf_or_flat_tac: Proof.context -> thm -> thm -> thm list -> tactic
  val mk_Lam_Inl_Inr_tac: Proof.context -> thm -> thm -> tactic
  val mk_mor_cutSsig_flat_tac: Proof.context -> term -> thm -> thm -> thm -> thm -> thm -> thm ->
    thm list -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> tactic
  val mk_natural_from_transfer_tac: Proof.context -> int -> bool list -> thm -> thm list ->
    thm list -> thm list -> tactic
  val mk_natural_by_unfolding_tac: Proof.context -> thm list -> tactic
  val mk_Retr_coinduct_tac: Proof.context -> thm -> thm -> tactic
  val mk_sig_transfer_tac: Proof.context -> thm -> thm list -> thm -> tactic
  val mk_transfer_by_transfer_prover_tac: Proof.context -> thm list -> thm list -> thm list ->
    tactic
end;

structure BNF_GFP_Grec_Tactics : BNF_GFP_GREC_TACTICS =
struct

open BNF_Util
open BNF_Tactics
open BNF_FP_Util

val o_assoc = @{thm o_assoc};
val o_def = @{thm o_def};

fun ss_only_silent thms ctxt =
  ss_only thms (ctxt |> Context_Position.set_visible false);

fun context_relator_eq_add rel_eqs ctxt =
  fold (snd oo Thm.proof_attributes (map (Attrib.attribute ctxt) @{attributes [relator_eq]}))
    rel_eqs ctxt;
val context_transfer_rule_add = fold (snd oo Thm.proof_attributes [Transfer.transfer_add]);

fun transfer_prover_eq_tac ctxt =
  SELECT_GOAL (Local_Defs.fold_tac ctxt (Transfer.get_relator_eq ctxt)) THEN'
  Transfer.transfer_prover_tac ctxt;

fun transfer_prover_add_tac ctxt rel_eqs transfers =
  transfer_prover_eq_tac (ctxt
    |> context_relator_eq_add rel_eqs
    |> context_transfer_rule_add transfers);

fun instantiate_natural_rule_with_id ctxt live =
  Rule_Insts.of_rule ctxt ([], NONE :: replicate live (SOME \<^const_name>\<open>id\<close>)) [];

fun instantiate_transfer_rule_with_Grp_UNIV ctxt alives thm =
  let
    val n = length alives;
    val fs = map (prefix "f" o string_of_int) (1 upto n);
    val ss = map2 (fn live => fn f => SOME (\<^const_name>\<open>BNF_Def.Grp\<close> ^ " " ^ \<^const_name>\<open>top\<close> ^
        " " ^ (if live then f else \<^const_name>\<open>id\<close>))) alives fs;
    val bs = map_filter (fn (live, f) => if live then SOME (Binding.name f, NONE, NoSyn) else NONE)
      (alives ~~ fs);
  in
    Rule_Insts.of_rule ctxt ([], ss) bs thm
  end;

fun mk_algLam_algLam_tac ctxt dead_pre_map_comp dtor_inject unsig sig_map Lam_def eval_embL
    old_dtor_algLam dtor_algLam =
  HEADGOAL (rtac ctxt ext THEN' rtac ctxt (dtor_inject RS iffD1)) THEN
  unfold_thms_tac ctxt (dead_pre_map_comp :: unsig :: sig_map :: Lam_def :: eval_embL ::
    old_dtor_algLam :: dtor_algLam :: @{thms o_apply id_o map_sum.simps sum.case}) THEN
  HEADGOAL (rtac ctxt refl);

fun mk_algLam_algrho_tac ctxt algLam_def algrho_def =
  HEADGOAL (rtac ctxt ext) THEN unfold_thms_tac ctxt [algLam_def, algrho_def, o_apply] THEN
  HEADGOAL (rtac ctxt refl);

fun mk_algLam_base_tac ctxt dead_pre_map_dtor dead_pre_map_id dead_pre_map_comp ctor_dtor dtor_ctor
    dtor_unfold_unique unsig Sig_pointful_natural ssig_maps Lam_def flat_simps eval_core_simps eval
    algLam_def =
  HEADGOAL (rtac ctxt (infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt dead_pre_map_dtor)]
    (trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym]) OF [ext, ext])) THEN
  ALLGOALS (asm_simp_tac (ss_only_silent (dead_pre_map_id :: ctor_dtor :: dtor_ctor :: unsig ::
    Sig_pointful_natural :: Lam_def :: eval :: algLam_def ::
    unfold_thms ctxt [o_def] dead_pre_map_comp :: ssig_maps @ flat_simps @ eval_core_simps @
    @{thms o_apply id_apply id_def[symmetric] snd_conv convol_apply}) ctxt));

fun mk_algLam_step_tac ctxt proto_sctr_def old_algLam_pointful algLam_algLam_pointful =
  HEADGOAL (rtac ctxt ext) THEN
  unfold_thms_tac ctxt [proto_sctr_def, old_algLam_pointful, algLam_algLam_pointful, o_apply] THEN
  HEADGOAL (rtac ctxt refl);

fun mk_cong_locale_tac ctxt dead_pre_rel_mono dead_pre_rel_maps equivp_Retr
    ssig_rel_mono ssig_rel_maps eval eval_core_transfer =
  HEADGOAL (resolve_tac ctxt (Locale.get_unfolds \<^context>) THEN'
    etac ctxt ssig_rel_mono THEN' etac ctxt equivp_Retr) THEN
  unfold_thms_tac ctxt (eval :: dead_pre_rel_maps @ @{thms id_apply}) THEN
  HEADGOAL (rtac ctxt (@{thm predicate2I} RS (dead_pre_rel_mono RS @{thm predicate2D})) THEN'
    etac ctxt @{thm rel_funD} THEN' assume_tac ctxt THEN'
    rtac ctxt (eval_core_transfer RS @{thm rel_funD})) THEN
  unfold_thms_tac ctxt (ssig_rel_maps @ @{thms vimage2p_rel_prod vimage2p_id}) THEN
  unfold_thms_tac ctxt @{thms vimage2p_def} THEN HEADGOAL (assume_tac ctxt);

fun mk_corecU_pointfree_tac ctxt dead_pre_map_comp dtor_unfold ssig_maps dead_ssig_map_comp0
    flat_simps flat_VLeaf eval_core_simps cutSsig_def mor_cutSsig_flat corecU_def =
  unfold_thms_tac ctxt [corecU_def, dead_ssig_map_comp0, o_assoc] THEN
  HEADGOAL (subst_tac ctxt NONE [ext RS mor_cutSsig_flat] THEN'
    asm_simp_tac (ss_only_silent [dtor_unfold, o_apply] ctxt) THEN'
    asm_simp_tac (ss_only_silent (dtor_unfold :: flat_VLeaf :: cutSsig_def :: ssig_maps @
      flat_simps @ eval_core_simps @ unfold_thms ctxt [o_def] dead_pre_map_comp ::
      @{thms o_def id_apply id_def[symmetric] snd_conv convol_apply}) ctxt));

fun mk_corecUU_tail_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor ssig_map_comp
    flat_pointful_natural eval_core_pointful_natural eval eval_flat sctr_pointful_natural
    eval_sctr_pointful =
  asm_simp_tac (ss_only_silent (dtor_ctor :: flat_pointful_natural :: eval :: eval_flat ::
    map (unfold_thms ctxt [o_def]) [dead_pre_map_comp, ssig_map_comp] @
    @{thms o_apply id_apply id_def[symmetric] convol_apply}) ctxt) THEN'
  asm_simp_tac (ss_only_silent (eval_core_pointful_natural :: sctr_pointful_natural ::
    eval_sctr_pointful :: map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, ssig_map_comp] @
    @{thms id_apply id_def[symmetric] convol_apply map_prod_simp}) ctxt);

fun mk_corecUU_pointfree_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor dtor_inject
    ssig_map_comp flat_pointful_natural eval_core_pointful_natural eval eval_flat corecU_ctor
    sctr_pointful_natural eval_sctr_pointful corecUU_def =
  unfold_thms_tac ctxt [corecUU_def] THEN
  HEADGOAL (rtac ctxt ext THEN' subst_tac ctxt NONE [corecU_ctor RS sym]) THEN
  unfold_thms_tac ctxt [corecUU_def RS symmetric_thm] THEN
  HEADGOAL (rtac ctxt (dtor_inject RS iffD1) THEN'
    mk_corecUU_tail_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor ssig_map_comp
      flat_pointful_natural eval_core_pointful_natural eval eval_flat sctr_pointful_natural
      eval_sctr_pointful);

fun mk_corecUU_unique_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor ssig_map_comp
    flat_pointful_natural eval_core_pointful_natural eval eval_flat corecU_unique
    sctr_pointful_natural eval_sctr_pointful corecUU_def prem =
  unfold_thms_tac ctxt [corecUU_def] THEN
  HEADGOAL (rtac ctxt corecU_unique THEN' rtac ctxt sym THEN' subst_tac ctxt NONE [prem] THEN'
    rtac ctxt ext THEN'
    mk_corecUU_tail_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor ssig_map_comp
      flat_pointful_natural eval_core_pointful_natural eval eval_flat sctr_pointful_natural
      eval_sctr_pointful);

fun mk_corecUU_Inl_tac ctxt inl_case' pre_map_comp dead_pre_map_ident dead_pre_map_comp0 ctor_dtor
    ssig_maps ssig_map_id0 eval_core_simps eval_core_pointful_natural eval_VLeaf corecUU_pointfree
    corecUU_unique =
  HEADGOAL (rtac ctxt (infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt inl_case')]
      (trans OF [corecUU_unique, corecUU_unique RS sym]) OF [ext, ext]) THEN'
    subst_tac ctxt NONE [corecUU_pointfree] THEN'
    asm_simp_tac (ss_only_silent (dead_pre_map_comp0 :: eval_core_pointful_natural :: ssig_maps @
      @{thms o_apply sum.case convol_apply id_apply map_prod_simp}) ctxt) THEN'
    asm_simp_tac (ss_only_silent (dead_pre_map_ident :: ctor_dtor :: ssig_map_id0 ::
        eval_core_pointful_natural :: eval_VLeaf :: unfold_thms ctxt [o_def] pre_map_comp ::
        ssig_maps @ eval_core_simps @ @{thms o_apply prod.map_id convol_apply snd_conv id_apply})
      ctxt));

fun mk_dtor_algLam_tac ctxt pre_map_comp dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp
    sig_map_comp Oper_pointful_natural ssig_maps dead_ssig_map_comp0 Lam_pointful_natural
    eval_core_simps eval eval_flat eval_VLeaf algLam_def =
  unfold_thms_tac ctxt [dead_ssig_map_comp0, o_assoc] THEN
  HEADGOAL (asm_simp_tac (ss_only_silent (sig_map_comp :: Oper_pointful_natural :: eval ::
      eval_flat :: algLam_def :: unfold_thms ctxt [o_def] dead_pre_map_comp :: eval_core_simps @
      @{thms o_apply id_apply id_def[symmetric]}) ctxt) THEN'
    asm_simp_tac (ss_only_silent (Lam_pointful_natural :: eval_VLeaf ::
      map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, sig_map_comp] @ ssig_maps @
      eval_core_simps @
      @{thms o_apply convol_apply snd_conv fst_conv id_apply map_prod_simp}) ctxt) THEN'
    asm_simp_tac (ss_only_silent (dead_pre_map_id :: eval_VLeaf ::
      unfold_thms ctxt [o_def] pre_map_comp ::
      @{thms id_apply id_def[symmetric] convol_def}) ctxt));

fun mk_dtor_algrho_tac ctxt eval k_as_ssig_natural_pointful eval_core_k_as_ssig algrho_def =
  HEADGOAL (asm_simp_tac (ss_only_silent [eval, k_as_ssig_natural_pointful, algrho_def,
    eval_core_k_as_ssig RS sym, o_apply] ctxt));

fun mk_dtor_transfer_tac ctxt dtor_rel =
  HEADGOAL (rtac ctxt refl ORELSE'
    rtac ctxt @{thm rel_funI} THEN' rtac ctxt (dtor_rel RS iffD1) THEN' assume_tac ctxt);

fun mk_equivp_Retr_tac ctxt dead_pre_rel_refl dead_pre_rel_flip dead_pre_rel_mono
    dead_pre_rel_compp =
  HEADGOAL (EVERY' [etac ctxt @{thm equivpE}, rtac ctxt @{thm equivpI},
    rtac ctxt @{thm reflpI}, rtac ctxt dead_pre_rel_refl, etac ctxt @{thm reflpD},
    SELECT_GOAL (unfold_thms_tac ctxt @{thms symp_iff}),
      REPEAT_DETERM o rtac ctxt ext, rtac ctxt (dead_pre_rel_flip RS sym RS trans),
      rtac ctxt ((@{thm conversep_iff} RS sym) RSN (2, trans)),
      asm_simp_tac (ss_only_silent @{thms conversep_eq} ctxt),
    SELECT_GOAL (unfold_thms_tac ctxt @{thms transp_relcompp}),
      rtac ctxt @{thm predicate2I}, etac ctxt @{thm relcomppE},
      etac ctxt (dead_pre_rel_mono RS @{thm rev_predicate2D[rotated -1]}),
      SELECT_GOAL (unfold_thms_tac ctxt
        (unfold_thms ctxt [@{thm eq_OO}] dead_pre_rel_compp :: @{thms relcompp_apply})),
      REPEAT_DETERM o resolve_tac ctxt [exI, conjI], assume_tac ctxt, assume_tac ctxt]);

fun mk_eval_core_k_as_ssig_tac ctxt pre_map_comp dead_pre_map_id sig_map_comp ssig_maps
    Lam_natural_pointful Lam_Inr flat_VLeaf eval_core_simps =
  HEADGOAL (asm_simp_tac (ss_only_silent (dead_pre_map_id :: flat_VLeaf :: (Lam_Inr RS sym) ::
    o_apply :: id_apply :: @{thm id_def[symmetric]} ::
    unfold_thms ctxt @{thms map_prod_def split_def} Lam_natural_pointful :: ssig_maps @
    eval_core_simps @ map (unfold_thms ctxt [o_def]) [pre_map_comp, sig_map_comp]) ctxt));

fun mk_eval_embL_tac ctxt dead_pre_map_comp0 dtor_unfold_unique embL_pointful_natural eval_core_embL
    old_eval eval =
  HEADGOAL (rtac ctxt (unfold_thms ctxt [o_apply]
      (trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym] OF [ext, ext])
    OF [asm_rl, old_eval RS sym])) THEN
  unfold_thms_tac ctxt [dead_pre_map_comp0, embL_pointful_natural, eval_core_embL, eval,
    o_apply] THEN
  HEADGOAL (rtac ctxt refl);

fun mk_eval_flat_tac ctxt dead_pre_map_comp0 ssig_map_id ssig_map_comp flat_pointful_natural
    eval_core_pointful_natural eval_core_flat eval cond_eval_o_flat =
  HEADGOAL (rtac ctxt (unfold_thms ctxt [o_apply] cond_eval_o_flat)) THEN
  unfold_thms_tac ctxt [dead_pre_map_comp0, flat_pointful_natural, eval_core_flat, eval,
    o_apply] THEN
  HEADGOAL (rtac ctxt refl THEN'
    asm_simp_tac (ss_only_silent (ssig_map_id :: eval_core_pointful_natural :: eval ::
        map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, ssig_map_comp] @
        @{thms id_apply id_def[symmetric] fst_conv map_prod_simp convol_apply})
      ctxt));

fun instantiate_map_comp_with_f_g ctxt =
  Rule_Insts.of_rule ctxt ([], [NONE, SOME ("%x. f (g x)")])
    [(Binding.name "f", NONE, NoSyn), (Binding.name "g", NONE, NoSyn)];

fun mk_eval_core_embL_tac ctxt old_ssig_induct dead_pre_map_comp0 dead_pre_map_comp
    Sig_pointful_natural unsig_thm old_sig_map_comp old_sig_map_cong old_Lam_pointful_natural
    Lam_def flat_embL old_eval_core_simps eval_core_simps embL_simps embL_pointful_natural =
  HEADGOAL (rtac ctxt old_ssig_induct) THEN
  ALLGOALS (asm_simp_tac (ss_only_silent (Sig_pointful_natural :: unsig_thm :: Lam_def ::
    (flat_embL RS sym) :: unfold_thms ctxt [o_def] dead_pre_map_comp :: embL_simps @
    old_eval_core_simps @ eval_core_simps @
    @{thms id_apply id_def[symmetric] o_apply map_sum.simps sum.case}) ctxt)) THEN
  HEADGOAL (asm_simp_tac (Simplifier.add_cong old_sig_map_cong (ss_only_silent
    (old_Lam_pointful_natural :: embL_pointful_natural ::
     map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, instantiate_map_comp_with_f_g ctxt
       dead_pre_map_comp0, old_sig_map_comp] @ @{thms map_prod_simp}) ctxt)));

fun mk_eval_core_flat_tac ctxt ssig_induct dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp
    fp_map_id sig_map_comp sig_map_cong ssig_maps ssig_map_comp flat_simps flat_natural flat_flat
    Lam_natural_sym eval_core_simps =
  HEADGOAL (rtac ctxt ssig_induct) THEN
  ALLGOALS (full_simp_tac (ss_only_silent ((flat_flat RS sym) :: dead_pre_map_id ::
    dead_pre_map_comp :: fp_map_id :: sig_map_comp :: ssig_map_comp :: ssig_maps @ flat_simps @
    eval_core_simps @ @{thms o_def id_def[symmetric] convol_apply id_apply snd_conv}) ctxt)) THEN
  HEADGOAL (asm_simp_tac (Simplifier.add_cong sig_map_cong (ss_only_silent
      (map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, sig_map_comp] @
       flat_natural :: Lam_natural_sym :: @{thms id_apply fst_conv map_prod_simp})
    ctxt)));

fun mk_eval_sctr_tac ctxt proto_sctr_pointful_natural eval_Oper algLam sctr_def =
  HEADGOAL (rtac ctxt ext) THEN
  unfold_thms_tac ctxt [proto_sctr_pointful_natural, eval_Oper, algLam RS sym, sctr_def,
    o_apply] THEN
  HEADGOAL (rtac ctxt refl);

fun mk_eval_V_or_CLeaf_tac ctxt dead_pre_map_id dead_pre_map_comp fp_map_id dtor_unfold_unique
    V_or_CLeaf_map eval_core_simps eval =
  HEADGOAL (rtac ctxt (trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym] RS fun_cong
    OF [ext, ext])) THEN
  ALLGOALS (asm_simp_tac (ss_only_silent (dead_pre_map_id :: fp_map_id ::
    unfold_thms ctxt @{thms o_def} dead_pre_map_comp :: V_or_CLeaf_map :: eval :: eval_core_simps @
    @{thms o_apply id_def[symmetric] id_apply snd_conv convol_apply}) ctxt));

fun mk_eval_Oper_tac ctxt live sig_map_ident sig_map_comp0 sig_map_comp Oper_natural_pointful
    VLeaf_natural flat_simps eval_flat algLam_def =
  let val VLeaf_natural' = instantiate_natural_rule_with_id ctxt live VLeaf_natural in
    unfold_thms_tac ctxt [sig_map_comp, VLeaf_natural', algLam_def, o_apply] THEN
    unfold_thms_tac ctxt (sig_map_comp0 :: Oper_natural_pointful :: (eval_flat RS sym) :: o_apply ::
      flat_simps) THEN
    unfold_thms_tac ctxt (@{thm id_apply} :: sig_map_ident :: unfold_thms ctxt [o_def] sig_map_comp ::
      flat_simps) THEN
    HEADGOAL (rtac ctxt refl)
  end;

fun mk_extdd_mor_tac ctxt dead_pre_map_comp0 dead_pre_map_comp VLeaf_map ssig_map_comp
    flat_pointful_natural eval_core_pointful_natural eval eval_flat eval_VLeaf cutSsig_def prem =
  HEADGOAL (rtac ctxt ext) THEN
  unfold_thms_tac ctxt (ssig_map_comp :: unfold_thms ctxt [o_def] dead_pre_map_comp ::
    flat_pointful_natural :: eval :: eval_flat :: cutSsig_def ::
    @{thms o_apply convol_o id_o id_apply id_def[symmetric]}) THEN
  unfold_thms_tac ctxt (unfold_thms ctxt [dead_pre_map_comp0] prem :: dead_pre_map_comp0 ::
    ssig_map_comp :: eval_core_pointful_natural ::
    @{thms o_def[symmetric] o_apply map_prod_o_convol}) THEN
  unfold_thms_tac ctxt (VLeaf_map :: eval_VLeaf :: @{thms o_def id_apply id_def[symmetric]}) THEN
  HEADGOAL (rtac ctxt refl);

fun mk_extdd_o_VLeaf_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_inject ssig_maps
    eval_core_simps eval eval_VLeaf prem =
  HEADGOAL (rtac ctxt ext THEN' rtac ctxt (dtor_inject RS iffD1) THEN'
    asm_simp_tac (ss_only_silent (dead_pre_map_comp0 :: ssig_maps @ eval_core_simps @ eval ::
      eval_VLeaf :: (mk_pointful ctxt prem RS sym) :: unfold_thms ctxt [o_def] dead_pre_map_comp ::
      @{thms o_apply convol_apply snd_conv id_apply}) ctxt));

fun mk_flat_embL_tac ctxt old_ssig_induct fp_map_id Sig_pointful_natural old_sig_map_comp
    old_sig_map_cong old_ssig_maps old_flat_simps flat_simps embL_simps =
  HEADGOAL (rtac ctxt old_ssig_induct) THEN
  ALLGOALS (asm_simp_tac (Simplifier.add_cong old_sig_map_cong (ss_only_silent
    (fp_map_id :: Sig_pointful_natural :: unfold_thms ctxt [o_def] old_sig_map_comp ::
     old_ssig_maps @ old_flat_simps @ flat_simps @ embL_simps @
     @{thms id_apply id_def[symmetric] map_sum.simps}) ctxt)));

fun mk_flat_VLeaf_or_flat_tac ctxt ssig_induct cong simps =
  HEADGOAL (rtac ctxt ssig_induct) THEN
  ALLGOALS (asm_simp_tac (Simplifier.add_cong cong (ss_only_silent simps ctxt)));

fun mk_Lam_Inl_Inr_tac ctxt unsig Lam_def =
  TRYALL Goal.conjunction_tac THEN ALLGOALS (rtac ctxt ext) THEN
  unfold_thms_tac ctxt (o_apply :: Lam_def :: unsig :: @{thms sum.case}) THEN
  ALLGOALS (rtac ctxt refl);

fun mk_mor_cutSsig_flat_tac ctxt eval_core_o_map dead_pre_map_comp0 dead_pre_map_comp
    dead_pre_map_cong dtor_unfold_unique dead_ssig_map_comp0 ssig_map_comp flat_simps
    flat_pointful_natural eval_core_pointful_natural flat_flat flat_VLeaf eval_core_flat cutSsig_def
    cutSsig_def_pointful_natural eval_thm prem =
  HEADGOAL (rtac ctxt (infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt eval_core_o_map)]
    (trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym]) OF [ext, ext]) THEN'
  asm_simp_tac (ss_only_silent ((prem RS sym) :: dead_pre_map_comp0 :: ssig_map_comp ::
    eval_core_pointful_natural :: eval_thm ::
    @{thms o_apply map_prod_o_convol o_id convol_o id_o}) ctxt) THEN'
  asm_simp_tac (ss_only_silent ((mk_pointful ctxt prem RS sym) :: dead_pre_map_comp0 ::
    cutSsig_def_pointful_natural :: flat_simps @
    @{thms o_apply convol_apply map_prod_simp id_apply}) ctxt) THEN'
  rtac ctxt (dead_pre_map_cong OF [asm_rl, refl]) THEN'
  asm_simp_tac (ss_only_silent (ssig_map_comp :: cutSsig_def :: flat_pointful_natural ::
    eval_core_flat :: unfold_thms ctxt [o_def] dead_pre_map_comp :: (dead_ssig_map_comp0 RS sym) ::
    (flat_flat RS sym) ::
    @{thms o_apply convol_o fst_convol id_apply id_def[symmetric]}) ctxt) THEN'
  asm_simp_tac (ss_only_silent (eval_core_pointful_natural :: flat_VLeaf ::
    map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, ssig_map_comp] @
    @{thms o_apply id_apply id_def[symmetric] map_prod_simp convol_def}) ctxt));

fun mk_natural_from_transfer_tac ctxt m alives transfer map_ids rel_Grps subst_rel_Grps =
  let
    val unfold_eq = unfold_thms ctxt @{thms Grp_UNIV_id[symmetric]};
    val (rel_Grps', subst_rel_Grps') =
      apply2 (map (fn thm => unfold_eq (thm RS eq_reflection))) (rel_Grps, subst_rel_Grps);
    val transfer' = instantiate_transfer_rule_with_Grp_UNIV ctxt alives (unfold_eq transfer)
      |> unfold_thms ctxt rel_Grps';
  in
    HEADGOAL (Method.insert_tac ctxt [transfer'] THEN'
      EVERY' (map (subst_asm_tac ctxt NONE o single) subst_rel_Grps')) THEN
    unfold_thms_tac ctxt (map_ids @ @{thms Grp_def rel_fun_def}) THEN
    HEADGOAL (REPEAT_DETERM_N m o rtac ctxt ext THEN'
      asm_full_simp_tac (ss_only_silent @{thms simp_thms id_apply o_apply mem_Collect_eq
        top_greatest UNIV_I subset_UNIV[simplified UNIV_def]} ctxt)) THEN
    ALLGOALS (REPEAT_DETERM o etac ctxt @{thm meta_allE} THEN' REPEAT_DETERM o etac ctxt allE THEN'
      forward_tac ctxt [sym] THEN' assume_tac ctxt)
  end;

fun mk_natural_by_unfolding_tac ctxt maps =
  HEADGOAL (rtac ctxt ext) THEN
  unfold_thms_tac ctxt (@{thms o_def[abs_def] id_apply id_def[symmetric]} @ maps) THEN
  HEADGOAL (rtac ctxt refl);

fun mk_Retr_coinduct_tac ctxt dtor_rel_coinduct rel_eq =
  HEADGOAL (EVERY' [rtac ctxt allI, rtac ctxt impI,
    rtac ctxt (@{thm ord_le_eq_trans} OF [dtor_rel_coinduct, rel_eq]),
    etac ctxt @{thm predicate2D}, assume_tac ctxt]);

fun mk_sig_transfer_tac ctxt pre_rel_def rel_eqs0 transfer =
  let
    val rel_eqs = no_refl rel_eqs0;
    val rel_eq_syms = map (fn thm => thm RS sym) rel_eqs;
    val transfer' = unfold_thms ctxt rel_eq_syms transfer
  in
    HEADGOAL (rtac ctxt transfer') ORELSE
    unfold_thms_tac ctxt (pre_rel_def :: rel_eq_syms @
      @{thms BNF_Def.vimage2p_def BNF_Composition.id_bnf_def}) THEN
    HEADGOAL (rtac ctxt transfer')
  end;

fun mk_transfer_by_transfer_prover_tac ctxt defs rel_eqs0 transfers =
  let
    val rel_eqs = no_refl rel_eqs0;
    val rel_eq_syms = map (fn thm => thm RS sym) rel_eqs;
  in
    unfold_thms_tac ctxt (defs @ rel_eq_syms) THEN
    HEADGOAL (transfer_prover_add_tac ctxt rel_eqs transfers)
  end;

end;

¤ Dauer der Verarbeitung: 0.3 Sekunden  (vorverarbeitet)  ¤



Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff