--- 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"
--- 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]}
--- 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 \<le> z \<longleftrightarrow> x < of_int z + 1"
by (simp add: not_less [symmetric] less_floor_iff)
+lemma floor_split[arith_split]: "P (floor t) \<longleftrightarrow> (\<forall>i. of_int i \<le> t \<and> t < of_int i + 1 \<longrightarrow> P i)"
+ by (metis floor_correct floor_unique less_floor_iff not_le order_refl)
+
lemma floor_mono: assumes "x \<le> y" shows "floor x \<le> floor y"
proof -
have "of_int (floor x) \<le> 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) \<longleftrightarrow> (\<forall>i. of_int i - 1 < t \<and> t \<le> of_int i \<longrightarrow> P i)"
+ by (auto simp add: ceiling_unique ceiling_correct)
+
lemma ceiling_diff_floor_le_1: "ceiling x - floor x \<le> 1"
proof -
have "of_int \<lceil>x\<rceil> - 1 < x"
--- 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 \<Rightarrow> _"]]
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 \<Rightarrow> integer)))
- (term_of (num_of_integer i))"
+ "term_of (i :: integer) =
+ (if i > 0 then
+ App (Const (STR ''Num.numeral_class.numeral'') (TYPEREP(num \<Rightarrow> 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 \<Rightarrow> integer))
+ (term_of (- i)))"
by(rule term_of_anything[THEN meta_eq_to_obj_eq])
code_reserved Eval HOLogic
--- /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 \<Rightarrow> yxml_of_term"
+ where [code del]: "yot_literal _ = YXML"
+definition yot_append :: "yxml_of_term \<Rightarrow> yxml_of_term \<Rightarrow> yxml_of_term"
+ where [code del]: "yot_append _ _ = YXML"
+definition yot_concat :: "yxml_of_term list \<Rightarrow> 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
+ \<rightharpoonup> (SML) "string"
+ and (OCaml) "string"
+ and (Haskell) "String"
+ and (Scala) "String"
+| constant yot_empty
+ \<rightharpoonup> (SML) "\"\""
+ and (OCaml) "\"\""
+ and (Haskell) "\"\""
+ and (Scala) "\"\""
+| constant yot_literal
+ \<rightharpoonup> (SML) "_"
+ and (OCaml) "_"
+ and (Haskell) "_"
+ and (Scala) "_"
+| constant yot_append
+ \<rightharpoonup> (SML) "String.concat [(_), (_)]"
+ and (OCaml) "String.concat \"\" [(_); (_)]"
+ and (Haskell) infixr 5 "++"
+ and (Scala) infixl 5 "+"
+| constant yot_concat
+ \<rightharpoonup> (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 \<times> String.literal) list"
+type_synonym body = "xml_tree list"
+
+definition Elem :: "String.literal \<Rightarrow> attributes \<Rightarrow> xml_tree list \<Rightarrow> xml_tree"
+where [code del]: "Elem _ _ _ = XML_Tree"
+
+definition Text :: "String.literal \<Rightarrow> xml_tree"
+where [code del]: "Text _ = XML_Tree"
+
+definition node :: "xml_tree list \<Rightarrow> xml_tree"
+where "node ts = Elem (STR '':'') [] ts"
+
+definition tagged :: "String.literal \<Rightarrow> String.literal option \<Rightarrow> xml_tree list \<Rightarrow> xml_tree"
+where "tagged tag x ts = Elem tag (case x of None \<Rightarrow> [] | Some x' \<Rightarrow> [(STR ''0'', x')]) ts"
+
+definition list where "list f xs = map (node \<circ> 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 \<Rightarrow> yxml_of_term \<Rightarrow> 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 (\<lambda>(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 \<Rightarrow> 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 \<Rightarrow> xml.body"
+where [code del]: "xml_of_typ _ = [XML_Tree]"
+
+definition xml_of_term :: "Code_Evaluation.term \<Rightarrow> 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 \<Rightarrow> yxml_of_term"
+where "yxml_string_of_term = yxml_string_of_body \<circ> xml_of_term"
+
+subsection {* Test engine and drivers *}
+
+ML_file "code_test.ML"
+
+end
--- /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 \<Rightarrow> 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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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 \<Rightarrow> yxml_of_term) option"}
+ | mk_term_of ts =
+ let
+ val tuple = mk_tuples ts
+ val T = fastype_of tuple
+ in
+ @{term "Some :: (unit \<Rightarrow> yxml_of_term) \<Rightarrow> (unit \<Rightarrow> 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
+
--- 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 \<longleftrightarrow> a = b"
by (cases rule: ereal2_cases[of a b]) simp_all
-function of_ereal :: "ereal \<Rightarrow> real" where
- "of_ereal (ereal r) = r"
-| "of_ereal \<infinity> = 0"
-| "of_ereal (-\<infinity>) = 0"
+instantiation ereal :: real_of
+begin
+
+function real_ereal :: "ereal \<Rightarrow> real" where
+ "real_ereal (ereal r) = r"
+| "real_ereal \<infinity> = 0"
+| "real_ereal (-\<infinity>) = 0"
by (auto intro: ereal_cases)
termination by default (rule wf_empty)
-defs (overloaded)
- real_of_ereal_def [code_unfold]: "real \<equiv> of_ereal"
+instance ..
+end
lemma real_of_ereal[simp]:
"real (- x :: ereal) = - (real x)"
- "real (ereal r) = r"
- "real (\<infinity>::ereal) = 0"
- by (cases x) (simp_all add: real_of_ereal_def)
+ by (cases x) simp_all
lemma range_ereal[simp]: "range ereal = UNIV - {\<infinity>, -\<infinity>}"
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]: "\<bar>0\<bar> = (0::ereal)"
unfolding zero_ereal_def abs_ereal.simps by simp
--- 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 \<Rightarrow> real" where
real_of_float_def[code_unfold]: "real \<equiv> real_of_float"
+instance ..
+end
+
lemma type_definition_float': "type_definition real float_of float"
using type_definition_float unfolding real_of_float_def .
--- 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) \<longleftrightarrow> (a \<noteq> b \<and> distinct (a # xs) \<and> 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 [] \<Rightarrow> [x] | y # xs \<Rightarrow> 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) \<Longrightarrow> remdups_adj xs ! i \<noteq> 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)
--- 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 {*
--- 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 \<equiv> of_rat"
-consts
- (*overloaded constant for injecting other types into "real"*)
- real :: "'a => real"
+class real_of =
+ fixes real :: "'a \<Rightarrow> real"
+
+instantiation nat :: real_of
+begin
+
+definition real_nat :: "nat \<Rightarrow> real" where real_of_nat_def [code_unfold]: "real \<equiv> 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 \<Rightarrow> real" where real_of_int_def [code_unfold]: "real \<equiv> of_int"
+
+instance ..
+end
declare [[coercion_enabled]]
declare [[coercion "real::nat\<Rightarrow>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 \<Rightarrow> real"})
- #> Lin_Arith.add_inj_const (@{const_name real}, @{typ "int \<Rightarrow> real"}))
+ #> Lin_Arith.add_inj_const (@{const_name real}, @{typ "int \<Rightarrow> real"})
+ #> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat \<Rightarrow> real"})
+ #> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int \<Rightarrow> 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: " \<exists>n::int. real n \<le> r & r < real (n+1)"
unfolding real_of_int_def by (rule floor_exists)
-lemma lemma_floor:
- assumes a1: "real m \<le> r" and a2: "r < real n + 1"
- shows "m \<le> (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 \<le> r \<Longrightarrow> r < real n + 1 \<Longrightarrow> m \<le> (n::int)"
+ by simp
lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r"
unfolding real_of_int_def by (rule of_int_floor_le)
lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \<le> x"
-by (auto intro: lemma_floor)
+ by simp
lemma real_of_int_floor_cancel [simp]:
"(real (floor x) = x) = (\<exists>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 \<le> 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 \<le> 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 \<le> 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 \<le> 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 \<le> (a :: real)" and "0 \<le> 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 \<le> 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) = (\<exists>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 \<le> 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 \<le> 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 \<le> 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) \<le> 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) \<longleftrightarrow> (t < 0 \<longrightarrow> P 0) \<and> (\<forall>n. of_nat n \<le> t \<and> t < of_nat n + 1 \<longrightarrow> P n)"
+proof -
+ have [dest]: "\<And>n m::nat. real n \<le> t \<Longrightarrow> t < real n + 1 \<Longrightarrow> real m \<le> t \<Longrightarrow> t < real m + 1 \<Longrightarrow> 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) \<longleftrightarrow> (t \<le> - 1 \<longrightarrow> P 0) \<and> (\<forall>n. of_nat n - 1 < t \<and> t \<le> of_nat n \<longrightarrow> P n)"
+proof -
+ have [dest]: "\<And>n m::nat. real n - 1 < t \<Longrightarrow> t \<le> real n \<Longrightarrow> real m - 1 < t \<Longrightarrow> t \<le> real m \<Longrightarrow> 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 \<le> x \<Longrightarrow> natfloor x < n \<longleftrightarrow> 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 \<le> x" and "x < real (n :: nat)"
- shows "natfloor x < n"
- using assms by (simp add: natfloor_less_iff)
+lemma less_natfloor: "0 \<le> x \<Longrightarrow> x < real (n :: nat) \<Longrightarrow> 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 \<le> x \<Longrightarrow> (numeral n \<le> natfloor x) = (numeral n \<le> x)"
+ by (subst le_natfloor_eq, assumption) simp
+
+lemma le_natfloor_eq_one [simp]: "(1 \<le> natfloor x) = (1 \<le> 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 \<le> x \<Longrightarrow> x < real n + 1 \<Longrightarrow> 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 \<Longrightarrow> 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: "\<exists> q \<in> \<rat>. (x :: real) \<le> q"
by (auto intro!: bexI[of _ "of_nat (natceiling x)"]) (metis real_natceiling_ge real_of_nat_def)
--- 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 \<equiv> "to_rat :: real \<Rightarrow> rat"
begin
- definition "real_to_rat (x\<Colon>real) = (inv real x\<Colon>rat)"
+ definition "real_to_rat (x\<Colon>real) = (inv of_rat x\<Colon>rat)"
end
overloading int_to_real \<equiv> "to_real :: int \<Rightarrow> 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\<Colon>rat\<Rightarrow>real)"
-by (metis injI of_rat_eq_iff rat_to_real_def)
+by (metis injI of_rat_eq_iff)
end
--- 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])])) =
--- 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;
--- 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