src/HOL/Library/simps_case_conv.ML
author wenzelm
Fri, 06 Sep 2013 12:05:01 +0200
changeset 53433 3b356b7f7cad
parent 53429 9d9945941eab
child 54401 f6950854855d
permissions -rw-r--r--
more standard header;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
53426
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
     1
(*  Title:      HOL/Library/simps_case_conv.ML
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
     2
    Author:     Lars Noschinski, TU Muenchen
53433
3b356b7f7cad more standard header;
wenzelm
parents: 53429
diff changeset
     3
    Author:     Gerwin Klein, NICTA
53426
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
     4
53433
3b356b7f7cad more standard header;
wenzelm
parents: 53429
diff changeset
     5
Convert function specifications between the representation as a list
3b356b7f7cad more standard header;
wenzelm
parents: 53429
diff changeset
     6
of equations (with patterns on the lhs) and a single equation (with a
3b356b7f7cad more standard header;
wenzelm
parents: 53429
diff changeset
     7
nested case expression on the rhs).
53426
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
     8
*)
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
     9
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    10
signature SIMPS_CASE_CONV =
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    11
sig
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    12
  val to_case: Proof.context -> thm list -> thm
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    13
  val gen_to_simps: Proof.context -> thm list -> thm -> thm list
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    14
  val to_simps: Proof.context -> thm -> thm list
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    15
end
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    16
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    17
structure Simps_Case_Conv: SIMPS_CASE_CONV =
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    18
struct
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    19
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    20
(* Collects all type constructors in a type *)
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    21
fun collect_Tcons (Type (name,Ts)) = name :: maps collect_Tcons Ts
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    22
  | collect_Tcons (TFree _) = []
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    23
  | collect_Tcons (TVar _) = []
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    24
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    25
fun get_split_ths thy = collect_Tcons
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    26
    #> distinct (op =)
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    27
    #> map_filter (Datatype_Data.get_info thy)
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    28
    #> map #split
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    29
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    30
val strip_eq = prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    31
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    32
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    33
local
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    34
53429
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    35
  fun transpose [] = []
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    36
    | transpose ([] :: xss) = transpose xss
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    37
    | transpose xss = map hd xss :: transpose (map tl xss);
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    38
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    39
  fun same_fun (ts as _ $ _ :: _) =
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    40
      let
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    41
        val (fs, argss) = map strip_comb ts |> split_list
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    42
        val f = hd fs
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    43
      in if forall (fn x => f = x) fs then SOME (f, argss) else NONE end
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    44
    | same_fun _ = NONE
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    45
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    46
  (* pats must be non-empty *)
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    47
  fun split_pat pats ctxt =
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    48
      case same_fun pats of
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    49
        NONE =>
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    50
          let
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    51
            val (name, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    52
            val var = Free (name, fastype_of (hd pats))
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    53
          in (((var, [var]), map single pats), ctxt') end
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    54
      | SOME (f, argss) =>
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    55
          let
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    56
            val (((def_pats, def_frees), case_patss), ctxt') =
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    57
              split_pats argss ctxt
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    58
            val def_pat = list_comb (f, def_pats)
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    59
          in (((def_pat, flat def_frees), case_patss), ctxt') end
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    60
  and
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    61
      split_pats patss ctxt =
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    62
        let
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    63
          val (splitted, ctxt') = fold_map split_pat (transpose patss) ctxt
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    64
          val r = splitted |> split_list |> apfst split_list |> apsnd (transpose #> map flat)
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    65
        in (r, ctxt') end
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    66
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    67
(*
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    68
  Takes a list lhss of left hand sides (which are lists of patterns)
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    69
  and a list rhss of right hand sides. Returns
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    70
    - a single equation with a (nested) case-expression on the rhs
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    71
    - a list of all split-thms needed to split the rhs
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    72
  Patterns which have the same outer context in all lhss remain
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    73
  on the lhs of the computed equation.
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    74
*)
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    75
fun build_case_t fun_t lhss rhss ctxt =
53426
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    76
  let
53429
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    77
    val (((def_pats, def_frees), case_patss), ctxt') =
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    78
      split_pats lhss ctxt
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    79
    val pattern = map HOLogic.mk_tuple case_patss
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    80
    val case_arg = HOLogic.mk_tuple (flat def_frees)
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    81
    val cases = Case_Translation.make_case ctxt' Case_Translation.Warning Name.context
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    82
      case_arg (pattern ~~ rhss)
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    83
    val split_thms = get_split_ths (Proof_Context.theory_of ctxt') (fastype_of case_arg)
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    84
    val t = (list_comb (fun_t, def_pats), cases)
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    85
      |> HOLogic.mk_eq
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    86
      |> HOLogic.mk_Trueprop
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
    87
  in ((t, split_thms), ctxt') end
53426
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    88
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    89
fun tac ctxt {splits, intros, defs} =
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    90
  let val ctxt' = Classical.addSIs (ctxt, intros) in
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    91
    REPEAT_DETERM1 (FIRSTGOAL (split_tac splits))
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    92
    THEN Local_Defs.unfold_tac ctxt defs
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    93
    THEN safe_tac ctxt'
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    94
  end
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    95
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    96
fun import [] ctxt = ([], ctxt)
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    97
  | import (thm :: thms) ctxt =
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    98
    let
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
    99
      val fun_ct = strip_eq #> fst #> strip_comb #> fst #> Logic.mk_term
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   100
        #> Thm.cterm_of (Proof_Context.theory_of ctxt)
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   101
      val ct = fun_ct thm
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   102
      val cts = map fun_ct thms
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   103
      val pairs = map (fn s => (s,ct)) cts
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   104
      val thms' = map (fn (th,p) => Thm.instantiate (Thm.match p) th) (thms ~~ pairs)
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   105
    in Variable.import true (thm :: thms') ctxt |> apfst snd end
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   106
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   107
in
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   108
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   109
(*
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   110
  For a list
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   111
    f p_11 ... p_1n = t1
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   112
    f p_21 ... p_2n = t2
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   113
    ...
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   114
    f p_mn ... p_mn = tm
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   115
  of theorems, prove a single theorem
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   116
    f x1 ... xn = t
53429
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
   117
  where t is a (nested) case expression. f must not be a function
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
   118
  application. Moreover, the terms p_11, ..., p_mn must be non-overlapping
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
   119
  datatype patterns. The patterns must be exhausting up to common constructor
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
   120
  contexts.
53426
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   121
*)
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   122
fun to_case ctxt ths =
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   123
  let
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   124
    val (iths, ctxt') = import ths ctxt
53429
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
   125
    val fun_t = hd iths |> strip_eq |> fst |> head_of
53426
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   126
    val eqs = map (strip_eq #> apfst (snd o strip_comb)) iths
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   127
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   128
    fun hide_rhs ((pat, rhs), name) lthy = let
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   129
        val frees = fold Term.add_frees pat []
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   130
        val abs_rhs = fold absfree frees rhs
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   131
        val ((f,def), lthy') = Local_Defs.add_def
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   132
          ((Binding.name name, Mixfix.NoSyn), abs_rhs) lthy
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   133
      in ((list_comb (f, map Free (rev frees)), def), lthy') end
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   134
53429
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
   135
    val ((def_ts, def_thms), ctxt2) = let
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
   136
        val nctxt = Variable.names_of ctxt'
53426
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   137
        val names = Name.invent nctxt "rhs" (length eqs)
53429
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
   138
      in fold_map hide_rhs (eqs ~~ names) ctxt' |> apfst split_list end
53426
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   139
53429
9d9945941eab allowed less exhaustive patterns
noschinl
parents: 53426
diff changeset
   140
    val ((t, split_thms), ctxt3) = build_case_t fun_t (map fst eqs) def_ts ctxt2
53426
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   141
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   142
    val th = Goal.prove ctxt3 [] [] t (fn {context=ctxt, ...} =>
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   143
          tac ctxt {splits=split_thms, intros=ths, defs=def_thms})
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   144
  in th
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   145
    |> singleton (Proof_Context.export ctxt3 ctxt)
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   146
    |> Goal.norm_result
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   147
  end
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   148
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   149
end
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   150
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   151
local
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   152
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   153
fun was_split t =
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   154
  let
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   155
    val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   156
              o fst o HOLogic.dest_imp
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   157
    val get_conjs = HOLogic.dest_conj o HOLogic.dest_Trueprop
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   158
    fun dest_alls (Const ("HOL.All", _) $ Abs (_, _, t)) = dest_alls t
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   159
      | dest_alls t = t
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   160
  in forall (is_free_eq_imp o dest_alls) (get_conjs t) end
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   161
        handle TERM _ => false
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   162
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   163
fun apply_split ctxt split thm = Seq.of_list
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   164
  let val ((_,thm'), ctxt') = Variable.import false [thm] ctxt in
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   165
    (Variable.export ctxt' ctxt) (filter (was_split o prop_of) (thm' RL [split]))
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   166
  end
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   167
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   168
fun forward_tac rules t = Seq.of_list ([t] RL rules)
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   169
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   170
val refl_imp = refl RSN (2, mp)
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   171
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   172
val get_rules_once_split =
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   173
  REPEAT (forward_tac [conjunct1, conjunct2])
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   174
    THEN REPEAT (forward_tac [spec])
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   175
    THEN (forward_tac [refl_imp])
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   176
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   177
fun do_split ctxt split =
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   178
  let
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   179
    val split' = split RS iffD1;
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   180
    val split_rhs = concl_of (hd (snd (fst (Variable.import false [split'] ctxt))))
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   181
  in if was_split split_rhs
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   182
     then DETERM (apply_split ctxt split') THEN get_rules_once_split
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   183
     else raise TERM ("malformed split rule", [split_rhs])
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   184
  end
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   185
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   186
val atomize_meta_eq = forward_tac [meta_eq_to_obj_eq]
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   187
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   188
in
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   189
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   190
fun gen_to_simps ctxt splitthms thm =
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   191
  Seq.list_of ((TRY atomize_meta_eq
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   192
                 THEN (REPEAT (FIRST (map (do_split ctxt) splitthms)))) thm)
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   193
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   194
fun to_simps ctxt thm =
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   195
  let
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   196
    val T = thm |> strip_eq |> fst |> strip_comb |> fst |> fastype_of
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   197
    val splitthms = get_split_ths (Proof_Context.theory_of ctxt) T
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   198
  in gen_to_simps ctxt splitthms thm end
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   199
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   200
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   201
end
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   202
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   203
fun case_of_simps_cmd (bind, thms_ref) lthy =
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   204
  let
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   205
    val thy = Proof_Context.theory_of lthy
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   206
    val bind' = apsnd (map (Attrib.intern_src thy)) bind
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   207
    val thm = (Attrib.eval_thms lthy) thms_ref |> to_case lthy
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   208
  in
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   209
    Local_Theory.note (bind', [thm]) lthy |> snd
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   210
  end
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   211
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   212
fun simps_of_case_cmd ((bind, thm_ref), splits_ref) lthy =
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   213
  let
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   214
    val thy = Proof_Context.theory_of lthy
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   215
    val bind' = apsnd (map (Attrib.intern_src thy)) bind
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   216
    val thm = singleton (Attrib.eval_thms lthy) thm_ref
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   217
    val simps = if null splits_ref
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   218
      then to_simps lthy thm
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   219
      else gen_to_simps lthy (Attrib.eval_thms lthy splits_ref) thm
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   220
  in
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   221
    Local_Theory.note (bind', simps) lthy |> snd
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   222
  end
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   223
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   224
val _ =
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   225
  Outer_Syntax.local_theory @{command_spec "case_of_simps"}
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   226
    "turns a list of equations into a case expression"
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   227
    (Parse_Spec.opt_thm_name ":"  -- Parse_Spec.xthms1 >> case_of_simps_cmd)
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   228
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   229
val parse_splits = @{keyword "("} |-- Parse.reserved "splits" |-- @{keyword ":"} |--
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   230
  Parse_Spec.xthms1 --| @{keyword ")"}
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   231
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   232
val _ =
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   233
  Outer_Syntax.local_theory @{command_spec "simps_of_case"}
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   234
    "perform case split on rule"
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   235
    (Parse_Spec.opt_thm_name ":"  -- Parse_Spec.xthm --
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   236
      Scan.optional parse_splits [] >> simps_of_case_cmd)
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   237
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   238
end
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff changeset
   239