Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: SameDN.java Sprache: SML

Original von: Isabelle^©

(*  Title:      HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
    Author:     Jasmin Blanchette, TU Muenchen
    Author:     Dmitriy Traytel, TU Muenchen
    Author:     Stefan Berghofer, TU Muenchen
    Author:     Florian Haftmann, TU Muenchen
    Copyright   2001-2013

Code generation for freely generated types.
*)

signature CTR_SUGAR_CODE =
sig
  val add_ctr_code: string -> typ list -> (string * typ) list -> thm list -> thm list -> thm list ->
    theory -> theory
end;

structure Ctr_Sugar_Code : CTR_SUGAR_CODE =
struct

open Ctr_Sugar_Util

val eqN = "eq"
val reflN = "refl"
val simpsN = "simps"

fun mk_case_certificate ctxt raw_thms =
  let
    val thms as thm1 :: _ = raw_thms
      |> Conjunction.intr_balanced
      |> Thm.unvarify_global (Proof_Context.theory_of ctxt)
      |> Conjunction.elim_balanced (length raw_thms)
      |> map Simpdata.mk_meta_eq
      |> map Drule.zero_var_indexes;
    val params = Term.add_free_names (Thm.prop_of thm1) [];
    val rhs = thm1
      |> Thm.prop_of |> Logic.dest_equals |> fst |> Term.strip_comb
      ||> fst o split_last |> list_comb;
    val lhs = Free (singleton (Name.variant_list params) "case", Term.fastype_of rhs);
    val assum = Thm.cterm_of ctxt (Logic.mk_equals (lhs, rhs));
  in
    thms
    |> Conjunction.intr_balanced
    |> rewrite_rule ctxt [Thm.symmetric (Thm.assume assum)]
    |> Thm.implies_intr assum
    |> Thm.generalize ([], params) 0
    |> Axclass.unoverload ctxt
    |> Thm.varifyT_global
  end;

fun mk_free_ctr_equations fcT ctrs inject_thms distinct_thms thy =
  let
    fun mk_fcT_eq (t, u) = Const (\<^const_name>\<open>HOL.equal\<close>, fcT --> fcT --> HOLogic.boolT) $ t $ u;
    fun true_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, \<^term>\<open>True\<close>);
    fun false_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, \<^term>\<open>False\<close>);

    val monomorphic_prop_of = Thm.prop_of o Thm.unvarify_global thy o Drule.zero_var_indexes;

    fun massage_inject (tp $ (eqv $ (_ $ t $ u) $ rhs)) = tp $ (eqv $ mk_fcT_eq (t, u) $ rhs);
    fun massage_distinct (tp $ (_ $ (_ $ t $ u))) = [tp $ false_eq (t, u), tp $ false_eq (u, t)];

    val triv_inject_goals =
      map_filter (fn c as (_, T) =>
          if T = fcT then SOME (HOLogic.mk_Trueprop (true_eq (Const c, Const c))) else NONE)
        ctrs;
    val inject_goals = map (massage_inject o monomorphic_prop_of) inject_thms;
    val distinct_goals = maps (massage_distinct o monomorphic_prop_of) distinct_thms;
    val refl_goal = HOLogic.mk_Trueprop (true_eq (Free ("x", fcT), Free ("x", fcT)));

    fun prove goal =
      Goal.prove_sorry_global thy [] [] goal (fn {context = ctxt, ...} =>
        HEADGOAL Goal.conjunction_tac THEN
        ALLGOALS (simp_tac
          (put_simpset HOL_basic_ss ctxt
            addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms)))));

    fun proves goals = goals
      |> Logic.mk_conjunction_balanced
      |> prove
      |> Thm.close_derivation \<^here>
      |> Conjunction.elim_balanced (length goals)
      |> map Simpdata.mk_eq;
  in
    (proves (triv_inject_goals @ inject_goals @ distinct_goals), Simpdata.mk_eq (prove refl_goal))
  end;

fun add_equality fcT fcT_name As ctrs inject_thms distinct_thms =
  let
    fun add_def lthy =
      let
        fun mk_side const_name =
          Const (const_name, fcT --> fcT --> HOLogic.boolT) $ Free ("x", fcT) $ Free ("y", fcT);
        val spec =
          mk_Trueprop_eq (mk_side \<^const_name>\<open>HOL.equal\<close>, mk_side \<^const_name>\<open>HOL.eq\<close>)
          |> Syntax.check_term lthy;
        val ((_, (_, raw_def)), lthy') =
          Specification.definition NONE [] [] (Binding.empty_atts, spec) lthy;
        val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy');
        val def = singleton (Proof_Context.export lthy' thy_ctxt) raw_def;
      in
        (def, lthy')
      end;

    fun tac ctxt thms =
      Class.intro_classes_tac ctxt [] THEN ALLGOALS (Proof_Context.fact_tac ctxt thms);

    val qualify =
      Binding.qualify true (Long_Name.base_name fcT_name) o Binding.qualify true eqN o Binding.name;
  in
    Class.instantiation ([fcT_name], map dest_TFree As, [HOLogic.class_equal])
    #> add_def
    #-> Class.prove_instantiation_exit_result (map o Morphism.thm) tac o single
    #> snd
    #> `(mk_free_ctr_equations fcT ctrs inject_thms distinct_thms)
    #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.theoremK
          [((qualify reflN, []), [([thm], [])]),
            ((qualify simpsN, []), [(rev thms, [])])])
    #-> (fn [(_, [thm]), (_, thms)] =>
          Code.declare_default_eqns_global ((thm, false) :: map (rpair true) thms))
  end;

fun add_ctr_code fcT_name raw_As raw_ctrs inject_thms distinct_thms case_thms thy =
  let
    val As = map (perhaps (try Logic.unvarifyT_global)) raw_As;
    val ctrs = map (apsnd (perhaps (try Logic.unvarifyT_global))) raw_ctrs;
    val fcT = Type (fcT_name, As);
    val unover_ctrs = map (fn ctr as (_, fcT) => (Axclass.unoverload_const thy ctr, fcT)) ctrs;
  in
    if can (Code.constrset_of_consts thy) unover_ctrs then
      thy
      |> Code.declare_datatype_global ctrs
      |> Code.declare_default_eqns_global (map (rpair true) (rev case_thms))
      |> Code.declare_case_global (mk_case_certificate (Proof_Context.init_global thy) case_thms)
      |> not (Sorts.has_instance (Sign.classes_of thy) fcT_name [HOLogic.class_equal])
        ? add_equality fcT fcT_name As ctrs inject_thms distinct_thms
    else
      thy
  end;

end;

¤ Dauer der Verarbeitung: 0.19 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.