# HG changeset patch # User haftmann # Date 1257578292 -3600 # Node ID 31872dd275c89853d680f77ea426c9f30c7c45a6 # Parent 39c9d0785911b81235c9ff53f2ca5b158431db5f# Parent 22e5725be1f303e8eee9dfa4c8a9d45ff961338f merged diff -r 22e5725be1f3 -r 31872dd275c8 NEWS --- a/NEWS Sat Nov 07 08:17:53 2009 +0100 +++ b/NEWS Sat Nov 07 08:18:12 2009 +0100 @@ -54,6 +54,8 @@ solvers using the oracle mechanism; for the SMT solver Z3, this method is proof-producing. Certificates are provided to avoid calling the external solvers solely for re-checking proofs. +Due to a remote SMT service there is no need for installing SMT +solvers locally. * New commands to load and prove verification conditions generated by the Boogie program verifier or derived systems @@ -227,6 +229,10 @@ * Maclauren.DERIV_tac and Maclauren.deriv_tac was removed, they are replaced by: (auto intro!: DERIV_intros). INCOMPATIBILITY. +* Renamed methods: + sizechange -> size_change + induct_scheme -> induction_schema + *** ML *** diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/Boogie/Tools/boogie_loader.ML --- a/src/HOL/Boogie/Tools/boogie_loader.ML Sat Nov 07 08:17:53 2009 +0100 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML Sat Nov 07 08:18:12 2009 +0100 @@ -293,8 +293,8 @@ fun read_int' s = (case read_int (explode s) of (i, []) => SOME i | _ => NONE) fun $$$ s = Scan.one (fn (_, Token s') => s = s' | _ => false) -val str = Scan.some (fn (_, Token s) => SOME s | _ => NONE) -val num = Scan.some (fn (_, Token s) => read_int' s | _ => NONE) +fun str st = Scan.some (fn (_, Token s) => SOME s | _ => NONE) st +fun num st = Scan.some (fn (_, Token s) => read_int' s | _ => NONE) st fun scan_line key scan = $$$ key |-- scan --| Scan.one (fn (_, Newline) => true | _ => false) diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/Code_Evaluation.thy --- a/src/HOL/Code_Evaluation.thy Sat Nov 07 08:17:53 2009 +0100 +++ b/src/HOL/Code_Evaluation.thy Sat Nov 07 08:18:12 2009 +0100 @@ -243,6 +243,26 @@ hide const dummy_term App valapp hide (open) const Const termify valtermify term_of term_of_num +subsection {* Tracing of generated and evaluated code *} + +definition tracing :: "String.literal => 'a => 'a" +where + [code del]: "tracing s x = x" + +ML {* +structure Code_Evaluation = +struct + +fun tracing s x = (Output.tracing s; x) + +end +*} + +code_const "tracing :: String.literal => 'a => 'a" + (Eval "Code'_Evaluation.tracing") + +hide (open) const tracing +code_reserved Eval Code_Evaluation subsection {* Evaluation setup *} diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/Decision_Procs/commutative_ring_tac.ML diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/FunDef.thy --- a/src/HOL/FunDef.thy Sat Nov 07 08:17:53 2009 +0100 +++ b/src/HOL/FunDef.thy Sat Nov 07 08:18:12 2009 +0100 @@ -22,7 +22,7 @@ ("Tools/Function/lexicographic_order.ML") ("Tools/Function/pat_completeness.ML") ("Tools/Function/fun.ML") - ("Tools/Function/induction_scheme.ML") + ("Tools/Function/induction_schema.ML") ("Tools/Function/termination.ML") ("Tools/Function/decompose.ML") ("Tools/Function/descent.ML") @@ -114,13 +114,13 @@ use "Tools/Function/function.ML" use "Tools/Function/pat_completeness.ML" use "Tools/Function/fun.ML" -use "Tools/Function/induction_scheme.ML" +use "Tools/Function/induction_schema.ML" setup {* Function.setup #> Pat_Completeness.setup #> Function_Fun.setup - #> Induction_Scheme.setup + #> Induction_Schema.setup *} subsection {* Measure Functions *} diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sat Nov 07 08:17:53 2009 +0100 +++ b/src/HOL/IsaMakefile Sat Nov 07 08:18:12 2009 +0100 @@ -180,7 +180,7 @@ Tools/Function/function_lib.ML \ Tools/Function/function.ML \ Tools/Function/fun.ML \ - Tools/Function/induction_scheme.ML \ + Tools/Function/induction_schema.ML \ Tools/Function/lexicographic_order.ML \ Tools/Function/measure_functions.ML \ Tools/Function/mutual.ML \ @@ -939,7 +939,7 @@ ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy \ ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \ ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \ - ex/Hilbert_Classical.thy ex/Induction_Scheme.thy \ + ex/Hilbert_Classical.thy ex/Induction_Schema.thy \ ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \ ex/Intuitionistic.thy ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \ ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \ diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/SMT/Examples/SMT_Examples.thy --- a/src/HOL/SMT/Examples/SMT_Examples.thy Sat Nov 07 08:17:53 2009 +0100 +++ b/src/HOL/SMT/Examples/SMT_Examples.thy Sat Nov 07 08:18:12 2009 +0100 @@ -549,7 +549,7 @@ section {* Bitvectors *} -locale bv +locale z3_bv_test begin text {* diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/SMT/SMT.thy --- a/src/HOL/SMT/SMT.thy Sat Nov 07 08:17:53 2009 +0100 +++ b/src/HOL/SMT/SMT.thy Sat Nov 07 08:18:12 2009 +0100 @@ -13,9 +13,59 @@ setup {* CVC3_Solver.setup #> Yices_Solver.setup *} -declare [[ smt_solver = z3, smt_timeout = 20 ]] + + +section {* Setup *} + +text {* +Without further ado, the SMT solvers CVC3 and Z3 are provided +remotely via an SMT server. For faster responses, the solver +environment variables CVC3_SOLVER, YICES_SOLVER, and Z3_SOLVER +need to point to the respective SMT solver executable. +*} + + + +section {* Available configuration options *} + +text {* Choose the SMT solver to be applied (one of cvc3, yices, or z3): *} + +declare [[ smt_solver = z3 ]] + +text {* Restrict the runtime of an SMT solver (in seconds): *} + +declare [[ smt_timeout = 20 ]] + + +subsection {* Z3-specific options *} + +text {* Enable proof reconstruction for Z3: *} + +declare [[ z3_proofs = false ]] + +text {* Pass extra command-line arguments to Z3 +to control its behaviour: *} + +declare [[ z3_options = "" ]] + + +subsection {* Special configuration options *} + +text {* +Trace the problem file, the result of the SMT solver and +further information: *} + +declare [[ smt_trace = false ]] + +text {* Unfold (some) definitions passed to the SMT solver: *} + declare [[ smt_unfold_defs = true ]] -declare [[ smt_trace = false, smt_keep = "", smt_cert = "" ]] -declare [[ z3_proofs = false, z3_options = "" ]] + +text {* +Produce or use certificates (to avoid repeated invocation of an +SMT solver again and again). The value is an absolute path +pointing to the problem file. See also the examples. *} + +declare [[ smt_keep = "", smt_cert = "" ]] end diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/SMT/Tools/cvc3_solver.ML --- a/src/HOL/SMT/Tools/cvc3_solver.ML Sat Nov 07 08:17:53 2009 +0100 +++ b/src/HOL/SMT/Tools/cvc3_solver.ML Sat Nov 07 08:18:12 2009 +0100 @@ -36,7 +36,7 @@ end fun smtlib_solver oracle _ = { - command = {env_var=env_var, remote_name=solver_name}, + command = {env_var=env_var, remote_name=SOME solver_name}, arguments = options, interface = SMTLIB_Interface.interface, reconstruct = oracle } diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/SMT/Tools/smt_solver.ML --- a/src/HOL/SMT/Tools/smt_solver.ML Sat Nov 07 08:17:53 2009 +0100 +++ b/src/HOL/SMT/Tools/smt_solver.ML Sat Nov 07 08:18:12 2009 +0100 @@ -18,7 +18,7 @@ recon: SMT_Translate.recon, assms: thm list option } type solver_config = { - command: {env_var: string, remote_name: string}, + command: {env_var: string, remote_name: string option}, arguments: string list, interface: interface, reconstruct: proof_data -> thm } @@ -69,7 +69,7 @@ assms: thm list option } type solver_config = { - command: {env_var: string, remote_name: string}, + command: {env_var: string, remote_name: string option}, arguments: string list, interface: interface, reconstruct: proof_data -> thm } @@ -96,7 +96,7 @@ local -fun with_files ctxt f x = +fun with_files ctxt f = let fun make_names n = (n, n ^ ".proof") @@ -107,43 +107,79 @@ else pairself (File.tmp_path o Path.explode) (make_names ("smt-" ^ serial_string ())) - val y = Exn.capture (f problem_path proof_path) x + val y = Exn.capture f (problem_path, proof_path) val _ = if keep' = "" then (pairself (try File.rm) paths; ()) else () in Exn.release y end -fun run in_path out_path (ctxt, cmd, output) = +fun invoke ctxt output f (paths as (problem_path, proof_path)) = let fun pretty tag ls = Pretty.string_of (Pretty.big_list tag (map Pretty.str ls)) - val x = File.open_output output in_path + val x = File.open_output output problem_path val _ = trace_msg ctxt (pretty "SMT problem:" o split_lines o File.read) - in_path + problem_path - val _ = with_timeout ctxt system_out (cmd in_path out_path) - fun lines_of path = the_default [] (try (File.fold_lines cons out_path) []) - val ls = rev (dropwhile (equal "") (lines_of out_path)) + val _ = with_timeout ctxt f paths + fun lines_of path = the_default [] (try (File.fold_lines cons path) []) + val ls = rev (dropwhile (equal "") (lines_of proof_path)) val _ = trace_msg ctxt (pretty "SMT result:") ls in (x, ls) end +val expand_name = Path.implode o Path.expand o Path.explode + +fun run_perl name args ps = + system_out (space_implode " " ("perl -w" :: + File.shell_path (Path.explode (getenv name)) :: + map File.shell_quote args @ ps)) + +fun use_certificate ctxt ps = + let val name = Config.get ctxt cert + in + if name = "" then false + else + (tracing ("Using certificate " ^ quote (expand_name name) ^ " ..."); + run_perl "CERT_SMT_SOLVER" [expand_name name] ps; + true) + end + +fun run_locally f ctxt env_var args ps = + if getenv env_var = "" + then f ("Undefined Isabelle environment variable: " ^ quote env_var) + else + let val app = Path.expand (Path.explode (getenv env_var)) + in + if not (File.exists app) + then f ("No such file: " ^ quote (Path.implode app)) + else + (tracing ("Invoking local SMT solver " ^ quote (Path.implode app) ^ + " ..."); + system_out (space_implode " " (File.shell_path app :: + map File.shell_quote args @ ps)); ()) + end + +fun run_remote remote_name args ps msg = + (case remote_name of + NONE => error msg + | SOME name => + let + val url = getenv "REMOTE_SMT_URL" + val _ = tracing ("Invoking remote SMT solver " ^ quote name ^ " at " ^ + quote url ^ " ...") + in (run_perl "REMOTE_SMT_SOLVER" (url :: name :: args) ps; ()) end) + +fun run ctxt {env_var, remote_name} args (problem_path, proof_path) = + let val ps = [File.shell_path problem_path, ">", File.shell_path proof_path] + in + if use_certificate ctxt ps then () + else run_locally (run_remote remote_name args ps) ctxt env_var args ps + end + in -fun run_solver ctxt {env_var, remote_name} args output = - let - val qf = File.shell_path and qq = File.shell_quote - val qs = qf o Path.explode - val local_name = getenv env_var - val cert_name = Config.get ctxt cert - val remote = qs (getenv "REMOTE_SMT_SOLVER") - val cert_script = qs (getenv "CERT_SMT_SOLVER") - fun cmd f1 f2 = - if cert_name <> "" - then "perl -w" :: [cert_script, qs cert_name, qf f1, ">", qf f2] - else if local_name <> "" - then qs local_name :: map qq args @ [qf f1, ">", qf f2] - else "perl -w" :: remote :: map qq (remote_name :: args) @ [qf f1, qf f2] - in with_files ctxt run (ctxt, space_implode " " oo cmd, output) end +fun run_solver ctxt cmd args output = + with_files ctxt (invoke ctxt output (run ctxt cmd args)) end @@ -223,13 +259,13 @@ (map (Syntax.pretty_term ctxt) ex)) end - fun fail_tac ctxt msg st = (trace_msg ctxt I msg; Tactical.no_tac st) + fun fail_tac f msg st = (f msg; Tactical.no_tac st) fun SAFE pass_exns tac ctxt i st = if pass_exns then tac ctxt i st else (tac ctxt i st - handle SMT msg => fail_tac ctxt ("SMT: " ^ msg) st - | SMT_COUNTEREXAMPLE cex => fail_tac ctxt (pretty_cex ctxt cex) st) + handle SMT msg => fail_tac (trace_msg ctxt (prefix "SMT: ")) msg st + | SMT_COUNTEREXAMPLE ce => fail_tac tracing (pretty_cex ctxt ce) st) fun smt_solver rules ctxt = solver_of (Context.Proof ctxt) ctxt rules in diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/SMT/Tools/yices_solver.ML --- a/src/HOL/SMT/Tools/yices_solver.ML Sat Nov 07 08:17:53 2009 +0100 +++ b/src/HOL/SMT/Tools/yices_solver.ML Sat Nov 07 08:18:12 2009 +0100 @@ -32,7 +32,7 @@ end fun smtlib_solver oracle _ = { - command = {env_var=env_var, remote_name=solver_name}, + command = {env_var=env_var, remote_name=NONE}, arguments = options, interface = SMTLIB_Interface.interface, reconstruct = oracle } diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/SMT/Tools/z3_model.ML --- a/src/HOL/SMT/Tools/z3_model.ML Sat Nov 07 08:17:53 2009 +0100 +++ b/src/HOL/SMT/Tools/z3_model.ML Sat Nov 07 08:18:12 2009 +0100 @@ -55,7 +55,8 @@ val value = mapping |-- expr val args_case = Scan.repeat expr -- value -val else_case = space -- Scan.this_string "else" |-- value >> pair [] +val else_case = space -- Scan.this_string "else" |-- value >> + pair ([] : expr list) val func = let fun cases st = (else_case >> single || args_case ::: cases) st diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/SMT/Tools/z3_solver.ML --- a/src/HOL/SMT/Tools/z3_solver.ML Sat Nov 07 08:17:53 2009 +0100 +++ b/src/HOL/SMT/Tools/z3_solver.ML Sat Nov 07 08:18:12 2009 +0100 @@ -66,7 +66,7 @@ fun solver oracle ctxt = let val with_proof = Config.get ctxt proofs in - {command = {env_var=env_var, remote_name=solver_name}, + {command = {env_var=env_var, remote_name=SOME solver_name}, arguments = cmdline_options ctxt, interface = Z3_Interface.interface, reconstruct = if with_proof then prover else oracle} diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/SMT/lib/scripts/remote_smt.pl --- a/src/HOL/SMT/lib/scripts/remote_smt.pl Sat Nov 07 08:17:53 2009 +0100 +++ b/src/HOL/SMT/lib/scripts/remote_smt.pl Sat Nov 07 08:18:12 2009 +0100 @@ -8,17 +8,12 @@ use LWP; -# environment - -my $remote_smt_url = $ENV{"REMOTE_SMT_URL"}; - - # arguments -my $solver = $ARGV[0]; -my @options = @ARGV[1 .. ($#ARGV - 2)]; -my $problem_file = $ARGV[-2]; -my $output_file = $ARGV[-1]; +my $url = $ARGV[0]; +my $solver = $ARGV[1]; +my @options = @ARGV[2 .. ($#ARGV - 1)]; +my $problem_file = $ARGV[-1]; # call solver @@ -26,7 +21,7 @@ my $agent = LWP::UserAgent->new; $agent->agent("SMT-Request"); $agent->timeout(180); -my $response = $agent->post($remote_smt_url, [ +my $response = $agent->post($url, [ "Solver" => $solver, "Options" => join(" ", @options), "Problem" => [$problem_file] ], @@ -36,8 +31,6 @@ exit 1; } else { - open(FILE, ">$output_file"); - print FILE $response->content; - close(FILE); + print $response->content; + exit 0; } - diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Sat Nov 07 08:17:53 2009 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Sat Nov 07 08:18:12 2009 +0100 @@ -1,11 +1,15 @@ (* Title: HOL/Tools/ATP_Manager/atp_minimal.ML Author: Philipp Meyer, TU Muenchen -Minimalization of theorem list for metis by using an external automated theorem prover +Minimization of theorem list for metis by using an external automated theorem prover *) signature ATP_MINIMAL = sig + val minimize: ATP_Wrapper.prover -> string -> int -> Proof.state -> + (string * thm list) list -> ((string * thm list) list * int) option * string + (* To be removed once TN has finished his measurements; + the int component of the result should then be removed: *) val minimalize: ATP_Wrapper.prover -> string -> int -> Proof.state -> (string * thm list) list -> ((string * thm list) list * int) option * string end @@ -13,7 +17,16 @@ structure ATP_Minimal: ATP_MINIMAL = struct -(* minimalization algorithm *) +(* Linear minimization *) + +fun lin_gen_minimize p s = +let + fun min [] needed = needed + | min (x::xs) needed = + if p(xs @ needed) then min xs needed else min xs (x::needed) +in (min s [], length s) end; + +(* Clever minimalization algorithm *) local fun isplit (l, r) [] = (l, r) @@ -120,7 +133,7 @@ (* minimalization of thms *) -fun minimalize prover prover_name time_limit state name_thms_pairs = +fun gen_minimalize gen_min prover prover_name time_limit state name_thms_pairs = let val _ = priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^ @@ -141,11 +154,11 @@ else name_thms_pairs val (min_thms, n) = if null to_use then ([], 0) - else minimal (test_thms (SOME filtered)) to_use + else gen_min (test_thms (SOME filtered)) to_use val min_names = sort_distinct string_ord (map fst min_thms) val _ = priority (cat_lines - ["Interations: " ^ string_of_int n, - "Minimal " ^ string_of_int (length min_thms) ^ " theorems"]) + ["Iterations: " ^ string_of_int n (* FIXME TN remove later *), + "Minimal " ^ string_of_int (length min_thms) ^ " theorems"]) in (SOME (min_thms, n), "Try this command: " ^ Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")")) @@ -193,6 +206,10 @@ fun get_options args = fold get_opt args (default_prover, default_time_limit) +val minimize = gen_minimalize lin_gen_minimize + +val minimalize = gen_minimalize minimal + fun sh_min_command args thm_names state = let val (prover_name, time_limit) = get_options args @@ -202,10 +219,11 @@ | NONE => error ("Unknown prover: " ^ quote prover_name)) val name_thms_pairs = get_thms (Proof.context_of state) thm_names in - writeln (#2 (minimalize prover prover_name time_limit state name_thms_pairs)) + writeln (#2 (minimize prover prover_name time_limit state name_thms_pairs)) end -val parse_args = Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) [] +val parse_args = + Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) [] val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel) val _ = @@ -217,4 +235,3 @@ end end - diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/Tools/Function/induction_schema.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Function/induction_schema.ML Sat Nov 07 08:18:12 2009 +0100 @@ -0,0 +1,405 @@ +(* Title: HOL/Tools/Function/induction_schema.ML + Author: Alexander Krauss, TU Muenchen + +A method to prove induction schemas. +*) + +signature INDUCTION_SCHEMA = +sig + val mk_ind_tac : (int -> tactic) -> (int -> tactic) -> (int -> tactic) + -> Proof.context -> thm list -> tactic + val induction_schema_tac : Proof.context -> thm list -> tactic + val setup : theory -> theory +end + + +structure Induction_Schema : INDUCTION_SCHEMA = +struct + +open Function_Lib + + +type rec_call_info = int * (string * typ) list * term list * term list + +datatype scheme_case = + SchemeCase of + { + bidx : int, + qs: (string * typ) list, + oqnames: string list, + gs: term list, + lhs: term list, + rs: rec_call_info list + } + +datatype scheme_branch = + SchemeBranch of + { + P : term, + xs: (string * typ) list, + ws: (string * typ) list, + Cs: term list + } + +datatype ind_scheme = + IndScheme of + { + T: typ, (* sum of products *) + branches: scheme_branch list, + cases: scheme_case list + } + +val ind_atomize = MetaSimplifier.rewrite true @{thms induct_atomize} +val ind_rulify = MetaSimplifier.rewrite true @{thms induct_rulify} + +fun meta thm = thm RS eq_reflection + +val sum_prod_conv = MetaSimplifier.rewrite true + (map meta (@{thm split_conv} :: @{thms sum.cases})) + +fun term_conv thy cv t = + cv (cterm_of thy t) + |> prop_of |> Logic.dest_equals |> snd + +fun mk_relT T = HOLogic.mk_setT (HOLogic.mk_prodT (T, T)) + +fun dest_hhf ctxt t = + let + val (ctxt', vars, imp) = dest_all_all_ctx ctxt t + in + (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp) + end + + +fun mk_scheme' ctxt cases concl = + let + fun mk_branch concl = + let + val (ctxt', ws, Cs, _ $ Pxs) = dest_hhf ctxt concl + val (P, xs) = strip_comb Pxs + in + SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs } + end + + val (branches, cases') = (* correction *) + case Logic.dest_conjunction_list concl of + [conc] => + let + val _ $ Pxs = Logic.strip_assums_concl conc + val (P, _) = strip_comb Pxs + val (cases', conds) = take_prefix (Term.exists_subterm (curry op aconv P)) cases + val concl' = fold_rev (curry Logic.mk_implies) conds conc + in + ([mk_branch concl'], cases') + end + | concls => (map mk_branch concls, cases) + + fun mk_case premise = + let + val (ctxt', qs, prems, _ $ Plhs) = dest_hhf ctxt premise + val (P, lhs) = strip_comb Plhs + + fun bidx Q = find_index (fn SchemeBranch {P=P',...} => Q aconv P') branches + + fun mk_rcinfo pr = + let + val (ctxt'', Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr + val (P', rcs) = strip_comb Phyp + in + (bidx P', Gvs, Gas, rcs) + end + + fun is_pred v = exists (fn SchemeBranch {P,...} => v aconv P) branches + + val (gs, rcprs) = + take_prefix (not o Term.exists_subterm is_pred) prems + in + SchemeCase {bidx=bidx P, qs=qs, oqnames=map fst qs(*FIXME*), gs=gs, lhs=lhs, rs=map mk_rcinfo rcprs} + end + + fun PT_of (SchemeBranch { xs, ...}) = + foldr1 HOLogic.mk_prodT (map snd xs) + + val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches) + in + IndScheme {T=ST, cases=map mk_case cases', branches=branches } + end + + + +fun mk_completeness ctxt (IndScheme {cases, branches, ...}) bidx = + let + val SchemeBranch { xs, ws, Cs, ... } = nth branches bidx + val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases + + val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases [] + val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs)) + val Cs' = map (Pattern.rewrite_term (ProofContext.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs + + fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) = + HOLogic.mk_Trueprop Pbool + |> fold_rev (fn x_l => curry Logic.mk_implies (HOLogic.mk_Trueprop(HOLogic.mk_eq x_l))) + (xs' ~~ lhs) + |> fold_rev (curry Logic.mk_implies) gs + |> fold_rev mk_forall_rename (oqnames ~~ map Free qs) + in + HOLogic.mk_Trueprop Pbool + |> fold_rev (curry Logic.mk_implies o mk_case) relevant_cases + |> fold_rev (curry Logic.mk_implies) Cs' + |> fold_rev (Logic.all o Free) ws + |> fold_rev mk_forall_rename (map fst xs ~~ xs') + |> mk_forall_rename ("P", Pbool) + end + +fun mk_wf ctxt R (IndScheme {T, ...}) = + HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R) + +fun mk_ineqs R (IndScheme {T, cases, branches}) = + let + fun inject i ts = + SumTree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts) + + val thesis = Free ("thesis", HOLogic.boolT) (* FIXME *) + + fun mk_pres bdx args = + let + val SchemeBranch { xs, ws, Cs, ... } = nth branches bdx + fun replace (x, v) t = betapply (lambda (Free x) t, v) + val Cs' = map (fold replace (xs ~~ args)) Cs + val cse = + HOLogic.mk_Trueprop thesis + |> fold_rev (curry Logic.mk_implies) Cs' + |> fold_rev (Logic.all o Free) ws + in + Logic.mk_implies (cse, HOLogic.mk_Trueprop thesis) + end + + fun f (SchemeCase {bidx, qs, oqnames, gs, lhs, rs, ...}) = + let + fun g (bidx', Gvs, Gas, rcarg) = + let val export = + fold_rev (curry Logic.mk_implies) Gas + #> fold_rev (curry Logic.mk_implies) gs + #> fold_rev (Logic.all o Free) Gvs + #> fold_rev mk_forall_rename (oqnames ~~ map Free qs) + in + (HOLogic.mk_mem (HOLogic.mk_prod (inject bidx' rcarg, inject bidx lhs), R) + |> HOLogic.mk_Trueprop + |> export, + mk_pres bidx' rcarg + |> export + |> Logic.all thesis) + end + in + map g rs + end + in + map f cases + end + + +fun mk_hol_imp a b = HOLogic.imp $ a $ b + +fun mk_ind_goal thy branches = + let + fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) = + HOLogic.mk_Trueprop (list_comb (P, map Free xs)) + |> fold_rev (curry Logic.mk_implies) Cs + |> fold_rev (Logic.all o Free) ws + |> term_conv thy ind_atomize + |> ObjectLogic.drop_judgment thy + |> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs)) + in + SumTree.mk_sumcases HOLogic.boolT (map brnch branches) + end + + +fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss (IndScheme {T, cases=scases, branches}) = + let + val n = length branches + + val scases_idx = map_index I scases + + fun inject i ts = + SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts) + val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches) + + val thy = ProofContext.theory_of ctxt + val cert = cterm_of thy + + val P_comp = mk_ind_goal thy branches + + (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) + val ihyp = Term.all T $ Abs ("z", T, + Logic.mk_implies + (HOLogic.mk_Trueprop ( + Const ("op :", HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) + $ (HOLogic.pair_const T T $ Bound 0 $ x) + $ R), + HOLogic.mk_Trueprop (P_comp $ Bound 0))) + |> cert + + val aihyp = assume ihyp + + (* Rule for case splitting along the sum types *) + val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches + val pats = map_index (uncurry inject) xss + val sum_split_rule = Pat_Completeness.prove_completeness thy [x] (P_comp $ x) xss (map single pats) + + fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) = + let + val fxs = map Free xs + val branch_hyp = assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat)))) + + val C_hyps = map (cert #> assume) Cs + + val (relevant_cases, ineqss') = filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx) (scases_idx ~~ ineqss) + |> split_list + + fun prove_case (cidx, SchemeCase {qs, oqnames, gs, lhs, rs, ...}) ineq_press = + let + val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs) + + val cqs = map (cert o Free) qs + val ags = map (assume o cert) gs + + val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps) + val sih = full_simplify replace_x_ss aihyp + + fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) = + let + val cGas = map (assume o cert) Gas + val cGvs = map (cert o Free) Gvs + val import = fold forall_elim (cqs @ cGvs) + #> fold Thm.elim_implies (ags @ cGas) + val ipres = pres + |> forall_elim (cert (list_comb (P_of idx, rcargs))) + |> import + in + sih |> forall_elim (cert (inject idx rcargs)) + |> Thm.elim_implies (import ineq) (* Psum rcargs *) + |> Conv.fconv_rule sum_prod_conv + |> Conv.fconv_rule ind_rulify + |> (fn th => th COMP ipres) (* P rs *) + |> fold_rev (implies_intr o cprop_of) cGas + |> fold_rev forall_intr cGvs + end + + val P_recs = map2 mk_Prec rs ineq_press (* [P rec1, P rec2, ... ] *) + + val step = HOLogic.mk_Trueprop (list_comb (P, lhs)) + |> fold_rev (curry Logic.mk_implies o prop_of) P_recs + |> fold_rev (curry Logic.mk_implies) gs + |> fold_rev (Logic.all o Free) qs + |> cert + + val Plhs_to_Pxs_conv = + foldl1 (uncurry Conv.combination_conv) + (Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps) + + val res = assume step + |> fold forall_elim cqs + |> fold Thm.elim_implies ags + |> fold Thm.elim_implies P_recs (* P lhs *) + |> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *) + |> fold_rev (implies_intr o cprop_of) (ags @ case_hyps) + |> fold_rev forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *) + in + (res, (cidx, step)) + end + + val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss') + + val bstep = complete_thm + |> forall_elim (cert (list_comb (P, fxs))) + |> fold (forall_elim o cert) (fxs @ map Free ws) + |> fold Thm.elim_implies C_hyps (* FIXME: optimization using rotate_prems *) + |> fold Thm.elim_implies cases (* P xs *) + |> fold_rev (implies_intr o cprop_of) C_hyps + |> fold_rev (forall_intr o cert o Free) ws + + val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x)) + |> Goal.init + |> (MetaSimplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases})) + THEN CONVERSION ind_rulify 1) + |> Seq.hd + |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep) + |> Goal.finish ctxt + |> implies_intr (cprop_of branch_hyp) + |> fold_rev (forall_intr o cert) fxs + in + (Pxs, steps) + end + + val (branches, steps) = split_list (map_index prove_branch (branches ~~ (complete_thms ~~ pats))) + |> apsnd flat + + val istep = sum_split_rule + |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches + |> implies_intr ihyp + |> forall_intr (cert x) (* "!!x. (!!y P x" *) + + val induct_rule = + @{thm "wf_induct_rule"} + |> (curry op COMP) wf_thm + |> (curry op COMP) istep + + val steps_sorted = map snd (sort (int_ord o pairself fst) steps) + in + (steps_sorted, induct_rule) + end + + +fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts = (ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL +(SUBGOAL (fn (t, i) => + let + val (ctxt', _, cases, concl) = dest_hhf ctxt t + val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl +(* val _ = tracing (makestring scheme)*) + val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt' + val R = Free (Rn, mk_relT ST) + val x = Free (xn, ST) + val cert = cterm_of (ProofContext.theory_of ctxt) + + val ineqss = mk_ineqs R scheme + |> map (map (pairself (assume o cert))) + val complete = map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches) + val wf_thm = mk_wf ctxt R scheme |> cert |> assume + + val (descent, pres) = split_list (flat ineqss) + val newgoals = complete @ pres @ wf_thm :: descent + + val (steps, indthm) = mk_induct_rule ctxt'' R x complete wf_thm ineqss scheme + + fun project (i, SchemeBranch {xs, ...}) = + let + val inst = cert (SumTree.mk_inj ST (length branches) (i + 1) (foldr1 HOLogic.mk_prod (map Free xs))) + in + indthm |> Drule.instantiate' [] [SOME inst] + |> simplify SumTree.sumcase_split_ss + |> Conv.fconv_rule ind_rulify +(* |> (fn thm => (tracing (makestring thm); thm))*) + end + + val res = Conjunction.intr_balanced (map_index project branches) + |> fold_rev implies_intr (map cprop_of newgoals @ steps) + |> (fn thm => Thm.generalize ([], [Rn]) (Thm.maxidx_of thm + 1) thm) + + val nbranches = length branches + val npres = length pres + in + Thm.compose_no_flatten false (res, length newgoals) i + THEN term_tac (i + nbranches + npres) + THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches)))) + THEN (EVERY (map (TRY o comp_tac) ((i + nbranches - 1) downto i))) + end)) + + +fun induction_schema_tac ctxt = + mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt; + +val setup = + Method.setup @{binding induction_schema} (Scan.succeed (RAW_METHOD o induction_schema_tac)) + "proves an induction principle" + +end diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/Tools/Function/induction_scheme.ML --- a/src/HOL/Tools/Function/induction_scheme.ML Sat Nov 07 08:17:53 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,405 +0,0 @@ -(* Title: HOL/Tools/Function/induction_scheme.ML - Author: Alexander Krauss, TU Muenchen - -A method to prove induction schemes. -*) - -signature INDUCTION_SCHEME = -sig - val mk_ind_tac : (int -> tactic) -> (int -> tactic) -> (int -> tactic) - -> Proof.context -> thm list -> tactic - val induct_scheme_tac : Proof.context -> thm list -> tactic - val setup : theory -> theory -end - - -structure Induction_Scheme : INDUCTION_SCHEME = -struct - -open Function_Lib - - -type rec_call_info = int * (string * typ) list * term list * term list - -datatype scheme_case = - SchemeCase of - { - bidx : int, - qs: (string * typ) list, - oqnames: string list, - gs: term list, - lhs: term list, - rs: rec_call_info list - } - -datatype scheme_branch = - SchemeBranch of - { - P : term, - xs: (string * typ) list, - ws: (string * typ) list, - Cs: term list - } - -datatype ind_scheme = - IndScheme of - { - T: typ, (* sum of products *) - branches: scheme_branch list, - cases: scheme_case list - } - -val ind_atomize = MetaSimplifier.rewrite true @{thms induct_atomize} -val ind_rulify = MetaSimplifier.rewrite true @{thms induct_rulify} - -fun meta thm = thm RS eq_reflection - -val sum_prod_conv = MetaSimplifier.rewrite true - (map meta (@{thm split_conv} :: @{thms sum.cases})) - -fun term_conv thy cv t = - cv (cterm_of thy t) - |> prop_of |> Logic.dest_equals |> snd - -fun mk_relT T = HOLogic.mk_setT (HOLogic.mk_prodT (T, T)) - -fun dest_hhf ctxt t = - let - val (ctxt', vars, imp) = dest_all_all_ctx ctxt t - in - (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp) - end - - -fun mk_scheme' ctxt cases concl = - let - fun mk_branch concl = - let - val (ctxt', ws, Cs, _ $ Pxs) = dest_hhf ctxt concl - val (P, xs) = strip_comb Pxs - in - SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs } - end - - val (branches, cases') = (* correction *) - case Logic.dest_conjunction_list concl of - [conc] => - let - val _ $ Pxs = Logic.strip_assums_concl conc - val (P, _) = strip_comb Pxs - val (cases', conds) = take_prefix (Term.exists_subterm (curry op aconv P)) cases - val concl' = fold_rev (curry Logic.mk_implies) conds conc - in - ([mk_branch concl'], cases') - end - | concls => (map mk_branch concls, cases) - - fun mk_case premise = - let - val (ctxt', qs, prems, _ $ Plhs) = dest_hhf ctxt premise - val (P, lhs) = strip_comb Plhs - - fun bidx Q = find_index (fn SchemeBranch {P=P',...} => Q aconv P') branches - - fun mk_rcinfo pr = - let - val (ctxt'', Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr - val (P', rcs) = strip_comb Phyp - in - (bidx P', Gvs, Gas, rcs) - end - - fun is_pred v = exists (fn SchemeBranch {P,...} => v aconv P) branches - - val (gs, rcprs) = - take_prefix (not o Term.exists_subterm is_pred) prems - in - SchemeCase {bidx=bidx P, qs=qs, oqnames=map fst qs(*FIXME*), gs=gs, lhs=lhs, rs=map mk_rcinfo rcprs} - end - - fun PT_of (SchemeBranch { xs, ...}) = - foldr1 HOLogic.mk_prodT (map snd xs) - - val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches) - in - IndScheme {T=ST, cases=map mk_case cases', branches=branches } - end - - - -fun mk_completeness ctxt (IndScheme {cases, branches, ...}) bidx = - let - val SchemeBranch { xs, ws, Cs, ... } = nth branches bidx - val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases - - val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases [] - val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs)) - val Cs' = map (Pattern.rewrite_term (ProofContext.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs - - fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) = - HOLogic.mk_Trueprop Pbool - |> fold_rev (fn x_l => curry Logic.mk_implies (HOLogic.mk_Trueprop(HOLogic.mk_eq x_l))) - (xs' ~~ lhs) - |> fold_rev (curry Logic.mk_implies) gs - |> fold_rev mk_forall_rename (oqnames ~~ map Free qs) - in - HOLogic.mk_Trueprop Pbool - |> fold_rev (curry Logic.mk_implies o mk_case) relevant_cases - |> fold_rev (curry Logic.mk_implies) Cs' - |> fold_rev (Logic.all o Free) ws - |> fold_rev mk_forall_rename (map fst xs ~~ xs') - |> mk_forall_rename ("P", Pbool) - end - -fun mk_wf ctxt R (IndScheme {T, ...}) = - HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R) - -fun mk_ineqs R (IndScheme {T, cases, branches}) = - let - fun inject i ts = - SumTree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts) - - val thesis = Free ("thesis", HOLogic.boolT) (* FIXME *) - - fun mk_pres bdx args = - let - val SchemeBranch { xs, ws, Cs, ... } = nth branches bdx - fun replace (x, v) t = betapply (lambda (Free x) t, v) - val Cs' = map (fold replace (xs ~~ args)) Cs - val cse = - HOLogic.mk_Trueprop thesis - |> fold_rev (curry Logic.mk_implies) Cs' - |> fold_rev (Logic.all o Free) ws - in - Logic.mk_implies (cse, HOLogic.mk_Trueprop thesis) - end - - fun f (SchemeCase {bidx, qs, oqnames, gs, lhs, rs, ...}) = - let - fun g (bidx', Gvs, Gas, rcarg) = - let val export = - fold_rev (curry Logic.mk_implies) Gas - #> fold_rev (curry Logic.mk_implies) gs - #> fold_rev (Logic.all o Free) Gvs - #> fold_rev mk_forall_rename (oqnames ~~ map Free qs) - in - (HOLogic.mk_mem (HOLogic.mk_prod (inject bidx' rcarg, inject bidx lhs), R) - |> HOLogic.mk_Trueprop - |> export, - mk_pres bidx' rcarg - |> export - |> Logic.all thesis) - end - in - map g rs - end - in - map f cases - end - - -fun mk_hol_imp a b = HOLogic.imp $ a $ b - -fun mk_ind_goal thy branches = - let - fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) = - HOLogic.mk_Trueprop (list_comb (P, map Free xs)) - |> fold_rev (curry Logic.mk_implies) Cs - |> fold_rev (Logic.all o Free) ws - |> term_conv thy ind_atomize - |> ObjectLogic.drop_judgment thy - |> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs)) - in - SumTree.mk_sumcases HOLogic.boolT (map brnch branches) - end - - -fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss (IndScheme {T, cases=scases, branches}) = - let - val n = length branches - - val scases_idx = map_index I scases - - fun inject i ts = - SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts) - val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches) - - val thy = ProofContext.theory_of ctxt - val cert = cterm_of thy - - val P_comp = mk_ind_goal thy branches - - (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) - val ihyp = Term.all T $ Abs ("z", T, - Logic.mk_implies - (HOLogic.mk_Trueprop ( - Const ("op :", HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) - $ (HOLogic.pair_const T T $ Bound 0 $ x) - $ R), - HOLogic.mk_Trueprop (P_comp $ Bound 0))) - |> cert - - val aihyp = assume ihyp - - (* Rule for case splitting along the sum types *) - val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches - val pats = map_index (uncurry inject) xss - val sum_split_rule = Pat_Completeness.prove_completeness thy [x] (P_comp $ x) xss (map single pats) - - fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) = - let - val fxs = map Free xs - val branch_hyp = assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat)))) - - val C_hyps = map (cert #> assume) Cs - - val (relevant_cases, ineqss') = filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx) (scases_idx ~~ ineqss) - |> split_list - - fun prove_case (cidx, SchemeCase {qs, oqnames, gs, lhs, rs, ...}) ineq_press = - let - val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs) - - val cqs = map (cert o Free) qs - val ags = map (assume o cert) gs - - val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps) - val sih = full_simplify replace_x_ss aihyp - - fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) = - let - val cGas = map (assume o cert) Gas - val cGvs = map (cert o Free) Gvs - val import = fold forall_elim (cqs @ cGvs) - #> fold Thm.elim_implies (ags @ cGas) - val ipres = pres - |> forall_elim (cert (list_comb (P_of idx, rcargs))) - |> import - in - sih |> forall_elim (cert (inject idx rcargs)) - |> Thm.elim_implies (import ineq) (* Psum rcargs *) - |> Conv.fconv_rule sum_prod_conv - |> Conv.fconv_rule ind_rulify - |> (fn th => th COMP ipres) (* P rs *) - |> fold_rev (implies_intr o cprop_of) cGas - |> fold_rev forall_intr cGvs - end - - val P_recs = map2 mk_Prec rs ineq_press (* [P rec1, P rec2, ... ] *) - - val step = HOLogic.mk_Trueprop (list_comb (P, lhs)) - |> fold_rev (curry Logic.mk_implies o prop_of) P_recs - |> fold_rev (curry Logic.mk_implies) gs - |> fold_rev (Logic.all o Free) qs - |> cert - - val Plhs_to_Pxs_conv = - foldl1 (uncurry Conv.combination_conv) - (Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps) - - val res = assume step - |> fold forall_elim cqs - |> fold Thm.elim_implies ags - |> fold Thm.elim_implies P_recs (* P lhs *) - |> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *) - |> fold_rev (implies_intr o cprop_of) (ags @ case_hyps) - |> fold_rev forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *) - in - (res, (cidx, step)) - end - - val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss') - - val bstep = complete_thm - |> forall_elim (cert (list_comb (P, fxs))) - |> fold (forall_elim o cert) (fxs @ map Free ws) - |> fold Thm.elim_implies C_hyps (* FIXME: optimization using rotate_prems *) - |> fold Thm.elim_implies cases (* P xs *) - |> fold_rev (implies_intr o cprop_of) C_hyps - |> fold_rev (forall_intr o cert o Free) ws - - val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x)) - |> Goal.init - |> (MetaSimplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases})) - THEN CONVERSION ind_rulify 1) - |> Seq.hd - |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep) - |> Goal.finish ctxt - |> implies_intr (cprop_of branch_hyp) - |> fold_rev (forall_intr o cert) fxs - in - (Pxs, steps) - end - - val (branches, steps) = split_list (map_index prove_branch (branches ~~ (complete_thms ~~ pats))) - |> apsnd flat - - val istep = sum_split_rule - |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches - |> implies_intr ihyp - |> forall_intr (cert x) (* "!!x. (!!y P x" *) - - val induct_rule = - @{thm "wf_induct_rule"} - |> (curry op COMP) wf_thm - |> (curry op COMP) istep - - val steps_sorted = map snd (sort (int_ord o pairself fst) steps) - in - (steps_sorted, induct_rule) - end - - -fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts = (ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL -(SUBGOAL (fn (t, i) => - let - val (ctxt', _, cases, concl) = dest_hhf ctxt t - val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl -(* val _ = tracing (makestring scheme)*) - val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt' - val R = Free (Rn, mk_relT ST) - val x = Free (xn, ST) - val cert = cterm_of (ProofContext.theory_of ctxt) - - val ineqss = mk_ineqs R scheme - |> map (map (pairself (assume o cert))) - val complete = map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches) - val wf_thm = mk_wf ctxt R scheme |> cert |> assume - - val (descent, pres) = split_list (flat ineqss) - val newgoals = complete @ pres @ wf_thm :: descent - - val (steps, indthm) = mk_induct_rule ctxt'' R x complete wf_thm ineqss scheme - - fun project (i, SchemeBranch {xs, ...}) = - let - val inst = cert (SumTree.mk_inj ST (length branches) (i + 1) (foldr1 HOLogic.mk_prod (map Free xs))) - in - indthm |> Drule.instantiate' [] [SOME inst] - |> simplify SumTree.sumcase_split_ss - |> Conv.fconv_rule ind_rulify -(* |> (fn thm => (tracing (makestring thm); thm))*) - end - - val res = Conjunction.intr_balanced (map_index project branches) - |> fold_rev implies_intr (map cprop_of newgoals @ steps) - |> (fn thm => Thm.generalize ([], [Rn]) (Thm.maxidx_of thm + 1) thm) - - val nbranches = length branches - val npres = length pres - in - Thm.compose_no_flatten false (res, length newgoals) i - THEN term_tac (i + nbranches + npres) - THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches)))) - THEN (EVERY (map (TRY o comp_tac) ((i + nbranches - 1) downto i))) - end)) - - -fun induct_scheme_tac ctxt = - mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt; - -val setup = - Method.setup @{binding induct_scheme} (Scan.succeed (RAW_METHOD o induct_scheme_tac)) - "proves an induction principle" - -end diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Nov 07 08:17:53 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Nov 07 08:18:12 2009 +0100 @@ -37,8 +37,7 @@ map (fn (c, thms) => "Constant " ^ c ^ " has specification:\n" ^ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs -(* TODO: *) -fun overload_const thy s = s +fun overload_const thy s = the_default s (Option.map fst (AxClass.inst_of_param thy s)) fun map_specs f specs = map (fn (s, ths) => (s, f ths)) specs @@ -87,8 +86,8 @@ val _ = print_intross options thy''' "Introduction rules with new constants: " intross3 val intross4 = map_specs (maps remove_pointless_clauses) intross3 val _ = print_intross options thy''' "After removing pointless clauses: " intross4 - val intross5 = (*map (fn (s, ths) => (overload_const s, map (AxClass.overload thy''') ths))*) intross4 - val intross6 = map_specs (map (expand_tuples thy''')) intross4 + val intross5 = map (fn (s, ths) => (overload_const thy''' s, map (AxClass.overload thy''') ths)) intross4 + val intross6 = map_specs (map (expand_tuples thy''')) intross5 val _ = print_intross options thy''' "introduction rules before registering: " intross6 val _ = print_step options "Registering introduction rules..." val thy'''' = fold Predicate_Compile_Core.register_intros intross6 thy''' @@ -121,7 +120,8 @@ skip_proof = chk "skip_proof", inductify = chk "inductify", random = chk "random", - depth_limited = chk "depth_limited" + depth_limited = chk "depth_limited", + annotated = chk "annotated" } end @@ -149,11 +149,14 @@ val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes", - "show_mode_inference", "show_compilation", "skip_proof", "inductify", "random", "depth_limited"] + "show_mode_inference", "show_compilation", "skip_proof", "inductify", "random", "depth_limited", + "annotated"] local structure P = OuterParse in +(* Parser for mode annotations *) + (*val parse_argmode' = P.nat >> rpair NONE || P.$$$ "(" |-- P.enum1 "," --| P.$$$ ")"*) datatype raw_argmode = Argmode of string | Argmode_Tuple of string list @@ -184,16 +187,42 @@ Scan.optional (P.$$$ "(" |-- Args.$$$ "mode" |-- P.$$$ ":" |-- P.enum1 "," (parse_mode || parse_mode') --| P.$$$ ")" >> SOME) NONE -val scan_params = +(* Parser for options *) + +val scan_options = let - val scan_bool_param = foldl1 (op ||) (map Args.$$$ bool_options) + val scan_bool_option = foldl1 (op ||) (map Args.$$$ bool_options) in - Scan.optional (P.$$$ "[" |-- P.enum1 "," scan_bool_param --| P.$$$ "]") [] + Scan.optional (P.$$$ "[" |-- P.enum1 "," scan_bool_option --| P.$$$ "]") [] end +val opt_print_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) []; + +val opt_smode = (P.$$$ "_" >> K NONE) || (parse_smode >> SOME) + +val opt_param_modes = Scan.optional (P.$$$ "[" |-- Args.$$$ "mode" |-- P.$$$ ":" |-- + P.enum ", " opt_smode --| P.$$$ "]" >> SOME) NONE + +val value_options = + let + val depth_limit = Scan.optional (Args.$$$ "depth_limit" |-- P.$$$ "=" |-- P.nat >> SOME) NONE + val random = Scan.optional (Args.$$$ "random" >> K true) false + val annotated = Scan.optional (Args.$$$ "annotated" >> K true) false + in + Scan.optional (P.$$$ "[" |-- depth_limit -- (random -- annotated) --| P.$$$ "]") + (NONE, (false, false)) + end + +(* code_pred command and values command *) + val _ = OuterSyntax.local_theory_to_proof "code_pred" "prove equations for predicate specified by intro/elim rules" - OuterKeyword.thy_goal (opt_modes -- scan_params -- P.term_group >> code_pred_cmd) + OuterKeyword.thy_goal (opt_modes -- scan_options -- P.term_group >> code_pred_cmd) + +val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag + (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional P.nat ~1 -- P.term + >> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.no_timing o Toplevel.keep + (Predicate_Compile_Core.values_cmd print_modes param_modes options k t))); end diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Nov 07 08:17:53 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Nov 07 08:18:12 2009 +0100 @@ -170,7 +170,8 @@ inductify : bool, random : bool, - depth_limited : bool + depth_limited : bool, + annotated : bool }; fun expected_modes (Options opt) = #expected_modes opt @@ -185,6 +186,7 @@ fun is_inductify (Options opt) = #inductify opt fun is_random (Options opt) = #random opt fun is_depth_limited (Options opt) = #depth_limited opt +fun is_annotated (Options opt) = #annotated opt val default_options = Options { expected_modes = NONE, @@ -198,7 +200,8 @@ inductify = false, random = false, - depth_limited = false + depth_limited = false, + annotated = false } diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Nov 07 08:17:53 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Nov 07 08:18:12 2009 +0100 @@ -6,9 +6,11 @@ signature PREDICATE_COMPILE_CORE = sig - val setup: theory -> theory - val code_pred: Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state - val code_pred_cmd: Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state + val setup : theory -> theory + val code_pred : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state + val code_pred_cmd : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state + val values_cmd : string list -> Predicate_Compile_Aux.smode option list option + -> int option * (bool * bool) -> int -> string -> Toplevel.state -> unit val register_predicate : (string * thm list * thm * int) -> theory -> theory val register_intros : string * thm list -> theory -> theory val is_registered : theory -> string -> bool @@ -19,20 +21,21 @@ val modes_of: theory -> string -> Predicate_Compile_Aux.mode list val depth_limited_modes_of: theory -> string -> Predicate_Compile_Aux.mode list val depth_limited_function_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string - val generator_modes_of: theory -> string -> Predicate_Compile_Aux.mode list - val generator_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string + val random_modes_of: theory -> string -> Predicate_Compile_Aux.mode list + val random_function_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string val all_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list - val all_generator_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list - val intros_of: theory -> string -> thm list - val nparams_of: theory -> string -> int - val add_intro: thm -> theory -> theory - val set_elim: thm -> theory -> theory + val all_random_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list + val intros_of : theory -> string -> thm list + val nparams_of : theory -> string -> int + val add_intro : thm -> theory -> theory + val set_elim : thm -> theory -> theory val set_nparams : string -> int -> theory -> theory - val print_stored_rules: theory -> unit - val print_all_modes: theory -> unit + val print_stored_rules : theory -> unit + val print_all_modes : theory -> unit val mk_casesrule : Proof.context -> term -> int -> thm list -> term val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref - val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int)) option Unsynchronized.ref + val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int)) + option Unsynchronized.ref val code_pred_intros_attrib : attribute (* used by Quickcheck_Generator *) (* temporary for testing of the compilation *) @@ -51,7 +54,9 @@ val randompred_compfuns : compilation_funs val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory val add_quickcheck_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory - val add_depth_limited_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory + val add_depth_limited_equations : Predicate_Compile_Aux.options + -> string list -> theory -> theory + val mk_tracing : string -> term -> term end; structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE = @@ -116,6 +121,10 @@ Type ("*", [Type ("*", [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T | dest_randomT T = raise TYPE ("dest_randomT", [T], []) +fun mk_tracing s t = + Const(@{const_name Code_Evaluation.tracing}, + @{typ String.literal} --> (fastype_of t) --> (fastype_of t)) $ (HOLogic.mk_literal s) $ t + (* destruction of intro rules *) (* FIXME: look for other place where this functionality was used before *) @@ -197,17 +206,22 @@ intros : thm list, elim : thm option, nparams : int, - functions : (mode * predfun_data) list, - generators : (mode * function_data) list, - depth_limited_functions : (mode * function_data) list + functions : bool * (mode * predfun_data) list, + random_functions : bool * (mode * function_data) list, + depth_limited_functions : bool * (mode * function_data) list, + annotated_functions : bool * (mode * function_data) list }; fun rep_pred_data (PredData data) = data; -fun mk_pred_data ((intros, elim, nparams), (functions, generators, depth_limited_functions)) = +fun mk_pred_data ((intros, elim, nparams), + (functions, random_functions, depth_limited_functions, annotated_functions)) = PredData {intros = intros, elim = elim, nparams = nparams, - functions = functions, generators = generators, depth_limited_functions = depth_limited_functions} -fun map_pred_data f (PredData {intros, elim, nparams, functions, generators, depth_limited_functions}) = - mk_pred_data (f ((intros, elim, nparams), (functions, generators, depth_limited_functions))) + functions = functions, random_functions = random_functions, + depth_limited_functions = depth_limited_functions, annotated_functions = annotated_functions} +fun map_pred_data f (PredData {intros, elim, nparams, + functions, random_functions, depth_limited_functions, annotated_functions}) = + mk_pred_data (f ((intros, elim, nparams), (functions, random_functions, + depth_limited_functions, annotated_functions))) fun eq_option eq (NONE, NONE) = true | eq_option eq (SOME x, SOME y) = eq (x, y) @@ -250,22 +264,19 @@ val nparams_of = #nparams oo the_pred_data -val modes_of = (map fst) o #functions oo the_pred_data +val modes_of = (map fst) o snd o #functions oo the_pred_data -val depth_limited_modes_of = (map fst) o #depth_limited_functions oo the_pred_data - -val random_modes_of = (map fst) o #generators oo the_pred_data - fun all_modes_of thy = map (fn name => (name, modes_of thy name)) (all_preds_of thy) -val is_compiled = not o null o #functions oo the_pred_data +val defined_functions = fst o #functions oo the_pred_data fun lookup_predfun_data thy name mode = - Option.map rep_predfun_data (AList.lookup (op =) - (#functions (the_pred_data thy name)) mode) + Option.map rep_predfun_data + (AList.lookup (op =) (snd (#functions (the_pred_data thy name))) mode) fun the_predfun_data thy name mode = case lookup_predfun_data thy name mode - of NONE => error ("No function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ name) + of NONE => error ("No function defined for mode " ^ string_of_mode mode ^ + " of predicate " ^ name) | SOME data => data; val predfun_name_of = #name ooo the_predfun_data @@ -276,31 +287,54 @@ val predfun_elim_of = #elim ooo the_predfun_data -fun lookup_generator_data thy name mode = - Option.map rep_function_data (AList.lookup (op =) - (#generators (the_pred_data thy name)) mode) +fun lookup_random_function_data thy name mode = + Option.map rep_function_data + (AList.lookup (op =) (snd (#random_functions (the_pred_data thy name))) mode) -fun the_generator_data thy name mode = case lookup_generator_data thy name mode - of NONE => error ("No generator defined for mode " ^ string_of_mode mode ^ " of predicate " ^ name) +fun the_random_function_data thy name mode = case lookup_random_function_data thy name mode of + NONE => error ("No random function defined for mode " ^ string_of_mode mode ^ + " of predicate " ^ name) | SOME data => data -val generator_name_of = #name ooo the_generator_data +val random_function_name_of = #name ooo the_random_function_data + +val random_modes_of = (map fst) o snd o #random_functions oo the_pred_data -val generator_modes_of = (map fst) o #generators oo the_pred_data +val defined_random_functions = fst o #random_functions oo the_pred_data -fun all_generator_modes_of thy = - map (fn name => (name, generator_modes_of thy name)) (all_preds_of thy) +fun all_random_modes_of thy = + map (fn name => (name, random_modes_of thy name)) (all_preds_of thy) fun lookup_depth_limited_function_data thy name mode = - Option.map rep_function_data (AList.lookup (op =) - (#depth_limited_functions (the_pred_data thy name)) mode) + Option.map rep_function_data + (AList.lookup (op =) (snd (#depth_limited_functions (the_pred_data thy name))) mode) + +fun the_depth_limited_function_data thy name mode = + case lookup_depth_limited_function_data thy name mode of + NONE => error ("No depth-limited function defined for mode " ^ string_of_mode mode + ^ " of predicate " ^ name) + | SOME data => data + +val depth_limited_function_name_of = #name ooo the_depth_limited_function_data -fun the_depth_limited_function_data thy name mode = case lookup_depth_limited_function_data thy name mode - of NONE => error ("No depth-limited function defined for mode " ^ string_of_mode mode +val depth_limited_modes_of = (map fst) o snd o #depth_limited_functions oo the_pred_data + +val defined_depth_limited_functions = fst o #depth_limited_functions oo the_pred_data + +fun lookup_annotated_function_data thy name mode = + Option.map rep_function_data + (AList.lookup (op =) (snd (#annotated_functions (the_pred_data thy name))) mode) + +fun the_annotated_function_data thy name mode = case lookup_annotated_function_data thy name mode + of NONE => error ("No annotated function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ name) | SOME data => data -val depth_limited_function_name_of = #name ooo the_depth_limited_function_data +val annotated_function_name_of = #name ooo the_annotated_function_data + +val annotated_modes_of = (map fst) o snd o #annotated_functions oo the_pred_data + +val defined_annotated_functions = fst o #annotated_functions oo the_pred_data (* diagnostic display functions *) @@ -555,6 +589,16 @@ fun expand_tuples_elim th = th +(* updaters *) + +fun apfst4 f (x1, x2, x3, x4) = (f x1, x2, x3, x4) +fun apsnd4 f (x1, x2, x3, x4) = (x1, f x2, x3, x4) +fun aptrd4 f (x1, x2, x3, x4) = (x1, x2, f x3, x4) +fun apfourth4 f (x1, x2, x3, x4) = (x1, x2, x3, f x4) +fun appair f g (x, y) = (f x, g x) + +val no_compilation = ((false, []), (false, []), (false, []), (false, [])) + fun fetch_pred_data thy name = case try (Inductive.the_inductive (ProofContext.init thy)) name of SOME (info as (_, result)) => @@ -576,19 +620,13 @@ (mk_casesrule (ProofContext.init thy) pred nparams intros) val (intros, elim) = (*if null intros then noclause thy name elim else*) (intros, elim) in - mk_pred_data ((intros, SOME elim, nparams), ([], [], [])) - end + mk_pred_data ((intros, SOME elim, nparams), no_compilation) + end | NONE => error ("No such predicate: " ^ quote name) -(* updaters *) - -fun apfst3 f (x, y, z) = (f x, y, z) -fun apsnd3 f (x, y, z) = (x, f y, z) -fun aptrd3 f (x, y, z) = (x, y, f z) - fun add_predfun name mode data = let - val add = (apsnd o apfst3 o cons) (mode, mk_predfun_data data) + val add = (apsnd o apfst4) (fn (x, y) => (true, cons (mode, mk_predfun_data data) y)) in PredData.map (Graph.map_node name (map_pred_data add)) end fun is_inductive_predicate thy name = @@ -599,7 +637,8 @@ val intros = (#intros o rep_pred_data) value in fold Term.add_const_names (map Thm.prop_of intros) [] - |> filter (fn c => (not (c = key)) andalso (is_inductive_predicate thy c orelse is_registered thy c)) + |> filter (fn c => (not (c = key)) andalso + (is_inductive_predicate thy c orelse is_registered thy c)) end; @@ -637,8 +676,9 @@ (apfst (fn (intros, elim, nparams) => (intros @ [thm], elim, nparams)))) gr | NONE => let - val nparams = the_default (guess_nparams T) (try (#nparams o rep_pred_data o (fetch_pred_data thy)) name) - in Graph.new_node (name, mk_pred_data (([thm], NONE, nparams), ([], [], []))) gr end; + val nparams = the_default (guess_nparams T) + (try (#nparams o rep_pred_data o (fetch_pred_data thy)) name) + in Graph.new_node (name, mk_pred_data (([thm], NONE, nparams), no_compilation)) gr end; in PredData.map cons_intro thy end fun set_elim thm = let @@ -659,7 +699,8 @@ in if not (member (op =) (Graph.keys (PredData.get thy)) constname) then PredData.map - (Graph.new_node (constname, mk_pred_data ((intros, SOME elim, nparams), ([], [], [])))) thy + (Graph.new_node (constname, + mk_pred_data ((intros, SOME elim, nparams), no_compilation))) thy else thy end @@ -679,16 +720,24 @@ (mk_casesrule (ProofContext.init thy) pred nparams pre_intros) in register_predicate (constname, pre_intros, pre_elim, nparams) thy end -fun set_generator_name pred mode name = +fun set_random_function_name pred mode name = let - val set = (apsnd o apsnd3 o cons) (mode, mk_function_data (name, NONE)) + val set = (apsnd o apsnd4) (fn (x, y) => (true, cons (mode, mk_function_data (name, NONE)) y)) in PredData.map (Graph.map_node pred (map_pred_data set)) end fun set_depth_limited_function_name pred mode name = let - val set = (apsnd o aptrd3 o cons) (mode, mk_function_data (name, NONE)) + val set = (apsnd o aptrd4) (fn (x, y) => (true, cons (mode, mk_function_data (name, NONE)) y)) + in + PredData.map (Graph.map_node pred (map_pred_data set)) + end + +fun set_annotated_function_name pred mode name = + let + val set = (apsnd o apfourth4) + (fn (x, y) => (true, cons (mode, mk_function_data (name, NONE)) y)) in PredData.map (Graph.map_node pred (map_pred_data set)) end @@ -715,19 +764,6 @@ fun mk_not (CompilationFuns funs) = #mk_not funs fun mk_map (CompilationFuns funs) = #mk_map funs -fun funT_of compfuns (iss, is) T = - let - val Ts = binder_types T - val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts - val paramTs' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss paramTs - in - (paramTs' @ inargTs) ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs)) - end; - -fun mk_fun_of compfuns thy (name, T) mode = - Const (predfun_name_of thy name mode, funT_of compfuns mode T) - - structure PredicateCompFuns = struct @@ -815,9 +851,9 @@ fun mk_map T1 T2 tf tp = Const (@{const_name Quickcheck.map}, (T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp -val compfuns = CompilationFuns {mk_predT = mk_randompredT, dest_predT = dest_randompredT, mk_bot = mk_bot, - mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not, - mk_map = mk_map}; +val compfuns = CompilationFuns {mk_predT = mk_randompredT, dest_predT = dest_randompredT, + mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, + mk_not = mk_not, mk_map = mk_map}; end; (* for external use with interactive mode *) @@ -829,25 +865,41 @@ val T = dest_randomT (fastype_of random) in Const (@{const_name Quickcheck.Random}, (@{typ Random.seed} --> - HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) --> + HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) --> RandomPredCompFuns.mk_randompredT T) $ random end; +(* function types and names of different compilations *) + +fun funT_of compfuns (iss, is) T = + let + val Ts = binder_types T + val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts + val paramTs' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss paramTs + in + (paramTs' @ inargTs) ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs)) + end; + fun depth_limited_funT_of compfuns (iss, is) T = let val Ts = binder_types T val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts - val paramTs' = map2 (fn SOME is => depth_limited_funT_of compfuns ([], is) | NONE => I) iss paramTs + val paramTs' = + map2 (fn SOME is => depth_limited_funT_of compfuns ([], is) | NONE => I) iss paramTs in (paramTs' @ inargTs @ [@{typ bool}, @{typ "code_numeral"}]) ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs)) - end; + end; -fun mk_depth_limited_fun_of compfuns thy (name, T) mode = - Const (depth_limited_function_name_of thy name mode, depth_limited_funT_of compfuns mode T) - -fun mk_generator_of compfuns thy (name, T) mode = - Const (generator_name_of thy name mode, depth_limited_funT_of compfuns mode T) +fun random_function_funT_of (iss, is) T = + let + val Ts = binder_types T + val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts + val paramTs' = map2 (fn SOME is => random_function_funT_of ([], is) | NONE => I) iss paramTs + in + (paramTs' @ inargTs @ [@{typ code_numeral}]) ---> + (mk_predT RandomPredCompFuns.compfuns (HOLogic.mk_tupleT outargTs)) + end (* Mode analysis *) @@ -860,7 +912,8 @@ fun check t = (case strip_comb t of (Free _, []) => true | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of - (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts + (SOME (i, Tname), Type (Tname', _)) => + length ts = i andalso Tname = Tname' andalso forall check ts | _ => false) | _ => false) in check end; @@ -993,11 +1046,14 @@ (filter_out (equal p) ps) | _ => let - val all_generator_vs = all_subsets (subtract (op =) vs prem_vs) |> sort (int_ord o (pairself length)) + val all_generator_vs = all_subsets (subtract (op =) vs prem_vs) + |> sort (int_ord o (pairself length)) in case (find_first (fn generator_vs => is_some - (select_mode_prem thy modes' (union (op =) vs generator_vs) ps)) all_generator_vs) of - SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps) + (select_mode_prem thy modes' (union (op =) vs generator_vs) ps)) + all_generator_vs) of + SOME generator_vs => check_mode_prems + ((map (generator vTs) generator_vs) @ acc_ps) (union (op =) vs generator_vs) ps | NONE => NONE end) @@ -1073,14 +1129,14 @@ let val prednames = map fst clauses val extra_modes' = all_modes_of thy - val gen_modes = all_generator_modes_of thy + val gen_modes = all_random_modes_of thy |> filter_out (fn (name, _) => member (op =) prednames name) val starting_modes = remove_from extra_modes' all_modes fun eq_mode (m1, m2) = (m1 = m2) val modes = fixp (fn modes => - map (check_modes_pred options true thy param_vs clauses extra_modes' (gen_modes @ modes)) modes) - starting_modes + map (check_modes_pred options true thy param_vs clauses extra_modes' + (gen_modes @ modes)) modes) starting_modes in AList.join (op =) (fn _ => fn ((mps1, mps2)) => @@ -1169,7 +1225,9 @@ datatype comp_modifiers = Comp_Modifiers of { - const_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string, + function_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string, + set_function_name : string -> Predicate_Compile_Aux.mode -> string -> theory -> theory, + function_name_prefix : string, funT_of : compilation_funs -> mode -> typ -> typ, additional_arguments : string list -> term list, wrap_compilation : compilation_funs -> string -> typ -> mode -> term list -> term -> term, @@ -1178,7 +1236,9 @@ fun dest_comp_modifiers (Comp_Modifiers c) = c -val const_name_of = #const_name_of o dest_comp_modifiers +val function_name_of = #function_name_of o dest_comp_modifiers +val set_function_name = #set_function_name o dest_comp_modifiers +val function_name_prefix = #function_name_prefix o dest_comp_modifiers val funT_of = #funT_of o dest_comp_modifiers val additional_arguments = #additional_arguments o dest_comp_modifiers val wrap_compilation = #wrap_compilation o dest_comp_modifiers @@ -1200,7 +1260,8 @@ | map_params t = t in map_aterms map_params arg end -fun compile_match compilation_modifiers compfuns additional_arguments param_vs iss thy eqs eqs' out_ts success_t = +fun compile_match compilation_modifiers compfuns additional_arguments + param_vs iss thy eqs eqs' out_ts success_t = let val eqs'' = maps mk_eq eqs @ eqs' val eqs'' = @@ -1243,7 +1304,7 @@ val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params) val f' = case f of - Const (name, T) => Const (Comp_Mod.const_name_of compilation_modifiers thy name mode, + Const (name, T) => Const (Comp_Mod.function_name_of compilation_modifiers thy name mode, Comp_Mod.funT_of compilation_modifiers compfuns mode T) | Free (name, T) => Free (name, Comp_Mod.funT_of compilation_modifiers compfuns mode T) | _ => error ("PredicateCompiler: illegal parameter term") @@ -1251,23 +1312,26 @@ list_comb (f', params' @ args') end -fun compile_expr compilation_modifiers compfuns thy ((Mode (mode, _, ms)), t) inargs additional_arguments = +fun compile_expr compilation_modifiers compfuns thy ((Mode (mode, _, ms)), t) + inargs additional_arguments = case strip_comb t of (Const (name, T), params) => let val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params) - (*val mk_fun_of = if depth_limited then mk_depth_limited_fun_of else mk_fun_of*) - val name' = Comp_Mod.const_name_of compilation_modifiers thy name mode + val name' = Comp_Mod.function_name_of compilation_modifiers thy name mode val T' = Comp_Mod.funT_of compilation_modifiers compfuns mode T in (list_comb (Const (name', T'), params' @ inargs @ additional_arguments)) end | (Free (name, T), params) => - list_comb (Free (name, Comp_Mod.funT_of compilation_modifiers compfuns mode T), params @ inargs @ additional_arguments) + list_comb (Free (name, Comp_Mod.funT_of compilation_modifiers compfuns mode T), + params @ inargs @ additional_arguments) -fun compile_clause compilation_modifiers compfuns thy all_vs param_vs additional_arguments (iss, is) inp (ts, moded_ps) = +fun compile_clause compilation_modifiers compfuns thy all_vs param_vs additional_arguments + (iss, is) inp (ts, moded_ps) = let - val compile_match = compile_match compilation_modifiers compfuns additional_arguments param_vs iss thy + val compile_match = compile_match compilation_modifiers compfuns + additional_arguments param_vs iss thy fun check_constrt t (names, eqs) = if is_constrt thy t then (t, (names, eqs)) else let @@ -1302,10 +1366,11 @@ Prem (us, t) => let val (in_ts, out_ts''') = split_smode is us; - val in_ts = map (compile_arg compilation_modifiers compfuns additional_arguments - thy param_vs iss) in_ts + val in_ts = map (compile_arg compilation_modifiers compfuns + additional_arguments thy param_vs iss) in_ts val u = - compile_expr compilation_modifiers compfuns thy (mode, t) in_ts additional_arguments' + compile_expr compilation_modifiers compfuns thy + (mode, t) in_ts additional_arguments' val rest = compile_prems out_ts''' vs' names'' ps in (u, rest) @@ -1313,10 +1378,11 @@ | Negprem (us, t) => let val (in_ts, out_ts''') = split_smode is us - val in_ts = map (compile_arg compilation_modifiers compfuns additional_arguments - thy param_vs iss) in_ts + val in_ts = map (compile_arg compilation_modifiers compfuns + additional_arguments thy param_vs iss) in_ts val u = mk_not compfuns - (compile_expr compilation_modifiers compfuns thy (mode, t) in_ts additional_arguments') + (compile_expr compilation_modifiers compfuns thy + (mode, t) in_ts additional_arguments') val rest = compile_prems out_ts''' vs' names'' ps in (u, rest) @@ -1351,12 +1417,14 @@ val (Ts1, Ts2) = chop (length (fst mode)) (binder_types T) val (Us1, Us2) = split_smodeT (snd mode) Ts2 val Ts1' = - map2 (fn NONE => I | SOME is => Comp_Mod.funT_of compilation_modifiers compfuns ([], is)) (fst mode) Ts1 + map2 (fn NONE => I | SOME is => Comp_Mod.funT_of compilation_modifiers compfuns ([], is)) + (fst mode) Ts1 fun mk_input_term (i, NONE) = [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))] | mk_input_term (i, SOME pis) = case HOLogic.strip_tupleT (nth Ts2 (i - 1)) of [] => error "strange unit input" - | [T] => [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))] + | [T] => [Free (Name.variant (all_vs @ param_vs) + ("x" ^ string_of_int i), nth Ts2 (i - 1))] | Ts => let val vnames = Name.variant_list (all_vs @ param_vs) (map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j) @@ -1365,16 +1433,18 @@ else [HOLogic.mk_tuple (map Free (vnames ~~ map (fn j => nth Ts (j - 1)) pis))] end val in_ts = maps mk_input_term (snd mode) val params = map2 (fn s => fn T => Free (s, T)) param_vs Ts1' - val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers (all_vs @ param_vs) + val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers + (all_vs @ param_vs) val cl_ts = map (compile_clause compilation_modifiers compfuns thy all_vs param_vs additional_arguments mode (HOLogic.mk_tuple in_ts)) moded_cls; - val compilation = Comp_Mod.wrap_compilation compilation_modifiers compfuns s T mode additional_arguments + val compilation = Comp_Mod.wrap_compilation compilation_modifiers compfuns + s T mode additional_arguments (if null cl_ts then mk_bot compfuns (HOLogic.mk_tupleT Us2) else foldr1 (mk_sup compfuns) cl_ts) val fun_const = - Const (Comp_Mod.const_name_of compilation_modifiers thy s mode, + Const (Comp_Mod.function_name_of compilation_modifiers thy s mode, Comp_Mod.funT_of compilation_modifiers compfuns mode T) in HOLogic.mk_Trueprop @@ -1399,7 +1469,8 @@ val Ts = binder_types (fastype_of pred) val funtrm = Const (mode_id, funT) val (Ts1, Ts2) = chop (length iss) Ts; - val Ts1' = map2 (fn NONE => I | SOME is => funT_of (PredicateCompFuns.compfuns) ([], is)) iss Ts1 + val Ts1' = + map2 (fn NONE => I | SOME is => funT_of (PredicateCompFuns.compfuns) ([], is)) iss Ts1 val param_names = Name.variant_list [] (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1))); val params = map Free (param_names ~~ Ts1') @@ -1440,14 +1511,12 @@ val simprules = [defthm, @{thm eval_pred}, @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}] val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1 - val introthm = - Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y"]) [] introtrm - (fn _ => unfolddef_tac) + val introthm = Goal.prove (ProofContext.init thy) + (argnames @ param_names @ param_names' @ ["y"]) [] introtrm (fn _ => unfolddef_tac) val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT)); val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P) - val elimthm = - Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y", "P"]) [] elimtrm - (fn _ => unfolddef_tac) + val elimthm = Goal.prove (ProofContext.init thy) + (argnames @ param_names @ param_names' @ ["y", "P"]) [] elimtrm (fn _ => unfolddef_tac) in (introthm, elimthm) end; @@ -1455,7 +1524,8 @@ fun create_constname_of_mode thy prefix name mode = let fun string_of_mode mode = if null mode then "0" - else space_implode "_" (map (fn (i, NONE) => string_of_int i | (i, SOME pis) => string_of_int i ^ "p" + else space_implode "_" + (map (fn (i, NONE) => string_of_int i | (i, SOME pis) => string_of_int i ^ "p" ^ space_implode "p" (map string_of_int pis)) mode) val HOmode = space_implode "_and_" (fold (fn NONE => I | SOME mode => cons (string_of_mode mode)) (fst mode) []) @@ -1529,7 +1599,9 @@ val xin = Free (name_in, HOLogic.mk_tupleT Tins) val xout = Free (name_out, HOLogic.mk_tupleT Touts) val xarg = mk_arg xin xout pis T - in (((if null Tins then [] else [xin], if null Touts then [] else [xout]), xarg), name_in :: name_out :: names) end + in + (((if null Tins then [] else [xin], + if null Touts then [] else [xout]), xarg), name_in :: name_out :: names) end end val (xinoutargs, names) = fold_map mk_vars ((1 upto (length Ts2)) ~~ Ts2) param_names val (xinout, xargs) = split_list xinoutargs @@ -1563,46 +1635,22 @@ fold create_definition modes thy end; -fun create_definitions_of_depth_limited_functions preds (name, modes) thy = +fun define_functions comp_modifiers compfuns preds (name, modes) thy = let val T = AList.lookup (op =) preds name |> the fun create_definition mode thy = let - val mode_cname = create_constname_of_mode thy "depth_limited_" name mode - val funT = depth_limited_funT_of PredicateCompFuns.compfuns mode T + val function_name_prefix = Comp_Mod.function_name_prefix comp_modifiers + val mode_cname = create_constname_of_mode thy function_name_prefix name mode + val funT = Comp_Mod.funT_of comp_modifiers compfuns mode T in thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)] - |> set_depth_limited_function_name name mode mode_cname + |> Comp_Mod.set_function_name comp_modifiers name mode mode_cname end; in fold create_definition modes thy end; -fun generator_funT_of (iss, is) T = - let - val Ts = binder_types T - val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts - val paramTs' = map2 (fn SOME is => generator_funT_of ([], is) | NONE => I) iss paramTs - in - (paramTs' @ inargTs @ [@{typ code_numeral}]) ---> - (mk_predT RandomPredCompFuns.compfuns (HOLogic.mk_tupleT outargTs)) - end - -fun random_create_definitions preds (name, modes) thy = - let - val T = AList.lookup (op =) preds name |> the - fun create_definition mode thy = - let - val mode_cname = create_constname_of_mode thy "gen_" name mode - val funT = generator_funT_of mode T - in - thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)] - |> set_generator_name name mode mode_cname - end; - in - fold create_definition modes thy - end; - (* Proving equivalence of term *) fun is_Type (Type _) = true @@ -1752,7 +1800,8 @@ in rtac @{thm bindI} 1 THEN (if (is_some name) then - simp_tac (HOL_basic_ss addsimps [predfun_definition_of thy (the name) (iss, is)]) 1 + simp_tac (HOL_basic_ss addsimps + [predfun_definition_of thy (the name) (iss, is)]) 1 THEN rtac @{thm not_predI} 1 THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1 THEN (REPEAT_DETERM (atac 1)) @@ -1823,14 +1872,16 @@ THEN (print_tac "after splitting with split_asm rules") (* THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1) THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*) - THEN (REPEAT_DETERM_N (num_of_constrs - 1) (etac @{thm botE} 1 ORELSE etac @{thm botE} 2))) + THEN (REPEAT_DETERM_N (num_of_constrs - 1) + (etac @{thm botE} 1 ORELSE etac @{thm botE} 2))) THEN (assert_tac (Max_number_of_subgoals 2)) THEN (EVERY (map split_term_tac ts)) end else all_tac in split_term_tac (HOLogic.mk_tuple out_ts) - THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1) THEN (etac @{thm botE} 2)))) + THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1) + THEN (etac @{thm botE} 2)))) end (* VERY LARGE SIMILIRATIY to function prove_param @@ -1910,7 +1961,8 @@ THEN (print_tac "state before assumption matching") THEN (REPEAT (atac 1 ORELSE (CHANGED (asm_full_simp_tac (HOL_basic_ss' addsimps - [@{thm split_eta}, @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]) 1) + [@{thm split_eta}, @{thm "split_beta"}, @{thm "fst_conv"}, + @{thm "snd_conv"}, @{thm pair_collapse}]) 1) THEN print_tac "state after simp_tac:")))) | prove_prems2 out_ts ((p, mode as Mode ((iss, is), _, param_modes)) :: ps) = let @@ -1932,7 +1984,8 @@ print_tac "before neg prem 2" THEN etac @{thm bindE} 1 THEN (if is_some name then - full_simp_tac (HOL_basic_ss addsimps [predfun_definition_of thy (the name) (iss, is)]) 1 + full_simp_tac (HOL_basic_ss addsimps + [predfun_definition_of thy (the name) (iss, is)]) 1 THEN etac @{thm not_predE} 1 THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1 THEN (EVERY (map (prove_param2 thy) (param_modes ~~ params))) @@ -2027,9 +2080,10 @@ fun dest_prem thy params t = (case strip_comb t of (v as Free _, ts) => if v mem params then Prem (ts, v) else Sidecond t - | (c as Const (@{const_name Not}, _), [t]) => (case dest_prem thy params t of + | (c as Const (@{const_name Not}, _), [t]) => (case dest_prem thy params t of Prem (ts, t) => Negprem (ts, t) - | Negprem _ => error ("Double negation not allowed in premise: " ^ (Syntax.string_of_term_global thy (c $ t))) + | Negprem _ => error ("Double negation not allowed in premise: " ^ + Syntax.string_of_term_global thy (c $ t)) | Sidecond t => Sidecond (c $ t)) | (c as Const (s, _), ts) => if is_registered thy s then @@ -2044,14 +2098,17 @@ val nparams = nparams_of thy (hd prednames) val preds = map (fn c => Const (c, Sign.the_const_type thy c)) prednames val (preds, intrs) = unify_consts thy preds intrs - val ([preds, intrs], _) = fold_burrow (Variable.import_terms false) [preds, intrs] (ProofContext.init thy) + val ([preds, intrs], _) = fold_burrow (Variable.import_terms false) [preds, intrs] + (ProofContext.init thy) val preds = map dest_Const preds - val extra_modes = all_modes_of thy |> filter_out (fn (name, _) => member (op =) prednames name) + val extra_modes = all_modes_of thy + |> filter_out (fn (name, _) => member (op =) prednames name) val params = case intrs of [] => let val (paramTs, _) = chop nparams (binder_types (snd (hd preds))) - val param_names = Name.variant_list [] (map (fn i => "p" ^ string_of_int i) (1 upto length paramTs)) + val param_names = Name.variant_list [] (map (fn i => "p" ^ string_of_int i) + (1 upto length paramTs)) in map Free (param_names ~~ paramTs) end | intr :: _ => fst (chop nparams (snd (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))))) @@ -2087,12 +2144,13 @@ [] => [(i + 1, NONE)] | [U] => [(i + 1, NONE)] | Us => (i + 1, NONE) :: - (map (pair (i + 1) o SOME) (subtract (op =) [[], 1 upto (length Us)] (subsets 1 (length Us))))) + (map (pair (i + 1) o SOME) + (subtract (op =) [[], 1 upto (length Us)] (subsets 1 (length Us))))) Ts) in cprod (cprods (map (fn T => case strip_type T of - (Rs as _ :: _, Type ("bool", [])) => map SOME (all_smodes_of_typs Rs) | _ => [NONE]) Ts), - all_smodes_of_typs Us) + (Rs as _ :: _, Type ("bool", [])) => + map SOME (all_smodes_of_typs Rs) | _ => [NONE]) Ts), all_smodes_of_typs Us) end val all_modes = map (fn (s, T) => (s, modes_of_typ T)) preds in (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) end; @@ -2180,7 +2238,7 @@ { compile_preds : theory -> string list -> string list -> (string * typ) list -> (moded_clause list) pred_mode_table -> term pred_mode_table, - create_definitions: (string * typ) list -> string * mode list -> theory -> theory, + define_functions : (string * typ) list -> string * mode list -> theory -> theory, infer_modes : options -> theory -> (string * mode list) list -> (string * mode list) list -> string list -> (string * (term list * indprem list) list) list -> moded_clause list pred_mode_table, @@ -2189,7 +2247,7 @@ -> moded_clause list pred_mode_table -> term pred_mode_table -> thm pred_mode_table, add_code_equations : theory -> int -> (string * typ) list -> (string * thm list) list -> (string * thm list) list, - are_not_defined : theory -> string list -> bool, + defined : theory -> string -> bool, qname : bstring } @@ -2197,19 +2255,21 @@ fun add_equations_of steps options prednames thy = let fun dest_steps (Steps s) = s - val _ = print_step options ("Starting predicate compiler for predicates " ^ commas prednames ^ "...") + val _ = print_step options + ("Starting predicate compiler for predicates " ^ commas prednames ^ "...") (*val _ = check_intros_elim_match thy prednames*) (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*) val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) = prepare_intrs thy prednames (maps (intros_of thy) prednames) val _ = print_step options "Infering modes..." - val moded_clauses = #infer_modes (dest_steps steps) options thy extra_modes all_modes param_vs clauses + val moded_clauses = + #infer_modes (dest_steps steps) options thy extra_modes all_modes param_vs clauses val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses val _ = check_expected_modes options modes val _ = print_modes options modes (*val _ = print_moded_clauses thy moded_clauses*) val _ = print_step options "Defining executable functions..." - val thy' = fold (#create_definitions (dest_steps steps) preds) modes thy + val thy' = fold (#define_functions (dest_steps steps) preds) modes thy |> Theory.checkpoint val _ = print_step options "Compiling equations..." val compiled_terms = @@ -2236,7 +2296,8 @@ val (G', v) = case try (Graph.get_node G) key of SOME v => (G, v) | NONE => (Graph.new_node (key, value_of key) G, value_of key) - val (G'', visited') = fold (extend' value_of edges_of) (subtract (op =) visited (edges_of (key, v))) + val (G'', visited') = fold (extend' value_of edges_of) + (subtract (op =) visited (edges_of (key, v))) (G', key :: visited) in (fold (Graph.add_edge o (pair key)) (edges_of (key, v)) G'', visited') @@ -2247,22 +2308,26 @@ fun gen_add_equations steps options names thy = let fun dest_steps (Steps s) = s - val thy' = PredData.map (fold (extend (fetch_pred_data thy) (depending_preds_of thy)) names) thy + val thy' = thy + |> PredData.map (fold (extend (fetch_pred_data thy) (depending_preds_of thy)) names) |> Theory.checkpoint; fun strong_conn_of gr keys = Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr) val scc = strong_conn_of (PredData.get thy') names val thy'' = fold_rev (fn preds => fn thy => - if #are_not_defined (dest_steps steps) thy preds then - add_equations_of steps options preds thy else thy) + if not (forall (#defined (dest_steps steps) thy) preds) then + add_equations_of steps options preds thy + else thy) scc thy' |> Theory.checkpoint in thy'' end (* different instantiantions of the predicate compiler *) val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers - {const_name_of = predfun_name_of : (theory -> string -> mode -> string), + {function_name_of = predfun_name_of : (theory -> string -> mode -> string), + set_function_name = (fn _ => fn _ => fn _ => I), + function_name_prefix = "", funT_of = funT_of : (compilation_funs -> mode -> typ -> typ), additional_arguments = K [], wrap_compilation = K (K (K (K (K I)))) @@ -2271,8 +2336,10 @@ } val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers - {const_name_of = depth_limited_function_name_of, + {function_name_of = depth_limited_function_name_of, + set_function_name = set_depth_limited_function_name, funT_of = depth_limited_funT_of : (compilation_funs -> mode -> typ -> typ), + function_name_prefix = "depth_limited_", additional_arguments = fn names => let val [depth_name, polarity_name] = Name.variant_list names ["depth", "polarity"] @@ -2289,7 +2356,8 @@ in if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"}) $ (if_const $ polarity $ mk_bot compfuns (dest_predT compfuns T') - $ (if full_mode then mk_single compfuns HOLogic.unit else Const (@{const_name undefined}, T'))) + $ (if full_mode then mk_single compfuns HOLogic.unit else + Const (@{const_name undefined}, T'))) $ compilation end, transform_additional_arguments = @@ -2304,39 +2372,62 @@ } val random_comp_modifiers = Comp_Mod.Comp_Modifiers - {const_name_of = generator_name_of, - funT_of = K generator_funT_of : (compilation_funs -> mode -> typ -> typ), + {function_name_of = random_function_name_of, + set_function_name = set_random_function_name, + function_name_prefix = "random", + funT_of = K random_function_funT_of : (compilation_funs -> mode -> typ -> typ), additional_arguments = fn names => [Free (Name.variant names "size", @{typ code_numeral})], wrap_compilation = K (K (K (K (K I)))) : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), transform_additional_arguments = K I : (indprem -> term list -> term list) } +val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers + {function_name_of = annotated_function_name_of, + set_function_name = set_annotated_function_name, + function_name_prefix = "annotated", + funT_of = funT_of : (compilation_funs -> mode -> typ -> typ), + additional_arguments = K [], + wrap_compilation = + fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation => + mk_tracing ("calling predicate " ^ s ^ " with mode " ^ string_of_mode mode) compilation, + transform_additional_arguments = K I : (indprem -> term list -> term list) + } + val add_equations = gen_add_equations (Steps {infer_modes = infer_modes, - create_definitions = create_definitions, + define_functions = create_definitions, compile_preds = compile_preds predicate_comp_modifiers PredicateCompFuns.compfuns, prove = prove, add_code_equations = add_code_equations, - are_not_defined = fn thy => forall (null o modes_of thy), + defined = defined_functions, qname = "equation"}) val add_depth_limited_equations = gen_add_equations (Steps {infer_modes = infer_modes, - create_definitions = create_definitions_of_depth_limited_functions, + define_functions = define_functions depth_limited_comp_modifiers PredicateCompFuns.compfuns, compile_preds = compile_preds depth_limited_comp_modifiers PredicateCompFuns.compfuns, prove = prove_by_skip, add_code_equations = K (K (K I)), - are_not_defined = fn thy => forall (null o depth_limited_modes_of thy), + defined = defined_depth_limited_functions, qname = "depth_limited_equation"}) +val add_annotated_equations = gen_add_equations + (Steps {infer_modes = infer_modes, + define_functions = define_functions annotated_comp_modifiers PredicateCompFuns.compfuns, + compile_preds = compile_preds annotated_comp_modifiers PredicateCompFuns.compfuns, + prove = prove_by_skip, + add_code_equations = K (K (K I)), + defined = defined_annotated_functions, + qname = "annotated_equation"}) + val add_quickcheck_equations = gen_add_equations (Steps {infer_modes = infer_modes_with_generator, - create_definitions = random_create_definitions, + define_functions = define_functions random_comp_modifiers RandomPredCompFuns.compfuns, compile_preds = compile_preds random_comp_modifiers RandomPredCompFuns.compfuns, prove = prove_by_skip, add_code_equations = K (K (K I)), - are_not_defined = fn thy => forall (null o random_modes_of thy), + defined = defined_random_functions, qname = "random_equation"}) (** user interface **) @@ -2396,6 +2487,8 @@ add_quickcheck_equations options [const]) else if is_depth_limited options then add_depth_limited_equations options [const] + else if is_annotated options then + add_annotated_equations options [const] else add_equations options [const])) end @@ -2409,11 +2502,12 @@ (* transformation for code generation *) val eval_ref = Unsynchronized.ref (NONE : (unit -> term Predicate.pred) option); -val random_eval_ref = Unsynchronized.ref (NONE : (unit -> int * int -> term Predicate.pred * (int * int)) option); +val random_eval_ref = + Unsynchronized.ref (NONE : (unit -> int * int -> term Predicate.pred * (int * int)) option); (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*) -(* TODO: *) -fun analyze_compr thy compfuns (depth_limit, random) t_compr = +(* TODO: make analyze_compr generic with respect to the compilation modifiers*) +fun analyze_compr thy compfuns param_user_modes (depth_limit, (random, annotated)) t_compr = let val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t_compr); @@ -2424,9 +2518,17 @@ (fn (i, t) => case t of Bound j => if j < length Ts then NONE else SOME (i+1) | _ => SOME (i+1)) args); (*FIXME dangling bounds should not occur*) val user_mode' = map (rpair NONE) user_mode - val all_modes_of = if random then all_generator_modes_of else all_modes_of - (*val compile_expr = if random then compile_gen_expr else compile_expr*) - val modes = filter (fn Mode (_, is, _) => is = user_mode') + val all_modes_of = if random then all_random_modes_of else all_modes_of + fun fits_to is NONE = true + | fits_to is (SOME pm) = (is = pm) + fun valid ((SOME (Mode (_, is, ms))) :: ms') (pm :: pms) = + fits_to is pm andalso valid (ms @ ms') pms + | valid (NONE :: ms') pms = valid ms' pms + | valid [] [] = true + | valid [] _ = error "Too many mode annotations" + | valid (SOME _ :: _) [] = error "Not enough mode annotations" + val modes = filter (fn Mode (_, is, ms) => is = user_mode' + andalso (the_default true (Option.map (valid ms) param_user_modes))) (modes_of_term (all_modes_of thy) (list_comb (pred, params))); val m = case modes of [] => error ("No mode possible for comprehension " @@ -2440,10 +2542,11 @@ NONE => (if random then [@{term "5 :: code_numeral"}] else []) | SOME d => [@{term "True"}, HOLogic.mk_number @{typ "code_numeral"} d] val comp_modifiers = - case depth_limit of NONE => - (if random then random_comp_modifiers else predicate_comp_modifiers) | SOME _ => depth_limited_comp_modifiers - val mk_fun_of = if random then mk_generator_of else - if (is_some depth_limit) then mk_depth_limited_fun_of else mk_fun_of + case depth_limit of + NONE => + (if random then random_comp_modifiers else + if annotated then annotated_comp_modifiers else predicate_comp_modifiers) + | SOME _ => depth_limited_comp_modifiers val t_pred = compile_expr comp_modifiers compfuns thy (m, list_comb (pred, params)) inargs additional_arguments; val t_eval = if null outargs then t_pred else @@ -2461,10 +2564,10 @@ in mk_map compfuns T_pred T_compr arrange t_pred end in t_eval end; -fun eval thy (options as (depth_limit, random)) t_compr = +fun eval thy param_user_modes (options as (depth_limit, (random, annotated))) t_compr = let val compfuns = if random then RandomPredCompFuns.compfuns else PredicateCompFuns.compfuns - val t = analyze_compr thy compfuns options t_compr; + val t = analyze_compr thy compfuns param_user_modes options t_compr; val T = dest_predT compfuns (fastype_of t); val t' = mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t; val eval = @@ -2476,15 +2579,16 @@ Code_ML.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref) Predicate.map thy t' [] in (T, eval) end; -fun values ctxt options k t_compr = +fun values ctxt param_user_modes options k t_compr = let val thy = ProofContext.theory_of ctxt; - val (T, ts) = eval thy options t_compr; + val (T, ts) = eval thy param_user_modes options t_compr; val (ts, _) = Predicate.yieldn k ts; val setT = HOLogic.mk_setT T; val elemsT = HOLogic.mk_set T ts; + val cont = Free ("...", setT) in if k = ~1 orelse length ts < k then elemsT - else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ t_compr + else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ cont end; (* fun random_values ctxt k t = @@ -2494,35 +2598,16 @@ in end; *) -fun values_cmd modes options k raw_t state = +fun values_cmd print_modes param_user_modes options k raw_t state = let val ctxt = Toplevel.context_of state; val t = Syntax.read_term ctxt raw_t; - val t' = values ctxt options k t; + val t' = values ctxt param_user_modes options k t; val ty' = Term.type_of t'; val ctxt' = Variable.auto_fixes t' ctxt; - val p = PrintMode.with_modes modes (fn () => + val p = PrintMode.with_modes print_modes (fn () => Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); in Pretty.writeln p end; -local structure P = OuterParse in - -val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) []; - -val options = - let - val depth_limit = Scan.optional (Args.$$$ "depth_limit" |-- P.$$$ "=" |-- P.nat >> SOME) NONE - val random = Scan.optional (Args.$$$ "random" >> K true) false - in - Scan.optional (P.$$$ "[" |-- depth_limit -- random --| P.$$$ "]") (NONE, false) - end - -val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag - (opt_modes -- options -- Scan.optional P.nat ~1 -- P.term - >> (fn (((modes, options), k), t) => Toplevel.no_timing o Toplevel.keep - (values_cmd modes options k t))); - end; - -end; diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sat Nov 07 08:17:53 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sat Nov 07 08:18:12 2009 +0100 @@ -161,7 +161,9 @@ fun make_const_spec_table options thy = let - fun store ignore_const f = fold (store_thm_in_table options ignore_const thy) (map (Thm.transfer thy) (f (ProofContext.init thy))) + fun store ignore_const f = + fold (store_thm_in_table options ignore_const thy) + (map (Thm.transfer thy) (f (ProofContext.init thy))) val table = Symtab.empty |> store [] Predicate_Compile_Alternative_Defs.get val ignore_consts = Symtab.keys table diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Sat Nov 07 08:17:53 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Sat Nov 07 08:18:12 2009 +0100 @@ -33,7 +33,8 @@ inductify = false, random = false, - depth_limited = false + depth_limited = false, + annotated = false } fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs @@ -86,11 +87,11 @@ (* |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*) |> Predicate_Compile_Core.add_quickcheck_equations options [full_constname] val depth_limited_modes = Predicate_Compile_Core.depth_limited_modes_of thy'' full_constname - val modes = Predicate_Compile_Core.generator_modes_of thy'' full_constname + val modes = Predicate_Compile_Core.random_modes_of thy'' full_constname val prog = if member (op =) modes ([], []) then let - val name = Predicate_Compile_Core.generator_name_of thy'' full_constname ([], []) + val name = Predicate_Compile_Core.random_function_name_of thy'' full_constname ([], []) val T = [@{typ code_numeral}] ---> (mk_randompredT (HOLogic.mk_tupleT (map snd vs'))) in Const (name, T) $ Bound 0 end (*else if member (op =) depth_limited_modes ([], []) then diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/ex/Induction_Schema.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Induction_Schema.thy Sat Nov 07 08:18:12 2009 +0100 @@ -0,0 +1,48 @@ +(* Title: HOL/ex/Induction_Schema.thy + Author: Alexander Krauss, TU Muenchen +*) + +header {* Examples of automatically derived induction rules *} + +theory Induction_Schema +imports Main +begin + +subsection {* Some simple induction principles on nat *} + +lemma nat_standard_induct: (* cf. Nat.thy *) + "\P 0; \n. P n \ P (Suc n)\ \ P x" +by induction_schema (pat_completeness, lexicographic_order) + +lemma nat_induct2: + "\ P 0; P (Suc 0); \k. P k ==> P (Suc k) ==> P (Suc (Suc k)) \ + \ P n" +by induction_schema (pat_completeness, lexicographic_order) + +lemma minus_one_induct: + "\\n::nat. (n \ 0 \ P (n - 1)) \ P n\ \ P x" +by induction_schema (pat_completeness, lexicographic_order) + +theorem diff_induct: (* cf. Nat.thy *) + "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==> + (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n" +by induction_schema (pat_completeness, lexicographic_order) + +lemma list_induct2': (* cf. List.thy *) + "\ P [] []; + \x xs. P (x#xs) []; + \y ys. P [] (y#ys); + \x xs y ys. P xs ys \ P (x#xs) (y#ys) \ + \ P xs ys" +by induction_schema (pat_completeness, lexicographic_order) + +theorem even_odd_induct: + assumes "R 0" + assumes "Q 0" + assumes "\n. Q n \ R (Suc n)" + assumes "\n. R n \ Q (Suc n)" + shows "R n" "Q n" + using assms +by induction_schema (pat_completeness+, lexicographic_order) + +end \ No newline at end of file diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/ex/Induction_Scheme.thy --- a/src/HOL/ex/Induction_Scheme.thy Sat Nov 07 08:17:53 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,49 +0,0 @@ -(* Title: HOL/ex/Induction_Scheme.thy - ID: $Id$ - Author: Alexander Krauss, TU Muenchen -*) - -header {* Examples of automatically derived induction rules *} - -theory Induction_Scheme -imports Main -begin - -subsection {* Some simple induction principles on nat *} - -lemma nat_standard_induct: (* cf. Nat.thy *) - "\P 0; \n. P n \ P (Suc n)\ \ P x" -by induct_scheme (pat_completeness, lexicographic_order) - -lemma nat_induct2: - "\ P 0; P (Suc 0); \k. P k ==> P (Suc k) ==> P (Suc (Suc k)) \ - \ P n" -by induct_scheme (pat_completeness, lexicographic_order) - -lemma minus_one_induct: - "\\n::nat. (n \ 0 \ P (n - 1)) \ P n\ \ P x" -by induct_scheme (pat_completeness, lexicographic_order) - -theorem diff_induct: (* cf. Nat.thy *) - "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==> - (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n" -by induct_scheme (pat_completeness, lexicographic_order) - -lemma list_induct2': (* cf. List.thy *) - "\ P [] []; - \x xs. P (x#xs) []; - \y ys. P [] (y#ys); - \x xs y ys. P xs ys \ P (x#xs) (y#ys) \ - \ P xs ys" -by induct_scheme (pat_completeness, lexicographic_order) - -theorem even_odd_induct: - assumes "R 0" - assumes "Q 0" - assumes "\n. Q n \ R (Suc n)" - assumes "\n. R n \ Q (Suc n)" - shows "R n" "Q n" - using assms -by induct_scheme (pat_completeness+, lexicographic_order) - -end \ No newline at end of file diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy --- a/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy Sat Nov 07 08:17:53 2009 +0100 +++ b/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy Sat Nov 07 08:18:12 2009 +0100 @@ -9,7 +9,9 @@ quickcheck[generator=predicate_compile] oops +(* TODO: some error with doubled negation *) lemma "x \ {Suc 0, Suc (Suc 0)} ==> x \ Suc 0" +(*quickcheck[generator=predicate_compile]*) oops lemma "x \ {Suc 0, Suc (Suc 0)} ==> x = Suc 0" @@ -23,12 +25,17 @@ section {* Numerals *} lemma - "x \ {1, 2, (3::nat)} ==> x < 3" + "x \ {1, 2, (3::nat)} ==> x = 1 \ x = 2" +quickcheck[generator=predicate_compile] +oops + +lemma "x \ {1, 2, (3::nat)} ==> x < 3" (*quickcheck[generator=predicate_compile]*) oops + lemma - "x \ {1, 2} \ {3, 4} ==> x > 4" -(*quickcheck[generator=predicate_compile]*) + "x \ {1, 2} \ {3, 4} ==> x = (1::nat) \ x = (2::nat)" +quickcheck[generator=predicate_compile] oops section {* Context Free Grammar *} diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Sat Nov 07 08:17:53 2009 +0100 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Sat Nov 07 08:18:12 2009 +0100 @@ -188,13 +188,23 @@ (*values "{x. one_or_two x}"*) values [random] "{x. one_or_two x}" -definition one_or_two': - "one_or_two' == {1, (2::nat)}" +inductive one_or_two' :: "nat => bool" +where + "one_or_two' 1" +| "one_or_two' 2" + +code_pred one_or_two' . +thm one_or_two'.equation -code_pred [inductify] one_or_two' . -thm one_or_two'.equation -(* TODO: handling numerals *) -(*values "{x. one_or_two' x}"*) +values "{x. one_or_two' x}" + +definition one_or_two'': + "one_or_two'' == {1, (2::nat)}" + +code_pred [inductify] one_or_two'' . +thm one_or_two''.equation + +values "{x. one_or_two'' x}" subsection {* even predicate *} @@ -250,10 +260,12 @@ code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append . code_pred [depth_limited] append . code_pred [random] append . +code_pred [annotated] append . thm append.equation thm append.depth_limited_equation thm append.random_equation +thm append.annotated_equation values "{(ys, xs). append xs ys [0, Suc 0, 2]}" values "{zs. append [0, Suc 0, 2] [17, 8] zs}" @@ -264,6 +276,7 @@ value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])" value [code] "Predicate.the (append_3 ([]::int list))" + text {* tricky case with alternative rules *} inductive append2 @@ -460,13 +473,13 @@ values "{m. succ 0 m}" values "{m. succ m 0}" -(* FIXME: why does this not terminate? -- value chooses mode [] --> [1] and then starts enumerating all successors *) +text {* values command needs mode annotation of the parameter succ +to disambiguate which mode is to be chosen. *} -(* -values 20 "{n. tranclp succ 10 n}" -values "{n. tranclp succ n 10}" +values [mode: [1]] 20 "{n. tranclp succ 10 n}" +values [mode: [2]] 10 "{n. tranclp succ n 10}" values 20 "{(n, m). tranclp succ n m}" -*) + subsection {* IMP *} @@ -529,10 +542,13 @@ code_pred steps . +values 3 + "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}" + values 5 "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}" -(* FIXME +(* FIXME: values 3 "{(a,q). step (par nil nil) a q}" *) @@ -645,6 +661,7 @@ thm set_of.equation code_pred [inductify] is_ord . +thm is_ord_aux.equation thm is_ord.equation @@ -699,7 +716,7 @@ code_pred [inductify] take . code_pred [inductify] drop . code_pred [inductify] zip . -code_pred [inductify] upt . +(*code_pred [inductify] upt .*) code_pred [inductify] remdups . code_pred [inductify] remove1 . code_pred [inductify] removeAll . diff -r 22e5725be1f3 -r 31872dd275c8 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Sat Nov 07 08:17:53 2009 +0100 +++ b/src/HOL/ex/ROOT.ML Sat Nov 07 08:18:12 2009 +0100 @@ -24,7 +24,7 @@ "Binary", "Recdefs", "Fundefs", - "Induction_Scheme", + "Induction_Schema", "InductiveInvariant_examples", "LocaleTest2", "Records",