--- a/CONTRIBUTORS Fri Sep 18 14:40:06 2009 +0200
+++ b/CONTRIBUTORS Fri Sep 18 14:40:24 2009 +0200
@@ -7,6 +7,12 @@
Contributions to this Isabelle version
--------------------------------------
+* September 2009: Florian Haftmann, TUM
+ Refinement of Sets and Lattices
+
+* July 2009: Jeremy Avigad and Amine Chaieb
+ New number theory
+
* July 2009: Philipp Meyer, TUM
HOL/Library/Sum_of_Squares: functionality to call a remote csdp prover
--- a/NEWS Fri Sep 18 14:40:06 2009 +0200
+++ b/NEWS Fri Sep 18 14:40:24 2009 +0200
@@ -19,14 +19,28 @@
*** HOL ***
* Reorganization of number theory:
- * former session NumberTheory now named Old_Number_Theory; former session NewNumberTheory
- named NumberTheory;
- * split off prime number ingredients from theory GCD to theory Number_Theory/Primes;
+ * former session NumberTheory now named Old_Number_Theory
+ * new session Number_Theory by Jeremy Avigad; if possible, prefer this.
* moved legacy theories Legacy_GCD and Primes from Library/ to Old_Number_Theory/;
* moved theory Pocklington from Library/ to Old_Number_Theory/;
* removed various references to Old_Number_Theory from HOL distribution.
INCOMPATIBILITY.
+* Theory GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm
+of finite and infinite sets. It is shown that they form a complete
+lattice.
+
+* Split off prime number ingredients from theory GCD
+to theory Number_Theory/Primes;
+
+* Class semiring_div requires superclass no_zero_divisors and proof of
+div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
+div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
+generalized to class semiring_div, subsuming former theorems
+zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
+zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default.
+INCOMPATIBILITY.
+
* New testing tool "Mirabelle" for automated (proof) tools. Applies
several tools and tactics like sledgehammer, metis, or quickcheck, to
every proof step in a theory. To be used in batch mode via the
@@ -47,16 +61,15 @@
etc.
INCOMPATIBILITY.
-* New class "boolean_algebra".
-
* 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
+ - new class "boolean_algebra"
- class "complete_lattice" moved to separate theory "complete_lattice";
- corresponding constants (and abbreviations) renamed:
+ corresponding constants (and abbreviations) renamed and with authentic syntax:
Set.Inf ~> Complete_Lattice.Inf
Set.Sup ~> Complete_Lattice.Sup
Set.INFI ~> Complete_Lattice.INFI
@@ -66,24 +79,22 @@
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
+ Set.Int ~> Set.inter
+ Set.Un ~> Set.union
+ - authentic syntax for
+ Set.Pow
+ Set.image
- mere abbreviations:
Set.empty (for bot)
Set.UNIV (for top)
Complete_Lattice.Inter (for Inf)
Complete_Lattice.Union (for Sup)
+ Complete_Lattice.INTER (for INFI)
+ Complete_Lattice.UNION (for SUPR)
+ - object-logic definitions as far as appropriate
INCOMPATIBILITY.
-* Class semiring_div requires superclass no_zero_divisors and proof of
-div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
-div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
-generalized to class semiring_div, subsuming former theorems
-zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
-zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default.
-INCOMPATIBILITY.
-
* Power operations on relations and functions are now one dedicate
constant "compow" with infix syntax "^^". Power operations on
multiplicative monoids retains syntax "^" and is now defined generic
@@ -96,10 +107,6 @@
this. Fix using O_assoc[symmetric]. The same applies to the curried
version "R OO S".
-* Theory GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm
-of finite and infinite sets. It is shown that they form a complete
-lattice.
-
* ML antiquotation @{code_datatype} inserts definition of a datatype
generated by the code generator; see Predicate.thy for an example.
@@ -110,10 +117,6 @@
default generators are provided for all suitable HOL types, records
and datatypes.
-* Constants Set.Pow and Set.image now with authentic syntax;
-object-logic definitions Set.Pow_def and Set.image_def.
-INCOMPATIBILITY.
-
* Renamed theorems:
Suc_eq_add_numeral_1 -> Suc_eq_plus1
Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
@@ -138,9 +141,6 @@
INCOMPATIBILITY.
-* NewNumberTheory: Jeremy Avigad's new version of part of
-NumberTheory. If possible, use NewNumberTheory, not NumberTheory.
-
* Discontinued abbreviation "arbitrary" of constant
"undefined". INCOMPATIBILITY, use "undefined" directly.
--- a/src/HOL/Complete_Lattice.thy Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Complete_Lattice.thy Fri Sep 18 14:40:24 2009 +0200
@@ -278,8 +278,8 @@
subsection {* Unions of families *}
-definition UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
- SUPR_set_eq [symmetric]: "UNION S f = (SUP x:S. f x)"
+abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
+ "UNION \<equiv> SUPR"
syntax
"@UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" [0, 10] 10)
@@ -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])
+ by (fact SUPR_def)
lemma Union_def:
"\<Union>S = (\<Union>x\<in>S. x)"
@@ -351,7 +351,7 @@
by blast
lemma UN_upper: "a \<in> A ==> B a \<subseteq> (\<Union>x\<in>A. B x)"
- by blast
+ by (fact le_SUPI)
lemma UN_least: "(!!x. x \<in> A ==> B x \<subseteq> C) ==> (\<Union>x\<in>A. B x) \<subseteq> C"
by (iprover intro: subsetI elim: UN_E dest: subsetD)
@@ -514,8 +514,8 @@
subsection {* Intersections of families *}
-definition INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
- INFI_set_eq [symmetric]: "INTER S f = (INF x:S. f x)"
+abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
+ "INTER \<equiv> INFI"
syntax
"@INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" [0, 10] 10)
@@ -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])
+ by (fact INFI_def)
lemma Inter_def:
"\<Inter>S = (\<Inter>x\<in>S. x)"
@@ -579,10 +579,10 @@
by blast
lemma INT_lower: "a \<in> A ==> (\<Inter>x\<in>A. B x) \<subseteq> B a"
- by blast
+ by (fact INF_leI)
lemma INT_greatest: "(!!x. x \<in> A ==> C \<subseteq> B x) ==> C \<subseteq> (\<Inter>x\<in>A. B x)"
- by (iprover intro: INT_I subsetI dest: subsetD)
+ by (fact le_INFI)
lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
by blast
--- a/src/HOL/Lambda/Eta.thy Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Lambda/Eta.thy Fri Sep 18 14:40:24 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Lambda/Eta.thy
- ID: $Id$
Author: Tobias Nipkow and Stefan Berghofer
Copyright 1995, 2005 TU Muenchen
*)
@@ -87,7 +86,6 @@
lemma square_eta: "square eta eta (eta^==) (eta^==)"
apply (unfold square_def id_def)
apply (rule impI [THEN allI [THEN allI]])
- apply simp
apply (erule eta.induct)
apply (slowsimp intro: subst_not_free eta_subst free_eta [THEN iffD1])
apply safe
--- a/src/HOL/Library/Executable_Set.thy Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Library/Executable_Set.thy Fri Sep 18 14:40:24 2009 +0200
@@ -32,8 +32,8 @@
declare inter [code]
-declare Inter_image_eq [symmetric, code]
-declare Union_image_eq [symmetric, code]
+declare Inter_image_eq [symmetric, code_unfold]
+declare Union_image_eq [symmetric, code_unfold]
declare List_Set.project_def [symmetric, code_unfold]
--- a/src/HOL/Predicate.thy Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Predicate.thy Fri Sep 18 14:40:24 2009 +0200
@@ -75,29 +75,29 @@
subsubsection {* Binary union *}
-lemma sup1_iff [simp]: "sup A B x \<longleftrightarrow> A x | B x"
+lemma sup1_iff: "sup A B x \<longleftrightarrow> A x | B x"
by (simp add: sup_fun_eq sup_bool_eq)
-lemma sup2_iff [simp]: "sup A B x y \<longleftrightarrow> A x y | B x y"
+lemma sup2_iff: "sup A B x y \<longleftrightarrow> A x y | B x y"
by (simp add: sup_fun_eq sup_bool_eq)
lemma sup_Un_eq [pred_set_conv]: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
- by (simp add: expand_fun_eq)
+ by (simp add: sup1_iff expand_fun_eq)
lemma sup_Un_eq2 [pred_set_conv]: "sup (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
- by (simp add: expand_fun_eq)
+ by (simp add: sup2_iff expand_fun_eq)
lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x"
- by simp
+ by (simp add: sup1_iff)
lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y"
- by simp
+ by (simp add: sup2_iff)
lemma sup1I2 [elim?]: "B x \<Longrightarrow> sup A B x"
- by simp
+ by (simp add: sup1_iff)
lemma sup2I2 [elim?]: "B x y \<Longrightarrow> sup A B x y"
- by simp
+ by (simp add: sup2_iff)
text {*
\medskip Classical introduction rule: no commitment to @{text A} vs
@@ -105,115 +105,115 @@
*}
lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x"
- by auto
+ by (auto simp add: sup1_iff)
lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y"
- by auto
+ by (auto simp add: sup2_iff)
lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
- by simp iprover
+ by (simp add: sup1_iff) iprover
lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
- by simp iprover
+ by (simp add: sup2_iff) iprover
subsubsection {* Binary intersection *}
-lemma inf1_iff [simp]: "inf A B x \<longleftrightarrow> A x \<and> B x"
+lemma inf1_iff: "inf A B x \<longleftrightarrow> A x \<and> B x"
by (simp add: inf_fun_eq inf_bool_eq)
-lemma inf2_iff [simp]: "inf A B x y \<longleftrightarrow> A x y \<and> B x y"
+lemma inf2_iff: "inf A B x y \<longleftrightarrow> A x y \<and> B x y"
by (simp add: inf_fun_eq inf_bool_eq)
lemma inf_Int_eq [pred_set_conv]: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
- by (simp add: expand_fun_eq)
+ by (simp add: inf1_iff expand_fun_eq)
lemma inf_Int_eq2 [pred_set_conv]: "inf (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
- by (simp add: expand_fun_eq)
+ by (simp add: inf2_iff expand_fun_eq)
lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
- by simp
+ by (simp add: inf1_iff)
lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
- by simp
+ by (simp add: inf2_iff)
lemma inf1D1: "inf A B x ==> A x"
- by simp
+ by (simp add: inf1_iff)
lemma inf2D1: "inf A B x y ==> A x y"
- by simp
+ by (simp add: inf2_iff)
lemma inf1D2: "inf A B x ==> B x"
- by simp
+ by (simp add: inf1_iff)
lemma inf2D2: "inf A B x y ==> B x y"
- by simp
+ by (simp add: inf2_iff)
lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
- by simp
+ by (simp add: inf1_iff)
lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
- by simp
+ by (simp add: inf2_iff)
subsubsection {* Unions of families *}
-lemma SUP1_iff [simp]: "(SUP x:A. B x) b = (EX x:A. B x b)"
+lemma SUP1_iff: "(SUP x:A. B x) b = (EX x:A. B x b)"
by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast
-lemma SUP2_iff [simp]: "(SUP x:A. B x) b c = (EX x:A. B x b c)"
+lemma SUP2_iff: "(SUP x:A. B x) b c = (EX x:A. B x b c)"
by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast
lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b"
- by auto
+ by (auto simp add: SUP1_iff)
lemma SUP2_I [intro]: "a : A ==> B a b c ==> (SUP x:A. B x) b c"
- by auto
+ by (auto simp add: SUP2_iff)
lemma SUP1_E [elim!]: "(SUP x:A. B x) b ==> (!!x. x : A ==> B x b ==> R) ==> R"
- by auto
+ by (auto simp add: SUP1_iff)
lemma SUP2_E [elim!]: "(SUP x:A. B x) b c ==> (!!x. x : A ==> B x b c ==> R) ==> R"
- by auto
+ by (auto simp add: SUP2_iff)
lemma SUP_UN_eq: "(SUP i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (UN i. r i))"
- by (simp add: expand_fun_eq)
+ by (simp add: SUP1_iff expand_fun_eq)
lemma SUP_UN_eq2: "(SUP i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (UN i. r i))"
- by (simp add: expand_fun_eq)
+ by (simp add: SUP2_iff expand_fun_eq)
subsubsection {* Intersections of families *}
-lemma INF1_iff [simp]: "(INF x:A. B x) b = (ALL x:A. B x b)"
+lemma INF1_iff: "(INF x:A. B x) b = (ALL x:A. B x b)"
by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
-lemma INF2_iff [simp]: "(INF x:A. B x) b c = (ALL x:A. B x b c)"
+lemma INF2_iff: "(INF x:A. B x) b c = (ALL x:A. B x b c)"
by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
lemma INF1_I [intro!]: "(!!x. x : A ==> B x b) ==> (INF x:A. B x) b"
- by auto
+ by (auto simp add: INF1_iff)
lemma INF2_I [intro!]: "(!!x. x : A ==> B x b c) ==> (INF x:A. B x) b c"
- by auto
+ by (auto simp add: INF2_iff)
lemma INF1_D [elim]: "(INF x:A. B x) b ==> a : A ==> B a b"
- by auto
+ by (auto simp add: INF1_iff)
lemma INF2_D [elim]: "(INF x:A. B x) b c ==> a : A ==> B a b c"
- by auto
+ by (auto simp add: INF2_iff)
lemma INF1_E [elim]: "(INF x:A. B x) b ==> (B a b ==> R) ==> (a ~: A ==> R) ==> R"
- by auto
+ by (auto simp add: INF1_iff)
lemma INF2_E [elim]: "(INF x:A. B x) b c ==> (B a b c ==> R) ==> (a ~: A ==> R) ==> R"
- by auto
+ by (auto simp add: INF2_iff)
lemma INF_INT_eq: "(INF i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (INT i. r i))"
- by (simp add: expand_fun_eq)
+ by (simp add: INF1_iff expand_fun_eq)
lemma INF_INT_eq2: "(INF i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (INT i. r i))"
- by (simp add: expand_fun_eq)
+ by (simp add: INF2_iff expand_fun_eq)
subsection {* Predicates as relations *}
@@ -429,7 +429,7 @@
by (auto simp add: bind_def sup_pred_def expand_fun_eq)
lemma Sup_bind: "(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)"
- by (auto simp add: bind_def Sup_pred_def expand_fun_eq)
+ by (auto simp add: bind_def Sup_pred_def SUP1_iff expand_fun_eq)
lemma pred_iffI:
assumes "\<And>x. eval A x \<Longrightarrow> eval B x"
@@ -462,10 +462,10 @@
unfolding bot_pred_def by auto
lemma supI1: "eval A x \<Longrightarrow> eval (A \<squnion> B) x"
- unfolding sup_pred_def by simp
+ unfolding sup_pred_def by (simp add: sup1_iff)
lemma supI2: "eval B x \<Longrightarrow> eval (A \<squnion> B) x"
- unfolding sup_pred_def by simp
+ unfolding sup_pred_def by (simp add: sup1_iff)
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
--- a/src/HOL/Tools/Function/decompose.ML Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/Function/decompose.ML Fri Sep 18 14:40:24 2009 +0200
@@ -29,7 +29,7 @@
fun prove_chain c1 c2 D =
if is_some (Termination.get_chain D c1 c2) then D else
let
- val goal = HOLogic.mk_eq (HOLogic.mk_binop @{const_name "Relation.rel_comp"} (c1, c2),
+ val goal = HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.rel_comp} (c1, c2),
Const (@{const_name Set.empty}, fastype_of c1))
|> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
--- a/src/HOL/Tools/Function/fundef_common.ML Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_common.ML Fri Sep 18 14:40:24 2009 +0200
@@ -16,7 +16,7 @@
fun PROFILE msg = if !profile then timeap_msg msg else I
-val acc_const_name = @{const_name "accp"}
+val acc_const_name = @{const_name accp}
fun mk_acc domT R =
Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R
--- a/src/HOL/Tools/Function/fundef_core.ML Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_core.ML Fri Sep 18 14:40:24 2009 +0200
@@ -769,7 +769,7 @@
val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
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'" *)
+ val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
(* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
val ihyp = Term.all domT $ Abs ("z", domT,
--- a/src/HOL/Tools/Function/induction_scheme.ML Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/Function/induction_scheme.ML Fri Sep 18 14:40:24 2009 +0200
@@ -152,7 +152,7 @@
end
fun mk_wf ctxt R (IndScheme {T, ...}) =
- HOLogic.Trueprop $ (Const (@{const_name "wf"}, mk_relT T --> HOLogic.boolT) $ R)
+ HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R)
fun mk_ineqs R (IndScheme {T, cases, branches}) =
let
--- a/src/HOL/Tools/Function/lexicographic_order.ML Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Fri Sep 18 14:40:24 2009 +0200
@@ -26,7 +26,7 @@
val mlexT = (domT --> HOLogic.natT) --> relT --> relT
fun mk_ms [] = Const (@{const_name Set.empty}, relT)
| mk_ms (f::fs) =
- Const (@{const_name "mlex_prod"}, mlexT) $ f $ mk_ms fs
+ Const (@{const_name mlex_prod}, mlexT) $ f $ mk_ms fs
in
mk_ms mfuns
end
--- a/src/HOL/Tools/Function/measure_functions.ML Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/Function/measure_functions.ML Fri Sep 18 14:40:24 2009 +0200
@@ -22,7 +22,7 @@
val description = "Rules that guide the heuristic generation of measure functions"
);
-fun mk_is_measures t = Const (@{const_name "is_measure"}, fastype_of t --> HOLogic.boolT) $ t
+fun mk_is_measures t = Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t
fun find_measures ctxt T =
DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1)
--- a/src/HOL/Tools/Function/sum_tree.ML Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/Function/sum_tree.ML Fri Sep 18 14:40:24 2009 +0200
@@ -17,22 +17,22 @@
(* Sum types *)
fun mk_sumT LT RT = Type ("+", [LT, RT])
-fun mk_sumcase TL TR T l r = Const (@{const_name "sum.sum_case"}, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
+fun mk_sumcase TL TR T l r = Const (@{const_name sum.sum_case}, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
val App = curry op $
fun mk_inj ST n i =
access_top_down
{ init = (ST, I : term -> term),
- left = (fn (T as Type ("+", [LT, RT]), inj) => (LT, inj o App (Const (@{const_name "Inl"}, LT --> T)))),
- right =(fn (T as Type ("+", [LT, RT]), inj) => (RT, inj o App (Const (@{const_name "Inr"}, RT --> T))))} n i
+ left = (fn (T as Type ("+", [LT, RT]), inj) => (LT, inj o App (Const (@{const_name Inl}, LT --> T)))),
+ right =(fn (T as Type ("+", [LT, RT]), inj) => (RT, inj o App (Const (@{const_name Inr}, RT --> T))))} n i
|> snd
fun mk_proj ST n i =
access_top_down
{ init = (ST, I : term -> term),
- left = (fn (T as Type ("+", [LT, RT]), proj) => (LT, App (Const (@{const_name "Datatype.Projl"}, T --> LT)) o proj)),
- right =(fn (T as Type ("+", [LT, RT]), proj) => (RT, App (Const (@{const_name "Datatype.Projr"}, T --> RT)) o proj))} n i
+ left = (fn (T as Type ("+", [LT, RT]), proj) => (LT, App (Const (@{const_name Datatype.Projl}, T --> LT)) o proj)),
+ right =(fn (T as Type ("+", [LT, RT]), proj) => (RT, App (Const (@{const_name Datatype.Projr}, T --> RT)) o proj))} n i
|> snd
fun mk_sumcases T fs =
--- a/src/HOL/Tools/Function/termination.ML Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/Function/termination.ML Fri Sep 18 14:40:24 2009 +0200
@@ -79,14 +79,14 @@
(* concrete versions for sum types *)
-fun is_inj (Const ("Sum_Type.Inl", _) $ _) = true
- | is_inj (Const ("Sum_Type.Inr", _) $ _) = true
+fun is_inj (Const (@{const_name Sum_Type.Inl}, _) $ _) = true
+ | is_inj (Const (@{const_name Sum_Type.Inr}, _) $ _) = true
| is_inj _ = false
-fun dest_inl (Const ("Sum_Type.Inl", _) $ t) = SOME t
+fun dest_inl (Const (@{const_name Sum_Type.Inl}, _) $ t) = SOME t
| dest_inl _ = NONE
-fun dest_inr (Const ("Sum_Type.Inr", _) $ t) = SOME t
+fun dest_inr (Const (@{const_name Sum_Type.Inr}, _) $ t) = SOME t
| dest_inr _ = NONE
@@ -145,8 +145,8 @@
fun mk_sum_skel rel =
let
- val cs = FundefLib.dest_binop_list @{const_name union} rel
- fun collect_pats (Const ("Collect", _) $ Abs (_, _, c)) =
+ val cs = FundefLib.dest_binop_list @{const_name Set.union} rel
+ fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
let
val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
= Term.strip_qnt_body "Ex" c
@@ -179,7 +179,7 @@
fun get_descent (_, _, _, _, D) c m1 m2 =
Term3tab.lookup D (c, (m1, m2))
-fun dest_call D (Const ("Collect", _) $ Abs (_, _, c)) =
+fun dest_call D (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
let
val n = get_num_points D
val (sk, _, _, _, _) = D
@@ -233,13 +233,13 @@
fun CALLS tac i st =
if Thm.no_prems st then all_tac st
else case Thm.term_of (Thm.cprem_of st i) of
- (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name union} rel, i) st
+ (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Set.union} rel, i) st
|_ => no_tac st
type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
fun TERMINATION ctxt tac =
- SUBGOAL (fn (_ $ (Const (@{const_name "wf"}, wfT) $ rel), i) =>
+ SUBGOAL (fn (_ $ (Const (@{const_name wf}, wfT) $ rel), i) =>
let
val (T, _) = HOLogic.dest_prodT (HOLogic.dest_setT (domain_type wfT))
in
@@ -293,7 +293,7 @@
if null ineqs then
Const (@{const_name Set.empty}, fastype_of rel)
else
- foldr1 (HOLogic.mk_binop @{const_name union}) (map mk_compr ineqs)
+ foldr1 (HOLogic.mk_binop @{const_name Set.union}) (map mk_compr ineqs)
fun solve_membership_tac i =
(EVERY' (replicate (i - 2) (rtac @{thm UnI2})) (* pick the right component of the union *)
--- a/src/HOL/Tools/Qelim/cooper.ML Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Fri Sep 18 14:40:24 2009 +0200
@@ -81,7 +81,7 @@
else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
| Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$y$_) =>
if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox
-| Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_)) =>
+| Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$y$_)) =>
if term_of x aconv y then
NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox
| _ => Nox)
--- a/src/HOL/Tools/Qelim/presburger.ML Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/Qelim/presburger.ML Fri Sep 18 14:40:24 2009 +0200
@@ -52,18 +52,18 @@
local
fun isnum t = case t of
- Const(@{const_name "HOL.zero"},_) => true
- | Const(@{const_name "HOL.one"},_) => true
+ Const(@{const_name HOL.zero},_) => true
+ | Const(@{const_name HOL.one},_) => true
| @{term "Suc"}$s => isnum s
| @{term "nat"}$s => isnum s
| @{term "int"}$s => isnum s
- | Const(@{const_name "HOL.uminus"},_)$s => isnum s
- | Const(@{const_name "HOL.plus"},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name "HOL.times"},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name "HOL.minus"},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name "Power.power"},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name "Divides.mod"},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name "Divides.div"},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name HOL.uminus},_)$s => isnum s
+ | Const(@{const_name HOL.plus},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name HOL.times},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name HOL.minus},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r
| _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t
fun ty cts t =
--- a/src/HOL/Tools/Qelim/qelim.ML Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML Fri Sep 18 14:40:24 2009 +0200
@@ -29,8 +29,8 @@
@{const_name "op -->"}, @{const_name "op ="}] s
then binop_conv (conv env) p
else atcv env p
- | Const(@{const_name "Not"},_)$_ => arg_conv (conv env) p
- | Const(@{const_name "Ex"},_)$Abs(s,_,_) =>
+ | Const(@{const_name Not},_)$_ => arg_conv (conv env) p
+ | Const(@{const_name Ex},_)$Abs(s,_,_) =>
let
val (e,p0) = Thm.dest_comb p
val (x,p') = Thm.dest_abs (SOME s) p0
@@ -41,8 +41,8 @@
val (l,r) = Thm.dest_equals (cprop_of th')
in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))
else Thm.transitive (Thm.transitive th th') (conv env r) end
- | Const(@{const_name "Ex"},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
- | Const(@{const_name "All"},_)$_ =>
+ | Const(@{const_name Ex},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
+ | Const(@{const_name All},_)$_ =>
let
val p = Thm.dest_arg p
val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)
--- a/src/HOL/Tools/TFL/rules.ML Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Fri Sep 18 14:40:24 2009 +0200
@@ -456,7 +456,7 @@
fun is_cong thm =
case (Thm.prop_of thm)
of (Const("==>",_)$(Const("Trueprop",_)$ _) $
- (Const("==",_) $ (Const (@{const_name "Recdef.cut"},_) $ f $ R $ a $ x) $ _)) => false
+ (Const("==",_) $ (Const (@{const_name Recdef.cut},_) $ f $ R $ a $ x) $ _)) => false
| _ => true;
@@ -659,7 +659,7 @@
end;
fun restricted t = isSome (S.find_term
- (fn (Const(@{const_name "Recdef.cut"},_)) =>true | _ => false)
+ (fn (Const(@{const_name Recdef.cut},_)) =>true | _ => false)
t)
fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
--- a/src/HOL/Tools/TFL/usyntax.ML Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML Fri Sep 18 14:40:24 2009 +0200
@@ -398,7 +398,7 @@
end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure"
else raise USYN_ERR "dest_relation" "not a boolean term";
-fun is_WFR (Const(@{const_name "Wellfounded.wf"},_)$_) = true
+fun is_WFR (Const(@{const_name Wellfounded.wf},_)$_) = true
| is_WFR _ = false;
fun ARB ty = mk_select{Bvar=Free("v",ty),
--- a/src/HOL/Tools/float_syntax.ML Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/float_syntax.ML Fri Sep 18 14:40:24 2009 +0200
@@ -27,10 +27,10 @@
fun mk_frac str =
let
val {mant=i, exp = n} = Syntax.read_float str;
- val exp = Syntax.const @{const_name "Power.power"};
+ val exp = Syntax.const @{const_name Power.power};
val ten = mk_number 10;
val exp10 = if n=1 then ten else exp $ ten $ (mk_number n);
- in (Syntax.const @{const_name "divide"}) $ (mk_number i) $ exp10 end
+ in (Syntax.const @{const_name divide}) $ (mk_number i) $ exp10 end
in
fun float_tr (*"_Float"*) [t as Const (str, _)] = mk_frac str
--- a/src/HOL/Tools/inductive.ML Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/inductive.ML Fri Sep 18 14:40:24 2009 +0200
@@ -86,13 +86,13 @@
(** theory context references **)
val inductive_forall_name = "HOL.induct_forall";
-val inductive_forall_def = thm "induct_forall_def";
+val inductive_forall_def = @{thm induct_forall_def};
val inductive_conj_name = "HOL.induct_conj";
-val inductive_conj_def = thm "induct_conj_def";
-val inductive_conj = thms "induct_conj";
-val inductive_atomize = thms "induct_atomize";
-val inductive_rulify = thms "induct_rulify";
-val inductive_rulify_fallback = thms "induct_rulify_fallback";
+val inductive_conj_def = @{thm induct_conj_def};
+val inductive_conj = @{thms induct_conj};
+val inductive_atomize = @{thms induct_atomize};
+val inductive_rulify = @{thms induct_rulify};
+val inductive_rulify_fallback = @{thms induct_rulify_fallback};
val notTrueE = TrueI RSN (2, notE);
val notFalseI = Seq.hd (atac 1 notI);
@@ -176,7 +176,7 @@
case concl of
Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
| _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
- | _ $ (Const ("HOL.ord_class.less_eq", _) $ _ $ _) =>
+ | _ $ (Const (@{const_name HOL.less_eq}, _) $ _ $ _) =>
[dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
(resolve_tac [le_funI, le_boolI'])) thm))]
| _ => [thm]
--- a/src/HOL/Tools/inductive_set.ML Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/inductive_set.ML Fri Sep 18 14:40:24 2009 +0200
@@ -74,8 +74,8 @@
in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
(p (fold (Logic.all o Var) vs t) f)
end;
- fun mkop "op &" T x = SOME (Const (@{const_name inter}, T --> T --> T), x)
- | mkop "op |" T x = SOME (Const (@{const_name union}, T --> T --> T), x)
+ fun mkop "op &" T x = SOME (Const (@{const_name Set.inter}, T --> T --> T), x)
+ | mkop "op |" T x = SOME (Const (@{const_name Set.union}, T --> T --> T), x)
| mkop _ _ _ = NONE;
fun mk_collect p T t =
let val U = HOLogic.dest_setT T
--- a/src/HOL/Tools/int_arith.ML Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/int_arith.ML Fri Sep 18 14:40:24 2009 +0200
@@ -49,13 +49,13 @@
make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
proc = proc1, identifier = []};
-fun check (Const (@{const_name "HOL.one"}, @{typ int})) = false
- | check (Const (@{const_name "HOL.one"}, _)) = true
+fun check (Const (@{const_name HOL.one}, @{typ int})) = false
+ | check (Const (@{const_name HOL.one}, _)) = true
| check (Const (s, _)) = member (op =) [@{const_name "op ="},
- @{const_name "HOL.times"}, @{const_name "HOL.uminus"},
- @{const_name "HOL.minus"}, @{const_name "HOL.plus"},
- @{const_name "HOL.zero"},
- @{const_name "HOL.less"}, @{const_name "HOL.less_eq"}] s
+ @{const_name HOL.times}, @{const_name HOL.uminus},
+ @{const_name HOL.minus}, @{const_name HOL.plus},
+ @{const_name HOL.zero},
+ @{const_name HOL.less}, @{const_name HOL.less_eq}] s
| check (a $ b) = check a andalso check b
| check _ = false;
--- a/src/HOL/Tools/lin_arith.ML Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/lin_arith.ML Fri Sep 18 14:40:24 2009 +0200
@@ -51,7 +51,7 @@
atomize (thm RS conjunct1) @ atomize (thm RS conjunct2)
| _ => [thm];
-fun neg_prop ((TP as Const("Trueprop", _)) $ (Const (@{const_name "Not"}, _) $ t)) = TP $ t
+fun neg_prop ((TP as Const("Trueprop", _)) $ (Const (@{const_name Not}, _) $ t)) = TP $ t
| neg_prop ((TP as Const("Trueprop", _)) $ t) = TP $ (HOLogic.Not $t)
| neg_prop t = raise TERM ("neg_prop", [t]);
--- a/src/HOL/Transitive_Closure.thy Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Transitive_Closure.thy Fri Sep 18 14:40:24 2009 +0200
@@ -77,7 +77,7 @@
subsection {* Reflexive-transitive closure *}
lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r Un Id)"
- by (simp add: expand_fun_eq)
+ by (simp add: expand_fun_eq sup2_iff)
lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*"
-- {* @{text rtrancl} of @{text r} contains @{text r} *}
--- a/src/HOL/UNITY/ProgressSets.thy Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/UNITY/ProgressSets.thy Fri Sep 18 14:40:24 2009 +0200
@@ -534,7 +534,7 @@
subsubsection{*Commutativity of Functions and Relation*}
text{*Thesis, page 109*}
-(*FIXME: this proof is an ungodly mess*)
+(*FIXME: this proof is still an ungodly mess*)
text{*From Meier's thesis, section 4.5.6*}
lemma commutativity2_lemma:
assumes dcommutes:
@@ -548,36 +548,35 @@
and TL: "T \<in> L"
and Fstable: "F \<in> stable T"
shows "commutes F T B L"
-apply (simp add: commutes_def del: Int_subset_iff, clarify)
-apply (rename_tac t)
-apply (subgoal_tac "\<exists>s. (s,t) \<in> relcl L & s \<in> T \<inter> wp act M")
- prefer 2
- apply (force simp add: cl_eq_Collect_relcl [OF lattice], simp, clarify)
-apply (subgoal_tac "\<forall>u\<in>L. s \<in> u --> t \<in> u")
- prefer 2
- apply (intro ballI impI)
- apply (subst cl_ident [symmetric], assumption)
- apply (simp add: relcl_def)
- apply (blast intro: cl_mono [THEN [2] rev_subsetD])
-apply (subgoal_tac "funof act s \<in> T\<inter>M")
- prefer 2
- apply (cut_tac Fstable)
- apply (force intro!: funof_in
- simp add: wp_def stable_def constrains_def determ total)
-apply (subgoal_tac "s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L")
- prefer 2
- apply (rule dcommutes [rule_format], assumption+)
-apply (subgoal_tac "t \<in> B | funof act t \<in> cl L (T\<inter>M)")
- prefer 2
- apply (simp add: relcl_def)
- apply (blast intro: BL cl_mono [THEN [2] rev_subsetD])
-apply (subgoal_tac "t \<in> B | t \<in> wp act (cl L (T\<inter>M))")
- prefer 2
- apply (blast intro: funof_imp_wp determ)
-apply (blast intro: TL cl_mono [THEN [2] rev_subsetD])
-done
-
-
+apply (simp add: commutes_def del: Int_subset_iff le_inf_iff, clarify)
+proof -
+ fix M and act and t
+ assume 1: "B \<subseteq> M" "act \<in> Acts F" "t \<in> cl L (T \<inter> wp act M)"
+ then have "\<exists>s. (s,t) \<in> relcl L \<and> s \<in> T \<inter> wp act M"
+ by (force simp add: cl_eq_Collect_relcl [OF lattice])
+ then obtain s where 2: "(s, t) \<in> relcl L" "s \<in> T" "s \<in> wp act M"
+ by blast
+ then have 3: "\<forall>u\<in>L. s \<in> u --> t \<in> u"
+ apply (intro ballI impI)
+ apply (subst cl_ident [symmetric], assumption)
+ apply (simp add: relcl_def)
+ apply (blast intro: cl_mono [THEN [2] rev_subsetD])
+ done
+ with 1 2 Fstable have 4: "funof act s \<in> T\<inter>M"
+ by (force intro!: funof_in
+ simp add: wp_def stable_def constrains_def determ total)
+ with 1 2 3 have 5: "s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
+ by (intro dcommutes [rule_format]) assumption+
+ with 1 2 3 4 have "t \<in> B | funof act t \<in> cl L (T\<inter>M)"
+ by (simp add: relcl_def) (blast intro: BL cl_mono [THEN [2] rev_subsetD])
+ with 1 2 3 4 5 have "t \<in> B | t \<in> wp act (cl L (T\<inter>M))"
+ by (blast intro: funof_imp_wp determ)
+ with 2 3 have "t \<in> T \<and> (t \<in> B \<or> t \<in> wp act (cl L (T \<inter> M)))"
+ by (blast intro: TL cl_mono [THEN [2] rev_subsetD])
+ then show "t \<in> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))"
+ by simp
+qed
+
text{*Version packaged with @{thm progress_set_Union}*}
lemma commutativity2:
assumes leadsTo: "F \<in> A leadsTo B"