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