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