# HG changeset patch # User wenzelm # Date 1412784617 -7200 # Node ID 9b33fe5b60f3084105bb4ca63c069e12a60b9364 # Parent 1329679abb2d1c771a895f89a0aebfed54e3d08a# Parent 010b610eb55d1e3e5512c4783ef1043d9720159e merged diff -r 1329679abb2d -r 9b33fe5b60f3 NEWS --- a/NEWS Wed Oct 08 10:22:00 2014 +0200 +++ b/NEWS Wed Oct 08 18:10:17 2014 +0200 @@ -126,11 +126,20 @@ generated code in target languages in HOL/Library/Code_Test. See HOL/Codegenerator_Test/Code_Test* for examples. +* Library/Sum_of_Squares: simplified and improved "sos" method. Always +use local CSDP executable, which is much faster than the NEOS server. +The "sos_cert" functionality is invoked as "sos" with additional +argument. Minor INCOMPATIBILITY. + + *** ML *** * Tactical PARALLEL_ALLGOALS is the most common way to refer to PARALLEL_GOALS. +* Basic combinators map, fold, fold_map, split_list are available as +parameterized antiquotations, e.g. @{map 4} for lists of quadruples. + *** System *** diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Library/Sum_of_Squares.thy --- a/src/HOL/Library/Sum_of_Squares.thy Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Library/Sum_of_Squares.thy Wed Oct 08 18:10:17 2014 +0200 @@ -3,8 +3,8 @@ Author: Philipp Meyer, TU Muenchen *) -header {* A decision method for universal multivariate real arithmetic with addition, - multiplication and ordering using semidefinite programming *} +header {* A decision procedure for universal multivariate real arithmetic + with addition, multiplication and ordering using semidefinite programming *} theory Sum_of_Squares imports Complex_Main @@ -15,27 +15,4 @@ ML_file "Sum_of_Squares/positivstellensatz_tools.ML" ML_file "Sum_of_Squares/sos_wrapper.ML" -text {* - Proof method sos invocations: - \begin{itemize} - - \item remote solver: @{text "(sos remote_csdp)"} - - \item local solver: @{text "(sos csdp)"} - - The latter requires a local executable from - @{url "https://projects.coin-or.org/Csdp"} and the Isabelle settings variable - variable @{text ISABELLE_CSDP} pointing to it. - - \end{itemize} - - By default, method sos calls @{text remote_csdp}. This can take of - the order of a minute for one sos call, because sos calls CSDP - repeatedly. If you install CSDP locally, sos calls typically takes - only a few seconds. - - The sos method generates a certificate which can be used to repeat - the proof without calling an external prover. -*} - end diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Library/Sum_of_Squares/etc/settings --- a/src/HOL/Library/Sum_of_Squares/etc/settings Wed Oct 08 10:22:00 2014 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -# -*- shell-script -*- :mode=shellscript: - -ISABELLE_SUM_OF_SQUARES="$COMPONENT" -ISABELLE_NEOS_SERVER="http://neos-server.org:3332" - -# local SDP Solver, cf. https://projects.coin-or.org/Csdp -#ISABELLE_CSDP="/usr/local/bin/csdp" - diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Library/Sum_of_Squares/neos_csdp_client --- a/src/HOL/Library/Sum_of_Squares/neos_csdp_client Wed Oct 08 10:22:00 2014 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,85 +0,0 @@ -#!/usr/bin/env python -import sys -import signal -import xmlrpclib -import time -import re -import os - -# Neos server config -neos = xmlrpclib.Server(os.getenv("ISABELLE_NEOS_SERVER")) - -jobNumber = 0 -password = "" -inputfile = None -outputfile = None -# interrupt handler -def cleanup(signal, frame): - sys.stdout.write("Caught interrupt, cleaning up\n") - if jobNumber != 0: - neos.killJob(jobNumber, password) - if inputfile != None: - inputfile.close() - if outputfile != None: - outputfile.close() - sys.exit(21) - -signal.signal(signal.SIGHUP, cleanup) -signal.signal(signal.SIGINT, cleanup) -signal.signal(signal.SIGQUIT, cleanup) -signal.signal(signal.SIGTERM, cleanup) - -if len(sys.argv) <> 3: - sys.stderr.write("Usage: neos_csdp_client \n") - sys.exit(19) - -xml_pre = "\nsdp\ncsdp\nSPARSE_SDPA\n\n\n" -xml = xml_pre -inputfile = open(sys.argv[1],"r") -buffer = 1 -while buffer: - buffer = inputfile.read() - xml += buffer -inputfile.close() -xml += xml_post - -(jobNumber,password) = neos.submitJob(xml) - -if jobNumber == 0: - sys.stdout.write("error submitting job: %s" % password) - sys.exit(20) -else: - sys.stdout.write("jobNumber = %d\tpassword = %s\n" % (jobNumber,password)) - -offset=0 -messages = "" -status="Waiting" -while status == "Running" or status=="Waiting": - time.sleep(1) - (msg,offset) = neos.getIntermediateResults(jobNumber,password,offset) - messages += msg.data - sys.stdout.write(msg.data) - status = neos.getJobStatus(jobNumber, password) - -msg = neos.getFinalResults(jobNumber, password).data -sys.stdout.write("---------- Begin CSDP Output -------------\n"); -sys.stdout.write(msg) - -# extract solution -result = msg.split("Solution:") -if len(result) > 1: - solution = result[1].strip() - if solution != "": - outputfile = open(sys.argv[2],"w") - outputfile.write(solution) - outputfile.close() - -# extract return code -p = re.compile(r"^Error: Command exited with non-zero status (\d+)$", re.MULTILINE) -m = p.search(messages) -if m: - sys.exit(int(m.group(1))) -else: - sys.exit(0) - diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML --- a/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML Wed Oct 08 18:10:17 2014 +0200 @@ -7,14 +7,16 @@ signature POSITIVSTELLENSATZ_TOOLS = sig - val pss_tree_to_cert : RealArith.pss_tree -> string - val cert_to_pss_tree : Proof.context -> string -> RealArith.pss_tree + val print_cert: RealArith.pss_tree -> string + val read_cert: Proof.context -> string -> RealArith.pss_tree end -structure PositivstellensatzTools : POSITIVSTELLENSATZ_TOOLS = +structure Positivstellensatz_Tools : POSITIVSTELLENSATZ_TOOLS = struct -(*** certificate generation ***) +(** print certificate **) + +local fun string_of_rat r = let @@ -24,6 +26,7 @@ else string_of_int nom ^ "/" ^ string_of_int den end + (* map polynomials to strings *) fun string_of_varpow x k = @@ -48,7 +51,7 @@ fun string_of_cmonomial (m,c) = if FuncUtil.Ctermfunc.is_empty m then string_of_rat c else if c = Rat.one then string_of_monomial m - else string_of_rat c ^ "*" ^ string_of_monomial m; + else string_of_rat c ^ "*" ^ string_of_monomial m fun string_of_poly p = if FuncUtil.Monomialfunc.is_empty p then "0" @@ -56,7 +59,10 @@ let val cms = map string_of_cmonomial (sort (prod_ord FuncUtil.monomial_order (K EQUAL)) (FuncUtil.Monomialfunc.dest p)) - in foldr1 (fn (t1, t2) => t1 ^ " + " ^ t2) cms end; + in foldr1 (fn (t1, t2) => t1 ^ " + " ^ t2) cms end + + +(* print cert *) fun pss_to_cert (RealArith.Axiom_eq i) = "A=" ^ string_of_int i | pss_to_cert (RealArith.Axiom_le i) = "A<=" ^ string_of_int i @@ -72,15 +78,22 @@ | pss_to_cert (RealArith.Product (pss1, pss2)) = "(" ^ pss_to_cert pss1 ^ " * " ^ pss_to_cert pss2 ^ ")" -fun pss_tree_to_cert RealArith.Trivial = "()" - | pss_tree_to_cert (RealArith.Cert pss) = "(" ^ pss_to_cert pss ^ ")" - | pss_tree_to_cert (RealArith.Branch (t1, t2)) = - "(" ^ pss_tree_to_cert t1 ^ " & " ^ pss_tree_to_cert t2 ^ ")" +in + +fun print_cert RealArith.Trivial = "()" + | print_cert (RealArith.Cert pss) = "(" ^ pss_to_cert pss ^ ")" + | print_cert (RealArith.Branch (t1, t2)) = + "(" ^ print_cert t1 ^ " & " ^ print_cert t2 ^ ")" + +end -(*** certificate parsing ***) + +(** read certificate **) -(* basic parser *) +local + +(* basic parsers *) val str = Scan.this_string @@ -89,12 +102,12 @@ >> foldl1 (fn (n, d) => n * 10 + d) val nat = number -val int = Scan.optional (str "~" >> K ~1) 1 -- nat >> op *; +val int = Scan.optional (str "~" >> K ~1) 1 -- nat >> op * val rat = int --| str "/" -- int >> Rat.rat_of_quotient val rat_int = rat || int >> Rat.rat_of_int -(* polynomial parser *) +(* polynomial parsers *) fun repeat_sep s f = f ::: Scan.repeat (str s |-- f) @@ -115,7 +128,7 @@ (fn xs => fold FuncUtil.Monomialfunc.update xs FuncUtil.Monomialfunc.empty) -(* positivstellensatz parser *) +(* positivstellensatz parsers *) val parse_axiom = (str "A=" |-- int >> RealArith.Axiom_eq) || @@ -150,12 +163,13 @@ str "(" |-- pt --| str "&" -- pt --| str ")" >> RealArith.Branch) input end +in -(* scanner *) - -fun cert_to_pss_tree ctxt input_str = +fun read_cert ctxt input_str = Symbol.scanner "Bad certificate" (parse_cert_tree ctxt) (filter_out Symbol.is_blank (Symbol.explode input_str)) end +end + diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Library/Sum_of_Squares/sos_wrapper.ML --- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Wed Oct 08 18:10:17 2014 +0200 @@ -1,14 +1,12 @@ (* Title: HOL/Library/Sum_of_Squares/sos_wrapper.ML Author: Philipp Meyer, TU Muenchen -Added functionality for sums of squares, e.g. calling a remote prover. +Wrapper for "sos" proof method. *) signature SOS_WRAPPER = sig - datatype prover_result = Success | Failure | Error - val dest_dir: string Config.T - val prover_name: string Config.T + val sos_tac: Proof.context -> string option -> int -> tactic end structure SOS_Wrapper: SOS_WRAPPER = @@ -20,70 +18,8 @@ | str_of_result Failure = "Failure" | str_of_result Error = "Error" - -(*** calling provers ***) - -val dest_dir = Attrib.setup_config_string @{binding sos_dest_dir} (K "") - -fun filename dir name = - let - val probfile = Path.basic (name ^ serial_string ()) - val dir_path = Path.explode dir - in - if dir = "" then - File.tmp_path probfile - else if File.exists dir_path then - Path.append dir_path probfile - else error ("No such directory: " ^ dir) - end - -fun run_solver ctxt name exe find_failure input = - let - val _ = warning ("Calling solver: " ^ name) - - (* create input file *) - val dir = Config.get ctxt dest_dir - val input_file = filename dir "sos_in" - val _ = File.write input_file input - - (* call solver *) - val output_file = filename dir "sos_out" - val (output, rv) = - Isabelle_System.bash_output - (if File.exists exe then - space_implode " " (map File.shell_path [exe, input_file, output_file]) - else error ("Bad executable: " ^ File.platform_path exe)) - - (* read and analyze output *) - val (res, res_msg) = find_failure rv - val result = if File.exists output_file then File.read output_file else "" - - (* remove temporary files *) - val _ = - if dir = "" then - (File.rm input_file; if File.exists output_file then File.rm output_file else ()) - else () - - val _ = - if Config.get ctxt Sum_of_Squares.trace - then writeln ("Solver output:\n" ^ output) - else () - - val _ = warning (str_of_result res ^ ": " ^ res_msg) - in - (case res of - Success => result - | Failure => raise Sum_of_Squares.Failure res_msg - | Error => error ("Prover failed: " ^ res_msg)) - end - - -(*** various provers ***) - -(* local csdp client *) - -fun find_csdp_failure rv = - case rv of +fun get_result rc = + (case rc of 0 => (Success, "SDP solved") | 1 => (Failure, "SDP is primal infeasible") | 2 => (Failure, "SDP is dual infeasible") @@ -94,62 +30,49 @@ | 7 => (Failure, "Lack of progress") | 8 => (Failure, "X, Z, or O was singular") | 9 => (Failure, "Detected NaN or Inf values") - | _ => (Error, "return code is " ^ string_of_int rv) - -val csdp = (Path.explode "$ISABELLE_CSDP", find_csdp_failure) - - -(* remote neos server *) + | _ => (Error, "return code is " ^ string_of_int rc)) -fun find_neos_failure rv = - case rv of - 20 => (Error, "error submitting job") - | 21 => (Error, "interrupt") - | _ => find_csdp_failure rv - -val neos_csdp = (Path.explode "$ISABELLE_SUM_OF_SQUARES/neos_csdp_client", find_neos_failure) - - -(* named provers *) +fun run_solver ctxt input = + Isabelle_System.with_tmp_file "sos_in" "" (fn in_path => + Isabelle_System.with_tmp_file "sos_out" "" (fn out_path => + let + val _ = File.write in_path input -fun prover "remote_csdp" = neos_csdp - | prover "csdp" = csdp - | prover name = error ("Unknown prover: " ^ name) + val (output, rc) = + Isabelle_System.bash_output + ("\"$ISABELLE_CSDP\" " ^ File.shell_path in_path ^ " " ^ File.shell_path out_path) + val _ = Sum_of_Squares.debug_message ctxt (fn () => "Solver output:\n" ^ output) -val prover_name = Attrib.setup_config_string @{binding sos_prover_name} (K "remote_csdp") + val result = if File.exists out_path then File.read out_path else "" -fun call_solver ctxt opt_name = - let - val name = the_default (Config.get ctxt prover_name) opt_name - val (exe, find_failure) = prover name - in run_solver ctxt name exe find_failure end - - -(* certificate output *) - -fun output_line cert = - "To repeat this proof with a certificate use this command:\n" ^ - Active.sendback_markup [] ("apply (sos_cert \"" ^ cert ^ "\")") - -val print_cert = warning o output_line o PositivstellensatzTools.pss_tree_to_cert + val (res, res_msg) = get_result rc + val _ = Sum_of_Squares.trace_message ctxt (fn () => str_of_result res ^ ": " ^ res_msg) + in + (case res of + Success => result + | Failure => raise Sum_of_Squares.Failure res_msg + | Error => error ("Prover failed: " ^ res_msg)) + end)) (* method setup *) -fun sos_solver print method = SIMPLE_METHOD' o Sum_of_Squares.sos_tac print method +fun print_cert cert = + (writeln o Markup.markup Markup.information) + ("To repeat this proof with a certificate use this command:\n" ^ + Active.sendback_markup [] ("by (sos \"" ^ Positivstellensatz_Tools.print_cert cert ^ "\")")) + +fun sos_tac ctxt NONE = + Sum_of_Squares.sos_tac print_cert + (Sum_of_Squares.Prover (run_solver ctxt)) ctxt + | sos_tac ctxt (SOME cert) = + Sum_of_Squares.sos_tac ignore + (Sum_of_Squares.Certificate (Positivstellensatz_Tools.read_cert ctxt cert)) ctxt val _ = Theory.setup (Method.setup @{binding sos} - (Scan.lift (Scan.option Parse.xname) - >> (fn opt_name => fn ctxt => - sos_solver print_cert - (Sum_of_Squares.Prover (call_solver ctxt opt_name)) ctxt)) - "prove universal problems over the reals using sums of squares" #> - Method.setup @{binding sos_cert} - (Scan.lift Parse.string - >> (fn cert => fn ctxt => - sos_solver ignore - (Sum_of_Squares.Certificate (PositivstellensatzTools.cert_to_pss_tree ctxt cert)) ctxt)) - "prove universal problems over the reals using sums of squares with certificates") + (Scan.lift (Scan.option Parse.string) + >> (fn arg => fn ctxt => SIMPLE_METHOD' (sos_tac ctxt arg))) + "prove universal problems over the reals using sums of squares") end diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Library/Sum_of_Squares/sum_of_squares.ML --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Wed Oct 08 18:10:17 2014 +0200 @@ -10,6 +10,9 @@ datatype proof_method = Certificate of RealArith.pss_tree | Prover of string -> string val sos_tac: (RealArith.pss_tree -> unit) -> proof_method -> Proof.context -> int -> tactic val trace: bool Config.T + val debug: bool Config.T + val trace_message: Proof.context -> (unit -> string) -> unit + val debug_message: Proof.context -> (unit -> string) -> unit exception Failure of string; end @@ -52,7 +55,13 @@ val pow2 = rat_pow rat_2; val pow10 = rat_pow rat_10; + val trace = Attrib.setup_config_bool @{binding sos_trace} (K false); +val debug = Attrib.setup_config_bool @{binding sos_debug} (K false); + +fun trace_message ctxt msg = + if Config.get ctxt trace orelse Config.get ctxt debug then tracing (msg ()) else (); +fun debug_message ctxt msg = if Config.get ctxt debug then tracing (msg ()) else (); exception Sanity; @@ -125,7 +134,7 @@ fun vector_of_list l = let val n = length l in - (n, fold_rev2 (curry FuncUtil.Intfunc.update) (1 upto n) l FuncUtil.Intfunc.empty): vector + (n, fold_rev FuncUtil.Intfunc.update (1 upto n ~~ l) FuncUtil.Intfunc.empty): vector end; (* Matrices; again rows and columns indexed from 1. *) @@ -583,8 +592,8 @@ (space_implode " " (map string_of_int blocksizes)) ^ "\n" ^ sdpa_of_vector obj ^ - fold_rev2 (fn k => fn m => fn a => sdpa_of_blockdiagonal (k - 1) m ^ a) - (1 upto length mats) mats "" + fold_rev (fn (k, m) => fn a => sdpa_of_blockdiagonal (k - 1) m ^ a) + (1 upto length mats ~~ mats) "" end; (* Run prover on a problem in block diagonal form. *) @@ -674,9 +683,9 @@ val (_(*idmonlist*),ids) = split_list (map2 mk_idmultiplier (1 upto length eqs) eqs) val blocksizes = map length sqmonlist val bigsum = - fold_rev2 (fn p => fn q => fn a => tri_epoly_pmul p q a) eqs ids - (fold_rev2 (fn (p,_) => fn s => fn a => tri_epoly_pmul p s a) monoid sqs - (epoly_of_poly(poly_neg pol))) + fold_rev (fn (p, q) => fn a => tri_epoly_pmul p q a) (eqs ~~ ids) + (fold_rev (fn ((p, _), s) => fn a => tri_epoly_pmul p s a) (monoid ~~ sqs) + (epoly_of_poly (poly_neg pol))) val eqns = FuncUtil.Monomialfunc.fold (fn (_, e) => fn a => e :: a) bigsum [] val (pvs, assig) = tri_eliminate_all_equations (0, 0, 0) eqns val qvars = (0, 0, 0) :: pvs @@ -710,9 +719,7 @@ fun find_rounding d = let val _ = - if Config.get ctxt trace - then writeln ("Trying rounding with limit "^Rat.string_of_rat d ^ "\n") - else () + debug_message ctxt (fn () => "Trying rounding with limit "^Rat.string_of_rat d ^ "\n") val vec = nice_vector d raw_vec val blockmat = iter (1, dim vec) @@ -746,7 +753,7 @@ fun eval_sq sqs = fold_rev (fn (c, q) => poly_add (poly_cmul c (poly_mul q q))) sqs poly_0 val sanity = fold_rev (fn ((p, _), s) => poly_add (poly_mul p (eval_sq s))) msq - (fold_rev2 (fn p => fn q => poly_add (poly_mul p q)) cfs eqs (poly_neg pol)) + (fold_rev (fn (p, q) => poly_add (poly_mul p q)) (cfs ~~ eqs) (poly_neg pol)) in if not(FuncUtil.Monomialfunc.is_empty sanity) then raise Sanity else (cfs, map (fn (a, b) => (snd a, b)) msq) @@ -755,9 +762,10 @@ (* Iterative deepening. *) -fun deepen f n = - (writeln ("Searching with depth limit " ^ string_of_int n); - (f n handle Failure s => (writeln ("failed with message: " ^ s); deepen f (n + 1)))); +fun deepen ctxt f n = + (trace_message ctxt (fn () => "Searching with depth limit " ^ string_of_int n); + (f n handle Failure s => + (trace_message ctxt (fn () => "failed with message: " ^ s); deepen ctxt f (n + 1)))); (* Map back polynomials and their composites to a positivstellensatz. *) @@ -839,7 +847,7 @@ (poly_neg(poly_pow pol i)))) (0 upto k) end - val (_,i,(cert_ideal,cert_cone)) = deepen tryall 0 + val (_,i,(cert_ideal,cert_cone)) = deepen ctxt tryall 0 val proofs_ideal = map2 (fn q => fn (_,ax) => RealArith.Eqmul(q,ax)) cert_ideal eq val proofs_cone = map cterm_of_sos cert_cone diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Library/bnf_lfp_countable.ML --- a/src/HOL/Library/bnf_lfp_countable.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Library/bnf_lfp_countable.ML Wed Oct 08 18:10:17 2014 +0200 @@ -58,7 +58,7 @@ fun mk_encode_injectives_tac ctxt ns induct nchotomys injectss recss map_comps' inj_map_strongs' = HEADGOAL (rtac induct) THEN - EVERY (map4 (fn n => fn nchotomy => fn injects => fn recs => + EVERY (@{map 4} (fn n => fn nchotomy => fn injects => fn recs => mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs') ns nchotomys injectss recss); @@ -166,7 +166,7 @@ val (xs, names_ctxt) = ctxt |> mk_Frees "x" fpTs; - val conjuncts = map3 mk_conjunct fpTs xs (mk_encode_funs ctxt fpTs ns ctrss0 recs0); + val conjuncts = @{map 3} mk_conjunct fpTs xs (mk_encode_funs ctxt fpTs ns ctrss0 recs0); val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj conjuncts); in Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} => diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Wed Oct 08 18:10:17 2014 +0200 @@ -2,8 +2,8 @@ Author: Amine Chaieb, University of Cambridge A generic arithmetic prover based on Positivstellensatz certificates ---- also implements Fourrier-Motzkin elimination as a special case -Fourrier-Motzkin elimination. +--- also implements Fourier-Motzkin elimination as a special case +Fourier-Motzkin elimination. *) (* A functor for finite mappings based on Tables *) @@ -360,7 +360,8 @@ absconv1,absconv2,prover) = let val pre_ss = put_simpset HOL_basic_ss ctxt addsimps - @{thms simp_thms ex_simps all_simps not_all not_ex ex_disj_distrib all_conj_distrib if_bool_eq_disj} + @{thms simp_thms ex_simps all_simps not_all not_ex ex_disj_distrib + all_conj_distrib if_bool_eq_disj} val prenex_ss = put_simpset HOL_basic_ss ctxt addsimps prenex_simps val skolemize_ss = put_simpset HOL_basic_ss ctxt addsimps [choice_iff] val presimp_conv = Simplifier.rewrite pre_ss @@ -439,7 +440,9 @@ let val (p,q) = Thm.dest_binop (concl th) val c = concl th1 - val _ = if c aconvc (concl th2) then () else error "disj_cases : conclusions not alpha convertible" + val _ = + if c aconvc (concl th2) then () + else error "disj_cases : conclusions not alpha convertible" in Thm.implies_elim (Thm.implies_elim (Thm.implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th) (Thm.implies_intr (Thm.apply @{cterm Trueprop} p) th1)) @@ -463,8 +466,12 @@ in overall cert_choice dun (th1::th2::oths) end else if is_disj ct then let - val (th1, cert1) = overall (Left::cert_choice) dun (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths) - val (th2, cert2) = overall (Right::cert_choice) dun (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg ct))::oths) + val (th1, cert1) = + overall (Left::cert_choice) dun + (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths) + val (th2, cert2) = + overall (Right::cert_choice) dun + (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg ct))::oths) in (disj_cases th th1 th2, Branch (cert1, cert2)) end else overall cert_choice (th::dun) oths end @@ -495,7 +502,8 @@ let fun h (acc, t) = case (term_of t) of - Const(@{const_name Ex},_)$Abs(_,_,_) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc)) + Const(@{const_name Ex},_)$Abs(_,_,_) => + h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc)) | _ => (acc,t) in fn t => h ([],t) end @@ -505,7 +513,10 @@ | Var ((s,_),_) => s | _ => "x" - fun mk_forall x th = Drule.arg_cong_rule (instantiate_cterm' [SOME (ctyp_of_term x)] [] @{cpat "All :: (?'a => bool) => _" }) (Thm.abstract_rule (name_of x) x th) + fun mk_forall x th = + Drule.arg_cong_rule + (instantiate_cterm' [SOME (ctyp_of_term x)] [] @{cpat "All :: (?'a => bool) => _" }) + (Thm.abstract_rule (name_of x) x th) val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec)); @@ -527,13 +538,16 @@ | _ => raise THM ("choose",0,[th, th']) fun simple_choose v th = - choose v (Thm.assume ((Thm.apply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th + choose v + (Thm.assume + ((Thm.apply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th val strip_forall = let fun h (acc, t) = case (term_of t) of - Const(@{const_name All},_)$Abs(_,_,_) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc)) + Const(@{const_name All},_)$Abs(_,_,_) => + h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc)) | _ => (acc,t) in fn t => h ([],t) end @@ -560,7 +574,9 @@ val (avs,ibod) = strip_forall bod val th1 = Drule.arg_cong_rule @{cterm Trueprop} (fold mk_forall avs (absremover ibod)) val (th2, certs) = overall [] [] [specl avs (Thm.assume (Thm.rhs_of th1))] - val th3 = fold simple_choose evs (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.apply @{cterm Trueprop} bod))) th2) + val th3 = + fold simple_choose evs + (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.apply @{cterm Trueprop} bod))) th2) in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume nct)) th3), certs) end in (Thm.implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates) diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Multivariate_Analysis/normarith.ML --- a/src/HOL/Multivariate_Analysis/normarith.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/normarith.ML Wed Oct 08 18:10:17 2014 +0200 @@ -295,7 +295,7 @@ val rawverts = vertices nvs constraints fun check_solution v = let - val f = fold_rev2 (curry FuncUtil.Intfunc.update) nvs v (FuncUtil.Intfunc.onefunc (0, Rat.one)) + val f = fold_rev FuncUtil.Intfunc.update (nvs ~~ v) (FuncUtil.Intfunc.onefunc (0, Rat.one)) in forall (fn e => evaluate f e =/ Rat.zero) flippedequations end val goodverts = filter check_solution rawverts diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/ROOT --- a/src/HOL/ROOT Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/ROOT Wed Oct 08 18:10:17 2014 +0200 @@ -600,11 +600,8 @@ ML SAT_Examples Nominal2_Dummy + SOS SOS_Cert - theories [condition = ISABELLE_CSDP] - SOS - theories [condition = ISABELLE_FULL_TEST] - SOS_Remote theories [skip_proofs = false] Meson_Test theories [condition = SVC_HOME] diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/BNF/bnf_comp.ML --- a/src/HOL/Tools/BNF/bnf_comp.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Wed Oct 08 18:10:17 2014 +0200 @@ -154,12 +154,12 @@ ||>> mk_Frees "A" (map HOLogic.mk_setT As) ||>> mk_Frees "x" As; - val CAs = map3 mk_T_of_bnf Dss Ass_repl inners; + val CAs = @{map 3} mk_T_of_bnf Dss Ass_repl inners; val CCA = mk_T_of_bnf oDs CAs outer; - val CBs = map3 mk_T_of_bnf Dss Bss_repl inners; + val CBs = @{map 3} mk_T_of_bnf Dss Bss_repl inners; val outer_sets = mk_sets_of_bnf (replicate olive oDs) (replicate olive CAs) outer; - val inner_setss = map3 mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners; - val inner_bds = map3 mk_bd_of_bnf Dss Ass_repl inners; + val inner_setss = @{map 3} mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners; + val inner_bds = @{map 3} mk_bd_of_bnf Dss Ass_repl inners; val outer_bd = mk_bd_of_bnf oDs CAs outer; (*%f1 ... fn. outer.map (inner_1.map f1 ... fn) ... (inner_m.map f1 ... fn)*) @@ -280,7 +280,7 @@ val single_set_bd_thmss = map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1); in - map3 (fn set'_eq_set => fn set_alt => fn single_set_bds => fn ctxt => + @{map 3} (fn set'_eq_set => fn set_alt => fn single_set_bds => fn ctxt => mk_comp_set_bd_tac ctxt set'_eq_set bd_ordIso_natLeq_thm_opt set_alt single_set_bds) set'_eq_sets set_alt_thms single_set_bd_thmss end; @@ -320,7 +320,7 @@ val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer; val inner_witss = map (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I))) - (map3 (fn Ds => fn n => mk_wits_of_bnf (replicate n Ds) (replicate n As)) + (@{map 3} (fn Ds => fn n => mk_wits_of_bnf (replicate n Ds) (replicate n As)) Dss inwitss inners); val inner_witsss = map (map (nth inner_witss) o fst) outer_wits; @@ -637,7 +637,7 @@ val before_kill_dest = map2 append kill_poss live_poss; val kill_ns = map length kill_poss; val (inners', accum') = - fold_map5 (fn i => permute_and_kill (qualify i)) + @{fold_map 5} (fn i => permute_and_kill (qualify i)) (if length bnfs = 1 then [0] else (1 upto length bnfs)) kill_ns before_kill_src before_kill_dest bnfs accum; @@ -649,7 +649,7 @@ val after_lift_src = map2 append new_poss old_poss; val lift_ns = map (fn xs => length As - length xs) Ass'; in - ((kill_poss, As), fold_map5 (fn i => lift_and_permute (qualify i)) + ((kill_poss, As), @{fold_map 5} (fn i => lift_and_permute (qualify i)) (if length bnfs = 1 then [0] else 1 upto length bnfs) lift_ns after_lift_src after_lift_dest inners' accum') end; @@ -667,7 +667,7 @@ val ((kill_poss, As), (inners', ((cache', unfold_set'), lthy'))) = normalize_bnfs qualify Ass Ds flatten_tyargs inners accum; - val Ds = oDs @ flat (map3 (uncurry append oo curry swap oo map o nth) tfreess kill_poss Dss); + val Ds = oDs @ flat (@{map 3} (uncurry append oo curry swap oo map o nth) tfreess kill_poss Dss); val As = map TFree As; in apfst (rpair (Ds, As)) @@ -931,7 +931,7 @@ val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1)); val ((inners, (Dss, Ass)), (accum', lthy')) = apfst (apsnd split_list o split_list) - (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) flatten_tyargs Xs Ds0) + (@{fold_map 2} (fn i => bnf_of_typ Smart_Inline (qualify i) flatten_tyargs Xs Ds0) (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' accum); in compose_bnf const_policy qualify flatten_tyargs bnf inners oDs Dss Ass (accum', lthy') diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Wed Oct 08 18:10:17 2014 +0200 @@ -864,7 +864,7 @@ val CA = mk_bnf_T Ds As Calpha; val CR = mk_bnf_T Ds RTs Calpha; val setRs = - map3 (fn R => fn T => fn U => + @{map 3} (fn R => fn T => fn U => HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split R) Rs As Bs; (*Grp (in (Collect (split R1) .. Collect (split Rn))) (map fst .. fst)^--1 OO @@ -1057,7 +1057,7 @@ val map_cong0_goal = let - val prems = map4 (mk_map_cong_prem Logic.mk_implies x) zs bnf_sets_As fs fs_copy; + val prems = @{map 4} (mk_map_cong_prem Logic.mk_implies x) zs bnf_sets_As fs fs_copy; val eq = mk_Trueprop_eq (Term.list_comb (bnf_map_AsBs, fs) $ x, Term.list_comb (bnf_map_AsBs, fs_copy) $ x); in @@ -1074,7 +1074,7 @@ fold_rev Logic.all fs (mk_Trueprop_eq (set_comp_map, image_comp_set)) end; in - map3 mk_goal bnf_sets_As bnf_sets_Bs fs + @{map 3} mk_goal bnf_sets_As bnf_sets_Bs fs end; val card_order_bd_goal = HOLogic.mk_Trueprop (mk_card_order bnf_bd_As); @@ -1185,7 +1185,7 @@ fun mk_map_cong mk_implies () = let val prem0 = mk_Trueprop_eq (x, x_copy); - val prems = map4 (mk_map_cong_prem mk_implies x_copy) zs bnf_sets_As fs fs_copy; + val prems = @{map 4} (mk_map_cong_prem mk_implies x_copy) zs bnf_sets_As fs fs_copy; val eq = mk_Trueprop_eq (Term.list_comb (bnf_map_AsBs, fs) $ x, Term.list_comb (bnf_map_AsBs, fs_copy) $ x_copy); val goal = fold_rev Logic.all (x :: x_copy :: fs @ fs_copy) @@ -1364,7 +1364,7 @@ (mk_Ball (setB $ y) (Term.absfree (dest_Free b) (HOLogic.mk_imp (R $ a $ b, S $ a $ b)))))); val prems = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs) $ x $ y) :: - map6 mk_prem bnf_sets_As bnf_sets_Bs Rs Rs_copy zs ys; + @{map 6} mk_prem bnf_sets_As bnf_sets_Bs Rs Rs_copy zs ys; val concl = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs_copy) $ x $ y); in Goal.prove_sorry lthy [] [] @@ -1389,9 +1389,9 @@ [Term.list_comb (relCsBs, S_CsBs) $ (Term.list_comb (bnf_map_AsCs, is) $ x) $ y, Term.list_comb (relAsCs, S_AsCs) $ x $ (Term.list_comb (bnf_map_BsCs, gs) $ y)]; val rhss = - [Term.list_comb (rel, map3 (fn f => fn P => fn T => + [Term.list_comb (rel, @{map 3} (fn f => fn P => fn T => mk_vimage2p f (HOLogic.id_const T) $ P) is S_CsBs Bs') $ x $ y, - Term.list_comb (rel, map3 (fn f => fn P => fn T => + Term.list_comb (rel, @{map 3} (fn f => fn P => fn T => mk_vimage2p (HOLogic.id_const T) f $ P) gs S_AsCs As') $ x $ y]; val goals = map2 mk_goal lhss rhss; in @@ -1451,7 +1451,7 @@ let val rel_sets = map2 (fn A => fn B => mk_rel 1 [A] [B] @{term rel_set}) As' Bs'; val rel_Rs = Term.list_comb (rel, Rs); - val goals = map4 (fn R => fn rel_set => fn setA => fn setB => HOLogic.mk_Trueprop + val goals = @{map 4} (fn R => fn rel_set => fn setA => fn setB => HOLogic.mk_Trueprop (mk_rel_fun rel_Rs (rel_set $ R) $ setA $ setB)) Rs rel_sets bnf_sets_As bnf_sets_Bs; in if null goals then [] @@ -1468,7 +1468,7 @@ fun mk_inj_map_strong () = let - val assms = map5 (fn setA => fn z => fn f => fn z' => fn f' => + val assms = @{map 5} (fn setA => fn z => fn f => fn z' => fn f' => fold_rev Logic.all [z, z'] (Logic.mk_implies (mk_Trueprop_mem (z, setA $ x), Logic.mk_implies (mk_Trueprop_mem (z', setA $ x'), diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Oct 08 18:10:17 2014 +0200 @@ -524,7 +524,7 @@ fun massage_multi_notes b_names Ts = maps (fn (thmN, thmss, attrs) => - map3 (fn b_name => fn Type (T_name, _) => fn thms => + @{map 3} (fn b_name => fn Type (T_name, _) => fn thms => ((Binding.qualify true b_name (Binding.name thmN), attrs T_name), [(thms, [])])) b_names Ts thmss) #> filter_out (null o fst o hd o snd); @@ -788,7 +788,7 @@ [] else [mk_Trueprop_eq (build_rel_app names_lthy Rs [] ta tb, - (case flat (map5 (mk_conjunct n) (1 upto n) discAs selAss discBs selBss) of + (case flat (@{map 5} (mk_conjunct n) (1 upto n) discAs selAss discBs selBss) of [] => @{term True} | conjuncts => Library.foldr1 HOLogic.mk_conj conjuncts))]; @@ -824,7 +824,7 @@ names_ctxt) end; - val (assms, names_lthy) = fold_map2 mk_assms ctrAs ctrBs names_lthy; + val (assms, names_lthy) = @{fold_map 2} mk_assms ctrAs ctrBs names_lthy; val goal = Logic.list_implies (HOLogic.mk_Trueprop rel_Rs_a_b :: assms, thesis); val thm = Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => @@ -968,7 +968,7 @@ ([], ctxt) end; val (goals, names_lthy) = apfst (flat o flat o flat) - (fold_map2 (fn disc => + (@{fold_map 2} (fn disc => fold_map (fn sel => fold_map (mk_goal disc sel) setAs)) discAs selAss names_lthy); in @@ -1072,7 +1072,7 @@ let val Css = map2 replicate ns Cs; val x_Tssss = - map6 (fn absT => fn repT => fn n => fn ms => fn ctr_Tss => fn ctor_rec_fun_T => + @{map 6} (fn absT => fn repT => fn n => fn ms => fn ctr_Tss => fn ctor_rec_fun_T => map2 (map2 unzip_recT) ctr_Tss (dest_absumprodT absT repT n ms (domain_type ctor_rec_fun_T))) absTs repTs ns mss ctr_Tsss ctor_rec_fun_Ts; @@ -1100,8 +1100,8 @@ let val ctr_Tsss' = map repair_nullary_single_ctr ctr_Tsss; val g_absTs = map range_type fun_Ts; - val g_Tsss = map repair_nullary_single_ctr (map5 dest_absumprodT absTs repTs ns mss g_absTs); - val g_Tssss = map3 (fn C => map2 (map2 (map (curry (op -->) C) oo unzip_corecT))) + val g_Tsss = map repair_nullary_single_ctr (@{map 5} dest_absumprodT absTs repTs ns mss g_absTs); + val g_Tssss = @{map 3} (fn C => map2 (map2 (map (curry (op -->) C) oo unzip_corecT))) Cs ctr_Tsss' g_Tsss; val q_Tssss = map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) g_Tssss; in @@ -1139,10 +1139,10 @@ mk_If cq (build_sum_inj Inl_const (fastype_of cg, T) $ cg) (build_sum_inj Inr_const (fastype_of cg', T) $ cg'); - val pgss = map3 flat_corec_preds_predsss_gettersss pss qssss gssss; + val pgss = @{map 3} flat_corec_preds_predsss_gettersss pss qssss gssss; val cqssss = map2 (map o map o map o rapp) cs qssss; val cgssss = map2 (map o map o map o rapp) cs gssss; - val cqgsss = map3 (map3 (map3 build_dtor_corec_arg)) g_Tsss cqssss cgssss; + val cqgsss = @{map 3} (@{map 3} (@{map 3} build_dtor_corec_arg)) g_Tsss cqssss cgssss; in ((x, cs, cpss, (((pgss, pss, qssss, gssss), cqgsss), corec_types)), lthy) end; @@ -1200,7 +1200,7 @@ in define_co_rec_as Least_FP Cs fpT (mk_binding recN) (fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_rec, - map4 (fn ctor_rec_absT => fn rep => fn fs => fn xsss => + @{map 4} (fn ctor_rec_absT => fn rep => fn fs => fn xsss => mk_case_absumprod ctor_rec_absT rep fs (map (map HOLogic.mk_tuple) xsss) (map flat_rec_arg_args xsss)) ctor_rec_absTs reps fss xssss))) @@ -1213,7 +1213,7 @@ in define_co_rec_as Greatest_FP Cs fpT (mk_binding corecN) (fold_rev (fold_rev Term.lambda) pgss (Term.list_comb (dtor_corec, - map5 mk_preds_getterss_join cs cpss f_absTs abss cqgsss))) + @{map 5} mk_preds_getterss_join cs cpss f_absTs abss cqgsss))) end; fun postproc_co_induct lthy nn prop prop_conj = @@ -1256,7 +1256,7 @@ (HOLogic.mk_Trueprop (build_rel_app names_lthy (Rs @ IRs) fpA_Ts (Term.list_comb (ctrA, argAs)) (Term.list_comb (ctrB, argBs))))); in - flat (map4 (map4 mk_prem) ctrAss ctrBss ctrAsss ctrBsss) + flat (@{map 4} (@{map 4} mk_prem) ctrAss ctrBss ctrAsss ctrBsss) end; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq @@ -1354,7 +1354,7 @@ fun mk_prem (xs, raw_pprems, concl) = fold_rev Logic.all xs (Logic.list_implies (map (mk_prem_prem xs) raw_pprems, concl)); - val raw_premss = map4 (map3 o mk_raw_prem) ps ctrss ctr_Tsss ctrXs_Tsss; + val raw_premss = @{map 4} (@{map 3} o mk_raw_prem) ps ctrss ctr_Tsss ctrXs_Tsss; val goal = Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss, @@ -1402,9 +1402,9 @@ end; val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss; - val goalss = map5 (map4 o mk_goal) frecs xctrss fss xsss fxsss; + val goalss = @{map 5} (@{map 4} o mk_goal) frecs xctrss fss xsss fxsss; - val tacss = map4 (map ooo + val tacss = @{map 4} (map ooo mk_rec_tac pre_map_defs (fp_nesting_map_ident0s @ live_nesting_map_ident0s) rec_defs) ctor_rec_thms fp_abs_inverses abs_inverses ctr_defss; @@ -1441,7 +1441,7 @@ val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names); val coinduct_conclss = - map3 (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss; + @{map 3} (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss; val common_coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn)); val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1)); @@ -1506,7 +1506,7 @@ (map2 (build_rel_app lthy (Rs @ IRs) fpA_Ts) selA_ts selB_ts))]); fun mk_prem_concl n discA_ts selA_tss discB_ts selB_tss = - Library.foldr1 HOLogic.mk_conj (flat (map5 (mk_prem_ctr_concls n) + Library.foldr1 HOLogic.mk_conj (flat (@{map 5} (mk_prem_ctr_concls n) (1 upto n) discA_ts selA_tss discB_ts selB_tss)) handle List.Empty => @{term True}; @@ -1514,7 +1514,7 @@ fold_rev Logic.all [tA, tB] (Logic.mk_implies (HOLogic.mk_Trueprop (IR $ tA $ tB), HOLogic.mk_Trueprop (mk_prem_concl n discA_ts selA_tss discB_ts selB_tss))); in - map8 mk_prem IRs fpAs fpBs ns discA_tss selA_tsss discB_tss selB_tsss + @{map 8} mk_prem IRs fpAs fpBs ns discA_tss selA_tsss discB_tss selB_tsss end; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq @@ -1632,7 +1632,8 @@ fun mk_ctor_dtor_corec_thm dtor_inject dtor_ctor corec = iffD1 OF [dtor_inject, trans OF [corec, dtor_ctor RS sym]]; - val ctor_dtor_corec_thms = map3 mk_ctor_dtor_corec_thm dtor_injects dtor_ctors dtor_corec_thms; + val ctor_dtor_corec_thms = + @{map 3} mk_ctor_dtor_corec_thm dtor_injects dtor_ctors dtor_corec_thms; val nn = length pre_bnfs; @@ -1667,10 +1668,10 @@ val coinduct_thms_pairs = let - val uvrs = map3 (fn r => fn u => fn v => r $ u $ v) rs us vs; + val uvrs = @{map 3} (fn r => fn u => fn v => r $ u $ v) rs us vs; val uv_eqs = map2 (curry HOLogic.mk_eq) us vs; val strong_rs = - map4 (fn u => fn v => fn uvr => fn uv_eq => + @{map 4} (fn u => fn v => fn uvr => fn uv_eq => fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs; fun build_the_rel rs' T Xs_T = @@ -1686,10 +1687,10 @@ [] else [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc], - Library.foldr1 HOLogic.mk_conj (map3 (build_rel_app rs') usels vsels ctrXs_Ts))]); + Library.foldr1 HOLogic.mk_conj (@{map 3} (build_rel_app rs') usels vsels ctrXs_Ts))]); fun mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss = - Library.foldr1 HOLogic.mk_conj (flat (map6 (mk_prem_ctr_concls rs' n) + Library.foldr1 HOLogic.mk_conj (flat (@{map 6} (mk_prem_ctr_concls rs' n) (1 upto n) udiscs uselss vdiscs vselss ctrXs_Tss)) handle List.Empty => @{term True}; @@ -1699,11 +1700,11 @@ val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map3 (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v))) + (@{map 3} (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v))) uvrs us vs)); fun mk_goal rs' = - Logic.list_implies (map9 (mk_prem rs') uvrs us vs ns udiscss uselsss vdiscss vselsss + Logic.list_implies (@{map 9} (mk_prem rs') uvrs us vs ns udiscss uselsss vdiscss vselsss ctrXs_Tsss, concl); val goals = map mk_goal [rs, strong_rs]; @@ -1757,10 +1758,10 @@ end; val cqgsss' = map (map (map build_corec)) cqgsss; - val goalss = map8 (map4 oooo mk_goal) cs cpss gcorecs ns kss ctrss mss cqgsss'; + val goalss = @{map 8} (@{map 4} oooo mk_goal) cs cpss gcorecs ns kss ctrss mss cqgsss'; val tacss = - map4 (map ooo mk_corec_tac corec_defs live_nesting_map_ident0s) + @{map 4} (map ooo mk_corec_tac corec_defs live_nesting_map_ident0s) ctor_dtor_corec_thms pre_map_defs abs_inverses ctr_defss; fun prove goal tac = @@ -1778,13 +1779,13 @@ if n = 1 then @{const True} else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps)); - val goalss = map6 (map2 oooo mk_goal) cs cpss gcorecs ns kss discss; + val goalss = @{map 6} (map2 oooo mk_goal) cs cpss gcorecs ns kss discss; fun mk_case_split' cp = Drule.instantiate' [] [SOME (certify lthy cp)] @{thm case_split}; val case_splitss' = map (map mk_case_split') cpss; - val tacss = map3 (map oo mk_corec_disc_iff_tac) case_splitss' corec_thmss disc_thmsss; + val tacss = @{map 3} (map oo mk_corec_disc_iff_tac) case_splitss' corec_thmss disc_thmsss; fun prove goal tac = Goal.prove_sorry lthy [] [] goal (tac o #context) @@ -1815,7 +1816,7 @@ end; fun mk_corec_sel_thms corec_thmss = - map3 (map3 (map2 o mk_corec_sel_thm)) corec_thmss selsss sel_thmsss; + @{map 3} (@{map 3} (map2 o mk_corec_sel_thm)) corec_thmss selsss sel_thmsss; val corec_sel_thmsss = mk_corec_sel_thms corec_thmss; in @@ -1997,7 +1998,7 @@ (); val Bs = - map3 (fn alive => fn A as TFree (_, S) => fn B => + @{map 3} (fn alive => fn A as TFree (_, S) => fn B => if alive then resort_tfree_or_tvar S B else A) (liveness_of_fp_bnf num_As any_fp_bnf) As Bs0; @@ -2044,7 +2045,7 @@ #> not (Config.get no_defs_lthy bnf_note_all) ? Binding.conceal; val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy - |> apfst split_list o fold_map3 (fn b => fn mx => fn rhs => + |> apfst split_list o @{fold_map 3} (fn b => fn mx => fn rhs => Local_Theory.define ((b, mx), ((maybe_conceal_def_binding b, []), rhs)) #>> apsnd snd) ctr_bindings ctr_mixfixes ctr_rhss ||> `Local_Theory.restore; @@ -2103,7 +2104,7 @@ val sel_default_eqs = map (prepare_term sel_default_lthy) raw_sel_default_eqs; fun ctr_spec_of disc_b ctr0 sel_bs = ((disc_b, ctr0), sel_bs); - val ctr_specs = map3 ctr_spec_of disc_bindings ctrs0 sel_bindingss; + val ctr_specs = @{map 3} ctr_spec_of disc_bindings ctrs0 sel_bindingss; val (ctr_sugar as {case_cong, ...}, lthy') = free_constructors tacss ((((plugins, discs_sels), standard_binding), ctr_specs), @@ -2136,7 +2137,7 @@ fun wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types (wrap_one_etc, lthy) = fold_map I wrap_one_etc lthy - |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list15 o split_list) + |>> apsnd split_list o apfst (apsnd @{split_list 4} o apfst @{split_list 15} o split_list) o split_list; fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects @@ -2204,7 +2205,7 @@ end; val simp_thmss = - map6 mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss set_thmss; + @{map 6} mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss set_thmss; val common_notes = (if nn > 1 then @@ -2315,8 +2316,8 @@ |> split_list; val simp_thmss = - map6 mk_simp_thms ctr_sugars - (map3 flat_corec_thms corec_disc_thmss corec_disc_iff_thmss corec_sel_thmss) + @{map 6} mk_simp_thms ctr_sugars + (@{map 3} flat_corec_thms corec_disc_thmss corec_disc_iff_thmss corec_sel_thmss) map_thmss rel_injectss rel_distinctss set_thmss; val common_notes = diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed Oct 08 18:10:17 2014 +0200 @@ -141,7 +141,7 @@ fun mk_ctor_iff_dtor_tac ctxt cTs cctor cdtor ctor_dtor dtor_ctor = HEADGOAL (rtac iffI THEN' - EVERY' (map3 (fn cTs => fn cx => fn th => + EVERY' (@{map 3} (fn cTs => fn cx => fn th => dtac (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN' SELECT_GOAL (unfold_thms_tac ctxt [th]) THEN' atac) [rev cTs, cTs] [cdtor, cctor] [dtor_ctor, ctor_dtor])); @@ -212,7 +212,7 @@ end; fun mk_corec_disc_iff_tac case_splits' corecs discs ctxt = - EVERY (map3 (fn case_split_tac => fn corec_thm => fn disc => + EVERY (@{map 3} (fn case_split_tac => fn corec_thm => fn disc => HEADGOAL case_split_tac THEN unfold_thms_tac ctxt [corec_thm] THEN HEADGOAL (asm_simp_tac (ss_only basic_simp_thms ctxt)) THEN (if is_refl disc then all_tac else HEADGOAL (rtac disc))) @@ -277,7 +277,7 @@ fun mk_unfold_prop_tac dtor_corec_transfer corec_def = mk_unfold_corec_type_tac dtor_corec_transfer corec_def THEN - EVERY (map4 mk_unfold_type_tac type_definitions pss qssss gssss); + EVERY (@{map 4} mk_unfold_type_tac type_definitions pss qssss gssss); in HEADGOAL Goal.conjunction_tac THEN EVERY (map2 mk_unfold_prop_tac dtor_corec_transfers corec_defs) @@ -315,7 +315,7 @@ else unfold_thms_tac ctxt ctr_defs) THEN HEADGOAL (rtac ctor_induct') THEN co_induct_inst_as_projs_tac ctxt 0 THEN - EVERY (map4 (EVERY oooo map3 o + EVERY (@{map 4} (EVERY oooo @{map 3} o mk_induct_discharge_prem_tac ctxt nn n fp_abs_inverses abs_inverses set_maps) pre_set_defss mss (unflat mss (1 upto n)) kkss) end; @@ -348,7 +348,7 @@ EVERY' ([rtac allI, rtac allI, rtac impI, select_prem_tac nn (dtac meta_spec) kk, dtac meta_spec, dtac meta_mp, atac, rtac exhaust, K (co_induct_inst_as_projs_tac ctxt 0), hyp_subst_tac ctxt] @ - map4 (fn k => fn ctr_def => fn discs => fn sels => + @{map 4} (fn k => fn ctr_def => fn discs => fn sels => EVERY' ([rtac exhaust, K (co_induct_inst_as_projs_tac ctxt 1)] @ map2 (fn k' => fn discs' => if k' = k then @@ -361,7 +361,7 @@ fun mk_coinduct_tac ctxt rel_eqs' nn ns dtor_coinduct' pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss selsss = HEADGOAL (rtac dtor_coinduct' THEN' - EVERY' (map10 (mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn) + EVERY' (@{map 10} (mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn) (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss selsss)); @@ -401,7 +401,7 @@ fun mk_rel_coinduct0_tac ctxt dtor_rel_coinduct cts assms exhausts discss selss ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses nesting_rel_eqs = rtac dtor_rel_coinduct 1 THEN - EVERY (map11 (fn ct => fn assm => fn exhaust => fn discs => fn sels => fn ctor_defs => + EVERY (@{map 11} (fn ct => fn assm => fn exhaust => fn discs => fn sels => fn ctor_defs => fn dtor_ctor => fn ctor_inject => fn abs_inject => fn rel_pre_def => fn abs_inverse => (rtac exhaust THEN_ALL_NEW (rtac exhaust THEN_ALL_NEW (dtac (rotate_prems ~1 (cterm_instantiate_pos [NONE, NONE, NONE, NONE, SOME ct] @@ -420,7 +420,7 @@ fun mk_rel_induct0_tac ctxt ctor_rel_induct assms cterms exhausts ctor_defss ctor_injects rel_pre_list_defs Abs_inverses nesting_rel_eqs = - rtac ctor_rel_induct 1 THEN EVERY (map6 (fn cterm => fn exhaust => fn ctor_defs => + rtac ctor_rel_induct 1 THEN EVERY (@{map 6} (fn cterm => fn exhaust => fn ctor_defs => fn ctor_inject => fn rel_pre_list_def => fn Abs_inverse => HEADGOAL (rtac exhaust THEN_ALL_NEW (rtac exhaust THEN_ALL_NEW (rtac (cterm_instantiate_pos (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2) diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Oct 08 18:10:17 2014 +0200 @@ -125,8 +125,8 @@ val xTs = map (domain_type o fastype_of) xtors; val yTs = map (domain_type o fastype_of) xtor's; - val absAs = map3 (fn Ds => mk_abs o mk_T_of_bnf Ds allAs) Dss bnfs abss; - val absBs = map3 (fn Ds => mk_abs o mk_T_of_bnf Ds allBs) Dss bnfs abss; + val absAs = @{map 3} (fn Ds => mk_abs o mk_T_of_bnf Ds allAs) Dss bnfs abss; + val absBs = @{map 3} (fn Ds => mk_abs o mk_T_of_bnf Ds allBs) Dss bnfs abss; val fp_repAs = map2 mk_rep absATs fp_reps; val fp_repBs = map2 mk_rep absBTs fp_reps; @@ -186,7 +186,7 @@ val fp_or_nesting_rel_monos = map rel_mono_of_bnf fp_or_nesting_bnfs; val xtor_rel_co_induct = - mk_xtor_rel_co_induct_thm fp (map3 cast castAs castBs pre_rels) pre_phis rels phis xs ys + mk_xtor_rel_co_induct_thm fp (@{map 3} cast castAs castBs pre_rels) pre_phis rels phis xs ys xtors xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts rel_defs rel_monos fp_or_nesting_rel_eqs fp_or_nesting_rel_monos) lthy; @@ -268,7 +268,7 @@ val subst = Term.typ_subst_atomic fold_thetaAs; fun mk_fp_absT_repT fp_repT fp_absT = mk_absT thy fp_repT fp_absT ooo mk_repT; - val mk_fp_absT_repTs = map5 mk_fp_absT_repT fp_repTs fp_absTs absTs repTs; + val mk_fp_absT_repTs = @{map 5} mk_fp_absT_repT fp_repTs fp_absTs absTs repTs; val fold_preTs' = mk_fp_absT_repTs (map subst fold_preTs); @@ -411,7 +411,7 @@ fp_abs fp_rep abs rep rhs) end; - val goals = map8 mk_goals recs xtors rec_strs pre_rec_maps fp_abss fp_reps abss reps; + val goals = @{map 8} mk_goals recs xtors rec_strs pre_rec_maps fp_abss fp_reps abss reps; val pre_map_defs = no_refl (map map_def_of_bnf bnfs); val fp_pre_map_defs = no_refl (map map_def_of_bnf pre_bnfs); diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Oct 08 18:10:17 2014 +0200 @@ -205,7 +205,7 @@ | freeze_fpTs_call _ _ _ T = T; val ctr_Tsss = map (map binder_types) ctr_Tss; - val ctrXs_Tsss = map4 (map2 o map2 oo freeze_fpTs_call) kks fpTs callssss ctr_Tsss; + val ctrXs_Tsss = @{map 4} (map2 o map2 oo freeze_fpTs_call) kks fpTs callssss ctr_Tsss; val ctrXs_repTs = map mk_sumprodT_balanced ctrXs_Tsss; val ns = map length ctr_Tsss; @@ -261,7 +261,7 @@ fun mk_binding b pre = Binding.prefix_name (pre ^ "_") b; val ((co_recs, co_rec_defs), lthy) = - fold_map2 (fn b => + @{fold_map 2} (fn b => if fp = Least_FP then define_rec (the recs_args_types) (mk_binding b) fpTs Cs reps else define_corec (the corecs_args_types) (mk_binding b) fpTs Cs abss) fp_bs xtor_co_recs lthy @@ -340,9 +340,9 @@ |> morph_fp_sugar phi; val target_fp_sugars = - map16 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars - co_recs co_rec_defs mapss (transpose co_inductss') co_rec_thmss co_rec_disc_thmss - co_rec_sel_thmsss fp_sugars0; + @{map 16} mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss + ctr_sugars co_recs co_rec_defs mapss (transpose co_inductss') co_rec_thmss + co_rec_disc_thmss co_rec_sel_thmsss fp_sugars0; val n2m_sugar = (target_fp_sugars, fp_sugar_thms); in diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML Wed Oct 08 18:10:17 2014 +0200 @@ -32,7 +32,7 @@ val folded_C_IHs = map (fn thm => thm RS @{thm spec2} RS mp) raw_C_IHs; val C_IHs = map2 (curry op |>) folded_C_IHs unfolds; val C_IH_monos = - map3 (fn C_IH => fn mono => fn unfold => + @{map 3} (fn C_IH => fn mono => fn unfold => (mono RSN (2, @{thm vimage2p_mono}), C_IH) |> fp = Greatest_FP ? swap |> op RS diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Oct 08 18:10:17 2014 +0200 @@ -433,7 +433,7 @@ if xs = [x] then f else HOLogic.tupled_lambda x (Term.list_comb (f, xs)); fun mk_case_absumprod absT rep fs xss xss' = - HOLogic.mk_comp (mk_case_sumN_balanced (map3 mk_tupled_fun fs (map mk_tuple_balanced xss) xss'), + HOLogic.mk_comp (mk_case_sumN_balanced (@{map 3} mk_tupled_fun fs (map mk_tuple_balanced xss) xss'), mk_rep absT rep); fun If_const T = Const (@{const_name If}, HOLogic.boolT --> T --> T --> T); @@ -512,7 +512,7 @@ fun mk_prem pre_relphi phi x y xtor xtor' = HOLogic.mk_Trueprop (list_all_free [x, y] (flip (curry HOLogic.mk_imp) (pre_relphi $ (dtor xtor x) $ (dtor xtor' y)) (phi $ (ctor xtor x) $ (ctor xtor' y)))); - val prems = map6 mk_prem pre_relphis pre_phis xs ys xtors xtor's; + val prems = @{map 6} mk_prem pre_relphis pre_phis xs ys xtors xtor's; val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (flip mk_leq) relphis pre_phis)); @@ -531,7 +531,7 @@ val arg_rels = map2 (flip mk_rel_fun) pre_relphis pre_ophis; fun mk_transfer relphi pre_phi un_fold un_fold' = fold_rev mk_rel_fun arg_rels (flip mk_rel_fun relphi pre_phi) $ un_fold $ un_fold'; - val transfers = map4 mk_transfer relphis pre_ophis un_folds un_folds'; + val transfers = @{map 4} mk_transfer relphis pre_ophis un_folds un_folds'; val goal = fold_rev Logic.all (phis @ pre_ophis) (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj transfers)); @@ -565,7 +565,7 @@ val rewrite1s = mk_rewrites map_cong1s; val rewrite2s = mk_rewrites map_cong2s; val unique_prems = - map4 (fn xtor_map => fn un_fold => fn rewrite1 => fn rewrite2 => + @{map 4} (fn xtor_map => fn un_fold => fn rewrite1 => fn rewrite2 => mk_trans (rewrite_comp_comp2 OF [xtor_map, un_fold]) (mk_trans rewrite1 (mk_sym rewrite2))) xtor_maps xtor_un_folds rewrite1s rewrite2s; @@ -613,7 +613,8 @@ val ((bnfs, (deadss, livess)), accum) = apfst (apsnd split_list o split_list) - (fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) flatten_tyargs Xs Ds0) bs rhsXs + (@{fold_map 2} + (fn b => bnf_of_typ Smart_Inline (raw_qualify b) flatten_tyargs Xs Ds0) bs rhsXs ((empty_comp_cache, empty_unfolds), lthy)); fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1)))) @@ -631,13 +632,13 @@ val ((kill_poss, _), (bnfs', ((_, unfold_set'), lthy'))) = normalize_bnfs norm_qualify Ass Ds (K (resBs' @ Xs)) bnfs accum; - val Dss = map3 (uncurry append oo curry swap oo map o nth) livess kill_poss deadss; + val Dss = @{map 3} (uncurry append oo curry swap oo map o nth) livess kill_poss deadss; fun pre_qualify b = Binding.qualify false (Binding.name_of b) #> not (Config.get lthy' bnf_note_all) ? Binding.conceal; val ((pre_bnfs, (deadss, absT_infos)), lthy'') = - fold_map4 (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b)) + @{fold_map 4} (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b)) bs (not (null live_phantoms) :: replicate (nn - 1) false) Dss bnfs' lthy' |>> split_list |>> apsnd split_list; diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Wed Oct 08 18:10:17 2014 +0200 @@ -138,21 +138,21 @@ val sum_sTs = map2 (fn T => fn U => T --> U) activeAs sumFTs; (* terms *) - val mapsAsAs = map4 mk_map_of_bnf Dss Ass Ass bnfs; - val mapsAsBs = map4 mk_map_of_bnf Dss Ass Bss bnfs; - val mapsBsCs' = map4 mk_map_of_bnf Dss Bss Css' bnfs; - val mapsAsCs' = map4 mk_map_of_bnf Dss Ass Css' bnfs; - val map_Inls = map4 mk_map_of_bnf Dss Bss (replicate n (passiveAs @ sumBsAs)) bnfs; - val map_Inls_rev = map4 mk_map_of_bnf Dss (replicate n (passiveAs @ sumBsAs)) Bss bnfs; - val map_fsts = map4 mk_map_of_bnf Dss (replicate n (passiveAs @ RTs)) Ass bnfs; - val map_snds = map4 mk_map_of_bnf Dss (replicate n (passiveAs @ RTs)) Bss bnfs; - fun mk_setss Ts = map3 mk_sets_of_bnf (map (replicate live) Dss) + val mapsAsAs = @{map 4} mk_map_of_bnf Dss Ass Ass bnfs; + val mapsAsBs = @{map 4} mk_map_of_bnf Dss Ass Bss bnfs; + val mapsBsCs' = @{map 4} mk_map_of_bnf Dss Bss Css' bnfs; + val mapsAsCs' = @{map 4} mk_map_of_bnf Dss Ass Css' bnfs; + val map_Inls = @{map 4} mk_map_of_bnf Dss Bss (replicate n (passiveAs @ sumBsAs)) bnfs; + val map_Inls_rev = @{map 4} mk_map_of_bnf Dss (replicate n (passiveAs @ sumBsAs)) Bss bnfs; + val map_fsts = @{map 4} mk_map_of_bnf Dss (replicate n (passiveAs @ RTs)) Ass bnfs; + val map_snds = @{map 4} mk_map_of_bnf Dss (replicate n (passiveAs @ RTs)) Bss bnfs; + fun mk_setss Ts = @{map 3} mk_sets_of_bnf (map (replicate live) Dss) (map (replicate live) (replicate n Ts)) bnfs; val setssAs = mk_setss allAs; val setssAs' = transpose setssAs; val bis_setss = mk_setss (passiveAs @ RTs); - val relsAsBs = map4 mk_rel_of_bnf Dss Ass Bss bnfs; - val bds = map3 mk_bd_of_bnf Dss Ass bnfs; + val relsAsBs = @{map 4} mk_rel_of_bnf Dss Ass Bss bnfs; + val bds = @{map 3} mk_bd_of_bnf Dss Ass bnfs; val sum_bd = Library.foldr1 (uncurry mk_csum) bds; val sum_bdT = fst (dest_relT (fastype_of sum_bd)); val (sum_bdT_params, sum_bdT_params') = `(map TFree) (Term.add_tfreesT sum_bdT []); @@ -244,7 +244,7 @@ |> singleton (Proof_Context.export names_lthy lthy) end; - val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps; + val map_comp_id_thms = @{map 5} mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps; (*forall a : set(m+1) x. f(m+1) a = a; ...; forall a : set(m+n) x. f(m+n) a = a ==> map id ... id f(m+1) ... f(m+n) x = x*) @@ -253,7 +253,7 @@ fun mk_prem set f z z' = HOLogic.mk_Trueprop (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z)))); - val prems = map4 mk_prem (drop m sets) self_fs zs zs'; + val prems = @{map 4} mk_prem (drop m sets) self_fs zs zs'; val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x); in Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal)) @@ -262,7 +262,7 @@ |> singleton (Proof_Context.export names_lthy lthy) end; - val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids; + val map_cong0L_thms = @{map 5} mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids; val in_mono'_thms = map (fn thm => (thm OF (replicate m subset_refl)) RS @{thm set_mp}) in_monos; @@ -271,7 +271,8 @@ val prems = map2 (curry mk_Trueprop_eq) yFs yFs_copy; val maps = map (fn mapx => Term.list_comb (mapx, all_gs)) mapsBsCs'; val concls = - map3 (fn x => fn y => fn mapx => mk_Trueprop_eq (mapx $ x, mapx $ y)) yFs yFs_copy maps; + @{map 3} (fn x => fn y => fn mapx => mk_Trueprop_eq (mapx $ x, mapx $ y)) + yFs yFs_copy maps; val goals = map2 (fn prem => fn concl => Logic.mk_implies (prem, concl)) prems concls; in map (fn goal => @@ -290,11 +291,11 @@ (*forall i = 1 ... n: (\x \ Bi. si \ Fi_in UNIV .. UNIV B1 ... Bn)*) val coalg_spec = let - val ins = map3 mk_in (replicate n (passive_UNIVs @ Bs)) setssAs FTsAs; + val ins = @{map 3} mk_in (replicate n (passive_UNIVs @ Bs)) setssAs FTsAs; fun mk_coalg_conjunct B s X z z' = mk_Ball B (Term.absfree z' (HOLogic.mk_mem (s $ z, X))); - val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_coalg_conjunct Bs ss ins zs zs') + val rhs = Library.foldr1 HOLogic.mk_conj (@{map 5} mk_coalg_conjunct Bs ss ins zs zs') in fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss) rhs end; @@ -328,7 +329,7 @@ fun mk_prem x B = mk_Trueprop_mem (x, B); fun mk_concl s x B set = HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) B); val prems = map2 mk_prem zs Bs; - val conclss = map3 (fn s => fn x => fn sets => map2 (mk_concl s x) Bs (drop m sets)) + val conclss = @{map 3} (fn s => fn x => fn sets => map2 (mk_concl s x) Bs (drop m sets)) ss zs setssAs; val goalss = map2 (fn prem => fn concls => map (fn concl => Logic.list_implies (coalg_prem :: [prem], concl)) concls) prems conclss; @@ -371,8 +372,8 @@ mk_Ball B (Term.absfree z' (HOLogic.mk_eq (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ z]), s' $ (f $ z)))); val rhs = HOLogic.mk_conj - (Library.foldr1 HOLogic.mk_conj (map5 mk_fbetw fs Bs B's zs zs'), - Library.foldr1 HOLogic.mk_conj (map7 mk_mor Bs mapsAsBs fs ss s's zs zs')) + (Library.foldr1 HOLogic.mk_conj (@{map 5} mk_fbetw fs Bs B's zs zs'), + Library.foldr1 HOLogic.mk_conj (@{map 7} mk_mor Bs mapsAsBs fs ss s's zs zs')) in fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ fs) rhs end; @@ -402,11 +403,11 @@ val prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs); fun mk_image_goal f B1 B2 = Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_leq (mk_image f $ B1) B2)); - val image_goals = map3 mk_image_goal fs Bs B's; + val image_goals = @{map 3} mk_image_goal fs Bs B's; fun mk_elim_goal B mapAsBs f s s' x = Logic.list_implies ([prem, mk_Trueprop_mem (x, B)], mk_Trueprop_eq (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ x]), s' $ (f $ x))); - val elim_goals = map6 mk_elim_goal Bs mapsAsBs fs ss s's zs; + val elim_goals = @{map 6} mk_elim_goal Bs mapsAsBs fs ss s's zs; fun prove goal = Goal.prove_sorry lthy [] [] goal (K (mk_mor_elim_tac mor_def)) |> Thm.close_derivation @@ -462,7 +463,7 @@ (HOLogic.mk_comp (Term.list_comb (mapAsBs, passive_ids @ fs), s), HOLogic.mk_comp (s', f)); val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs; - val rhs = Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct mapsAsBs fs ss s's); + val rhs = Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct mapsAsBs fs ss s's); in Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (lhs, rhs)) (K (mk_mor_UNIV_tac morE_thms mor_def)) @@ -484,7 +485,7 @@ val mor_case_sum_thm = let - val maps = map3 (fn s => fn sum_s => fn mapx => + val maps = @{map 3} (fn s => fn sum_s => fn mapx => mk_case_sum (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ Inls), s), sum_s)) s's sum_ss map_Inls; in @@ -503,7 +504,7 @@ val bis_def_bind = (Thm.def_binding bis_bind, []); fun mk_bis_le_conjunct R B1 B2 = mk_leq R (mk_Times (B1, B2)); - val bis_le = Library.foldr1 HOLogic.mk_conj (map3 mk_bis_le_conjunct Rs Bs B's) + val bis_le = Library.foldr1 HOLogic.mk_conj (@{map 3} mk_bis_le_conjunct Rs Bs B's) val bis_spec = let @@ -519,7 +520,7 @@ val rhs = HOLogic.mk_conj (bis_le, Library.foldr1 HOLogic.mk_conj - (map9 mk_bis Rs ss s's zs z's RFs map_fsts map_snds bis_setss)) + (@{map 9} mk_bis Rs ss s's zs z's RFs map_fsts map_snds bis_setss)) in fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ Rs) rhs end; @@ -563,7 +564,7 @@ val rhs = HOLogic.mk_conj (bis_le, Library.foldr1 HOLogic.mk_conj - (map6 mk_conjunct Rs ss s's zs z's relsAsBs)) + (@{map 6} mk_conjunct Rs ss s's zs z's relsAsBs)) in Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (mk_bis Bs ss B's s's Rs, rhs)) (K (mk_bis_rel_tac m bis_def in_rels map_comps map_cong0s set_mapss)) @@ -684,7 +685,7 @@ fun mk_concl i R = HOLogic.mk_Trueprop (mk_leq R (mk_lsbis Bs ss i)); val goals = map2 (fn i => fn R => Logic.mk_implies (sbis_prem, mk_concl i R)) ks sRs; in - map3 (fn goal => fn i => fn def => + @{map 3} (fn goal => fn i => fn def => Goal.prove_sorry lthy [] [] goal (K (mk_incl_lsbis_tac n i def)) |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy)) goals ks lsbis_defs @@ -695,7 +696,7 @@ fun mk_concl i B = HOLogic.mk_Trueprop (mk_equiv B (mk_lsbis Bs ss i)); val goals = map2 (fn i => fn B => Logic.mk_implies (coalg_prem, mk_concl i B)) ks Bs; in - map3 (fn goal => fn l_incl => fn incl_l => + @{map 3} (fn goal => fn l_incl => fn incl_l => Goal.prove_sorry lthy [] [] goal (K (mk_equiv_lsbis_tac sbis_lsbis_thm l_incl incl_l bis_Id_on_thm bis_converse_thm bis_O_thm)) @@ -755,7 +756,7 @@ fun mk_set_sbd i bd_Card_order bds = map (fn thm => @{thm ordLeq_ordIso_trans} OF [bd_Card_order RS mk_ordLeq_csum n i thm, sbd_ordIso]) bds; - val set_sbdss = map3 mk_set_sbd ks bd_Card_orders set_bdss; + val set_sbdss = @{map 3} mk_set_sbd ks bd_Card_orders set_bdss; in (lthy, sbd, sbdT, sbd_card_order, sbd_Cinfinite, sbd_Card_order, set_sbdss) end; @@ -765,7 +766,7 @@ val sum_sbd_listT = HOLogic.listT sum_sbdT; val sum_sbd_list_setT = HOLogic.mk_setT sum_sbd_listT; val bdTs = passiveAs @ replicate n sbdT; - val to_sbd_maps = map4 mk_map_of_bnf Dss Ass (replicate n bdTs) bnfs; + val to_sbd_maps = @{map 4} mk_map_of_bnf Dss Ass (replicate n bdTs) bnfs; val bdFTs = mk_FTs bdTs; val sbdFT = mk_sumTN bdFTs; val treeT = HOLogic.mk_prodT (sum_sbd_list_setT, sum_sbd_listT --> sbdFT); @@ -773,15 +774,15 @@ val treeTs = passiveAs @ replicate n treeT; val treeQTs = passiveAs @ replicate n treeQT; val treeFTs = mk_FTs treeTs; - val tree_maps = map4 mk_map_of_bnf Dss (replicate n bdTs) (replicate n treeTs) bnfs; - val final_maps = map4 mk_map_of_bnf Dss (replicate n treeTs) (replicate n treeQTs) bnfs; + val tree_maps = @{map 4} mk_map_of_bnf Dss (replicate n bdTs) (replicate n treeTs) bnfs; + val final_maps = @{map 4} mk_map_of_bnf Dss (replicate n treeTs) (replicate n treeQTs) bnfs; val isNode_setss = mk_setss (passiveAs @ replicate n sbdT); val root = HOLogic.mk_set sum_sbd_listT [HOLogic.mk_list sum_sbdT []]; val Zero = HOLogic.mk_tuple (map (fn U => absdummy U root) activeAs); val Lev_recT = fastype_of Zero; - val Nil = HOLogic.mk_tuple (map3 (fn i => fn z => fn z'=> + val Nil = HOLogic.mk_tuple (@{map 3} (fn i => fn z => fn z'=> Term.absfree z' (mk_InN activeAs z i)) ks zs zs'); val rv_recT = fastype_of Nil; @@ -812,7 +813,7 @@ val isNodeT = Library.foldr (op -->) (map fastype_of [Kl, lab, kl], HOLogic.boolT); - val Succs = map3 (fn i => fn k => fn k' => + val Succs = @{map 3} (fn i => fn k => fn k' => HOLogic.mk_Collect (fst k', snd k', HOLogic.mk_mem (mk_InN sbdTs k i, mk_Succ Kl kl))) ks kks kks'; @@ -828,7 +829,7 @@ val ((isNode_frees, (_, isNode_def_frees)), (lthy, lthy_old)) = lthy - |> fold_map3 (fn i => fn x => fn sets => Local_Theory.define + |> @{fold_map 3} (fn i => fn x => fn sets => Local_Theory.define ((isNode_bind i, NoSyn), (isNode_def_bind i, isNode_spec sets x i))) ks xs isNode_setss |>> apsnd split_list o split_list @@ -848,7 +849,7 @@ val empty = HOLogic.mk_mem (HOLogic.mk_list sum_sbdT [], Kl); val tree = mk_Ball Kl (Term.absfree kl' - (Library.foldr1 HOLogic.mk_conj (map4 (fn Succ => fn i => fn k => fn k' => + (Library.foldr1 HOLogic.mk_conj (@{map 4} (fn Succ => fn i => fn k => fn k' => mk_Ball Succ (Term.absfree k' (mk_isNode (mk_append (kl, HOLogic.mk_list sum_sbdT [mk_InN sbdTs k i])) i))) Succs ks kks kks'))); @@ -889,7 +890,7 @@ let val in_k = mk_InN sbdTs k i; in Term.absfree k' (HOLogic.mk_prod (mk_Shift Kl in_k, mk_shift lab in_k)) end; - val f = Term.list_comb (mapFT, passive_ids @ map3 mk_f ks kks kks'); + val f = Term.list_comb (mapFT, passive_ids @ @{map 3} mk_f ks kks kks'); val (fTs1, fTs2) = apsnd tl (chop (i - 1) (map (fn T => T --> FT) bdFTs)); val fs = map mk_undefined fTs1 @ (f :: map mk_undefined fTs2); in @@ -899,7 +900,7 @@ val ((strT_frees, (_, strT_def_frees)), (lthy, lthy_old)) = lthy - |> fold_map3 (fn i => fn mapFT => fn FT => Local_Theory.define + |> @{fold_map 3} (fn i => fn mapFT => fn FT => Local_Theory.define ((strT_bind i, NoSyn), (strT_def_bind i, strT_spec mapFT FT i))) ks tree_maps treeFTs |>> apsnd split_list o split_list @@ -955,11 +956,11 @@ (HOLogic.mk_conj (Cons, HOLogic.mk_conj (b_set, kl_rec)))) end; in - Term.absfree a' (Library.foldl1 mk_union (map3 mk_set ks sets zs_copy)) + Term.absfree a' (Library.foldl1 mk_union (@{map 3} mk_set ks sets zs_copy)) end; val Suc = Term.absdummy HOLogic.natT (Term.absfree Lev_rec' - (HOLogic.mk_tuple (map5 mk_Suc ks ss setssAs zs zs'))); + (HOLogic.mk_tuple (@{map 5} mk_Suc ks ss setssAs zs zs'))); val rhs = mk_rec_nat Zero Suc; in @@ -1002,7 +1003,7 @@ end; val Cons = Term.absfree sumx' (Term.absdummy sum_sbd_listT (Term.absfree rv_rec' - (HOLogic.mk_tuple (map4 mk_Cons ks ss zs zs')))); + (HOLogic.mk_tuple (@{map 4} mk_Cons ks ss zs zs')))); val rhs = mk_rec_list Nil Cons; in @@ -1043,7 +1044,7 @@ (Term.list_comb (to_sbd_map, passive_ids @ map (mk_to_sbd s k i) ks) $ (s $ k)) i); val Lab = Term.absfree kl' - (mk_case_sumN (map5 mk_case ks to_sbd_maps ss zs zs') $ (mk_rv ss kl i $ z)); + (mk_case_sumN (@{map 5} mk_case ks to_sbd_maps ss zs zs') $ (mk_rv ss kl i $ z)); val rhs = HOLogic.mk_prod (mk_UNION (HOLogic.mk_UNIV HOLogic.natT) (Term.absfree nat' (mk_Lev ss nat i $ z)), Lab); @@ -1053,7 +1054,7 @@ val ((beh_frees, (_, beh_def_frees)), (lthy, lthy_old)) = lthy - |> fold_map2 (fn i => fn z => + |> @{fold_map 2} (fn i => fn z => Local_Theory.define ((beh_bind i, NoSyn), (beh_def_bind i, beh_spec i z))) ks zs |>> apsnd split_list o split_list ||> `Local_Theory.restore; @@ -1141,11 +1142,12 @@ mk_Lev ss (HOLogic.mk_Suc nat) i $ z)); in HOLogic.mk_imp (HOLogic.mk_eq (mk_rv ss kl i $ z, mk_InN activeAs z' i'), - (Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct'' ks (drop m sets) zs_copy2))) + (Library.foldr1 HOLogic.mk_conj + (@{map 3} mk_conjunct'' ks (drop m sets) zs_copy2))) end; in HOLogic.mk_imp (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z), - Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct' ks setssAs ss zs_copy)) + Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct' ks setssAs ss zs_copy)) end; val goal = list_all_free (kl :: zs @ zs_copy @ zs_copy2) @@ -1180,7 +1182,7 @@ HOLogic.mk_imp (HOLogic.mk_mem (mk_append (kl, HOLogic.mk_list sum_sbdT [mk_InN sbdTs k i']), mk_Lev ss (HOLogic.mk_Suc nat) i $ z), - (Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct'' ks sets ss zs_copy))) + (Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct'' ks sets ss zs_copy))) end; in HOLogic.mk_imp (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z), @@ -1238,9 +1240,9 @@ HOLogic.mk_Trueprop (mk_congruent R (HOLogic.mk_comp (Term.list_comb (final_map, passive_ids @ map mk_proj lsbisAs), strT))); - val goals = map3 mk_goal lsbisAs final_maps strTAs; + val goals = @{map 3} mk_goal lsbisAs final_maps strTAs; in - map4 (fn goal => fn lsbisE => fn map_comp_id => fn map_cong0 => + @{map 4} (fn goal => fn lsbisE => fn map_comp_id => fn map_cong0 => Goal.prove_sorry lthy [] [] goal (K (mk_congruent_str_final_tac m lsbisE map_comp_id map_cong0 equiv_LSBIS_thms)) |> Thm.close_derivation) @@ -1265,7 +1267,7 @@ val ((T_names, (T_glob_infos, T_loc_infos)), lthy) = lthy - |> fold_map4 (fn b => fn mx => fn car_final => fn in_car_final => + |> @{fold_map 4} (fn b => fn mx => fn car_final => fn in_car_final => typedef (b, params, mx) car_final NONE (EVERY' [rtac exI, rtac in_car_final] 1)) bs mixfixes car_finals in_car_final_thms |>> apsnd split_list o split_list; @@ -1323,7 +1325,7 @@ val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) = lthy - |> fold_map6 (fn i => fn rep => fn str => fn mapx => fn Jz => fn Jz' => + |> @{fold_map 6} (fn i => fn rep => fn str => fn mapx => fn Jz => fn Jz' => Local_Theory.define ((dtor_bind i, NoSyn), (dtor_def_bind i, dtor_spec rep str mapx Jz Jz'))) ks Rep_Ts str_finals map_FTs Jzs Jzs' @@ -1368,7 +1370,7 @@ val ((unfold_frees, (_, unfold_def_frees)), (lthy, lthy_old)) = lthy - |> fold_map4 (fn i => fn abs => fn f => fn z => + |> @{fold_map 4} (fn i => fn abs => fn f => fn z => Local_Theory.define ((unfold_bind i, NoSyn), (unfold_def_bind i, unfold_spec abs f z))) ks Abs_Ts (map (fn i => HOLogic.mk_comp (mk_proj (nth lsbisAs (i - 1)), mk_beh ss i)) ks) zs @@ -1379,7 +1381,7 @@ val unfolds = map (Morphism.term phi) unfold_frees; val unfold_names = map (fst o dest_Const) unfolds; fun mk_unfolds passives actives = - map3 (fn name => fn T => fn active => + @{map 3} (fn name => fn T => fn active => Const (name, Library.foldr (op -->) (map2 (curry op -->) actives (mk_FTs (passives @ actives)), active --> T))) unfold_names (mk_Ts passives) actives; @@ -1478,9 +1480,9 @@ let fun mk_goal dtor ctor FT = mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT); - val goals = map3 mk_goal dtors ctors FTs; + val goals = @{map 3} mk_goal dtors ctors FTs; in - map5 (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_cong0L => + @{map 5} (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_cong0L => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => mk_dtor_o_ctor_tac ctxt ctor_def unfold map_comp_id map_cong0L unfold_o_dtor_thms) @@ -1521,7 +1523,7 @@ val corec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o corec_bind; val corec_strs = - map3 (fn dtor => fn sum_s => fn mapx => + @{map 3} (fn dtor => fn sum_s => fn mapx => mk_case_sum (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ corec_Inls), dtor), sum_s)) dtors corec_ss corec_maps; @@ -1532,7 +1534,7 @@ val ((corec_frees, (_, corec_def_frees)), (lthy, lthy_old)) = lthy - |> fold_map3 (fn i => fn T => fn AT => + |> @{fold_map 3} (fn i => fn T => fn AT => Local_Theory.define ((corec_bind i, NoSyn), (corec_def_bind i, corec_spec i T AT))) ks Ts activeAs |>> apsnd split_list o split_list @@ -1544,7 +1546,7 @@ fun mk_corecs Ts passives actives = let val Tactives = map2 (curry mk_sumT) Ts actives; in - map3 (fn name => fn T => fn active => + @{map 3} (fn name => fn T => fn active => Const (name, Library.foldr (op -->) (map2 (curry op -->) actives (mk_FTs (passives @ Tactives)), active --> T))) corec_names Ts actives @@ -1565,9 +1567,9 @@ in mk_Trueprop_eq (lhs, rhs) end; - val goals = map5 mk_goal ks corec_ss corec_maps_rev dtors zs; + val goals = @{map 5} mk_goal ks corec_ss corec_maps_rev dtors zs; in - map3 (fn goal => fn unfold => fn map_cong0 => + @{map 3} (fn goal => fn unfold => fn map_cong0 => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => mk_corec_tac ctxt m corec_defs unfold map_cong0 corec_Inl_sum_thms) @@ -1611,7 +1613,7 @@ fun mk_concl phi z1 z2 = HOLogic.mk_imp (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2)); val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map3 mk_concl phis Jzs1 Jzs2)); + (@{map 3} mk_concl phis Jzs1 Jzs2)); fun mk_rel_prem phi dtor rel Jz Jz_copy = let @@ -1622,7 +1624,7 @@ (list_all_free [Jz, Jz_copy] (HOLogic.mk_imp (phi $ Jz $ Jz_copy, concl))) end; - val rel_prems = map5 mk_rel_prem phis dtors rels Jzs Jzs_copy; + val rel_prems = @{map 5} mk_rel_prem phis dtors rels Jzs Jzs_copy; val dtor_coinduct_goal = Logic.list_implies (rel_prems, concl); val dtor_coinduct = @@ -1720,14 +1722,14 @@ end; val Suc = Term.absdummy HOLogic.natT (Term.absfree hrec' - (HOLogic.mk_tuple (map4 mk_Suc dtors FTs_setss Jzs Jzs'))); + (HOLogic.mk_tuple (@{map 4} mk_Suc dtors FTs_setss Jzs Jzs'))); in mk_rec_nat Zero Suc end; val ((col_frees, (_, col_def_frees)), (lthy, lthy_old)) = lthy - |> fold_map4 (fn j => fn Zero => fn hrec => fn hrec' => Local_Theory.define + |> @{fold_map 4} (fn j => fn Zero => fn hrec => fn hrec' => Local_Theory.define ((col_bind j, NoSyn), (col_def_bind j, col_spec j Zero hrec hrec'))) ls Zeros hrecs hrecs' |>> apsnd split_list o split_list @@ -1758,7 +1760,7 @@ val setss = map (fn i => map2 (mk_set Ts i) ls passiveAs) ks; val (Jbnf_consts, lthy) = - fold_map7 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn T => + @{fold_map 7} (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn T => fn lthy => define_bnf_consts Hardly_Inline (user_policy Note_Some lthy) false (SOME deads) map_b rel_b set_bs @@ -1766,10 +1768,10 @@ [Const (@{const_name undefined}, T)]), NONE) lthy) bs map_bs rel_bs set_bss fs_maps setss Ts lthy; - val (_, Jconsts, Jconst_defs, mk_Jconsts) = split_list4 Jbnf_consts; - val (_, Jsetss, Jbds_Ds, _, _) = split_list5 Jconsts; - val (Jmap_defs, Jset_defss, Jbd_defs, _, Jrel_defs) = split_list5 Jconst_defs; - val (mk_Jmaps_Ds, mk_Jt_Ds, _, mk_Jrels_Ds, _) = split_list5 mk_Jconsts; + val (_, Jconsts, Jconst_defs, mk_Jconsts) = @{split_list 4} Jbnf_consts; + val (_, Jsetss, Jbds_Ds, _, _) = @{split_list 5} Jconsts; + val (Jmap_defs, Jset_defss, Jbd_defs, _, Jrel_defs) = @{split_list 5} Jconst_defs; + val (mk_Jmaps_Ds, mk_Jt_Ds, _, mk_Jrels_Ds, _) = @{split_list 5} mk_Jconsts; val Jrel_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Jrel_defs; val Jset_defs = flat Jset_defss; @@ -1793,9 +1795,9 @@ let fun mk_goal fs_Jmap map dtor dtor' = mk_Trueprop_eq (HOLogic.mk_comp (dtor', fs_Jmap), HOLogic.mk_comp (Term.list_comb (map, fs @ fs_Jmaps), dtor)); - val goals = map4 mk_goal fs_Jmaps map_FTFT's dtors dtor's; + val goals = @{map 4} mk_goal fs_Jmaps map_FTFT's dtors dtor's; val maps = - map5 (fn goal => fn unfold => fn map_comp => fn map_cong0 => fn map_arg_cong => + @{map 5} (fn goal => fn unfold => fn map_comp => fn map_cong0 => fn map_arg_cong => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN mk_map_tac m n map_arg_cong unfold map_comp map_cong0) @@ -1811,7 +1813,7 @@ fun mk_prem u map dtor dtor' = mk_Trueprop_eq (HOLogic.mk_comp (dtor', u), HOLogic.mk_comp (Term.list_comb (map, fs @ us), dtor)); - val prems = map4 mk_prem us map_FTFT's dtors dtor's; + val prems = @{map 4} mk_prem us map_FTFT's dtors dtor's; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) us fs_Jmaps)); @@ -1826,7 +1828,7 @@ val Jmap_comp0_thms = let val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map3 (fn fmap => fn gmap => fn fgmap => + (@{map 3} (fn fmap => fn gmap => fn fgmap => HOLogic.mk_eq (HOLogic.mk_comp (gmap, fmap), fgmap)) fs_Jmaps gs_Jmaps fgs_Jmaps)) in @@ -1849,17 +1851,17 @@ HOLogic.mk_Trueprop (mk_leq (K2 $ x2) (K1 $ x1)))); val premss = map2 (fn j => fn Ks => - map4 mk_passive_prem (map (fn xs => nth xs (j - 1)) FTs_setss) dtors Jzs Ks @ - flat (map4 (fn sets => fn s => fn x1 => fn K1 => - map3 (mk_active_prem s x1 K1) (drop m sets) Jzs_copy Ks) FTs_setss dtors Jzs Ks)) + @{map 4} mk_passive_prem (map (fn xs => nth xs (j - 1)) FTs_setss) dtors Jzs Ks @ + flat (@{map 4} (fn sets => fn s => fn x1 => fn K1 => + @{map 3} (mk_active_prem s x1 K1) (drop m sets) Jzs_copy Ks) FTs_setss dtors Jzs Ks)) ls Kss; val col_minimal_thms = let fun mk_conjunct j T i K x = mk_leq (mk_col Ts nat i j T $ x) (K $ x); fun mk_concl j T Ks = list_all_free Jzs - (Library.foldr1 HOLogic.mk_conj (map3 (mk_conjunct j T) ks Ks Jzs)); - val concls = map3 mk_concl ls passiveAs Kss; + (Library.foldr1 HOLogic.mk_conj (@{map 3} (mk_conjunct j T) ks Ks Jzs)); + val concls = @{map 3} mk_concl ls passiveAs Kss; val goals = map2 (fn prems => fn concl => Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) premss concls @@ -1867,7 +1869,7 @@ val ctss = map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) concls; in - map4 (fn goal => fn cts => fn col_0s => fn col_Sucs => + @{map 4} (fn goal => fn cts => fn col_0s => fn col_Sucs => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => mk_col_minimal_tac ctxt m cts col_0s col_Sucs) @@ -1877,7 +1879,7 @@ end; fun mk_conjunct set K x = mk_leq (set $ x) (K $ x); - fun mk_concl sets Ks = Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct sets Ks Jzs); + fun mk_concl sets Ks = Library.foldr1 HOLogic.mk_conj (@{map 3} mk_conjunct sets Ks Jzs); val concls = map2 mk_concl Jsetss_by_range Kss; val goals = map2 (fn prems => fn concl => @@ -1902,14 +1904,14 @@ HOLogic.mk_Trueprop (mk_leq (Jset1 $ x) (Jset2 $ y))); val set_incl_Jset_goalss = - map4 (fn dtor => fn x => fn sets => fn Jsets => + @{map 4} (fn dtor => fn x => fn sets => fn Jsets => map2 (mk_set_incl_Jset dtor x) (take m sets) Jsets) dtors Jzs FTs_setss Jsetss_by_bnf; (*x(k) : F(i)set(m+k) (dtor(i) y(i)) ==> J(k)set(j) x(k) <= J(i)set(j) y(i)*) val set_Jset_incl_Jset_goalsss = - map4 (fn dtori => fn yi => fn sets => fn Jsetsi => - map3 (fn xk => fn set => fn Jsetsk => + @{map 4} (fn dtori => fn yi => fn sets => fn Jsetsi => + @{map 3} (fn xk => fn set => fn Jsetsk => map2 (mk_set_Jset_incl_Jset dtori xk yi set) Jsetsk Jsetsi) Jzs_copy (drop m sets) Jsetss_by_bnf) dtors Jzs FTs_setss Jsetss_by_bnf; @@ -1952,12 +1954,12 @@ val cTs = map (SOME o certifyT lthy) params'; fun mk_induct_tinst phis jsets y y' = - map4 (fn phi => fn jset => fn Jz => fn Jz' => + @{map 4} (fn phi => fn jset => fn Jz => fn Jz' => SOME (certify lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y', HOLogic.mk_conj (HOLogic.mk_mem (y, jset $ Jz), phi $ y $ Jz)))))) phis jsets Jzs Jzs'; in - map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis => + @{map 6} (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis => ((set_minimal |> Drule.instantiate' cTs (mk_induct_tinst phis jsets y y') |> unfold_thms lthy incls) OF @@ -1976,7 +1978,7 @@ (map2 (fn X => mk_UNION (X $ (dtor $ z))) act_sets sets))); fun mk_goals eq = map2 (fn i => fn sets => - map4 (fn Fsets => + @{map 4} (fn Fsets => mk_simp_goal eq (nth Fsets (i - 1)) (drop m Fsets) sets) FTs_setss dtors Jzs sets) ls Jsetss_by_range; @@ -1984,7 +1986,7 @@ val le_goals = map (HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj) (mk_goals (uncurry mk_leq)); val set_le_thmss = map split_conj_thm - (map4 (fn goal => fn Jset_minimal => fn set_Jsets => fn set_Jset_Jsetss => + (@{map 4} (fn goal => fn Jset_minimal => fn set_Jsets => fn set_Jset_Jsetss => Goal.prove_sorry lthy [] [] goal (K (mk_set_le_tac n Jset_minimal set_Jsets set_Jset_Jsetss)) |> Thm.close_derivation @@ -1993,7 +1995,7 @@ val ge_goalss = map (map HOLogic.mk_Trueprop) (mk_goals (uncurry mk_leq o swap)); val set_ge_thmss = - map3 (map3 (fn goal => fn set_incl_Jset => fn set_Jset_incl_Jsets => + @{map 3} (@{map 3} (fn goal => fn set_incl_Jset => fn set_Jset_incl_Jsets => Goal.prove_sorry lthy [] [] goal (K (mk_set_ge_tac n set_incl_Jset set_Jset_incl_Jsets)) |> Thm.close_derivation @@ -2017,15 +2019,15 @@ HOLogic.mk_eq (mk_image f $ (col $ z), col' $ (map $ z)); fun mk_goal f cols cols' = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj - (map4 (mk_col_natural f) fs_Jmaps Jzs cols cols')); + (@{map 4} (mk_col_natural f) fs_Jmaps Jzs cols cols')); - val goals = map3 mk_goal fs colss colss'; + val goals = @{map 3} mk_goal fs colss colss'; val ctss = map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) goals; val thms = - map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs => + @{map 4} (fn goal => fn cts => fn rec_0s => fn rec_Sucs => Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) (fn {context = ctxt, prems = _} => mk_col_natural_tac ctxt cts rec_0s rec_Sucs dtor_Jmap_thms set_mapss) @@ -2041,7 +2043,7 @@ fun mk_col_bd z col bd = mk_ordLeq (mk_card_of (col $ z)) bd; fun mk_goal bds cols = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj - (map3 mk_col_bd Jzs cols bds)); + (@{map 3} mk_col_bd Jzs cols bds)); val goals = map (mk_goal Jbds) colss; @@ -2049,7 +2051,7 @@ (map (mk_goal (replicate n sbd)) colss); val thms = - map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs => + @{map 5} (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs => Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jbd_defs THEN mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss) @@ -2069,7 +2071,7 @@ mk_Ball (set $ z) (Term.absfree y' (HOLogic.mk_eq (f $ y, g $ y))); fun mk_prems sets z = - Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys') + Library.foldr1 HOLogic.mk_conj (@{map 5} (mk_prem z) sets fs fs_copy ys ys') fun mk_map_cong0 sets z fmap gmap = HOLogic.mk_imp (mk_prems sets z, HOLogic.mk_eq (fmap $ z, gmap $ z)); @@ -2086,14 +2088,14 @@ |> Term.absfree y' |> certify lthy; - val cphis = map9 mk_cphi + val cphis = @{map 9} mk_cphi Jsetss_by_bnf Jzs' Jzs fs_Jmaps fs_copy_Jmaps Jys' Jys Jys'_copy Jys_copy; val coinduct = Drule.instantiate' cTs (map SOME cphis) dtor_coinduct_thm; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map4 mk_map_cong0 Jsetss_by_bnf Jzs fs_Jmaps fs_copy_Jmaps)); + (@{map 4} mk_map_cong0 Jsetss_by_bnf Jzs fs_Jmaps fs_copy_Jmaps)); val thm = Goal.prove_sorry lthy [] [] goal @@ -2120,9 +2122,9 @@ let fun mk_goal Jz Jz' dtor dtor' Jrelphi relphi = mk_Trueprop_eq (Jrelphi $ Jz $ Jz', relphi $ (dtor $ Jz) $ (dtor' $ Jz')); - val goals = map6 mk_goal Jzs Jz's dtors dtor's Jrelphis relphis; + val goals = @{map 6} mk_goal Jzs Jz's dtors dtor's Jrelphis relphis; in - map12 (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 => + @{map 12} (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 => fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor => fn set_map0s => fn dtor_set_incls => fn dtor_set_set_inclss => Goal.prove_sorry lthy [] [] goal @@ -2139,7 +2141,7 @@ val zip_ranTs = passiveABs @ prodTsTs'; val allJphis = Jphis @ activeJphis; val zipFTs = mk_FTs zip_ranTs; - val zipTs = map3 (fn T => fn T' => fn FT => T --> T' --> FT) Ts Ts' zipFTs; + val zipTs = @{map 3} (fn T => fn T' => fn FT => T --> T' --> FT) Ts Ts' zipFTs; val zip_zTs = mk_Ts passiveABs; val (((zips, (abs, abs')), (zip_zs, zip_zs')), names_lthy) = names_lthy |> mk_Frees "zip" zipTs @@ -2176,17 +2178,17 @@ HOLogic.mk_conj (HOLogic.mk_eq (map $ zipxy, dtor $ x), HOLogic.mk_eq (map' $ zipxy, dtor' $ y)))))) end; - val helper_prems = map9 mk_helper_prem + val helper_prems = @{map 9} mk_helper_prem activeJphis in_phis zips Jzs Jz's map_all_fsts map_all_snds dtors dtor's; fun mk_helper_coind_phi fst phi x alt y map zip_unfold = list_exists_free [if fst then y else x] (HOLogic.mk_conj (phi $ x $ y, HOLogic.mk_eq (alt, map $ (zip_unfold $ HOLogic.mk_prod (x, y))))) - val coind1_phis = map6 (mk_helper_coind_phi true) + val coind1_phis = @{map 6} (mk_helper_coind_phi true) activeJphis Jzs Jzs_copy Jz's Jmap_fsts zip_unfolds; - val coind2_phis = map6 (mk_helper_coind_phi false) + val coind2_phis = @{map 6} (mk_helper_coind_phi false) activeJphis Jzs Jz's_copy Jz's Jmap_snds zip_unfolds; fun mk_cts zs z's phis = - map3 (fn z => fn z' => fn phi => + @{map 3} (fn z => fn z' => fn phi => SOME (certify lthy (fold_rev (Term.absfree o Term.dest_Free) [z', z] phi))) zs z's phis @ map (SOME o certify lthy) (splice z's zs); @@ -2197,10 +2199,10 @@ HOLogic.mk_imp (coind_phi, HOLogic.mk_eq (alt, z)); val helper_coind1_concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map3 mk_helper_coind_concl Jzs Jzs_copy coind1_phis)); + (@{map 3} mk_helper_coind_concl Jzs Jzs_copy coind1_phis)); val helper_coind2_concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map3 mk_helper_coind_concl Jz's Jz's_copy coind2_phis)); + (@{map 3} mk_helper_coind_concl Jz's Jz's_copy coind2_phis)); fun mk_helper_coind_thms fst concl cts = Goal.prove_sorry lthy [] [] (Logic.list_implies (helper_prems, concl)) @@ -2220,8 +2222,8 @@ HOLogic.mk_eq (z, zip_unfold $ HOLogic.mk_prod (x, y))), phi $ (fst $ ab) $ (snd $ ab))); val helper_ind_phiss = - map4 (fn Jphi => fn ab => fn fst => fn snd => - map5 (mk_helper_ind_phi Jphi ab fst snd) + @{map 4} (fn Jphi => fn ab => fn fst => fn snd => + @{map 5} (mk_helper_ind_phi Jphi ab fst snd) zip_zs activeJphis Jzs Jz's zip_unfolds) Jphis abs fstABs sndABs; val ctss = map2 (fn ab' => fn phis => @@ -2234,13 +2236,13 @@ mk_Ball (set $ z) (Term.absfree ab' ind_phi); val mk_helper_ind_concls = - map3 (fn ab' => fn ind_phis => fn zip_sets => - map3 (mk_helper_ind_concl ab') zip_zs ind_phis zip_sets) + @{map 3} (fn ab' => fn ind_phis => fn zip_sets => + @{map 3} (mk_helper_ind_concl ab') zip_zs ind_phis zip_sets) abs' helper_ind_phiss zip_setss |> map (HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj); val helper_ind_thmss = if m = 0 then replicate n [] else - map4 (fn concl => fn j => fn set_induct => fn cts => + @{map 4} (fn concl => fn j => fn set_induct => fn cts => Goal.prove_sorry lthy [] [] (Logic.list_implies (helper_prems, concl)) (fn {context = ctxt, prems = _} => mk_rel_coinduct_ind_tac ctxt m ks dtor_unfold_thms set_mapss j (cterm_instantiate_pos cts set_induct)) @@ -2262,7 +2264,7 @@ let fun mk_le_Jrel_OO Jrelpsi1 Jrelpsi2 Jrelpsi12 = mk_leq (mk_rel_compp (Jrelpsi1, Jrelpsi2)) Jrelpsi12; - val goals = map3 mk_le_Jrel_OO Jrelpsi1s Jrelpsi2s Jrelpsi12s; + val goals = @{map 3} mk_le_Jrel_OO Jrelpsi1s Jrelpsi2s Jrelpsi12s; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals); in @@ -2380,9 +2382,9 @@ else @{term True})); in HOLogic.mk_Trueprop - (Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct sets Jzs dummys wits)) + (Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct sets Jzs dummys wits)) end; - val goals = map5 mk_goal Jsetss_by_range ys ys_copy ys'_copy ls; + val goals = @{map 5} mk_goal Jsetss_by_range ys ys_copy ys'_copy ls; in map2 (fn goal => fn induct => Goal.prove_sorry lthy [] [] goal @@ -2432,14 +2434,14 @@ val rel_OO_Grp_tacs = map (fn def => K (rtac def 1)) Jrel_unabs_defs; - val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss + val tacss = @{map 9} zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs; fun wit_tac thms ctxt = mk_wit_tac ctxt n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms; val (Jbnfs, lthy) = - fold_map6 (fn tacs => fn map_b => fn rel_b => fn set_bs => fn wit_thms => + @{fold_map 6} (fn tacs => fn map_b => fn rel_b => fn set_bs => fn wit_thms => fn consts => bnf_def Hardly_Inline (user_policy Note_Some) false I tacs (wit_tac wit_thms) (SOME deads) map_b rel_b set_bs consts) diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Oct 08 18:10:17 2014 +0200 @@ -289,7 +289,7 @@ val Type (_, dom_Ts) = domain_type (fastype_of1 (bound_Ts, t)); val map' = mk_map (length fs) dom_Ts Us map0; val fs' = - map_flattened_map_args ctxt s (map3 (massage_map_or_map_arg bound_Ts) Us Ts) fs; + map_flattened_map_args ctxt s (@{map 3} (massage_map_or_map_arg bound_Ts) Us Ts) fs; in Term.list_comb (map', fs') end @@ -325,7 +325,7 @@ val f'_T = typof f'; val arg_Ts = map typof args; in - Term.list_comb (f', map3 (massage_call bound_Ts) (binder_types f'_T) arg_Ts args) + Term.list_comb (f', @{map 3} (massage_call bound_Ts) (binder_types f'_T) arg_Ts args) end | NONE => (case t of @@ -394,7 +394,7 @@ fun mk_spec ctr disc sels = {ctr = substA ctr, disc = substA disc, sels = map substA sels}; in - map3 mk_spec ctrs discs selss + @{map 3} mk_spec ctrs discs selss handle ListPair.UnequalLengths => not_codatatype ctxt res_T end) | _ => not_codatatype ctxt res_T); @@ -452,7 +452,7 @@ val (perm_f_hssss, _) = indexedddd perm_f_Tssss h'; val fun_arg_hs = - flat (map3 flat_corec_preds_predsss_gettersss perm_p_hss perm_q_hssss perm_f_hssss); + flat (@{map 3} flat_corec_preds_predsss_gettersss perm_p_hss perm_q_hssss perm_f_hssss); fun unpermute0 perm0_xs = permute_like_unique (op =) perm0_kks kks perm0_xs; fun unpermute perm_xs = permute_like_unique (op =) perm_indices indices perm_xs; @@ -486,7 +486,7 @@ corec_thm corec_disc corec_sels = let val nullary = not (can dest_funT (fastype_of ctr)) in {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_io, - calls = map3 (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms, + calls = @{map 3} (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms, distinct_discss = distinct_discss, collapse = collapse, corec_thm = corec_thm, corec_disc = corec_disc, corec_sels = corec_sels} end; @@ -494,7 +494,7 @@ fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, distinct_discsss, collapses, ...} : ctr_sugar) p_is q_isss f_isss f_Tsss corec_thms corec_discs corec_selss = let val p_ios = map SOME p_is @ [NONE] in - map14 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss + @{map 14} mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss distinct_discsss collapses corec_thms corec_discs corec_selss end; @@ -509,7 +509,7 @@ ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms corec_discs corec_selss}; in - (map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts, + (@{map 5} mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts, co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms, co_induct_of coinduct_thmss, strong_co_induct_of coinduct_thmss, coinduct_attrs_pair, is_some gfp_sugar_thms, lthy) @@ -738,7 +738,7 @@ val sequentials = replicate (length fun_names) false; in - fold_map2 (dissect_coeqn_ctr lthy fun_names sequentials basic_ctr_specss eqn_pos eqn0 + @{fold_map 2} (dissect_coeqn_ctr lthy fun_names sequentials basic_ctr_specss eqn_pos eqn0 (SOME (abstract (List.rev fun_args) rhs))) ctr_premss ctr_concls matchedsss end; @@ -909,7 +909,7 @@ |> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss |> map2 currys arg_Tss |> Syntax.check_terms lthy - |> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t))) + |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t))) bs mxs |> rpair excludess' end; @@ -981,7 +981,7 @@ val frees = map (fst #>> Binding.name_of #> Free) fixes; val has_call = exists_subterm (member (op =) frees); val eqns_data = - fold_map2 (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss) + @{fold_map 2} (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss) (tag_list 0 (map snd specs)) of_specs_opt [] |> flat o fst; @@ -1030,7 +1030,7 @@ |> map (flat o snd); val arg_Tss = map (binder_types o snd o fst) fixes; - val disc_eqnss = map6 mk_actual_disc_eqns bs arg_Tss exhaustives corec_specs sel_eqnss + val disc_eqnss = @{map 6} mk_actual_disc_eqns bs arg_Tss exhaustives corec_specs sel_eqnss disc_eqnss'; val (defs, excludess') = build_codefs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss; @@ -1045,7 +1045,7 @@ else tac_opt; - val excludess'' = map3 (fn tac_opt => fn sequential => map (fn (j, goal) => + val excludess'' = @{map 3} (fn tac_opt => fn sequential => map (fn (j, goal) => (j, (Option.map (Goal.prove_sorry lthy [] [] goal #> Thm.close_derivation) (exclude_tac tac_opt sequential j), goal)))) tac_opts sequentials excludess'; @@ -1072,7 +1072,7 @@ de_facto_exhaustives disc_eqnss |> list_all_fun_args [] val nchotomy_taut_thmss = - map5 (fn tac_opt => fn {exhaust_discs = res_exhaust_discs, ...} => + @{map 5} (fn tac_opt => fn {exhaust_discs = res_exhaust_discs, ...} => fn {code_rhs_opt, ...} :: _ => fn [] => K [] | [goal] => fn true => let @@ -1121,7 +1121,7 @@ end) de_facto_exhaustives disc_eqnss |> list_all_fun_args ps - |> map3 (fn disc_eqns as {fun_args, ...} :: _ => fn [] => K [] + |> @{map 3} (fn disc_eqns as {fun_args, ...} :: _ => fn [] => K [] | [nchotomy_thm] => fn [goal] => [mk_primcorec_exhaust_tac lthy ("" (* for "P" *) :: map (fst o dest_Free) fun_args) (length disc_eqns) nchotomy_thm @@ -1334,9 +1334,9 @@ end) end; - val disc_alistss = map3 (map oo prove_disc) corec_specs excludessss disc_eqnss; + val disc_alistss = @{map 3} (map oo prove_disc) corec_specs excludessss disc_eqnss; val disc_alists = map (map snd o flat) disc_alistss; - val sel_alists = map4 (map ooo prove_sel) corec_specs disc_eqnss excludessss sel_eqnss; + val sel_alists = @{map 4} (map ooo prove_sel) corec_specs disc_eqnss excludessss sel_eqnss; val disc_thmss = map (map snd o sort_list_duplicates o flat) disc_alistss; val disc_thmsss' = map (map (map (snd o snd))) disc_alistss; val sel_thmss = map (map (fst o snd) o sort_list_duplicates) sel_alists; @@ -1364,17 +1364,18 @@ |> single end; - val disc_iff_thmss = map6 (flat ooo map2 oooo prove_disc_iff) corec_specs exhaust_thmss + val disc_iff_thmss = @{map 6} (flat ooo map2 oooo prove_disc_iff) corec_specs exhaust_thmss disc_thmsss' disc_eqnss disc_thmsss' disc_eqnss |> map sort_list_duplicates; - val ctr_alists = map6 (fn disc_alist => maps oooo prove_ctr disc_alist) disc_alists + val ctr_alists = @{map 6} (fn disc_alist => maps oooo prove_ctr disc_alist) disc_alists (map (map snd) sel_alists) corec_specs disc_eqnss sel_eqnss ctr_specss; val ctr_thmss' = map (map snd) ctr_alists; val ctr_thmss = map (map snd o order_list) ctr_alists; - val code_thmss = map6 prove_code exhaustives disc_eqnss sel_eqnss nchotomy_thmss ctr_thmss' - ctr_specss; + val code_thmss = + @{map 6} prove_code exhaustives disc_eqnss sel_eqnss nchotomy_thmss ctr_thmss' + ctr_specss; val disc_iff_or_disc_thmss = map2 (fn [] => I | disc_iffs => K disc_iffs) disc_iff_thmss disc_thmss; diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/BNF/bnf_gfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Wed Oct 08 18:10:17 2014 +0200 @@ -608,7 +608,7 @@ else (rtac (sum_case_cong_weak RS trans) THEN' rtac (mk_sum_caseN n i) THEN' rtac (mk_sum_caseN n i RS trans)), rtac (map_comp_id RS trans), rtac (map_cong0 OF replicate m refl), - EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd => + EVERY' (@{map 3} (fn i' => fn to_sbd_inj => fn from_to_sbd => DETERM o EVERY' [rtac trans, rtac o_apply, rtac prod_injectI, rtac conjI, rtac trans, rtac @{thm Shift_def}, rtac equalityI, rtac subsetI, etac thin_rl, @@ -783,7 +783,7 @@ EVERY' [rtac Jset_minimal, REPEAT_DETERM_N n o rtac @{thm Un_upper1}, REPEAT_DETERM_N n o - EVERY' (map3 (fn i => fn set_Jset => fn set_Jset_Jsets => + EVERY' (@{map 3} (fn i => fn set_Jset => fn set_Jset_Jsets => EVERY' [rtac subsetI, rtac @{thm UnI2}, rtac (mk_UnIN n i), etac @{thm UN_I}, etac UnE, etac set_Jset, REPEAT_DETERM_N (n - 1) o etac UnE, EVERY' (map (fn thm => EVERY' [etac @{thm UN_E}, etac thm, atac]) set_Jset_Jsets)]) @@ -1018,7 +1018,7 @@ val snd_diag_nth = if fst then @{thm snd_diag_fst} else @{thm snd_diag_snd}; in EVERY' [rtac coinduct, - EVERY' (map8 (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_map0s => + EVERY' (@{map 8} (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_map0s => fn dtor_unfold => fn dtor_map => fn in_rel => EVERY' [REPEAT_DETERM o resolve_tac [allI, impI, in_rel RS iffD2], REPEAT_DETERM o eresolve_tac [exE, conjE], @@ -1050,7 +1050,7 @@ let val n = length ks; in rtac set_induct 1 THEN - EVERY' (map3 (fn unfold => fn set_map0s => fn i => + EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i => EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], etac conjE, select_prem_tac n (dtac @{thm spec2}) i, dtac mp, atac, REPEAT_DETERM o eresolve_tac [CollectE, conjE, Collect_splitD_set_mp, set_rev_mp], @@ -1058,7 +1058,7 @@ SELECT_GOAL (unfold_thms_tac ctxt ([unfold, nth set_map0s (j - 1)] @ split_id_unfolds)), rtac subset_refl]) unfolds set_map0ss ks) 1 THEN - EVERY' (map3 (fn unfold => fn set_map0s => fn i => + EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i => EVERY' (map (fn set_map0 => EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], etac conjE, select_prem_tac n (dtac @{thm spec2}) i, dtac mp, atac, diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Wed Oct 08 18:10:17 2014 +0200 @@ -100,18 +100,18 @@ val prod_sTs = map2 (curry op -->) prodFTs activeAs; (* terms *) - val mapsAsAs = map4 mk_map_of_bnf Dss Ass Ass bnfs; - val mapsAsBs = map4 mk_map_of_bnf Dss Ass Bss bnfs; - val mapsBsCs' = map4 mk_map_of_bnf Dss Bss Css' bnfs; - val mapsAsCs' = map4 mk_map_of_bnf Dss Ass Css' bnfs; - val map_fsts = map4 mk_map_of_bnf Dss (replicate n (passiveAs @ prodBsAs)) Bss bnfs; - val map_fsts_rev = map4 mk_map_of_bnf Dss Bss (replicate n (passiveAs @ prodBsAs)) bnfs; - fun mk_setss Ts = map3 mk_sets_of_bnf (map (replicate live) Dss) + val mapsAsAs = @{map 4} mk_map_of_bnf Dss Ass Ass bnfs; + val mapsAsBs = @{map 4} mk_map_of_bnf Dss Ass Bss bnfs; + val mapsBsCs' = @{map 4} mk_map_of_bnf Dss Bss Css' bnfs; + val mapsAsCs' = @{map 4} mk_map_of_bnf Dss Ass Css' bnfs; + val map_fsts = @{map 4} mk_map_of_bnf Dss (replicate n (passiveAs @ prodBsAs)) Bss bnfs; + val map_fsts_rev = @{map 4} mk_map_of_bnf Dss Bss (replicate n (passiveAs @ prodBsAs)) bnfs; + fun mk_setss Ts = @{map 3} mk_sets_of_bnf (map (replicate live) Dss) (map (replicate live) (replicate n Ts)) bnfs; val setssAs = mk_setss allAs; - val bd0s = map3 mk_bd_of_bnf Dss Ass bnfs; + val bd0s = @{map 3} mk_bd_of_bnf Dss Ass bnfs; val bds = - map3 (fn bd0 => fn Ds => fn bnf => mk_csum bd0 + @{map 3} (fn bd0 => fn Ds => fn bnf => mk_csum bd0 (mk_card_of (HOLogic.mk_UNIV (mk_T_of_bnf Ds (replicate live (fst (dest_relT (fastype_of bd0)))) bnf)))) bd0s Dss bnfs; @@ -209,7 +209,7 @@ |> singleton (Proof_Context.export names_lthy lthy) end; - val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps; + val map_comp_id_thms = @{map 5} mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps; (*forall a : set(m+1) x. f(m+1) a = a; ...; forall a : set(m+n) x. f(m+n) a = a ==> map id ... id f(m+1) ... f(m+n) x = x*) @@ -217,7 +217,7 @@ let fun mk_prem set f z z' = HOLogic.mk_Trueprop (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z)))); - val prems = map4 mk_prem (drop m sets) self_fs zs zs'; + val prems = @{map 4} mk_prem (drop m sets) self_fs zs zs'; val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x); in Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal)) @@ -226,7 +226,7 @@ |> singleton (Proof_Context.export names_lthy lthy) end; - val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids; + val map_cong0L_thms = @{map 5} mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids; val in_mono'_thms = map (fn bnf => in_mono_of_bnf bnf OF (replicate m subset_refl)) bnfs; val in_cong'_thms = map (fn bnf => in_cong_of_bnf bnf OF (replicate m refl)) bnfs; @@ -240,11 +240,11 @@ (*forall i = 1 ... n: (\x \ Fi_in UNIV .. UNIV B1 ... Bn. si x \ Bi)*) val alg_spec = let - val ins = map3 mk_in (replicate n (passive_UNIVs @ Bs)) setssAs FTsAs; + val ins = @{map 3} mk_in (replicate n (passive_UNIVs @ Bs)) setssAs FTsAs; fun mk_alg_conjunct B s X x x' = mk_Ball X (Term.absfree x' (HOLogic.mk_mem (s $ x, B))); - val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_alg_conjunct Bs ss ins xFs xFs') + val rhs = Library.foldr1 HOLogic.mk_conj (@{map 5} mk_alg_conjunct Bs ss ins xFs xFs') in fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss) rhs end; @@ -273,7 +273,7 @@ fun mk_prem x set B = HOLogic.mk_Trueprop (mk_leq (set $ x) B); fun mk_concl s x B = mk_Trueprop_mem (s $ x, B); val premss = map2 ((fn x => fn sets => map2 (mk_prem x) (drop m sets) Bs)) xFs setssAs; - val concls = map3 mk_concl ss xFs Bs; + val concls = @{map 3} mk_concl ss xFs Bs; val goals = map2 (fn prems => fn concl => Logic.list_implies (alg_prem :: prems, concl)) premss concls; in @@ -321,9 +321,9 @@ (Term.absfree x' (HOLogic.mk_eq (f $ (s $ x), s' $ (Term.list_comb (mapAsBs, passive_ids @ fs) $ x)))); val rhs = HOLogic.mk_conj - (Library.foldr1 HOLogic.mk_conj (map5 mk_fbetw fs Bs B's zs zs'), + (Library.foldr1 HOLogic.mk_conj (@{map 5} mk_fbetw fs Bs B's zs zs'), Library.foldr1 HOLogic.mk_conj - (map8 mk_mor setssAs mapsAsBs fs ss s's FTsAs xFs xFs')) + (@{map 8} mk_mor setssAs mapsAsBs fs ss s's FTsAs xFs xFs')) in fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ fs) rhs end; @@ -354,7 +354,7 @@ fun mk_elim_goal sets mapAsBs f s s' x T = Logic.list_implies ([prem, mk_elim_prem sets x T], mk_Trueprop_eq (f $ (s $ x), s' $ Term.list_comb (mapAsBs, passive_ids @ fs @ [x]))); - val elim_goals = map7 mk_elim_goal setssAs mapsAsBs fs ss s's xFs FTsAs; + val elim_goals = @{map 7} mk_elim_goal setssAs mapsAsBs fs ss s's xFs FTsAs; fun prove goal = Goal.prove_sorry lthy [] [] goal (K (mk_mor_elim_tac mor_def)) |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy); @@ -414,7 +414,7 @@ val mor_convol_thm = let - val maps = map3 (fn s => fn prod_s => fn mapx => + val maps = @{map 3} (fn s => fn prod_s => fn mapx => mk_convol (HOLogic.mk_comp (s, Term.list_comb (mapx, passive_ids @ fsts)), prod_s)) s's prod_ss map_fsts; in @@ -432,7 +432,7 @@ (HOLogic.mk_comp (f, s), HOLogic.mk_comp (s', Term.list_comb (mapAsBs, passive_ids @ fs))); val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs; - val rhs = Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct mapsAsBs fs ss s's); + val rhs = Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct mapsAsBs fs ss s's); in Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (lhs, rhs)) (K (mk_mor_UNIV_tac m morE_thms mor_def)) @@ -490,13 +490,13 @@ fun mk_set_sbd i bd_Card_order bds = map (fn thm => @{thm ordLeq_ordIso_trans} OF [bd_Card_order RS mk_ordLeq_csum n i thm, sbd_ordIso]) bds; - val set_sbdss = map3 mk_set_sbd ks bd_Card_orders set_bdss; + val set_sbdss = @{map 3} mk_set_sbd ks bd_Card_orders set_bdss; fun mk_in_bd_sum i Co Cnz bd = Cnz RS ((@{thm ordLeq_ordIso_trans} OF [Co RS mk_ordLeq_csum n i (Co RS @{thm ordLeq_refl}), sbd_ordIso]) RS (bd RS @{thm ordLeq_transitive[OF _ cexp_mono2_Cnotzero[OF _ Card_order_csum]]})); - val in_sbds = map4 mk_in_bd_sum ks bd_Card_orders bd_Cnotzeros in_bds; + val in_sbds = @{map 4} mk_in_bd_sum ks bd_Card_orders bd_Cnotzeros in_bds; in (lthy, sbd, sbd_Cinfinite, sbd_Card_order, set_sbdss, in_sbds) end; @@ -573,7 +573,7 @@ Library.foldr1 HOLogic.mk_prodT (map HOLogic.mk_setT BTs)); in mk_worec suc_bd (Term.absfree Asi' (Term.absfree idx' (HOLogic.mk_tuple - (map4 (mk_minH_component Asi idx) (mk_setss Ts) (mk_FTs Ts) ss ks)))) + (@{map 4} (mk_minH_component Asi idx) (mk_setss Ts) (mk_FTs Ts) ss ks)))) end; val (min_algs_thms, min_algs_mono_thms, card_of_min_algs_thm, least_min_algs_thm) = @@ -585,7 +585,7 @@ val concl = HOLogic.mk_Trueprop (HOLogic.mk_eq (min_algs $ idx, HOLogic.mk_tuple - (map4 (mk_minH_component min_algs idx) setssAs FTsAs ss ks))); + (@{map 4} (mk_minH_component min_algs idx) setssAs FTsAs ss ks))); val goal = Logic.mk_implies (HOLogic.mk_Trueprop i_field, concl); val min_algs_thm = Goal.prove_sorry lthy [] [] goal @@ -696,7 +696,7 @@ |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy); - val leasts = map3 mk_least_thm min_algs Bs min_alg_defs; + val leasts = @{map 3} mk_least_thm min_algs Bs min_alg_defs; val incl_prem = HOLogic.mk_Trueprop (mk_alg Bs ss); val incl = Goal.prove_sorry lthy [] [] @@ -811,7 +811,7 @@ mk_mor car_inits str_inits Bs ss init_fs_copy]; fun mk_fun_eq f g x = HOLogic.mk_eq (f $ x, g $ x); val unique = HOLogic.mk_Trueprop - (Library.foldr1 HOLogic.mk_conj (map3 mk_fun_eq init_fs init_fs_copy init_xs)); + (Library.foldr1 HOLogic.mk_conj (@{map 3} mk_fun_eq init_fs init_fs_copy init_xs)); val cts = map (certify lthy) ss; val unique_mor = Goal.prove_sorry lthy [] [] (Logic.list_implies (prems @ mor_prems, unique)) @@ -839,7 +839,7 @@ end; in Library.foldr1 HOLogic.mk_conj - (map6 mk_conjunct phis str_inits active_init_setss init_ins init_xFs init_xFs') + (@{map 6} mk_conjunct phis str_inits active_init_setss init_ins init_xFs init_xFs') end; val init_induct_thm = @@ -858,7 +858,7 @@ val ((T_names, (T_glob_infos, T_loc_infos)), lthy) = lthy - |> fold_map3 (fn b => fn mx => fn car_init => + |> @{fold_map 3} (fn b => fn mx => fn car_init => typedef (b, params, mx) car_init NONE (EVERY' [rtac iffD2, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms, rtac alg_init_thm] 1)) bs mixfixes car_inits @@ -918,7 +918,7 @@ val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) = lthy - |> fold_map4 (fn i => fn abs => fn str => fn mapx => + |> @{fold_map 4} (fn i => fn abs => fn str => fn mapx => Local_Theory.define ((ctor_bind i, NoSyn), (ctor_def_bind i, ctor_spec abs str mapx))) ks Abs_Ts str_inits map_FT_inits @@ -945,7 +945,7 @@ |> Thm.close_derivation; fun mk_ct initFT str abs = Term.absdummy initFT (abs $ (str $ Bound 0)) - val cts = map3 (certify lthy ooo mk_ct) init_FTs str_inits Abs_Ts; + val cts = @{map 3} (certify lthy ooo mk_ct) init_FTs str_inits Abs_Ts; val mor_Abs = Goal.prove_sorry lthy [] [] @@ -979,7 +979,7 @@ val folds = map (Morphism.term phi) fold_frees; val fold_names = map (fst o dest_Const) folds; fun mk_folds passives actives = - map3 (fn name => fn T => fn active => + @{map 3} (fn name => fn T => fn active => Const (name, Library.foldr (op -->) (map2 (curry op -->) (mk_FTs (passives @ actives)) actives, T --> active))) fold_names (mk_Ts passives) actives; @@ -993,7 +993,7 @@ val copy_thm = let val prems = HOLogic.mk_Trueprop (mk_alg Bs ss) :: - map3 (HOLogic.mk_Trueprop ooo mk_bij_betw) inv_fs B's Bs; + @{map 3} (HOLogic.mk_Trueprop ooo mk_bij_betw) inv_fs B's Bs; val concl = HOLogic.mk_Trueprop (list_exists_free s's (HOLogic.mk_conj (mk_alg B's s's, mk_mor B's s's Bs ss inv_fs))); in @@ -1094,9 +1094,9 @@ let fun mk_goal dtor ctor FT = mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT); - val goals = map3 mk_goal dtors ctors FTs; + val goals = @{map 3} mk_goal dtors ctors FTs; in - map5 (fn goal => fn dtor_def => fn foldx => fn map_comp_id => fn map_cong0L => + @{map 5} (fn goal => fn dtor_def => fn foldx => fn map_comp_id => fn map_cong0L => Goal.prove_sorry lthy [] [] goal (K (mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_cong0L ctor_o_fold_thms)) |> Thm.close_derivation) @@ -1136,7 +1136,7 @@ val rec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o rec_bind; val rec_strs = - map3 (fn ctor => fn prod_s => fn mapx => + @{map 3} (fn ctor => fn prod_s => fn mapx => mk_convol (HOLogic.mk_comp (ctor, Term.list_comb (mapx, passive_ids @ rec_fsts)), prod_s)) ctors rec_ss rec_maps; @@ -1146,7 +1146,7 @@ val ((rec_frees, (_, rec_def_frees)), (lthy, lthy_old)) = lthy - |> fold_map3 (fn i => fn T => fn AT => + |> @{fold_map 3} (fn i => fn T => fn AT => Local_Theory.define ((rec_bind i, NoSyn), (rec_def_bind i, rec_spec i T AT))) ks Ts activeAs |>> apsnd split_list o split_list ||> `Local_Theory.restore; @@ -1157,7 +1157,7 @@ fun mk_recs Ts passives actives = let val Tactives = map2 (curry HOLogic.mk_prodT) Ts actives; in - map3 (fn name => fn T => fn active => + @{map 3} (fn name => fn T => fn active => Const (name, Library.foldr (op -->) (map2 (curry op -->) (mk_FTs (passives @ Tactives)) actives, T --> active))) rec_names Ts actives @@ -1177,7 +1177,7 @@ in mk_Trueprop_eq (lhs, rhs) end; - val goals = map5 mk_goal ks rec_ss rec_maps_rev ctors xFs; + val goals = @{map 5} mk_goal ks rec_ss rec_maps_rev ctors xFs; in map2 (fn goal => fn foldx => Goal.prove_sorry lthy [] [] goal @@ -1221,13 +1221,13 @@ Logic.all z (Logic.mk_implies (prem, concl)) end; - val IHs = map3 mk_IH phis (drop m sets) Izs; + val IHs = @{map 3} mk_IH phis (drop m sets) Izs; val concl = HOLogic.mk_Trueprop (phi $ (ctor $ x)); in Logic.all x (Logic.list_implies (IHs, concl)) end; - val prems = map4 mk_prem phis ctors FTs_setss xFs; + val prems = @{map 4} mk_prem phis ctors FTs_setss xFs; fun mk_concl phi z = phi $ z; val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_concl phis Izs)); @@ -1261,20 +1261,20 @@ fold_rev Logic.all [z1, z2] (Logic.list_implies ([prem1, prem2], concl)) end; - val IHs = map5 mk_IH phi2s (drop m sets) (drop m sets') Izs1 Izs2; + val IHs = @{map 5} mk_IH phi2s (drop m sets) (drop m sets') Izs1 Izs2; val concl = HOLogic.mk_Trueprop (phi $ (ctor $ x) $ (ctor' $ y)); in fold_rev Logic.all [x, y] (Logic.list_implies (IHs, concl)) end; - val prems = map7 mk_prem phi2s ctors ctor's FTs_setss FTs'_setss xFs yFs; + val prems = @{map 7} mk_prem phi2s ctors ctor's FTs_setss FTs'_setss xFs yFs; fun mk_concl phi z1 z2 = phi $ z1 $ z2; val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map3 mk_concl phi2s Izs1 Izs2)); + (@{map 3} mk_concl phi2s Izs1 Izs2)); fun mk_t phi (z1, z1') (z2, z2') = Term.absfree z1' (HOLogic.mk_all (fst z2', snd z2', phi $ z1 $ z2)); - val cts = map3 (SOME o certify lthy ooo mk_t) phi2s (Izs1 ~~ Izs1') (Izs2 ~~ Izs2'); + val cts = @{map 3} (SOME o certify lthy ooo mk_t) phi2s (Izs1 ~~ Izs1') (Izs2 ~~ Izs2'); val goal = Logic.list_implies (prems, concl); in (Goal.prove_sorry lthy [] [] goal @@ -1347,7 +1347,7 @@ Library.foldl1 mk_union (map mk_UN (drop m sets)))) end; - val colss = map5 (fn l => fn T => map3 (mk_col l T)) ls passiveAs AFss AFss' setsss; + val colss = @{map 5} (fn l => fn T => @{map 3} (mk_col l T)) ls passiveAs AFss AFss' setsss; val setss_by_range = map (fn cols => map (mk_fold Ts cols) ks) colss; val setss_by_bnf = transpose setss_by_range; @@ -1376,7 +1376,7 @@ |> minimize_wits end; in - map3 (fn ctor => fn i => map close_wit o minimize_wits o maps (mk_wit witss ctor i)) + @{map 3} (fn ctor => fn i => map close_wit o minimize_wits o maps (mk_wit witss ctor i)) ctors (0 upto n - 1) witss end; @@ -1431,23 +1431,23 @@ fun mk_set_sbd0 i bd0_Card_order bd0s = map (fn thm => @{thm ordLeq_ordIso_trans} OF [bd0_Card_order RS mk_ordLeq_csum n i thm, sbd0_ordIso]) bd0s; - val set_sbd0ss = map3 mk_set_sbd0 ks bd0_Card_orders set_bd0ss; + val set_sbd0ss = @{map 3} mk_set_sbd0 ks bd0_Card_orders set_bd0ss; in (lthy, sbd0, sbd0_card_order, sbd0_Cinfinite, set_sbd0ss) end; val (Ibnf_consts, lthy) = - fold_map8 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn wits => - fn T => fn lthy => + @{fold_map 8} (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => + fn wits => fn T => fn lthy => define_bnf_consts Hardly_Inline (user_policy Note_Some lthy) false (SOME deads) map_b rel_b set_bs ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd0), wits), NONE) lthy) bs map_bs rel_bs set_bss fs_maps setss_by_bnf ctor_witss Ts lthy; - val (_, Iconsts, Iconst_defs, mk_Iconsts) = split_list4 Ibnf_consts; - val (_, Isetss, Ibds_Ds, Iwitss_Ds, _) = split_list5 Iconsts; - val (Imap_defs, Iset_defss, Ibd_defs, Iwit_defss, Irel_defs) = split_list5 Iconst_defs; - val (mk_Imaps_Ds, mk_It_Ds, _, mk_Irels_Ds, _) = split_list5 mk_Iconsts; + val (_, Iconsts, Iconst_defs, mk_Iconsts) = @{split_list 4} Ibnf_consts; + val (_, Isetss, Ibds_Ds, Iwitss_Ds, _) = @{split_list 5} Iconsts; + val (Imap_defs, Iset_defss, Ibd_defs, Iwit_defss, Irel_defs) = @{split_list 5} Iconst_defs; + val (mk_Imaps_Ds, mk_It_Ds, _, mk_Irels_Ds, _) = @{split_list 5} mk_Iconsts; val Irel_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Irel_defs; val Iset_defs = flat Iset_defss; @@ -1474,9 +1474,9 @@ fun mk_goal fs_map map ctor ctor' = mk_Trueprop_eq (HOLogic.mk_comp (fs_map, ctor), HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ fs_Imaps))); - val goals = map4 mk_goal fs_Imaps map_FTFT's ctors ctor's; + val goals = @{map 4} mk_goal fs_Imaps map_FTFT's ctors ctor's; val maps = - map4 (fn goal => fn foldx => fn map_comp_id => fn map_cong0 => + @{map 4} (fn goal => fn foldx => fn map_comp_id => fn map_cong0 => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN mk_map_tac m n foldx map_comp_id map_cong0) @@ -1492,7 +1492,7 @@ fun mk_prem u map ctor ctor' = mk_Trueprop_eq (HOLogic.mk_comp (u, ctor), HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ us))); - val prems = map4 mk_prem us map_FTFT's ctors ctor's; + val prems = @{map 4} mk_prem us map_FTFT's ctors ctor's; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) us fs_Imaps)); @@ -1513,7 +1513,8 @@ mk_Trueprop_eq (HOLogic.mk_comp (set, ctor), HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets))); val goalss = - map3 (fn sets => map4 (mk_goal sets) ctors sets) Isetss_by_range colss map_setss; + @{map 3} (fn sets => @{map 4} (mk_goal sets) ctors sets) + Isetss_by_range colss map_setss; val setss = map (map2 (fn foldx => fn goal => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Iset_defs THEN mk_set_tac foldx) @@ -1526,11 +1527,11 @@ Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ z)) act_sets sets))); val simp_goalss = map2 (fn i => fn sets => - map4 (fn Fsets => mk_simp_goal (nth Fsets (i - 1)) (drop m Fsets) sets) + @{map 4} (fn Fsets => mk_simp_goal (nth Fsets (i - 1)) (drop m Fsets) sets) FTs_setss ctors xFs sets) ls Isetss_by_range; - val ctor_setss = map3 (fn i => map3 (fn set_nats => fn goal => fn set => + val ctor_setss = @{map 3} (fn i => @{map 3} (fn set_nats => fn goal => fn set => Goal.prove_sorry lthy [] [] goal (K (mk_ctor_set_tac set (nth set_nats (i - 1)) (drop m set_nats))) |> Thm.close_derivation @@ -1563,21 +1564,21 @@ val csetss = map (map (certify lthy)) Isetss_by_range'; - val cphiss = map3 (fn f => fn sets => fn sets' => - (map4 (mk_cphi f) fs_Imaps Izs sets sets')) fs Isetss_by_range Isetss_by_range'; + val cphiss = @{map 3} (fn f => fn sets => fn sets' => + (@{map 4} (mk_cphi f) fs_Imaps Izs sets sets')) fs Isetss_by_range Isetss_by_range'; val inducts = map (fn cphis => Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss; val goals = - map3 (fn f => fn sets => fn sets' => + @{map 3} (fn f => fn sets => fn sets' => HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map4 (mk_set_map0 f) fs_Imaps Izs sets sets'))) + (@{map 4} (mk_set_map0 f) fs_Imaps Izs sets sets'))) fs Isetss_by_range Isetss_by_range'; fun mk_tac ctxt induct = mk_set_nat_tac ctxt m (rtac induct) set_mapss ctor_Imap_thms; val thms = - map5 (fn goal => fn csets => fn ctor_sets => fn induct => fn i => + @{map 5} (fn goal => fn csets => fn ctor_sets => fn induct => fn i => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => mk_tac ctxt induct csets ctor_sets i) |> Thm.close_derivation @@ -1601,11 +1602,11 @@ val goals = map (fn sets => HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map3 mk_set_bd Izs Ibds sets))) Isetss_by_range; + (@{map 3} mk_set_bd Izs Ibds sets))) Isetss_by_range; fun mk_tac ctxt induct = mk_set_bd_tac ctxt m (rtac induct) sbd0_Cinfinite set_sbd0ss; val thms = - map4 (fn goal => fn ctor_sets => fn induct => fn i => + @{map 4} (fn goal => fn ctor_sets => fn induct => fn i => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Ibd_defs THEN mk_tac ctxt induct ctor_sets i) @@ -1623,19 +1624,19 @@ fun mk_map_cong0 sets z fmap gmap = HOLogic.mk_imp - (Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys'), + (Library.foldr1 HOLogic.mk_conj (@{map 5} (mk_prem z) sets fs fs_copy ys ys'), HOLogic.mk_eq (fmap $ z, gmap $ z)); fun mk_cphi sets z fmap gmap = certify lthy (Term.absfree (dest_Free z) (mk_map_cong0 sets z fmap gmap)); - val cphis = map4 mk_cphi Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps; + val cphis = @{map 4} mk_cphi Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps; val induct = Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map4 mk_map_cong0 Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps)); + (@{map 4} mk_map_cong0 Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps)); val thm = Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => mk_mcong_tac ctxt (rtac induct) set_Iset_thmsss @@ -1666,9 +1667,9 @@ let fun mk_goal xF yF ctor ctor' Irelphi relphi = mk_Trueprop_eq (Irelphi $ (ctor $ xF) $ (ctor' $ yF), relphi $ xF $ yF); - val goals = map6 mk_goal xFs yFs ctors ctor's Irelphis relphis; + val goals = @{map 6} mk_goal xFs yFs ctors ctor's Irelphis relphis; in - map12 (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 => + @{map 12} (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 => fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor => fn set_map0s => fn ctor_set_incls => fn ctor_set_set_inclss => Goal.prove_sorry lthy [] [] goal @@ -1686,12 +1687,12 @@ fun mk_le_Irel_OO Irelpsi1 Irelpsi2 Irelpsi12 Iz1 Iz2 = HOLogic.mk_imp (mk_rel_compp (Irelpsi1, Irelpsi2) $ Iz1 $ Iz2, Irelpsi12 $ Iz1 $ Iz2); - val goals = map5 mk_le_Irel_OO Irelpsi1s Irelpsi2s Irelpsi12s Izs1 Izs2; + val goals = @{map 5} mk_le_Irel_OO Irelpsi1s Irelpsi2s Irelpsi12s Izs1 Izs2; val cTs = map (SOME o certifyT lthy o TFree) induct2_params; val cxs = map (SOME o certify lthy) (splice Izs1 Izs2); fun mk_cphi z1 z2 goal = SOME (certify lthy (Term.absfree z1 (Term.absfree z2 goal))); - val cphis = map3 mk_cphi Izs1' Izs2' goals; + val cphis = @{map 3} mk_cphi Izs1' Izs2' goals; val induct = Drule.instantiate' cTs (cphis @ cxs) ctor_induct2_thm; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals); @@ -1720,14 +1721,14 @@ val rel_OO_Grp_tacs = map (fn def => K (rtac def 1)) Irel_unabs_defs; - val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss + val tacss = @{map 9} zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs; fun wit_tac ctxt = unfold_thms_tac ctxt (flat Iwit_defss) THEN mk_wit_tac ctxt n (flat ctor_Iset_thmss) (maps wit_thms_of_bnf bnfs); val (Ibnfs, lthy) = - fold_map5 (fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts => + @{fold_map 5} (fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts => bnf_def Do_Inline (user_policy Note_Some) false I tacs wit_tac (SOME deads) map_b rel_b set_bs consts) tacss map_bs rel_bs set_bss diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Wed Oct 08 18:10:17 2014 +0200 @@ -115,7 +115,7 @@ val bs = map mk_binding b_names; val rhss = mk_split_rec_rhs lthy fpTs Cs recs; in - fold_map3 (define_co_rec_as Least_FP Cs) fpTs bs rhss lthy + @{fold_map 3} (define_co_rec_as Least_FP Cs) fpTs bs rhss lthy end; fun mk_split_rec_thmss ctxt Xs ctrXs_Tsss ctrss rec0_thmss (recs as rec1 :: _) rec_defs = @@ -149,7 +149,7 @@ (mk_Trueprop_eq (frec $ gctr, Term.list_comb (f, fgs))) end; - val goalss = map4 (map3 o mk_goal) frecs ctrXs_Tsss ctrss fss; + val goalss = @{map 4} (@{map 3} o mk_goal) frecs ctrXs_Tsss ctrss fss; fun tac ctxt = unfold_thms_tac ctxt (@{thms o_apply fst_conv snd_conv} @ rec_defs @ flat rec0_thmss) THEN @@ -237,7 +237,7 @@ (index, (T_name, map mk_dtyp Ts, map (mk_ctr_descr Ts) ctrs)); val fp_ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar o checked_fp_sugar_of) fpT_names; - val orig_descr = map3 mk_typ_descr (0 upto nn_fp - 1) fpTs fp_ctr_sugars; + val orig_descr = @{map 3} mk_typ_descr (0 upto nn_fp - 1) fpTs fp_ctr_sugars; val all_infos = Old_Datatype_Data.get_all thy; val (orig_descr' :: nested_descrs) = if member (op =) prefs Keep_Nesting then [orig_descr] diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Wed Oct 08 18:10:17 2014 +0200 @@ -232,7 +232,7 @@ end; fun mk_ctr_specs fp_res_index k ctrs rec_thms = - map4 mk_ctr_spec ctrs (k upto k + length ctrs - 1) (nth perm_fun_arg_Tssss fp_res_index) + @{map 4} mk_ctr_spec ctrs (k upto k + length ctrs - 1) (nth perm_fun_arg_Tssss fp_res_index) rec_thms; fun mk_spec ctr_offset @@ -433,7 +433,7 @@ (recs, ctr_poss) |-> map2 (fn recx => fn ctr_pos => list_comb (recx, rec_args) |> permute_args ctr_pos) |> Syntax.check_terms ctxt - |> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t))) + |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t))) bs mxs end; @@ -595,11 +595,11 @@ val (fixes, specs) = fst (prep_spec raw_fixes raw_specs lthy); val mk_notes = - flat ooo map3 (fn js => fn prefix => fn thms => + flat ooo @{map 3} (fn js => fn prefix => fn thms => let val (bs, attrss) = map_split (fst o nth specs) js; val notes = - map3 (fn b => fn attrs => fn thm => + @{map 3} (fn b => fn attrs => fn thm => ((Binding.qualify false prefix b, code_nitpicksimp_simp_attrs @ attrs), [([thm], [])])) bs attrss thms; diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Wed Oct 08 18:10:17 2014 +0200 @@ -57,7 +57,7 @@ val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs; val fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs; in - (missing_arg_Ts, perm0_kks, map3 basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars, + (missing_arg_Ts, perm0_kks, @{map 3} basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars, fp_nesting_map_ident0s, fp_nesting_map_comps, common_induct, induct_attrs, is_some lfp_sugar_thms, lthy) end; @@ -102,7 +102,7 @@ let val Type (_, ran_Ts) = range_type (typof t); val map' = mk_map (length fs) Us ran_Ts map0; - val fs' = map_flattened_map_args ctxt s (map3 massage_map_or_map_arg Us Ts) fs; + val fs' = map_flattened_map_args ctxt s (@{map 3} massage_map_or_map_arg Us Ts) fs; in Term.list_comb (map', fs') end diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Wed Oct 08 18:10:17 2014 +0200 @@ -192,7 +192,7 @@ val nested_size_o_maps = fold (union Thm.eq_thm_prop) nested_size_o_mapss []; val ((raw_size_consts, raw_size_defs), (lthy1', lthy1)) = lthy0 - |> apfst split_list o fold_map2 (fn b => fn rhs => + |> apfst split_list o @{fold_map 2} (fn b => fn rhs => Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs)) #>> apsnd snd) size_bs size_rhss @@ -227,7 +227,7 @@ val (overloaded_size_defs, lthy2) = lthy1 |> Local_Theory.background_theory_result (Class.instantiation (T_names, map dest_TFree As, [HOLogic.class_size]) - #> fold_map3 define_overloaded_size overloaded_size_def_bs overloaded_size_consts + #> @{fold_map 3} define_overloaded_size overloaded_size_def_bs overloaded_size_consts overloaded_size_rhss ##> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) ##> Local_Theory.exit_global); @@ -324,7 +324,7 @@ map2 (fold_rev (fold_rev Logic.all) [gs, hs] o HOLogic.mk_Trueprop oo curry HOLogic.mk_eq) rec_o_map_lhss rec_o_map_rhss; val rec_o_map_thms = - map3 (fn goal => fn rec_def => fn ctor_rec_o_map => + @{map 3} (fn goal => fn rec_def => fn ctor_rec_o_map => Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} => mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses ctor_rec_o_map) @@ -351,7 +351,7 @@ val size_o_map_thmss = if nested_size_o_maps_complete then - map3 (fn goal => fn size_def => fn rec_o_map => + @{map 3} (fn goal => fn size_def => fn rec_o_map => Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} => mk_size_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps) |> Thm.close_derivation diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/BNF/bnf_lfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Wed Oct 08 18:10:17 2014 +0200 @@ -473,7 +473,7 @@ EVERY' [select_prem_tac n (dtac asm_rl) k, rtac ballI, rtac impI, rtac (mor_Abs RS morE RS arg_cong RS iffD2), atac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], dtac @{thm meta_spec}, - EVERY' (map3 mk_IH_tac Rep_invs Abs_invs (drop m set_maps)), atac]; + EVERY' (@{map 3} mk_IH_tac Rep_invs Abs_invs (drop m set_maps)), atac]; fun mk_induct_tac (Rep, Rep_inv) = EVERY' [rtac (Rep_inv RS arg_cong RS iffD1), etac (Rep RSN (2, bspec))]; @@ -547,7 +547,7 @@ REPEAT_DETERM_N (n - 1) o EVERY' (map rtac [trans, @{thm image_Un}, Un_cong]), EVERY' (map useIH (drop m set_nats))]; in - (induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps ctor_sets set_mapss)) 1 + (induct_tac THEN' EVERY' (@{map 4} mk_set_nat csets ctor_maps ctor_sets set_mapss)) 1 end; fun mk_set_bd_tac ctxt m induct_tac bd_Cinfinite set_bdss ctor_sets i = @@ -581,12 +581,12 @@ EVERY' (map useIH (transpose (map tl set_setss))), rtac sym, rtac ctor_map]; in - (induct_tac THEN' EVERY' (map3 mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1 + (induct_tac THEN' EVERY' (@{map 3} mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1 end; fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs = EVERY' (rtac induct :: - map4 (fn nchotomy => fn Irel => fn rel_mono => fn le_rel_OO => + @{map 4} (fn nchotomy => fn Irel => fn rel_mono => fn le_rel_OO => EVERY' [rtac impI, etac (nchotomy RS @{thm nchotomy_relcomppE}), REPEAT_DETERM_N 2 o dtac (Irel RS iffD1), rtac (Irel RS iffD2), rtac rel_mono, rtac (le_rel_OO RS @{thm predicate2D}), @@ -725,7 +725,7 @@ in unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN EVERY' [REPEAT_DETERM o rtac allI, rtac ctor_induct2, - EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong0 => + EVERY' (@{map 3} (fn IH => fn ctor_rel => fn rel_mono_strong0 => EVERY' [rtac impI, dtac (ctor_rel RS iffD1), rtac (IH RS @{thm spec2} RS mp), etac rel_mono_strong0, REPEAT_DETERM_N m o rtac @{thm ballI[OF ballI[OF imp_refl]]}, diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_util.ML Wed Oct 08 18:10:17 2014 +0200 @@ -10,82 +10,6 @@ include CTR_SUGAR_UTIL include BNF_FP_REC_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) -> - 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list - val map8: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i) -> - 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i list - val map9: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j) -> - 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> - 'i list -> 'j list - val map10: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k) -> - 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> - 'i list -> 'j list -> 'k list - val map11: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l) -> - 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> - 'i list -> 'j list -> 'k list -> 'l list - val map12: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm) -> - '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 - 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 map14: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n -> - 'o) -> - '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 -> 'o list - val map15: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n -> - 'o -> 'p) -> - '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 -> 'o list -> 'p list - val map16: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n -> - 'o -> 'p -> 'q) -> - '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 -> 'o list -> 'p list -> 'q list - 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) -> - 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f -> 'g list * 'f - val fold_map6: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h * 'g) -> - 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g -> 'h list * 'g - val fold_map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i * 'h) -> - 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h -> 'i list * 'h - val fold_map8: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j * 'i) -> - 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i -> - 'j list * 'i - val fold_map9: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k * 'j) -> - '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 split_list5: ('a * 'b * 'c * 'd * 'e) list -> 'a list * 'b list * 'c list * 'd list * 'e list - val split_list6: ('a * 'b * 'c * 'd * 'e * 'f) list -> 'a list * 'b list * 'c list * 'd list * - 'e list * 'f list - val split_list7: ('a * 'b * 'c * 'd * 'e * 'f * 'g) list -> 'a list * 'b list * 'c list * - 'd list * 'e list * 'f list * 'g list - val split_list8: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h) list -> 'a list * 'b list * 'c list * - 'd list * 'e list * 'f list * 'g list * 'h list - val split_list9: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i) list -> 'a list * 'b list * - 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list - val split_list10: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j) list -> 'a list * 'b list * - 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list * 'j list - val split_list11: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k) list -> 'a list * - 'b list * 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list * 'j list * - 'k list - val split_list12: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l) list -> 'a list * - 'b list * 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list * 'j list * - 'k list * 'l list - val split_list13: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l * 'm) list -> - '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 - val split_list14: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l * 'm * 'n) list -> - '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 split_list15: - ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l * 'm * 'n * 'o) list -> - '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 * 'o list - val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context val mk_Freesss: string -> typ list list list -> Proof.context -> term list list list * Proof.context @@ -192,194 +116,6 @@ (* Library proper *) -fun map6 _ [] [] [] [] [] [] = [] - | map6 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) = - f x1 x2 x3 x4 x5 x6 :: map6 f x1s x2s x3s x4s x5s x6s - | map6 _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; - -fun map7 _ [] [] [] [] [] [] [] = [] - | map7 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) = - f x1 x2 x3 x4 x5 x6 x7 :: map7 f x1s x2s x3s x4s x5s x6s x7s - | map7 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; - -fun map8 _ [] [] [] [] [] [] [] [] = [] - | map8 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) = - f x1 x2 x3 x4 x5 x6 x7 x8 :: map8 f x1s x2s x3s x4s x5s x6s x7s x8s - | map8 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; - -fun map9 _ [] [] [] [] [] [] [] [] [] = [] - | map9 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) - (x9::x9s) = - f x1 x2 x3 x4 x5 x6 x7 x8 x9 :: map9 f x1s x2s x3s x4s x5s x6s x7s x8s x9s - | map9 _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; - -fun map10 _ [] [] [] [] [] [] [] [] [] [] = [] - | map10 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) - (x9::x9s) (x10::x10s) = - f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 :: map10 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s - | map10 _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; - -fun map11 _ [] [] [] [] [] [] [] [] [] [] [] = [] - | map11 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) - (x9::x9s) (x10::x10s) (x11::x11s) = - f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 :: map11 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s - | map11 _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; - -fun map12 _ [] [] [] [] [] [] [] [] [] [] [] [] = [] - | map12 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) - (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) = - f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 :: - map12 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s - | map12 _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; - -fun map13 _ [] [] [] [] [] [] [] [] [] [] [] [] [] = [] - | map13 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) - (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) = - f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 :: - map13 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s - | map13 _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; - -fun map14 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] = [] - | map14 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) - (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) = - f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 :: - map14 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s - | map14 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; - -fun map15 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] = [] - | map15 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) - (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) (x15::x15s) = - f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 :: - map15 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s - | map15 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; - -fun map16 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] = [] - | map16 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) - (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) (x15::x15s) (x16::x16s) = - f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 :: - map16 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s x16s - | map16 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; - -fun fold_map4 _ [] [] [] [] acc = ([], acc) - | fold_map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) acc = - let - val (x, acc') = f x1 x2 x3 x4 acc; - val (xs, acc'') = fold_map4 f x1s x2s x3s x4s acc'; - in (x :: xs, acc'') end - | fold_map4 _ _ _ _ _ _ = raise ListPair.UnequalLengths; - -fun fold_map5 _ [] [] [] [] [] acc = ([], acc) - | fold_map5 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) acc = - let - val (x, acc') = f x1 x2 x3 x4 x5 acc; - val (xs, acc'') = fold_map5 f x1s x2s x3s x4s x5s acc'; - in (x :: xs, acc'') end - | fold_map5 _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; - -fun fold_map6 _ [] [] [] [] [] [] acc = ([], acc) - | fold_map6 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) acc = - let - val (x, acc') = f x1 x2 x3 x4 x5 x6 acc; - val (xs, acc'') = fold_map6 f x1s x2s x3s x4s x5s x6s acc'; - in (x :: xs, acc'') end - | fold_map6 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; - -fun fold_map7 _ [] [] [] [] [] [] [] acc = ([], acc) - | fold_map7 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) acc = - let - val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 acc; - val (xs, acc'') = fold_map7 f x1s x2s x3s x4s x5s x6s x7s acc'; - in (x :: xs, acc'') end - | fold_map7 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; - -fun fold_map8 _ [] [] [] [] [] [] [] [] acc = ([], acc) - | fold_map8 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) - acc = - let - val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 x8 acc; - val (xs, acc'') = fold_map8 f x1s x2s x3s x4s x5s x6s x7s x8s acc'; - in (x :: xs, acc'') end - | fold_map8 _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; - -fun fold_map9 _ [] [] [] [] [] [] [] [] [] acc = ([], acc) - | fold_map9 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) - (x9::x9s) acc = - let - val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 x8 x9 acc; - val (xs, acc'') = fold_map9 f x1s x2s x3s x4s x5s x6s x7s x8s x9s acc'; - in (x :: xs, acc'') end - | fold_map9 _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; - -fun split_list4 [] = ([], [], [], []) - | split_list4 ((x1, x2, x3, x4) :: xs) = - let val (xs1, xs2, xs3, xs4) = split_list4 xs; - in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4) end; - -fun split_list5 [] = ([], [], [], [], []) - | split_list5 ((x1, x2, x3, x4, x5) :: xs) = - let val (xs1, xs2, xs3, xs4, xs5) = split_list5 xs; - in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5) end; - -fun split_list6 [] = ([], [], [], [], [], []) - | split_list6 ((x1, x2, x3, x4, x5, x6) :: xs) = - let val (xs1, xs2, xs3, xs4, xs5, xs6) = split_list6 xs; - in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6) end; - -fun split_list7 [] = ([], [], [], [], [], [], []) - | split_list7 ((x1, x2, x3, x4, x5, x6, x7) :: xs) = - let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7) = split_list7 xs; - in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7) end; - -fun split_list8 [] = ([], [], [], [], [], [], [], []) - | split_list8 ((x1, x2, x3, x4, x5, x6, x7, x8) :: xs) = - let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8) = split_list8 xs; - in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8) end; - -fun split_list9 [] = ([], [], [], [], [], [], [], [], []) - | split_list9 ((x1, x2, x3, x4, x5, x6, x7, x8, x9) :: xs) = - let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9) = split_list9 xs; - in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8, - x9 :: xs9) end; - -fun split_list10 [] = ([], [], [], [], [], [], [], [], [], []) - | split_list10 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) :: xs) = - let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10) = split_list10 xs; - in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8, - x9 :: xs9, x10 :: xs10) end; - -fun split_list11 [] = ([], [], [], [], [], [], [], [], [], [], []) - | split_list11 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) :: xs) = - let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11) = split_list11 xs; - in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8, - x9 :: xs9, x10 :: xs10, x11 :: xs11) end; - -fun split_list12 [] = ([], [], [], [], [], [], [], [], [], [], [], []) - | split_list12 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) :: xs) = - let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11, xs12) = split_list12 xs; - in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8, - x9 :: xs9, x10 :: xs10, x11 :: xs11, x12 :: xs12) end; - -fun split_list13 [] = ([], [], [], [], [], [], [], [], [], [], [], [], []) - | split_list13 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) :: xs) = - let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11, xs12, xs13) = split_list13 xs; - in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8, - x9 :: xs9, x10 :: xs10, x11 :: xs11, x12 :: xs12, x13 :: xs13) end; - -fun split_list14 [] = ([], [], [], [], [], [], [], [], [], [], [], [], [], []) - | split_list14 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14) :: xs) = - let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11, xs12, xs13, xs14) = - split_list14 xs; - in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8, - x9 :: xs9, x10 :: xs10, x11 :: xs11, x12 :: xs12, x13 :: xs13, x14 :: xs14) end; - -fun split_list15 [] = ([], [], [], [], [], [], [], [], [], [], [], [], [], [], []) - | split_list15 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) :: xs) = - let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11, xs12, xs13, xs14, xs15) = - split_list15 xs; - in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8, - x9 :: xs9, x10 :: xs10, x11 :: xs11, x12 :: xs12, x13 :: xs13, x14 :: xs14, x15 :: xs15) - end; - val parse_type_arg_constrained = Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort); @@ -430,8 +166,8 @@ val mk_TFreess = fold_map mk_TFrees; -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_Freesss x Tsss = @{fold_map 2} mk_Freess (mk_names (length Tsss) x) Tsss; +fun mk_Freessss x Tssss = @{fold_map 2} mk_Freesss (mk_names (length Tssss) x) Tssss; (** Types **) diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Oct 08 18:10:17 2014 +0200 @@ -414,7 +414,7 @@ val disc_bindings = raw_disc_bindings - |> map4 (fn k => fn m => fn ctr => fn disc => + |> @{map 4} (fn k => fn m => fn ctr => fn disc => qualify false (if Binding.is_empty disc then if m = 0 then equal_binding @@ -428,7 +428,7 @@ fun standard_sel_binding m l = Binding.name o mk_unN m l o base_name_of_ctr; val sel_bindingss = - map3 (fn ctr => fn m => map2 (fn l => fn sel => + @{map 3} (fn ctr => fn m => map2 (fn l => fn sel => qualify false (if Binding.is_empty sel orelse Binding.eq_name (sel, standard_binding) then standard_sel_binding m l ctr @@ -476,7 +476,7 @@ val case_rhs = fold_rev (fold_rev Term.lambda) [fs, [u]] (Const (@{const_name The}, (B --> HOLogic.boolT) --> B) $ - Term.lambda w (Library.foldr1 HOLogic.mk_disj (map3 mk_case_disj xctrs xfs xss))); + Term.lambda w (Library.foldr1 HOLogic.mk_disj (@{map 3} mk_case_disj xctrs xfs xss))); val ((raw_case, (_, raw_case_def)), (lthy', lthy)) = no_defs_lthy |> Local_Theory.define ((case_binding, NoSyn), @@ -538,7 +538,7 @@ else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) all_sel_bindings; - val all_proto_sels = flat (map3 (fn k => fn xs => map (pair k o pair xs)) ks xss xss); + val all_proto_sels = flat (@{map 3} (fn k => fn xs => map (pair k o pair xs)) ks xss xss); val sel_infos = AList.group (op =) (sel_binding_index ~~ all_proto_sels) |> sort (int_ord o pairself fst) @@ -565,7 +565,7 @@ Term.lambda u (alternate_disc_lhs (K o rapp u o disc_free) (3 - k)); fun mk_sel_case_args b proto_sels T = - map3 (fn Const (c, _) => fn Ts => fn k => + @{map 3} (fn Const (c, _) => fn Ts => fn k => (case AList.lookup (op =) proto_sels k of NONE => (case filter (curry (op =) (c, Binding.name_of b) o fst) sel_defaults of @@ -596,7 +596,7 @@ val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) = lthy - |> apfst split_list o fold_map3 (fn k => fn exist_xs_u_eq_ctr => fn b => + |> apfst split_list o @{fold_map 3} (fn k => fn exist_xs_u_eq_ctr => fn b => if Binding.is_empty b then if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def) else pair (alternate_disc k, alternate_disc_no_def) @@ -640,7 +640,7 @@ [fold_rev Logic.all (xs @ ys) (mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr), Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys)))]; in - map4 mk_goal xctrs yctrs xss yss + @{map 4} mk_goal xctrs yctrs xss yss end; val half_distinct_goalss = @@ -686,10 +686,10 @@ val case_thms = let val goals = - map3 (fn xctr => fn xf => fn xs => + @{map 3} (fn xctr => fn xf => fn xs => fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (fcase $ xctr, xf))) xctrs xfs xss; in - map4 (fn k => fn goal => fn injects => fn distinctss => + @{map 4} (fn k => fn goal => fn injects => fn distinctss => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => mk_case_tac ctxt n k case_def injects distinctss) |> Thm.close_derivation) @@ -703,7 +703,7 @@ mk_Trueprop_eq (xf, xg))); val goal = - Logic.list_implies (uv_eq :: map4 mk_prem xctrs xss xfs xgs, + Logic.list_implies (uv_eq :: @{map 4} mk_prem xctrs xss xfs xgs, mk_Trueprop_eq (eta_ufcase, eta_vgcase)); val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase)); in @@ -723,10 +723,10 @@ fun mk_split_goal xctrs xss xfs = mk_Trueprop_eq (split_lhs, Library.foldr1 HOLogic.mk_conj - (map3 mk_split_conjunct xctrs xss xfs)); + (@{map 3} mk_split_conjunct xctrs xss xfs)); fun mk_split_asm_goal xctrs xss xfs = mk_Trueprop_eq (split_lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj - (map3 mk_split_disjunct xctrs xss xfs))); + (@{map 3} mk_split_disjunct xctrs xss xfs))); fun prove_split selss goal = Goal.prove_sorry lthy [] [] goal (fn _ => @@ -771,7 +771,7 @@ zero_var_indexes (Drule.gen_all (Drule.rename_bvars' (map (SOME o fst) xs') (Drule.forall_intr_vars (case_thm RS (sel_def RS trans))))); - val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss; + val sel_thmss = @{map 3} (map oo make_sel_thm) xss' case_thms sel_defss; fun has_undefined_rhs thm = (case snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) of @@ -833,7 +833,7 @@ | mk_thm _ not_discI [distinct] = distinct RS not_discI; fun mk_thms discI not_discI distinctss = map (mk_thm discI not_discI) distinctss; in - map3 mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose + @{map 3} mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose end; val nontriv_disc_thmss = @@ -861,7 +861,7 @@ val half_goalss = map mk_goal half_pairss; val half_thmss = - map3 (fn [] => K (K []) | [goal] => fn [(((m, discD), _), _)] => + @{map 3} (fn [] => K (K []) | [goal] => fn [(((m, discD), _), _)] => fn disc_thm => [prove (mk_half_distinct_disc_tac lthy m discD disc_thm) goal]) half_goalss half_pairss (flat disc_thmss'); @@ -893,9 +893,9 @@ in (prem aconv concl, Logic.all u (Logic.mk_implies (prem, concl))) end; - val (trivs, goals) = map3 mk_goal ms udiscs usel_ctrs |> split_list; + val (trivs, goals) = @{map 3} mk_goal ms udiscs usel_ctrs |> split_list; val thms = - map5 (fn m => fn discD => fn sel_thms => fn triv => fn goal => + @{map 5} (fn m => fn discD => fn sel_thms => fn triv => fn goal => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => mk_collapse_tac ctxt m discD sel_thms ORELSE HEADGOAL atac) |> Thm.close_derivation @@ -933,7 +933,7 @@ val goal = Library.foldr Logic.list_implies - (map5 mk_prems ks udiscs uselss vdiscs vselss, uv_eq); + (@{map 5} mk_prems ks udiscs uselss vdiscs vselss, uv_eq); val uncollapse_thms = map2 (fn thm => fn [] => thm | _ => thm RS sym) all_collapse_thms uselss; in diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Wed Oct 08 18:10:17 2014 +0200 @@ -100,9 +100,9 @@ else let val ks = 1 upto n in HEADGOAL (rtac uexhaust_disc THEN' - EVERY' (map5 (fn k => fn m => fn distinct_discss => fn distinct_discss' => fn uuncollapse => + EVERY' (@{map 5} (fn k => fn m => fn distinct_discss => fn distinct_discss' => fn uuncollapse => EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac, rtac sym, rtac vexhaust_disc, - EVERY' (map4 (fn k' => fn distinct_discs => fn distinct_discs' => fn vuncollapse => + EVERY' (@{map 4} (fn k' => fn distinct_discs => fn distinct_discs' => fn vuncollapse => EVERY' (if k' = k then [rtac (vuncollapse RS trans), TRY o atac] @ @@ -150,7 +150,7 @@ fun mk_case_eq_if_tac ctxt n uexhaust cases discss' selss = HEADGOAL (rtac uexhaust THEN' - EVERY' (map3 (fn casex => fn if_discs => fn sels => + EVERY' (@{map 3} (fn casex => fn if_discs => fn sels => EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)), rtac casex]) cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss)); diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Wed Oct 08 18:10:17 2014 +0200 @@ -10,13 +10,6 @@ sig val map_prod: ('a -> 'b) -> ('c -> 'd) -> 'a * 'c -> 'b * 'd - 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 @@ -108,35 +101,6 @@ fun map_prod f g (x, y) = (f x, g y); -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) @@ -174,10 +138,10 @@ fun mk_TFrees n = mk_TFrees' (replicate n @{sort type}); 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_Freess' x Tss = @{fold_map 2} 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 mk_Freess x Tss = @{fold_map 2} mk_Frees (mk_names (length Tss) x) Tss; fun dest_TFree_or_TVar (TFree sS) = sS | dest_TFree_or_TVar (TVar ((s, _), S)) = (s, S) @@ -191,7 +155,7 @@ 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); + @{fold_map 2} (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; diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/Function/function_core.ML --- a/src/HOL/Tools/Function/function_core.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/Function/function_core.ML Wed Oct 08 18:10:17 2014 +0200 @@ -873,7 +873,7 @@ val cert = cterm_of (Proof_Context.theory_of lthy) val xclauses = PROFILE "xclauses" - (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees + (@{map 7} (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss val complete = diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/Function/function_lib.ML --- a/src/HOL/Tools/Function/function_lib.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/Function/function_lib.ML Wed Oct 08 18:10:17 2014 +0200 @@ -11,10 +11,6 @@ val dest_all_all: term -> term list * term - val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list - val map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) -> 'a list -> 'b list -> 'c list -> - 'd list -> 'e list -> 'f list -> 'g list -> 'h list - val unordered_pairs: 'a list -> ('a * 'a) list val rename_bound: string -> term -> term @@ -50,14 +46,6 @@ | dest_all_all t = ([],t) -fun map4 f = Ctr_Sugar_Util.map4 f - -fun map7 _ [] [] [] [] [] [] [] = [] - | 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 - | map7 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; - - - (* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *) fun unordered_pairs [] = [] | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/Function/mutual.ML --- a/src/HOL/Tools/Function/mutual.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/Function/mutual.ML Wed Oct 08 18:10:17 2014 +0200 @@ -106,7 +106,7 @@ (MutualPart {i=i, i'=i', fvar=fvar,cargTs=caTs,f_def=def,f=NONE,f_defthm=NONE}, rew) end - val (parts, rews) = split_list (map4 define fs caTss resultTs (1 upto num)) + val (parts, rews) = split_list (@{map 4} define fs caTss resultTs (1 upto num)) fun convert_eqs (f, qs, gs, args, rhs) = let diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/Lifting/lifting_bnf.ML --- a/src/HOL/Tools/Lifting/lifting_bnf.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Wed Oct 08 18:10:17 2014 +0200 @@ -57,7 +57,8 @@ ||>> mk_TFrees live ||>> mk_TFrees (dead_of_bnf bnf) val argTss = map2 (fn a => fn b => [mk_pred2T a a, a --> b, b --> a,mk_pred2T a b]) As Bs - val ((argss, argss'), ctxt) = fold_map2 mk_Frees ["R", "Abs", "Rep", "T"] (transpose argTss) ctxt + val ((argss, argss'), ctxt) = + @{fold_map 2} mk_Frees ["R", "Abs", "Rep", "T"] (transpose argTss) ctxt |>> `transpose val assms = map (mk_Quotient #> HOLogic.mk_Trueprop) argss diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Oct 08 18:10:17 2014 +0200 @@ -1319,7 +1319,7 @@ construct_value ctxt (if new_s = @{type_name prod} then @{const_name Pair} else @{const_name PairBox}, new_Ts ---> new_T) - (map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2] + (@{map 3} (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2] [t1, t2]) | t' => raise TERM ("Nitpick_HOL.coerce_term", [t']) else diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Oct 08 18:10:17 2014 +0200 @@ -602,7 +602,7 @@ val old_rs = map2 (#kk_project_seq kk r) old_offsets old_arities in fold1 (#kk_product kk) - (map3 (rel_expr_from_rel_expr kk) Rs Rs' old_rs) + (@{map 3} (rel_expr_from_rel_expr kk) Rs Rs' old_rs) end else lone_rep_fallback kk (Struct Rs) old_R r diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Oct 08 18:10:17 2014 +0200 @@ -508,7 +508,7 @@ val k2 = k div k1 in list_comb (HOLogic.pair_const T1 T2, - map3 (fn T => term_for_atom seen T T) [T1, T2] + @{map 3} (fn T => term_for_atom seen T T) [T1, T2] (* ### k2 or k1? FIXME *) [j div k2, j mod k2] [k1, k2]) end @@ -578,7 +578,7 @@ if length arg_Ts = 0 then [] else - map3 (fn Ts => term_for_rep true seen Ts Ts) arg_Ts arg_Rs + @{map 3} (fn Ts => term_for_rep true seen Ts Ts) arg_Ts arg_Rs arg_jsss |> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts) |> dest_n_tuple (length uncur_arg_Ts) @@ -633,7 +633,7 @@ val (js1, js2) = chop arity1 js in list_comb (HOLogic.pair_const T1 T2, - map3 (fn T => term_for_rep true seen T T) [T1, T2] [R1, R2] + @{map 3} (fn T => term_for_rep true seen T T) [T1, T2] [R1, R2] [[js1], [js2]]) end | term_for_rep _ seen T T' (Vect (k, R')) [js] = diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Wed Oct 08 18:10:17 2014 +0200 @@ -700,7 +700,7 @@ (mk_quasi_clauses res_aa aa1 aa2)) fun add_connective_frames conn mk_quasi_clauses res_frame frame1 frame2 = - fold I (map3 (fn (_, res_aa) => fn (_, aa1) => fn (_, aa2) => + fold I (@{map 3} (fn (_, res_aa) => fn (_, aa1) => fn (_, aa2) => add_connective_var conn mk_quasi_clauses res_aa aa1 aa2) res_frame frame1 frame2) diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Wed Oct 08 18:10:17 2014 +0200 @@ -1151,7 +1151,7 @@ (j :: js, pool) end) ([], pool) - val ws' = map3 (fn j => fn x => fn T => + val ws' = @{map 3} (fn j => fn x => fn T => constr ((1, j), T, Atom x, nick ^ " [" ^ string_of_int j ^ "]")) (rev js) atom_schema type_schema diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Oct 08 18:10:17 2014 +0200 @@ -439,7 +439,7 @@ s_let Ts "l" (n + 1) dataT bool_T (fn t1 => discriminate_value hol_ctxt x t1 :: - map3 (sel_eq Ts x t1) (index_seq 0 n) arg_Ts args + @{map 3} (sel_eq Ts x t1) (index_seq 0 n) arg_Ts args |> foldr1 s_conj) t1 else raise SAME () diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Oct 08 18:10:17 2014 +0200 @@ -39,7 +39,6 @@ val all_permutations : 'a list -> 'a list list val chunk_list : int -> 'a list -> 'a list list val chunk_list_unevenly : int list -> 'a list -> 'a list list - val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list val double_lookup : ('a * 'a -> bool) -> ('a option * 'b) list -> 'a -> 'b option val triple_lookup : @@ -202,10 +201,6 @@ | chunk_list_unevenly (k :: ks) xs = let val (xs1, xs2) = chop k xs in xs1 :: chunk_list_unevenly ks xs2 end -fun map3 _ [] [] [] = [] - | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs - | map3 _ _ _ _ = raise ListPair.UnequalLengths - fun double_lookup eq ps key = case AList.lookup (fn (SOME x, SOME y) => eq (x, y) | _ => false) ps (SOME key) of diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/SMT/smt_datatypes.ML --- a/src/HOL/Tools/SMT/smt_datatypes.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML Wed Oct 08 18:10:17 2014 +0200 @@ -38,7 +38,7 @@ val selss = if has_duplicates (op aconv) (flat selss0) then [] else selss0 in - Ctr_Sugar_Util.fold_map2 mk_constr ctrs0 (Ctr_Sugar_Util.pad_list [] (length ctrs0) selss) ctxt + @{fold_map 2} mk_constr ctrs0 (Ctr_Sugar_Util.pad_list [] (length ctrs0) selss) ctxt |>> (pair T #> single) end diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Wed Oct 08 18:10:17 2014 +0200 @@ -217,14 +217,14 @@ val time_slice = time_mult (1.0 / Real.fromInt (length labels)) (reference_time l) val timeouts = map (adjust_merge_timeout preplay_timeout o curry Time.+ time_slice) times0 - val meths_outcomess = map3 (preplay_isar_step ctxt) timeouts hopelesses succs' + val meths_outcomess = @{map 3} (preplay_isar_step ctxt) timeouts hopelesses succs' in (case try (map (fn (_, Played time) :: _ => time)) meths_outcomess of NONE => steps | SOME times => (* "l" successfully eliminated *) (decrement_step_count (); - map3 (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data) + @{map 3} (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data) times succs' meths_outcomess; map (replace_successor l labels) lfs; steps_before @ update_steps succs' steps_after)) diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Oct 08 18:10:17 2014 +0200 @@ -8,7 +8,6 @@ sig val sledgehammerN : string val log2 : real -> real - val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list val app_hd : ('a -> 'a) -> 'a list -> 'a list val plural_s : int -> string val serial_commas : string -> string list -> string list @@ -39,8 +38,6 @@ val log10_2 = Math.log10 2.0 fun log2 n = Math.log10 n / log10_2 -fun map3 xs = Ctr_Sugar_Util.map3 xs - fun app_hd f (x :: xs) = f x :: xs fun plural_s n = if n = 1 then "" else "s" diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/Tools/coinduction.ML --- a/src/HOL/Tools/coinduction.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/Tools/coinduction.ML Wed Oct 08 18:10:17 2014 +0200 @@ -73,7 +73,7 @@ val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs |>> (fn names => Variable.variant_fixes names names_ctxt) ; val eqs = - map3 (fn name => fn T => fn (_, rhs) => + @{map 3} (fn name => fn T => fn (_, rhs) => HOLogic.mk_eq (Free (name, T), rhs)) names Ts raw_eqs; val phi = eqs @ map (HOLogic.dest_Trueprop o prop_of) prems diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/ex/SOS.thy --- a/src/HOL/ex/SOS.thy Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/ex/SOS.thy Wed Oct 08 18:10:17 2014 +0200 @@ -10,121 +10,121 @@ begin lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \ a < 0" - by (sos csdp) + by sos lemma "a1 >= 0 & a2 >= 0 \ (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \ (a1 * b1 + a2 * b2 = 0) --> a1 * a2 - b1 * b2 >= (0::real)" - by (sos csdp) + by sos lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x --> a < 0" - by (sos csdp) + by sos lemma "(0::real) <= x & x <= 1 & 0 <= y & y <= 1 --> x^2 + y^2 < 1 |(x - 1)^2 + y^2 < 1 | x^2 + (y - 1)^2 < 1 | (x - 1)^2 + (y - 1)^2 < 1" - by (sos csdp) + by sos lemma "(0::real) <= x & 0 <= y & 0 <= z & x + y + z <= 3 --> x * y + x * z + y * z >= 3 * x * y * z" - by (sos csdp) + by sos lemma "((x::real)^2 + y^2 + z^2 = 1) --> (x + y + z)^2 <= 3" - by (sos csdp) + by sos lemma "(w^2 + x^2 + y^2 + z^2 = 1) --> (w + x + y + z)^2 <= (4::real)" - by (sos csdp) + by sos lemma "(x::real) >= 1 & y >= 1 --> x * y >= x + y - 1" - by (sos csdp) + by sos lemma "(x::real) > 1 & y > 1 --> x * y > x + y - 1" - by (sos csdp) + by sos lemma "abs(x) <= 1 --> abs(64 * x^7 - 112 * x^5 + 56 * x^3 - 7 * x) <= (1::real)" - by (sos csdp) + by sos text \One component of denominator in dodecahedral example.\ lemma "2 <= x & x <= 125841 / 50000 & 2 <= y & y <= 125841 / 50000 & 2 <= z & z <= 125841 / 50000 --> 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z) >= (0::real)" - by (sos csdp) + by sos text \Over a larger but simpler interval.\ lemma "(2::real) <= x & x <= 4 & 2 <= y & y <= 4 & 2 <= z & z <= 4 --> 0 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" - by (sos csdp) + by sos text \We can do 12. I think 12 is a sharp bound; see PP's certificate.\ lemma "2 <= (x::real) & x <= 4 & 2 <= y & y <= 4 & 2 <= z & z <= 4 --> 12 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" - by (sos csdp) + by sos text \Inequality from sci.math (see "Leon-Sotelo, por favor").\ lemma "0 <= (x::real) & 0 <= y & (x * y = 1) --> x + y <= x^2 + y^2" - by (sos csdp) + by sos lemma "0 <= (x::real) & 0 <= y & (x * y = 1) --> x * y * (x + y) <= x^2 + y^2" - by (sos csdp) + by sos lemma "0 <= (x::real) & 0 <= y --> x * y * (x + y)^2 <= (x^2 + y^2)^2" - by (sos csdp) + by sos lemma "(0::real) <= a & 0 <= b & 0 <= c & c * (2 * a + b)^3/ 27 <= x \ c * a^2 * b <= x" - by (sos csdp) + by sos lemma "(0::real) < x --> 0 < 1 + x + x^2" - by (sos csdp) + by sos lemma "(0::real) <= x --> 0 < 1 + x + x^2" - by (sos csdp) + by sos lemma "(0::real) < 1 + x^2" - by (sos csdp) + by sos lemma "(0::real) <= 1 + 2 * x + x^2" - by (sos csdp) + by sos lemma "(0::real) < 1 + abs x" - by (sos csdp) + by sos lemma "(0::real) < 1 + (1 + x)^2 * (abs x)" - by (sos csdp) + by sos lemma "abs ((1::real) + x^2) = (1::real) + x^2" - by (sos csdp) + by sos lemma "(3::real) * x + 7 * a < 4 \ 3 < 2 * x \ a < 0" - by (sos csdp) + by sos lemma "(0::real) < x --> 1 < y --> y * x <= z --> x < z" - by (sos csdp) + by sos lemma "(1::real) < x --> x^2 < y --> 1 < y" - by (sos csdp) + by sos lemma "(b::real)^2 < 4 * a * c --> ~(a * x^2 + b * x + c = 0)" - by (sos csdp) + by sos lemma "(b::real)^2 < 4 * a * c --> ~(a * x^2 + b * x + c = 0)" - by (sos csdp) + by sos lemma "((a::real) * x^2 + b * x + c = 0) --> b^2 >= 4 * a * c" - by (sos csdp) + by sos lemma "(0::real) <= b & 0 <= c & 0 <= x & 0 <= y & (x^2 = c) & (y^2 = a^2 * c + b) --> a * c <= y * x" - by (sos csdp) + by sos lemma "abs(x - z) <= e & abs(y - z) <= e & 0 <= u & 0 <= v & (u + v = 1) --> abs((u * x + v * y) - z) <= (e::real)" - by (sos csdp) + by sos (* lemma "((x::real) - y - 2 * x^4 = 0) & 0 <= x & x <= 2 & 0 <= y & y <= 3 --> y^2 - 7 * y - 12 * x + 17 >= 0" by sos *) (* Too hard?*) lemma "(0::real) <= x --> (1 + x + x^2)/(1 + x^2) <= 1 + x" - by (sos csdp) + by sos lemma "(0::real) <= x --> 1 - x <= 1 / (1 + x + x^2)" - by (sos csdp) + by sos lemma "(x::real) <= 1 / 2 --> - x - 2 * x^2 <= - x / (1 - x)" - by (sos csdp) + by sos lemma "4*r^2 = p^2 - 4*q & r >= (0::real) & x^2 + p*x + q = 0 --> 2*(x::real) = - p + 2*r | 2*x = -p - 2*r" - by (sos csdp) + by sos end diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/ex/SOS_Cert.thy --- a/src/HOL/ex/SOS_Cert.thy Wed Oct 08 10:22:00 2014 +0200 +++ b/src/HOL/ex/SOS_Cert.thy Wed Oct 08 18:10:17 2014 +0200 @@ -10,121 +10,121 @@ begin lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \ a < 0" - by (sos_cert "((R<1 + (((A<1 * R<1) * (R<2 * [1]^2)) + (((A<0 * R<1) * (R<3 * [1]^2)) + ((A<=0 * R<1) * (R<14 * [1]^2))))))") + by (sos "((R<1 + (((A<1 * R<1) * (R<2 * [1]^2)) + (((A<0 * R<1) * (R<3 * [1]^2)) + ((A<=0 * R<1) * (R<14 * [1]^2))))))") lemma "a1 >= 0 & a2 >= 0 \ (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \ (a1 * b1 + a2 * b2 = 0) --> a1 * a2 - b1 * b2 >= (0::real)" - by (sos_cert "(((A<0 * R<1) + (([~1/2*a1*b2 + ~1/2*a2*b1] * A=0) + (([~1/2*a1*a2 + 1/2*b1*b2] * A=1) + (((A<0 * R<1) * ((R<1/2 * [b2]^2) + (R<1/2 * [b1]^2))) + ((A<=0 * (A<=1 * R<1)) * ((R<1/2 * [b2]^2) + ((R<1/2 * [b1]^2) + ((R<1/2 * [a2]^2) + (R<1/2 * [a1]^2))))))))))") + by (sos "(((A<0 * R<1) + (([~1/2*a1*b2 + ~1/2*a2*b1] * A=0) + (([~1/2*a1*a2 + 1/2*b1*b2] * A=1) + (((A<0 * R<1) * ((R<1/2 * [b2]^2) + (R<1/2 * [b1]^2))) + ((A<=0 * (A<=1 * R<1)) * ((R<1/2 * [b2]^2) + ((R<1/2 * [b1]^2) + ((R<1/2 * [a2]^2) + (R<1/2 * [a1]^2))))))))))") lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x --> a < 0" - by (sos_cert "((R<1 + (((A<1 * R<1) * (R<2 * [1]^2)) + (((A<0 * R<1) * (R<3 * [1]^2)) + ((A<=0 * R<1) * (R<14 * [1]^2))))))") + by (sos "((R<1 + (((A<1 * R<1) * (R<2 * [1]^2)) + (((A<0 * R<1) * (R<3 * [1]^2)) + ((A<=0 * R<1) * (R<14 * [1]^2))))))") lemma "(0::real) <= x & x <= 1 & 0 <= y & y <= 1 --> x^2 + y^2 < 1 |(x - 1)^2 + y^2 < 1 | x^2 + (y - 1)^2 < 1 | (x - 1)^2 + (y - 1)^2 < 1" - by (sos_cert "((R<1 + (((A<=3 * (A<=4 * R<1)) * (R<1 * [1]^2)) + (((A<=2 * (A<=7 * R<1)) * (R<1 * [1]^2)) + (((A<=1 * (A<=6 * R<1)) * (R<1 * [1]^2)) + ((A<=0 * (A<=5 * R<1)) * (R<1 * [1]^2)))))))") + by (sos "((R<1 + (((A<=3 * (A<=4 * R<1)) * (R<1 * [1]^2)) + (((A<=2 * (A<=7 * R<1)) * (R<1 * [1]^2)) + (((A<=1 * (A<=6 * R<1)) * (R<1 * [1]^2)) + ((A<=0 * (A<=5 * R<1)) * (R<1 * [1]^2)))))))") lemma "(0::real) <= x & 0 <= y & 0 <= z & x + y + z <= 3 --> x * y + x * z + y * z >= 3 * x * y * z" - by (sos_cert "(((A<0 * R<1) + (((A<0 * R<1) * (R<1/2 * [1]^2)) + (((A<=2 * R<1) * (R<1/2 * [~1*x + y]^2)) + (((A<=1 * R<1) * (R<1/2 * [~1*x + z]^2)) + (((A<=1 * (A<=2 * (A<=3 * R<1))) * (R<1/2 * [1]^2)) + (((A<=0 * R<1) * (R<1/2 * [~1*y + z]^2)) + (((A<=0 * (A<=2 * (A<=3 * R<1))) * (R<1/2 * [1]^2)) + ((A<=0 * (A<=1 * (A<=3 * R<1))) * (R<1/2 * [1]^2))))))))))") + by (sos "(((A<0 * R<1) + (((A<0 * R<1) * (R<1/2 * [1]^2)) + (((A<=2 * R<1) * (R<1/2 * [~1*x + y]^2)) + (((A<=1 * R<1) * (R<1/2 * [~1*x + z]^2)) + (((A<=1 * (A<=2 * (A<=3 * R<1))) * (R<1/2 * [1]^2)) + (((A<=0 * R<1) * (R<1/2 * [~1*y + z]^2)) + (((A<=0 * (A<=2 * (A<=3 * R<1))) * (R<1/2 * [1]^2)) + ((A<=0 * (A<=1 * (A<=3 * R<1))) * (R<1/2 * [1]^2))))))))))") lemma "((x::real)^2 + y^2 + z^2 = 1) --> (x + y + z)^2 <= 3" - by (sos_cert "(((A<0 * R<1) + (([~3] * A=0) + (R<1 * ((R<2 * [~1/2*x + ~1/2*y + z]^2) + (R<3/2 * [~1*x + y]^2))))))") + by (sos "(((A<0 * R<1) + (([~3] * A=0) + (R<1 * ((R<2 * [~1/2*x + ~1/2*y + z]^2) + (R<3/2 * [~1*x + y]^2))))))") lemma "(w^2 + x^2 + y^2 + z^2 = 1) --> (w + x + y + z)^2 <= (4::real)" - by (sos_cert "(((A<0 * R<1) + (([~4] * A=0) + (R<1 * ((R<3 * [~1/3*w + ~1/3*x + ~1/3*y + z]^2) + ((R<8/3 * [~1/2*w + ~1/2*x + y]^2) + (R<2 * [~1*w + x]^2)))))))") + by (sos "(((A<0 * R<1) + (([~4] * A=0) + (R<1 * ((R<3 * [~1/3*w + ~1/3*x + ~1/3*y + z]^2) + ((R<8/3 * [~1/2*w + ~1/2*x + y]^2) + (R<2 * [~1*w + x]^2)))))))") lemma "(x::real) >= 1 & y >= 1 --> x * y >= x + y - 1" - by (sos_cert "(((A<0 * R<1) + ((A<=0 * (A<=1 * R<1)) * (R<1 * [1]^2))))") + by (sos "(((A<0 * R<1) + ((A<=0 * (A<=1 * R<1)) * (R<1 * [1]^2))))") lemma "(x::real) > 1 & y > 1 --> x * y > x + y - 1" - by (sos_cert "((((A<0 * A<1) * R<1) + ((A<=0 * R<1) * (R<1 * [1]^2))))") + by (sos "((((A<0 * A<1) * R<1) + ((A<=0 * R<1) * (R<1 * [1]^2))))") lemma "abs(x) <= 1 --> abs(64 * x^7 - 112 * x^5 + 56 * x^3 - 7 * x) <= (1::real)" - by (sos_cert "((((A<0 * R<1) + ((A<=1 * R<1) * (R<1 * [~8*x^3 + ~4*x^2 + 4*x + 1]^2)))) & ((((A<0 * A<1) * R<1) + ((A<=1 * (A<0 * R<1)) * (R<1 * [8*x^3 + ~4*x^2 + ~4*x + 1]^2)))))") + by (sos "((((A<0 * R<1) + ((A<=1 * R<1) * (R<1 * [~8*x^3 + ~4*x^2 + 4*x + 1]^2)))) & ((((A<0 * A<1) * R<1) + ((A<=1 * (A<0 * R<1)) * (R<1 * [8*x^3 + ~4*x^2 + ~4*x + 1]^2)))))") text \One component of denominator in dodecahedral example.\ lemma "2 <= x & x <= 125841 / 50000 & 2 <= y & y <= 125841 / 50000 & 2 <= z & z <= 125841 / 50000 --> 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z) >= (0::real)" - by (sos_cert "(((A<0 * R<1) + ((R<1 * ((R<5749028157/5000000000 * [~25000/222477*x + ~25000/222477*y + ~25000/222477*z + 1]^2) + ((R<864067/1779816 * [419113/864067*x + 419113/864067*y + z]^2) + ((R<320795/864067 * [419113/1283180*x + y]^2) + (R<1702293/5132720 * [x]^2))))) + (((A<=4 * (A<=5 * R<1)) * (R<3/2 * [1]^2)) + (((A<=3 * (A<=5 * R<1)) * (R<1/2 * [1]^2)) + (((A<=2 * (A<=4 * R<1)) * (R<1 * [1]^2)) + (((A<=2 * (A<=3 * R<1)) * (R<3/2 * [1]^2)) + (((A<=1 * (A<=5 * R<1)) * (R<1/2 * [1]^2)) + (((A<=1 * (A<=3 * R<1)) * (R<1/2 * [1]^2)) + (((A<=0 * (A<=4 * R<1)) * (R<1 * [1]^2)) + (((A<=0 * (A<=2 * R<1)) * (R<1 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<3/2 * [1]^2)))))))))))))") + by (sos "(((A<0 * R<1) + ((R<1 * ((R<5749028157/5000000000 * [~25000/222477*x + ~25000/222477*y + ~25000/222477*z + 1]^2) + ((R<864067/1779816 * [419113/864067*x + 419113/864067*y + z]^2) + ((R<320795/864067 * [419113/1283180*x + y]^2) + (R<1702293/5132720 * [x]^2))))) + (((A<=4 * (A<=5 * R<1)) * (R<3/2 * [1]^2)) + (((A<=3 * (A<=5 * R<1)) * (R<1/2 * [1]^2)) + (((A<=2 * (A<=4 * R<1)) * (R<1 * [1]^2)) + (((A<=2 * (A<=3 * R<1)) * (R<3/2 * [1]^2)) + (((A<=1 * (A<=5 * R<1)) * (R<1/2 * [1]^2)) + (((A<=1 * (A<=3 * R<1)) * (R<1/2 * [1]^2)) + (((A<=0 * (A<=4 * R<1)) * (R<1 * [1]^2)) + (((A<=0 * (A<=2 * R<1)) * (R<1 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<3/2 * [1]^2)))))))))))))") text \Over a larger but simpler interval.\ lemma "(2::real) <= x & x <= 4 & 2 <= y & y <= 4 & 2 <= z & z <= 4 --> 0 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" - by (sos_cert "((R<1 + ((R<1 * ((R<1 * [~1/6*x + ~1/6*y + ~1/6*z + 1]^2) + ((R<1/18 * [~1/2*x + ~1/2*y + z]^2) + (R<1/24 * [~1*x + y]^2)))) + (((A<0 * R<1) * (R<1/12 * [1]^2)) + (((A<=4 * (A<=5 * R<1)) * (R<1/6 * [1]^2)) + (((A<=2 * (A<=4 * R<1)) * (R<1/6 * [1]^2)) + (((A<=2 * (A<=3 * R<1)) * (R<1/6 * [1]^2)) + (((A<=0 * (A<=4 * R<1)) * (R<1/6 * [1]^2)) + (((A<=0 * (A<=2 * R<1)) * (R<1/6 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<1/6 * [1]^2)))))))))))") + by (sos "((R<1 + ((R<1 * ((R<1 * [~1/6*x + ~1/6*y + ~1/6*z + 1]^2) + ((R<1/18 * [~1/2*x + ~1/2*y + z]^2) + (R<1/24 * [~1*x + y]^2)))) + (((A<0 * R<1) * (R<1/12 * [1]^2)) + (((A<=4 * (A<=5 * R<1)) * (R<1/6 * [1]^2)) + (((A<=2 * (A<=4 * R<1)) * (R<1/6 * [1]^2)) + (((A<=2 * (A<=3 * R<1)) * (R<1/6 * [1]^2)) + (((A<=0 * (A<=4 * R<1)) * (R<1/6 * [1]^2)) + (((A<=0 * (A<=2 * R<1)) * (R<1/6 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<1/6 * [1]^2)))))))))))") text \We can do 12. I think 12 is a sharp bound; see PP's certificate.\ lemma "2 <= (x::real) & x <= 4 & 2 <= y & y <= 4 & 2 <= z & z <= 4 --> 12 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" - by (sos_cert "(((A<0 * R<1) + (((A<=4 * R<1) * (R<2/3 * [1]^2)) + (((A<=4 * (A<=5 * R<1)) * (R<1 * [1]^2)) + (((A<=3 * (A<=4 * R<1)) * (R<1/3 * [1]^2)) + (((A<=2 * R<1) * (R<2/3 * [1]^2)) + (((A<=2 * (A<=5 * R<1)) * (R<1/3 * [1]^2)) + (((A<=2 * (A<=4 * R<1)) * (R<8/3 * [1]^2)) + (((A<=2 * (A<=3 * R<1)) * (R<1 * [1]^2)) + (((A<=1 * (A<=4 * R<1)) * (R<1/3 * [1]^2)) + (((A<=1 * (A<=2 * R<1)) * (R<1/3 * [1]^2)) + (((A<=0 * R<1) * (R<2/3 * [1]^2)) + (((A<=0 * (A<=5 * R<1)) * (R<1/3 * [1]^2)) + (((A<=0 * (A<=4 * R<1)) * (R<8/3 * [1]^2)) + (((A<=0 * (A<=3 * R<1)) * (R<1/3 * [1]^2)) + (((A<=0 * (A<=2 * R<1)) * (R<8/3 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<1 * [1]^2))))))))))))))))))") + by (sos "(((A<0 * R<1) + (((A<=4 * R<1) * (R<2/3 * [1]^2)) + (((A<=4 * (A<=5 * R<1)) * (R<1 * [1]^2)) + (((A<=3 * (A<=4 * R<1)) * (R<1/3 * [1]^2)) + (((A<=2 * R<1) * (R<2/3 * [1]^2)) + (((A<=2 * (A<=5 * R<1)) * (R<1/3 * [1]^2)) + (((A<=2 * (A<=4 * R<1)) * (R<8/3 * [1]^2)) + (((A<=2 * (A<=3 * R<1)) * (R<1 * [1]^2)) + (((A<=1 * (A<=4 * R<1)) * (R<1/3 * [1]^2)) + (((A<=1 * (A<=2 * R<1)) * (R<1/3 * [1]^2)) + (((A<=0 * R<1) * (R<2/3 * [1]^2)) + (((A<=0 * (A<=5 * R<1)) * (R<1/3 * [1]^2)) + (((A<=0 * (A<=4 * R<1)) * (R<8/3 * [1]^2)) + (((A<=0 * (A<=3 * R<1)) * (R<1/3 * [1]^2)) + (((A<=0 * (A<=2 * R<1)) * (R<8/3 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<1 * [1]^2))))))))))))))))))") text \Inequality from sci.math (see "Leon-Sotelo, por favor").\ lemma "0 <= (x::real) & 0 <= y & (x * y = 1) --> x + y <= x^2 + y^2" - by (sos_cert "(((A<0 * R<1) + (([1] * A=0) + (R<1 * ((R<1 * [~1/2*x + ~1/2*y + 1]^2) + (R<3/4 * [~1*x + y]^2))))))") + by (sos "(((A<0 * R<1) + (([1] * A=0) + (R<1 * ((R<1 * [~1/2*x + ~1/2*y + 1]^2) + (R<3/4 * [~1*x + y]^2))))))") lemma "0 <= (x::real) & 0 <= y & (x * y = 1) --> x * y * (x + y) <= x^2 + y^2" - by (sos_cert "(((A<0 * R<1) + (([~1*x + ~1*y + 1] * A=0) + (R<1 * ((R<1 * [~1/2*x + ~1/2*y + 1]^2) + (R<3/4 * [~1*x + y]^2))))))") + by (sos "(((A<0 * R<1) + (([~1*x + ~1*y + 1] * A=0) + (R<1 * ((R<1 * [~1/2*x + ~1/2*y + 1]^2) + (R<3/4 * [~1*x + y]^2))))))") lemma "0 <= (x::real) & 0 <= y --> x * y * (x + y)^2 <= (x^2 + y^2)^2" - by (sos_cert "(((A<0 * R<1) + (R<1 * ((R<1 * [~1/2*x^2 + y^2 + ~1/2*x*y]^2) + (R<3/4 * [~1*x^2 + x*y]^2)))))") + by (sos "(((A<0 * R<1) + (R<1 * ((R<1 * [~1/2*x^2 + y^2 + ~1/2*x*y]^2) + (R<3/4 * [~1*x^2 + x*y]^2)))))") lemma "(0::real) <= a & 0 <= b & 0 <= c & c * (2 * a + b)^3/ 27 <= x \ c * a^2 * b <= x" - by (sos_cert "(((A<0 * R<1) + (((A<=3 * R<1) * (R<1 * [1]^2)) + (((A<=1 * (A<=2 * R<1)) * (R<1/27 * [~1*a + b]^2)) + ((A<=0 * (A<=2 * R<1)) * (R<8/27 * [~1*a + b]^2))))))") + by (sos "(((A<0 * R<1) + (((A<=3 * R<1) * (R<1 * [1]^2)) + (((A<=1 * (A<=2 * R<1)) * (R<1/27 * [~1*a + b]^2)) + ((A<=0 * (A<=2 * R<1)) * (R<8/27 * [~1*a + b]^2))))))") lemma "(0::real) < x --> 0 < 1 + x + x^2" - by (sos_cert "((R<1 + ((R<1 * (R<1 * [x]^2)) + (((A<0 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))") + by (sos "((R<1 + ((R<1 * (R<1 * [x]^2)) + (((A<0 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))") lemma "(0::real) <= x --> 0 < 1 + x + x^2" - by (sos_cert "((R<1 + ((R<1 * (R<1 * [x]^2)) + (((A<=1 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))") + by (sos "((R<1 + ((R<1 * (R<1 * [x]^2)) + (((A<=1 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))") lemma "(0::real) < 1 + x^2" - by (sos_cert "((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2)))))") + by (sos "((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2)))))") lemma "(0::real) <= 1 + 2 * x + x^2" - by (sos_cert "(((A<0 * R<1) + (R<1 * (R<1 * [x + 1]^2))))") + by (sos "(((A<0 * R<1) + (R<1 * (R<1 * [x + 1]^2))))") lemma "(0::real) < 1 + abs x" - by (sos_cert "((R<1 + (((A<=1 * R<1) * (R<1/2 * [1]^2)) + ((A<=0 * R<1) * (R<1/2 * [1]^2)))))") + by (sos "((R<1 + (((A<=1 * R<1) * (R<1/2 * [1]^2)) + ((A<=0 * R<1) * (R<1/2 * [1]^2)))))") lemma "(0::real) < 1 + (1 + x)^2 * (abs x)" - by (sos_cert "(((R<1 + (((A<=1 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [x + 1]^2))))) & ((R<1 + (((A<0 * R<1) * (R<1 * [x + 1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))") + by (sos "(((R<1 + (((A<=1 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [x + 1]^2))))) & ((R<1 + (((A<0 * R<1) * (R<1 * [x + 1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))") lemma "abs ((1::real) + x^2) = (1::real) + x^2" - by (sos_cert "(() & (((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<1 * R<1) * (R<1/2 * [1]^2))))) & ((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<0 * R<1) * (R<1 * [1]^2)))))))") + by (sos "(() & (((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<1 * R<1) * (R<1/2 * [1]^2))))) & ((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<0 * R<1) * (R<1 * [1]^2)))))))") lemma "(3::real) * x + 7 * a < 4 \ 3 < 2 * x \ a < 0" - by (sos_cert "((R<1 + (((A<1 * R<1) * (R<2 * [1]^2)) + (((A<0 * R<1) * (R<3 * [1]^2)) + ((A<=0 * R<1) * (R<14 * [1]^2))))))") + by (sos "((R<1 + (((A<1 * R<1) * (R<2 * [1]^2)) + (((A<0 * R<1) * (R<3 * [1]^2)) + ((A<=0 * R<1) * (R<14 * [1]^2))))))") lemma "(0::real) < x --> 1 < y --> y * x <= z --> x < z" - by (sos_cert "((((A<0 * A<1) * R<1) + (((A<=1 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2)))))") + by (sos "((((A<0 * A<1) * R<1) + (((A<=1 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2)))))") lemma "(1::real) < x --> x^2 < y --> 1 < y" - by (sos_cert "((((A<0 * A<1) * R<1) + ((R<1 * ((R<1/10 * [~2*x + y + 1]^2) + (R<1/10 * [~1*x + y]^2))) + (((A<1 * R<1) * (R<1/2 * [1]^2)) + (((A<0 * R<1) * (R<1 * [x]^2)) + (((A<=0 * R<1) * ((R<1/10 * [x + 1]^2) + (R<1/10 * [x]^2))) + (((A<=0 * (A<1 * R<1)) * (R<1/5 * [1]^2)) + ((A<=0 * (A<0 * R<1)) * (R<1/5 * [1]^2)))))))))") + by (sos "((((A<0 * A<1) * R<1) + ((R<1 * ((R<1/10 * [~2*x + y + 1]^2) + (R<1/10 * [~1*x + y]^2))) + (((A<1 * R<1) * (R<1/2 * [1]^2)) + (((A<0 * R<1) * (R<1 * [x]^2)) + (((A<=0 * R<1) * ((R<1/10 * [x + 1]^2) + (R<1/10 * [x]^2))) + (((A<=0 * (A<1 * R<1)) * (R<1/5 * [1]^2)) + ((A<=0 * (A<0 * R<1)) * (R<1/5 * [1]^2)))))))))") lemma "(b::real)^2 < 4 * a * c --> ~(a * x^2 + b * x + c = 0)" - by (sos_cert "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))") + by (sos "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))") lemma "(b::real)^2 < 4 * a * c --> ~(a * x^2 + b * x + c = 0)" - by (sos_cert "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))") + by (sos "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))") lemma "((a::real) * x^2 + b * x + c = 0) --> b^2 >= 4 * a * c" - by (sos_cert "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))") + by (sos "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))") lemma "(0::real) <= b & 0 <= c & 0 <= x & 0 <= y & (x^2 = c) & (y^2 = a^2 * c + b) --> a * c <= y * x" - by (sos_cert "(((A<0 * (A<0 * R<1)) + (((A<=2 * (A<=3 * (A<0 * R<1))) * (R<2 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<1 * [1]^2)))))") + by (sos "(((A<0 * (A<0 * R<1)) + (((A<=2 * (A<=3 * (A<0 * R<1))) * (R<2 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<1 * [1]^2)))))") lemma "abs(x - z) <= e & abs(y - z) <= e & 0 <= u & 0 <= v & (u + v = 1) --> abs((u * x + v * y) - z) <= (e::real)" - by (sos_cert "((((A<0 * R<1) + (((A<=3 * (A<=6 * R<1)) * (R<1 * [1]^2)) + ((A<=1 * (A<=5 * R<1)) * (R<1 * [1]^2))))) & ((((A<0 * A<1) * R<1) + (((A<=3 * (A<=5 * (A<0 * R<1))) * (R<1 * [1]^2)) + ((A<=1 * (A<=4 * (A<0 * R<1))) * (R<1 * [1]^2))))))") + by (sos "((((A<0 * R<1) + (((A<=3 * (A<=6 * R<1)) * (R<1 * [1]^2)) + ((A<=1 * (A<=5 * R<1)) * (R<1 * [1]^2))))) & ((((A<0 * A<1) * R<1) + (((A<=3 * (A<=5 * (A<0 * R<1))) * (R<1 * [1]^2)) + ((A<=1 * (A<=4 * (A<0 * R<1))) * (R<1 * [1]^2))))))") (* lemma "((x::real) - y - 2 * x^4 = 0) & 0 <= x & x <= 2 & 0 <= y & y <= 3 --> y^2 - 7 * y - 12 * x + 17 >= 0" by sos *) (* Too hard?*) lemma "(0::real) <= x --> (1 + x + x^2)/(1 + x^2) <= 1 + x" - by (sos_cert "(((((A<0 * A<1) * R<1) + ((A<=0 * (A<0 * R<1)) * (R<1 * [x]^2)))) & ((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<0 * R<1) * (R<1 * [1]^2))))))") + by (sos "(((((A<0 * A<1) * R<1) + ((A<=0 * (A<0 * R<1)) * (R<1 * [x]^2)))) & ((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<0 * R<1) * (R<1 * [1]^2))))))") lemma "(0::real) <= x --> 1 - x <= 1 / (1 + x + x^2)" - by (sos_cert "(((R<1 + (([~4/3] * A=0) + ((R<1 * ((R<1/3 * [3/2*x + 1]^2) + (R<7/12 * [x]^2))) + ((A<=0 * R<1) * (R<1/3 * [1]^2)))))) & (((((A<0 * A<1) * R<1) + ((A<=0 * (A<0 * R<1)) * (R<1 * [x]^2)))) & ((R<1 + ((R<1 * (R<1 * [x]^2)) + (((A<0 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))))") + by (sos "(((R<1 + (([~4/3] * A=0) + ((R<1 * ((R<1/3 * [3/2*x + 1]^2) + (R<7/12 * [x]^2))) + ((A<=0 * R<1) * (R<1/3 * [1]^2)))))) & (((((A<0 * A<1) * R<1) + ((A<=0 * (A<0 * R<1)) * (R<1 * [x]^2)))) & ((R<1 + ((R<1 * (R<1 * [x]^2)) + (((A<0 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))))") lemma "(x::real) <= 1 / 2 --> - x - 2 * x^2 <= - x / (1 - x)" - by (sos_cert "((((A<0 * A<1) * R<1) + ((A<=0 * (A<0 * R<1)) * (R<1 * [x]^2))))") + by (sos "((((A<0 * A<1) * R<1) + ((A<=0 * (A<0 * R<1)) * (R<1 * [x]^2))))") lemma "4*r^2 = p^2 - 4*q & r >= (0::real) & x^2 + p*x + q = 0 --> 2*(x::real) = - p + 2*r | 2*x = -p - 2*r" - by (sos_cert "((((((A<0 * A<1) * R<1) + ([~4] * A=0))) & ((((A<0 * A<1) * R<1) + ([4] * A=0)))) & (((((A<0 * A<1) * R<1) + ([4] * A=0))) & ((((A<0 * A<1) * R<1) + ([~4] * A=0)))))") + by (sos "((((((A<0 * A<1) * R<1) + ([~4] * A=0))) & ((((A<0 * A<1) * R<1) + ([4] * A=0)))) & (((((A<0 * A<1) * R<1) + ([4] * A=0))) & ((((A<0 * A<1) * R<1) + ([~4] * A=0)))))") end diff -r 1329679abb2d -r 9b33fe5b60f3 src/HOL/ex/SOS_Remote.thy --- a/src/HOL/ex/SOS_Remote.thy Wed Oct 08 10:22:00 2014 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,37 +0,0 @@ -(* Title: HOL/ex/SOS_Remote.thy - Author: Amine Chaieb, University of Cambridge - Author: Philipp Meyer, TU Muenchen - -Examples for Sum_of_Squares: remote CSDP server. -*) - -theory SOS_Remote -imports "~~/src/HOL/Library/Sum_of_Squares" -begin - -lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \ a < 0" - by (sos remote_csdp) - -lemma "a1 >= 0 & a2 >= 0 \ (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \ (a1 * b1 + a2 * b2 = 0) --> a1 * a2 - b1 * b2 >= (0::real)" - by (sos remote_csdp) - -lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x --> a < 0" - by (sos remote_csdp) - -lemma "(0::real) <= x & x <= 1 & 0 <= y & y <= 1 --> x^2 + y^2 < 1 |(x - 1)^2 + y^2 < 1 | x^2 + (y - 1)^2 < 1 | (x - 1)^2 + (y - 1)^2 < 1" - by (sos remote_csdp) - -lemma "(0::real) <= x & 0 <= y & 0 <= z & x + y + z <= 3 --> x * y + x * z + y * z >= 3 * x * y * z" - by (sos remote_csdp) - -lemma "((x::real)^2 + y^2 + z^2 = 1) --> (x + y + z)^2 <= 3" - by (sos remote_csdp) - -lemma "(w^2 + x^2 + y^2 + z^2 = 1) --> (w + x + y + z)^2 <= (4::real)" - by (sos remote_csdp) - -lemma "(x::real) >= 1 & y >= 1 --> x * y >= x + y - 1" - by (sos remote_csdp) - -end - diff -r 1329679abb2d -r 9b33fe5b60f3 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/Pure/Isar/code.ML Wed Oct 08 18:10:17 2014 +0200 @@ -545,7 +545,7 @@ else bad_thm ("Projection mismatch: " ^ quote rep_const ^ " vs. " ^ quote rep'); val _ = check_eqn thy { allow_nonlinear = false, allow_consts = false, allow_pats = false } thm (lhs, rhs); - val _ = if forall2 (fn T => fn (_, sort) => Sign.of_sort thy (T, sort)) Ts vs' then () + val _ = if ListPair.all (fn (T, (_, sort)) => Sign.of_sort thy (T, sort)) (Ts, vs') then () else error ("Type arguments do not satisfy sort constraints of abstype certificate."); in (thm, tyco) end; diff -r 1329679abb2d -r 9b33fe5b60f3 src/Pure/ML/ml_antiquotations.ML --- a/src/Pure/ML/ml_antiquotations.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/Pure/ML/ml_antiquotations.ML Wed Oct 08 18:10:17 2014 +0200 @@ -7,6 +7,41 @@ structure ML_Antiquotations: sig end = struct +(* ML support *) + +val _ = Theory.setup + (ML_Antiquotation.inline @{binding assert} + (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #> + + ML_Antiquotation.inline @{binding make_string} (Scan.succeed ml_make_string) #> + + ML_Antiquotation.declaration @{binding print} + (Scan.lift (Scan.optional Args.name "Output.writeln")) + (fn src => fn output => fn ctxt => + let + val (_, pos) = Token.name_of_src src; + val (a, ctxt') = ML_Antiquotation.variant "output" ctxt; + val env = + "val " ^ a ^ ": string -> unit =\n\ + \ (" ^ output ^ ") o (fn s => s ^ Position.here (" ^ + ML_Syntax.print_position pos ^ "));\n"; + val body = + "(fn x => (Isabelle." ^ a ^ " (" ^ ml_make_string ^ " x); x))"; + in (K (env, body), ctxt') end)); + + +(* embedded source *) + +val _ = Theory.setup + (ML_Antiquotation.value @{binding source} + (Scan.lift Args.text_source_position >> (fn {delimited, text, pos} => + "{delimited = " ^ Bool.toString delimited ^ + ", text = " ^ ML_Syntax.print_string text ^ + ", pos = " ^ ML_Syntax.print_position pos ^ "}"))); + + +(* formal entities *) + val _ = Theory.setup (ML_Antiquotation.value @{binding system_option} (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) => @@ -52,39 +87,6 @@ ML_Syntax.atomic (ML_Syntax.print_term t)))); -(* embedded source *) - -val _ = Theory.setup - (ML_Antiquotation.value @{binding source} - (Scan.lift Args.text_source_position >> (fn {delimited, text, pos} => - "{delimited = " ^ Bool.toString delimited ^ - ", text = " ^ ML_Syntax.print_string text ^ - ", pos = " ^ ML_Syntax.print_position pos ^ "}"))); - - -(* ML support *) - -val _ = Theory.setup - (ML_Antiquotation.inline @{binding assert} - (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #> - - ML_Antiquotation.inline @{binding make_string} (Scan.succeed ml_make_string) #> - - ML_Antiquotation.declaration @{binding print} - (Scan.lift (Scan.optional Args.name "Output.writeln")) - (fn src => fn output => fn ctxt => - let - val (_, pos) = Token.name_of_src src; - val (a, ctxt') = ML_Antiquotation.variant "output" ctxt; - val env = - "val " ^ a ^ ": string -> unit =\n\ - \ (" ^ output ^ ") o (fn s => s ^ Position.here (" ^ - ML_Syntax.print_position pos ^ "));\n"; - val body = - "(fn x => (Isabelle." ^ a ^ " (" ^ ml_make_string ^ " x); x))"; - in (K (env, body), ctxt') end)); - - (* type classes *) fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) => @@ -165,6 +167,70 @@ in ML_Syntax.atomic (ML_Syntax.print_term const) end))); +(* basic combinators *) + +local + +val parameter = Parse.position Parse.nat >> (fn (n, pos) => + if n > 1 then n else error ("Bad parameter: " ^ string_of_int n ^ Position.here pos)); + +fun indices n = map string_of_int (1 upto n); + +fun empty n = replicate_string n " []"; +fun dummy n = replicate_string n " _"; +fun vars x n = implode (map (fn a => " " ^ x ^ a) (indices n)); +fun cons n = implode (map (fn a => " (x" ^ a ^ " :: xs" ^ a ^ ")") (indices n)); + +val tuple = enclose "(" ")" o commas; +fun tuple_empty n = tuple (replicate n "[]"); +fun tuple_vars x n = tuple (map (fn a => x ^ a) (indices n)); +fun tuple_cons n = "(" ^ tuple_vars "x" n ^ " :: xs)" +fun cons_tuple n = tuple (map (fn a => "x" ^ a ^ " :: xs" ^ a) (indices n)); + +in + +val _ = Theory.setup + (ML_Antiquotation.value @{binding map} + (Scan.lift parameter >> (fn n => + "fn f =>\n\ + \ let\n\ + \ fun map _" ^ empty n ^ " = []\n\ + \ | map f" ^ cons n ^ " = f" ^ vars "x" n ^ " :: map f" ^ vars "xs" n ^ "\n\ + \ | map _" ^ dummy n ^ " = raise ListPair.UnequalLengths\n" ^ + " in map f end")) #> + ML_Antiquotation.value @{binding fold} + (Scan.lift parameter >> (fn n => + "fn f =>\n\ + \ let\n\ + \ fun fold _" ^ empty n ^ " a = a\n\ + \ | fold f" ^ cons n ^ " a = fold f" ^ vars "xs" n ^ " (f" ^ vars "x" n ^ " a)\n\ + \ | fold _" ^ dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^ + " in fold f end")) #> + ML_Antiquotation.value @{binding fold_map} + (Scan.lift parameter >> (fn n => + "fn f =>\n\ + \ let\n\ + \ fun fold_map _" ^ empty n ^ " a = ([], a)\n\ + \ | fold_map f" ^ cons n ^ " a =\n\ + \ let\n\ + \ val (x, a') = f" ^ vars "x" n ^ " a\n\ + \ val (xs, a'') = fold_map f" ^ vars "xs" n ^ " a'\n\ + \ in (x :: xs, a'') end\n\ + \ | fold_map _" ^ dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^ + " in fold_map f end")) #> + ML_Antiquotation.value @{binding split_list} + (Scan.lift parameter >> (fn n => + "fn list =>\n\ + \ let\n\ + \ fun split_list [] =" ^ tuple_empty n ^ "\n\ + \ | split_list" ^ tuple_cons n ^ " =\n\ + \ let val" ^ tuple_vars "xs" n ^ " = split_list xs\n\ + \ in " ^ cons_tuple n ^ "end\n\ + \ in split_list list end"))) + +end; + + (* outer syntax *) fun with_keyword f = diff -r 1329679abb2d -r 9b33fe5b60f3 src/Pure/library.ML --- a/src/Pure/library.ML Wed Oct 08 10:22:00 2014 +0200 +++ b/src/Pure/library.ML Wed Oct 08 18:10:17 2014 +0200 @@ -101,8 +101,6 @@ val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c - val fold_rev2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c - val forall2: ('a -> 'b -> bool) -> 'a list -> 'b list -> bool val map_split: ('a -> 'b * 'c) -> 'a list -> 'b list * 'c list val zip_options: 'a list -> 'b option list -> ('a * 'b) list val ~~ : 'a list * 'b list -> ('a * 'b) list @@ -531,19 +529,11 @@ | map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys | map2 _ _ _ = raise ListPair.UnequalLengths; -fun fold2 f [] [] z = z +fun fold2 _ [] [] z = z | fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z) - | fold2 f _ _ _ = raise ListPair.UnequalLengths; + | fold2 _ _ _ _ = raise ListPair.UnequalLengths; -fun fold_rev2 f [] [] z = z - | fold_rev2 f (x :: xs) (y :: ys) z = f x y (fold_rev2 f xs ys z) - | fold_rev2 f _ _ _ = raise ListPair.UnequalLengths; - -fun forall2 P [] [] = true - | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys - | forall2 P _ _ = raise ListPair.UnequalLengths; - -fun map_split f [] = ([], []) +fun map_split _ [] = ([], []) | map_split f (x :: xs) = let val (y, w) = f x;