Quelle bnf_gfp_grec_unique_sugar.ML Sprache: SML

(*  Title:      HOL/Tools/BNF/bnf_gfp_grec_unique_sugar.ML
    Author:     Jasmin Blanchette, Inria, LORIA, MPII
    Copyright   2016

Proof method for proving uniqueness of corecursive equations ("corec_unique").
*)

signature BNF_GFP_GREC_UNIQUE_SUGAR =
sig
  val corec_unique_tac: Proof.context -> int -> tactic
end;

structure BNF_GFP_Grec_Unique_Sugar : BNF_GFP_GREC_UNIQUE_SUGAR =
struct

open BNF_Util
open BNF_GFP_Grec
open BNF_GFP_Grec_Sugar_Util
open BNF_GFP_Grec_Sugar

fun corec_unique_tac ctxt =
  Subgoal.FOCUS (fn {context = ctxt, prems, concl, ...} =>
    let
      (* Workaround for odd name clash for goals with "x" in their context *)
      val (_, ctxt) = ctxt
        |> yield_singleton (mk_Frees "x") \<^typ>\<open>unit\<close>;

      val code_thm = (if null prems then error "No premise" else hd prems)
        |> Object_Logic.rulify ctxt;
      val code_goal = Thm.prop_of code_thm;

      val (fun_t, args) = strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop code_goal)))
        handle TERM _ => error "Wrong format for first premise";

      val _ = is_Free fun_t orelse
        error ("Expected free variable as function in premise, found " ^
          Syntax.string_of_term ctxt fun_t);
      val _ =
        (case filter_out is_Var args of
          [] => ()
        | arg :: _ =>
          error ("Expected universal variable as argument to function in premise, found " ^
            Syntax.string_of_term ctxt arg));

      val fun_T = fastype_of fun_t;
      val (arg_Ts, res_T) = strip_type fun_T;

      val num_args_in_concl = length (snd (strip_comb (fst (HOLogic.dest_eq
          (HOLogic.dest_Trueprop (Thm.term_of concl))))))
        handle TERM _ => error "Wrong format for conclusion";

      val (corec_info, corec_parse_info) =
        (case maybe_corec_info_of ctxt res_T of
          SOME (info as {buffer, ...}) => (info, corec_parse_info_of ctxt arg_Ts res_T buffer)
        | NONE => error ("No corecursor for " ^ quote (Syntax.string_of_typ ctxt res_T) ^
          " (use " ^ quote (#1 \<^command_keyword>\<open>coinduction_upto\<close>) ^ " to derive it)"));

      val Type (fpT_name, _) = res_T;

      val parsed_eq = parse_corec_equation ctxt [fun_t] code_goal;
      val explored_eq =
        explore_corec_equation ctxt false false "" fun_t corec_parse_info res_T parsed_eq;

      val ((_, corecUU_arg), _) = build_corecUU_arg_and_goals false fun_t explored_eq ctxt;
      val eq_corecUU = derive_eq_corecUU ctxt corec_info fun_t corecUU_arg code_thm;

      val unique' = derive_unique ctxt Morphism.identity code_goal corec_info fpT_name eq_corecUU
        |> funpow num_args_in_concl (fn thm => thm RS fun_cong);
    in
      HEADGOAL ((K all_tac APPEND' rtac ctxt sym) THEN' rtac ctxt unique' THEN'
        REPEAT_DETERM_N num_args_in_concl o rtac ctxt ext)
    end) ctxt THEN'
  etac ctxt thin_rl;

end;

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.