# HG changeset patch # User blanchet # Date 1380629125 -7200 # Node ID b15cfc2864dede0d8b84eb5f11f183d6bad778bc # Parent 07028b08045f4d21ead28199c11657401a5e9e07 refactoring -- splitting between constructor sugar dependencies and true BNF dependencies diff -r 07028b08045f -r b15cfc2864de src/HOL/BNF/BNF_Util.thy --- a/src/HOL/BNF/BNF_Util.thy Tue Oct 01 14:05:25 2013 +0200 +++ b/src/HOL/BNF/BNF_Util.thy Tue Oct 01 14:05:25 2013 +0200 @@ -9,7 +9,7 @@ header {* Library for Bounded Natural Functors *} theory BNF_Util -imports "../Cardinals/Cardinal_Arithmetic" +imports Ctr_Sugar "../Cardinals/Cardinal_Arithmetic" begin lemma subset_Collect_iff: "B \ A \ (B \ {x \ A. P x}) = (\x \ B. P x)" diff -r 07028b08045f -r b15cfc2864de src/HOL/BNF/Ctr_Sugar.thy --- a/src/HOL/BNF/Ctr_Sugar.thy Tue Oct 01 14:05:25 2013 +0200 +++ b/src/HOL/BNF/Ctr_Sugar.thy Tue Oct 01 14:05:25 2013 +0200 @@ -8,7 +8,7 @@ header {* Wrapping Existing Freely Generated Type's Constructors *} theory Ctr_Sugar -imports BNF_Util +imports Main keywords "wrap_free_constructors" :: thy_goal and "no_discs_sels" and @@ -23,6 +23,7 @@ "\ Q \ P \ Q \ P \ R" by blast+ +ML_file "Tools/ctr_sugar_util.ML" ML_file "Tools/ctr_sugar_tactics.ML" ML_file "Tools/ctr_sugar.ML" diff -r 07028b08045f -r b15cfc2864de src/HOL/BNF/Tools/bnf_tactics.ML --- a/src/HOL/BNF/Tools/bnf_tactics.ML Tue Oct 01 14:05:25 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_tactics.ML Tue Oct 01 14:05:25 2013 +0200 @@ -8,11 +8,9 @@ signature BNF_TACTICS = sig - val ss_only : thm list -> Proof.context -> Proof.context + include CTR_SUGAR_GENERAL_TACTICS - val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic val fo_rtac: thm -> Proof.context -> int -> tactic - val unfold_thms_tac: Proof.context -> thm list -> tactic val mk_unfold_thms_then_tac: Proof.context -> thm list -> ('a -> tactic) -> 'a -> tactic val mk_flatten_assoc_tac: (int -> tactic) -> thm -> thm -> thm -> tactic @@ -35,13 +33,9 @@ structure BNF_Tactics : BNF_TACTICS = struct +open Ctr_Sugar_General_Tactics open BNF_Util -fun ss_only ths ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps ths - -fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl, - tac, REPEAT_DETERM_N (n - k) o etac thin_rl]); - (*stolen from Christian Urban's Cookbook*) fun fo_rtac thm = Subgoal.FOCUS (fn {concl, ...} => let @@ -51,9 +45,6 @@ rtac (Drule.instantiate_normalize insts thm) 1 end); -fun unfold_thms_tac _ [] = all_tac - | unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms); - fun mk_unfold_thms_then_tac lthy defs tac x = unfold_thms_tac lthy defs THEN tac x; (*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*) diff -r 07028b08045f -r b15cfc2864de src/HOL/BNF/Tools/bnf_util.ML --- a/src/HOL/BNF/Tools/bnf_util.ML Tue Oct 01 14:05:25 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_util.ML Tue Oct 01 14:05:25 2013 +0200 @@ -7,10 +7,8 @@ signature BNF_UTIL = sig - val map3: ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list - val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list - val map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f) -> - 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list + include CTR_SUGAR_UTIL + val map6: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list val map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) -> @@ -32,9 +30,6 @@ val map13: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list - val fold_map2: ('a -> 'b -> 'c -> 'd * 'c) -> 'a list -> 'b list -> 'c -> 'd list * 'c - val fold_map3: ('a -> 'b -> 'c -> 'd -> 'e * 'd) -> - 'a list -> 'b list -> 'c list -> 'd -> 'e list * 'd val fold_map4: ('a -> 'b -> 'c -> 'd -> 'e -> 'f * 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e -> 'f list * 'e val fold_map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g * 'f) -> @@ -50,35 +45,16 @@ 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i list -> 'j -> 'k list * 'j val split_list4: ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list - val splice: 'a list -> 'a list -> 'a list - val transpose: 'a list list -> 'a list list - val seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list - val pad_list: 'a -> int -> 'a list -> 'a list + val find_indices: ('b * 'a -> bool) -> 'a list -> 'b list -> int list - val find_indices: ('b * 'a -> bool) -> 'a list -> 'b list -> int list - val permute_like: ('a * 'b -> bool) -> 'a list -> 'b list -> 'c list -> 'c list - - val mk_fresh_names: Proof.context -> int -> string -> string list * Proof.context - val mk_TFrees: int -> Proof.context -> typ list * Proof.context val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context - val mk_TFrees': sort list -> Proof.context -> typ list * Proof.context - val mk_Frees: string -> typ list -> Proof.context -> term list * Proof.context - val mk_Freess: string -> typ list list -> Proof.context -> term list list * Proof.context val mk_Freesss: string -> typ list list list -> Proof.context -> term list list list * Proof.context val mk_Freessss: string -> typ list list list list -> Proof.context -> term list list list list * Proof.context - val mk_Frees': string -> typ list -> Proof.context -> - (term list * (string * typ) list) * Proof.context - val mk_Freess': string -> typ list list -> Proof.context -> - (term list list * (string * typ) list list) * Proof.context val nonzero_string_of_int: int -> string - val resort_tfree: sort -> typ -> typ val retype_free: typ -> term -> term val typ_subst_nonatomic: (typ * typ) list -> typ -> typ - val variant_types: string list -> sort list -> Proof.context -> - (string * sort) list * Proof.context - val variant_tfrees: string list -> Proof.context -> typ list * Proof.context val binder_fun_types: typ -> typ list val body_fun_type: typ -> typ @@ -86,8 +62,6 @@ val strip_fun_type: typ -> typ list * typ val strip_typeN: int -> typ -> typ list * typ - val mk_predT: typ list -> typ - val mk_pred1T: typ -> typ val mk_pred2T: typ -> typ -> typ val mk_relT: typ * typ -> typ val dest_relT: typ -> typ * typ @@ -105,8 +79,6 @@ val mk_Field: term -> term val mk_Gr: term -> term -> term val mk_Grp: term -> term -> term - val mk_IfN: typ -> term list -> term list -> term - val mk_Trueprop_eq: term * term -> term val mk_UNION: term -> term -> term val mk_Union: typ -> term val mk_card_binop: string -> (typ * typ -> typ) -> term -> term -> term @@ -129,13 +101,6 @@ val mk_rel_compp: term * term -> term val mk_wpull: term -> term -> term -> term -> term -> (term * term) option -> term -> term -> term - val rapp: term -> term -> term - - val list_all_free: term list -> term -> term - val list_exists_free: term list -> term -> term - - val fo_match: Proof.context -> term -> term -> Type.tyenv * Envir.tenv - (*parameterized terms*) val mk_nthN: int -> term -> int -> term @@ -144,7 +109,6 @@ val mk_conjIN: int -> thm val mk_conjunctN: int -> int -> thm val conj_dests: int -> thm -> thm list - val mk_disjIN: int -> int -> thm val mk_nthI: int -> int -> thm val mk_nth_conv: int -> int -> thm val mk_ordLeq_csum: int -> int -> thm -> thm @@ -162,7 +126,6 @@ val subset_UNIV: thm val mk_sym: thm -> thm val mk_trans: thm -> thm -> thm - val mk_unabs_def: int -> thm -> thm val is_triv_implies: thm -> bool val is_refl: thm -> bool @@ -172,14 +135,7 @@ val cterm_instantiate_pos: cterm option list -> thm -> thm val fold_thms: Proof.context -> thm list -> thm -> thm - val unfold_thms: Proof.context -> thm list -> thm -> thm - val certifyT: Proof.context -> typ -> ctyp - val certify: Proof.context -> term -> cterm - - val standard_binding: binding - val equal_binding: binding - val parse_binding: binding parser val parse_binding_colon: binding parser val parse_opt_binding_colon: binding parser @@ -198,20 +154,9 @@ structure BNF_Util : BNF_UTIL = struct -(* Library proper *) - -fun map3 _ [] [] [] = [] - | map3 f (x1::x1s) (x2::x2s) (x3::x3s) = f x1 x2 x3 :: map3 f x1s x2s x3s - | map3 _ _ _ _ = raise ListPair.UnequalLengths; +open Ctr_Sugar_Util -fun map4 _ [] [] [] [] = [] - | map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) = f x1 x2 x3 x4 :: map4 f x1s x2s x3s x4s - | map4 _ _ _ _ _ = raise ListPair.UnequalLengths; - -fun map5 _ [] [] [] [] [] = [] - | map5 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) = - f x1 x2 x3 x4 x5 :: map5 f x1s x2s x3s x4s x5s - | map5 _ _ _ _ _ _ = raise ListPair.UnequalLengths; +(* Library proper *) fun map6 _ [] [] [] [] [] [] = [] | map6 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) = @@ -260,22 +205,6 @@ map13 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s | map13 _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; -fun fold_map2 _ [] [] acc = ([], acc) - | fold_map2 f (x1::x1s) (x2::x2s) acc = - let - val (x, acc') = f x1 x2 acc; - val (xs, acc'') = fold_map2 f x1s x2s acc'; - in (x :: xs, acc'') end - | fold_map2 _ _ _ _ = raise ListPair.UnequalLengths; - -fun fold_map3 _ [] [] [] acc = ([], acc) - | fold_map3 f (x1::x1s) (x2::x2s) (x3::x3s) acc = - let - val (x, acc') = f x1 x2 x3 acc; - val (xs, acc'') = fold_map3 f x1s x2s x3s acc'; - in (x :: xs, acc'') end - | fold_map3 _ _ _ _ _ = raise ListPair.UnequalLengths; - fun fold_map4 _ [] [] [] [] acc = ([], acc) | fold_map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) acc = let @@ -331,17 +260,6 @@ let val (xs1, xs2, xs3, xs4) = split_list4 xs; in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4) end; -(*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*) -fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt); -fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt); - -(* The standard binding stands for a name generated following the canonical convention (e.g., - "is_Nil" from "Nil"). The smart binding is either the standard binding or no binding at all, - depending on the context. *) -val standard_binding = @{binding _}; -val equal_binding = @{binding "="}; - -val parse_binding = Parse.binding || @{keyword "="} >> K equal_binding; val parse_binding_colon = parse_binding --| @{keyword ":"}; val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty; @@ -387,13 +305,8 @@ fun nonzero_string_of_int 0 = "" | nonzero_string_of_int n = string_of_int n; -val mk_TFrees' = apfst (map TFree) oo Variable.invent_types; - -fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS); val mk_TFreess = fold_map mk_TFrees; -fun resort_tfree S (TFree (s, _)) = TFree (s, S); - (*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*) fun typ_subst_nonatomic [] = I | typ_subst_nonatomic inst = @@ -402,32 +315,12 @@ | subst T = perhaps (AList.lookup (op =) inst) T; in subst end; -fun mk_names n x = if n = 1 then [x] else map (fn i => x ^ string_of_int i) (1 upto n); - -fun mk_fresh_names ctxt = (fn xs => Variable.variant_fixes xs ctxt) oo mk_names; -fun mk_Frees x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => map2 (curry Free) xs Ts); -fun mk_Freess x Tss = fold_map2 mk_Frees (mk_names (length Tss) x) Tss; fun mk_Freesss x Tsss = fold_map2 mk_Freess (mk_names (length Tsss) x) Tsss; fun mk_Freessss x Tssss = fold_map2 mk_Freesss (mk_names (length Tssss) x) Tssss; -fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts)); -fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list; fun retype_free T (Free (s, _)) = Free (s, T) | retype_free _ t = raise TERM ("retype_free", [t]); -fun ensure_prefix pre s = s |> not (String.isPrefix pre s) ? prefix pre; - -fun variant_types ss Ss ctxt = - let - val (tfrees, _) = - fold_map2 (fn s => fn S => Name.variant s #> apfst (rpair S)) ss Ss (Variable.names_of ctxt); - val ctxt' = fold (Variable.declare_constraints o Logic.mk_type o TFree) tfrees ctxt; - in (tfrees, ctxt') end; - -fun variant_tfrees ss = - apfst (map TFree) o - variant_types (map (ensure_prefix "'") ss) (replicate (length ss) HOLogic.typeS); - (** Types **) @@ -447,8 +340,6 @@ val binder_fun_types = fst o strip_fun_type; val body_fun_type = snd o strip_fun_type; -fun mk_predT Ts = Ts ---> HOLogic.boolT; -fun mk_pred1T T = mk_predT [T]; fun mk_pred2T T U = mk_predT [T, U]; val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT; val dest_relT = HOLogic.dest_prodT o HOLogic.dest_setT; @@ -465,12 +356,6 @@ (** Operators **) -val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq; - -fun mk_IfN _ _ [t] = t - | mk_IfN T (c :: cs) (t :: ts) = - Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ c $ t $ mk_IfN T cs ts; - fun mk_converse R = let val RT = dest_relT (fastype_of R); @@ -637,21 +522,6 @@ let val T = (case xs of [] => defT | (x::_) => fastype_of x); in Const (@{const_name collect}, HOLogic.mk_setT T --> T) $ (HOLogic.mk_set T xs) end; -fun rapp u t = betapply (t, u); - -fun list_quant_free quant_const = - fold_rev (fn free => fn P => - let val (x, T) = Term.dest_Free free; - in quant_const T $ Term.absfree (x, T) P end); - -val list_all_free = list_quant_free HOLogic.all_const; -val list_exists_free = list_quant_free HOLogic.exists_const; - -fun fo_match ctxt t pat = - let val thy = Proof_Context.theory_of ctxt in - Pattern.first_order_match thy (pat, t) (Vartab.empty, Vartab.empty) - end; - fun find_indices eq xs ys = map_filter I (map_index (fn (i, y) => if member eq xs y then SOME i else NONE) ys); @@ -699,11 +569,6 @@ fun mk_conjIN 1 = @{thm TrueE[OF TrueI]} | mk_conjIN n = mk_conjIN (n - 1) RSN (2, conjI); -fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]} - | mk_disjIN _ 1 = disjI1 - | mk_disjIN 2 2 = disjI2 - | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2; - fun mk_ordLeq_csum 1 1 thm = thm | mk_ordLeq_csum _ 1 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum1}] | mk_ordLeq_csum 2 2 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum2}] @@ -730,26 +595,6 @@ | mk_UnIN n m = mk_UnIN' (n - m) end; -fun splice xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys); - -fun transpose [] = [] - | transpose ([] :: xss) = transpose xss - | transpose xss = map hd xss :: transpose (map tl xss); - -fun permute_like eq xs xs' ys = map (nth ys o (fn y => find_index (fn x => eq (x, y)) xs)) xs'; - -fun seq_conds f n k xs = - if k = n then - map (f false) (take (k - 1) xs) - else - let val (negs, pos) = split_last (take k xs) in - map (f false) negs @ [f true pos] - end; - -fun pad_list x n xs = xs @ replicate (n - length xs) x; - -fun mk_unabs_def n = funpow n (fn thm => thm RS fun_cong); - fun is_triv_implies thm = op aconv (Logic.dest_implies (Thm.prop_of thm)) handle TERM _ => false; @@ -776,6 +621,5 @@ end; fun fold_thms ctxt thms = Local_Defs.fold ctxt (distinct Thm.eq_thm_prop thms); -fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms); end; diff -r 07028b08045f -r b15cfc2864de src/HOL/BNF/Tools/ctr_sugar.ML --- a/src/HOL/BNF/Tools/ctr_sugar.ML Tue Oct 01 14:05:25 2013 +0200 +++ b/src/HOL/BNF/Tools/ctr_sugar.ML Tue Oct 01 14:05:25 2013 +0200 @@ -60,7 +60,7 @@ structure Ctr_Sugar : CTR_SUGAR = struct -open BNF_Util +open Ctr_Sugar_Util open Ctr_Sugar_Tactics type ctr_sugar = @@ -779,14 +779,14 @@ val (safe_collapse_thms, all_collapse_thms) = let - fun mk_goal m ctr udisc usel_ctr = + fun mk_goal m udisc usel_ctr = let val prem = HOLogic.mk_Trueprop udisc; val concl = mk_Trueprop_eq ((usel_ctr, u) |> m = 0 ? swap); in (prem aconv concl, Logic.all u (Logic.mk_implies (prem, concl))) end; - val (trivs, goals) = map4 mk_goal ms ctrs udiscs usel_ctrs |> split_list; + val (trivs, goals) = map3 mk_goal ms udiscs usel_ctrs |> split_list; val thms = map5 (fn m => fn discD => fn sel_thms => fn triv => fn goal => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => diff -r 07028b08045f -r b15cfc2864de src/HOL/BNF/Tools/ctr_sugar_tactics.ML --- a/src/HOL/BNF/Tools/ctr_sugar_tactics.ML Tue Oct 01 14:05:25 2013 +0200 +++ b/src/HOL/BNF/Tools/ctr_sugar_tactics.ML Tue Oct 01 14:05:25 2013 +0200 @@ -5,8 +5,16 @@ Tactics for wrapping existing freely generated type's constructors. *) +signature CTR_SUGAR_GENERAL_TACTICS = +sig + val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic + val unfold_thms_tac: Proof.context -> thm list -> tactic +end; + signature CTR_SUGAR_TACTICS = sig + include CTR_SUGAR_GENERAL_TACTICS + val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic val mk_case_tac: Proof.context -> int -> int -> thm -> thm list -> thm list list -> tactic val mk_case_cong_tac: Proof.context -> thm -> thm list -> tactic @@ -29,11 +37,16 @@ structure Ctr_Sugar_Tactics : CTR_SUGAR_TACTICS = struct -open BNF_Util -open BNF_Tactics +open Ctr_Sugar_Util val meta_mp = @{thm meta_mp}; +fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl, + tac, REPEAT_DETERM_N (n - k) o etac thin_rl]); + +fun unfold_thms_tac _ [] = all_tac + | unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms); + fun if_P_or_not_P_OF pos thm = thm RS (if pos then @{thm if_P} else @{thm if_not_P}); fun mk_nchotomy_tac n exhaust = @@ -155,3 +168,5 @@ HEADGOAL (rtac refl); end; + +structure Ctr_Sugar_General_Tactics: CTR_SUGAR_GENERAL_TACTICS = Ctr_Sugar_Tactics; diff -r 07028b08045f -r b15cfc2864de src/HOL/BNF/Tools/ctr_sugar_util.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BNF/Tools/ctr_sugar_util.ML Tue Oct 01 14:05:25 2013 +0200 @@ -0,0 +1,192 @@ +(* Title: HOL/BNF/Tools/ctr_sugar_util.ML + Author: Jasmin Blanchette, TU Muenchen + Copyright 2012 + +Library for wrapping existing freely generated type's constructors. +*) + +signature CTR_SUGAR_UTIL = +sig + val map3: ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list + val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list + val map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f) -> + 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list + val fold_map2: ('a -> 'b -> 'c -> 'd * 'c) -> 'a list -> 'b list -> 'c -> 'd list * 'c + val fold_map3: ('a -> 'b -> 'c -> 'd -> 'e * 'd) -> + 'a list -> 'b list -> 'c list -> 'd -> 'e list * 'd + val seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list + val transpose: 'a list list -> 'a list list + val pad_list: 'a -> int -> 'a list -> 'a list + val splice: 'a list -> 'a list -> 'a list + val permute_like: ('a * 'b -> bool) -> 'a list -> 'b list -> 'c list -> 'c list + + val mk_names: int -> string -> string list + val mk_fresh_names: Proof.context -> int -> string -> string list * Proof.context + val mk_TFrees': sort list -> Proof.context -> typ list * Proof.context + val mk_TFrees: int -> Proof.context -> typ list * Proof.context + val mk_Frees': string -> typ list -> Proof.context -> + (term list * (string * typ) list) * Proof.context + val mk_Freess': string -> typ list list -> Proof.context -> + (term list list * (string * typ) list list) * Proof.context + val mk_Frees: string -> typ list -> Proof.context -> term list * Proof.context + val mk_Freess: string -> typ list list -> Proof.context -> term list list * Proof.context + val resort_tfree: sort -> typ -> typ + val variant_types: string list -> sort list -> Proof.context -> + (string * sort) list * Proof.context + val variant_tfrees: string list -> Proof.context -> typ list * Proof.context + + val mk_predT: typ list -> typ + val mk_pred1T: typ -> typ + + val mk_disjIN: int -> int -> thm + + val mk_unabs_def: int -> thm -> thm + + val mk_IfN: typ -> term list -> term list -> term + val mk_Trueprop_eq: term * term -> term + + val rapp: term -> term -> term + + val list_all_free: term list -> term -> term + val list_exists_free: term list -> term -> term + + val fo_match: Proof.context -> term -> term -> Type.tyenv * Envir.tenv + + val unfold_thms: Proof.context -> thm list -> thm -> thm + + val certifyT: Proof.context -> typ -> ctyp + val certify: Proof.context -> term -> cterm + + val standard_binding: binding + val equal_binding: binding + val parse_binding: binding parser + + val ss_only: thm list -> Proof.context -> Proof.context +end; + +structure Ctr_Sugar_Util : CTR_SUGAR_UTIL = +struct + +fun map3 _ [] [] [] = [] + | map3 f (x1::x1s) (x2::x2s) (x3::x3s) = f x1 x2 x3 :: map3 f x1s x2s x3s + | map3 _ _ _ _ = raise ListPair.UnequalLengths; + +fun map4 _ [] [] [] [] = [] + | map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) = f x1 x2 x3 x4 :: map4 f x1s x2s x3s x4s + | map4 _ _ _ _ _ = raise ListPair.UnequalLengths; + +fun map5 _ [] [] [] [] [] = [] + | map5 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) = + f x1 x2 x3 x4 x5 :: map5 f x1s x2s x3s x4s x5s + | map5 _ _ _ _ _ _ = raise ListPair.UnequalLengths; + +fun fold_map2 _ [] [] acc = ([], acc) + | fold_map2 f (x1::x1s) (x2::x2s) acc = + let + val (x, acc') = f x1 x2 acc; + val (xs, acc'') = fold_map2 f x1s x2s acc'; + in (x :: xs, acc'') end + | fold_map2 _ _ _ _ = raise ListPair.UnequalLengths; + +fun fold_map3 _ [] [] [] acc = ([], acc) + | fold_map3 f (x1::x1s) (x2::x2s) (x3::x3s) acc = + let + val (x, acc') = f x1 x2 x3 acc; + val (xs, acc'') = fold_map3 f x1s x2s x3s acc'; + in (x :: xs, acc'') end + | fold_map3 _ _ _ _ _ = raise ListPair.UnequalLengths; + +fun seq_conds f n k xs = + if k = n then + map (f false) (take (k - 1) xs) + else + let val (negs, pos) = split_last (take k xs) in + map (f false) negs @ [f true pos] + end; + +fun transpose [] = [] + | transpose ([] :: xss) = transpose xss + | transpose xss = map hd xss :: transpose (map tl xss); + +fun pad_list x n xs = xs @ replicate (n - length xs) x; + +fun splice xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys); + +fun permute_like eq xs xs' ys = map (nth ys o (fn y => find_index (fn x => eq (x, y)) xs)) xs'; + +fun mk_names n x = if n = 1 then [x] else map (fn i => x ^ string_of_int i) (1 upto n); +fun mk_fresh_names ctxt = (fn xs => Variable.variant_fixes xs ctxt) oo mk_names; + +val mk_TFrees' = apfst (map TFree) oo Variable.invent_types; + +fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS); + +fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts)); +fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list; + +fun mk_Frees x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => map2 (curry Free) xs Ts); +fun mk_Freess x Tss = fold_map2 mk_Frees (mk_names (length Tss) x) Tss; + +fun resort_tfree S (TFree (s, _)) = TFree (s, S); + +fun ensure_prefix pre s = s |> not (String.isPrefix pre s) ? prefix pre; + +fun variant_types ss Ss ctxt = + let + val (tfrees, _) = + fold_map2 (fn s => fn S => Name.variant s #> apfst (rpair S)) ss Ss (Variable.names_of ctxt); + val ctxt' = fold (Variable.declare_constraints o Logic.mk_type o TFree) tfrees ctxt; + in (tfrees, ctxt') end; + +fun variant_tfrees ss = + apfst (map TFree) o + variant_types (map (ensure_prefix "'") ss) (replicate (length ss) HOLogic.typeS); + +fun mk_predT Ts = Ts ---> HOLogic.boolT; +fun mk_pred1T T = mk_predT [T]; + +fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]} + | mk_disjIN _ 1 = disjI1 + | mk_disjIN 2 2 = disjI2 + | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2; + +fun mk_unabs_def n = funpow n (fn thm => thm RS fun_cong); + +fun mk_IfN _ _ [t] = t + | mk_IfN T (c :: cs) (t :: ts) = + Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ c $ t $ mk_IfN T cs ts; + +val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq; + +fun rapp u t = betapply (t, u); + +fun list_quant_free quant_const = + fold_rev (fn free => fn P => + let val (x, T) = Term.dest_Free free; + in quant_const T $ Term.absfree (x, T) P end); + +val list_all_free = list_quant_free HOLogic.all_const; +val list_exists_free = list_quant_free HOLogic.exists_const; + +fun fo_match ctxt t pat = + let val thy = Proof_Context.theory_of ctxt in + Pattern.first_order_match thy (pat, t) (Vartab.empty, Vartab.empty) + end; + +fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms); + +(*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*) +fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt); +fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt); + +(* The standard binding stands for a name generated following the canonical convention (e.g., + "is_Nil" from "Nil"). In contrast, the empty binding is either the standard binding or no + binding at all, depending on the context. *) +val standard_binding = @{binding _}; +val equal_binding = @{binding "="}; + +val parse_binding = Parse.binding || @{keyword "="} >> K equal_binding; + +fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms; + +end;