# HG changeset patch # User wenzelm # Date 1409144133 -7200 # Node ID 930727de976c3656b1df3d5a73bf7e1092887b61 # Parent b5cdfb352814072081b9097c457d73dacc149502# Parent aa6296d09e0eaef6d99dba5d4e4eabf26a901574 merged diff -r aa6296d09e0e -r 930727de976c NEWS --- a/NEWS Wed Aug 27 14:54:32 2014 +0200 +++ b/NEWS Wed Aug 27 14:55:33 2014 +0200 @@ -33,7 +33,10 @@ strong_coinduct ~> coinduct_strong weak_case_cong ~> case_cong_weak INCOMPATIBILITY. - - The rule "set_cases" is registered with the "[cases set]" + - The rules "set_empty" have been removed. They are easy + consequences of other set rules "by auto". + INCOMPATIBILITY. + - The rule "set_cases" is now registered with the "[cases set]" attribute. This can influence the behavior of the "cases" proof method when more than one case rule is applicable (e.g., an assumption is of the form "w : set ws" and the method "cases w" diff -r aa6296d09e0e -r 930727de976c src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Wed Aug 27 14:54:32 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Wed Aug 27 14:55:33 2014 +0200 @@ -867,9 +867,6 @@ \item[@{text "t."}\hthm{set_cases} @{text "[consumes 1, cases set: set\<^sub>i_t]"}\rm:] ~ \\ @{thm list.set_cases[no_vars]} -\item[@{text "t."}\hthm{set_empty}\rm:] ~ \\ -@{thm list.set_empty[no_vars]} - \item[@{text "t."}\hthm{set_intros}\rm:] ~ \\ @{thm list.set_intros(1)[no_vars]} \\ @{thm list.set_intros(2)[no_vars]} diff -r aa6296d09e0e -r 930727de976c src/HOL/Archimedean_Field.thy --- a/src/HOL/Archimedean_Field.thy Wed Aug 27 14:54:32 2014 +0200 +++ b/src/HOL/Archimedean_Field.thy Wed Aug 27 14:55:33 2014 +0200 @@ -174,6 +174,9 @@ lemma floor_le_iff: "floor x \ z \ x < of_int z + 1" by (simp add: not_less [symmetric] less_floor_iff) +lemma floor_split[arith_split]: "P (floor t) \ (\i. of_int i \ t \ t < of_int i + 1 \ P i)" + by (metis floor_correct floor_unique less_floor_iff not_le order_refl) + lemma floor_mono: assumes "x \ y" shows "floor x \ floor y" proof - have "of_int (floor x) \ x" by (rule of_int_floor_le) @@ -285,7 +288,6 @@ lemma floor_diff_one [simp]: "floor (x - 1) = floor x - 1" using floor_diff_of_int [of x 1] by simp - subsection {* Ceiling function *} definition @@ -426,6 +428,9 @@ lemma ceiling_diff_one [simp]: "ceiling (x - 1) = ceiling x - 1" using ceiling_diff_of_int [of x 1] by simp +lemma ceiling_split[arith_split]: "P (ceiling t) \ (\i. of_int i - 1 < t \ t \ of_int i \ P i)" + by (auto simp add: ceiling_unique ceiling_correct) + lemma ceiling_diff_floor_le_1: "ceiling x - floor x \ 1" proof - have "of_int \x\ - 1 < x" diff -r aa6296d09e0e -r 930727de976c src/HOL/Code_Evaluation.thy --- a/src/HOL/Code_Evaluation.thy Wed Aug 27 14:54:32 2014 +0200 +++ b/src/HOL/Code_Evaluation.thy Wed Aug 27 14:55:33 2014 +0200 @@ -131,10 +131,14 @@ declare [[code drop: "term_of :: integer \ _"]] lemma term_of_integer [unfolded typerep_fun_def typerep_num_def typerep_integer_def, code]: - "Code_Evaluation.term_of (i :: integer) = - Code_Evaluation.App - (Code_Evaluation.Const (STR ''Num.numeral_class.numeral'') (TYPEREP(num \ integer))) - (term_of (num_of_integer i))" + "term_of (i :: integer) = + (if i > 0 then + App (Const (STR ''Num.numeral_class.numeral'') (TYPEREP(num \ integer))) + (term_of (num_of_integer i)) + else if i = 0 then Const (STR ''Groups.zero_class.zero'') TYPEREP(integer) + else + App (Const (STR ''Groups.uminus_class.uminus'') TYPEREP(integer \ integer)) + (term_of (- i)))" by(rule term_of_anything[THEN meta_eq_to_obj_eq]) code_reserved Eval HOLogic diff -r aa6296d09e0e -r 930727de976c src/HOL/Codegenerator_Test/Code_Test.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codegenerator_Test/Code_Test.thy Wed Aug 27 14:55:33 2014 +0200 @@ -0,0 +1,148 @@ +(* Title: Code_Test.thy + Author: Andreas Lochbihler, ETH Zurich + +Test infrastructure for the code generator +*) + +theory Code_Test +imports Main +keywords "test_code" "eval_term" :: diag +begin + +subsection {* YXML encoding for @{typ Code_Evaluation.term} *} + +datatype yxml_of_term = YXML + +lemma yot_anything: "x = (y :: yxml_of_term)" +by(cases x y rule: yxml_of_term.exhaust[case_product yxml_of_term.exhaust])(simp) + +definition yot_empty :: yxml_of_term where [code del]: "yot_empty = YXML" +definition yot_literal :: "String.literal \ yxml_of_term" + where [code del]: "yot_literal _ = YXML" +definition yot_append :: "yxml_of_term \ yxml_of_term \ yxml_of_term" + where [code del]: "yot_append _ _ = YXML" +definition yot_concat :: "yxml_of_term list \ yxml_of_term" + where [code del]: "yot_concat _ = YXML" + +text {* Serialise @{typ yxml_of_term} to native string of target language *} + +code_printing type_constructor yxml_of_term + \ (SML) "string" + and (OCaml) "string" + and (Haskell) "String" + and (Scala) "String" +| constant yot_empty + \ (SML) "\"\"" + and (OCaml) "\"\"" + and (Haskell) "\"\"" + and (Scala) "\"\"" +| constant yot_literal + \ (SML) "_" + and (OCaml) "_" + and (Haskell) "_" + and (Scala) "_" +| constant yot_append + \ (SML) "String.concat [(_), (_)]" + and (OCaml) "String.concat \"\" [(_); (_)]" + and (Haskell) infixr 5 "++" + and (Scala) infixl 5 "+" +| constant yot_concat + \ (SML) "String.concat" + and (OCaml) "String.concat \"\"" + and (Haskell) "Prelude.concat" + and (Scala) "_.mkString(\"\")" + +text {* + Stripped-down implementations of Isabelle's XML tree with YXML encoding + as defined in @{file "~~/src/Pure/PIDE/xml.ML"}, @{file "~~/src/Pure/PIDE/yxml.ML"} + sufficient to encode @{typ "Code_Evaluation.term"} as in @{file "~~/src/Pure/term_xml.ML"}. +*} + +datatype xml_tree = XML_Tree + +lemma xml_tree_anything: "x = (y :: xml_tree)" +by(cases x y rule: xml_tree.exhaust[case_product xml_tree.exhaust])(simp) + +context begin +local_setup {* Local_Theory.map_naming (Name_Space.mandatory_path "xml") *} + +type_synonym attributes = "(String.literal \ String.literal) list" +type_synonym body = "xml_tree list" + +definition Elem :: "String.literal \ attributes \ xml_tree list \ xml_tree" +where [code del]: "Elem _ _ _ = XML_Tree" + +definition Text :: "String.literal \ xml_tree" +where [code del]: "Text _ = XML_Tree" + +definition node :: "xml_tree list \ xml_tree" +where "node ts = Elem (STR '':'') [] ts" + +definition tagged :: "String.literal \ String.literal option \ xml_tree list \ xml_tree" +where "tagged tag x ts = Elem tag (case x of None \ [] | Some x' \ [(STR ''0'', x')]) ts" + +definition list where "list f xs = map (node \ f) xs" + +definition X :: yxml_of_term where "X = yot_literal (STR [Char Nibble0 Nibble5])" +definition Y :: yxml_of_term where "Y = yot_literal (STR [Char Nibble0 Nibble6])" +definition XY :: yxml_of_term where "XY = yot_append X Y" +definition XYX :: yxml_of_term where "XYX = yot_append XY X" + +end + +code_datatype xml.Elem xml.Text + +definition yxml_string_of_xml_tree :: "xml_tree \ yxml_of_term \ yxml_of_term" +where [code del]: "yxml_string_of_xml_tree _ _ = YXML" + +lemma yxml_string_of_xml_tree_code [code]: + "yxml_string_of_xml_tree (xml.Elem name atts ts) rest = + yot_append xml.XY ( + yot_append (yot_literal name) ( + foldr (\(a, x) rest. + yot_append xml.Y ( + yot_append (yot_literal a) ( + yot_append (yot_literal (STR ''='')) ( + yot_append (yot_literal x) rest)))) atts ( + foldr yxml_string_of_xml_tree ts ( + yot_append xml.XYX rest))))" + "yxml_string_of_xml_tree (xml.Text s) rest = yot_append (yot_literal s) rest" +by(rule yot_anything)+ + +definition yxml_string_of_body :: "xml.body \ yxml_of_term" +where "yxml_string_of_body ts = foldr yxml_string_of_xml_tree ts yot_empty" + +text {* + Encoding @{typ Code_Evaluation.term} into XML trees + as defined in @{file "~~/src/Pure/term_xml.ML"} +*} + +definition xml_of_typ :: "Typerep.typerep \ xml.body" +where [code del]: "xml_of_typ _ = [XML_Tree]" + +definition xml_of_term :: "Code_Evaluation.term \ xml.body" +where [code del]: "xml_of_term _ = [XML_Tree]" + +lemma xml_of_typ_code [code]: + "xml_of_typ (typerep.Typerep t args) = [xml.tagged (STR ''0'') (Some t) (xml.list xml_of_typ args)]" +by(simp add: xml_of_typ_def xml_tree_anything) + +lemma xml_of_term_code [code]: + "xml_of_term (Code_Evaluation.Const x ty) = [xml.tagged (STR ''0'') (Some x) (xml_of_typ ty)]" + "xml_of_term (Code_Evaluation.App t1 t2) = [xml.tagged (STR ''5'') None [xml.node (xml_of_term t1), xml.node (xml_of_term t2)]]" + "xml_of_term (Code_Evaluation.Abs x ty t) = [xml.tagged (STR ''4'') (Some x) [xml.node (xml_of_typ ty), xml.node (xml_of_term t)]]" + -- {* + FIXME: @{const Code_Evaluation.Free} is used only in Quickcheck_Narrowing to represent + uninstantiated parameters in constructors. Here, we always translate them to @{ML Free} variables. + *} + "xml_of_term (Code_Evaluation.Free x ty) = [xml.tagged (STR ''1'') (Some x) (xml_of_typ ty)]" +by(simp_all add: xml_of_term_def xml_tree_anything) + +definition yxml_string_of_term :: "Code_Evaluation.term \ yxml_of_term" +where "yxml_string_of_term = yxml_string_of_body \ xml_of_term" + +subsection {* Test engine and drivers *} + +ML_file "code_test.ML" + +end diff -r aa6296d09e0e -r 930727de976c src/HOL/Codegenerator_Test/Code_Test_GHC.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Wed Aug 27 14:55:33 2014 +0200 @@ -0,0 +1,15 @@ +(* Title: Code_Test_GHC.thy + Author: Andreas Lochbihler, ETH Zurich + +Test case for test_code on GHC +*) + +theory Code_Test_GHC imports Code_Test begin + +definition id_integer :: "integer \ integer" where "id_integer = id" + +test_code "id_integer (14 + 7 * -12) = 140 div -2" in GHC + +eval_term "14 + 7 * -12 :: integer" in GHC + +end diff -r aa6296d09e0e -r 930727de976c src/HOL/Codegenerator_Test/Code_Test_MLton.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codegenerator_Test/Code_Test_MLton.thy Wed Aug 27 14:55:33 2014 +0200 @@ -0,0 +1,13 @@ +(* Title: Code_Test_MLtonL.thy + Author: Andreas Lochbihler, ETH Zurich + +Test case for test_code on MLton +*) + +theory Code_Test_MLton imports Code_Test begin + +test_code "14 + 7 * -12 = (140 div -2 :: integer)" in MLton + +eval_term "14 + 7 * -12 :: integer" in MLton + +end diff -r aa6296d09e0e -r 930727de976c src/HOL/Codegenerator_Test/Code_Test_OCaml.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Wed Aug 27 14:55:33 2014 +0200 @@ -0,0 +1,13 @@ +(* Title: Code_Test_OCaml.thy + Author: Andreas Lochbihler, ETH Zurich + +Test case for test_code on OCaml +*) + +theory Code_Test_OCaml imports Code_Test begin + +test_code "14 + 7 * -12 = (140 div -2 :: integer)" in OCaml + +eval_term "14 + 7 * -12 :: integer" in OCaml + +end diff -r aa6296d09e0e -r 930727de976c src/HOL/Codegenerator_Test/Code_Test_PolyML.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy Wed Aug 27 14:55:33 2014 +0200 @@ -0,0 +1,13 @@ +(* Title: Code_Test_PolyML.thy + Author: Andreas Lochbihler, ETH Zurich + +Test case for test_code on PolyML +*) + +theory Code_Test_PolyML imports Code_Test begin + +test_code "14 + 7 * -12 = (140 div -2 :: integer)" in PolyML + +eval_term "14 + 7 * -12 :: integer" in PolyML + +end diff -r aa6296d09e0e -r 930727de976c src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy Wed Aug 27 14:55:33 2014 +0200 @@ -0,0 +1,13 @@ +(* Title: Code_Test_SMLNJ.thy + Author: Andreas Lochbihler, ETH Zurich + +Test case for test_code on SMLNJ +*) + +theory Code_Test_SMLNJ imports Code_Test begin + +test_code "14 + 7 * -12 = (140 div -2 :: integer)" in SMLNJ + +eval_term "14 + 7 * -12 :: integer" in SMLNJ + +end diff -r aa6296d09e0e -r 930727de976c src/HOL/Codegenerator_Test/Code_Test_Scala.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Wed Aug 27 14:55:33 2014 +0200 @@ -0,0 +1,13 @@ +(* Title: Code_Test_Scala.thy + Author: Andreas Lochbihler, ETH Zurich + +Test case for test_code on Scala +*) + +theory Code_Test_Scala imports Code_Test begin + +test_code "14 + 7 * -12 = (140 div -2 :: integer)" in Scala + +eval_term "14 + 7 * -12 :: integer" in Scala + +end diff -r aa6296d09e0e -r 930727de976c src/HOL/Codegenerator_Test/code_test.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codegenerator_Test/code_test.ML Wed Aug 27 14:55:33 2014 +0200 @@ -0,0 +1,594 @@ +(* Title: Code_Test.ML + Author: Andreas Lochbihler, ETH Zurich + +Test infrastructure for the code generator +*) + +signature CODE_TEST = sig + val add_driver : string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) -> theory -> theory + val get_driver : theory -> string -> ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) option + val overlord : bool Config.T + val successN : string + val failureN : string + val start_markerN : string + val end_markerN : string + val test_terms : Proof.context -> term list -> string -> unit + val test_targets : Proof.context -> term list -> string list -> unit list + val test_code_cmd : string list -> string list -> Toplevel.state -> unit + + val eval_term : Proof.context -> term -> string -> unit + + val gen_driver : + (theory -> Path.T -> string list -> string -> + {files : (Path.T * string) list, + compile_cmd : string option, run_cmd : string, mk_code_file : string -> Path.T}) + -> string -> string -> string + -> theory -> (string * string) list * string -> Path.T -> string + + val ISABELLE_POLYML_PATH : string + val polymlN : string + val evaluate_in_polyml : Proof.context -> (string * string) list * string -> Path.T -> string + + val mltonN : string + val ISABELLE_MLTON : string + val evaluate_in_mlton : Proof.context -> (string * string) list * string -> Path.T -> string + + val smlnjN : string + val ISABELLE_SMLNJ : string + val evaluate_in_smlnj : Proof.context -> (string * string) list * string -> Path.T -> string + + val ocamlN : string + val ISABELLE_OCAMLC : string + val evaluate_in_ocaml : Proof.context -> (string * string) list * string -> Path.T -> string + + val ghcN : string + val ISABELLE_GHC : string + val ghc_options : string Config.T + val evaluate_in_ghc : Proof.context -> (string * string) list * string -> Path.T -> string + + val scalaN : string + val ISABELLE_SCALA : string + val evaluate_in_scala : Proof.context -> (string * string) list * string -> Path.T -> string +end + +structure Code_Test : CODE_TEST = struct + +(* convert a list of terms into nested tuples and back *) +fun mk_tuples [] = @{term "()"} + | mk_tuples [t] = t + | mk_tuples (t :: ts) = HOLogic.mk_prod (t, mk_tuples ts) + +fun dest_tuples (Const (@{const_name Pair}, _) $ l $ r) = l :: dest_tuples r + | dest_tuples t = [t] + + +fun map_option _ NONE = NONE + | map_option f (SOME x) = SOME (f x) + +fun last_field sep str = + let + val n = size sep; + val len = size str; + fun find i = + if i < 0 then NONE + else if String.substring (str, i, n) = sep then SOME i + else find (i - 1); + in + (case find (len - n) of + NONE => NONE + | SOME i => SOME (String.substring (str, 0, i), String.extract (str, i + n, NONE))) + end; + +fun split_first_last start stop s = + case first_field start s + of NONE => NONE + | SOME (initial, rest) => + case last_field stop rest + of NONE => NONE + | SOME (middle, tail) => SOME (initial, middle, tail); + +(* Data slot for drivers *) + +structure Drivers = Theory_Data +( + type T = (string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string)) list; + val empty = []; + val extend = I; + fun merge data : T = AList.merge (op =) (K true) data; +) + +val add_driver = Drivers.map o AList.update (op =); +val get_driver = AList.lookup (op =) o Drivers.get; + +(* + Test drivers must produce output of the following format: + + The start of the relevant data is marked with start_markerN, + its end with end_markerN. + + Between these two markers, every line corresponds to one test. + Lines of successful tests start with successN, failures start with failureN. + The failure failureN may continue with the YXML encoding of the evaluated term. + There must not be any additional whitespace in between. +*) + +(* Parsing of results *) + +val successN = "True" +val failureN = "False" +val start_markerN = "*@*Isabelle/Code_Test-start*@*" +val end_markerN = "*@*Isabelle/Code_Test-end*@*" + +fun parse_line line = + if String.isPrefix successN line then (true, NONE) + else if String.isPrefix failureN line then (false, + if size line > size failureN then + String.extract (line, size failureN, NONE) + |> YXML.parse_body + |> Term_XML.Decode.term + |> dest_tuples + |> SOME + else NONE) + else raise Fail ("Cannot parse result of evaluation:\n" ^ line) + +fun parse_result target out = + case split_first_last start_markerN end_markerN out + of NONE => error ("Evaluation failed for " ^ target ^ "!\nBash output:\n" ^ out) + | SOME (_, middle, _) => middle |> trim_line |> split_lines |> map parse_line + +(* Pretty printing of test results *) + +fun pretty_eval _ NONE _ = [] + | pretty_eval ctxt (SOME evals) ts = + [Pretty.fbrk, + Pretty.big_list "Evaluated terms" + (map (fn (t, eval) => Pretty.block + [Syntax.pretty_term ctxt t, Pretty.brk 1, Pretty.str "=", Pretty.brk 1, + Syntax.pretty_term ctxt eval]) + (ts ~~ evals))] + +fun pretty_failure ctxt target (((_, evals), query), eval_ts) = + Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for") @ [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)] + @ pretty_eval ctxt evals eval_ts) + +fun pretty_failures ctxt target failures = + Pretty.blk (0, Pretty.fbreaks (map (pretty_failure ctxt target) failures)) + +(* Driver invocation *) + +val overlord = Attrib.setup_config_bool @{binding "code_test_overlord"} (K false); + +fun with_overlord_dir name f = + let + val path = Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ())) + val _ = Isabelle_System.mkdirs path; + in + Exn.release (Exn.capture f path) + end; + +fun dynamic_value_strict ctxt t compiler = + let + val thy = Proof_Context.theory_of ctxt + val (driver, target) = case get_driver thy compiler + of NONE => error ("No driver for target " ^ compiler) + | SOME f => f; + val debug = Config.get (Proof_Context.init_global thy) overlord + val with_dir = if debug then with_overlord_dir else Isabelle_System.with_tmp_dir + fun evaluate f = with_dir "Code_Test" (driver ctxt f) |> parse_result compiler + fun evaluator program _ vs_ty deps = + Exn.interruptible_capture evaluate (Code_Target.evaluator ctxt target program deps true vs_ty); + fun postproc f = map (apsnd (map_option (map f))) + in + Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t) + end; + +(* Term preprocessing *) + +fun add_eval (Const (@{const_name Trueprop}, _) $ t) = add_eval t + | add_eval (Const (@{const_name "HOL.eq"}, _) $ lhs $ rhs) = (fn acc => + acc + |> add_eval rhs + |> add_eval lhs + |> cons rhs + |> cons lhs) + | add_eval (Const (@{const_name "Not"}, _) $ t) = add_eval t + | add_eval (Const (@{const_name "Orderings.ord_class.less_eq"}, _) $ lhs $ rhs) = (fn acc => + lhs :: rhs :: acc) + | add_eval (Const (@{const_name "Orderings.ord_class.less"}, _) $ lhs $ rhs) = (fn acc => + lhs :: rhs :: acc) + | add_eval _ = I + +fun mk_term_of [] = @{term "None :: (unit \ yxml_of_term) option"} + | mk_term_of ts = + let + val tuple = mk_tuples ts + val T = fastype_of tuple + in + @{term "Some :: (unit \ yxml_of_term) \ (unit \ yxml_of_term) option"} $ + (absdummy @{typ unit} (@{const yxml_string_of_term} $ + (Const (@{const_name Code_Evaluation.term_of}, T --> @{typ term}) $ tuple))) + end + +fun test_terms ctxt ts target = + let + val thy = Proof_Context.theory_of ctxt + + fun term_of t = Sign.of_sort thy (fastype_of t, @{sort term_of}) + + fun ensure_bool t = case fastype_of t of @{typ bool} => () + | _ => error ("Test case not of type bool: " ^ Pretty.string_of (Syntax.pretty_term ctxt t)) + + val _ = map ensure_bool ts + + val evals = map (fn t => filter term_of (add_eval t [])) ts + val eval = map mk_term_of evals + + val T = HOLogic.mk_prodT (@{typ bool}, Type (@{type_name option}, [@{typ unit} --> @{typ yxml_of_term}])) + val t = HOLogic.mk_list T (map HOLogic.mk_prod (ts ~~ eval)) + + val result = dynamic_value_strict ctxt t target; + + val failed = + filter_out (fst o fst o fst) (result ~~ ts ~~ evals) + handle ListPair.UnequalLengths => + error ("Evaluation failed!\nWrong number of test results: " ^ Int.toString (length result)) + val _ = case failed of [] => () + | _ => error (Pretty.string_of (pretty_failures ctxt target failed)) + in + () + end + +fun test_targets ctxt = map o test_terms ctxt + +fun test_code_cmd raw_ts targets state = + let + val ctxt = Toplevel.context_of state; + val ts = Syntax.read_terms ctxt raw_ts; + val frees = fold Term.add_free_names ts [] + val _ = if frees = [] then () else + error ("Terms contain free variables: " ^ + Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees)))) + in + test_targets ctxt ts targets; () + end + + +fun eval_term ctxt t target = + let + val thy = Proof_Context.theory_of ctxt + + val T_t = fastype_of t + val _ = if Sign.of_sort thy (T_t, @{sort term_of}) then () else error + ("Type " ^ Pretty.string_of (Syntax.pretty_typ ctxt T_t) ^ + " of term not of sort " ^ Pretty.string_of (Syntax.pretty_sort ctxt @{sort term_of})) + + val T = HOLogic.mk_prodT (@{typ bool}, Type (@{type_name option}, [@{typ unit} --> @{typ yxml_of_term}])) + val t' = HOLogic.mk_list T [HOLogic.mk_prod (@{term "False"}, mk_term_of [t])] + + val result = dynamic_value_strict ctxt t' target; + val t_eval = case result of [(_, SOME [t])] => t | _ => error "Evaluation failed" + in + Pretty.writeln (Syntax.pretty_term ctxt t_eval) + end + +fun eval_term_cmd raw_t target state = + let + val ctxt = Toplevel.context_of state; + val t = Syntax.read_term ctxt raw_t; + val frees = Term.add_free_names t [] + val _ = if frees = [] then () else + error ("Term contains free variables: " ^ + Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees)))) + in + eval_term ctxt t target + end + + +(* Generic driver *) + +fun gen_driver mk_driver env_var env_var_dest compilerN ctxt (code_files, value_name) = + let + val compiler = getenv env_var + val _ = if compiler <> "" then () else error (Pretty.string_of (Pretty.para + ("Environment variable " ^ env_var ^ " is not set. To test code generation with " ^ + compilerN ^ ", set this variable to your " ^ env_var_dest ^ " in the settings file."))) + + fun compile NONE = () + | compile (SOME cmd) = + let + val (out, ret) = Isabelle_System.bash_output cmd + in + if ret = 0 then () else error + ("Compilation with " ^ compilerN ^ " failed:\n" ^ cmd ^ "\n" ^ out) + end + + fun run (path : Path.T)= + let + val modules = map fst code_files + val {files, compile_cmd, run_cmd, mk_code_file} + = mk_driver ctxt path modules value_name + + val _ = map (fn (name, code) => File.write (mk_code_file name) code) code_files + val _ = map (fn (name, content) => File.write name content) files + + val _ = compile compile_cmd + + val (out, res) = Isabelle_System.bash_output run_cmd + val _ = if res = 0 then () else error + ("Evaluation for " ^ compilerN ^ " terminated with error code " ^ Int.toString res ^ + "\nBash output:\n" ^ out) + in + out + end + in + run + end + +(* Driver for PolyML *) + +val ISABELLE_POLYML_PATH = "ISABELLE_POLYML_PATH" +val polymlN = "PolyML"; + +fun mk_driver_polyml _ path _ value_name = + let + val generatedN = "generated.sml" + val driverN = "driver.sml" + + val code_path = Path.append path (Path.basic generatedN) + val driver_path = Path.append path (Path.basic driverN) + val driver = + "fun main prog_name = \n" ^ + " let\n" ^ + " fun format_term NONE = \"\"\n" ^ + " | format_term (SOME t) = t ();\n" ^ + " fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^ + " | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^ + " val result = " ^ value_name ^ " ();\n" ^ + " val _ = print \"" ^ start_markerN ^ "\";\n" ^ + " val _ = map (print o format) result;\n" ^ + " val _ = print \"" ^ end_markerN ^ "\";\n" ^ + " in\n" ^ + " ()\n" ^ + " end;\n" + val cmd = + "echo \"use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^ + Path.implode driver_path ^ "\\\"; main ();\" | " ^ + Path.implode (Path.variable ISABELLE_POLYML_PATH) + in + {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path} + end + +val evaluate_in_polyml = gen_driver mk_driver_polyml ISABELLE_POLYML_PATH "PolyML executable" polymlN + +(* Driver for mlton *) + +val mltonN = "MLton" +val ISABELLE_MLTON = "ISABELLE_MLTON" + +fun mk_driver_mlton _ path _ value_name = + let + val generatedN = "generated.sml" + val driverN = "driver.sml" + val projectN = "test" + val ml_basisN = projectN ^ ".mlb" + + val code_path = Path.append path (Path.basic generatedN) + val driver_path = Path.append path (Path.basic driverN) + val ml_basis_path = Path.append path (Path.basic ml_basisN) + val driver = + "fun format_term NONE = \"\"\n" ^ + " | format_term (SOME t) = t ();\n" ^ + "fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^ + " | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^ + "val result = " ^ value_name ^ " ();\n" ^ + "val _ = print \"" ^ start_markerN ^ "\";\n" ^ + "val _ = map (print o format) result;\n" ^ + "val _ = print \"" ^ end_markerN ^ "\";\n" + val ml_basis = + "$(SML_LIB)/basis/basis.mlb\n" ^ + generatedN ^ "\n" ^ + driverN + + val compile_cmd = + File.shell_path (Path.variable ISABELLE_MLTON) ^ + " -default-type intinf " ^ File.shell_path ml_basis_path + val run_cmd = File.shell_path (Path.append path (Path.basic projectN)) + in + {files = [(driver_path, driver), (ml_basis_path, ml_basis)], + compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path} + end + +val evaluate_in_mlton = gen_driver mk_driver_mlton ISABELLE_MLTON "MLton executable" mltonN + +(* Driver for SML/NJ *) + +val smlnjN = "SMLNJ" +val ISABELLE_SMLNJ = "ISABELLE_SMLNJ" + +fun mk_driver_smlnj _ path _ value_name = + let + val generatedN = "generated.sml" + val driverN = "driver.sml" + + val code_path = Path.append path (Path.basic generatedN) + val driver_path = Path.append path (Path.basic driverN) + val driver = + "structure Test = struct\n" ^ + "fun main prog_name =\n" ^ + " let\n" ^ + " fun format_term NONE = \"\"\n" ^ + " | format_term (SOME t) = t ();\n" ^ + " fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^ + " | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^ + " val result = " ^ value_name ^ " ();\n" ^ + " val _ = print \"" ^ start_markerN ^ "\";\n" ^ + " val _ = map (print o format) result;\n" ^ + " val _ = print \"" ^ end_markerN ^ "\";\n" ^ + " in\n" ^ + " 0\n" ^ + " end;\n" ^ + "end;" + val cmd = + "echo \"Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^ + "use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^ Path.implode driver_path ^ "\\\";" ^ + "Test.main ();\" | " ^ Path.implode (Path.variable ISABELLE_SMLNJ) + in + {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path} + end + +val evaluate_in_smlnj = gen_driver mk_driver_smlnj ISABELLE_SMLNJ "SMLNJ executable" smlnjN + +(* Driver for OCaml *) + +val ocamlN = "OCaml" +val ISABELLE_OCAMLC = "ISABELLE_OCAMLC" + +fun mk_driver_ocaml _ path _ value_name = + let + val generatedN = "generated.ml" + val driverN = "driver.ml" + + val code_path = Path.append path (Path.basic generatedN) + val driver_path = Path.append path (Path.basic driverN) + val driver = + "let format_term = function\n" ^ + " | None -> \"\"\n" ^ + " | Some t -> t ();;\n" ^ + "let format = function\n" ^ + " | (true, _) -> \"" ^ successN ^ "\\n\"\n" ^ + " | (false, x) -> \"" ^ failureN ^ "\" ^ format_term x ^ \"\\n\";;\n" ^ + "let result = " ^ ("Generated." ^ value_name) ^ " ();;\n" ^ + "let main x =\n" ^ + " let _ = print_string \"" ^ start_markerN ^ "\" in\n" ^ + " let _ = List.map (fun x -> print_string (format x)) result in\n" ^ + " print_string \"" ^ end_markerN ^ "\";;\n" ^ + "main ();;" + + val compiled_path = Path.append path (Path.basic "test") + val compile_cmd = + Path.implode (Path.variable ISABELLE_OCAMLC) ^ " -w pu -o " ^ Path.implode compiled_path ^ + " -I " ^ Path.implode path ^ + " nums.cma " ^ Path.implode code_path ^ " " ^ Path.implode driver_path + + val run_cmd = File.shell_path compiled_path + in + {files = [(driver_path, driver)], + compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path} + end + +val evaluate_in_ocaml = gen_driver mk_driver_ocaml ISABELLE_OCAMLC "ocamlc executable" ocamlN + +(* Driver for GHC *) + +val ghcN = "GHC" +val ISABELLE_GHC = "ISABELLE_GHC" + +val ghc_options = Attrib.setup_config_string @{binding code_test_ghc} (K "") + +fun mk_driver_ghc ctxt path modules value_name = + let + val driverN = "Main.hs" + + fun mk_code_file name = Path.append path (Path.basic (name ^ ".hs")) + val driver_path = Path.append path (Path.basic driverN) + val driver = + "module Main where {\n" ^ + String.concat (map (fn module => "import qualified " ^ module ^ ";\n") modules) ^ + "main = do {\n" ^ + " let {\n" ^ + " format_term Nothing = \"\";\n" ^ + " format_term (Just t) = t ();\n" ^ + " format (True, _) = \"" ^ successN ^ "\\n\";\n" ^ + " format (False, to) = \"" ^ failureN ^ "\" ++ format_term to ++ \"\\n\";\n" ^ + " result = " ^ value_name ^ " ();\n" ^ + " };\n" ^ + " Prelude.putStr \"" ^ start_markerN ^ "\";\n" ^ + " Prelude.mapM_ (putStr . format) result;\n" ^ + " Prelude.putStr \"" ^ end_markerN ^ "\";\n" ^ + " }\n" ^ + "}\n" + + val compiled_path = Path.append path (Path.basic "test") + val compile_cmd = + Path.implode (Path.variable ISABELLE_GHC) ^ " " ^ Code_Haskell.language_params ^ " " ^ + Config.get ctxt ghc_options ^ " -o " ^ Path.implode compiled_path ^ " " ^ + Path.implode driver_path ^ " -i" ^ Path.implode path + + val run_cmd = File.shell_path compiled_path + in + {files = [(driver_path, driver)], + compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = mk_code_file} + end + +val evaluate_in_ghc = gen_driver mk_driver_ghc ISABELLE_GHC "GHC executable" ghcN + +(* Driver for Scala *) + +val scalaN = "Scala" +val ISABELLE_SCALA = "ISABELLE_SCALA" + +fun mk_driver_scala _ path _ value_name = + let + val generatedN = "Generated_Code" + val driverN = "Driver.scala" + + val code_path = Path.append path (Path.basic (generatedN ^ ".scala")) + val driver_path = Path.append path (Path.basic driverN) + val driver = + "import " ^ generatedN ^ "._\n" ^ + "object Test {\n" ^ + " def format_term(x : Option[Unit => String]) : String = x match {\n" ^ + " case None => \"\"\n" ^ + " case Some(x) => x(())\n" ^ + " }\n" ^ + " def format(term : (Boolean, Option[Unit => String])) : String = term match {\n" ^ + " case (true, _) => \"True\\n\"\n" ^ + " case (false, x) => \"False\" + format_term(x) + \"\\n\"\n" ^ + " }\n" ^ + " def main(args:Array[String]) = {\n" ^ + " val result = " ^ value_name ^ "(());\n" ^ + " print(\"" ^ start_markerN ^ "\");\n" ^ + " result.map{test:(Boolean, Option[Unit => String]) => print(format(test))};\n" ^ + " print(\"" ^ end_markerN ^ "\");\n" ^ + " }\n" ^ + "}\n" + + val compile_cmd = + Path.implode (Path.append (Path.variable ISABELLE_SCALA) (Path.basic "scalac")) ^ + " -d " ^ File.shell_path path ^ " -classpath " ^ File.shell_path path ^ " " ^ + File.shell_path code_path ^ " " ^ File.shell_path driver_path + + val run_cmd = + Path.implode (Path.append (Path.variable ISABELLE_SCALA) (Path.basic "scala")) ^ + " -cp " ^ File.shell_path path ^ " Test" + in + {files = [(driver_path, driver)], + compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path} + end + +val evaluate_in_scala = gen_driver mk_driver_scala ISABELLE_SCALA "Scala directory" scalaN + +val test_codeP = Scan.repeat1 Parse.prop -- (@{keyword "in"} |-- Scan.repeat1 Parse.name) + +val _ = + Outer_Syntax.command @{command_spec "test_code"} + "compile test cases to target languages, execute them and report results" + (test_codeP >> (fn (raw_ts, targets) => Toplevel.keep (test_code_cmd raw_ts targets))) + +val eval_termP = Parse.term -- (@{keyword "in"} |-- Parse.name) + +val _ = + Outer_Syntax.command @{command_spec "eval_term"} + "evaluate term in target language" + (eval_termP >> (fn (raw_t, target) => Toplevel.keep (eval_term_cmd raw_t target))) + +val _ = Context.>> (Context.map_theory ( + fold add_driver + [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)), + (mltonN, (evaluate_in_mlton, Code_ML.target_SML)), + (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)), + (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)), + (ghcN, (evaluate_in_ghc, Code_Haskell.target)), + (scalaN, (evaluate_in_scala, Code_Scala.target))])) +end + diff -r aa6296d09e0e -r 930727de976c src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Wed Aug 27 14:54:32 2014 +0200 +++ b/src/HOL/Library/Extended_Real.thy Wed Aug 27 14:55:33 2014 +0200 @@ -91,21 +91,22 @@ shows "-a = -b \ a = b" by (cases rule: ereal2_cases[of a b]) simp_all -function of_ereal :: "ereal \ real" where - "of_ereal (ereal r) = r" -| "of_ereal \ = 0" -| "of_ereal (-\) = 0" +instantiation ereal :: real_of +begin + +function real_ereal :: "ereal \ real" where + "real_ereal (ereal r) = r" +| "real_ereal \ = 0" +| "real_ereal (-\) = 0" by (auto intro: ereal_cases) termination by default (rule wf_empty) -defs (overloaded) - real_of_ereal_def [code_unfold]: "real \ of_ereal" +instance .. +end lemma real_of_ereal[simp]: "real (- x :: ereal) = - (real x)" - "real (ereal r) = r" - "real (\::ereal) = 0" - by (cases x) (simp_all add: real_of_ereal_def) + by (cases x) simp_all lemma range_ereal[simp]: "range ereal = UNIV - {\, -\}" proof safe @@ -216,7 +217,7 @@ instance ereal :: numeral .. lemma real_of_ereal_0[simp]: "real (0::ereal) = 0" - unfolding real_of_ereal_def zero_ereal_def by simp + unfolding zero_ereal_def by simp lemma abs_ereal_zero[simp]: "\0\ = (0::ereal)" unfolding zero_ereal_def abs_ereal.simps by simp diff -r aa6296d09e0e -r 930727de976c src/HOL/Library/Float.thy --- a/src/HOL/Library/Float.thy Wed Aug 27 14:54:32 2014 +0200 +++ b/src/HOL/Library/Float.thy Wed Aug 27 14:55:33 2014 +0200 @@ -15,9 +15,15 @@ morphisms real_of_float float_of unfolding float_def by auto -defs (overloaded) +instantiation float :: real_of +begin + +definition real_float :: "float \ real" where real_of_float_def[code_unfold]: "real \ real_of_float" +instance .. +end + lemma type_definition_float': "type_definition real float_of float" using type_definition_float unfolding real_of_float_def . diff -r aa6296d09e0e -r 930727de976c src/HOL/List.thy --- a/src/HOL/List.thy Wed Aug 27 14:54:32 2014 +0200 +++ b/src/HOL/List.thy Wed Aug 27 14:55:33 2014 +0200 @@ -3436,6 +3436,9 @@ "distinct (a # b # xs) \ (a \ b \ distinct (a # xs) \ distinct (b # xs))" by force +lemma hd_remdups_adj[simp]: "hd (remdups_adj xs) = hd xs" + by (induction xs rule: remdups_adj.induct) simp_all + lemma remdups_adj_Cons: "remdups_adj (x # xs) = (case remdups_adj xs of [] \ [x] | y # xs \ if x = y then y # xs else x # y # xs)" by (induct xs arbitrary: x) (auto split: list.splits) @@ -3444,6 +3447,13 @@ "remdups_adj (xs @ [x,y]) = remdups_adj (xs @ [x]) @ (if x = y then [] else [y])" by (induct xs rule: remdups_adj.induct, simp_all) +lemma remdups_adj_adjacent: + "Suc i < length (remdups_adj xs) \ remdups_adj xs ! i \ remdups_adj xs ! Suc i" +proof (induction xs arbitrary: i rule: remdups_adj.induct) + case (3 x y xs i) + thus ?case by (cases i, cases "x = y") (simp, auto simp: hd_conv_nth[symmetric]) +qed simp_all + lemma remdups_adj_rev[simp]: "remdups_adj (rev xs) = rev (remdups_adj xs)" by (induct xs rule: remdups_adj.induct, simp_all add: remdups_adj_append_two) diff -r aa6296d09e0e -r 930727de976c src/HOL/ROOT --- a/src/HOL/ROOT Wed Aug 27 14:54:32 2014 +0200 +++ b/src/HOL/ROOT Wed Aug 27 14:55:33 2014 +0200 @@ -237,6 +237,19 @@ Generate_Target_Nat Generate_Efficient_Datastructures Generate_Pretty_Char + Code_Test + theories[condition = ISABELLE_GHC] + Code_Test_GHC + theories[condition = ISABELLE_MLTON] + Code_Test_MLton + theories[condition = ISABELLE_OCAMLC] + Code_Test_OCaml + theories[condition = ISABELLE_POLYML_PATH] + Code_Test_PolyML + theories[condition = ISABELLE_SCALA] + Code_Test_Scala + theories[condition = ISABELLE_SMLNJ] + Code_Test_SMLNJ session "HOL-Metis_Examples" in Metis_Examples = HOL + description {* diff -r aa6296d09e0e -r 930727de976c src/HOL/Real.thy --- a/src/HOL/Real.thy Wed Aug 27 14:54:32 2014 +0200 +++ b/src/HOL/Real.thy Wed Aug 27 14:55:33 2014 +0200 @@ -1000,13 +1000,24 @@ where "real_of_rat \ of_rat" -consts - (*overloaded constant for injecting other types into "real"*) - real :: "'a => real" +class real_of = + fixes real :: "'a \ real" + +instantiation nat :: real_of +begin + +definition real_nat :: "nat \ real" where real_of_nat_def [code_unfold]: "real \ of_nat" -defs (overloaded) - real_of_nat_def [code_unfold]: "real == real_of_nat" - real_of_int_def [code_unfold]: "real == real_of_int" +instance .. +end + +instantiation int :: real_of +begin + +definition real_int :: "int \ real" where real_of_int_def [code_unfold]: "real \ of_int" + +instance .. +end declare [[coercion_enabled]] declare [[coercion "real::nat\real"]] @@ -1463,12 +1474,14 @@ @{thm real_of_nat_mult}, @{thm real_of_int_zero}, @{thm real_of_one}, @{thm real_of_int_add}, @{thm real_of_int_minus}, @{thm real_of_int_diff}, @{thm real_of_int_mult}, @{thm real_of_int_of_nat_eq}, - @{thm real_of_nat_numeral}, @{thm real_numeral(1)}, @{thm real_numeral(2)}] + @{thm real_of_nat_numeral}, @{thm real_numeral(1)}, @{thm real_numeral(2)}, + @{thm real_of_int_def[symmetric]}, @{thm real_of_nat_def[symmetric]}] #> Lin_Arith.add_inj_const (@{const_name real}, @{typ "nat \ real"}) - #> Lin_Arith.add_inj_const (@{const_name real}, @{typ "int \ real"})) + #> Lin_Arith.add_inj_const (@{const_name real}, @{typ "int \ real"}) + #> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat \ real"}) + #> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int \ real"})) *} - subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*} lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)" @@ -1650,78 +1663,66 @@ lemma real_lb_ub_int: " \n::int. real n \ r & r < real (n+1)" unfolding real_of_int_def by (rule floor_exists) -lemma lemma_floor: - assumes a1: "real m \ r" and a2: "r < real n + 1" - shows "m \ (n::int)" -proof - - have "real m < real n + 1" using a1 a2 by (rule order_le_less_trans) - also have "... = real (n + 1)" by simp - finally have "m < n + 1" by (simp only: real_of_int_less_iff) - thus ?thesis by arith -qed +lemma lemma_floor: "real m \ r \ r < real n + 1 \ m \ (n::int)" + by simp lemma real_of_int_floor_le [simp]: "real (floor r) \ r" unfolding real_of_int_def by (rule of_int_floor_le) lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \ x" -by (auto intro: lemma_floor) + by simp lemma real_of_int_floor_cancel [simp]: "(real (floor x) = x) = (\n::int. x = real n)" using floor_real_of_int by metis lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n" - unfolding real_of_int_def using floor_unique [of n x] by simp + by linarith lemma floor_eq2: "[| real n \ x; x < real n + 1 |] ==> floor x = n" - unfolding real_of_int_def by (rule floor_unique) + by linarith lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n" -apply (rule inj_int [THEN injD]) -apply (simp add: real_of_nat_Suc) -apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "int n"]) -done + by linarith lemma floor_eq4: "[| real n \ x; x < real (Suc n) |] ==> nat(floor x) = n" -apply (drule order_le_imp_less_or_eq) -apply (auto intro: floor_eq3) -done + by linarith lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \ real(floor r)" - unfolding real_of_int_def using floor_correct [of r] by simp + by linarith lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)" - unfolding real_of_int_def using floor_correct [of r] by simp + by linarith lemma real_of_int_floor_add_one_ge [simp]: "r \ real(floor r) + 1" - unfolding real_of_int_def using floor_correct [of r] by simp + by linarith lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1" - unfolding real_of_int_def using floor_correct [of r] by simp + by linarith lemma le_floor: "real a <= x ==> a <= floor x" - unfolding real_of_int_def by (simp add: le_floor_iff) + by linarith lemma real_le_floor: "a <= floor x ==> real a <= x" - unfolding real_of_int_def by (simp add: le_floor_iff) + by linarith lemma le_floor_eq: "(a <= floor x) = (real a <= x)" - unfolding real_of_int_def by (rule le_floor_iff) + by linarith lemma floor_less_eq: "(floor x < a) = (x < real a)" - unfolding real_of_int_def by (rule floor_less_iff) + by linarith lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)" - unfolding real_of_int_def by (rule less_floor_iff) + by linarith lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)" - unfolding real_of_int_def by (rule floor_le_iff) + by linarith lemma floor_add [simp]: "floor (x + real a) = floor x + a" - unfolding real_of_int_def by (rule floor_add_of_int) + by linarith lemma floor_subtract [simp]: "floor (x - real a) = floor x - a" - unfolding real_of_int_def by (rule floor_diff_of_int) + by linarith lemma le_mult_floor: assumes "0 \ (a :: real)" and "0 \ b" @@ -1746,56 +1747,56 @@ qed (auto simp: real_of_int_div) lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n" - unfolding real_of_nat_def by simp + by linarith lemma real_of_int_ceiling_ge [simp]: "r \ real (ceiling r)" - unfolding real_of_int_def by (rule le_of_int_ceiling) + by linarith lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n" - unfolding real_of_int_def by simp + by linarith lemma real_of_int_ceiling_cancel [simp]: "(real (ceiling x) = x) = (\n::int. x = real n)" using ceiling_real_of_int by metis lemma ceiling_eq: "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1" - unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp + by linarith lemma ceiling_eq2: "[| real n < x; x \ real n + 1 |] ==> ceiling x = n + 1" - unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp + by linarith lemma ceiling_eq3: "[| real n - 1 < x; x \ real n |] ==> ceiling x = n" - unfolding real_of_int_def using ceiling_unique [of n x] by simp + by linarith lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \ r" - unfolding real_of_int_def using ceiling_correct [of r] by simp + by linarith lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \ r + 1" - unfolding real_of_int_def using ceiling_correct [of r] by simp + by linarith lemma ceiling_le: "x <= real a ==> ceiling x <= a" - unfolding real_of_int_def by (simp add: ceiling_le_iff) + by linarith lemma ceiling_le_real: "ceiling x <= a ==> x <= real a" - unfolding real_of_int_def by (simp add: ceiling_le_iff) + by linarith lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)" - unfolding real_of_int_def by (rule ceiling_le_iff) + by linarith lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)" - unfolding real_of_int_def by (rule less_ceiling_iff) + by linarith lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a - 1)" - unfolding real_of_int_def by (rule ceiling_less_iff) + by linarith lemma le_ceiling_eq: "(a <= ceiling x) = (real a - 1 < x)" - unfolding real_of_int_def by (rule le_ceiling_iff) + by linarith lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a" - unfolding real_of_int_def by (rule ceiling_add_of_int) + by linarith lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a" - unfolding real_of_int_def by (rule ceiling_diff_of_int) + by linarith subsubsection {* Versions for the natural numbers *} @@ -1808,111 +1809,88 @@ natceiling :: "real => nat" where "natceiling x = nat(ceiling x)" +lemma natfloor_split[arith_split]: "P (natfloor t) \ (t < 0 \ P 0) \ (\n. of_nat n \ t \ t < of_nat n + 1 \ P n)" +proof - + have [dest]: "\n m::nat. real n \ t \ t < real n + 1 \ real m \ t \ t < real m + 1 \ n = m" + by simp + show ?thesis + by (auto simp: natfloor_def real_of_nat_def[symmetric] split: split_nat floor_split) +qed + +lemma natceiling_split[arith_split]: + "P (natceiling t) \ (t \ - 1 \ P 0) \ (\n. of_nat n - 1 < t \ t \ of_nat n \ P n)" +proof - + have [dest]: "\n m::nat. real n - 1 < t \ t \ real n \ real m - 1 < t \ t \ real m \ n = m" + by simp + show ?thesis + by (auto simp: natceiling_def real_of_nat_def[symmetric] split: split_nat ceiling_split) +qed + lemma natfloor_zero [simp]: "natfloor 0 = 0" - by (unfold natfloor_def, simp) + by linarith lemma natfloor_one [simp]: "natfloor 1 = 1" - by (unfold natfloor_def, simp) - -lemma zero_le_natfloor [simp]: "0 <= natfloor x" - by (unfold natfloor_def, simp) + by linarith lemma natfloor_numeral_eq [simp]: "natfloor (numeral n) = numeral n" by (unfold natfloor_def, simp) lemma natfloor_real_of_nat [simp]: "natfloor(real n) = n" - by (unfold natfloor_def, simp) + by linarith lemma real_natfloor_le: "0 <= x ==> real(natfloor x) <= x" - by (unfold natfloor_def, simp) + by linarith lemma natfloor_neg: "x <= 0 ==> natfloor x = 0" - unfolding natfloor_def by simp + by linarith lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y" - unfolding natfloor_def by (intro nat_mono floor_mono) + by linarith lemma le_natfloor: "real x <= a ==> x <= natfloor a" - apply (unfold natfloor_def) - apply (subst nat_int [THEN sym]) - apply (rule nat_mono) - apply (rule le_floor) - apply simp -done + by linarith lemma natfloor_less_iff: "0 \ x \ natfloor x < n \ x < real n" - unfolding natfloor_def real_of_nat_def - by (simp add: nat_less_iff floor_less_iff) + by linarith -lemma less_natfloor: - assumes "0 \ x" and "x < real (n :: nat)" - shows "natfloor x < n" - using assms by (simp add: natfloor_less_iff) +lemma less_natfloor: "0 \ x \ x < real (n :: nat) \ natfloor x < n" + by linarith lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)" - apply (rule iffI) - apply (rule order_trans) - prefer 2 - apply (erule real_natfloor_le) - apply (subst real_of_nat_le_iff) - apply assumption - apply (erule le_natfloor) -done + by linarith lemma le_natfloor_eq_numeral [simp]: - "~ neg((numeral n)::int) ==> 0 <= x ==> - (numeral n <= natfloor x) = (numeral n <= x)" - apply (subst le_natfloor_eq, assumption) - apply simp -done + "0 \ x \ (numeral n \ natfloor x) = (numeral n \ x)" + by (subst le_natfloor_eq, assumption) simp + +lemma le_natfloor_eq_one [simp]: "(1 \ natfloor x) = (1 \ x)" + by linarith -lemma le_natfloor_eq_one [simp]: "(1 <= natfloor x) = (1 <= x)" - apply (case_tac "0 <= x") - apply (subst le_natfloor_eq, assumption, simp) - apply (rule iffI) - apply (subgoal_tac "natfloor x <= natfloor 0") - apply simp - apply (rule natfloor_mono) - apply simp - apply simp -done +lemma natfloor_eq: "real n \ x \ x < real n + 1 \ natfloor x = n" + by linarith -lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n" - unfolding natfloor_def by (simp add: floor_eq2 [where n="int n"]) - -lemma real_natfloor_add_one_gt: "x < real(natfloor x) + 1" - apply (case_tac "0 <= x") - apply (unfold natfloor_def) - apply simp - apply simp_all -done +lemma real_natfloor_add_one_gt: "x < real (natfloor x) + 1" + by linarith lemma real_natfloor_gt_diff_one: "x - 1 < real(natfloor x)" -using real_natfloor_add_one_gt by (simp add: algebra_simps) + by linarith lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n" - apply (subgoal_tac "z < real(natfloor z) + 1") - apply arith - apply (rule real_natfloor_add_one_gt) -done + by linarith lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a" - unfolding natfloor_def - unfolding real_of_int_of_nat_eq [symmetric] floor_add - by (simp add: nat_add_distrib) + by linarith lemma natfloor_add_numeral [simp]: - "~neg ((numeral n)::int) ==> 0 <= x ==> - natfloor (x + numeral n) = natfloor x + numeral n" + "0 <= x \ natfloor (x + numeral n) = natfloor x + numeral n" by (simp add: natfloor_add [symmetric]) lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1" - by (simp add: natfloor_add [symmetric] del: One_nat_def) + by linarith lemma natfloor_subtract [simp]: "natfloor(x - real a) = natfloor x - a" - unfolding natfloor_def real_of_int_of_nat_eq [symmetric] floor_subtract - by simp + by linarith lemma natfloor_div_nat: assumes "1 <= x" and "y > 0" @@ -1939,67 +1917,57 @@ (auto simp add: le_natfloor_eq mult_mono' real_natfloor_le natfloor_neg) lemma natceiling_zero [simp]: "natceiling 0 = 0" - by (unfold natceiling_def, simp) + by linarith lemma natceiling_one [simp]: "natceiling 1 = 1" - by (unfold natceiling_def, simp) + by linarith lemma zero_le_natceiling [simp]: "0 <= natceiling x" - by (unfold natceiling_def, simp) + by linarith lemma natceiling_numeral_eq [simp]: "natceiling (numeral n) = numeral n" - by (unfold natceiling_def, simp) + by (simp add: natceiling_def) lemma natceiling_real_of_nat [simp]: "natceiling(real n) = n" - by (unfold natceiling_def, simp) + by linarith lemma real_natceiling_ge: "x <= real(natceiling x)" - unfolding natceiling_def by (cases "x < 0", simp_all) + by linarith lemma natceiling_neg: "x <= 0 ==> natceiling x = 0" - unfolding natceiling_def by simp + by linarith lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y" - unfolding natceiling_def by (intro nat_mono ceiling_mono) + by linarith lemma natceiling_le: "x <= real a ==> natceiling x <= a" - unfolding natceiling_def real_of_nat_def - by (simp add: nat_le_iff ceiling_le_iff) + by linarith lemma natceiling_le_eq: "(natceiling x <= a) = (x <= real a)" - unfolding natceiling_def real_of_nat_def - by (simp add: nat_le_iff ceiling_le_iff) + by linarith lemma natceiling_le_eq_numeral [simp]: - "~ neg((numeral n)::int) ==> - (natceiling x <= numeral n) = (x <= numeral n)" + "(natceiling x <= numeral n) = (x <= numeral n)" by (simp add: natceiling_le_eq) lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)" - unfolding natceiling_def - by (simp add: nat_le_iff ceiling_le_iff) + by linarith lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1" - unfolding natceiling_def - by (simp add: ceiling_eq2 [where n="int n"]) + by linarith -lemma natceiling_add [simp]: "0 <= x ==> - natceiling (x + real a) = natceiling x + a" - unfolding natceiling_def - unfolding real_of_int_of_nat_eq [symmetric] ceiling_add - by (simp add: nat_add_distrib) +lemma natceiling_add [simp]: "0 <= x ==> natceiling (x + real a) = natceiling x + a" + by linarith lemma natceiling_add_numeral [simp]: - "~ neg ((numeral n)::int) ==> 0 <= x ==> - natceiling (x + numeral n) = natceiling x + numeral n" + "0 <= x ==> natceiling (x + numeral n) = natceiling x + numeral n" by (simp add: natceiling_add [symmetric]) lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1" - by (simp add: natceiling_add [symmetric] del: One_nat_def) + by linarith lemma natceiling_subtract [simp]: "natceiling(x - real a) = natceiling x - a" - unfolding natceiling_def real_of_int_of_nat_eq [symmetric] ceiling_subtract - by simp + by linarith lemma Rats_no_top_le: "\ q \ \. (x :: real) \ q" by (auto intro!: bexI[of _ "of_nat (natceiling x)"]) (metis real_natceiling_ge real_of_nat_def) diff -r aa6296d09e0e -r 930727de976c src/HOL/TPTP/THF_Arith.thy --- a/src/HOL/TPTP/THF_Arith.thy Wed Aug 27 14:54:32 2014 +0200 +++ b/src/HOL/TPTP/THF_Arith.thy Wed Aug 27 14:55:33 2014 +0200 @@ -51,7 +51,7 @@ overloading real_to_rat \ "to_rat :: real \ rat" begin - definition "real_to_rat (x\real) = (inv real x\rat)" + definition "real_to_rat (x\real) = (inv of_rat x\rat)" end overloading int_to_real \ "to_real :: int \ real" @@ -85,6 +85,6 @@ by (metis Rats_of_rat rat_to_real_def real_is_rat_def) lemma inj_of_rat [intro, simp]: "inj (of_rat\rat\real)" -by (metis injI of_rat_eq_iff rat_to_real_def) +by (metis injI of_rat_eq_iff) end diff -r aa6296d09e0e -r 930727de976c src/HOL/Tools/ATP/atp_satallax.ML --- a/src/HOL/Tools/ATP/atp_satallax.ML Wed Aug 27 14:54:32 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_satallax.ML Wed Aug 27 14:55:33 2014 +0200 @@ -99,7 +99,7 @@ if state = 1 orelse state = 0 then sep_dep l used_assumptions (x :: new_goals) generated_assumptions 1 else - raise Fail ("incorrect Satallax proof" ^ PolyML.makestring l) + raise Fail ("incorrect Satallax proof: " ^ @{make_string} l) in sep_dep dependencies [] [] [] 0 end @@ -154,7 +154,7 @@ fun find_proof_step ((x as Satallax_Step {id, ...}) :: l) h = if h = id then x else find_proof_step l h - | find_proof_step [] h = raise Fail ("not_found: " ^ PolyML.makestring h ^ "(probably a parsing \ + | find_proof_step [] h = raise Fail ("not_found: " ^ @{make_string} h ^ " (probably a parsing \ \error)") fun remove_not_not (x as ATerm ((op1, _), [ATerm ((op2, _), [th])])) = diff -r aa6296d09e0e -r 930727de976c src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Aug 27 14:54:32 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Aug 27 14:55:33 2014 +0200 @@ -103,7 +103,6 @@ val map_disc_iffN = "map_disc_iff"; val map_selN = "map_sel"; val set_casesN = "set_cases"; -val set_emptyN = "set_empty"; val set_introsN = "set_intros"; val set_inductN = "set_induct"; val set_selN = "set_sel"; @@ -1429,42 +1428,6 @@ |> map (unfold_thms lthy @{thms insert_is_Un[THEN sym] Un_empty_left Un_insert_left}); - val sets = map (mk_set (snd (Term.dest_Type fpT))) (sets_of_bnf fp_bnf); - - val set_empty_thms = - let - val ctr_argT_namess = map ((fn Ts => fold Term.add_tfree_namesT Ts []) o - binder_types o fastype_of) ctrs; - val setTs = map (HOLogic.dest_setT o range_type o fastype_of) sets; - val setT_names = map (fn T => the_single (Term.add_tfree_namesT T [])) setTs; - - fun mk_set_empty_goal disc set T = - Logic.mk_implies (HOLogic.mk_Trueprop (disc $ u), - mk_Trueprop_eq (set $ u, HOLogic.mk_set T [])); - - val goals = - if null discs then - [] - else - map_filter I (flat - (map2 (fn names => fn disc => - map3 (fn name => fn setT => fn set => - if member (op =) names name then NONE - else SOME (mk_set_empty_goal disc set setT)) - setT_names setTs sets) - ctr_argT_namess discs)); - in - if null goals then - [] - else - Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) - (fn {context = ctxt, prems = _} => - mk_set_empty_tac ctxt (certify ctxt u) exhaust set0_thms (flat disc_thmss)) - |> Conjunction.elim_balanced (length goals) - |> Proof_Context.export names_lthy lthy - |> map Thm.close_derivation - end; - val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns); fun mk_rel_thm postproc ctr_defs' cxIn cyIn = @@ -1538,7 +1501,7 @@ val goals = mk_parametricity_goals names_lthy Rs ctrAs ctrBs; in Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) - (fn {context = ctxt, prems = _} => mk_ctr_transfer_tac rel_intro_thms) + (K (mk_ctr_transfer_tac rel_intro_thms)) |> Conjunction.elim_balanced (length goals) |> Proof_Context.export names_lthy lthy |> map Thm.close_derivation @@ -1596,7 +1559,7 @@ val thm = Goal.prove_sorry lthy [] (flat premss) goal (fn {context = ctxt, prems} => - mk_set_cases_tac ctxt (certify ctxt ta) prems exhaust set_thms) + mk_set_cases_tac ctxt (certify ctxt ta) prems exhaust set_thms) |> singleton (Proof_Context.export names_lthy lthy) |> Thm.close_derivation |> rotate_prems ~1; @@ -1680,9 +1643,9 @@ else Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) (fn {context = ctxt, prems = _} => - mk_rel_sel_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust - (flat disc_thmss) (flat sel_thmss) rel_inject_thms distincts - rel_distinct_thms) + mk_rel_sel_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust + (flat disc_thmss) (flat sel_thmss) rel_inject_thms distincts + rel_distinct_thms) |> Conjunction.elim_balanced (length goals) |> Proof_Context.export names_lthy lthy |> map Thm.close_derivation @@ -1718,9 +1681,9 @@ val thm = Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => - mk_rel_cases_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust - injects rel_inject_thms distincts rel_distinct_thms - (map rel_eq_of_bnf live_nesting_bnfs)) + mk_rel_cases_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust + injects rel_inject_thms distincts rel_distinct_thms + (map rel_eq_of_bnf live_nesting_bnfs)) |> singleton (Proof_Context.export names_lthy lthy) |> Thm.close_derivation; @@ -1751,8 +1714,8 @@ else Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) (fn {context = ctxt, prems = _} => - mk_map_disc_iff_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss) - map_thms) + mk_map_disc_iff_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss) + map_thms) |> Conjunction.elim_balanced (length goals) |> Proof_Context.export names_lthy lthy |> map Thm.close_derivation @@ -1778,6 +1741,7 @@ if is_refl_bool prem then concl else Logic.mk_implies (HOLogic.mk_Trueprop prem, concl) end; + val goals = map mk_goal discAs_selAss; in if null goals then @@ -1785,8 +1749,8 @@ else Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) (fn {context = ctxt, prems = _} => - mk_map_sel_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss) - map_thms (flat sel_thmss)) + mk_map_sel_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss) + map_thms (flat sel_thmss)) |> Conjunction.elim_balanced (length goals) |> Proof_Context.export names_lthy lthy |> map Thm.close_derivation @@ -1878,7 +1842,6 @@ (rel_selN, rel_sel_thms, K []), (setN, set_thms, K (code_nitpicksimp_attrs @ simp_attrs)), (set_casesN, set_cases_thms, nth set_cases_attrss), - (set_emptyN, set_empty_thms, K []), (set_introsN, set_intros_thms, K []), (set_selN, set_sel_thms, K [])] |> massage_simple_notes fp_b_name; diff -r aa6296d09e0e -r 930727de976c src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed Aug 27 14:54:32 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed Aug 27 14:55:33 2014 +0200 @@ -40,7 +40,6 @@ val mk_rel_sel_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> thm list -> thm list -> thm list -> tactic val mk_set_cases_tac: Proof.context -> cterm -> thm list -> thm -> thm list -> tactic - val mk_set_empty_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic val mk_set_induct0_tac: Proof.context -> cterm list -> thm list -> thm list -> thm list -> thm list -> thm list -> thm list -> thm list -> tactic val mk_set_intros_tac: Proof.context -> thm list -> tactic @@ -317,14 +316,6 @@ hyp_subst_tac ctxt ORELSE' SELECT_GOAL (SOLVE (HEADGOAL (eresolve_tac assms THEN' REPEAT_DETERM o atac))))); -fun mk_set_empty_tac ctxt ct exhaust sets discs = - TRYALL Goal.conjunction_tac THEN - ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW - REPEAT_DETERM o hyp_subst_tac ctxt) THEN - unfold_thms_tac ctxt (sets @ map_filter (fn thm => - SOME (thm RS eqFalseI) handle THM _ => NONE) discs) THEN - ALLGOALS (rtac refl ORELSE' etac FalseE); - fun mk_set_intros_tac ctxt sets = TRYALL Goal.conjunction_tac THEN unfold_thms_tac ctxt sets THEN