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