# HG changeset patch # User paulson # Date 1331225364 0 # Node ID 52e9770e0107d5eb18674e5f143581c0c13bef42 # Parent 49b91b716cbeab62e5302a0579d8ca74db9e7a9d# Parent be56a254d880ea708677f5990a258a7a676b390a Structured and calculation-based proofs (with new trans rules!) diff -r 49b91b716cbe -r 52e9770e0107 NEWS --- a/NEWS Thu Mar 08 16:43:29 2012 +0000 +++ b/NEWS Thu Mar 08 16:49:24 2012 +0000 @@ -83,11 +83,15 @@ used as predicates by "%x. x : S" and predicates P accidentally used as sets by "{x. P x}". Corresponding proofs in a first step should be pruned from any tinkering with former theorems mem_def and -Collect_def. For developments which deliberately mixed predicates and +Collect_def as far as possible. +For developments which deliberately mixed predicates and sets, a planning step is necessary to determine what should become a predicate and what a set. It can be helpful to carry out that step in Isabelle2011-1 before jumping right into the current release. +* Code generation by default implements sets as container type rather +than predicates. INCOMPATIBILITY. + * New type synonym 'a rel = ('a * 'a) set * More default pred/set conversions on a couple of relation operations diff -r 49b91b716cbe -r 52e9770e0107 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Mar 08 16:43:29 2012 +0000 +++ b/src/HOL/IsaMakefile Thu Mar 08 16:49:24 2012 +0000 @@ -41,7 +41,6 @@ HOL-HOL4 \ HOL-HOL4-Imported \ HOL-HOL_Light \ -# HOL-HOL_Light-Imported \ FIXME not operative at the moment \ HOL-IMPP \ HOL-IOA \ IOA-ABP \ diff -r 49b91b716cbe -r 52e9770e0107 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Mar 08 16:43:29 2012 +0000 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Mar 08 16:49:24 2012 +0000 @@ -17,12 +17,14 @@ val force_sosK = "force_sos" val max_relevantK = "max_relevant" val max_callsK = "max_calls" -val minimizeK = "minimize" +val minimizeK = "minimize" (*refers to minimization attempted by Mirabelle*) val minimize_timeoutK = "minimize_timeout" val metis_ftK = "metis_ft" val reconstructorK = "reconstructor" - -val preplay_timeout = "4" +val preplay_timeoutK = "preplay_timeout" +val sh_minimizeK = "sh_minimize" (*refers to minimizer run within Sledgehammer*) +val max_new_mono_instancesK = "max_new_mono_instances" +val max_mono_itersK = "max_mono_iters" fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: " fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): " @@ -31,6 +33,17 @@ val separator = "-----" +val preplay_timeout_default = "4" +(*FIXME sensible to have Mirabelle-level Sledgehammer defaults?*) + +(*If a key is present in args then augment a list with its pair*) +(*This is used to avoid fixing default values at the Mirabelle level, and + instead use the default values of the tool (Sledgehammer in this case).*) +fun available_parameter args key label list = + let + val value = AList.lookup (op =) args key + in if is_some value then (label, the value) :: list else list end + datatype sh_data = ShData of { calls: int, @@ -363,8 +376,9 @@ SH_ERROR fun run_sh prover_name prover type_enc strict max_relevant slice lam_trans - uncurried_aliases e_weight_method force_sos hard_timeout timeout dir pos - st = + uncurried_aliases e_weight_method force_sos hard_timeout timeout + preplay_timeout sh_minimizeLST max_new_mono_instancesLST max_mono_itersLST + dir pos st = let val {context = ctxt, facts = chained_ths, goal} = Proof.goal st val i = 1 @@ -385,7 +399,7 @@ force_sos |> the_default I)) val params as {relevance_thresholds, max_relevant, slice, ...} = Sledgehammer_Isar.default_params ctxt - [("verbose", "true"), + ([("verbose", "true"), ("type_enc", type_enc), ("strict", strict), ("lam_trans", lam_trans |> the_default "smart"), @@ -394,6 +408,9 @@ ("slice", slice), ("timeout", string_of_int timeout), ("preplay_timeout", preplay_timeout)] + |> sh_minimizeLST (*don't confuse the two minimization flags*) + |> max_new_mono_instancesLST + |> max_mono_itersLST) val default_max_relevant = Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice prover_name @@ -481,11 +498,18 @@ val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30) (* always use a hard timeout, but give some slack so that the automatic minimizer has a chance to do its magic *) + val preplay_timeout = AList.lookup (op =) args preplay_timeoutK + |> the_default preplay_timeout_default + val sh_minimizeLST = available_parameter args sh_minimizeK "minimize" + val max_new_mono_instancesLST = + available_parameter args max_new_mono_instancesK max_new_mono_instancesK + val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK val hard_timeout = SOME (2 * timeout) val (msg, result) = run_sh prover_name prover type_enc strict max_relevant slice lam_trans - uncurried_aliases e_weight_method force_sos hard_timeout timeout dir pos - st + uncurried_aliases e_weight_method force_sos hard_timeout timeout + preplay_timeout sh_minimizeLST max_new_mono_instancesLST max_mono_itersLST + dir pos st in case result of SH_OK (time_isa, time_prover, names) => @@ -526,13 +550,22 @@ AList.lookup (op =) args minimize_timeoutK |> Option.map (fst o read_int o raw_explode) (* FIXME Symbol.explode (?) *) |> the_default 5 + val preplay_timeout = AList.lookup (op =) args preplay_timeoutK + |> the_default preplay_timeout_default + val sh_minimizeLST = available_parameter args sh_minimizeK "minimize" + val max_new_mono_instancesLST = + available_parameter args max_new_mono_instancesK max_new_mono_instancesK + val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK val params = Sledgehammer_Isar.default_params ctxt - [("provers", prover_name), + ([("provers", prover_name), ("verbose", "true"), ("type_enc", type_enc), ("strict", strict), ("timeout", string_of_int timeout), ("preplay_timeout", preplay_timeout)] + |> sh_minimizeLST (*don't confuse the two minimization flags*) + |> max_new_mono_instancesLST + |> max_mono_itersLST) val minimize = Sledgehammer_Minimize.minimize_facts prover_name params true 1 (Sledgehammer_Util.subgoal_count st) diff -r 49b91b716cbe -r 52e9770e0107 src/HOL/Mirabelle/lib/Tools/mirabelle --- a/src/HOL/Mirabelle/lib/Tools/mirabelle Thu Mar 08 16:43:29 2012 +0000 +++ b/src/HOL/Mirabelle/lib/Tools/mirabelle Thu Mar 08 16:49:24 2012 +0000 @@ -26,7 +26,7 @@ echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)" echo " -O DIR output directory for test data (default $out)" echo " -t TIMEOUT timeout for each action in seconds (default $timeout)" - echo " -q be quiet (suppress output of Isabelle process)" + echo " -q be quiet (suppress output of Isabelle process)" echo echo " Apply the given actions (i.e., automated proof tools)" echo " at all proof steps in the given theory files." diff -r 49b91b716cbe -r 52e9770e0107 src/HOL/Mirabelle/lib/scripts/mirabelle.pl --- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Thu Mar 08 16:43:29 2012 +0000 +++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Thu Mar 08 16:49:24 2012 +0000 @@ -67,7 +67,7 @@ $tools begin -setup {* +setup {* Config.put_global Mirabelle.logfile "$log_file" #> Config.put_global Mirabelle.timeout $timeout #> Config.put_global Mirabelle.start_line $start_line #> @@ -76,7 +76,9 @@ END -foreach (reverse(split(/:/, $actions))) { +@action_list = split(/:/, $actions); + +foreach (reverse(@action_list)) { if (m/([^[]*)(?:\[(.*)\])?/) { my ($name, $settings_str) = ($1, $2 || ""); $name =~ s/^([a-z])/\U$1/; @@ -88,8 +90,8 @@ $sep = ", "; } elsif (m/\s*(.*)\s*/) { - print SETUP_FILE "$sep(\"$1\", \"\")"; - $sep = ", "; + print SETUP_FILE "$sep(\"$1\", \"\")"; + $sep = ", "; } } print SETUP_FILE "] *}\n"; @@ -121,8 +123,8 @@ open(LOG_FILE, ">$log_file"); print LOG_FILE "Run of $new_thy_file with:\n"; -foreach $name (@action_names) { - print LOG_FILE " $name\n"; +foreach $action (@action_list) { + print LOG_FILE " $action\n"; } close(LOG_FILE); diff -r 49b91b716cbe -r 52e9770e0107 src/HOL/Relation.thy --- a/src/HOL/Relation.thy Thu Mar 08 16:43:29 2012 +0000 +++ b/src/HOL/Relation.thy Thu Mar 08 16:49:24 2012 +0000 @@ -60,16 +60,16 @@ subsubsection {* Conversions between set and predicate relations *} -lemma pred_equals_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)" +lemma pred_equals_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S) \<longleftrightarrow> R = S" by (simp add: set_eq_iff fun_eq_iff) -lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R = S)" +lemma pred_equals_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S) \<longleftrightarrow> R = S" by (simp add: set_eq_iff fun_eq_iff) -lemma pred_subset_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R \<subseteq> S)" +lemma pred_subset_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S) \<longleftrightarrow> R \<subseteq> S" by (simp add: subset_iff le_fun_def) -lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) \<le> (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R \<subseteq> S)" +lemma pred_subset_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<le> (\<lambda>x y. (x, y) \<in> S) \<longleftrightarrow> R \<subseteq> S" by (simp add: subset_iff le_fun_def) lemma bot_empty_eq (* CANDIDATE [pred_set_conv] *): "\<bottom> = (\<lambda>x. x \<in> {})" @@ -96,12 +96,54 @@ lemma sup_Un_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<squnion> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)" by (simp add: sup_fun_def) +lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> INTER S Collect)" + by (simp add: fun_eq_iff Inf_apply) + +(* CANDIDATE +lemma INF_Int_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Inter>S)" + by (simp add: fun_eq_iff INF_apply) + +lemma Inf_INT_eq2 [pred_set_conv]: "\<Sqinter>S = (\<lambda>x y. (x, y) \<in> INTER (prod_case ` S) Collect)" + by (simp add: fun_eq_iff Inf_apply INF_apply) + +lemma INF_Int_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Inter>S)" + by (simp add: fun_eq_iff INF_apply) + +lemma Sup_SUP_eq [pred_set_conv]: "\<Squnion>S = (\<lambda>x. x \<in> UNION S Collect)" + by (simp add: fun_eq_iff Sup_apply) + +lemma SUP_Sup_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Union>S)" + by (simp add: fun_eq_iff SUP_apply) + +lemma Sup_SUP_eq2 [pred_set_conv]: "\<Squnion>S = (\<lambda>x y. (x, y) \<in> UNION (prod_case ` S) Collect)" + by (simp add: fun_eq_iff Sup_apply SUP_apply) + +lemma SUP_Sup_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Union>S)" + by (simp add: fun_eq_iff SUP_apply) +*) + +(* CANDIDATE prefer those generalized versions: +lemma INF_INT_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i\<in>S. r i))" + by (simp add: INF_apply fun_eq_iff) + +lemma INF_INT_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i\<in>S. r i))" + by (simp add: INF_apply fun_eq_iff) +*) + lemma INF_INT_eq (* CANDIDATE [pred_set_conv] *): "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))" by (simp add: INF_apply fun_eq_iff) lemma INF_INT_eq2 (* CANDIDATE [pred_set_conv] *): "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i. r i))" by (simp add: INF_apply fun_eq_iff) +(* CANDIDATE prefer those generalized versions: +lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i\<in>S. r i))" + by (simp add: SUP_apply fun_eq_iff) + +lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i\<in>S. r i))" + by (simp add: SUP_apply fun_eq_iff) +*) + lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))" by (simp add: SUP_apply fun_eq_iff) diff -r 49b91b716cbe -r 52e9770e0107 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Thu Mar 08 16:43:29 2012 +0000 +++ b/src/HOL/Tools/inductive_set.ML Thu Mar 08 16:49:24 2012 +0000 @@ -227,12 +227,16 @@ fun mk_to_pred_inst thy fs = map (fn (x, ps) => let - val U = HOLogic.dest_setT (fastype_of x); - val x' = map_type (K (HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x; + val (Ts, T) = strip_type (fastype_of x); + val U = HOLogic.dest_setT T; + val x' = map_type + (K (Ts @ HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x; in (cterm_of thy x, - cterm_of thy (HOLogic.Collect_const U $ - HOLogic.mk_psplits ps U HOLogic.boolT x')) + cterm_of thy (fold_rev (Term.abs o pair "x") Ts + (HOLogic.Collect_const U $ + HOLogic.mk_psplits ps U HOLogic.boolT + (list_comb (x', map Bound (length Ts - 1 downto 0)))))) end) fs; fun mk_to_pred_eq p fs optfs' T thm = @@ -366,12 +370,16 @@ val insts = map (fn (x, ps) => let val Ts = binder_types (fastype_of x); - val T = HOLogic.mk_ptupleT ps Ts; - val x' = map_type (K (HOLogic.mk_setT T)) x + val l = length Ts; + val k = length ps; + val (Rs, Us) = chop (l - k - 1) Ts; + val T = HOLogic.mk_ptupleT ps Us; + val x' = map_type (K (Rs ---> HOLogic.mk_setT T)) x in (cterm_of thy x, cterm_of thy (fold_rev (Term.abs o pair "x") Ts - (HOLogic.mk_mem (HOLogic.mk_ptuple ps T (map Bound (length ps downto 0)), x')))) + (HOLogic.mk_mem (HOLogic.mk_ptuple ps T (map Bound (k downto 0)), + list_comb (x', map Bound (l - 1 downto k + 1)))))) end) fs; in thm |> diff -r 49b91b716cbe -r 52e9770e0107 src/Pure/General/properties.ML --- a/src/Pure/General/properties.ML Thu Mar 08 16:43:29 2012 +0000 +++ b/src/Pure/General/properties.ML Thu Mar 08 16:49:24 2012 +0000 @@ -6,30 +6,21 @@ signature PROPERTIES = sig - type entry = string * string - type T = entry list + type T = (string * string) list val defined: T -> string -> bool val get: T -> string -> string option - val get_int: T -> string -> int option - val put: entry -> T -> T - val put_int: string * int -> T -> T + val put: string * string -> T -> T val remove: string -> T -> T end; structure Properties: PROPERTIES = struct -type entry = string * string; -type T = entry list; +type T = (string * string) list; fun defined (props: T) name = AList.defined (op =) props name; - fun get (props: T) name = AList.lookup (op =) props name; -fun get_int props name = (case get props name of NONE => NONE | SOME s => Int.fromString s); - fun put entry (props: T) = AList.update (op =) entry props; -fun put_int (name, i) = put (name, signed_string_of_int i); - fun remove name (props: T) = AList.delete (op =) name props; end; diff -r 49b91b716cbe -r 52e9770e0107 src/Pure/PIDE/yxml.ML --- a/src/Pure/PIDE/yxml.ML Thu Mar 08 16:43:29 2012 +0000 +++ b/src/Pure/PIDE/yxml.ML Thu Mar 08 16:49:24 2012 +0000 @@ -21,7 +21,6 @@ val embed_controls: string -> string val detect: string -> bool val output_markup: Markup.T -> string * string - val element: string -> XML.attributes -> string list -> string val string_of_body: XML.body -> string val string_of: XML.tree -> string val parse_body: string -> XML.body @@ -62,15 +61,9 @@ if Markup.is_empty markup then Markup.no_output else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX); -fun element name atts body = - let val (pre, post) = output_markup (name, atts) - in pre ^ implode body ^ post end; - fun string_of_body body = let - fun attrib (a, x) = - Buffer.add Y #> - Buffer.add a #> Buffer.add "=" #> Buffer.add x; + fun attrib (a, x) = Buffer.add Y #> Buffer.add a #> Buffer.add "=" #> Buffer.add x; fun tree (XML.Elem ((name, atts), ts)) = Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #> trees ts #> @@ -99,7 +92,7 @@ (* structural errors *) -fun err msg = raise Fail ("Malformed YXML encoding: " ^ msg); +fun err msg = raise Fail ("Malformed YXML: " ^ msg); fun err_attribute () = err "bad attribute"; fun err_element () = err "bad element"; fun err_unbalanced "" = err "unbalanced element" diff -r 49b91b716cbe -r 52e9770e0107 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Mar 08 16:43:29 2012 +0000 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Mar 08 16:49:24 2012 +0000 @@ -104,6 +104,9 @@ [Isabelle_Markup.tfreeN, Isabelle_Markup.tvarN, Isabelle_Markup.freeN, Isabelle_Markup.boundN, Isabelle_Markup.varN, Isabelle_Markup.skolemN]; +fun get_int props name = + (case Properties.get props name of NONE => NONE | SOME s => Int.fromString s); + in fun pgml_terms (XML.Elem ((name, atts), body)) = @@ -114,9 +117,9 @@ let val content = maps pgml_terms body in if name = Isabelle_Markup.blockN then [Pgml.Box {orient = NONE, - indent = Properties.get_int atts Isabelle_Markup.indentN, content = content}] + indent = get_int atts Isabelle_Markup.indentN, content = content}] else if name = Isabelle_Markup.breakN then - [Pgml.Break {mandatory = NONE, indent = Properties.get_int atts Isabelle_Markup.widthN}] + [Pgml.Break {mandatory = NONE, indent = get_int atts Isabelle_Markup.widthN}] else content end | pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text); diff -r 49b91b716cbe -r 52e9770e0107 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Thu Mar 08 16:43:29 2012 +0000 +++ b/src/Pure/more_thm.ML Thu Mar 08 16:49:24 2012 +0000 @@ -79,9 +79,9 @@ val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context val no_attributes: 'a -> 'a * 'b list val simple_fact: 'a -> ('a * 'b list) list - val tag_rule: Properties.entry -> thm -> thm + val tag_rule: string * string -> thm -> thm val untag_rule: string -> thm -> thm - val tag: Properties.entry -> attribute + val tag: string * string -> attribute val untag: string -> attribute val def_name: string -> string val def_name_optional: string -> string -> string