src/HOL/Tools/Function/function_lib.ML
author wenzelm
Fri Mar 06 15:58:56 2015 +0100 (2015-03-06)
changeset 59621 291934bac95e
parent 59618 e6939796717e
child 59625 aacdce52b2fc
permissions -rw-r--r--
Thm.cterm_of and Thm.ctyp_of operate on local context;
haftmann@37744
     1
(*  Title:      HOL/Tools/Function/function_lib.ML
krauss@33099
     2
    Author:     Alexander Krauss, TU Muenchen
krauss@33099
     3
krauss@41113
     4
Ad-hoc collection of function waiting to be eliminated, generalized,
krauss@41113
     5
moved elsewhere or otherwise cleaned up.
krauss@33099
     6
*)
krauss@33099
     7
krauss@41113
     8
signature FUNCTION_LIB =
krauss@41113
     9
sig
krauss@41113
    10
  val plural: string -> string -> 'a list -> string
krauss@41113
    11
krauss@41113
    12
  val dest_all_all: term -> term list * term
krauss@41113
    13
krauss@41113
    14
  val unordered_pairs: 'a list -> ('a * 'a) list
krauss@41113
    15
krauss@41113
    16
  val rename_bound: string -> term -> term
krauss@41113
    17
  val mk_forall_rename: (string * term) -> term -> term
krauss@41113
    18
  val forall_intr_rename: (string * cterm) -> thm -> thm
krauss@41113
    19
krauss@41113
    20
  datatype proof_attempt = Solved of thm | Stuck of thm | Fail
krauss@41113
    21
  val try_proof: cterm -> tactic -> proof_attempt
krauss@41113
    22
krauss@41113
    23
  val dest_binop_list: string -> term -> term list
krauss@41113
    24
  val regroup_conv: string -> string -> thm list -> int list -> conv
krauss@41113
    25
  val regroup_union_conv: int list -> conv
blanchet@54406
    26
blanchet@54407
    27
  val inst_constrs_of: Proof.context -> typ -> term list
krauss@41113
    28
end
krauss@41113
    29
krauss@41113
    30
structure Function_Lib: FUNCTION_LIB =
krauss@33099
    31
struct
krauss@33099
    32
krauss@40076
    33
(* "The variable" ^ plural " is" "s are" vs *)
krauss@33099
    34
fun plural sg pl [x] = sg
krauss@33099
    35
  | plural sg pl _ = pl
krauss@33099
    36
krauss@33099
    37
krauss@33099
    38
(* Removes all quantifiers from a term, replacing bound variables by frees. *)
wenzelm@56245
    39
fun dest_all_all (t as (Const (@{const_name Pure.all},_) $ _)) =
krauss@34232
    40
  let
krauss@40076
    41
    val (v,b) = Logic.dest_all t |> apfst Free
krauss@34232
    42
    val (vs, b') = dest_all_all b
krauss@34232
    43
  in
krauss@34232
    44
    (v :: vs, b')
krauss@34232
    45
  end
krauss@33099
    46
  | dest_all_all t = ([],t)
haftmann@33611
    47
krauss@33099
    48
krauss@33099
    49
(* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *)
krauss@33099
    50
fun unordered_pairs [] = []
krauss@33099
    51
  | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs
krauss@33099
    52
krauss@33099
    53
krauss@42497
    54
(* renaming bound variables *)
krauss@33099
    55
krauss@34232
    56
fun rename_bound n (Q $ Abs (_, T, b)) = (Q $ Abs (n, T, b))
krauss@33099
    57
  | rename_bound n _ = raise Match
krauss@33099
    58
krauss@33099
    59
fun mk_forall_rename (n, v) =
krauss@34232
    60
  rename_bound n o Logic.all v
krauss@33099
    61
krauss@33099
    62
fun forall_intr_rename (n, cv) thm =
krauss@34232
    63
  let
wenzelm@36945
    64
    val allthm = Thm.forall_intr cv thm
wenzelm@59582
    65
    val (_ $ abs) = Thm.prop_of allthm
wenzelm@45156
    66
  in Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy)) allthm end
