--- 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 ***
--- 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
--- 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"
-
--- 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 <input_filename> <output_filename>\n")
- sys.exit(19)
-
-xml_pre = "<document>\n<category>sdp</category>\n<solver>csdp</solver>\n<inputMethod>SPARSE_SDPA</inputMethod>\n<dat><![CDATA["
-xml_post = "]]></dat>\n</document>\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)
-
--- 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
+
--- 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
--- 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
--- 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 = _} =>
--- 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)
--- 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
--- 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]
--- 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')
--- 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'),
--- 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 =
--- 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)
--- 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);
--- 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
--- 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
--- 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;
--- 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: (\<forall>x \<in> Bi. si \<in> 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)
--- 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;
--- 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,
--- 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: (\<forall>x \<in> Fi_in UNIV .. UNIV B1 ... Bn. si x \<in> 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
--- 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]
--- 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;
--- 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
--- 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
--- 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]]},
--- 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 **)
--- 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
--- 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));
--- 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;
--- 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 =
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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] =
--- 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)
--- 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
--- 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 ()
--- 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
--- 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
--- 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))
--- 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"
--- 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
--- 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 \<Longrightarrow> a < 0"
- by (sos csdp)
+ by sos
lemma "a1 >= 0 & a2 >= 0 \<and> (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \<and> (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 \<open>One component of denominator in dodecahedral example.\<close>
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 \<open>Over a larger but simpler interval.\<close>
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 \<open>We can do 12. I think 12 is a sharp bound; see PP's certificate.\<close>
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 \<open>Inequality from sci.math (see "Leon-Sotelo, por favor").\<close>
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 \<longrightarrow> 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 \<and> 3 < 2 * x \<longrightarrow> 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
--- 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 \<Longrightarrow> 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 \<and> (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \<and> (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 \<open>One component of denominator in dodecahedral example.\<close>
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 \<open>Over a larger but simpler interval.\<close>
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 \<open>We can do 12. I think 12 is a sharp bound; see PP's certificate.\<close>
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 \<open>Inequality from sci.math (see "Leon-Sotelo, por favor").\<close>
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 \<longrightarrow> 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 \<and> 3 < 2 * x \<longrightarrow> 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
--- 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 \<Longrightarrow> a < 0"
- by (sos remote_csdp)
-
-lemma "a1 >= 0 & a2 >= 0 \<and> (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \<and> (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
-
--- 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;
--- 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 =
--- 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;