src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
author wenzelm
Sat Dec 14 17:28:05 2013 +0100 (2013-12-14)
changeset 54742 7a86358a3c0b
parent 54701 4ed7454aebde
child 54895 515630483010
permissions -rw-r--r--
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;
     1 (*  Title:      HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Author:     Dmitriy Traytel, TU Muenchen
     4     Author:     Stefan Berghofer, TU Muenchen
     5     Author:     Florian Haftmann, TU Muenchen
     6     Copyright   2001-2013
     7 
     8 Code generation for freely generated types.
     9 *)
    10 
    11 signature CTR_SUGAR_CODE =
    12 sig
    13   val add_ctr_code: string -> typ list -> (string * typ) list -> thm list -> thm list -> thm list ->
    14     theory -> theory
    15 end;
    16 
    17 structure Ctr_Sugar_Code : CTR_SUGAR_CODE =
    18 struct
    19 
    20 open Ctr_Sugar_Util
    21 
    22 val eqN = "eq"
    23 val reflN = "refl"
    24 val simpsN = "simps"
    25 
    26 fun mk_case_certificate thy raw_thms =
    27   let
    28     val thms as thm1 :: _ = raw_thms
    29       |> Conjunction.intr_balanced
    30       |> Thm.unvarify_global
    31       |> Conjunction.elim_balanced (length raw_thms)
    32       |> map Simpdata.mk_meta_eq
    33       |> map Drule.zero_var_indexes;
    34     val params = Term.add_free_names (Thm.prop_of thm1) [];
    35     val rhs = thm1
    36       |> Thm.prop_of |> Logic.dest_equals |> fst |> Term.strip_comb
    37       ||> fst o split_last |> list_comb;
    38     val lhs = Free (singleton (Name.variant_list params) "case", Term.fastype_of rhs);
    39     val assum = Thm.cterm_of thy (Logic.mk_equals (lhs, rhs));
    40   in
    41     thms
    42     |> Conjunction.intr_balanced
    43     |> rewrite_rule (Proof_Context.init_global thy) [Thm.symmetric (Thm.assume assum)]
    44     |> Thm.implies_intr assum
    45     |> Thm.generalize ([], params) 0
    46     |> Axclass.unoverload thy
    47     |> Thm.varifyT_global
    48   end;
    49 
    50 fun mk_free_ctr_equations fcT ctrs inject_thms distinct_thms thy =
    51   let
    52     fun mk_fcT_eq (t, u) = Const (@{const_name HOL.equal}, fcT --> fcT --> HOLogic.boolT) $ t $ u;
    53     fun true_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term True});
    54     fun false_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term False});
    55 
    56     val monomorphic_prop_of = prop_of o Thm.unvarify_global o Drule.zero_var_indexes;
    57 
    58     fun massage_inject (tp $ (eqv $ (_ $ t $ u) $ rhs)) = tp $ (eqv $ mk_fcT_eq (t, u) $ rhs);
    59     fun massage_distinct (tp $ (_ $ (_ $ t $ u))) = [tp $ false_eq (t, u), tp $ false_eq (u, t)];
    60 
    61     val triv_inject_goals =
    62       map_filter (fn c as (_, T) =>
    63           if T = fcT then SOME (HOLogic.mk_Trueprop (true_eq (Const c, Const c))) else NONE)
    64         ctrs;
    65     val inject_goals = map (massage_inject o monomorphic_prop_of) inject_thms;
    66     val distinct_goals = maps (massage_distinct o monomorphic_prop_of) distinct_thms;
    67     val refl_goal = HOLogic.mk_Trueprop (true_eq (Free ("x", fcT), Free ("x", fcT)));
    68 
    69     val simp_ctxt =
    70       Simplifier.global_context thy HOL_basic_ss
    71         addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms));
    72 
    73     fun prove goal =
    74       Goal.prove_sorry_global thy [] [] goal (K (ALLGOALS (simp_tac simp_ctxt)))
    75       |> Simpdata.mk_eq;
    76   in
    77     (map prove (triv_inject_goals @ inject_goals @ distinct_goals), prove refl_goal)
    78   end;
    79 
    80 fun add_equality fcT fcT_name As ctrs inject_thms distinct_thms =
    81   let
    82     fun add_def lthy =
    83       let
    84         fun mk_side const_name =
    85           Const (const_name, fcT --> fcT --> HOLogic.boolT) $ Free ("x", fcT) $ Free ("y", fcT);
    86         val spec =
    87           mk_Trueprop_eq (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq})
    88           |> Syntax.check_term lthy;
    89         val ((_, (_, raw_def)), lthy') =
    90           Specification.definition (NONE, (Attrib.empty_binding, spec)) lthy;
    91         val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy); (* FIXME? *)
    92         val def = singleton (Proof_Context.export lthy' ctxt_thy) raw_def;
    93       in
    94         (def, lthy')
    95       end;
    96 
    97     fun tac ctxt thms = Class.intro_classes_tac [] THEN ALLGOALS (Proof_Context.fact_tac ctxt thms);
    98 
    99     val qualify =
   100       Binding.qualify true (Long_Name.base_name fcT_name) o Binding.qualify true eqN o Binding.name;
   101   in
   102     Class.instantiation ([fcT_name], map dest_TFree As, [HOLogic.class_equal])
   103     #> add_def
   104     #-> Class.prove_instantiation_exit_result (map o Morphism.thm) tac o single
   105     #-> fold Code.del_eqn
   106     #> `(mk_free_ctr_equations fcT ctrs inject_thms distinct_thms)
   107     #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.lemmaK
   108       [((qualify reflN, [Code.add_nbe_default_eqn_attribute]), [([thm], [])]),
   109         ((qualify simpsN, [Code.add_default_eqn_attribute]), [(rev thms, [])])])
   110     #> snd
   111   end;
   112 
   113 fun add_ctr_code fcT_name raw_As raw_ctrs inject_thms distinct_thms case_thms thy =
   114   let
   115     val As = map (perhaps (try Logic.unvarifyT_global)) raw_As;
   116     val ctrs = map (apsnd (perhaps (try Logic.unvarifyT_global))) raw_ctrs;
   117     val fcT = Type (fcT_name, As);
   118     val unover_ctrs = map (fn ctr as (_, fcT) => (Axclass.unoverload_const thy ctr, fcT)) ctrs;
   119   in
   120     if can (Code.constrset_of_consts thy) unover_ctrs then
   121       thy
   122       |> Code.add_datatype ctrs
   123       |> fold_rev Code.add_default_eqn case_thms
   124       |> Code.add_case (mk_case_certificate thy case_thms)
   125       |> not (Sorts.has_instance (Sign.classes_of thy) fcT_name [HOLogic.class_equal])
   126         ? add_equality fcT fcT_name As ctrs inject_thms distinct_thms
   127     else
   128       thy
   129   end;
   130 
   131 end;