src/HOL/Codatatype/Tools/bnf_sugar.ML
author blanchet
Thu Aug 30 09:47:46 2012 +0200 (2012-08-30)
changeset 49019 fc4decdba5ce
parent 49017 66fc7fc2d49b
child 49020 f379cf5d71bd
permissions -rw-r--r--
more work on BNF sugar
blanchet@49017
     1
(*  Title:      HOL/Codatatype/Tools/bnf_sugar.ML
blanchet@49017
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@49017
     3
    Copyright   2012
blanchet@49017
     4
blanchet@49017
     5
Sugar on top of a BNF.
blanchet@49017
     6
*)
blanchet@49017
     7
blanchet@49017
     8
signature BNF_SUGAR =
blanchet@49017
     9
sig
blanchet@49017
    10
end;
blanchet@49017
    11
blanchet@49017
    12
structure BNF_Sugar : BNF_SUGAR =
blanchet@49017
    13
struct
blanchet@49017
    14
blanchet@49017
    15
open BNF_Util
blanchet@49019
    16
open BNF_FP_Util
blanchet@49017
    17
blanchet@49019
    18
val distinctN = "distinct";
blanchet@49019
    19
blanchet@49019
    20
fun prepare_sugar prep_typ prep_term ((((raw_T, raw_ctors), raw_dtors), raw_storss), raw_recur)
blanchet@49019
    21
  lthy =
blanchet@49017
    22
  let
blanchet@49019
    23
    (* TODO: sanity checks on arguments *)
blanchet@49017
    24
blanchet@49019
    25
    val T as Type (T_name, _) = prep_typ lthy raw_T;
blanchet@49019
    26
    val b = Binding.qualified_name T_name;
blanchet@49019
    27
blanchet@49019
    28
    val ctors = map (prep_term lthy) raw_ctors;
blanchet@49017
    29
    val ctor_Tss = map (binder_types o fastype_of) ctors;
blanchet@49017
    30
blanchet@49019
    31
    val ((xss, yss), _) = lthy |>
blanchet@49019
    32
      mk_Freess "x" ctor_Tss
blanchet@49019
    33
      ||>> mk_Freess "y" ctor_Tss;
blanchet@49019
    34
blanchet@49019
    35
    val goal_injects =
blanchet@49017
    36
      let
blanchet@49019
    37
        fun mk_goal _ [] [] = NONE
blanchet@49019
    38
          | mk_goal ctor xs ys =
blanchet@49019
    39
            SOME (HOLogic.mk_Trueprop (HOLogic.mk_eq
blanchet@49019
    40
              (HOLogic.mk_eq (Term.list_comb (ctor, xs), Term.list_comb (ctor, ys)),
blanchet@49019
    41
               Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys))));
blanchet@49017
    42
      in
blanchet@49019
    43
        map_filter I (map3 mk_goal ctors xss yss)
blanchet@49017
    44
      end;
blanchet@49017
    45
blanchet@49019
    46
    val goal_half_distincts =
blanchet@49019
    47
      let
blanchet@49019
    48
        fun mk_goal t u = HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (t, u)));
blanchet@49019
    49
        fun mk_goals [] = []
blanchet@49019
    50
          | mk_goals (t :: ts) = fold_rev (cons o mk_goal t) ts (mk_goals ts);
blanchet@49019
    51
      in
blanchet@49019
    52
        mk_goals (map2 (curry Term.list_comb) ctors xss)
blanchet@49019
    53
      end;
blanchet@49019
    54
blanchet@49019
    55
    val goals = [goal_injects, goal_half_distincts];
blanchet@49019
    56
blanchet@49019
    57
    fun after_qed thmss lthy =
blanchet@49019
    58
      let
blanchet@49019
    59
        val [inject_thms, half_distinct_thms] = thmss;
blanchet@49019
    60
blanchet@49019
    61
        val other_half_distinct_thms = map (fn thm => thm RS not_sym) half_distinct_thms;
blanchet@49019
    62
blanchet@49019
    63
        fun note thmN thms =
blanchet@49019
    64
          snd o Local_Theory.note
blanchet@49019
    65
            ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), thms);
blanchet@49019
    66
      in
blanchet@49019
    67
        lthy
blanchet@49019
    68
        |> note injectN inject_thms
blanchet@49019
    69
        |> note distinctN (half_distinct_thms @ other_half_distinct_thms)
blanchet@49019
    70
      end;
blanchet@49017
    71
  in
blanchet@49019
    72
    (goals, after_qed, lthy)
blanchet@49017
    73
  end;
blanchet@49017
    74
blanchet@49017
    75
val parse_binding_list = Parse.$$$ "[" |--  Parse.list Parse.binding --| Parse.$$$ "]";
blanchet@49017
    76
blanchet@49019
    77
val bnf_sugar_cmd = (fn (goalss, after_qed, lthy) =>
blanchet@49019
    78
  Proof.theorem NONE after_qed (map (map (rpair [])) goalss) lthy) oo
blanchet@49019
    79
  prepare_sugar Syntax.read_typ Syntax.read_term;
blanchet@49017
    80
blanchet@49017
    81
val _ =
blanchet@49017
    82
  Outer_Syntax.local_theory_to_proof @{command_spec "bnf_sugar"} "adds sugar on top of a BNF"
blanchet@49017
    83
    ((Parse.typ -- (Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") --
blanchet@49017
    84
      parse_binding_list -- (Parse.$$$ "[" |-- Parse.list parse_binding_list --| Parse.$$$ "]") --
blanchet@49017
    85
      Parse.term) >> bnf_sugar_cmd);
blanchet@49017
    86
blanchet@49017
    87
end;