krauss@33099
    67
krauss@33099
    68
krauss@33099
    69
datatype proof_attempt = Solved of thm | Stuck of thm | Fail
krauss@33099
    70
krauss@34232
    71
fun try_proof cgoal tac =
krauss@34232
    72
  case SINGLE tac (Goal.init cgoal) of
krauss@34232
    73
    NONE => Fail
krauss@34232
    74
  | SOME st =>
krauss@34232
    75
    if Thm.no_prems st
krauss@34232
    76
    then Solved (Goal.finish (Syntax.init_pretty_global (Thm.theory_of_cterm cgoal)) st)
krauss@34232
    77
    else Stuck st
krauss@33099
    78
krauss@33099
    79
krauss@34232
    80
fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) =
krauss@34232
    81
  if cn = n then dest_binop_list cn a @ dest_binop_list cn b else [ t ]
krauss@33099
    82
  | dest_binop_list _ t = [ t ]
krauss@33099
    83
krauss@33099
    84
krauss@33099
    85
(* separate two parts in a +-expression:
krauss@33099
    86
   "a + b + c + d + e" --> "(a + b + d) + (c + e)"
krauss@33099
    87
krauss@33099
    88
   Here, + can be any binary operation that is AC.
krauss@33099
    89
krauss@33099
    90
   cn - The name of the binop-constructor (e.g. @{const_name Un})
krauss@33099
    91
   ac - the AC rewrite rules for cn
krauss@33099
    92
   is - the list of indices of the expressions that should become the first part
krauss@33099
    93
        (e.g. [0,1,3] in the above example)
krauss@33099
    94
*)
krauss@33099
    95
krauss@33099
    96
fun regroup_conv neu cn ac is ct =
krauss@33099
    97
 let
wenzelm@59582
    98
   val thy = Thm.theory_of_cterm ct
wenzelm@54742
    99
   val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
wenzelm@54742
   100
krauss@33099
   101
   val mk = HOLogic.mk_binop cn
wenzelm@59582
   102
   val t = Thm.term_of ct
krauss@33099
   103
   val xs = dest_binop_list cn t
krauss@33099
   104
   val js = subtract (op =) is (0 upto (length xs) - 1)
krauss@33099
   105
   val ty = fastype_of t
krauss@33099
   106
 in
wenzelm@54883
   107
   Goal.prove_internal ctxt []
wenzelm@59621
   108
     (Thm.cterm_of ctxt
krauss@33099
   109
       (Logic.mk_equals (t,
haftmann@33611
   110
          if null is
krauss@33099
   111
          then mk (Const (neu, ty), foldr1 mk (map (nth xs) js))
haftmann@33611
   112
          else if null js
krauss@33099
   113
            then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
krauss@33099
   114
            else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
wenzelm@54742
   115
     (K (rewrite_goals_tac ctxt ac
wenzelm@59498
   116
         THEN resolve_tac ctxt [Drule.reflexive_thm] 1))
krauss@33099
   117
 end
krauss@33099
   118
krauss@33099
   119
(* instance for unions *)
krauss@34232
   120
val regroup_union_conv =
wenzelm@35402
   121
  regroup_conv @{const_abbrev Set.empty} @{const_name Lattices.sup}
krauss@34232
   122
    (map (fn t => t RS eq_reflection)
krauss@34232
   123
      (@{thms Un_ac} @ @{thms Un_empty_right} @ @{thms Un_empty_left}))
krauss@33099
   124
krauss@33099
   125
blanchet@54407
   126
fun inst_constrs_of ctxt (Type (name, Ts)) =
blanchet@54407
   127
    map (Ctr_Sugar.mk_ctr Ts) (#ctrs (the (Ctr_Sugar.ctr_sugar_of ctxt name)))
blanchet@54407
   128
  | inst_constrs_of _ _ = raise Match
blanchet@54406
   129
krauss@33099
   130
end