Branch merge with updates from mainline isabelle.
--- a/NEWS Fri Sep 11 20:58:29 2009 +1000
+++ b/NEWS Thu Sep 17 14:17:37 2009 +1000
@@ -41,14 +41,6 @@
semidefinite programming solvers. For more information and examples
see src/HOL/Library/Sum_Of_Squares.
-* Set.UNIV and Set.empty are mere abbreviations for top and bot.
-INCOMPATIBILITY.
-
-* More convenient names for set intersection and union.
-INCOMPATIBILITY:
- Set.Int ~> Set.inter
- Set.Un ~> Set.union
-
* Code generator attributes follow the usual underscore convention:
code_unfold replaces code unfold
code_post replaces code post
@@ -57,16 +49,14 @@
* New class "boolean_algebra".
-* Refinements to lattices classes:
- - added boolean_algebra type class
+* Refinements to lattice classes and sets:
- less default intro/elim rules in locale variant, more default
intro/elim rules in class variant: more uniformity
- lemma ge_sup_conv renamed to le_sup_iff, in accordance with le_inf_iff
- dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and sup_aci)
- renamed ACI to inf_sup_aci
- class "complete_lattice" moved to separate theory "complete_lattice";
- corresponding constants renamed:
-
+ corresponding constants (and abbreviations) renamed:
Set.Inf ~> Complete_Lattice.Inf
Set.Sup ~> Complete_Lattice.Sup
Set.INFI ~> Complete_Lattice.INFI
@@ -75,6 +65,14 @@
Set.Union ~> Complete_Lattice.Union
Set.INTER ~> Complete_Lattice.INTER
Set.UNION ~> Complete_Lattice.UNION
+ - more convenient names for set intersection and union:
+ Set.Int ~> Set.inter
+ Set.Un ~> Set.union
+ - mere abbreviations:
+ Set.empty (for bot)
+ Set.UNIV (for top)
+ Complete_Lattice.Inter (for Inf)
+ Complete_Lattice.Union (for Sup)
INCOMPATIBILITY.
@@ -87,7 +85,7 @@
INCOMPATIBILITY.
* Power operations on relations and functions are now one dedicate
-constant compow with infix syntax "^^". Power operations on
+constant "compow" with infix syntax "^^". Power operations on
multiplicative monoids retains syntax "^" and is now defined generic
in class power. INCOMPATIBILITY.
--- a/doc-src/manual.bib Fri Sep 11 20:58:29 2009 +1000
+++ b/doc-src/manual.bib Thu Sep 17 14:17:37 2009 +1000
@@ -484,7 +484,7 @@
booktitle = {Types for Proofs and Programs, TYPES 2008},
publisher = {Springer},
series = {LNCS},
- volume = {????},
+ volume = {5497},
year = {2009}
}
--- a/src/HOL/Complete_Lattice.thy Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Complete_Lattice.thy Thu Sep 17 14:17:37 2009 +1000
@@ -203,8 +203,8 @@
subsection {* Union *}
-definition Union :: "'a set set \<Rightarrow> 'a set" where
- Sup_set_eq [symmetric]: "Union S = \<Squnion>S"
+abbreviation Union :: "'a set set \<Rightarrow> 'a set" where
+ "Union S \<equiv> \<Squnion>S"
notation (xsymbols)
Union ("\<Union>_" [90] 90)
@@ -216,7 +216,7 @@
have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)"
by auto
then show "x \<in> \<Union>A \<longleftrightarrow> x \<in> {x. \<exists>B\<in>A. x \<in> B}"
- by (simp add: Sup_set_eq [symmetric] Sup_fun_def Sup_bool_def) (simp add: mem_def)
+ by (simp add: Sup_fun_def Sup_bool_def) (simp add: mem_def)
qed
lemma Union_iff [simp, noatp]:
@@ -314,7 +314,7 @@
lemma UNION_eq_Union_image:
"(\<Union>x\<in>A. B x) = \<Union>(B`A)"
- by (simp add: SUPR_def SUPR_set_eq [symmetric] Sup_set_eq)
+ by (simp add: SUPR_def SUPR_set_eq [symmetric])
lemma Union_def:
"\<Union>S = (\<Union>x\<in>S. x)"
@@ -439,8 +439,8 @@
subsection {* Inter *}
-definition Inter :: "'a set set \<Rightarrow> 'a set" where
- Inf_set_eq [symmetric]: "Inter S = \<Sqinter>S"
+abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
+ "Inter S \<equiv> \<Sqinter>S"
notation (xsymbols)
Inter ("\<Inter>_" [90] 90)
@@ -452,7 +452,7 @@
have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"
by auto
then show "x \<in> \<Inter>A \<longleftrightarrow> x \<in> {x. \<forall>B \<in> A. x \<in> B}"
- by (simp add: Inf_fun_def Inf_bool_def Inf_set_eq [symmetric]) (simp add: mem_def)
+ by (simp add: Inf_fun_def Inf_bool_def) (simp add: mem_def)
qed
lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
@@ -541,7 +541,7 @@
lemma INTER_eq_Inter_image:
"(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
- by (simp add: INFI_def INFI_set_eq [symmetric] Inf_set_eq)
+ by (simp add: INFI_def INFI_set_eq [symmetric])
lemma Inter_def:
"\<Inter>S = (\<Inter>x\<in>S. x)"
--- a/src/HOL/Fact.thy Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Fact.thy Thu Sep 17 14:17:37 2009 +1000
@@ -8,7 +8,7 @@
header{*Factorial Function*}
theory Fact
-imports NatTransfer
+imports Nat_Transfer
begin
class fact =
--- a/src/HOL/Fun.thy Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Fun.thy Thu Sep 17 14:17:37 2009 +1000
@@ -7,6 +7,7 @@
theory Fun
imports Complete_Lattice
+uses ("Tools/transfer.ML")
begin
text{*As a simplification rule, it replaces all function equalities by
@@ -568,6 +569,16 @@
*}
+subsection {* Generic transfer procedure *}
+
+definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
+ where "TransferMorphism a B \<longleftrightarrow> True"
+
+use "Tools/transfer.ML"
+
+setup Transfer.setup
+
+
subsection {* Code generator setup *}
types_code
--- a/src/HOL/Imperative_HOL/Array.thy Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Imperative_HOL/Array.thy Thu Sep 17 14:17:37 2009 +1000
@@ -176,12 +176,11 @@
code_type array (OCaml "_/ array")
code_const Array (OCaml "failwith/ \"bare Array\"")
-code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ _/ _)")
+code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)")
code_const Array.of_list (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)")
-code_const Array.make' (OCaml "(fun/ ()/ ->/ Array.init/ _/ _)")
-code_const Array.length' (OCaml "(fun/ ()/ ->/ Array.length/ _)")
-code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ _)")
-code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ _/ _)")
+code_const Array.length' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
+code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))")
+code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)")
code_reserved OCaml Array
--- a/src/HOL/Imperative_HOL/ex/Sublist.thy Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Imperative_HOL/ex/Sublist.thy Thu Sep 17 14:17:37 2009 +1000
@@ -1,4 +1,3 @@
-(* $Id$ *)
header {* Slices of lists *}
@@ -6,7 +5,6 @@
imports Multiset
begin
-
lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}"
apply (induct xs arbitrary: i j k)
apply simp
--- a/src/HOL/Inductive.thy Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Inductive.thy Thu Sep 17 14:17:37 2009 +1000
@@ -111,8 +111,7 @@
and P_f: "!!S. P S ==> P(f S)"
and P_Union: "!!M. !S:M. P S ==> P(Union M)"
shows "P(lfp f)"
- using assms unfolding Sup_set_eq [symmetric]
- by (rule lfp_ordinal_induct [where P=P])
+ using assms by (rule lfp_ordinal_induct [where P=P])
text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct},
--- a/src/HOL/IntDiv.thy Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/IntDiv.thy Thu Sep 17 14:17:37 2009 +1000
@@ -1102,20 +1102,6 @@
thus ?thesis by simp
qed
-
-theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
-apply (simp split add: split_nat)
-apply (rule iffI)
-apply (erule exE)
-apply (rule_tac x = "int x" in exI)
-apply simp
-apply (erule exE)
-apply (rule_tac x = "nat x" in exI)
-apply (erule conjE)
-apply (erule_tac x = "nat x" in allE)
-apply simp
-done
-
theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
proof -
have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
--- a/src/HOL/IsaMakefile Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/IsaMakefile Thu Sep 17 14:17:37 2009 +1000
@@ -291,7 +291,7 @@
Log.thy \
Lubs.thy \
MacLaurin.thy \
- NatTransfer.thy \
+ Nat_Transfer.thy \
NthRoot.thy \
SEQ.thy \
Series.thy \
@@ -306,7 +306,7 @@
Real.thy \
RealVector.thy \
Tools/float_syntax.ML \
- Tools/transfer_data.ML \
+ Tools/transfer.ML \
Tools/Qelim/ferrante_rackoff_data.ML \
Tools/Qelim/ferrante_rackoff.ML \
Tools/Qelim/langford_data.ML \
@@ -901,7 +901,7 @@
ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \
ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
ex/Sudoku.thy ex/Tarski.thy \
- ex/Termination.thy ex/Unification.thy ex/document/root.bib \
+ ex/Termination.thy ex/Transfer_Ex.thy ex/Unification.thy ex/document/root.bib \
ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \
ex/Predicate_Compile.thy ex/predicate_compile.ML ex/Predicate_Compile_ex.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
--- a/src/HOL/Lattices.thy Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Lattices.thy Thu Sep 17 14:17:37 2009 +1000
@@ -12,7 +12,9 @@
notation
less_eq (infix "\<sqsubseteq>" 50) and
- less (infix "\<sqsubset>" 50)
+ less (infix "\<sqsubset>" 50) and
+ top ("\<top>") and
+ bot ("\<bottom>")
class lower_semilattice = order +
fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
@@ -220,6 +222,46 @@
end
+subsubsection {* Strict order *}
+
+context lower_semilattice
+begin
+
+lemma less_infI1:
+ "a \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
+ by (auto simp add: less_le intro: le_infI1)
+
+lemma less_infI2:
+ "b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
+ by (auto simp add: less_le intro: le_infI2)
+
+end
+
+context upper_semilattice
+begin
+
+lemma less_supI1:
+ "x < a \<Longrightarrow> x < a \<squnion> b"
+proof -
+ interpret dual: lower_semilattice "op \<ge>" "op >" sup
+ by (fact dual_semilattice)
+ assume "x < a"
+ then show "x < a \<squnion> b"
+ by (fact dual.less_infI1)
+qed
+
+lemma less_supI2:
+ "x < b \<Longrightarrow> x < a \<squnion> b"
+proof -
+ interpret dual: lower_semilattice "op \<ge>" "op >" sup
+ by (fact dual_semilattice)
+ assume "x < b"
+ then show "x < a \<squnion> b"
+ by (fact dual.less_infI2)
+qed
+
+end
+
subsection {* Distributive lattices *}
@@ -306,6 +348,40 @@
"x \<squnion> bot = x"
by (rule sup_absorb1) simp
+lemma inf_eq_top_eq1:
+ assumes "A \<sqinter> B = \<top>"
+ shows "A = \<top>"
+proof (cases "B = \<top>")
+ case True with assms show ?thesis by simp
+next
+ case False with top_greatest have "B < \<top>" by (auto intro: neq_le_trans)
+ then have "A \<sqinter> B < \<top>" by (rule less_infI2)
+ with assms show ?thesis by simp
+qed
+
+lemma inf_eq_top_eq2:
+ assumes "A \<sqinter> B = \<top>"
+ shows "B = \<top>"
+ by (rule inf_eq_top_eq1, unfold inf_commute [of B]) (fact assms)
+
+lemma sup_eq_bot_eq1:
+ assumes "A \<squnion> B = \<bottom>"
+ shows "A = \<bottom>"
+proof -
+ interpret dual: boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" top bot
+ by (rule dual_boolean_algebra)
+ from dual.inf_eq_top_eq1 assms show ?thesis .
+qed
+
+lemma sup_eq_bot_eq2:
+ assumes "A \<squnion> B = \<bottom>"
+ shows "B = \<bottom>"
+proof -
+ interpret dual: boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" top bot
+ by (rule dual_boolean_algebra)
+ from dual.inf_eq_top_eq2 assms show ?thesis .
+qed
+
lemma compl_unique:
assumes "x \<sqinter> y = bot"
and "x \<squnion> y = top"
@@ -517,6 +593,8 @@
less_eq (infix "\<sqsubseteq>" 50) and
less (infix "\<sqsubset>" 50) and
inf (infixl "\<sqinter>" 70) and
- sup (infixl "\<squnion>" 65)
+ sup (infixl "\<squnion>" 65) and
+ top ("\<top>") and
+ bot ("\<bottom>")
end
--- a/src/HOL/Library/Executable_Set.thy Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Library/Executable_Set.thy Thu Sep 17 14:17:37 2009 +1000
@@ -8,7 +8,7 @@
imports Main Fset
begin
-subsection {* Derived set operations *}
+subsection {* Preprocessor setup *}
declare member [code]
@@ -24,9 +24,7 @@
definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
[code del]: "eq_set = op ="
-(* FIXME allow for Stefan's code generator:
-declare set_eq_subset[code_unfold]
-*)
+(*declare eq_set_def [symmetric, code_unfold]*)
lemma [code]:
"eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
@@ -37,13 +35,20 @@
declare Inter_image_eq [symmetric, code]
declare Union_image_eq [symmetric, code]
-
-subsection {* Rewrites for primitive operations *}
-
declare List_Set.project_def [symmetric, code_unfold]
+definition Inter :: "'a set set \<Rightarrow> 'a set" where
+ "Inter = Complete_Lattice.Inter"
-subsection {* code generator setup *}
+declare Inter_def [symmetric, code_unfold]
+
+definition Union :: "'a set set \<Rightarrow> 'a set" where
+ "Union = Complete_Lattice.Union"
+
+declare Union_def [symmetric, code_unfold]
+
+
+subsection {* Code generator setup *}
ML {*
nonfix inter;
@@ -75,8 +80,8 @@
"op \<union>" ("{*Fset.union*}")
"op \<inter>" ("{*Fset.inter*}")
"op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
- "Complete_Lattice.Union" ("{*Fset.Union*}")
- "Complete_Lattice.Inter" ("{*Fset.Inter*}")
+ "Union" ("{*Fset.Union*}")
+ "Inter" ("{*Fset.Inter*}")
card ("{*Fset.card*}")
fold ("{*foldl o flip*}")
--- a/src/HOL/Mirabelle/Mirabelle.thy Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Mirabelle/Mirabelle.thy Thu Sep 17 14:17:37 2009 +1000
@@ -1,5 +1,5 @@
-(* Title: Mirabelle.thy
- Author: Jasmin Blanchette and Sascha Boehme
+(* Title: HOL/Mirabelle/Mirabelle.thy
+ Author: Jasmin Blanchette and Sascha Boehme, TU Munich
*)
theory Mirabelle
--- a/src/HOL/Mirabelle/Mirabelle_Test.thy Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Mirabelle/Mirabelle_Test.thy Thu Sep 17 14:17:37 2009 +1000
@@ -1,5 +1,5 @@
-(* Title: Mirabelle_Test.thy
- Author: Sascha Boehme
+(* Title: HOL/Mirabelle/Mirabelle_Test.thy
+ Author: Sascha Boehme, TU Munich
*)
header {* Simple test theory for Mirabelle actions *}
@@ -14,9 +14,9 @@
"Tools/mirabelle_sledgehammer.ML"
begin
-(*
- only perform type-checking of the actions,
- any reasonable test would be too complicated
-*)
+text {*
+ Only perform type-checking of the actions,
+ any reasonable test would be too complicated.
+*}
end
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Thu Sep 17 14:17:37 2009 +1000
@@ -1,27 +1,30 @@
-(* Title: mirabelle.ML
- Author: Jasmin Blanchette and Sascha Boehme
+(* Title: HOL/Mirabelle/Tools/mirabelle.ML
+ Author: Jasmin Blanchette and Sascha Boehme, TU Munich
*)
signature MIRABELLE =
sig
- (* configuration *)
+ (*configuration*)
val logfile : string Config.T
val timeout : int Config.T
val start_line : int Config.T
val end_line : int Config.T
val setup : theory -> theory
- (* core *)
- type init_action
- type done_action
- type run_action
- type action
+ (*core*)
+ type init_action = int -> theory -> theory
+ type done_args = {last: Toplevel.state, log: string -> unit}
+ type done_action = int -> done_args -> unit
+ type run_args = {pre: Proof.state, post: Toplevel.state option,
+ timeout: Time.time, log: string -> unit, pos: Position.T}
+ type run_action = int -> run_args -> unit
+ type action = init_action * run_action * done_action
val catch : (int -> string) -> run_action -> run_action
val register : action -> theory -> theory
val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
unit
- (* utility functions *)
+ (*utility functions*)
val goal_thm_of : Proof.state -> thm
val can_apply : Time.time -> (Proof.context -> int -> tactic) ->
Proof.state -> bool
@@ -47,14 +50,14 @@
val setup = setup1 #> setup2 #> setup3 #> setup4
-
(* Mirabelle core *)
-
type init_action = int -> theory -> theory
-type done_action = int -> {last: Toplevel.state, log: string -> unit} -> unit
-type run_action = int -> {pre: Proof.state, post: Toplevel.state option,
- timeout: Time.time, log: string -> unit, pos: Position.T} -> unit
+type done_args = {last: Toplevel.state, log: string -> unit}
+type done_action = int -> done_args -> unit
+type run_args = {pre: Proof.state, post: Toplevel.state option,
+ timeout: Time.time, log: string -> unit, pos: Position.T}
+type run_action = int -> run_args -> unit
type action = init_action * run_action * done_action
structure Actions = TheoryDataFun
@@ -70,7 +73,7 @@
fun app_with f g x = (g x; ())
handle (exn as Exn.Interrupt) => reraise exn | exn => (f exn; ())
-fun catch tag f id (st as {log, ...}) =
+fun catch tag f id (st as {log, ...}: run_args) =
let fun log_exn e = log (tag id ^ "exception:\n" ^ General.exnMessage e)
in app_with log_exn (f id) st end
--- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML Thu Sep 17 14:17:37 2009 +1000
@@ -1,5 +1,5 @@
-(* Title: mirabelle_arith.ML
- Author: Jasmin Blanchette and Sascha Boehme
+(* Title: HOL/Mirabelle/Tools/mirabelle_arith.ML
+ Author: Jasmin Blanchette and Sascha Boehme, TU Munich
*)
structure Mirabelle_Arith : MIRABELLE_ACTION =
@@ -10,7 +10,7 @@
fun init _ = I
fun done _ _ = ()
-fun run id {pre, timeout, log, ...} =
+fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) =
if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
then log (arith_tag id ^ "succeeded")
else ()
--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Thu Sep 17 14:17:37 2009 +1000
@@ -1,5 +1,5 @@
-(* Title: mirabelle_metis.ML
- Author: Jasmin Blanchette and Sascha Boehme
+(* Title: HOL/Mirabelle/Tools/mirabelle_metis.ML
+ Author: Jasmin Blanchette and Sascha Boehme, TU Munich
*)
structure Mirabelle_Metis : MIRABELLE_ACTION =
@@ -10,7 +10,7 @@
fun init _ = I
fun done _ _ = ()
-fun run id {pre, post, timeout, log} =
+fun run id ({pre, post, timeout, log, ...}: Mirabelle.run_args) =
let
val thms = Mirabelle.theorems_of_sucessful_proof post
val names = map Thm.get_name thms
--- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML Thu Sep 17 14:17:37 2009 +1000
@@ -1,5 +1,5 @@
-(* Title: mirabelle_quickcheck.ML
- Author: Jasmin Blanchette and Sascha Boehme
+(* Title: HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
+ Author: Jasmin Blanchette and Sascha Boehme, TU Munich
*)
structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
@@ -10,7 +10,7 @@
fun init _ = I
fun done _ _ = ()
-fun run args id {pre, timeout, log, ...} =
+fun run args id ({pre, timeout, log, ...}: Mirabelle.run_args) =
let
val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1
--- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Thu Sep 17 14:17:37 2009 +1000
@@ -1,5 +1,5 @@
-(* Title: mirabelle_refute.ML
- Author: Jasmin Blanchette and Sascha Boehme
+(* Title: HOL/Mirabelle/Tools/mirabelle_refute.ML
+ Author: Jasmin Blanchette and Sascha Boehme, TU Munich
*)
structure Mirabelle_Refute : MIRABELLE_ACTION =
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Sep 17 14:17:37 2009 +1000
@@ -1,5 +1,5 @@
-(* Title: mirabelle_sledgehammer.ML
- Author: Jasmin Blanchette and Sascha Boehme and Tobias Nipkow
+(* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
+ Author: Jasmin Blanchette and Sascha Boehme and Tobias Nipkow, TU Munich
*)
structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =
@@ -7,6 +7,7 @@
val proverK = "prover"
val prover_timeoutK = "prover_timeout"
+val prover_hard_timeoutK = "prover_hard_timeout"
val keepK = "keep"
val full_typesK = "full_types"
val minimizeK = "minimize"
@@ -22,6 +23,7 @@
datatype sh_data = ShData of {
calls: int,
success: int,
+ lemmas: int,
time_isa: int,
time_atp: int,
time_atp_fail: int}
@@ -35,46 +37,77 @@
posns: Position.T list
}
+datatype min_data = MinData of {
+ calls: int,
+ ratios: int,
+ lemmas: int
+ }
(* The first me_data component is only used if "minimize" is on.
Then it records how metis behaves with un-minimized lemmas.
*)
-datatype data = Data of sh_data * me_data * me_data
+datatype data = Data of sh_data * me_data * min_data * me_data
-fun make_sh_data (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail) =
- ShData{calls=sh_calls, success=sh_success, time_isa=sh_time_isa,
- time_atp=sh_time_atp, time_atp_fail=sh_time_atp_fail}
+fun make_sh_data (calls,success,lemmas,time_isa,time_atp,time_atp_fail) =
+ ShData{calls=calls, success=success, lemmas=lemmas, time_isa=time_isa,
+ time_atp=time_atp, time_atp_fail=time_atp_fail}
+
+fun make_min_data (calls, ratios, lemmas) =
+ MinData{calls=calls, ratios=ratios, lemmas=lemmas}
fun make_me_data (calls, success, time, timeout, lemmas, posns) =
MeData{calls=calls, success=success, time=time, timeout=timeout, lemmas=lemmas, posns=posns}
-val empty_data = Data(make_sh_data (0, 0, 0, 0, 0), make_me_data(0, 0, 0, 0, 0, []), make_me_data(0, 0, 0, 0, 0, []))
+val empty_data =
+ Data(make_sh_data (0, 0, 0, 0, 0, 0),
+ make_me_data(0, 0, 0, 0, 0, []),
+ MinData{calls=0, ratios=0, lemmas=0},
+ make_me_data(0, 0, 0, 0, 0, []))
fun map_sh_data f
- (Data (ShData{calls, success, time_isa, time_atp, time_atp_fail}, meda0, meda)) =
- Data (make_sh_data (f (calls, success, time_isa, time_atp, time_atp_fail)),
- meda0, meda)
+ (Data (ShData{calls, success, lemmas, time_isa, time_atp, time_atp_fail}, meda0, minda, meda)) =
+ Data (make_sh_data (f (calls, success, lemmas, time_isa, time_atp, time_atp_fail)),
+ meda0, minda, meda)
+
+fun map_min_data f
+ (Data(shda, meda0, MinData{calls,ratios,lemmas}, meda)) =
+ Data(shda, meda0, make_min_data(f(calls,ratios,lemmas)), meda)
+
+fun map_me_data0 f (Data (shda, MeData{calls,success,time,timeout,lemmas,posns}, minda, meda)) =
+ Data(shda, make_me_data(f (calls,success,time,timeout,lemmas,posns)), minda, meda)
-fun map_me_data0 f (Data (shda, MeData{calls,success,time,timeout,lemmas,posns}, meda)) =
- Data(shda, make_me_data(f (calls,success,time,timeout,lemmas,posns)), meda)
+fun map_me_data f (Data (shda, meda0, minda, MeData{calls,success,time,timeout,lemmas,posns})) =
+ Data(shda, meda0, minda, make_me_data(f (calls,success,time,timeout,lemmas,posns)))
-fun map_me_data f (Data (shda, meda0, MeData{calls,success,time,timeout,lemmas,posns})) =
- Data(shda, meda0, make_me_data(f (calls,success,time,timeout,lemmas,posns)))
+val inc_sh_calls =
+ map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail)
+ => (calls + 1, success, lemmas, time_isa, time_atp, time_atp_fail))
+
+val inc_sh_success =
+ map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail)
+ => (calls, success + 1, lemmas, time_isa, time_atp, time_atp_fail))
-val inc_sh_calls = map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
- => (sh_calls + 1, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail))
+fun inc_sh_lemmas n =
+ map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail)
+ => (calls, success, lemmas + n, time_isa, time_atp, time_atp_fail))
-val inc_sh_success = map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
- => (sh_calls, sh_success + 1, sh_time_isa, sh_time_atp, sh_time_atp_fail))
+fun inc_sh_time_isa t =
+ map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail)
+ => (calls, success, lemmas, time_isa + t, time_atp, time_atp_fail))
-fun inc_sh_time_isa t = map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
- => (sh_calls, sh_success, sh_time_isa + t, sh_time_atp, sh_time_atp_fail))
+fun inc_sh_time_atp t =
+ map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail)
+ => (calls, success, lemmas, time_isa, time_atp + t, time_atp_fail))
-fun inc_sh_time_atp t = map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
- => (sh_calls, sh_success, sh_time_isa, sh_time_atp + t, sh_time_atp_fail))
+fun inc_sh_time_atp_fail t =
+ map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail)
+ => (calls, success, lemmas, time_isa, time_atp, time_atp_fail + t))
-fun inc_sh_time_atp_fail t = map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
- => (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail + t))
+val inc_min_calls =
+ map_min_data (fn (calls, ratios, lemmas) => (calls + 1, ratios, lemmas))
+
+fun inc_min_ratios n =
+ map_min_data (fn (calls, ratios, lemmas) => (calls, ratios + n, lemmas))
val inc_metis_calls = map_me_data
(fn (calls, success, time, timeout, lemmas,posns)
@@ -133,9 +166,10 @@
fun avg_time t n =
if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0
-fun log_sh_data log sh_calls sh_success sh_time_isa sh_time_atp sh_time_atp_fail =
+fun log_sh_data log sh_calls sh_success sh_lemmas sh_time_isa sh_time_atp sh_time_atp_fail =
(log ("Total number of sledgehammer calls: " ^ str sh_calls);
log ("Number of successful sledgehammer calls: " ^ str sh_success);
+ log ("Number of sledgehammer lemmas: " ^ str sh_lemmas);
log ("Success rate: " ^ percentage sh_success sh_calls ^ "%");
log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time sh_time_isa));
log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time sh_time_atp));
@@ -161,7 +195,7 @@
log ("Number of " ^ tag ^ "metis exceptions: " ^
str (sh_success - metis_success - metis_timeout));
log ("Success rate: " ^ percentage metis_success sh_calls ^ "%");
- log ("Number of " ^ tag ^ "metis lemmas: " ^ str metis_lemmas);
+ log ("Number of successful " ^ tag ^ "metis lemmas: " ^ str metis_lemmas);
log ("Total time for successful metis calls: " ^ str3 (time metis_time));
log ("Average time for successful metis calls: " ^
str3 (avg_time metis_time metis_success));
@@ -169,22 +203,36 @@
then log ("Proved: " ^ space_implode " " (map str_of_pos metis_posns))
else ()
)
+
+fun log_min_data log calls ratios =
+ (log ("Number of minimizations: " ^ string_of_int calls);
+ log ("Minimization ratios: " ^ string_of_int ratios)
+ )
+
in
-fun log_data id log (Data (ShData{calls=sh_calls, success=sh_success, time_isa=sh_time_isa, time_atp=sh_time_atp, time_atp_fail=sh_time_atp_fail}, MeData{calls=metis_calls0,
- success=metis_success0, time=metis_time0, timeout=metis_timeout0, lemmas=metis_lemmas0,posns=metis_posns0}, MeData{calls=metis_calls,
- success=metis_success, time=metis_time, timeout=metis_timeout, lemmas=metis_lemmas,posns=metis_posns})) =
+fun log_data id log (Data
+ (ShData{calls=sh_calls, lemmas=sh_lemmas, success=sh_success,
+ time_isa=sh_time_isa,time_atp=sh_time_atp,time_atp_fail=sh_time_atp_fail},
+ MeData{calls=metis_calls0,
+ success=metis_success0, time=metis_time0, timeout=metis_timeout0,
+ lemmas=metis_lemmas0,posns=metis_posns0},
+ MinData{calls=min_calls, ratios=min_ratios, lemmas=min_lemmas},
+ MeData{calls=metis_calls,
+ success=metis_success, time=metis_time, timeout=metis_timeout,
+ lemmas=metis_lemmas,posns=metis_posns})) =
if sh_calls > 0
then
(log ("\n\n\nReport #" ^ string_of_int id ^ ":\n");
- log_sh_data log sh_calls sh_success sh_time_isa sh_time_atp sh_time_atp_fail;
+ log_sh_data log sh_calls sh_success sh_lemmas sh_time_isa sh_time_atp sh_time_atp_fail;
log "";
if metis_calls > 0 then log_metis_data log "" sh_calls sh_success metis_calls
metis_success metis_time metis_timeout metis_lemmas metis_posns else ();
log "";
if metis_calls0 > 0
- then log_metis_data log "unminimized " sh_calls sh_success metis_calls0
- metis_success0 metis_time0 metis_timeout0 metis_lemmas0 metis_posns0
+ then (log_min_data log min_calls min_ratios; log "";
+ log_metis_data log "unminimized " sh_calls sh_success metis_calls0
+ metis_success0 metis_time0 metis_timeout0 metis_lemmas0 metis_posns0)
else ()
)
else ()
@@ -196,7 +244,7 @@
val data = ref ([] : (int * data) list)
fun init id thy = (change data (cons (id, empty_data)); thy)
-fun done id {log, ...} =
+fun done id ({log, ...}: Mirabelle.done_args) =
AList.lookup (op =) (!data) id
|> Option.map (log_data id log)
|> K ()
@@ -233,17 +281,22 @@
SH_FAIL of int * int |
SH_ERROR
-fun run_sh (prover_name, prover) timeout st _ =
+fun run_sh (prover_name, prover) hard_timeout timeout st _ =
let
val atp = prover timeout NONE NONE prover_name 1
+ val time_limit =
+ (case hard_timeout of
+ NONE => I
+ | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
val ((success, (message, thm_names), time_atp, _, _, _), time_isa) =
- Mirabelle.cpu_time atp (Proof.get_goal st)
+ time_limit (Mirabelle.cpu_time atp) (Proof.get_goal st)
in
if success then (message, SH_OK (time_isa, time_atp, thm_names))
else (message, SH_FAIL(time_isa, time_atp))
end
handle ResHolClause.TOO_TRIVIAL => ("trivial", SH_OK (0, 0, []))
| ERROR msg => ("error: " ^ msg, SH_ERROR)
+ | TimeLimit.TimeOut => ("timeout", SH_ERROR)
fun thms_of_name ctxt name =
let
@@ -260,18 +313,22 @@
in
-fun run_sledgehammer args named_thms id {pre=st, log, ...} =
+fun run_sledgehammer args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
let
val _ = change_data id inc_sh_calls
val atp as (prover_name, _) = get_atp (Proof.theory_of st) args
val dir = AList.lookup (op =) args keepK
val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
- val (msg, result) = safe init_sh done_sh (run_sh atp timeout st) dir
+ val hard_timeout = AList.lookup (op =) args prover_hard_timeoutK
+ |> Option.map (fst o read_int o explode)
+ val (msg, result) = safe init_sh done_sh
+ (run_sh atp hard_timeout timeout st) dir
in
case result of
SH_OK (time_isa, time_atp, names) =>
let
val _ = change_data id inc_sh_success
+ val _ = change_data id (inc_sh_lemmas (length names))
val _ = change_data id (inc_sh_time_isa time_isa)
val _ = change_data id (inc_sh_time_atp time_atp)
@@ -292,8 +349,9 @@
end
-fun run_minimize args named_thms id {pre=st, log, ...} =
+fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
let
+ val n0 = length (these (!named_thms))
val (prover_name, prover) = get_atp (Proof.theory_of st) args
val minimize = AtpMinimal.minimalize prover prover_name
val timeout =
@@ -302,24 +360,29 @@
|> the_default 5
val _ = log separator
in
- (case minimize timeout st (these (!named_thms)) of
- (SOME named_thms', msg) =>
- if length named_thms' = length (these (!named_thms))
- then log (minimize_tag id ^ "already minimal")
- else
- (named_thms := SOME named_thms';
- log (minimize_tag id ^ "succeeded:\n" ^ msg))
- | (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg))
+ case minimize timeout st (these (!named_thms)) of
+ (SOME (named_thms',its), msg) =>
+ (change_data id inc_min_calls;
+ change_data id (inc_min_ratios ((100*its) div n0));
+ if length named_thms' = n0
+ then log (minimize_tag id ^ "already minimal")
+ else (named_thms := SOME named_thms';
+ log (minimize_tag id ^ "succeeded:\n" ^ msg))
+ )
+ | (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg)
end
-fun run_metis (inc_metis_calls, inc_metis_success, inc_metis_time, inc_metis_timeout, inc_metis_lemmas, inc_metis_posns) args named_thms id {pre=st, timeout, log, pos, ...} =
+fun run_metis (inc_metis_calls, inc_metis_success, inc_metis_time, inc_metis_timeout,
+ inc_metis_lemmas, inc_metis_posns) args named_thms id
+ ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
let
fun metis thms ctxt = MetisTools.metis_tac ctxt thms
fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
| with_time (true, t) = (change_data id inc_metis_success;
+ change_data id (inc_metis_lemmas (length named_thms));
change_data id (inc_metis_time t);
change_data id (inc_metis_posns pos);
"succeeded (" ^ string_of_int t ^ ")")
@@ -329,17 +392,18 @@
val _ = log separator
val _ = change_data id inc_metis_calls
- val _ = change_data id (inc_metis_lemmas (length named_thms))
in
maps snd named_thms
|> timed_metis
|> log o prefix (metis_tag id)
end
-fun sledgehammer_action args id (st as {log, ...}) =
+fun sledgehammer_action args id (st as {log, ...}: Mirabelle.run_args) =
let
- val metis_fns = (inc_metis_calls, inc_metis_success, inc_metis_time, inc_metis_timeout, inc_metis_lemmas, inc_metis_posns)
- val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_time0, inc_metis_timeout0, inc_metis_lemmas0, inc_metis_posns0)
+ val metis_fns = (inc_metis_calls, inc_metis_success, inc_metis_time,
+ inc_metis_timeout, inc_metis_lemmas, inc_metis_posns)
+ val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_time0,
+ inc_metis_timeout0, inc_metis_lemmas0, inc_metis_posns0)
val named_thms = ref (NONE : (string * thm list) list option)
fun if_enabled k f =
@@ -349,9 +413,8 @@
val _ = Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st
val _ = if_enabled minimizeK
(Mirabelle.catch metis_tag (run_metis metis0_fns args (these (!named_thms))))
- val _ = if is_some (!named_thms)
- then Mirabelle.catch minimize_tag (run_minimize args named_thms) id st
- else ()
+ val _ = if_enabled minimizeK
+ (Mirabelle.catch minimize_tag (run_minimize args named_thms))
val _ = if is_some (!named_thms)
then Mirabelle.catch metis_tag (run_metis metis_fns args (these (!named_thms))) id st
else ()
--- a/src/HOL/Mirabelle/doc/options.txt Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Mirabelle/doc/options.txt Thu Sep 17 14:17:37 2009 +1000
@@ -1,9 +1,11 @@
Options for sledgehammer:
* prover=NAME: name of the external prover to call
- * prover_timeout=TIME: timeout for invoked ATP
+ * prover_timeout=TIME: timeout for invoked ATP (seconds of process time)
+ * prover_hard_timeout=TIME: timeout for invoked ATP (seconds of elapsed time)
* keep=PATH: path where to keep temporary files created by sledgehammer
* full_types: enable full-typed encoding
* minimize: enable minimization of theorem set found by sledgehammer
- * minimize_timeout=TIME: timeout for each minimization step
+ * minimize_timeout=TIME: timeout for each minimization step (seconds of
+ process time)
* metis: apply metis with the theorems found by sledgehammer
--- a/src/HOL/NatTransfer.thy Fri Sep 11 20:58:29 2009 +1000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,537 +0,0 @@
-(* Title: HOL/Library/NatTransfer.thy
- Authors: Jeremy Avigad and Amine Chaieb
-
- Sets up transfer from nats to ints and
- back.
-*)
-
-
-header {* NatTransfer *}
-
-theory NatTransfer
-imports Main Parity
-uses ("Tools/transfer_data.ML")
-begin
-
-subsection {* A transfer Method between isomorphic domains*}
-
-definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
- where "TransferMorphism a B = True"
-
-use "Tools/transfer_data.ML"
-
-setup TransferData.setup
-
-
-subsection {* Set up transfer from nat to int *}
-
-(* set up transfer direction *)
-
-lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
- by (simp add: TransferMorphism_def)
-
-declare TransferMorphism_nat_int[transfer
- add mode: manual
- return: nat_0_le
- labels: natint
-]
-
-(* basic functions and relations *)
-
-lemma transfer_nat_int_numerals:
- "(0::nat) = nat 0"
- "(1::nat) = nat 1"
- "(2::nat) = nat 2"
- "(3::nat) = nat 3"
- by auto
-
-definition
- tsub :: "int \<Rightarrow> int \<Rightarrow> int"
-where
- "tsub x y = (if x >= y then x - y else 0)"
-
-lemma tsub_eq: "x >= y \<Longrightarrow> tsub x y = x - y"
- by (simp add: tsub_def)
-
-
-lemma transfer_nat_int_functions:
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
- "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
- by (auto simp add: eq_nat_nat_iff nat_mult_distrib
- nat_power_eq nat_div_distrib nat_mod_distrib tsub_def)
-
-lemma transfer_nat_int_function_closures:
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
- "(x::int) >= 0 \<Longrightarrow> x^n >= 0"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
- "(0::int) >= 0"
- "(1::int) >= 0"
- "(2::int) >= 0"
- "(3::int) >= 0"
- "int z >= 0"
- apply (auto simp add: zero_le_mult_iff tsub_def)
- apply (case_tac "y = 0")
- apply auto
- apply (subst pos_imp_zdiv_nonneg_iff, auto)
- apply (case_tac "y = 0")
- apply force
- apply (rule pos_mod_sign)
- apply arith
-done
-
-lemma transfer_nat_int_relations:
- "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
- (nat (x::int) = nat y) = (x = y)"
- "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
- (nat (x::int) < nat y) = (x < y)"
- "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
- (nat (x::int) <= nat y) = (x <= y)"
- "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
- (nat (x::int) dvd nat y) = (x dvd y)"
- by (auto simp add: zdvd_int even_nat_def)
-
-declare TransferMorphism_nat_int[transfer add return:
- transfer_nat_int_numerals
- transfer_nat_int_functions
- transfer_nat_int_function_closures
- transfer_nat_int_relations
-]
-
-
-(* first-order quantifiers *)
-
-lemma transfer_nat_int_quantifiers:
- "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
- "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))"
- by (rule all_nat, rule ex_nat)
-
-(* should we restrict these? *)
-lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
- (ALL x. Q x \<longrightarrow> P x) = (ALL x. Q x \<longrightarrow> P' x)"
- by auto
-
-lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
- (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
- by auto
-
-declare TransferMorphism_nat_int[transfer add
- return: transfer_nat_int_quantifiers
- cong: all_cong ex_cong]
-
-
-(* if *)
-
-lemma nat_if_cong: "(if P then (nat x) else (nat y)) =
- nat (if P then x else y)"
- by auto
-
-declare TransferMorphism_nat_int [transfer add return: nat_if_cong]
-
-
-(* operations with sets *)
-
-definition
- nat_set :: "int set \<Rightarrow> bool"
-where
- "nat_set S = (ALL x:S. x >= 0)"
-
-lemma transfer_nat_int_set_functions:
- "card A = card (int ` A)"
- "{} = nat ` ({}::int set)"
- "A Un B = nat ` (int ` A Un int ` B)"
- "A Int B = nat ` (int ` A Int int ` B)"
- "{x. P x} = nat ` {x. x >= 0 & P(nat x)}"
- "{..n} = nat ` {0..int n}"
- "{m..n} = nat ` {int m..int n}" (* need all variants of these! *)
- apply (rule card_image [symmetric])
- apply (auto simp add: inj_on_def image_def)
- apply (rule_tac x = "int x" in bexI)
- apply auto
- apply (rule_tac x = "int x" in bexI)
- apply auto
- apply (rule_tac x = "int x" in bexI)
- apply auto
- apply (rule_tac x = "int x" in exI)
- apply auto
- apply (rule_tac x = "int x" in bexI)
- apply auto
- apply (rule_tac x = "int x" in bexI)
- apply auto
-done
-
-lemma transfer_nat_int_set_function_closures:
- "nat_set {}"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
- "x >= 0 \<Longrightarrow> nat_set {x..y}"
- "nat_set {x. x >= 0 & P x}"
- "nat_set (int ` C)"
- "nat_set A \<Longrightarrow> x : A \<Longrightarrow> x >= 0" (* does it hurt to turn this on? *)
- unfolding nat_set_def apply auto
-done
-
-lemma transfer_nat_int_set_relations:
- "(finite A) = (finite (int ` A))"
- "(x : A) = (int x : int ` A)"
- "(A = B) = (int ` A = int ` B)"
- "(A < B) = (int ` A < int ` B)"
- "(A <= B) = (int ` A <= int ` B)"
-
- apply (rule iffI)
- apply (erule finite_imageI)
- apply (erule finite_imageD)
- apply (auto simp add: image_def expand_set_eq inj_on_def)
- apply (drule_tac x = "int x" in spec, auto)
- apply (drule_tac x = "int x" in spec, auto)
- apply (drule_tac x = "int x" in spec, auto)
-done
-
-lemma transfer_nat_int_set_return_embed: "nat_set A \<Longrightarrow>
- (int ` nat ` A = A)"
- by (auto simp add: nat_set_def image_def)
-
-lemma transfer_nat_int_set_cong: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>
- {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
- by auto
-
-declare TransferMorphism_nat_int[transfer add
- return: transfer_nat_int_set_functions
- transfer_nat_int_set_function_closures
- transfer_nat_int_set_relations
- transfer_nat_int_set_return_embed
- cong: transfer_nat_int_set_cong
-]
-
-
-(* setsum and setprod *)
-
-(* this handles the case where the *domain* of f is nat *)
-lemma transfer_nat_int_sum_prod:
- "setsum f A = setsum (%x. f (nat x)) (int ` A)"
- "setprod f A = setprod (%x. f (nat x)) (int ` A)"
- apply (subst setsum_reindex)
- apply (unfold inj_on_def, auto)
- apply (subst setprod_reindex)
- apply (unfold inj_on_def o_def, auto)
-done
-
-(* this handles the case where the *range* of f is nat *)
-lemma transfer_nat_int_sum_prod2:
- "setsum f A = nat(setsum (%x. int (f x)) A)"
- "setprod f A = nat(setprod (%x. int (f x)) A)"
- apply (subst int_setsum [symmetric])
- apply auto
- apply (subst int_setprod [symmetric])
- apply auto
-done
-
-lemma transfer_nat_int_sum_prod_closure:
- "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
- "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
- unfolding nat_set_def
- apply (rule setsum_nonneg)
- apply auto
- apply (rule setprod_nonneg)
- apply auto
-done
-
-(* this version doesn't work, even with nat_set A \<Longrightarrow>
- x : A \<Longrightarrow> x >= 0 turned on. Why not?
-
- also: what does =simp=> do?
-
-lemma transfer_nat_int_sum_prod_closure:
- "(!!x. x : A ==> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
- "(!!x. x : A ==> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
- unfolding nat_set_def simp_implies_def
- apply (rule setsum_nonneg)
- apply auto
- apply (rule setprod_nonneg)
- apply auto
-done
-*)
-
-(* Making A = B in this lemma doesn't work. Why not?
- Also, why aren't setsum_cong and setprod_cong enough,
- with the previously mentioned rule turned on? *)
-
-lemma transfer_nat_int_sum_prod_cong:
- "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
- setsum f A = setsum g B"
- "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
- setprod f A = setprod g B"
- unfolding nat_set_def
- apply (subst setsum_cong, assumption)
- apply auto [2]
- apply (subst setprod_cong, assumption, auto)
-done
-
-declare TransferMorphism_nat_int[transfer add
- return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2
- transfer_nat_int_sum_prod_closure
- cong: transfer_nat_int_sum_prod_cong]
-
-(* lists *)
-
-definition
- embed_list :: "nat list \<Rightarrow> int list"
-where
- "embed_list l = map int l";
-
-definition
- nat_list :: "int list \<Rightarrow> bool"
-where
- "nat_list l = nat_set (set l)";
-
-definition
- return_list :: "int list \<Rightarrow> nat list"
-where
- "return_list l = map nat l";
-
-thm nat_0_le;
-
-lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>
- embed_list (return_list l) = l";
- unfolding embed_list_def return_list_def nat_list_def nat_set_def
- apply (induct l);
- apply auto;
-done;
-
-lemma transfer_nat_int_list_functions:
- "l @ m = return_list (embed_list l @ embed_list m)"
- "[] = return_list []";
- unfolding return_list_def embed_list_def;
- apply auto;
- apply (induct l, auto);
- apply (induct m, auto);
-done;
-
-(*
-lemma transfer_nat_int_fold1: "fold f l x =
- fold (%x. f (nat x)) (embed_list l) x";
-*)
-
-
-
-
-subsection {* Set up transfer from int to nat *}
-
-(* set up transfer direction *)
-
-lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
- by (simp add: TransferMorphism_def)
-
-declare TransferMorphism_int_nat[transfer add
- mode: manual
-(* labels: int-nat *)
- return: nat_int
-]
-
-
-(* basic functions and relations *)
-
-definition
- is_nat :: "int \<Rightarrow> bool"
-where
- "is_nat x = (x >= 0)"
-
-lemma transfer_int_nat_numerals:
- "0 = int 0"
- "1 = int 1"
- "2 = int 2"
- "3 = int 3"
- by auto
-
-lemma transfer_int_nat_functions:
- "(int x) + (int y) = int (x + y)"
- "(int x) * (int y) = int (x * y)"
- "tsub (int x) (int y) = int (x - y)"
- "(int x)^n = int (x^n)"
- "(int x) div (int y) = int (x div y)"
- "(int x) mod (int y) = int (x mod y)"
- by (auto simp add: int_mult tsub_def int_power zdiv_int zmod_int)
-
-lemma transfer_int_nat_function_closures:
- "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
- "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)"
- "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)"
- "is_nat x \<Longrightarrow> is_nat (x^n)"
- "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
- "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
- "is_nat 0"
- "is_nat 1"
- "is_nat 2"
- "is_nat 3"
- "is_nat (int z)"
- by (simp_all only: is_nat_def transfer_nat_int_function_closures)
-
-lemma transfer_int_nat_relations:
- "(int x = int y) = (x = y)"
- "(int x < int y) = (x < y)"
- "(int x <= int y) = (x <= y)"
- "(int x dvd int y) = (x dvd y)"
- "(even (int x)) = (even x)"
- by (auto simp add: zdvd_int even_nat_def)
-
-lemma UNIV_apply:
- "UNIV x = True"
- by (simp add: top_fun_eq top_bool_eq)
-
-declare TransferMorphism_int_nat[transfer add return:
- transfer_int_nat_numerals
- transfer_int_nat_functions
- transfer_int_nat_function_closures
- transfer_int_nat_relations
- UNIV_apply
-]
-
-
-(* first-order quantifiers *)
-
-lemma transfer_int_nat_quantifiers:
- "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"
- "(EX (x::int) >= 0. P x) = (EX (x::nat). P (int x))"
- apply (subst all_nat)
- apply auto [1]
- apply (subst ex_nat)
- apply auto
-done
-
-declare TransferMorphism_int_nat[transfer add
- return: transfer_int_nat_quantifiers]
-
-
-(* if *)
-
-lemma int_if_cong: "(if P then (int x) else (int y)) =
- int (if P then x else y)"
- by auto
-
-declare TransferMorphism_int_nat [transfer add return: int_if_cong]
-
-
-
-(* operations with sets *)
-
-lemma transfer_int_nat_set_functions:
- "nat_set A \<Longrightarrow> card A = card (nat ` A)"
- "{} = int ` ({}::nat set)"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Int B = int ` (nat ` A Int nat ` B)"
- "{x. x >= 0 & P x} = int ` {x. P(int x)}"
- "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
- (* need all variants of these! *)
- by (simp_all only: is_nat_def transfer_nat_int_set_functions
- transfer_nat_int_set_function_closures
- transfer_nat_int_set_return_embed nat_0_le
- cong: transfer_nat_int_set_cong)
-
-lemma transfer_int_nat_set_function_closures:
- "nat_set {}"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
- "is_nat x \<Longrightarrow> nat_set {x..y}"
- "nat_set {x. x >= 0 & P x}"
- "nat_set (int ` C)"
- "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
- by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)
-
-lemma transfer_int_nat_set_relations:
- "nat_set A \<Longrightarrow> finite A = finite (nat ` A)"
- "is_nat x \<Longrightarrow> nat_set A \<Longrightarrow> (x : A) = (nat x : nat ` A)"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A = B) = (nat ` A = nat ` B)"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A < B) = (nat ` A < nat ` B)"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A <= B) = (nat ` A <= nat ` B)"
- by (simp_all only: is_nat_def transfer_nat_int_set_relations
- transfer_nat_int_set_return_embed nat_0_le)
-
-lemma transfer_int_nat_set_return_embed: "nat ` int ` A = A"
- by (simp only: transfer_nat_int_set_relations
- transfer_nat_int_set_function_closures
- transfer_nat_int_set_return_embed nat_0_le)
-
-lemma transfer_int_nat_set_cong: "(!!x. P x = P' x) \<Longrightarrow>
- {(x::nat). P x} = {x. P' x}"
- by auto
-
-declare TransferMorphism_int_nat[transfer add
- return: transfer_int_nat_set_functions
- transfer_int_nat_set_function_closures
- transfer_int_nat_set_relations
- transfer_int_nat_set_return_embed
- cong: transfer_int_nat_set_cong
-]
-
-
-(* setsum and setprod *)
-
-(* this handles the case where the *domain* of f is int *)
-lemma transfer_int_nat_sum_prod:
- "nat_set A \<Longrightarrow> setsum f A = setsum (%x. f (int x)) (nat ` A)"
- "nat_set A \<Longrightarrow> setprod f A = setprod (%x. f (int x)) (nat ` A)"
- apply (subst setsum_reindex)
- apply (unfold inj_on_def nat_set_def, auto simp add: eq_nat_nat_iff)
- apply (subst setprod_reindex)
- apply (unfold inj_on_def nat_set_def o_def, auto simp add: eq_nat_nat_iff
- cong: setprod_cong)
-done
-
-(* this handles the case where the *range* of f is int *)
-lemma transfer_int_nat_sum_prod2:
- "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> setsum f A = int(setsum (%x. nat (f x)) A)"
- "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
- setprod f A = int(setprod (%x. nat (f x)) A)"
- unfolding is_nat_def
- apply (subst int_setsum, auto)
- apply (subst int_setprod, auto simp add: cong: setprod_cong)
-done
-
-declare TransferMorphism_int_nat[transfer add
- return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
- cong: setsum_cong setprod_cong]
-
-
-subsection {* Test it out *}
-
-(* nat to int *)
-
-lemma ex1: "(x::nat) + y = y + x"
- by auto
-
-thm ex1 [transferred]
-
-lemma ex2: "(a::nat) div b * b + a mod b = a"
- by (rule mod_div_equality)
-
-thm ex2 [transferred]
-
-lemma ex3: "ALL (x::nat). ALL y. EX z. z >= x + y"
- by auto
-
-thm ex3 [transferred natint]
-
-lemma ex4: "(x::nat) >= y \<Longrightarrow> (x - y) + y = x"
- by auto
-
-thm ex4 [transferred]
-
-lemma ex5: "(2::nat) * (SUM i <= n. i) = n * (n + 1)"
- by (induct n rule: nat_induct, auto)
-
-thm ex5 [transferred]
-
-theorem ex6: "0 <= (n::int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
- by (rule ex5 [transferred])
-
-thm ex6 [transferred]
-
-thm ex5 [transferred, transferred]
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nat_Transfer.thy Thu Sep 17 14:17:37 2009 +1000
@@ -0,0 +1,484 @@
+
+(* Authors: Jeremy Avigad and Amine Chaieb *)
+
+header {* Sets up transfer from nats to ints and back. *}
+
+theory Nat_Transfer
+imports Main Parity
+begin
+
+subsection {* Set up transfer from nat to int *}
+
+(* set up transfer direction *)
+
+lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
+ by (simp add: TransferMorphism_def)
+
+declare TransferMorphism_nat_int[transfer
+ add mode: manual
+ return: nat_0_le
+ labels: natint
+]
+
+(* basic functions and relations *)
+
+lemma transfer_nat_int_numerals:
+ "(0::nat) = nat 0"
+ "(1::nat) = nat 1"
+ "(2::nat) = nat 2"
+ "(3::nat) = nat 3"
+ by auto
+
+definition
+ tsub :: "int \<Rightarrow> int \<Rightarrow> int"
+where
+ "tsub x y = (if x >= y then x - y else 0)"
+
+lemma tsub_eq: "x >= y \<Longrightarrow> tsub x y = x - y"
+ by (simp add: tsub_def)
+
+
+lemma transfer_nat_int_functions:
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)"
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
+ "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)"
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
+ by (auto simp add: eq_nat_nat_iff nat_mult_distrib
+ nat_power_eq nat_div_distrib nat_mod_distrib tsub_def)
+
+lemma transfer_nat_int_function_closures:
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
+ "(x::int) >= 0 \<Longrightarrow> x^n >= 0"
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
+ "(0::int) >= 0"
+ "(1::int) >= 0"
+ "(2::int) >= 0"
+ "(3::int) >= 0"
+ "int z >= 0"
+ apply (auto simp add: zero_le_mult_iff tsub_def)
+ apply (case_tac "y = 0")
+ apply auto
+ apply (subst pos_imp_zdiv_nonneg_iff, auto)
+ apply (case_tac "y = 0")
+ apply force
+ apply (rule pos_mod_sign)
+ apply arith
+done
+
+lemma transfer_nat_int_relations:
+ "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
+ (nat (x::int) = nat y) = (x = y)"
+ "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
+ (nat (x::int) < nat y) = (x < y)"
+ "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
+ (nat (x::int) <= nat y) = (x <= y)"
+ "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
+ (nat (x::int) dvd nat y) = (x dvd y)"
+ by (auto simp add: zdvd_int)
+
+declare TransferMorphism_nat_int[transfer add return:
+ transfer_nat_int_numerals
+ transfer_nat_int_functions
+ transfer_nat_int_function_closures
+ transfer_nat_int_relations
+]
+
+
+(* first-order quantifiers *)
+
+lemma transfer_nat_int_quantifiers:
+ "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
+ "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))"
+ by (rule all_nat, rule ex_nat)
+
+(* should we restrict these? *)
+lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
+ (ALL x. Q x \<longrightarrow> P x) = (ALL x. Q x \<longrightarrow> P' x)"
+ by auto
+
+lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
+ (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
+ by auto
+
+declare TransferMorphism_nat_int[transfer add
+ return: transfer_nat_int_quantifiers
+ cong: all_cong ex_cong]
+
+
+(* if *)
+
+lemma nat_if_cong: "(if P then (nat x) else (nat y)) =
+ nat (if P then x else y)"
+ by auto
+
+declare TransferMorphism_nat_int [transfer add return: nat_if_cong]
+
+
+(* operations with sets *)
+
+definition
+ nat_set :: "int set \<Rightarrow> bool"
+where
+ "nat_set S = (ALL x:S. x >= 0)"
+
+lemma transfer_nat_int_set_functions:
+ "card A = card (int ` A)"
+ "{} = nat ` ({}::int set)"
+ "A Un B = nat ` (int ` A Un int ` B)"
+ "A Int B = nat ` (int ` A Int int ` B)"
+ "{x. P x} = nat ` {x. x >= 0 & P(nat x)}"
+ "{..n} = nat ` {0..int n}"
+ "{m..n} = nat ` {int m..int n}" (* need all variants of these! *)
+ apply (rule card_image [symmetric])
+ apply (auto simp add: inj_on_def image_def)
+ apply (rule_tac x = "int x" in bexI)
+ apply auto
+ apply (rule_tac x = "int x" in bexI)
+ apply auto
+ apply (rule_tac x = "int x" in bexI)
+ apply auto
+ apply (rule_tac x = "int x" in exI)
+ apply auto
+ apply (rule_tac x = "int x" in bexI)
+ apply auto
+ apply (rule_tac x = "int x" in bexI)
+ apply auto
+done
+
+lemma transfer_nat_int_set_function_closures:
+ "nat_set {}"
+ "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
+ "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
+ "x >= 0 \<Longrightarrow> nat_set {x..y}"
+ "nat_set {x. x >= 0 & P x}"
+ "nat_set (int ` C)"
+ "nat_set A \<Longrightarrow> x : A \<Longrightarrow> x >= 0" (* does it hurt to turn this on? *)
+ unfolding nat_set_def apply auto
+done
+
+lemma transfer_nat_int_set_relations:
+ "(finite A) = (finite (int ` A))"
+ "(x : A) = (int x : int ` A)"
+ "(A = B) = (int ` A = int ` B)"
+ "(A < B) = (int ` A < int ` B)"
+ "(A <= B) = (int ` A <= int ` B)"
+
+ apply (rule iffI)
+ apply (erule finite_imageI)
+ apply (erule finite_imageD)
+ apply (auto simp add: image_def expand_set_eq inj_on_def)
+ apply (drule_tac x = "int x" in spec, auto)
+ apply (drule_tac x = "int x" in spec, auto)
+ apply (drule_tac x = "int x" in spec, auto)
+done
+
+lemma transfer_nat_int_set_return_embed: "nat_set A \<Longrightarrow>
+ (int ` nat ` A = A)"
+ by (auto simp add: nat_set_def image_def)
+
+lemma transfer_nat_int_set_cong: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>
+ {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
+ by auto
+
+declare TransferMorphism_nat_int[transfer add
+ return: transfer_nat_int_set_functions
+ transfer_nat_int_set_function_closures
+ transfer_nat_int_set_relations
+ transfer_nat_int_set_return_embed
+ cong: transfer_nat_int_set_cong
+]
+
+
+(* setsum and setprod *)
+
+(* this handles the case where the *domain* of f is nat *)
+lemma transfer_nat_int_sum_prod:
+ "setsum f A = setsum (%x. f (nat x)) (int ` A)"
+ "setprod f A = setprod (%x. f (nat x)) (int ` A)"
+ apply (subst setsum_reindex)
+ apply (unfold inj_on_def, auto)
+ apply (subst setprod_reindex)
+ apply (unfold inj_on_def o_def, auto)
+done
+
+(* this handles the case where the *range* of f is nat *)
+lemma transfer_nat_int_sum_prod2:
+ "setsum f A = nat(setsum (%x. int (f x)) A)"
+ "setprod f A = nat(setprod (%x. int (f x)) A)"
+ apply (subst int_setsum [symmetric])
+ apply auto
+ apply (subst int_setprod [symmetric])
+ apply auto
+done
+
+lemma transfer_nat_int_sum_prod_closure:
+ "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
+ "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
+ unfolding nat_set_def
+ apply (rule setsum_nonneg)
+ apply auto
+ apply (rule setprod_nonneg)
+ apply auto
+done
+
+(* this version doesn't work, even with nat_set A \<Longrightarrow>
+ x : A \<Longrightarrow> x >= 0 turned on. Why not?
+
+ also: what does =simp=> do?
+
+lemma transfer_nat_int_sum_prod_closure:
+ "(!!x. x : A ==> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
+ "(!!x. x : A ==> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
+ unfolding nat_set_def simp_implies_def
+ apply (rule setsum_nonneg)
+ apply auto
+ apply (rule setprod_nonneg)
+ apply auto
+done
+*)
+
+(* Making A = B in this lemma doesn't work. Why not?
+ Also, why aren't setsum_cong and setprod_cong enough,
+ with the previously mentioned rule turned on? *)
+
+lemma transfer_nat_int_sum_prod_cong:
+ "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
+ setsum f A = setsum g B"
+ "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
+ setprod f A = setprod g B"
+ unfolding nat_set_def
+ apply (subst setsum_cong, assumption)
+ apply auto [2]
+ apply (subst setprod_cong, assumption, auto)
+done
+
+declare TransferMorphism_nat_int[transfer add
+ return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2
+ transfer_nat_int_sum_prod_closure
+ cong: transfer_nat_int_sum_prod_cong]
+
+(* lists *)
+
+definition
+ embed_list :: "nat list \<Rightarrow> int list"
+where
+ "embed_list l = map int l";
+
+definition
+ nat_list :: "int list \<Rightarrow> bool"
+where
+ "nat_list l = nat_set (set l)";
+
+definition
+ return_list :: "int list \<Rightarrow> nat list"
+where
+ "return_list l = map nat l";
+
+thm nat_0_le;
+
+lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>
+ embed_list (return_list l) = l";
+ unfolding embed_list_def return_list_def nat_list_def nat_set_def
+ apply (induct l);
+ apply auto;
+done;
+
+lemma transfer_nat_int_list_functions:
+ "l @ m = return_list (embed_list l @ embed_list m)"
+ "[] = return_list []";
+ unfolding return_list_def embed_list_def;
+ apply auto;
+ apply (induct l, auto);
+ apply (induct m, auto);
+done;
+
+(*
+lemma transfer_nat_int_fold1: "fold f l x =
+ fold (%x. f (nat x)) (embed_list l) x";
+*)
+
+
+
+
+subsection {* Set up transfer from int to nat *}
+
+(* set up transfer direction *)
+
+lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
+ by (simp add: TransferMorphism_def)
+
+declare TransferMorphism_int_nat[transfer add
+ mode: manual
+(* labels: int-nat *)
+ return: nat_int
+]
+
+
+(* basic functions and relations *)
+
+definition
+ is_nat :: "int \<Rightarrow> bool"
+where
+ "is_nat x = (x >= 0)"
+
+lemma transfer_int_nat_numerals:
+ "0 = int 0"
+ "1 = int 1"
+ "2 = int 2"
+ "3 = int 3"
+ by auto
+
+lemma transfer_int_nat_functions:
+ "(int x) + (int y) = int (x + y)"
+ "(int x) * (int y) = int (x * y)"
+ "tsub (int x) (int y) = int (x - y)"
+ "(int x)^n = int (x^n)"
+ "(int x) div (int y) = int (x div y)"
+ "(int x) mod (int y) = int (x mod y)"
+ by (auto simp add: int_mult tsub_def int_power zdiv_int zmod_int)
+
+lemma transfer_int_nat_function_closures:
+ "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
+ "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)"
+ "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)"
+ "is_nat x \<Longrightarrow> is_nat (x^n)"
+ "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
+ "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
+ "is_nat 0"
+ "is_nat 1"
+ "is_nat 2"
+ "is_nat 3"
+ "is_nat (int z)"
+ by (simp_all only: is_nat_def transfer_nat_int_function_closures)
+
+lemma transfer_int_nat_relations:
+ "(int x = int y) = (x = y)"
+ "(int x < int y) = (x < y)"
+ "(int x <= int y) = (x <= y)"
+ "(int x dvd int y) = (x dvd y)"
+ "(even (int x)) = (even x)"
+ by (auto simp add: zdvd_int even_nat_def)
+
+lemma UNIV_apply:
+ "UNIV x = True"
+ by (simp add: top_fun_eq top_bool_eq)
+
+declare TransferMorphism_int_nat[transfer add return:
+ transfer_int_nat_numerals
+ transfer_int_nat_functions
+ transfer_int_nat_function_closures
+ transfer_int_nat_relations
+ UNIV_apply
+]
+
+
+(* first-order quantifiers *)
+
+lemma transfer_int_nat_quantifiers:
+ "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"
+ "(EX (x::int) >= 0. P x) = (EX (x::nat). P (int x))"
+ apply (subst all_nat)
+ apply auto [1]
+ apply (subst ex_nat)
+ apply auto
+done
+
+declare TransferMorphism_int_nat[transfer add
+ return: transfer_int_nat_quantifiers]
+
+
+(* if *)
+
+lemma int_if_cong: "(if P then (int x) else (int y)) =
+ int (if P then x else y)"
+ by auto
+
+declare TransferMorphism_int_nat [transfer add return: int_if_cong]
+
+
+
+(* operations with sets *)
+
+lemma transfer_int_nat_set_functions:
+ "nat_set A \<Longrightarrow> card A = card (nat ` A)"
+ "{} = int ` ({}::nat set)"
+ "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)"
+ "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Int B = int ` (nat ` A Int nat ` B)"
+ "{x. x >= 0 & P x} = int ` {x. P(int x)}"
+ "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
+ (* need all variants of these! *)
+ by (simp_all only: is_nat_def transfer_nat_int_set_functions
+ transfer_nat_int_set_function_closures
+ transfer_nat_int_set_return_embed nat_0_le
+ cong: transfer_nat_int_set_cong)
+
+lemma transfer_int_nat_set_function_closures:
+ "nat_set {}"
+ "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
+ "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
+ "is_nat x \<Longrightarrow> nat_set {x..y}"
+ "nat_set {x. x >= 0 & P x}"
+ "nat_set (int ` C)"
+ "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
+ by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)
+
+lemma transfer_int_nat_set_relations:
+ "nat_set A \<Longrightarrow> finite A = finite (nat ` A)"
+ "is_nat x \<Longrightarrow> nat_set A \<Longrightarrow> (x : A) = (nat x : nat ` A)"
+ "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A = B) = (nat ` A = nat ` B)"
+ "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A < B) = (nat ` A < nat ` B)"
+ "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A <= B) = (nat ` A <= nat ` B)"
+ by (simp_all only: is_nat_def transfer_nat_int_set_relations
+ transfer_nat_int_set_return_embed nat_0_le)
+
+lemma transfer_int_nat_set_return_embed: "nat ` int ` A = A"
+ by (simp only: transfer_nat_int_set_relations
+ transfer_nat_int_set_function_closures
+ transfer_nat_int_set_return_embed nat_0_le)
+
+lemma transfer_int_nat_set_cong: "(!!x. P x = P' x) \<Longrightarrow>
+ {(x::nat). P x} = {x. P' x}"
+ by auto
+
+declare TransferMorphism_int_nat[transfer add
+ return: transfer_int_nat_set_functions
+ transfer_int_nat_set_function_closures
+ transfer_int_nat_set_relations
+ transfer_int_nat_set_return_embed
+ cong: transfer_int_nat_set_cong
+]
+
+
+(* setsum and setprod *)
+
+(* this handles the case where the *domain* of f is int *)
+lemma transfer_int_nat_sum_prod:
+ "nat_set A \<Longrightarrow> setsum f A = setsum (%x. f (int x)) (nat ` A)"
+ "nat_set A \<Longrightarrow> setprod f A = setprod (%x. f (int x)) (nat ` A)"
+ apply (subst setsum_reindex)
+ apply (unfold inj_on_def nat_set_def, auto simp add: eq_nat_nat_iff)
+ apply (subst setprod_reindex)
+ apply (unfold inj_on_def nat_set_def o_def, auto simp add: eq_nat_nat_iff
+ cong: setprod_cong)
+done
+
+(* this handles the case where the *range* of f is int *)
+lemma transfer_int_nat_sum_prod2:
+ "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> setsum f A = int(setsum (%x. nat (f x)) A)"
+ "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
+ setprod f A = int(setprod (%x. nat (f x)) A)"
+ unfolding is_nat_def
+ apply (subst int_setsum, auto)
+ apply (subst int_setprod, auto simp add: cong: setprod_cong)
+done
+
+declare TransferMorphism_int_nat[transfer add
+ return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
+ cong: setsum_cong setprod_cong]
+
+end
--- a/src/HOL/Nominal/Examples/Class.thy Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Nominal/Examples/Class.thy Thu Sep 17 14:17:37 2009 +1000
@@ -11134,7 +11134,6 @@
shows "pi1\<bullet>(lfp f) = lfp (pi1\<bullet>f)"
and "pi2\<bullet>(lfp g) = lfp (pi2\<bullet>g)"
apply(simp add: lfp_def)
-apply(simp add: Inf_set_eq)
apply(simp add: big_inter_eqvt)
apply(simp add: pt_Collect_eqvt[OF pt_name_inst, OF at_name_inst])
apply(subgoal_tac "{u. (pi1\<bullet>f) u \<subseteq> u} = {u. ((rev pi1)\<bullet>((pi1\<bullet>f) u)) \<subseteq> ((rev pi1)\<bullet>u)}")
@@ -11146,7 +11145,6 @@
apply(drule subseteq_eqvt(1)[THEN iffD2])
apply(simp add: perm_bool)
apply(simp add: lfp_def)
-apply(simp add: Inf_set_eq)
apply(simp add: big_inter_eqvt)
apply(simp add: pt_Collect_eqvt[OF pt_coname_inst, OF at_coname_inst])
apply(subgoal_tac "{u. (pi2\<bullet>g) u \<subseteq> u} = {u. ((rev pi2)\<bullet>((pi2\<bullet>g) u)) \<subseteq> ((rev pi2)\<bullet>u)}")
--- a/src/HOL/Predicate.thy Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Predicate.thy Thu Sep 17 14:17:37 2009 +1000
@@ -366,7 +366,7 @@
definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<guillemotright>=" 70) where
"P \<guillemotright>= f = Pred (\<lambda>x. (\<exists>y. eval P y \<and> eval (f y) x))"
-instantiation pred :: (type) complete_lattice
+instantiation pred :: (type) "{complete_lattice, boolean_algebra}"
begin
definition
@@ -393,10 +393,16 @@
definition
[code del]: "\<Squnion>A = Pred (SUPR A eval)"
-instance by default
- (auto simp add: less_eq_pred_def less_pred_def
+definition
+ "- P = Pred (- eval P)"
+
+definition
+ "P - Q = Pred (eval P - eval Q)"
+
+instance proof
+qed (auto simp add: less_eq_pred_def less_pred_def
inf_pred_def sup_pred_def bot_pred_def top_pred_def
- Inf_pred_def Sup_pred_def,
+ Inf_pred_def Sup_pred_def uminus_pred_def minus_pred_def fun_Compl_def bool_Compl_def,
auto simp add: le_fun_def less_fun_def le_bool_def less_bool_def
eval_inject mem_def)
@@ -464,6 +470,127 @@
lemma supE: "eval (A \<squnion> B) x \<Longrightarrow> (eval A x \<Longrightarrow> P) \<Longrightarrow> (eval B x \<Longrightarrow> P) \<Longrightarrow> P"
unfolding sup_pred_def by auto
+lemma single_not_bot [simp]:
+ "single x \<noteq> \<bottom>"
+ by (auto simp add: single_def bot_pred_def expand_fun_eq)
+
+lemma not_bot:
+ assumes "A \<noteq> \<bottom>"
+ obtains x where "eval A x"
+using assms by (cases A)
+ (auto simp add: bot_pred_def, auto simp add: mem_def)
+
+
+subsubsection {* Emptiness check and definite choice *}
+
+definition is_empty :: "'a pred \<Rightarrow> bool" where
+ "is_empty A \<longleftrightarrow> A = \<bottom>"
+
+lemma is_empty_bot:
+ "is_empty \<bottom>"
+ by (simp add: is_empty_def)
+
+lemma not_is_empty_single:
+ "\<not> is_empty (single x)"
+ by (auto simp add: is_empty_def single_def bot_pred_def expand_fun_eq)
+
+lemma is_empty_sup:
+ "is_empty (A \<squnion> B) \<longleftrightarrow> is_empty A \<and> is_empty B"
+ by (auto simp add: is_empty_def intro: sup_eq_bot_eq1 sup_eq_bot_eq2)
+
+definition singleton :: "'a pred \<Rightarrow> 'a" where
+ "singleton A = (if \<exists>!x. eval A x then THE x. eval A x else undefined)"
+
+lemma singleton_eqI:
+ "\<exists>!x. eval A x \<Longrightarrow> eval A x \<Longrightarrow> singleton A = x"
+ by (auto simp add: singleton_def)
+
+lemma eval_singletonI:
+ "\<exists>!x. eval A x \<Longrightarrow> eval A (singleton A)"
+proof -
+ assume assm: "\<exists>!x. eval A x"
+ then obtain x where "eval A x" ..
+ moreover with assm have "singleton A = x" by (rule singleton_eqI)
+ ultimately show ?thesis by simp
+qed
+
+lemma single_singleton:
+ "\<exists>!x. eval A x \<Longrightarrow> single (singleton A) = A"
+proof -
+ assume assm: "\<exists>!x. eval A x"
+ then have "eval A (singleton A)"
+ by (rule eval_singletonI)
+ moreover from assm have "\<And>x. eval A x \<Longrightarrow> singleton A = x"
+ by (rule singleton_eqI)
+ ultimately have "eval (single (singleton A)) = eval A"
+ by (simp (no_asm_use) add: single_def expand_fun_eq) blast
+ then show ?thesis by (simp add: eval_inject)
+qed
+
+lemma singleton_undefinedI:
+ "\<not> (\<exists>!x. eval A x) \<Longrightarrow> singleton A = undefined"
+ by (simp add: singleton_def)
+
+lemma singleton_bot:
+ "singleton \<bottom> = undefined"
+ by (auto simp add: bot_pred_def intro: singleton_undefinedI)
+
+lemma singleton_single:
+ "singleton (single x) = x"
+ by (auto simp add: intro: singleton_eqI singleI elim: singleE)
+
+lemma singleton_sup_single_single:
+ "singleton (single x \<squnion> single y) = (if x = y then x else undefined)"
+proof (cases "x = y")
+ case True then show ?thesis by (simp add: singleton_single)
+next
+ case False
+ have "eval (single x \<squnion> single y) x"
+ and "eval (single x \<squnion> single y) y"
+ by (auto intro: supI1 supI2 singleI)
+ with False have "\<not> (\<exists>!z. eval (single x \<squnion> single y) z)"
+ by blast
+ then have "singleton (single x \<squnion> single y) = undefined"
+ by (rule singleton_undefinedI)
+ with False show ?thesis by simp
+qed
+
+lemma singleton_sup_aux:
+ "singleton (A \<squnion> B) = (if A = \<bottom> then singleton B
+ else if B = \<bottom> then singleton A
+ else singleton
+ (single (singleton A) \<squnion> single (singleton B)))"
+proof (cases "(\<exists>!x. eval A x) \<and> (\<exists>!y. eval B y)")
+ case True then show ?thesis by (simp add: single_singleton)
+next
+ case False
+ from False have A_or_B:
+ "singleton A = undefined \<or> singleton B = undefined"
+ by (auto intro!: singleton_undefinedI)
+ then have rhs: "singleton
+ (single (singleton A) \<squnion> single (singleton B)) = undefined"
+ by (auto simp add: singleton_sup_single_single singleton_single)
+ from False have not_unique:
+ "\<not> (\<exists>!x. eval A x) \<or> \<not> (\<exists>!y. eval B y)" by simp
+ show ?thesis proof (cases "A \<noteq> \<bottom> \<and> B \<noteq> \<bottom>")
+ case True
+ then obtain a b where a: "eval A a" and b: "eval B b"
+ by (blast elim: not_bot)
+ with True not_unique have "\<not> (\<exists>!x. eval (A \<squnion> B) x)"
+ by (auto simp add: sup_pred_def bot_pred_def)
+ then have "singleton (A \<squnion> B) = undefined" by (rule singleton_undefinedI)
+ with True rhs show ?thesis by simp
+ next
+ case False then show ?thesis by auto
+ qed
+qed
+
+lemma singleton_sup:
+ "singleton (A \<squnion> B) = (if A = \<bottom> then singleton B
+ else if B = \<bottom> then singleton A
+ else if singleton A = singleton B then singleton A else undefined)"
+using singleton_sup_aux [of A B] by (simp only: singleton_sup_single_single)
+
subsubsection {* Derived operations *}
@@ -630,6 +757,46 @@
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pred \<Rightarrow> 'b pred" where
"map f P = P \<guillemotright>= (single o f)"
+primrec null :: "'a seq \<Rightarrow> bool" where
+ "null Empty \<longleftrightarrow> True"
+ | "null (Insert x P) \<longleftrightarrow> False"
+ | "null (Join P xq) \<longleftrightarrow> is_empty P \<and> null xq"
+
+lemma null_is_empty:
+ "null xq \<longleftrightarrow> is_empty (pred_of_seq xq)"
+ by (induct xq) (simp_all add: is_empty_bot not_is_empty_single is_empty_sup)
+
+lemma is_empty_code [code]:
+ "is_empty (Seq f) \<longleftrightarrow> null (f ())"
+ by (simp add: null_is_empty Seq_def)
+
+primrec the_only :: "'a seq \<Rightarrow> 'a" where
+ [code del]: "the_only Empty = undefined"
+ | "the_only (Insert x P) = (if is_empty P then x else let y = singleton P in if x = y then x else undefined)"
+ | "the_only (Join P xq) = (if is_empty P then the_only xq else if null xq then singleton P
+ else let x = singleton P; y = the_only xq in
+ if x = y then x else undefined)"
+
+lemma the_only_singleton:
+ "the_only xq = singleton (pred_of_seq xq)"
+ by (induct xq)
+ (auto simp add: singleton_bot singleton_single is_empty_def
+ null_is_empty Let_def singleton_sup)
+
+lemma singleton_code [code]:
+ "singleton (Seq f) = (case f ()
+ of Empty \<Rightarrow> undefined
+ | Insert x P \<Rightarrow> if is_empty P then x
+ else let y = singleton P in
+ if x = y then x else undefined
+ | Join P xq \<Rightarrow> if is_empty P then the_only xq
+ else if null xq then singleton P
+ else let x = singleton P; y = the_only xq in
+ if x = y then x else undefined)"
+ by (cases "f ()")
+ (auto simp add: Seq_def the_only_singleton is_empty_def
+ null_is_empty singleton_bot singleton_single singleton_sup Let_def)
+
ML {*
signature PREDICATE =
sig
@@ -707,7 +874,7 @@
bind (infixl "\<guillemotright>=" 70)
hide (open) type pred seq
-hide (open) const Pred eval single bind if_pred not_pred
- Empty Insert Join Seq member pred_of_seq "apply" adjunct eq map
+hide (open) const Pred eval single bind is_empty singleton if_pred not_pred
+ Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map
end
--- a/src/HOL/Presburger.thy Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Presburger.thy Thu Sep 17 14:17:37 2009 +1000
@@ -382,15 +382,22 @@
lemma uminus_dvd_conv: "(d dvd (t::int)) \<equiv> (-d dvd t)" "(d dvd (t::int)) \<equiv> (d dvd -t)"
by simp_all
+
text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
-lemma all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
+
+lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
by (simp split add: split_nat)
-lemma ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
- apply (auto split add: split_nat)
- apply (rule_tac x="int x" in exI, simp)
- apply (rule_tac x = "nat x" in exI,erule_tac x = "nat x" in allE, simp)
- done
+lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
+proof
+ assume "\<exists>x. P x"
+ then obtain x where "P x" ..
+ then have "int x \<ge> 0 \<and> P (nat (int x))" by simp
+ then show "\<exists>x\<ge>0. P (nat x)" ..
+next
+ assume "\<exists>x\<ge>0. P (nat x)"
+ then show "\<exists>x. P x" by auto
+qed
lemma zdiff_int_split: "P (int (x - y)) =
((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Sep 17 14:17:37 2009 +1000
@@ -7,7 +7,7 @@
signature ATP_MINIMAL =
sig
val minimalize: AtpManager.prover -> string -> int -> Proof.state ->
- (string * thm list) list -> (string * thm list) list option * string
+ (string * thm list) list -> ((string * thm list) list * int) option * string
end
structure AtpMinimal: ATP_MINIMAL =
@@ -69,9 +69,14 @@
forall e in v. ~p(v \ e)
*)
fun minimal p s =
- case min p [] s of
- [x] => if p [] then [] else [x]
- | m => m
+ let val c = ref 0
+ fun pc xs = (c := !c + 1; p xs)
+ in
+ (case min pc [] s of
+ [x] => if pc [] then [] else [x]
+ | m => m,
+ !c)
+ end
end
@@ -150,13 +155,14 @@
filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
else
name_thms_pairs
- val min_thms = if null to_use then []
+ val (min_thms, n) = if null to_use then ([], 0)
else minimal (test_thms (SOME filtered)) to_use
val min_names = order_unique (map fst min_thms)
+ val _ = println ("Interations: " ^ string_of_int n)
val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems")
val _ = debug_fn (fn () => print_names min_thms)
in
- answer' (SOME min_thms) ("Try this command: " ^
+ answer' (SOME(min_thms,n)) ("Try this command: " ^
Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
end
| (Timeout, _) =>
@@ -167,7 +173,7 @@
| (Failure, _) =>
answer'' "Failure: No proof with the theorems supplied")
handle ResHolClause.TOO_TRIVIAL =>
- answer' (SOME []) ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
+ answer' (SOME ([],0)) ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
| ERROR msg =>
answer'' ("Error: " ^ msg)
end
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Thu Sep 17 14:17:37 2009 +1000
@@ -79,14 +79,14 @@
preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
(* write out problem file and call prover *)
- fun cmd_line probfile = "TIMEFORMAT='%3U'; ((time " ^ space_implode " "
- [File.shell_path cmd, args, File.platform_path probfile] ^ ") 2>&1)"
+ val perl_script = "perl -w $ISABELLE_ATP_MANAGER/lib/scripts/local_atp.pl"
+ fun cmd_line probfile = perl_script ^ " '" ^ space_implode " "
+ [File.shell_path cmd, args, File.platform_path probfile] ^ "'"
fun split_time s =
let
val split = String.tokens (fn c => str c = "\n")
val (proof, t) = s |> split |> split_last |> apfst cat_lines
- val num = Scan.many1 Symbol.is_ascii_digit >> (fst o read_int)
- val time = num --| Scan.$$ "." -- num >> (fn (a, b) => a * 1000 + b)
+ val time = Scan.many1 Symbol.is_ascii_digit >> (fst o read_int)
val as_time = the_default 0 o Scan.read Symbol.stopper time o explode
in (proof, as_time t) end
fun run_on probfile =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP_Manager/lib/scripts/local_atp.pl Thu Sep 17 14:17:37 2009 +1000
@@ -0,0 +1,15 @@
+use POSIX qw(setsid);
+
+$SIG{'INT'} = "DEFAULT";
+
+defined (my $pid = fork) or die "$!";
+if (not $pid) {
+ POSIX::setsid or die $!;
+ exec @ARGV;
+}
+else {
+ wait;
+ my ($user, $system, $cuser, $csystem) = times;
+ my $time = ($user + $cuser) * 1000;
+ print "$time\n";
+}
--- a/src/HOL/Tools/Function/fundef_core.ML Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Tools/Function/fundef_core.ML Thu Sep 17 14:17:37 2009 +1000
@@ -478,7 +478,7 @@
fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
let
val f_def =
- Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
+ Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
Abs ("y", ranT, G $ Bound 1 $ Bound 0))
|> Syntax.check_term lthy
@@ -767,7 +767,7 @@
val R' = Free ("R", fastype_of R)
val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
- val inrel_R = Const ("FunDef.in_rel", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
+ val inrel_R = Const (@{const_name FunDef.in_rel}, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name "Wellfounded.wfP"}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
--- a/src/HOL/Tools/res_reconstruct.ML Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/Tools/res_reconstruct.ML Thu Sep 17 14:17:37 2009 +1000
@@ -523,7 +523,7 @@
let
val last_axiom = Vector.length thm_names
fun is_axiom n = n <= last_axiom
- fun is_conj n = n >= #1 conj_count andalso n < #1 conj_count + #2 conj_count
+ fun is_conj n = n >= fst conj_count andalso n < fst conj_count + snd conj_count
fun getname i = Vector.sub(thm_names, i-1)
in
(sort_distinct string_ord (filter (fn x => x <> "??.unknown")
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/transfer.ML Thu Sep 17 14:17:37 2009 +1000
@@ -0,0 +1,241 @@
+(* Author: Amine Chaieb, University of Cambridge, 2009
+ Jeremy Avigad, Carnegie Mellon University
+*)
+
+signature TRANSFER =
+sig
+ type data
+ type entry
+ val get: Proof.context -> data
+ val del: attribute
+ val setup: theory -> theory
+end;
+
+structure Transfer : TRANSFER =
+struct
+
+val eq_thm = Thm.eq_thm;
+
+type entry = {inj : thm list, emb : thm list, ret : thm list, cong : thm list,
+ guess : bool, hints : string list};
+type data = simpset * (thm * entry) list;
+
+structure Data = GenericDataFun
+(
+ type T = data;
+ val empty = (HOL_ss, []);
+ val extend = I;
+ fun merge _ ((ss1, e1), (ss2, e2)) =
+ (merge_ss (ss1, ss2), AList.merge eq_thm (K true) (e1, e2));
+);
+
+val get = Data.get o Context.Proof;
+
+fun del_data key = apsnd (remove (eq_fst eq_thm) (key, []));
+
+val del = Thm.declaration_attribute (Data.map o del_data);
+val add_ss = Thm.declaration_attribute
+ (fn th => Data.map (fn (ss,data) => (ss addsimps [th], data)));
+
+val del_ss = Thm.declaration_attribute
+ (fn th => Data.map (fn (ss,data) => (ss delsimps [th], data)));
+
+val transM_pat = (Thm.dest_arg1 o Thm.dest_arg o cprop_of) @{thm TransferMorphism_def};
+
+fun merge_update eq m (k,v) [] = [(k,v)]
+ | merge_update eq m (k,v) ((k',v')::al) =
+ if eq (k,k') then (k',m (v,v')):: al else (k',v') :: merge_update eq m (k,v) al
+
+fun C f x y = f y x
+
+fun simpset_of_entry injonly {inj = inj, emb = emb, ret = ret, cong = cg, guess = g, hints = hints} =
+ HOL_ss addsimps inj addsimps (if injonly then [] else emb@ret) addcongs cg;
+
+fun basic_transfer_rule injonly a0 D0 e leave ctxt0 th =
+ let
+ val ([a,D], ctxt) = apfst (map Drule.dest_term o snd) (Variable.import true (map Drule.mk_term [a0, D0]) ctxt0)
+ val (aT,bT) =
+ let val T = typ_of (ctyp_of_term a)
+ in (Term.range_type T, Term.domain_type T)
+ end
+ val ctxt' = (Variable.declare_term (term_of a) o Variable.declare_term (term_of D) o Variable.declare_thm th) ctxt
+ val ns = filter (fn i => Type.could_unify (snd i, aT) andalso not (fst (fst i) mem_string leave)) (Term.add_vars (prop_of th) [])
+ val (ins, ctxt'') = Variable.variant_fixes (map (fst o fst) ns) ctxt'
+ val cns = map ((cterm_of o ProofContext.theory_of) ctxt'' o Var) ns
+ val cfis = map ((cterm_of o ProofContext.theory_of) ctxt'' o (fn n => Free (n, bT))) ins
+ val cis = map (Thm.capply a) cfis
+ val (hs,ctxt''') = Assumption.add_assumes (map (fn ct => Thm.capply @{cterm "Trueprop"} (Thm.capply D ct)) cfis) ctxt''
+ val th1 = Drule.cterm_instantiate (cns~~ cis) th
+ val th2 = fold (C implies_elim) hs (fold_rev implies_intr (map cprop_of hs) th1)
+ val th3 = Simplifier.asm_full_simplify (Simplifier.context ctxt''' (simpset_of_entry injonly e))
+ (fold_rev implies_intr (map cprop_of hs) th2)
+in hd (Variable.export ctxt''' ctxt0 [th3]) end;
+
+local
+fun transfer_ruleh a D leave ctxt th =
+ let val (ss,al) = get ctxt
+ val a0 = cterm_of (ProofContext.theory_of ctxt) a
+ val D0 = cterm_of (ProofContext.theory_of ctxt) D
+ fun h (th', e) = let val (a',D') = (Thm.dest_binop o Thm.dest_arg o cprop_of) th'
+ in if a0 aconvc a' andalso D0 aconvc D' then SOME e else NONE
+ end
+ in case get_first h al of
+ SOME e => basic_transfer_rule false a0 D0 e leave ctxt th
+ | NONE => error "Transfer: corresponding instance not found in context-data"
+ end
+in fun transfer_rule (a,D) leave (gctxt,th) =
+ (gctxt, transfer_ruleh a D leave (Context.proof_of gctxt) th)
+end;
+
+fun splits P [] = []
+ | splits P (xxs as (x::xs)) =
+ let val pss = filter (P x) xxs
+ val qss = filter_out (P x) xxs
+ in if null pss then [qss] else if null qss then [pss] else pss:: splits P qss
+ end
+
+fun all_transfers leave (gctxt,th) =
+ let
+ val ctxt = Context.proof_of gctxt
+ val tys = map snd (Term.add_vars (prop_of th) [])
+ val _ = if null tys then error "transfer: Unable to guess instance" else ()
+ val tyss = splits (curry Type.could_unify) tys
+ val get_ty = typ_of o ctyp_of_term o fst o Thm.dest_binop o Thm.dest_arg o cprop_of
+ val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
+ val insts =
+ map_filter (fn tys =>
+ get_first (fn (k,ss) => if Type.could_unify (hd tys, range_type (get_ty k))
+ then SOME (get_aD k, ss)
+ else NONE) (snd (get ctxt))) tyss
+ val _ = if null insts then error "Transfer guesser: there were no possible instances, use direction: in order to provide a direction" else ()
+ val ths = map (fn ((a,D),e) => basic_transfer_rule false a D e leave ctxt th) insts
+ val cth = Conjunction.intr_balanced ths
+ in (gctxt, cth)
+ end;
+
+fun transfer_rule_by_hint ls leave (gctxt,th) =
+ let
+ val ctxt = Context.proof_of gctxt
+ val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
+ val insts =
+ map_filter (fn (k,e) => if exists (fn l => l mem_string (#hints e)) ls
+ then SOME (get_aD k, e) else NONE)
+ (snd (get ctxt))
+ val _ = if null insts then error "Transfer: No labels provided are stored in the context" else ()
+ val ths = map (fn ((a,D),e) => basic_transfer_rule false a D e leave ctxt th) insts
+ val cth = Conjunction.intr_balanced ths
+ in (gctxt, cth)
+ end;
+
+
+fun transferred_attribute ls NONE leave =
+ if null ls then all_transfers leave else transfer_rule_by_hint ls leave
+ | transferred_attribute _ (SOME (a,D)) leave = transfer_rule (a,D) leave
+
+ (* Add data to the context *)
+fun gen_merge_entries {inj = inj0, emb = emb0, ret = ret0, cong = cg0, guess = g0, hints = hints0}
+ ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1},
+ {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2})
+ =
+ let fun h xs0 xs ys = subtract Thm.eq_thm xs0 (merge Thm.eq_thm (xs,ys)) in
+ {inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2,
+ ret = h ret0 ret1 ret2, cong = h cg0 cg1 cg2, guess = g1 andalso g2,
+ hints = subtract (op = : string*string -> bool) hints0
+ (hints1 union_string hints2)}
+ end;
+
+local
+ val h = curry (merge Thm.eq_thm)
+in
+fun merge_entries ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1},
+ {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2}) =
+ {inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = hints1 union_string hints2}
+end;
+
+fun add ((inja,injd), (emba,embd), (reta,retd), (cga,cgd), g, (hintsa, hintsd)) =
+ Thm.declaration_attribute (fn key => fn context => context |> Data.map
+ (fn (ss, al) =>
+ let
+ val _ = ((let val _ = Thm.match (transM_pat, (Thm.dest_arg o cprop_of) key)
+ in 0 end)
+ handle MATCH => error "Attribute expected Theorem of the form : TransferMorphism A a B b")
+ val e0 = {inj = inja, emb = emba, ret = reta, cong = cga, guess = g, hints = hintsa}
+ val ed = {inj = injd, emb = embd, ret = retd, cong = cgd, guess = g, hints = hintsd}
+ val entry =
+ if g then
+ let val (a0,D0) = (Thm.dest_binop o Thm.dest_arg o cprop_of) key
+ val ctxt0 = ProofContext.init (Thm.theory_of_thm key)
+ val inj' = if null inja then #inj (case AList.lookup eq_thm al key of SOME e => e | NONE => error "Transfer: can not generate return rules on the fly, either add injectivity axiom or force manual mode with mode: manual")
+ else inja
+ val ret' = merge Thm.eq_thm (reta, map (fn th => basic_transfer_rule true a0 D0 {inj = inj', emb = [], ret = [], cong = cga, guess = g, hints = hintsa} [] ctxt0 th RS sym) emba)
+ in {inj = inja, emb = emba, ret = ret', cong = cga, guess = g, hints = hintsa} end
+ else e0
+ in (ss, merge_update eq_thm (gen_merge_entries ed) (key, entry) al)
+ end));
+
+
+
+(* concrete syntax *)
+
+local
+
+fun keyword k = Scan.lift (Args.$$$ k) >> K ()
+fun keywordC k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
+
+val congN = "cong"
+val injN = "inj"
+val embedN = "embed"
+val returnN = "return"
+val addN = "add"
+val delN = "del"
+val modeN = "mode"
+val automaticN = "automatic"
+val manualN = "manual"
+val directionN = "direction"
+val labelsN = "labels"
+val leavingN = "leaving"
+
+val any_keyword = keywordC congN || keywordC injN || keywordC embedN || keywordC returnN || keywordC directionN || keywordC modeN || keywordC delN || keywordC labelsN || keywordC leavingN
+
+val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat
+val terms = thms >> map Drule.dest_term
+val types = thms >> (Logic.dest_type o HOLogic.dest_Trueprop o prop_of o hd)
+val name = Scan.lift Args.name
+val names = Scan.repeat (Scan.unless any_keyword name)
+fun optional scan = Scan.optional scan []
+fun optional2 scan = Scan.optional scan ([],[])
+
+val mode = keywordC modeN |-- ((Scan.lift (Args.$$$ manualN) >> K false) || (Scan.lift (Args.$$$ automaticN) >> K true))
+val inj = (keywordC injN |-- thms) -- optional (keywordC delN |-- thms)
+val embed = (keywordC embedN |-- thms) -- optional (keywordC delN |-- thms)
+val return = (keywordC returnN |-- thms) -- optional (keywordC delN |-- thms)
+val cong = (keywordC congN |-- thms) -- optional (keywordC delN |-- thms)
+val addscan = Scan.unless any_keyword (keyword addN)
+val labels = (keywordC labelsN |-- names) -- optional (keywordC delN |-- names)
+val entry = Scan.optional mode true -- optional2 inj -- optional2 embed -- optional2 return -- optional2 cong -- optional2 labels
+
+val transf_add = addscan |-- entry
+in
+
+val install_att_syntax =
+ (Scan.lift (Args.$$$ delN >> K del) ||
+ transf_add
+ >> (fn (((((g, inj), embed), ret), cg), hints) => add (inj, embed, ret, cg, g, hints)))
+
+val transferred_att_syntax = (optional names -- Scan.option (keywordC directionN |-- (Args.term -- Args.term))
+ -- optional (keywordC leavingN |-- names) >> (fn ((hints, aD),leave) => transferred_attribute hints aD leave));
+
+end;
+
+
+(* theory setup *)
+
+val setup =
+ Attrib.setup @{binding transfer} install_att_syntax
+ "Installs transfer data" #>
+ Attrib.setup @{binding transfer_simps} (Attrib.add_del add_ss del_ss)
+ "simp rules for transfer" #>
+ Attrib.setup @{binding transferred} transferred_att_syntax
+ "Transfers theorems";
+
+end;
--- a/src/HOL/Tools/transfer_data.ML Fri Sep 11 20:58:29 2009 +1000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,243 +0,0 @@
-(* Title: Tools/transfer.ML
- Author: Amine Chaieb, University of Cambridge, 2009
- Jeremy Avigad, Carnegie Mellon University
-*)
-
-signature TRANSFER_DATA =
-sig
- type data
- type entry
- val get: Proof.context -> data
- val del: attribute
- val add: attribute
- val setup: theory -> theory
-end;
-
-structure TransferData (* : TRANSFER_DATA*) =
-struct
-type entry = {inj : thm list , emb : thm list , ret : thm list , cong : thm list, guess : bool, hints : string list};
-type data = simpset * (thm * entry) list;
-
-val eq_key = Thm.eq_thm;
-fun eq_data arg = eq_fst eq_key arg;
-
-structure Data = GenericDataFun
-(
- type T = data;
- val empty = (HOL_ss, []);
- val extend = I;
- fun merge _ ((ss, e), (ss', e')) =
- (merge_ss (ss, ss'), AList.merge eq_key (K true) (e, e'));
-);
-
-val get = Data.get o Context.Proof;
-
-fun del_data key = apsnd (remove eq_data (key, []));
-
-val del = Thm.declaration_attribute (Data.map o del_data);
-val add_ss = Thm.declaration_attribute
- (fn th => Data.map (fn (ss,data) => (ss addsimps [th], data)));
-
-val del_ss = Thm.declaration_attribute
- (fn th => Data.map (fn (ss,data) => (ss delsimps [th], data)));
-
-val transM_pat = (Thm.dest_arg1 o Thm.dest_arg o cprop_of) @{thm TransferMorphism_def};
-
-fun merge_update eq m (k,v) [] = [(k,v)]
- | merge_update eq m (k,v) ((k',v')::al) =
- if eq (k,k') then (k',m (v,v')):: al else (k',v') :: merge_update eq m (k,v) al
-
-fun C f x y = f y x
-
-fun simpset_of_entry injonly {inj = inj, emb = emb, ret = ret, cong = cg, guess = g, hints = hints} =
- HOL_ss addsimps inj addsimps (if injonly then [] else emb@ret) addcongs cg;
-
-fun basic_transfer_rule injonly a0 D0 e leave ctxt0 th =
- let
- val ([a,D], ctxt) = apfst (map Drule.dest_term o snd) (Variable.import true (map Drule.mk_term [a0, D0]) ctxt0)
- val (aT,bT) =
- let val T = typ_of (ctyp_of_term a)
- in (Term.range_type T, Term.domain_type T)
- end
- val ctxt' = (Variable.declare_term (term_of a) o Variable.declare_term (term_of D) o Variable.declare_thm th) ctxt
- val ns = filter (fn i => Type.could_unify (snd i, aT) andalso not (fst (fst i) mem_string leave)) (Term.add_vars (prop_of th) [])
- val (ins, ctxt'') = Variable.variant_fixes (map (fst o fst) ns) ctxt'
- val cns = map ((cterm_of o ProofContext.theory_of) ctxt'' o Var) ns
- val cfis = map ((cterm_of o ProofContext.theory_of) ctxt'' o (fn n => Free (n, bT))) ins
- val cis = map (Thm.capply a) cfis
- val (hs,ctxt''') = Assumption.add_assumes (map (fn ct => Thm.capply @{cterm "Trueprop"} (Thm.capply D ct)) cfis) ctxt''
- val th1 = Drule.cterm_instantiate (cns~~ cis) th
- val th2 = fold (C implies_elim) hs (fold_rev implies_intr (map cprop_of hs) th1)
- val th3 = Simplifier.asm_full_simplify (Simplifier.context ctxt''' (simpset_of_entry injonly e))
- (fold_rev implies_intr (map cprop_of hs) th2)
-in hd (Variable.export ctxt''' ctxt0 [th3]) end;
-
-local
-fun transfer_ruleh a D leave ctxt th =
- let val (ss,al) = get ctxt
- val a0 = cterm_of (ProofContext.theory_of ctxt) a
- val D0 = cterm_of (ProofContext.theory_of ctxt) D
- fun h (th', e) = let val (a',D') = (Thm.dest_binop o Thm.dest_arg o cprop_of) th'
- in if a0 aconvc a' andalso D0 aconvc D' then SOME e else NONE
- end
- in case get_first h al of
- SOME e => basic_transfer_rule false a0 D0 e leave ctxt th
- | NONE => error "Transfer: corresponding instance not found in context-data"
- end
-in fun transfer_rule (a,D) leave (gctxt,th) =
- (gctxt, transfer_ruleh a D leave (Context.proof_of gctxt) th)
-end;
-
-fun splits P [] = []
- | splits P (xxs as (x::xs)) =
- let val pss = filter (P x) xxs
- val qss = filter_out (P x) xxs
- in if null pss then [qss] else if null qss then [pss] else pss:: splits P qss
- end
-
-fun all_transfers leave (gctxt,th) =
- let
- val ctxt = Context.proof_of gctxt
- val tys = map snd (Term.add_vars (prop_of th) [])
- val _ = if null tys then error "transfer: Unable to guess instance" else ()
- val tyss = splits (curry Type.could_unify) tys
- val get_ty = typ_of o ctyp_of_term o fst o Thm.dest_binop o Thm.dest_arg o cprop_of
- val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
- val insts =
- map_filter (fn tys =>
- get_first (fn (k,ss) => if Type.could_unify (hd tys, range_type (get_ty k))
- then SOME (get_aD k, ss)
- else NONE) (snd (get ctxt))) tyss
- val _ = if null insts then error "Transfer guesser: there were no possible instances, use direction: in order to provide a direction" else ()
- val ths = map (fn ((a,D),e) => basic_transfer_rule false a D e leave ctxt th) insts
- val cth = Conjunction.intr_balanced ths
- in (gctxt, cth)
- end;
-
-fun transfer_rule_by_hint ls leave (gctxt,th) =
- let
- val ctxt = Context.proof_of gctxt
- val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
- val insts =
- map_filter (fn (k,e) => if exists (fn l => l mem_string (#hints e)) ls
- then SOME (get_aD k, e) else NONE)
- (snd (get ctxt))
- val _ = if null insts then error "Transfer: No labels provided are stored in the context" else ()
- val ths = map (fn ((a,D),e) => basic_transfer_rule false a D e leave ctxt th) insts
- val cth = Conjunction.intr_balanced ths
- in (gctxt, cth)
- end;
-
-
-fun transferred_attribute ls NONE leave =
- if null ls then all_transfers leave else transfer_rule_by_hint ls leave
- | transferred_attribute _ (SOME (a,D)) leave = transfer_rule (a,D) leave
-
- (* Add data to the context *)
-fun gen_merge_entries {inj = inj0, emb = emb0, ret = ret0, cong = cg0, guess = g0, hints = hints0}
- ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1},
- {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2})
- =
- let fun h xs0 xs ys = subtract Thm.eq_thm xs0 (merge Thm.eq_thm (xs,ys)) in
- {inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2,
- ret = h ret0 ret1 ret2, cong = h cg0 cg1 cg2, guess = g1 andalso g2,
- hints = subtract (op = : string*string -> bool) hints0
- (hints1 union_string hints2)}
- end;
-
-local
- val h = curry (merge Thm.eq_thm)
-in
-fun merge_entries ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1},
- {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2}) =
- {inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = hints1 union_string hints2}
-end;
-
-fun add ((inja,injd), (emba,embd), (reta,retd), (cga,cgd), g, (hintsa, hintsd)) =
- Thm.declaration_attribute (fn key => fn context => context |> Data.map
- (fn (ss, al) =>
- let
- val _ = ((let val _ = Thm.match (transM_pat, (Thm.dest_arg o cprop_of) key)
- in 0 end)
- handle MATCH => error "Attribute expected Theorem of the form : TransferMorphism A a B b")
- val e0 = {inj = inja, emb = emba, ret = reta, cong = cga, guess = g, hints = hintsa}
- val ed = {inj = injd, emb = embd, ret = retd, cong = cgd, guess = g, hints = hintsd}
- val entry =
- if g then
- let val (a0,D0) = (Thm.dest_binop o Thm.dest_arg o cprop_of) key
- val ctxt0 = ProofContext.init (Thm.theory_of_thm key)
- val inj' = if null inja then #inj (case AList.lookup eq_key al key of SOME e => e | NONE => error "Transfer: can not generate return rules on the fly, either add injectivity axiom or force manual mode with mode: manual")
- else inja
- val ret' = merge Thm.eq_thm (reta, map (fn th => basic_transfer_rule true a0 D0 {inj = inj', emb = [], ret = [], cong = cga, guess = g, hints = hintsa} [] ctxt0 th RS sym) emba)
- in {inj = inja, emb = emba, ret = ret', cong = cga, guess = g, hints = hintsa} end
- else e0
- in (ss, merge_update eq_key (gen_merge_entries ed) (key, entry) al)
- end));
-
-
-
-(* concrete syntax *)
-
-local
-
-fun keyword k = Scan.lift (Args.$$$ k) >> K ()
-fun keywordC k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
-
-val congN = "cong"
-val injN = "inj"
-val embedN = "embed"
-val returnN = "return"
-val addN = "add"
-val delN = "del"
-val modeN = "mode"
-val automaticN = "automatic"
-val manualN = "manual"
-val directionN = "direction"
-val labelsN = "labels"
-val leavingN = "leaving"
-
-val any_keyword = keywordC congN || keywordC injN || keywordC embedN || keywordC returnN || keywordC directionN || keywordC modeN || keywordC delN || keywordC labelsN || keywordC leavingN
-
-val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat
-val terms = thms >> map Drule.dest_term
-val types = thms >> (Logic.dest_type o HOLogic.dest_Trueprop o prop_of o hd)
-val name = Scan.lift Args.name
-val names = Scan.repeat (Scan.unless any_keyword name)
-fun optional scan = Scan.optional scan []
-fun optional2 scan = Scan.optional scan ([],[])
-
-val mode = keywordC modeN |-- ((Scan.lift (Args.$$$ manualN) >> K false) || (Scan.lift (Args.$$$ automaticN) >> K true))
-val inj = (keywordC injN |-- thms) -- optional (keywordC delN |-- thms)
-val embed = (keywordC embedN |-- thms) -- optional (keywordC delN |-- thms)
-val return = (keywordC returnN |-- thms) -- optional (keywordC delN |-- thms)
-val cong = (keywordC congN |-- thms) -- optional (keywordC delN |-- thms)
-val addscan = Scan.unless any_keyword (keyword addN)
-val labels = (keywordC labelsN |-- names) -- optional (keywordC delN |-- names)
-val entry = Scan.optional mode true -- optional2 inj -- optional2 embed -- optional2 return -- optional2 cong -- optional2 labels
-
-val transf_add = addscan |-- entry
-in
-
-val install_att_syntax =
- (Scan.lift (Args.$$$ delN >> K del) ||
- transf_add
- >> (fn (((((g, inj), embed), ret), cg), hints) => add (inj, embed, ret, cg, g, hints)))
-
-val transferred_att_syntax = (optional names -- Scan.option (keywordC directionN |-- (Args.term -- Args.term))
- -- optional (keywordC leavingN |-- names) >> (fn ((hints, aD),leave) => transferred_attribute hints aD leave));
-
-end;
-
-
-(* theory setup *)
-
-
-val setup =
- Attrib.setup @{binding transfer} install_att_syntax
- "Installs transfer data" #>
- Attrib.setup @{binding transfer_simps} (Attrib.add_del add_ss del_ss)
- "simp rules for transfer" #>
- Attrib.setup @{binding transferred} transferred_att_syntax
- "Transfers theorems";
-
-end;
--- a/src/HOL/UNITY/Transformers.thy Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/UNITY/Transformers.thy Thu Sep 17 14:17:37 2009 +1000
@@ -88,7 +88,7 @@
done
lemma wens_Id [simp]: "wens F Id B = B"
-by (simp add: wens_def gfp_def wp_def awp_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def awp_def, blast)
text{*These two theorems justify the claim that @{term wens} returns the
weakest assertion satisfying the ensures property*}
@@ -101,7 +101,7 @@
lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B"
by (simp add: wens_def gfp_def constrains_def awp_def wp_def
- ensures_def transient_def Sup_set_eq, blast)
+ ensures_def transient_def, blast)
text{*These two results constitute assertion (4.13) of the thesis*}
lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
@@ -110,7 +110,7 @@
done
lemma wens_weakening: "B \<subseteq> wens F act B"
-by (simp add: wens_def gfp_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def, blast)
text{*Assertion (6), or 4.16 in the thesis*}
lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B"
@@ -120,7 +120,7 @@
text{*Assertion 4.17 in the thesis*}
lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
-by (simp add: wens_def gfp_def wp_def awp_def constrains_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast)
--{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
is declared as an iff-rule, then it's almost impossible to prove.
One proof is via @{text meson} after expanding all definitions, but it's
@@ -331,7 +331,7 @@
lemma wens_single_eq:
"wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B"
-by (simp add: wens_def gfp_def wp_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def, blast)
text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
--- a/src/HOL/ex/CTL.thy Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/ex/CTL.thy Thu Sep 17 14:17:37 2009 +1000
@@ -95,7 +95,7 @@
proof
assume "x \<in> gfp (\<lambda>s. - f (- s))"
then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)"
- by (auto simp add: gfp_def Sup_set_eq)
+ by (auto simp add: gfp_def)
then have "f (- u) \<subseteq> - u" by auto
then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
from l and this have "x \<notin> u" by auto
--- a/src/HOL/ex/Predicate_Compile_ex.thy Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Thu Sep 17 14:17:37 2009 +1000
@@ -157,4 +157,13 @@
values 3 "{(a,q). step (par nil nil) a q}"
*)
+
+inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
+ "k < l \<Longrightarrow> divmod_rel k l 0 k"
+ | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
+
+code_pred divmod_rel ..
+
+value [code] "Predicate.singleton (divmod_rel_1_2 1705 42)"
+
end
\ No newline at end of file
--- a/src/HOL/ex/ROOT.ML Fri Sep 11 20:58:29 2009 +1000
+++ b/src/HOL/ex/ROOT.ML Thu Sep 17 14:17:37 2009 +1000
@@ -60,6 +60,7 @@
"BinEx",
"Sqrt",
"Sqrt_Script",
+ "Transfer_Ex",
"Arithmetic_Series_Complex",
"HarmonicSeries",
"Refute_Examples",
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Transfer_Ex.thy Thu Sep 17 14:17:37 2009 +1000
@@ -0,0 +1,42 @@
+
+header {* Various examples for transfer procedure *}
+
+theory Transfer_Ex
+imports Complex_Main
+begin
+
+(* nat to int *)
+
+lemma ex1: "(x::nat) + y = y + x"
+ by auto
+
+thm ex1 [transferred]
+
+lemma ex2: "(a::nat) div b * b + a mod b = a"
+ by (rule mod_div_equality)
+
+thm ex2 [transferred]
+
+lemma ex3: "ALL (x::nat). ALL y. EX z. z >= x + y"
+ by auto
+
+thm ex3 [transferred natint]
+
+lemma ex4: "(x::nat) >= y \<Longrightarrow> (x - y) + y = x"
+ by auto
+
+thm ex4 [transferred]
+
+lemma ex5: "(2::nat) * (SUM i <= n. i) = n * (n + 1)"
+ by (induct n rule: nat_induct, auto)
+
+thm ex5 [transferred]
+
+theorem ex6: "0 <= (n::int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
+ by (rule ex5 [transferred])
+
+thm ex6 [transferred]
+
+thm ex5 [transferred, transferred]
+
+end
\ No newline at end of file
--- a/src/Pure/Concurrent/future.ML Fri Sep 11 20:58:29 2009 +1000
+++ b/src/Pure/Concurrent/future.ML Thu Sep 17 14:17:37 2009 +1000
@@ -84,7 +84,7 @@
fun group_of (Future {group, ...}) = group;
fun result_of (Future {result, ...}) = result;
-fun peek x = Synchronized.peek (result_of x);
+fun peek x = Synchronized.value (result_of x);
fun is_finished x = is_some (peek x);
fun value x = Future
--- a/src/Pure/Concurrent/synchronized.ML Fri Sep 11 20:58:29 2009 +1000
+++ b/src/Pure/Concurrent/synchronized.ML Thu Sep 17 14:17:37 2009 +1000
@@ -8,7 +8,6 @@
sig
type 'a var
val var: string -> 'a -> 'a var
- val peek: 'a var -> 'a
val value: 'a var -> 'a
val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option
val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
@@ -33,9 +32,7 @@
cond = ConditionVar.conditionVar (),
var = ref x};
-fun peek (Var {var, ...}) = ! var; (*unsynchronized!*)
-
-fun value (Var {name, lock, cond, var}) = SimpleThread.synchronized name lock (fn () => ! var);
+fun value (Var {var, ...}) = ! var;
(* synchronized access *)
--- a/src/Pure/General/binding.ML Fri Sep 11 20:58:29 2009 +1000
+++ b/src/Pure/General/binding.ML Thu Sep 17 14:17:37 2009 +1000
@@ -30,18 +30,19 @@
val str_of: binding -> string
end;
-structure Binding:> BINDING =
+structure Binding: BINDING =
struct
(** representation **)
(* datatype *)
-datatype binding = Binding of
+abstype binding = Binding of
{prefix: (string * bool) list, (*system prefix*)
qualifier: (string * bool) list, (*user qualifier*)
name: bstring, (*base name*)
- pos: Position.T}; (*source position*)
+ pos: Position.T} (*source position*)
+with
fun make_binding (prefix, qualifier, name, pos) =
Binding {prefix = prefix, qualifier = qualifier, name = name, pos = pos};
@@ -109,6 +110,7 @@
in Markup.markup (Markup.properties props (Markup.binding (name_of binding))) text end;
end;
+end;
type binding = Binding.binding;
--- a/src/Pure/General/linear_set.scala Fri Sep 11 20:58:29 2009 +1000
+++ b/src/Pure/General/linear_set.scala Thu Sep 17 14:17:37 2009 +1000
@@ -1,22 +1,22 @@
/* Title: Pure/General/linear_set.scala
Author: Makarius
- Author: Fabian Immler TU Munich
+ Author: Fabian Immler, TU Munich
Sets with canonical linear order, or immutable linked-lists.
*/
+
package isabelle
object Linear_Set
{
private case class Rep[A](
- val first_elem: Option[A], val last_elem: Option[A], val body: Map[A, A])
-
- private def empty_rep[A] = Rep[A](None, None, Map())
+ val first: Option[A], val last: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
- private def make[A](first_elem: Option[A], last_elem: Option[A], body: Map[A, A]): Linear_Set[A] =
- new Linear_Set[A] { override val rep = Rep(first_elem, last_elem, body) }
+ private def empty_rep[A] = Rep[A](None, None, Map(), Map())
+ private def make[A](first: Option[A], last: Option[A], nexts: Map[A, A], prevs: Map[A, A])
+ : Linear_Set[A] = new Linear_Set[A] { override val rep = Rep(first, last, nexts, prevs) }
def empty[A]: Linear_Set[A] = new Linear_Set
def apply[A](elems: A*): Linear_Set[A] = empty[A] ++ elems
@@ -35,48 +35,74 @@
/* auxiliary operations */
- def next(elem: A) = rep.body.get(elem)
- def prev(elem: A) = rep.body.find(_._2 == elem).map(_._1) // slow
+ def next(elem: A): Option[A] = rep.nexts.get(elem)
+ def prev(elem: A): Option[A] = rep.prevs.get(elem)
- private def _insert_after(hook: Option[A], elem: A): Linear_Set[A] =
+ def insert_after(hook: Option[A], elem: A): Linear_Set[A] =
if (contains(elem)) throw new Linear_Set.Duplicate(elem.toString)
- else hook match {
- case Some(hook) =>
- if (!contains(hook)) throw new Linear_Set.Undefined(hook.toString)
- else if (rep.body.isDefinedAt(hook))
- Linear_Set.make(rep.first_elem, rep.last_elem,
- rep.body - hook + (hook -> elem) + (elem -> rep.body(hook)))
- else Linear_Set.make(rep.first_elem, Some(elem), rep.body + (hook -> elem))
+ else
+ hook match {
+ case None =>
+ rep.first match {
+ case None => Linear_Set.make(Some(elem), Some(elem), Map(), Map())
+ case Some(elem1) =>
+ Linear_Set.make(Some(elem), rep.last,
+ rep.nexts + (elem -> elem1), rep.prevs + (elem1 -> elem))
+ }
+ case Some(elem1) =>
+ if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString)
+ else
+ rep.nexts.get(elem1) match {
+ case None =>
+ Linear_Set.make(rep.first, Some(elem),
+ rep.nexts + (elem1 -> elem), rep.prevs + (elem -> elem1))
+ case Some(elem2) =>
+ Linear_Set.make(rep.first, rep.last,
+ rep.nexts + (elem1 -> elem) + (elem -> elem2),
+ rep.prevs + (elem2 -> elem) + (elem -> elem1))
+ }
+ }
+
+ def delete_after(hook: Option[A]): Linear_Set[A] =
+ hook match {
case None =>
- if (isEmpty) Linear_Set.make(Some(elem), Some(elem), Map())
- else Linear_Set.make(Some(elem), rep.last_elem, rep.body + (elem -> rep.first_elem.get))
+ rep.first match {
+ case None => throw new Linear_Set.Undefined("")
+ case Some(elem1) =>
+ rep.nexts.get(elem1) match {
+ case None => empty
+ case Some(elem2) =>
+ Linear_Set.make(Some(elem2), rep.last, rep.nexts - elem1, rep.prevs - elem2)
+ }
+ }
+ case Some(elem1) =>
+ if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString)
+ else
+ rep.nexts.get(elem1) match {
+ case None => throw new Linear_Set.Undefined("")
+ case Some(elem2) =>
+ rep.nexts.get(elem2) match {
+ case None =>
+ Linear_Set.make(rep.first, Some(elem1), rep.nexts - elem1, rep.prevs - elem2)
+ case Some(elem3) =>
+ Linear_Set.make(rep.first, rep.last,
+ rep.nexts - elem2 + (elem1 -> elem3),
+ rep.prevs - elem2 + (elem3 -> elem1))
+ }
+ }
}
- def insert_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
- elems.reverse.foldLeft (this) ((ls, elem) => ls._insert_after(hook, elem))
+ def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
+ (elems :\ this)((elem, set) => set.insert_after(hook, elem))
- def delete_after(elem: Option[A]): Linear_Set[A] =
- elem match {
- case Some(elem) =>
- if (!contains(elem)) throw new Linear_Set.Undefined(elem.toString)
- else if (!rep.body.isDefinedAt(elem)) throw new Linear_Set.Undefined(null)
- else if (rep.body(elem) == rep.last_elem.get)
- Linear_Set.make(rep.first_elem, Some(elem), rep.body - elem)
- else Linear_Set.make(rep.first_elem, rep.last_elem,
- rep.body - elem - rep.body(elem) + (elem -> rep.body(rep.body(elem))))
- case None =>
- if (isEmpty) throw new Linear_Set.Undefined(null)
- else if (size == 1) empty
- else Linear_Set.make(Some(rep.body(rep.first_elem.get)), rep.last_elem, rep.body - rep.first_elem.get)
- }
-
- def delete_between(from: Option[A], to: Option[A]): Linear_Set[A] = {
- if(!rep.first_elem.isDefined) this
+ def delete_between(from: Option[A], to: Option[A]): Linear_Set[A] =
+ {
+ if (isEmpty) this
else {
val next =
- if (from == rep.last_elem) None
- else if (from == None) rep.first_elem
- else from.map(rep.body(_))
+ if (from == rep.last) None
+ else if (from == None) rep.first
+ else from.map(rep.nexts(_))
if (next == to) this
else delete_after(from).delete_between(from, to)
}
@@ -89,23 +115,23 @@
def empty[B]: Linear_Set[B] = Linear_Set.empty
- override def isEmpty: Boolean = !rep.last_elem.isDefined
- def size: Int = if (isEmpty) 0 else rep.body.size + 1
+ override def isEmpty: Boolean = !rep.first.isDefined
+ def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
def elements = new Iterator[A] {
- private var next_elem = rep.first_elem
+ private var next_elem = rep.first
def hasNext = next_elem.isDefined
def next = {
val elem = next_elem.get
- next_elem = if (rep.body.isDefinedAt(elem)) Some(rep.body(elem)) else None
+ next_elem = rep.nexts.get(elem)
elem
}
}
def contains(elem: A): Boolean =
- !isEmpty && (rep.last_elem.get == elem || rep.body.isDefinedAt(elem))
+ !isEmpty && (rep.last.get == elem || rep.nexts.isDefinedAt(elem))
- def + (elem: A): Linear_Set[A] = _insert_after(rep.last_elem, elem)
+ def + (elem: A): Linear_Set[A] = insert_after(rep.last, elem)
override def + (elem1: A, elem2: A, elems: A*): Linear_Set[A] =
this + elem1 + elem2 ++ elems
--- a/src/Pure/General/position.ML Fri Sep 11 20:58:29 2009 +1000
+++ b/src/Pure/General/position.ML Thu Sep 17 14:17:37 2009 +1000
@@ -21,6 +21,7 @@
val line: int -> T
val line_file: int -> string -> T
val id: string -> T
+ val id_only: string -> T
val get_id: T -> string option
val put_id: string -> T -> T
val of_properties: Properties.T -> T
@@ -97,8 +98,8 @@
fun line_file i name = Pos ((i, 0, 0), file_name name);
fun line i = line_file i "";
-
fun id id = Pos ((0, 0, 1), [(Markup.idN, id)]);
+fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props);
--- a/src/Pure/Isar/isar_document.ML Fri Sep 11 20:58:29 2009 +1000
+++ b/src/Pure/Isar/isar_document.ML Thu Sep 17 14:17:37 2009 +1000
@@ -278,6 +278,7 @@
val _ =
OuterSyntax.internal_command "Isar.define_command"
(P.string -- P.string >> (fn (id, text) =>
+ Toplevel.position (Position.id_only id) o
Toplevel.imperative (fn () =>
define_command id (OuterSyntax.prepare_command (Position.id id) text))));
--- a/src/Pure/ML-Systems/proper_int.ML Fri Sep 11 20:58:29 2009 +1000
+++ b/src/Pure/ML-Systems/proper_int.ML Thu Sep 17 14:17:37 2009 +1000
@@ -136,6 +136,24 @@
end;
+(* StringCvt *)
+
+structure StringCvt =
+struct
+ open StringCvt;
+ datatype realfmt = EXACT | FIX of int option | GEN of int option | SCI of int option
+ fun realfmt fmt = Real.fmt
+ (case fmt of
+ EXACT => StringCvt.EXACT
+ | FIX NONE => StringCvt.FIX NONE
+ | FIX (SOME b) => StringCvt.FIX (SOME (dest_int b))
+ | GEN NONE => StringCvt.GEN NONE
+ | GEN (SOME b) => StringCvt.GEN (SOME (dest_int b))
+ | SCI NONE => StringCvt.SCI NONE
+ | SCI (SOME b) => StringCvt.SCI (SOME (dest_int b)));
+end;
+
+
(* Word *)
structure Word =
@@ -165,6 +183,7 @@
val trunc = mk_int o Real.trunc;
fun toInt a b = mk_int (Real.toInt a b);
fun fromInt a = Real.fromInt (dest_int a);
+ val fmt = StringCvt.realfmt;
end;
val ceil = Real.ceil;
--- a/src/Pure/thm.ML Fri Sep 11 20:58:29 2009 +1000
+++ b/src/Pure/thm.ML Thu Sep 17 14:17:37 2009 +1000
@@ -153,7 +153,7 @@
val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
end;
-structure Thm:> THM =
+structure Thm: THM =
struct
structure Pt = Proofterm;
@@ -163,11 +163,12 @@
(** certified types **)
-datatype ctyp = Ctyp of
+abstype ctyp = Ctyp of
{thy_ref: theory_ref,
T: typ,
maxidx: int,
- sorts: sort OrdList.T};
+ sorts: sort OrdList.T}
+with
fun rep_ctyp (Ctyp args) = args;
fun theory_of_ctyp (Ctyp {thy_ref, ...}) = Theory.deref thy_ref;
@@ -189,12 +190,13 @@
(** certified terms **)
(*certified terms with checked typ, maxidx, and sorts*)
-datatype cterm = Cterm of
+abstype cterm = Cterm of
{thy_ref: theory_ref,
t: term,
T: typ,
maxidx: int,
- sorts: sort OrdList.T};
+ sorts: sort OrdList.T}
+with
exception CTERM of string * cterm list;
@@ -337,7 +339,7 @@
(*** Derivations and Theorems ***)
-datatype thm = Thm of
+abstype thm = Thm of
deriv * (*derivation*)
{thy_ref: theory_ref, (*dynamic reference to theory*)
tags: Properties.T, (*additional annotations/comments*)
@@ -348,7 +350,8 @@
prop: term} (*conclusion*)
and deriv = Deriv of
{promises: (serial * thm future) OrdList.T,
- body: Pt.proof_body};
+ body: Pt.proof_body}
+with
type conv = cterm -> thm;
@@ -1718,6 +1721,10 @@
end
end;
+end;
+end;
+end;
+
(* authentic derivation names *)