--- a/NEWS Wed May 12 15:25:02 2010 +0200
+++ b/NEWS Wed May 12 15:25:23 2010 +0200
@@ -73,14 +73,14 @@
discontinued (legacy feature).
* References 'trace_simp' and 'debug_simp' have been replaced by
-configuration options stored in the context. Enabling tracing
-(the case of debugging is similar) in proofs works via
-
- using [[trace_simp=true]]
-
-Tracing is then active for all invocations of the simplifier
-in subsequent goal refinement steps. Tracing may also still be
-enabled or disabled via the ProofGeneral settings menu.
+configuration options stored in the context. Enabling tracing (the
+case of debugging is similar) in proofs works via
+
+ using [[trace_simp = true]]
+
+Tracing is then active for all invocations of the simplifier in
+subsequent goal refinement steps. Tracing may also still be enabled or
+disabled via the ProofGeneral settings menu.
* Separate commands 'hide_class', 'hide_type', 'hide_const',
'hide_fact' replace the former 'hide' KIND command. Minor
@@ -89,18 +89,20 @@
*** Pure ***
-* Predicates of locales introduces by classes carry a mandatory "class"
-prefix. INCOMPATIBILITY.
-
-* 'code_reflect' allows to incorporate generated ML code into
-runtime environment; replaces immature code_datatype antiquotation.
+* Predicates of locales introduces by classes carry a mandatory
+"class" prefix. INCOMPATIBILITY.
+
+* Command 'code_reflect' allows to incorporate generated ML code into
+runtime environment; replaces immature code_datatype antiquotation.
INCOMPATIBILITY.
* Empty class specifications observe default sort. INCOMPATIBILITY.
-* Old 'axclass' has been discontinued. Use 'class' instead. INCOMPATIBILITY.
-
-* Code generator: simple concept for abstract datatypes obeying invariants.
+* Old 'axclass' command has been discontinued. Use 'class' instead.
+INCOMPATIBILITY.
+
+* Code generator: simple concept for abstract datatypes obeying
+invariants.
* Local theory specifications may depend on extra type variables that
are not present in the result type -- arguments TYPE('a) :: 'a itself
@@ -108,11 +110,12 @@
definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)"
-* Code generator: details of internal data cache have no impact on
-the user space functionality any longer.
-
-* Methods unfold_locales and intro_locales ignore non-locale subgoals. This
-is more appropriate for interpretations with 'where'. INCOMPATIBILITY.
+* Code generator: details of internal data cache have no impact on the
+user space functionality any longer.
+
+* Methods unfold_locales and intro_locales ignore non-locale subgoals.
+This is more appropriate for interpretations with 'where'.
+INCOMPATIBILITY.
* Discontinued unnamed infix syntax (legacy feature for many years) --
need to specify constant name and syntax separately. Internal ML
@@ -130,18 +133,18 @@
context -- without introducing dependencies on parameters or
assumptions, which is not possible in Isabelle/Pure.
-* Command 'defaultsort' is renamed to 'default_sort', it works within
-a local theory context. Minor INCOMPATIBILITY.
+* Command 'defaultsort' has been renamed to 'default_sort', it works
+within a local theory context. Minor INCOMPATIBILITY.
* Proof terms: Type substitutions on proof constants now use canonical
-order of type variables. INCOMPATIBILITY: Tools working with proof
-terms may need to be adapted.
+order of type variables. Potential INCOMPATIBILITY for tools working
+with proof terms.
*** HOL ***
-* Theorem Int.int_induct renamed to Int.int_of_nat_induct and is
-no longer shadowed. INCOMPATIBILITY.
+* Theorem Int.int_induct renamed to Int.int_of_nat_induct and is no
+longer shadowed. INCOMPATIBILITY.
* Dropped theorem duplicate comp_arith; use semiring_norm instead.
INCOMPATIBILITY.
@@ -149,12 +152,15 @@
* Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.
INCOMPATIBILITY.
-* Theory 'Finite_Set': various folding_* locales facilitate the application
-of the various fold combinators on finite sets.
-
-* Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT'
-provides abstract red-black tree type which is backed by RBT_Impl
-as implementation. INCOMPATIBILTY.
+* Dropped normalizing_semiring etc; use the facts in semiring classes
+instead. INCOMPATIBILITY.
+
+* Theory 'Finite_Set': various folding_XXX locales facilitate the
+application of the various fold combinators on finite sets.
+
+* Library theory "RBT" renamed to "RBT_Impl"; new library theory "RBT"
+provides abstract red-black tree type which is backed by "RBT_Impl" as
+implementation. INCOMPATIBILTY.
* Command 'typedef' now works within a local theory context -- without
introducing dependencies on parameters or assumptions, which is not
@@ -168,27 +174,28 @@
* Theory PReal, including the type "preal" and related operations, has
been removed. INCOMPATIBILITY.
-* Split off theory Big_Operators containing setsum, setprod, Inf_fin, Sup_fin,
-Min, Max from theory Finite_Set. INCOMPATIBILITY.
-
-* Theory "Rational" renamed to "Rat", for consistency with "Nat", "Int" etc.
-INCOMPATIBILITY.
-
-* New set of rules "ac_simps" provides combined assoc / commute rewrites
-for all interpretations of the appropriate generic locales.
-
-* Renamed theory "OrderedGroup" to "Groups" and split theory "Ring_and_Field"
-into theories "Rings" and "Fields"; for more appropriate and more
-consistent names suitable for name prefixes within the HOL theories.
-INCOMPATIBILITY.
+* Split off theory Big_Operators containing setsum, setprod, Inf_fin,
+Sup_fin, Min, Max from theory Finite_Set. INCOMPATIBILITY.
+
+* Theory "Rational" renamed to "Rat", for consistency with "Nat",
+"Int" etc. INCOMPATIBILITY.
+
+* New set of rules "ac_simps" provides combined assoc / commute
+rewrites for all interpretations of the appropriate generic locales.
+
+* Renamed theory "OrderedGroup" to "Groups" and split theory
+"Ring_and_Field" into theories "Rings" and "Fields"; for more
+appropriate and more consistent names suitable for name prefixes
+within the HOL theories. INCOMPATIBILITY.
* Some generic constants have been put to appropriate theories:
- * less_eq, less: Orderings
- * zero, one, plus, minus, uminus, times, abs, sgn: Groups
- * inverse, divide: Rings
+ - less_eq, less: Orderings
+ - zero, one, plus, minus, uminus, times, abs, sgn: Groups
+ - inverse, divide: Rings
INCOMPATIBILITY.
-* More consistent naming of type classes involving orderings (and lattices):
+* More consistent naming of type classes involving orderings (and
+lattices):
lower_semilattice ~> semilattice_inf
upper_semilattice ~> semilattice_sup
@@ -228,8 +235,8 @@
ordered_semiring_1_strict ~> linordered_semiring_1_strict
ordered_semiring_strict ~> linordered_semiring_strict
- The following slightly odd type classes have been moved to
- a separate theory Library/Lattice_Algebras.thy:
+ The following slightly odd type classes have been moved to a
+ separate theory Library/Lattice_Algebras.thy:
lordered_ab_group_add ~> lattice_ab_group_add
lordered_ab_group_add_abs ~> lattice_ab_group_add_abs
@@ -240,17 +247,20 @@
INCOMPATIBILITY.
* Refined field classes:
- * classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
- include rule inverse 0 = 0 -- subsumes former division_by_zero class.
- * numerous lemmas have been ported from field to division_ring;
- INCOMPATIBILITY.
+ - classes division_ring_inverse_zero, field_inverse_zero,
+ linordered_field_inverse_zero include rule inverse 0 = 0 --
+ subsumes former division_by_zero class;
+ - numerous lemmas have been ported from field to division_ring.
+INCOMPATIBILITY.
* Refined algebra theorem collections:
- * dropped theorem group group_simps, use algebra_simps instead;
- * dropped theorem group ring_simps, use field_simps instead;
- * proper theorem collection field_simps subsumes former theorem groups field_eq_simps and field_simps;
- * dropped lemma eq_minus_self_iff which is a duplicate for equal_neg_zero.
- INCOMPATIBILITY.
+ - dropped theorem group group_simps, use algebra_simps instead;
+ - dropped theorem group ring_simps, use field_simps instead;
+ - proper theorem collection field_simps subsumes former theorem
+ groups field_eq_simps and field_simps;
+ - dropped lemma eq_minus_self_iff which is a duplicate for
+ equal_neg_zero.
+INCOMPATIBILITY.
* Theory Finite_Set and List: some lemmas have been generalized from
sets to lattices:
@@ -276,14 +286,19 @@
* HOLogic.strip_psplit: types are returned in syntactic order, similar
to other strip and tuple operations. INCOMPATIBILITY.
-* Reorganized theory Multiset: swapped notation of pointwise and multiset order:
- * pointwise ordering is instance of class order with standard syntax <= and <;
- * multiset ordering has syntax <=# and <#; partial order properties are provided
- by means of interpretation with prefix multiset_order;
- * less duplication, less historical organization of sections,
- conversion from associations lists to multisets, rudimentary code generation;
- * use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union, if needed.
- INCOMPATIBILITY.
+* Reorganized theory Multiset: swapped notation of pointwise and
+multiset order:
+ - pointwise ordering is instance of class order with standard syntax
+ <= and <;
+ - multiset ordering has syntax <=# and <#; partial order properties
+ are provided by means of interpretation with prefix
+ multiset_order;
+ - less duplication, less historical organization of sections,
+ conversion from associations lists to multisets, rudimentary code
+ generation;
+ - use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union,
+ if needed.
+INCOMPATIBILITY.
* Code generation: ML and OCaml code is decorated with signatures.
@@ -3314,7 +3329,7 @@
* Pure: axiomatic type classes are now purely definitional, with
explicit proofs of class axioms and super class relations performed
internally. See Pure/axclass.ML for the main internal interfaces --
-notably AxClass.define_class supersedes AxClass.add_axclass, and
+notably AxClass.define_class supercedes AxClass.add_axclass, and
AxClass.axiomatize_class/classrel/arity supersede
Sign.add_classes/classrel/arities.
@@ -4208,7 +4223,7 @@
* Pure/library.ML: the exception LIST has been given up in favour of
the standard exceptions Empty and Subscript, as well as
Library.UnequalLengths. Function like Library.hd and Library.tl are
-superseded by the standard hd and tl functions etc.
+superceded by the standard hd and tl functions etc.
A number of basic list functions are no longer exported to the ML
toplevel, as they are variants of predefined functions. The following
@@ -4339,15 +4354,15 @@
* Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types,
fold_types traverse types/terms from left to right, observing natural
-argument order. Supersedes previous foldl_XXX versions, add_frees,
+argument order. Supercedes previous foldl_XXX versions, add_frees,
add_vars etc. have been adapted as well: INCOMPATIBILITY.
* Pure: name spaces have been refined, with significant changes of the
internal interfaces -- INCOMPATIBILITY. Renamed cond_extern(_table)
-to extern(_table). The plain name entry path is superseded by a
+to extern(_table). The plain name entry path is superceded by a
general 'naming' context, which also includes the 'policy' to produce
a fully qualified name and external accesses of a fully qualified
-name; NameSpace.extend is superseded by context dependent
+name; NameSpace.extend is superceded by context dependent
Sign.declare_name. Several theory and proof context operations modify
the naming context. Especially note Theory.restore_naming and
ProofContext.restore_naming to get back to a sane state; note that
@@ -4387,7 +4402,7 @@
etc.) as well as the sign field in Thm.rep_thm etc. have been retained
for convenience -- they merely return the theory.
-* Pure: type Type.tsig is superseded by theory in most interfaces.
+* Pure: type Type.tsig is superceded by theory in most interfaces.
* Pure: the Isar proof context type is already defined early in Pure
as Context.proof (note that ProofContext.context and Proof.context are
@@ -5519,7 +5534,7 @@
Eps_sym_eq -> some_sym_eq_trivial
Eps_eq -> some_eq_trivial
-* HOL: exhaust_tac on datatypes superseded by new generic case_tac;
+* HOL: exhaust_tac on datatypes superceded by new generic case_tac;
* HOL: removed obsolete theorem binding expand_if (refer to split_if
instead);
@@ -5657,7 +5672,7 @@
replaced "delrule" by "rule del";
* Isar/Provers: new 'hypsubst' method, plain 'subst' method and
-'symmetric' attribute (the latter supersedes [RS sym]);
+'symmetric' attribute (the latter supercedes [RS sym]);
* Isar/Provers: splitter support (via 'split' attribute and 'simp'
method modifier); 'simp' method: 'only:' modifier removes loopers as
--- a/src/HOL/Decision_Procs/Ferrack.thy Wed May 12 15:25:02 2010 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Wed May 12 15:25:23 2010 +0200
@@ -13,10 +13,9 @@
(* SOME GENERAL STUFF< HAS TO BE MOVED IN SOME LIB *)
(*********************************************************************************)
-consts alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list"
-primrec
+primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list" where
"alluopairs [] = []"
- "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
+| "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x,y). x\<in> set xs \<and> y\<in> set xs}"
by (induct xs, auto)
@@ -47,17 +46,6 @@
lemma filter_length: "length (List.filter P xs) < Suc (length xs)"
apply (induct xs, auto) done
-consts remdps:: "'a list \<Rightarrow> 'a list"
-
-recdef remdps "measure size"
- "remdps [] = []"
- "remdps (x#xs) = (x#(remdps (List.filter (\<lambda> y. y \<noteq> x) xs)))"
-(hints simp add: filter_length[rule_format])
-
-lemma remdps_set[simp]: "set (remdps xs) = set xs"
- by (induct xs rule: remdps.induct, auto)
-
-
(*********************************************************************************)
(**** SHADOW SYNTAX AND SEMANTICS ****)
@@ -67,26 +55,24 @@
| Mul int num
(* A size for num to make inductive proofs simpler*)
-consts num_size :: "num \<Rightarrow> nat"
-primrec
+primrec num_size :: "num \<Rightarrow> nat" where
"num_size (C c) = 1"
- "num_size (Bound n) = 1"
- "num_size (Neg a) = 1 + num_size a"
- "num_size (Add a b) = 1 + num_size a + num_size b"
- "num_size (Sub a b) = 3 + num_size a + num_size b"
- "num_size (Mul c a) = 1 + num_size a"
- "num_size (CN n c a) = 3 + num_size a "
+| "num_size (Bound n) = 1"
+| "num_size (Neg a) = 1 + num_size a"
+| "num_size (Add a b) = 1 + num_size a + num_size b"
+| "num_size (Sub a b) = 3 + num_size a + num_size b"
+| "num_size (Mul c a) = 1 + num_size a"
+| "num_size (CN n c a) = 3 + num_size a "
(* Semantics of numeral terms (num) *)
-consts Inum :: "real list \<Rightarrow> num \<Rightarrow> real"
-primrec
+primrec Inum :: "real list \<Rightarrow> num \<Rightarrow> real" where
"Inum bs (C c) = (real c)"
- "Inum bs (Bound n) = bs!n"
- "Inum bs (CN n c a) = (real c) * (bs!n) + (Inum bs a)"
- "Inum bs (Neg a) = -(Inum bs a)"
- "Inum bs (Add a b) = Inum bs a + Inum bs b"
- "Inum bs (Sub a b) = Inum bs a - Inum bs b"
- "Inum bs (Mul c a) = (real c) * Inum bs a"
+| "Inum bs (Bound n) = bs!n"
+| "Inum bs (CN n c a) = (real c) * (bs!n) + (Inum bs a)"
+| "Inum bs (Neg a) = -(Inum bs a)"
+| "Inum bs (Add a b) = Inum bs a + Inum bs b"
+| "Inum bs (Sub a b) = Inum bs a - Inum bs b"
+| "Inum bs (Mul c a) = (real c) * Inum bs a"
(* FORMULAE *)
datatype fm =
T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num|
@@ -94,38 +80,36 @@
(* A size for fm *)
-consts fmsize :: "fm \<Rightarrow> nat"
-recdef fmsize "measure size"
+fun fmsize :: "fm \<Rightarrow> nat" where
"fmsize (NOT p) = 1 + fmsize p"
- "fmsize (And p q) = 1 + fmsize p + fmsize q"
- "fmsize (Or p q) = 1 + fmsize p + fmsize q"
- "fmsize (Imp p q) = 3 + fmsize p + fmsize q"
- "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"
- "fmsize (E p) = 1 + fmsize p"
- "fmsize (A p) = 4+ fmsize p"
- "fmsize p = 1"
+| "fmsize (And p q) = 1 + fmsize p + fmsize q"
+| "fmsize (Or p q) = 1 + fmsize p + fmsize q"
+| "fmsize (Imp p q) = 3 + fmsize p + fmsize q"
+| "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"
+| "fmsize (E p) = 1 + fmsize p"
+| "fmsize (A p) = 4+ fmsize p"
+| "fmsize p = 1"
(* several lemmas about fmsize *)
lemma fmsize_pos: "fmsize p > 0"
by (induct p rule: fmsize.induct) simp_all
(* Semantics of formulae (fm) *)
-consts Ifm ::"real list \<Rightarrow> fm \<Rightarrow> bool"
-primrec
+primrec Ifm ::"real list \<Rightarrow> fm \<Rightarrow> bool" where
"Ifm bs T = True"
- "Ifm bs F = False"
- "Ifm bs (Lt a) = (Inum bs a < 0)"
- "Ifm bs (Gt a) = (Inum bs a > 0)"
- "Ifm bs (Le a) = (Inum bs a \<le> 0)"
- "Ifm bs (Ge a) = (Inum bs a \<ge> 0)"
- "Ifm bs (Eq a) = (Inum bs a = 0)"
- "Ifm bs (NEq a) = (Inum bs a \<noteq> 0)"
- "Ifm bs (NOT p) = (\<not> (Ifm bs p))"
- "Ifm bs (And p q) = (Ifm bs p \<and> Ifm bs q)"
- "Ifm bs (Or p q) = (Ifm bs p \<or> Ifm bs q)"
- "Ifm bs (Imp p q) = ((Ifm bs p) \<longrightarrow> (Ifm bs q))"
- "Ifm bs (Iff p q) = (Ifm bs p = Ifm bs q)"
- "Ifm bs (E p) = (\<exists> x. Ifm (x#bs) p)"
- "Ifm bs (A p) = (\<forall> x. Ifm (x#bs) p)"
+| "Ifm bs F = False"
+| "Ifm bs (Lt a) = (Inum bs a < 0)"
+| "Ifm bs (Gt a) = (Inum bs a > 0)"
+| "Ifm bs (Le a) = (Inum bs a \<le> 0)"
+| "Ifm bs (Ge a) = (Inum bs a \<ge> 0)"
+| "Ifm bs (Eq a) = (Inum bs a = 0)"
+| "Ifm bs (NEq a) = (Inum bs a \<noteq> 0)"
+| "Ifm bs (NOT p) = (\<not> (Ifm bs p))"
+| "Ifm bs (And p q) = (Ifm bs p \<and> Ifm bs q)"
+| "Ifm bs (Or p q) = (Ifm bs p \<or> Ifm bs q)"
+| "Ifm bs (Imp p q) = ((Ifm bs p) \<longrightarrow> (Ifm bs q))"
+| "Ifm bs (Iff p q) = (Ifm bs p = Ifm bs q)"
+| "Ifm bs (E p) = (\<exists> x. Ifm (x#bs) p)"
+| "Ifm bs (A p) = (\<forall> x. Ifm (x#bs) p)"
lemma IfmLeSub: "\<lbrakk> Inum bs s = s' ; Inum bs t = t' \<rbrakk> \<Longrightarrow> Ifm bs (Le (Sub s t)) = (s' \<le> t')"
apply simp
@@ -160,36 +144,35 @@
apply simp
done
-consts not:: "fm \<Rightarrow> fm"
-recdef not "measure size"
+fun not:: "fm \<Rightarrow> fm" where
"not (NOT p) = p"
- "not T = F"
- "not F = T"
- "not p = NOT p"
+| "not T = F"
+| "not F = T"
+| "not p = NOT p"
lemma not[simp]: "Ifm bs (not p) = Ifm bs (NOT p)"
by (cases p) auto
definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
- "conj p q \<equiv> (if (p = F \<or> q=F) then F else if p=T then q else if q=T then p else
+ "conj p q = (if (p = F \<or> q=F) then F else if p=T then q else if q=T then p else
if p = q then p else And p q)"
lemma conj[simp]: "Ifm bs (conj p q) = Ifm bs (And p q)"
by (cases "p=F \<or> q=F",simp_all add: conj_def) (cases p,simp_all)
definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
- "disj p q \<equiv> (if (p = T \<or> q=T) then T else if p=F then q else if q=F then p
+ "disj p q = (if (p = T \<or> q=T) then T else if p=F then q else if q=F then p
else if p=q then p else Or p q)"
lemma disj[simp]: "Ifm bs (disj p q) = Ifm bs (Or p q)"
by (cases "p=T \<or> q=T",simp_all add: disj_def) (cases p,simp_all)
definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
- "imp p q \<equiv> (if (p = F \<or> q=T \<or> p=q) then T else if p=T then q else if q=F then not p
+ "imp p q = (if (p = F \<or> q=T \<or> p=q) then T else if p=T then q else if q=F then not p
else Imp p q)"
lemma imp[simp]: "Ifm bs (imp p q) = Ifm bs (Imp p q)"
by (cases "p=F \<or> q=T",simp_all add: imp_def)
definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
- "iff p q \<equiv> (if (p = q) then T else if (p = NOT q \<or> NOT p = q) then F else
+ "iff p q = (if (p = q) then T else if (p = NOT q \<or> NOT p = q) then F else
if p=F then not q else if q=F then not p else if p=T then q else if q=T then p else
Iff p q)"
lemma iff[simp]: "Ifm bs (iff p q) = Ifm bs (Iff p q)"
@@ -236,57 +219,54 @@
using trivNOT
by (simp_all add: iff_def, cases p, auto)
(* Quantifier freeness *)
-consts qfree:: "fm \<Rightarrow> bool"
-recdef qfree "measure size"
+fun qfree:: "fm \<Rightarrow> bool" where
"qfree (E p) = False"
- "qfree (A p) = False"
- "qfree (NOT p) = qfree p"
- "qfree (And p q) = (qfree p \<and> qfree q)"
- "qfree (Or p q) = (qfree p \<and> qfree q)"
- "qfree (Imp p q) = (qfree p \<and> qfree q)"
- "qfree (Iff p q) = (qfree p \<and> qfree q)"
- "qfree p = True"
+| "qfree (A p) = False"
+| "qfree (NOT p) = qfree p"
+| "qfree (And p q) = (qfree p \<and> qfree q)"
+| "qfree (Or p q) = (qfree p \<and> qfree q)"
+| "qfree (Imp p q) = (qfree p \<and> qfree q)"
+| "qfree (Iff p q) = (qfree p \<and> qfree q)"
+| "qfree p = True"
(* Boundedness and substitution *)
-consts
- numbound0:: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *)
- bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *)
-primrec
+primrec numbound0:: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *) where
"numbound0 (C c) = True"
- "numbound0 (Bound n) = (n>0)"
- "numbound0 (CN n c a) = (n\<noteq>0 \<and> numbound0 a)"
- "numbound0 (Neg a) = numbound0 a"
- "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"
- "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)"
- "numbound0 (Mul i a) = numbound0 a"
+| "numbound0 (Bound n) = (n>0)"
+| "numbound0 (CN n c a) = (n\<noteq>0 \<and> numbound0 a)"
+| "numbound0 (Neg a) = numbound0 a"
+| "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"
+| "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)"
+| "numbound0 (Mul i a) = numbound0 a"
+
lemma numbound0_I:
assumes nb: "numbound0 a"
shows "Inum (b#bs) a = Inum (b'#bs) a"
using nb
-by (induct a rule: numbound0.induct,auto simp add: nth_pos2)
+by (induct a) (simp_all add: nth_pos2)
-primrec
+primrec bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *) where
"bound0 T = True"
- "bound0 F = True"
- "bound0 (Lt a) = numbound0 a"
- "bound0 (Le a) = numbound0 a"
- "bound0 (Gt a) = numbound0 a"
- "bound0 (Ge a) = numbound0 a"
- "bound0 (Eq a) = numbound0 a"
- "bound0 (NEq a) = numbound0 a"
- "bound0 (NOT p) = bound0 p"
- "bound0 (And p q) = (bound0 p \<and> bound0 q)"
- "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
- "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
- "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
- "bound0 (E p) = False"
- "bound0 (A p) = False"
+| "bound0 F = True"
+| "bound0 (Lt a) = numbound0 a"
+| "bound0 (Le a) = numbound0 a"
+| "bound0 (Gt a) = numbound0 a"
+| "bound0 (Ge a) = numbound0 a"
+| "bound0 (Eq a) = numbound0 a"
+| "bound0 (NEq a) = numbound0 a"
+| "bound0 (NOT p) = bound0 p"
+| "bound0 (And p q) = (bound0 p \<and> bound0 q)"
+| "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
+| "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
+| "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
+| "bound0 (E p) = False"
+| "bound0 (A p) = False"
lemma bound0_I:
assumes bp: "bound0 p"
shows "Ifm (b#bs) p = Ifm (b'#bs) p"
using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]
-by (induct p rule: bound0.induct) (auto simp add: nth_pos2)
+by (induct p) (auto simp add: nth_pos2)
lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)"
by (cases p, auto)
@@ -314,32 +294,28 @@
lemma iff_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (iff p q)"
using iff_def by (unfold iff_def,cases "p=q", auto)
-consts
- decrnum:: "num \<Rightarrow> num"
- decr :: "fm \<Rightarrow> fm"
-
-recdef decrnum "measure size"
+fun decrnum:: "num \<Rightarrow> num" where
"decrnum (Bound n) = Bound (n - 1)"
- "decrnum (Neg a) = Neg (decrnum a)"
- "decrnum (Add a b) = Add (decrnum a) (decrnum b)"
- "decrnum (Sub a b) = Sub (decrnum a) (decrnum b)"
- "decrnum (Mul c a) = Mul c (decrnum a)"
- "decrnum (CN n c a) = CN (n - 1) c (decrnum a)"
- "decrnum a = a"
+| "decrnum (Neg a) = Neg (decrnum a)"
+| "decrnum (Add a b) = Add (decrnum a) (decrnum b)"
+| "decrnum (Sub a b) = Sub (decrnum a) (decrnum b)"
+| "decrnum (Mul c a) = Mul c (decrnum a)"
+| "decrnum (CN n c a) = CN (n - 1) c (decrnum a)"
+| "decrnum a = a"
-recdef decr "measure size"
+fun decr :: "fm \<Rightarrow> fm" where
"decr (Lt a) = Lt (decrnum a)"
- "decr (Le a) = Le (decrnum a)"
- "decr (Gt a) = Gt (decrnum a)"
- "decr (Ge a) = Ge (decrnum a)"
- "decr (Eq a) = Eq (decrnum a)"
- "decr (NEq a) = NEq (decrnum a)"
- "decr (NOT p) = NOT (decr p)"
- "decr (And p q) = conj (decr p) (decr q)"
- "decr (Or p q) = disj (decr p) (decr q)"
- "decr (Imp p q) = imp (decr p) (decr q)"
- "decr (Iff p q) = iff (decr p) (decr q)"
- "decr p = p"
+| "decr (Le a) = Le (decrnum a)"
+| "decr (Gt a) = Gt (decrnum a)"
+| "decr (Ge a) = Ge (decrnum a)"
+| "decr (Eq a) = Eq (decrnum a)"
+| "decr (NEq a) = NEq (decrnum a)"
+| "decr (NOT p) = NOT (decr p)"
+| "decr (And p q) = conj (decr p) (decr q)"
+| "decr (Or p q) = disj (decr p) (decr q)"
+| "decr (Imp p q) = imp (decr p) (decr q)"
+| "decr (Iff p q) = iff (decr p) (decr q)"
+| "decr p = p"
lemma decrnum: assumes nb: "numbound0 t"
shows "Inum (x#bs) t = Inum bs (decrnum t)"
@@ -353,27 +329,25 @@
lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"
by (induct p, simp_all)
-consts
- isatom :: "fm \<Rightarrow> bool" (* test for atomicity *)
-recdef isatom "measure size"
+fun isatom :: "fm \<Rightarrow> bool" (* test for atomicity *) where
"isatom T = True"
- "isatom F = True"
- "isatom (Lt a) = True"
- "isatom (Le a) = True"
- "isatom (Gt a) = True"
- "isatom (Ge a) = True"
- "isatom (Eq a) = True"
- "isatom (NEq a) = True"
- "isatom p = False"
+| "isatom F = True"
+| "isatom (Lt a) = True"
+| "isatom (Le a) = True"
+| "isatom (Gt a) = True"
+| "isatom (Ge a) = True"
+| "isatom (Eq a) = True"
+| "isatom (NEq a) = True"
+| "isatom p = False"
lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p"
by (induct p, simp_all)
definition djf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm" where
- "djf f p q \<equiv> (if q=T then T else if q=F then f p else
+ "djf f p q = (if q=T then T else if q=F then f p else
(let fp = f p in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q))"
definition evaldjf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm" where
- "evaldjf f ps \<equiv> foldr (djf f) ps F"
+ "evaldjf f ps = foldr (djf f) ps F"
lemma djf_Or: "Ifm bs (djf f p q) = Ifm bs (Or (f p) q)"
by (cases "q=T", simp add: djf_def,cases "q=F",simp add: djf_def)
@@ -399,11 +373,10 @@
shows "qfree (evaldjf f xs)"
using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
-consts disjuncts :: "fm \<Rightarrow> fm list"
-recdef disjuncts "measure size"
- "disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)"
- "disjuncts F = []"
- "disjuncts p = [p]"
+fun disjuncts :: "fm \<Rightarrow> fm list" where
+ "disjuncts (Or p q) = disjuncts p @ disjuncts q"
+| "disjuncts F = []"
+| "disjuncts p = [p]"
lemma disjuncts: "(\<exists> q\<in> set (disjuncts p). Ifm bs q) = Ifm bs p"
by(induct p rule: disjuncts.induct, auto)
@@ -424,7 +397,7 @@
qed
definition DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm" where
- "DJ f p \<equiv> evaldjf f (disjuncts p)"
+ "DJ f p = evaldjf f (disjuncts p)"
lemma DJ: assumes fdj: "\<forall> p q. Ifm bs (f (Or p q)) = Ifm bs (Or (f p) (f q))"
and fF: "f F = F"
@@ -462,40 +435,37 @@
finally show "qfree (DJ qe p) \<and> Ifm bs (DJ qe p) = Ifm bs (E p)" using qfth by blast
qed
(* Simplification *)
-consts
- numgcd :: "num \<Rightarrow> int"
- numgcdh:: "num \<Rightarrow> int \<Rightarrow> int"
- reducecoeffh:: "num \<Rightarrow> int \<Rightarrow> num"
- reducecoeff :: "num \<Rightarrow> num"
- dvdnumcoeff:: "num \<Rightarrow> int \<Rightarrow> bool"
-consts maxcoeff:: "num \<Rightarrow> int"
-recdef maxcoeff "measure size"
+
+fun maxcoeff:: "num \<Rightarrow> int" where
"maxcoeff (C i) = abs i"
- "maxcoeff (CN n c t) = max (abs c) (maxcoeff t)"
- "maxcoeff t = 1"
+| "maxcoeff (CN n c t) = max (abs c) (maxcoeff t)"
+| "maxcoeff t = 1"
lemma maxcoeff_pos: "maxcoeff t \<ge> 0"
by (induct t rule: maxcoeff.induct, auto)
-recdef numgcdh "measure size"
+fun numgcdh:: "num \<Rightarrow> int \<Rightarrow> int" where
"numgcdh (C i) = (\<lambda>g. gcd i g)"
- "numgcdh (CN n c t) = (\<lambda>g. gcd c (numgcdh t g))"
- "numgcdh t = (\<lambda>g. 1)"
-defs numgcd_def [code]: "numgcd t \<equiv> numgcdh t (maxcoeff t)"
+| "numgcdh (CN n c t) = (\<lambda>g. gcd c (numgcdh t g))"
+| "numgcdh t = (\<lambda>g. 1)"
+
+definition numgcd :: "num \<Rightarrow> int" where
+ "numgcd t = numgcdh t (maxcoeff t)"
-recdef reducecoeffh "measure size"
+fun reducecoeffh:: "num \<Rightarrow> int \<Rightarrow> num" where
"reducecoeffh (C i) = (\<lambda> g. C (i div g))"
- "reducecoeffh (CN n c t) = (\<lambda> g. CN n (c div g) (reducecoeffh t g))"
- "reducecoeffh t = (\<lambda>g. t)"
+| "reducecoeffh (CN n c t) = (\<lambda> g. CN n (c div g) (reducecoeffh t g))"
+| "reducecoeffh t = (\<lambda>g. t)"
-defs reducecoeff_def: "reducecoeff t \<equiv>
+definition reducecoeff :: "num \<Rightarrow> num" where
+ "reducecoeff t =
(let g = numgcd t in
if g = 0 then C 0 else if g=1 then t else reducecoeffh t g)"
-recdef dvdnumcoeff "measure size"
+fun dvdnumcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" where
"dvdnumcoeff (C i) = (\<lambda> g. g dvd i)"
- "dvdnumcoeff (CN n c t) = (\<lambda> g. g dvd c \<and> (dvdnumcoeff t g))"
- "dvdnumcoeff t = (\<lambda>g. False)"
+| "dvdnumcoeff (CN n c t) = (\<lambda> g. g dvd c \<and> (dvdnumcoeff t g))"
+| "dvdnumcoeff t = (\<lambda>g. False)"
lemma dvdnumcoeff_trans:
assumes gdg: "g dvd g'" and dgt':"dvdnumcoeff t g'"
@@ -534,11 +504,11 @@
from gp have gnz: "g \<noteq> 0" by simp
from prems show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps)
qed (auto simp add: numgcd_def gp)
-consts ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool"
-recdef ismaxcoeff "measure size"
+
+fun ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" where
"ismaxcoeff (C i) = (\<lambda> x. abs i \<le> x)"
- "ismaxcoeff (CN n c t) = (\<lambda>x. abs c \<le> x \<and> (ismaxcoeff t x))"
- "ismaxcoeff t = (\<lambda>x. True)"
+| "ismaxcoeff (CN n c t) = (\<lambda>x. abs c \<le> x \<and> (ismaxcoeff t x))"
+| "ismaxcoeff t = (\<lambda>x. True)"
lemma ismaxcoeff_mono: "ismaxcoeff t c \<Longrightarrow> c \<le> c' \<Longrightarrow> ismaxcoeff t c'"
by (induct t rule: ismaxcoeff.induct, auto)
@@ -618,9 +588,8 @@
using reducecoeffh_numbound0 by (simp add: reducecoeff_def Let_def)
consts
- simpnum:: "num \<Rightarrow> num"
numadd:: "num \<times> num \<Rightarrow> num"
- nummul:: "num \<Rightarrow> int \<Rightarrow> num"
+
recdef numadd "measure (\<lambda> (t,s). size t + size s)"
"numadd (CN n1 c1 r1,CN n2 c2 r2) =
(if n1=n2 then
@@ -642,10 +611,10 @@
lemma numadd_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
by (induct t s rule: numadd.induct, auto simp add: Let_def)
-recdef nummul "measure size"
+fun nummul:: "num \<Rightarrow> int \<Rightarrow> num" where
"nummul (C j) = (\<lambda> i. C (i*j))"
- "nummul (CN n c a) = (\<lambda> i. CN n (i*c) (nummul a i))"
- "nummul t = (\<lambda> i. Mul i t)"
+| "nummul (CN n c a) = (\<lambda> i. CN n (i*c) (nummul a i))"
+| "nummul t = (\<lambda> i. Mul i t)"
lemma nummul[simp]: "\<And> i. Inum bs (nummul t i) = Inum bs (Mul i t)"
by (induct t rule: nummul.induct, auto simp add: algebra_simps)
@@ -654,10 +623,10 @@
by (induct t rule: nummul.induct, auto )
definition numneg :: "num \<Rightarrow> num" where
- "numneg t \<equiv> nummul t (- 1)"
+ "numneg t = nummul t (- 1)"
definition numsub :: "num \<Rightarrow> num \<Rightarrow> num" where
- "numsub s t \<equiv> (if s = t then C 0 else numadd (s,numneg t))"
+ "numsub s t = (if s = t then C 0 else numadd (s,numneg t))"
lemma numneg[simp]: "Inum bs (numneg t) = Inum bs (Neg t)"
using numneg_def by simp
@@ -671,27 +640,26 @@
lemma numsub_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numsub t s)"
using numsub_def by simp
-recdef simpnum "measure size"
+primrec simpnum:: "num \<Rightarrow> num" where
"simpnum (C j) = C j"
- "simpnum (Bound n) = CN n 1 (C 0)"
- "simpnum (Neg t) = numneg (simpnum t)"
- "simpnum (Add t s) = numadd (simpnum t,simpnum s)"
- "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)"
- "simpnum (Mul i t) = (if i = 0 then (C 0) else nummul (simpnum t) i)"
- "simpnum (CN n c t) = (if c = 0 then simpnum t else numadd (CN n c (C 0),simpnum t))"
+| "simpnum (Bound n) = CN n 1 (C 0)"
+| "simpnum (Neg t) = numneg (simpnum t)"
+| "simpnum (Add t s) = numadd (simpnum t,simpnum s)"
+| "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)"
+| "simpnum (Mul i t) = (if i = 0 then (C 0) else nummul (simpnum t) i)"
+| "simpnum (CN n c t) = (if c = 0 then simpnum t else numadd (CN n c (C 0),simpnum t))"
lemma simpnum_ci[simp]: "Inum bs (simpnum t) = Inum bs t"
-by (induct t rule: simpnum.induct, auto simp add: numneg numadd numsub nummul)
+by (induct t) simp_all
lemma simpnum_numbound0[simp]:
"numbound0 t \<Longrightarrow> numbound0 (simpnum t)"
-by (induct t rule: simpnum.induct, auto)
+by (induct t) simp_all
-consts nozerocoeff:: "num \<Rightarrow> bool"
-recdef nozerocoeff "measure size"
+fun nozerocoeff:: "num \<Rightarrow> bool" where
"nozerocoeff (C c) = True"
- "nozerocoeff (CN n c t) = (c\<noteq>0 \<and> nozerocoeff t)"
- "nozerocoeff t = True"
+| "nozerocoeff (CN n c t) = (c\<noteq>0 \<and> nozerocoeff t)"
+| "nozerocoeff t = True"
lemma numadd_nz : "nozerocoeff a \<Longrightarrow> nozerocoeff b \<Longrightarrow> nozerocoeff (numadd (a,b))"
by (induct a b rule: numadd.induct,auto simp add: Let_def)
@@ -706,7 +674,7 @@
by (simp add: numsub_def numneg_nz numadd_nz)
lemma simpnum_nz: "nozerocoeff (simpnum t)"
-by(induct t rule: simpnum.induct, auto simp add: numadd_nz numneg_nz numsub_nz nummul_nz)
+by(induct t) (simp_all add: numadd_nz numneg_nz numsub_nz nummul_nz)
lemma maxcoeff_nz: "nozerocoeff t \<Longrightarrow> maxcoeff t = 0 \<Longrightarrow> t = C 0"
proof (induct t rule: maxcoeff.induct)
@@ -725,7 +693,7 @@
qed
definition simp_num_pair :: "(num \<times> int) \<Rightarrow> num \<times> int" where
- "simp_num_pair \<equiv> (\<lambda> (t,n). (if n = 0 then (C 0, 0) else
+ "simp_num_pair = (\<lambda> (t,n). (if n = 0 then (C 0, 0) else
(let t' = simpnum t ; g = numgcd t' in
if g > 1 then (let g' = gcd n g in
if g' = 1 then (t',n)
@@ -800,21 +768,20 @@
ultimately show ?thesis by blast
qed
-consts simpfm :: "fm \<Rightarrow> fm"
-recdef simpfm "measure fmsize"
+fun simpfm :: "fm \<Rightarrow> fm" where
"simpfm (And p q) = conj (simpfm p) (simpfm q)"
- "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
- "simpfm (Imp p q) = imp (simpfm p) (simpfm q)"
- "simpfm (Iff p q) = iff (simpfm p) (simpfm q)"
- "simpfm (NOT p) = not (simpfm p)"
- "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v < 0) then T else F
+| "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
+| "simpfm (Imp p q) = imp (simpfm p) (simpfm q)"
+| "simpfm (Iff p q) = iff (simpfm p) (simpfm q)"
+| "simpfm (NOT p) = not (simpfm p)"
+| "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v < 0) then T else F
| _ \<Rightarrow> Lt a')"
- "simpfm (Le a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<le> 0) then T else F | _ \<Rightarrow> Le a')"
- "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v > 0) then T else F | _ \<Rightarrow> Gt a')"
- "simpfm (Ge a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<ge> 0) then T else F | _ \<Rightarrow> Ge a')"
- "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v = 0) then T else F | _ \<Rightarrow> Eq a')"
- "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<noteq> 0) then T else F | _ \<Rightarrow> NEq a')"
- "simpfm p = p"
+| "simpfm (Le a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<le> 0) then T else F | _ \<Rightarrow> Le a')"
+| "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v > 0) then T else F | _ \<Rightarrow> Gt a')"
+| "simpfm (Ge a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<ge> 0) then T else F | _ \<Rightarrow> Ge a')"
+| "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v = 0) then T else F | _ \<Rightarrow> Eq a')"
+| "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<noteq> 0) then T else F | _ \<Rightarrow> NEq a')"
+| "simpfm p = p"
lemma simpfm: "Ifm bs (simpfm p) = Ifm bs p"
proof(induct p rule: simpfm.induct)
case (6 a) let ?sa = "simpnum a" from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
@@ -921,16 +888,17 @@
by (induct p rule: prep.induct, auto)
(* Generic quantifier elimination *)
-consts qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
-recdef qelim "measure fmsize"
+function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm" where
"qelim (E p) = (\<lambda> qe. DJ qe (qelim p qe))"
- "qelim (A p) = (\<lambda> qe. not (qe ((qelim (NOT p) qe))))"
- "qelim (NOT p) = (\<lambda> qe. not (qelim p qe))"
- "qelim (And p q) = (\<lambda> qe. conj (qelim p qe) (qelim q qe))"
- "qelim (Or p q) = (\<lambda> qe. disj (qelim p qe) (qelim q qe))"
- "qelim (Imp p q) = (\<lambda> qe. imp (qelim p qe) (qelim q qe))"
- "qelim (Iff p q) = (\<lambda> qe. iff (qelim p qe) (qelim q qe))"
- "qelim p = (\<lambda> y. simpfm p)"
+| "qelim (A p) = (\<lambda> qe. not (qe ((qelim (NOT p) qe))))"
+| "qelim (NOT p) = (\<lambda> qe. not (qelim p qe))"
+| "qelim (And p q) = (\<lambda> qe. conj (qelim p qe) (qelim q qe))"
+| "qelim (Or p q) = (\<lambda> qe. disj (qelim p qe) (qelim q qe))"
+| "qelim (Imp p q) = (\<lambda> qe. imp (qelim p qe) (qelim q qe))"
+| "qelim (Iff p q) = (\<lambda> qe. iff (qelim p qe) (qelim q qe))"
+| "qelim p = (\<lambda> y. simpfm p)"
+by pat_completeness auto
+termination qelim by (relation "measure fmsize") simp_all
lemma qelim_ci:
assumes qe_inv: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bs (qe p) = Ifm bs (E p))"
@@ -940,56 +908,53 @@
(auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf
simpfm simpfm_qf simp del: simpfm.simps)
-consts
- plusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of +\<infinity>*)
- minusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of -\<infinity>*)
-recdef minusinf "measure size"
+fun minusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of -\<infinity>*) where
"minusinf (And p q) = conj (minusinf p) (minusinf q)"
- "minusinf (Or p q) = disj (minusinf p) (minusinf q)"
- "minusinf (Eq (CN 0 c e)) = F"
- "minusinf (NEq (CN 0 c e)) = T"
- "minusinf (Lt (CN 0 c e)) = T"
- "minusinf (Le (CN 0 c e)) = T"
- "minusinf (Gt (CN 0 c e)) = F"
- "minusinf (Ge (CN 0 c e)) = F"
- "minusinf p = p"
+| "minusinf (Or p q) = disj (minusinf p) (minusinf q)"
+| "minusinf (Eq (CN 0 c e)) = F"
+| "minusinf (NEq (CN 0 c e)) = T"
+| "minusinf (Lt (CN 0 c e)) = T"
+| "minusinf (Le (CN 0 c e)) = T"
+| "minusinf (Gt (CN 0 c e)) = F"
+| "minusinf (Ge (CN 0 c e)) = F"
+| "minusinf p = p"
-recdef plusinf "measure size"
+fun plusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of +\<infinity>*) where
"plusinf (And p q) = conj (plusinf p) (plusinf q)"
- "plusinf (Or p q) = disj (plusinf p) (plusinf q)"
- "plusinf (Eq (CN 0 c e)) = F"
- "plusinf (NEq (CN 0 c e)) = T"
- "plusinf (Lt (CN 0 c e)) = F"
- "plusinf (Le (CN 0 c e)) = F"
- "plusinf (Gt (CN 0 c e)) = T"
- "plusinf (Ge (CN 0 c e)) = T"
- "plusinf p = p"
+| "plusinf (Or p q) = disj (plusinf p) (plusinf q)"
+| "plusinf (Eq (CN 0 c e)) = F"
+| "plusinf (NEq (CN 0 c e)) = T"
+| "plusinf (Lt (CN 0 c e)) = F"
+| "plusinf (Le (CN 0 c e)) = F"
+| "plusinf (Gt (CN 0 c e)) = T"
+| "plusinf (Ge (CN 0 c e)) = T"
+| "plusinf p = p"
-consts
- isrlfm :: "fm \<Rightarrow> bool" (* Linearity test for fm *)
-recdef isrlfm "measure size"
+fun isrlfm :: "fm \<Rightarrow> bool" (* Linearity test for fm *) where
"isrlfm (And p q) = (isrlfm p \<and> isrlfm q)"
- "isrlfm (Or p q) = (isrlfm p \<and> isrlfm q)"
- "isrlfm (Eq (CN 0 c e)) = (c>0 \<and> numbound0 e)"
- "isrlfm (NEq (CN 0 c e)) = (c>0 \<and> numbound0 e)"
- "isrlfm (Lt (CN 0 c e)) = (c>0 \<and> numbound0 e)"
- "isrlfm (Le (CN 0 c e)) = (c>0 \<and> numbound0 e)"
- "isrlfm (Gt (CN 0 c e)) = (c>0 \<and> numbound0 e)"
- "isrlfm (Ge (CN 0 c e)) = (c>0 \<and> numbound0 e)"
- "isrlfm p = (isatom p \<and> (bound0 p))"
+| "isrlfm (Or p q) = (isrlfm p \<and> isrlfm q)"
+| "isrlfm (Eq (CN 0 c e)) = (c>0 \<and> numbound0 e)"
+| "isrlfm (NEq (CN 0 c e)) = (c>0 \<and> numbound0 e)"
+| "isrlfm (Lt (CN 0 c e)) = (c>0 \<and> numbound0 e)"
+| "isrlfm (Le (CN 0 c e)) = (c>0 \<and> numbound0 e)"
+| "isrlfm (Gt (CN 0 c e)) = (c>0 \<and> numbound0 e)"
+| "isrlfm (Ge (CN 0 c e)) = (c>0 \<and> numbound0 e)"
+| "isrlfm p = (isatom p \<and> (bound0 p))"
(* splits the bounded from the unbounded part*)
-consts rsplit0 :: "num \<Rightarrow> int \<times> num"
-recdef rsplit0 "measure num_size"
+function (sequential) rsplit0 :: "num \<Rightarrow> int \<times> num" where
"rsplit0 (Bound 0) = (1,C 0)"
- "rsplit0 (Add a b) = (let (ca,ta) = rsplit0 a ; (cb,tb) = rsplit0 b
+| "rsplit0 (Add a b) = (let (ca,ta) = rsplit0 a ; (cb,tb) = rsplit0 b
in (ca+cb, Add ta tb))"
- "rsplit0 (Sub a b) = rsplit0 (Add a (Neg b))"
- "rsplit0 (Neg a) = (let (c,t) = rsplit0 a in (-c,Neg t))"
- "rsplit0 (Mul c a) = (let (ca,ta) = rsplit0 a in (c*ca,Mul c ta))"
- "rsplit0 (CN 0 c a) = (let (ca,ta) = rsplit0 a in (c+ca,ta))"
- "rsplit0 (CN n c a) = (let (ca,ta) = rsplit0 a in (ca,CN n c ta))"
- "rsplit0 t = (0,t)"
+| "rsplit0 (Sub a b) = rsplit0 (Add a (Neg b))"
+| "rsplit0 (Neg a) = (let (c,t) = rsplit0 a in (-c,Neg t))"
+| "rsplit0 (Mul c a) = (let (ca,ta) = rsplit0 a in (c*ca,Mul c ta))"
+| "rsplit0 (CN 0 c a) = (let (ca,ta) = rsplit0 a in (c+ca,ta))"
+| "rsplit0 (CN n c a) = (let (ca,ta) = rsplit0 a in (ca,CN n c ta))"
+| "rsplit0 t = (0,t)"
+by pat_completeness auto
+termination rsplit0 by (relation "measure num_size") simp_all
+
lemma rsplit0:
shows "Inum bs ((split (CN 0)) (rsplit0 t)) = Inum bs t \<and> numbound0 (snd (rsplit0 t))"
proof (induct t rule: rsplit0.induct)
@@ -998,13 +963,13 @@
let ?ca = "fst ?sa" let ?cb = "fst ?sb"
let ?ta = "snd ?sa" let ?tb = "snd ?sb"
from prems have nb: "numbound0 (snd(rsplit0 (Add a b)))"
- by(cases "rsplit0 a",auto simp add: Let_def split_def)
+ by (cases "rsplit0 a") (auto simp add: Let_def split_def)
have "Inum bs ((split (CN 0)) (rsplit0 (Add a b))) =
Inum bs ((split (CN 0)) ?sa)+Inum bs ((split (CN 0)) ?sb)"
by (simp add: Let_def split_def algebra_simps)
- also have "\<dots> = Inum bs a + Inum bs b" using prems by (cases "rsplit0 a", simp_all)
+ also have "\<dots> = Inum bs a + Inum bs b" using prems by (cases "rsplit0 a") auto
finally show ?case using nb by simp
-qed(auto simp add: Let_def split_def algebra_simps , simp add: right_distrib[symmetric])
+qed (auto simp add: Let_def split_def algebra_simps , simp add: right_distrib[symmetric])
(* Linearize a formula*)
definition
@@ -1780,9 +1745,9 @@
(* Implement the right hand side of Ferrante and Rackoff's Theorem. *)
definition ferrack :: "fm \<Rightarrow> fm" where
- "ferrack p \<equiv> (let p' = rlfm (simpfm p); mp = minusinf p'; pp = plusinf p'
+ "ferrack p = (let p' = rlfm (simpfm p); mp = minusinf p'; pp = plusinf p'
in if (mp = T \<or> pp = T) then T else
- (let U = remdps(map simp_num_pair
+ (let U = remdups(map simp_num_pair
(map (\<lambda> ((t,n),(s,m)). (Add (Mul m t) (Mul n s) , 2*n*m))
(alluopairs (uset p'))))
in decr (disj mp (disj pp (evaldjf (simpfm o (usubst p')) U)))))"
@@ -1911,7 +1876,7 @@
let ?g = "\<lambda> ((t,n),(s,m)). (Add (Mul m t) (Mul n s) , 2*n*m)"
let ?S = "map ?g ?Up"
let ?SS = "map simp_num_pair ?S"
- let ?Y = "remdps ?SS"
+ let ?Y = "remdups ?SS"
let ?f= "(\<lambda> (t,n). ?N t / real n)"
let ?h = "\<lambda> ((t,n),(s,m)). (?N t/real n + ?N s/ real m) /2"
let ?F = "\<lambda> p. \<exists> a \<in> set (uset p). \<exists> b \<in> set (uset p). ?I x (usubst p (?g(a,b)))"
@@ -1996,49 +1961,53 @@
"ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0)))
(E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))"
-code_reserved SML oo
-
ML {* @{code ferrack_test} () *}
oracle linr_oracle = {*
let
-fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t
- of NONE => error "Variable not found in the list!"
- | SOME n => @{code Bound} n)
+fun num_of_term vs (Free vT) = @{code Bound} (find_index (fn vT' => vT = vT') vs)
| num_of_term vs @{term "real (0::int)"} = @{code C} 0
| num_of_term vs @{term "real (1::int)"} = @{code C} 1
| num_of_term vs @{term "0::real"} = @{code C} 0
| num_of_term vs @{term "1::real"} = @{code C} 1
| num_of_term vs (Bound i) = @{code Bound} i
| num_of_term vs (@{term "uminus :: real \<Rightarrow> real"} $ t') = @{code Neg} (num_of_term vs t')
- | num_of_term vs (@{term "op + :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = @{code Add} (num_of_term vs t1, num_of_term vs t2)
- | num_of_term vs (@{term "op - :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = @{code Sub} (num_of_term vs t1, num_of_term vs t2)
- | num_of_term vs (@{term "op * :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = (case (num_of_term vs t1)
+ | num_of_term vs (@{term "op + :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
+ @{code Add} (num_of_term vs t1, num_of_term vs t2)
+ | num_of_term vs (@{term "op - :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
+ @{code Sub} (num_of_term vs t1, num_of_term vs t2)
+ | num_of_term vs (@{term "op * :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = (case num_of_term vs t1
of @{code C} i => @{code Mul} (i, num_of_term vs t2)
- | _ => error "num_of_term: unsupported Multiplication")
- | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "number_of :: int \<Rightarrow> int"} $ t')) = @{code C} (HOLogic.dest_numeral t')
- | num_of_term vs (@{term "number_of :: int \<Rightarrow> real"} $ t') = @{code C} (HOLogic.dest_numeral t')
- | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term @{context} t);
+ | _ => error "num_of_term: unsupported multiplication")
+ | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "number_of :: int \<Rightarrow> int"} $ t')) =
+ @{code C} (HOLogic.dest_numeral t')
+ | num_of_term vs (@{term "number_of :: int \<Rightarrow> real"} $ t') =
+ @{code C} (HOLogic.dest_numeral t')
+ | num_of_term vs t = error ("num_of_term: unknown term");
fun fm_of_term vs @{term True} = @{code T}
| fm_of_term vs @{term False} = @{code F}
- | fm_of_term vs (@{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = @{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
- | fm_of_term vs (@{term "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = @{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
- | fm_of_term vs (@{term "op = :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
- | fm_of_term vs (@{term "op \<longleftrightarrow> :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) = @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
+ | fm_of_term vs (@{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) =
+ @{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
+ | fm_of_term vs (@{term "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) =
+ @{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
+ | fm_of_term vs (@{term "op = :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) =
+ @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
+ | fm_of_term vs (@{term "op \<longleftrightarrow> :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
+ @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "op &"} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "op -->"} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t')
| fm_of_term vs (Const ("Ex", _) $ Abs (xn, xT, p)) =
- @{code E} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
+ @{code E} (fm_of_term (("", dummyT) :: vs) p)
| fm_of_term vs (Const ("All", _) $ Abs (xn, xT, p)) =
- @{code A} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
+ @{code A} (fm_of_term (("", dummyT) :: vs) p)
| fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
fun term_of_num vs (@{code C} i) = @{term "real :: int \<Rightarrow> real"} $ HOLogic.mk_number HOLogic.intT i
- | term_of_num vs (@{code Bound} n) = fst (the (find_first (fn (_, m) => n = m) vs))
+ | term_of_num vs (@{code Bound} n) = Free (nth vs n)
| term_of_num vs (@{code Neg} t') = @{term "uminus :: real \<Rightarrow> real"} $ term_of_num vs t'
| term_of_num vs (@{code Add} (t1, t2)) = @{term "op + :: real \<Rightarrow> real \<Rightarrow> real"} $
term_of_num vs t1 $ term_of_num vs t2
@@ -2066,17 +2035,13 @@
| term_of_fm vs (@{code Or} (t1, t2)) = HOLogic.disj $ term_of_fm vs t1 $ term_of_fm vs t2
| term_of_fm vs (@{code Imp} (t1, t2)) = HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2
| term_of_fm vs (@{code Iff} (t1, t2)) = @{term "op \<longleftrightarrow> :: bool \<Rightarrow> bool \<Rightarrow> bool"} $
- term_of_fm vs t1 $ term_of_fm vs t2
- | term_of_fm vs _ = error "If this is raised, Isabelle/HOL or generate_code is inconsistent.";
+ term_of_fm vs t1 $ term_of_fm vs t2;
-in fn ct =>
+in fn (ctxt, t) =>
let
- val thy = Thm.theory_of_cterm ct;
- val t = Thm.term_of ct;
- val fs = OldTerm.term_frees t;
- val vs = map_index swap fs;
- val res = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (@{code linrqe} (fm_of_term vs t))));
- in Thm.cterm_of thy res end
+ val vs = Term.add_frees t [];
+ val t' = (term_of_fm vs o @{code linrqe} o fm_of_term vs) t;
+ in (Thm.cterm_of (ProofContext.theory_of ctxt) o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
end;
*}
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Wed May 12 15:25:02 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Wed May 12 15:25:23 2010 +0200
@@ -92,7 +92,7 @@
(* The result of the quantifier elimination *)
val (th, tac) = case prop_of pre_thm of
Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
- let val pth = linr_oracle (cterm_of thy (Pattern.eta_long [] t1))
+ let val pth = linr_oracle (ctxt, Pattern.eta_long [] t1)
in
(trace_msg ("calling procedure with term:\n" ^
Syntax.string_of_term ctxt t1);
--- a/src/HOL/List.thy Wed May 12 15:25:02 2010 +0200
+++ b/src/HOL/List.thy Wed May 12 15:25:23 2010 +0200
@@ -1529,6 +1529,14 @@
apply(simp add:list_update_append split:nat.splits)
done
+lemma last_map:
+ "xs \<noteq> [] \<Longrightarrow> last (map f xs) = f (last xs)"
+ by (cases xs rule: rev_cases) simp_all
+
+lemma map_butlast:
+ "map f (butlast xs) = butlast (map f xs)"
+ by (induct xs) simp_all
+
subsubsection {* @{text take} and @{text drop} *}
@@ -2910,6 +2918,14 @@
"remdups (remdups xs) = remdups xs"
by (induct xs) simp_all
+lemma distinct_butlast:
+ assumes "xs \<noteq> []" and "distinct xs"
+ shows "distinct (butlast xs)"
+proof -
+ from `xs \<noteq> []` obtain ys y where "xs = ys @ [y]" by (cases xs rule: rev_cases) auto
+ with `distinct xs` show ?thesis by simp
+qed
+
subsubsection {* @{const insert} *}
@@ -3605,6 +3621,18 @@
theorem sorted_sort[simp]: "sorted (sort xs)"
by(induct xs)(auto simp:sorted_insort)
+lemma sorted_butlast:
+ assumes "xs \<noteq> []" and "sorted xs"
+ shows "sorted (butlast xs)"
+proof -
+ from `xs \<noteq> []` obtain ys y where "xs = ys @ [y]" by (cases xs rule: rev_cases) auto
+ with `sorted xs` show ?thesis by (simp add: sorted_append)
+qed
+
+lemma insort_not_Nil [simp]:
+ "insort_key f a xs \<noteq> []"
+ by (induct xs) simp_all
+
lemma insort_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs"
by (cases xs) auto
--- a/src/HOL/Metis_Examples/BT.thy Wed May 12 15:25:02 2010 +0200
+++ b/src/HOL/Metis_Examples/BT.thy Wed May 12 15:25:23 2010 +0200
@@ -88,7 +88,7 @@
case Lf thus ?case by (metis reflect.simps(1))
next
case (Br a t1 t2) thus ?case
- by (metis normalizing.semiring_rules(24) n_nodes.simps(2) reflect.simps(2))
+ by (metis add_commute n_nodes.simps(2) reflect.simps(2))
qed
declare [[ atp_problem_prefix = "BT__depth_reflect" ]]
--- a/src/HOL/Metis_Examples/BigO.thy Wed May 12 15:25:02 2010 +0200
+++ b/src/HOL/Metis_Examples/BigO.thy Wed May 12 15:25:23 2010 +0200
@@ -41,7 +41,7 @@
fix c :: 'a and x :: 'b
assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> \<bar>x\<^isub>1\<bar>" by (metis abs_ge_zero)
- have F2: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
+ have F2: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1)
have F3: "\<forall>x\<^isub>1 x\<^isub>3. x\<^isub>3 \<le> \<bar>h x\<^isub>1\<bar> \<longrightarrow> x\<^isub>3 \<le> c * \<bar>f x\<^isub>1\<bar>" by (metis A1 order_trans)
have F4: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
by (metis abs_mult)
@@ -66,11 +66,11 @@
apply auto
apply (case_tac "c = 0", simp)
apply (rule_tac x = "1" in exI, simp)
- apply (rule_tac x = "abs c" in exI, auto);
+ apply (rule_tac x = "abs c" in exI, auto)
proof -
fix c :: 'a and x :: 'b
assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
- have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
+ have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1)
have F2: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
by (metis abs_mult)
have "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_mult_pos abs_one)
@@ -92,7 +92,7 @@
proof -
fix c :: 'a and x :: 'b
assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
- have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
+ have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1)
have F2: "\<forall>x\<^isub>3 x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> x\<^isub>1 \<longrightarrow> \<bar>x\<^isub>3 * x\<^isub>1\<bar> = \<bar>x\<^isub>3\<bar> * x\<^isub>1" by (metis abs_mult_pos)
hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_one)
hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^isub>3\<bar>" by (metis F2 A1 abs_ge_zero order_trans)
@@ -111,7 +111,7 @@
proof -
fix c :: 'a and x :: 'b
assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
- have "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
+ have "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1)
hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>"
by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one)
hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero abs_mult_pos abs_mult)
@@ -131,26 +131,26 @@
apply (rule conjI)
apply (rule mult_pos_pos)
apply (assumption)+
-(*sledgehammer*);
+(*sledgehammer*)
apply (rule allI)
apply (drule_tac x = "xa" in spec)+
- apply (subgoal_tac "ca * abs(f xa) <= ca * (c * abs(g xa))");
+ apply (subgoal_tac "ca * abs(f xa) <= ca * (c * abs(g xa))")
apply (erule order_trans)
apply (simp add: mult_ac)
apply (rule mult_left_mono, assumption)
- apply (rule order_less_imp_le, assumption);
+ apply (rule order_less_imp_le, assumption)
done
declare [[ atp_problem_prefix = "BigO__bigo_refl" ]]
lemma bigo_refl [intro]: "f : O(f)"
apply (auto simp add: bigo_def)
-by (metis normalizing.mul_1 order_refl)
+by (metis mult_1 order_refl)
declare [[ atp_problem_prefix = "BigO__bigo_zero" ]]
lemma bigo_zero: "0 : O(g)"
apply (auto simp add: bigo_def func_zero)
-by (metis normalizing.mul_0 order_refl)
+by (metis mult_zero_left order_refl)
lemma bigo_zero2: "O(%x.0) = {%x.0}"
apply (auto simp add: bigo_def)
@@ -237,7 +237,7 @@
apply (rule bigo_plus_subset)
apply (simp add: bigo_alt_def set_plus_def func_plus)
apply clarify
-(*sledgehammer*);
+(*sledgehammer*)
apply (rule_tac x = "max c ca" in exI)
apply (rule conjI)
apply (metis Orderings.less_max_iff_disj)
@@ -307,7 +307,7 @@
apply (auto simp add: diff_minus fun_Compl_def func_plus)
prefer 2
apply (drule_tac x = x in spec)+
- apply (metis add_right_mono normalizing.semiring_rules(24) diff_add_cancel diff_minus_eq_add le_less order_trans)
+ apply (metis add_right_mono add_commute diff_add_cancel diff_minus_eq_add le_less order_trans)
proof -
fix x :: 'a
assume "\<forall>x. lb x \<le> f x"
@@ -318,13 +318,13 @@
lemma bigo_abs: "(%x. abs(f x)) =o O(f)"
apply (unfold bigo_def)
apply auto
-by (metis normalizing.mul_1 order_refl)
+by (metis mult_1 order_refl)
declare [[ atp_problem_prefix = "BigO__bigo_abs2" ]]
lemma bigo_abs2: "f =o O(%x. abs(f x))"
apply (unfold bigo_def)
apply auto
-by (metis normalizing.mul_1 order_refl)
+by (metis mult_1 order_refl)
lemma bigo_abs3: "O(f) = O(%x. abs(f x))"
proof -
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed May 12 15:25:02 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed May 12 15:25:23 2010 +0200
@@ -1877,7 +1877,7 @@
using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_norm
unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_scaleR
apply (rule mult_left_le_imp_le[of "1 - u"])
- unfolding normalizing.mul_a using `u<1` by auto
+ unfolding mult_assoc[symmetric] using `u<1` by auto
thus "y \<in> s" using assms(1)[unfolded convex_def, rule_format, of "inverse(1 - u) *\<^sub>R (y - u *\<^sub>R x)" x "1 - u" u]
using as unfolding scaleR_scaleR by auto qed auto
thus "u *\<^sub>R x \<in> s - frontier s" using frontier_def and interior_subset by auto qed
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Wed May 12 15:25:02 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Wed May 12 15:25:23 2010 +0200
@@ -698,7 +698,8 @@
unfolding o_def apply(rule,rule has_derivative_lift_dot) using assms(3) by auto
then guess x .. note x=this
show ?thesis proof(cases "f a = f b")
- case False have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2" by(simp add:normalizing.semiring_rules)
+ case False
+ have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2" by(simp add: power2_eq_square)
also have "\<dots> = (f b - f a) \<bullet> (f b - f a)" unfolding power2_norm_eq_inner ..
also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)" using x unfolding inner_simps by auto
also have "\<dots> \<le> norm (f b - f a) * norm (f' x (b - a))" by(rule norm_cauchy_schwarz)
--- a/src/HOL/Multivariate_Analysis/Integration.thy Wed May 12 15:25:02 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed May 12 15:25:23 2010 +0200
@@ -2533,7 +2533,7 @@
show "content x \<ge> 0" unfolding as snd_conv * interval_doublesplit by(rule content_pos_le)
qed have **:"norm (1::real) \<le> 1" by auto note division_doublesplit[OF p'',unfolded interval_doublesplit]
note dsum_bound[OF this **,unfolded interval_doublesplit[THEN sym]]
- note this[unfolded real_scaleR_def real_norm_def normalizing.semiring_rules, of k c d] note le_less_trans[OF this d(2)]
+ note this[unfolded real_scaleR_def real_norm_def mult_1_right mult_1, of k c d] note le_less_trans[OF this d(2)]
from this[unfolded abs_of_nonneg[OF *]] show "(\<Sum>ka\<in>snd ` p. content (ka \<inter> {x. \<bar>x $ k - c\<bar> \<le> d})) < e"
apply(subst vsum_nonzero_image_lemma[of "snd ` p" content "{}", unfolded o_def,THEN sym])
apply(rule finite_imageI p' content_empty)+ unfolding forall_in_division[OF p'']
@@ -4723,7 +4723,7 @@
have "\<And>e sg dsa dia ig. norm(sg) \<le> dsa \<longrightarrow> abs(dsa - dia) < e / 2 \<longrightarrow> norm(sg - ig) < e / 2
\<longrightarrow> norm(ig) < dia + e"
proof safe case goal1 show ?case apply(rule le_less_trans[OF norm_triangle_sub[of ig sg]])
- apply(subst real_sum_of_halves[of e,THEN sym]) unfolding normalizing.add_a
+ apply(subst real_sum_of_halves[of e,THEN sym]) unfolding add_assoc[symmetric]
apply(rule add_le_less_mono) defer apply(subst norm_minus_commute,rule goal1)
apply(rule order_trans[OF goal1(1)]) using goal1(2) by arith
qed note norm=this[rule_format]
--- a/src/HOL/Probability/Lebesgue.thy Wed May 12 15:25:02 2010 +0200
+++ b/src/HOL/Probability/Lebesgue.thy Wed May 12 15:25:23 2010 +0200
@@ -939,17 +939,17 @@
proof safe
fix t assume t: "t \<in> space M"
{ fix m n :: nat assume "m \<le> n"
- hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding normalizing.mul_pwr by auto
+ hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding power_add[symmetric] by auto
have "real (natfloor (f t * 2^m) * natfloor (2^(n-m))) \<le> real (natfloor (f t * 2 ^ n))"
apply (subst *)
- apply (subst normalizing.mul_a)
+ apply (subst mult_assoc[symmetric])
apply (subst real_of_nat_le_iff)
apply (rule le_mult_natfloor)
using nonneg[OF t] by (auto intro!: mult_nonneg_nonneg)
hence "real (natfloor (f t * 2^m)) * 2^n \<le> real (natfloor (f t * 2^n)) * 2^m"
apply (subst *)
- apply (subst (3) normalizing.mul_c)
- apply (subst normalizing.mul_a)
+ apply (subst (3) mult_commute)
+ apply (subst mult_assoc[symmetric])
by (auto intro: mult_right_mono simp: natfloor_power real_of_nat_power[symmetric]) }
thus "incseq (\<lambda>n. ?u n t)" unfolding u_at_t[OF t] unfolding incseq_def
by (auto simp add: le_divide_eq divide_le_eq less_divide_eq)
--- a/src/HOL/Semiring_Normalization.thy Wed May 12 15:25:02 2010 +0200
+++ b/src/HOL/Semiring_Normalization.thy Wed May 12 15:25:23 2010 +0200
@@ -52,286 +52,155 @@
setup Semiring_Normalizer.setup
-locale normalizing_semiring =
- fixes add mul pwr r0 r1
- assumes add_a:"(add x (add y z) = add (add x y) z)"
- and add_c: "add x y = add y x" and add_0:"add r0 x = x"
- and mul_a:"mul x (mul y z) = mul (mul x y) z" and mul_c:"mul x y = mul y x"
- and mul_1:"mul r1 x = x" and mul_0:"mul r0 x = r0"
- and mul_d:"mul x (add y z) = add (mul x y) (mul x z)"
- and pwr_0:"pwr x 0 = r1" and pwr_Suc:"pwr x (Suc n) = mul x (pwr x n)"
-begin
-
-lemma mul_pwr:"mul (pwr x p) (pwr x q) = pwr x (p + q)"
-proof (induct p)
- case 0
- then show ?case by (auto simp add: pwr_0 mul_1)
-next
- case Suc
- from this [symmetric] show ?case
- by (auto simp add: pwr_Suc mul_1 mul_a)
-qed
-
-lemma pwr_mul: "pwr (mul x y) q = mul (pwr x q) (pwr y q)"
-proof (induct q arbitrary: x y, auto simp add:pwr_0 pwr_Suc mul_1)
- fix q x y
- assume "\<And>x y. pwr (mul x y) q = mul (pwr x q) (pwr y q)"
- have "mul (mul x y) (mul (pwr x q) (pwr y q)) = mul x (mul y (mul (pwr x q) (pwr y q)))"
- by (simp add: mul_a)
- also have "\<dots> = (mul (mul y (mul (pwr y q) (pwr x q))) x)" by (simp add: mul_c)
- also have "\<dots> = (mul (mul y (pwr y q)) (mul (pwr x q) x))" by (simp add: mul_a)
- finally show "mul (mul x y) (mul (pwr x q) (pwr y q)) =
- mul (mul x (pwr x q)) (mul y (pwr y q))" by (simp add: mul_c)
-qed
-
-lemma pwr_pwr: "pwr (pwr x p) q = pwr x (p * q)"
-proof (induct p arbitrary: q)
- case 0
- show ?case using pwr_Suc mul_1 pwr_0 by (induct q) auto
-next
- case Suc
- thus ?case by (auto simp add: mul_pwr [symmetric] pwr_mul pwr_Suc)
-qed
-
-lemma semiring_ops:
- shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)"
- and "TERM r0" and "TERM r1" .
+lemma (in comm_semiring_1) semiring_ops:
+ shows "TERM (x + y)" and "TERM (x * y)" and "TERM (x ^ n)"
+ and "TERM 0" and "TERM 1" .
-lemma semiring_rules:
- "add (mul a m) (mul b m) = mul (add a b) m"
- "add (mul a m) m = mul (add a r1) m"
- "add m (mul a m) = mul (add a r1) m"
- "add m m = mul (add r1 r1) m"
- "add r0 a = a"
- "add a r0 = a"
- "mul a b = mul b a"
- "mul (add a b) c = add (mul a c) (mul b c)"
- "mul r0 a = r0"
- "mul a r0 = r0"
- "mul r1 a = a"
- "mul a r1 = a"
- "mul (mul lx ly) (mul rx ry) = mul (mul lx rx) (mul ly ry)"
- "mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry))"
- "mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry)"
- "mul (mul lx ly) rx = mul (mul lx rx) ly"
- "mul (mul lx ly) rx = mul lx (mul ly rx)"
- "mul lx (mul rx ry) = mul (mul lx rx) ry"
- "mul lx (mul rx ry) = mul rx (mul lx ry)"
- "add (add a b) (add c d) = add (add a c) (add b d)"
- "add (add a b) c = add a (add b c)"
- "add a (add c d) = add c (add a d)"
- "add (add a b) c = add (add a c) b"
- "add a c = add c a"
- "add a (add c d) = add (add a c) d"
- "mul (pwr x p) (pwr x q) = pwr x (p + q)"
- "mul x (pwr x q) = pwr x (Suc q)"
- "mul (pwr x q) x = pwr x (Suc q)"
- "mul x x = pwr x 2"
- "pwr (mul x y) q = mul (pwr x q) (pwr y q)"
- "pwr (pwr x p) q = pwr x (p * q)"
- "pwr x 0 = r1"
- "pwr x 1 = x"
- "mul x (add y z) = add (mul x y) (mul x z)"
- "pwr x (Suc q) = mul x (pwr x q)"
- "pwr x (2*n) = mul (pwr x n) (pwr x n)"
- "pwr x (Suc (2*n)) = mul x (mul (pwr x n) (pwr x n))"
-proof -
- show "add (mul a m) (mul b m) = mul (add a b) m" using mul_d mul_c by simp
-next show"add (mul a m) m = mul (add a r1) m" using mul_d mul_c mul_1 by simp
-next show "add m (mul a m) = mul (add a r1) m" using mul_c mul_d mul_1 add_c by simp
-next show "add m m = mul (add r1 r1) m" using mul_c mul_d mul_1 by simp
-next show "add r0 a = a" using add_0 by simp
-next show "add a r0 = a" using add_0 add_c by simp
-next show "mul a b = mul b a" using mul_c by simp
-next show "mul (add a b) c = add (mul a c) (mul b c)" using mul_c mul_d by simp
-next show "mul r0 a = r0" using mul_0 by simp
-next show "mul a r0 = r0" using mul_0 mul_c by simp
-next show "mul r1 a = a" using mul_1 by simp
-next show "mul a r1 = a" using mul_1 mul_c by simp
-next show "mul (mul lx ly) (mul rx ry) = mul (mul lx rx) (mul ly ry)"
- using mul_c mul_a by simp
-next show "mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry))"
- using mul_a by simp
-next
- have "mul (mul lx ly) (mul rx ry) = mul (mul rx ry) (mul lx ly)" by (rule mul_c)
- also have "\<dots> = mul rx (mul ry (mul lx ly))" using mul_a by simp
- finally
- show "mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry)"
- using mul_c by simp
-next show "mul (mul lx ly) rx = mul (mul lx rx) ly" using mul_c mul_a by simp
-next
- show "mul (mul lx ly) rx = mul lx (mul ly rx)" by (simp add: mul_a)
-next show "mul lx (mul rx ry) = mul (mul lx rx) ry" by (simp add: mul_a )
-next show "mul lx (mul rx ry) = mul rx (mul lx ry)" by (simp add: mul_a,simp add: mul_c)
-next show "add (add a b) (add c d) = add (add a c) (add b d)"
- using add_c add_a by simp
-next show "add (add a b) c = add a (add b c)" using add_a by simp
-next show "add a (add c d) = add c (add a d)"
- apply (simp add: add_a) by (simp only: add_c)
-next show "add (add a b) c = add (add a c) b" using add_a add_c by simp
-next show "add a c = add c a" by (rule add_c)
-next show "add a (add c d) = add (add a c) d" using add_a by simp
-next show "mul (pwr x p) (pwr x q) = pwr x (p + q)" by (rule mul_pwr)
-next show "mul x (pwr x q) = pwr x (Suc q)" using pwr_Suc by simp
-next show "mul (pwr x q) x = pwr x (Suc q)" using pwr_Suc mul_c by simp
-next show "mul x x = pwr x 2" by (simp add: nat_number' pwr_Suc pwr_0 mul_1 mul_c)
-next show "pwr (mul x y) q = mul (pwr x q) (pwr y q)" by (rule pwr_mul)
-next show "pwr (pwr x p) q = pwr x (p * q)" by (rule pwr_pwr)
-next show "pwr x 0 = r1" using pwr_0 .
-next show "pwr x 1 = x" unfolding One_nat_def by (simp add: nat_number' pwr_Suc pwr_0 mul_1 mul_c)
-next show "mul x (add y z) = add (mul x y) (mul x z)" using mul_d by simp
-next show "pwr x (Suc q) = mul x (pwr x q)" using pwr_Suc by simp
-next show "pwr x (2 * n) = mul (pwr x n) (pwr x n)" by (simp add: nat_number' mul_pwr)
-next show "pwr x (Suc (2 * n)) = mul x (mul (pwr x n) (pwr x n))"
- by (simp add: nat_number' pwr_Suc mul_pwr)
-qed
-
-end
-
-sublocale comm_semiring_1
- < normalizing!: normalizing_semiring plus times power zero one
-proof
-qed (simp_all add: algebra_simps)
+lemma (in comm_semiring_1) semiring_rules:
+ "(a * m) + (b * m) = (a + b) * m"
+ "(a * m) + m = (a + 1) * m"
+ "m + (a * m) = (a + 1) * m"
+ "m + m = (1 + 1) * m"
+ "0 + a = a"
+ "a + 0 = a"
+ "a * b = b * a"
+ "(a + b) * c = (a * c) + (b * c)"
+ "0 * a = 0"
+ "a * 0 = 0"
+ "1 * a = a"
+ "a * 1 = a"
+ "(lx * ly) * (rx * ry) = (lx * rx) * (ly * ry)"
+ "(lx * ly) * (rx * ry) = lx * (ly * (rx * ry))"
+ "(lx * ly) * (rx * ry) = rx * ((lx * ly) * ry)"
+ "(lx * ly) * rx = (lx * rx) * ly"
+ "(lx * ly) * rx = lx * (ly * rx)"
+ "lx * (rx * ry) = (lx * rx) * ry"
+ "lx * (rx * ry) = rx * (lx * ry)"
+ "(a + b) + (c + d) = (a + c) + (b + d)"
+ "(a + b) + c = a + (b + c)"
+ "a + (c + d) = c + (a + d)"
+ "(a + b) + c = (a + c) + b"
+ "a + c = c + a"
+ "a + (c + d) = (a + c) + d"
+ "(x ^ p) * (x ^ q) = x ^ (p + q)"
+ "x * (x ^ q) = x ^ (Suc q)"
+ "(x ^ q) * x = x ^ (Suc q)"
+ "x * x = x ^ 2"
+ "(x * y) ^ q = (x ^ q) * (y ^ q)"
+ "(x ^ p) ^ q = x ^ (p * q)"
+ "x ^ 0 = 1"
+ "x ^ 1 = x"
+ "x * (y + z) = (x * y) + (x * z)"
+ "x ^ (Suc q) = x * (x ^ q)"
+ "x ^ (2*n) = (x ^ n) * (x ^ n)"
+ "x ^ (Suc (2*n)) = x * ((x ^ n) * (x ^ n))"
+ by (simp_all add: algebra_simps power_add power2_eq_square power_mult_distrib power_mult)
lemmas (in comm_semiring_1) normalizing_comm_semiring_1_axioms =
comm_semiring_1_axioms [normalizer
- semiring ops: normalizing.semiring_ops
- semiring rules: normalizing.semiring_rules]
+ semiring ops: semiring_ops
+ semiring rules: semiring_rules]
declaration (in comm_semiring_1)
{* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_axioms} *}
-locale normalizing_ring = normalizing_semiring +
- fixes sub :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
- and neg :: "'a \<Rightarrow> 'a"
- assumes neg_mul: "neg x = mul (neg r1) x"
- and sub_add: "sub x y = add x (neg y)"
-begin
-
-lemma ring_ops: shows "TERM (sub x y)" and "TERM (neg x)" .
+lemma (in comm_ring_1) ring_ops: shows "TERM (x- y)" and "TERM (- x)" .
-lemmas ring_rules = neg_mul sub_add
-
-end
-
-sublocale comm_ring_1
- < normalizing!: normalizing_ring plus times power zero one minus uminus
-proof
-qed (simp_all add: diff_minus)
+lemma (in comm_ring_1) ring_rules:
+ "- x = (- 1) * x"
+ "x - y = x + (- y)"
+ by (simp_all add: diff_minus)
lemmas (in comm_ring_1) normalizing_comm_ring_1_axioms =
comm_ring_1_axioms [normalizer
- semiring ops: normalizing.semiring_ops
- semiring rules: normalizing.semiring_rules
- ring ops: normalizing.ring_ops
- ring rules: normalizing.ring_rules]
+ semiring ops: semiring_ops
+ semiring rules: semiring_rules
+ ring ops: ring_ops
+ ring rules: ring_rules]
declaration (in comm_ring_1)
{* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_ring_1_axioms} *}
-locale normalizing_semiring_cancel = normalizing_semiring +
- assumes add_cancel: "add (x::'a) y = add x z \<longleftrightarrow> y = z"
- and add_mul_solve: "add (mul w y) (mul x z) =
- add (mul w z) (mul x y) \<longleftrightarrow> w = x \<or> y = z"
-begin
-
-lemma noteq_reduce: "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> add (mul a c) (mul b d) \<noteq> add (mul a d) (mul b c)"
+lemma (in comm_semiring_1_cancel_norm) noteq_reduce:
+ "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> (a * c) + (b * d) \<noteq> (a * d) + (b * c)"
proof-
have "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> \<not> (a = b \<or> c = d)" by simp
- also have "\<dots> \<longleftrightarrow> add (mul a c) (mul b d) \<noteq> add (mul a d) (mul b c)"
- using add_mul_solve by blast
- finally show "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> add (mul a c) (mul b d) \<noteq> add (mul a d) (mul b c)"
+ also have "\<dots> \<longleftrightarrow> (a * c) + (b * d) \<noteq> (a * d) + (b * c)"
+ using add_mult_solve by blast
+ finally show "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> (a * c) + (b * d) \<noteq> (a * d) + (b * c)"
by simp
qed
-lemma add_scale_eq_noteq: "\<lbrakk>r \<noteq> r0 ; (a = b) \<and> ~(c = d)\<rbrakk>
- \<Longrightarrow> add a (mul r c) \<noteq> add b (mul r d)"
+lemma (in comm_semiring_1_cancel_norm) add_scale_eq_noteq:
+ "\<lbrakk>r \<noteq> 0 ; a = b \<and> c \<noteq> d\<rbrakk> \<Longrightarrow> a + (r * c) \<noteq> b + (r * d)"
proof(clarify)
- assume nz: "r\<noteq> r0" and cnd: "c\<noteq>d"
- and eq: "add b (mul r c) = add b (mul r d)"
- hence "mul r c = mul r d" using cnd add_cancel by simp
- hence "add (mul r0 d) (mul r c) = add (mul r0 c) (mul r d)"
- using mul_0 add_cancel by simp
- thus "False" using add_mul_solve nz cnd by simp
+ assume nz: "r\<noteq> 0" and cnd: "c\<noteq>d"
+ and eq: "b + (r * c) = b + (r * d)"
+ have "(0 * d) + (r * c) = (0 * c) + (r * d)"
+ using add_imp_eq eq mult_zero_left by simp
+ thus "False" using add_mult_solve[of 0 d] nz cnd by simp
qed
-lemma add_r0_iff: " x = add x a \<longleftrightarrow> a = r0"
+lemma (in comm_semiring_1_cancel_norm) add_0_iff:
+ "x = x + a \<longleftrightarrow> a = 0"
proof-
- have "a = r0 \<longleftrightarrow> add x a = add x r0" by (simp add: add_cancel)
- thus "x = add x a \<longleftrightarrow> a = r0" by (auto simp add: add_c add_0)
+ have "a = 0 \<longleftrightarrow> x + a = x + 0" using add_imp_eq[of x a 0] by auto
+ thus "x = x + a \<longleftrightarrow> a = 0" by (auto simp add: add_commute)
qed
-end
-
-sublocale comm_semiring_1_cancel_norm
- < normalizing!: normalizing_semiring_cancel plus times power zero one
-proof
-qed (simp_all add: add_mult_solve)
-
declare (in comm_semiring_1_cancel_norm)
normalizing_comm_semiring_1_axioms [normalizer del]
lemmas (in comm_semiring_1_cancel_norm)
normalizing_comm_semiring_1_cancel_norm_axioms =
comm_semiring_1_cancel_norm_axioms [normalizer
- semiring ops: normalizing.semiring_ops
- semiring rules: normalizing.semiring_rules
- idom rules: normalizing.noteq_reduce normalizing.add_scale_eq_noteq]
+ semiring ops: semiring_ops
+ semiring rules: semiring_rules
+ idom rules: noteq_reduce add_scale_eq_noteq]
declaration (in comm_semiring_1_cancel_norm)
{* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_cancel_norm_axioms} *}
-locale normalizing_ring_cancel = normalizing_semiring_cancel + normalizing_ring +
- assumes subr0_iff: "sub x y = r0 \<longleftrightarrow> x = y"
-
-sublocale idom
- < normalizing!: normalizing_ring_cancel plus times power zero one minus uminus
-proof
-qed simp
-
declare (in idom) normalizing_comm_ring_1_axioms [normalizer del]
lemmas (in idom) normalizing_idom_axioms = idom_axioms [normalizer
- semiring ops: normalizing.semiring_ops
- semiring rules: normalizing.semiring_rules
- ring ops: normalizing.ring_ops
- ring rules: normalizing.ring_rules
- idom rules: normalizing.noteq_reduce normalizing.add_scale_eq_noteq
- ideal rules: normalizing.subr0_iff normalizing.add_r0_iff]
+ semiring ops: semiring_ops
+ semiring rules: semiring_rules
+ ring ops: ring_ops
+ ring rules: ring_rules
+ idom rules: noteq_reduce add_scale_eq_noteq
+ ideal rules: right_minus_eq add_0_iff]
declaration (in idom)
{* Semiring_Normalizer.semiring_funs @{thm normalizing_idom_axioms} *}
-locale normalizing_field = normalizing_ring_cancel +
- fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
- and inverse:: "'a \<Rightarrow> 'a"
- assumes divide_inverse: "divide x y = mul x (inverse y)"
- and inverse_divide: "inverse x = divide r1 x"
-begin
-
-lemma field_ops: shows "TERM (divide x y)" and "TERM (inverse x)" .
+lemma (in field) field_ops:
+ shows "TERM (x / y)" and "TERM (inverse x)" .
-lemmas field_rules = divide_inverse inverse_divide
-
-end
-
-sublocale field
- < normalizing!: normalizing_field plus times power zero one minus uminus divide inverse
-proof
-qed (simp_all add: divide_inverse)
+lemmas (in field) field_rules = divide_inverse inverse_eq_divide
lemmas (in field) normalizing_field_axioms =
field_axioms [normalizer
- semiring ops: normalizing.semiring_ops
- semiring rules: normalizing.semiring_rules
- ring ops: normalizing.ring_ops
- ring rules: normalizing.ring_rules
- field ops: normalizing.field_ops
- field rules: normalizing.field_rules
- idom rules: normalizing.noteq_reduce normalizing.add_scale_eq_noteq
- ideal rules: normalizing.subr0_iff normalizing.add_r0_iff]
+ semiring ops: semiring_ops
+ semiring rules: semiring_rules
+ ring ops: ring_ops
+ ring rules: ring_rules
+ field ops: field_ops
+ field rules: field_rules
+ idom rules: noteq_reduce add_scale_eq_noteq
+ ideal rules: right_minus_eq add_0_iff]
declaration (in field)
{* Semiring_Normalizer.field_funs @{thm normalizing_field_axioms} *}
+hide_fact (open) normalizing_comm_semiring_1_axioms
+ normalizing_comm_semiring_1_cancel_norm_axioms semiring_ops semiring_rules
+
+hide_fact (open) normalizing_comm_ring_1_axioms
+ normalizing_idom_axioms ring_ops ring_rules
+
+hide_fact (open) normalizing_field_axioms field_ops field_rules
+
+hide_fact (open) add_scale_eq_noteq noteq_reduce
+
end
--- a/src/HOL/SetInterval.thy Wed May 12 15:25:02 2010 +0200
+++ b/src/HOL/SetInterval.thy Wed May 12 15:25:23 2010 +0200
@@ -231,6 +231,8 @@
lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}"
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
+lemma atLeastAtMost_singleton': "a = b \<Longrightarrow> {a .. b} = {a}" by simp
+
lemma atLeastatMost_subset_iff[simp]:
"{a..b} <= {c..d} \<longleftrightarrow> (~ a <= b) | c <= a & b <= d"
unfolding atLeastAtMost_def atLeast_def atMost_def
@@ -241,6 +243,15 @@
((~ a <= b) | c <= a & b <= d & (c < a | b < d)) & c <= d"
by(simp add: psubset_eq expand_set_eq less_le_not_le)(blast intro: order_trans)
+lemma atLeastAtMost_singleton_iff[simp]:
+ "{a .. b} = {c} \<longleftrightarrow> a = b \<and> b = c"
+proof
+ assume "{a..b} = {c}"
+ hence "\<not> (\<not> a \<le> b)" unfolding atLeastatMost_empty_iff[symmetric] by simp
+ moreover with `{a..b} = {c}` have "c \<le> a \<and> b \<le> c" by auto
+ ultimately show "a = b \<and> b = c" by auto
+qed simp
+
end
lemma (in linorder) atLeastLessThan_subset_iff:
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Wed May 12 15:25:02 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Wed May 12 15:25:23 2010 +0200
@@ -38,14 +38,6 @@
(* composition of two theorems, used in maps *)
fun OF1 thm1 thm2 = thm2 RS thm1
-(* prints a warning, if the subgoal is not solved *)
-fun WARN (tac, msg) i st =
- case Seq.pull (SOLVED' tac i st) of
- NONE => (warning msg; Seq.single st)
- | seqcell => Seq.make (fn () => seqcell)
-
-fun RANGE_WARN tacs = RANGE (map WARN tacs)
-
fun atomize_thm thm =
let
val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *)
@@ -631,21 +623,14 @@
(* Automatic Proofs *)
-val msg1 = "The regularize proof failed."
-val msg2 = cat_lines ["The injection proof failed.",
- "This is probably due to missing respects lemmas.",
- "Try invoking the injection method manually to see",
- "which lemmas are missing."]
-val msg3 = "The cleaning proof failed."
-
fun lift_tac ctxt rthms =
let
fun mk_tac rthm =
procedure_tac ctxt rthm
- THEN' RANGE_WARN
- [(regularize_tac ctxt, msg1),
- (all_injection_tac ctxt, msg2),
- (clean_tac ctxt, msg3)]
+ THEN' RANGE
+ [regularize_tac ctxt,
+ all_injection_tac ctxt,
+ clean_tac ctxt]
in
simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *)
THEN' RANGE (map mk_tac rthms)
--- a/src/HOL/ex/HarmonicSeries.thy Wed May 12 15:25:02 2010 +0200
+++ b/src/HOL/ex/HarmonicSeries.thy Wed May 12 15:25:23 2010 +0200
@@ -168,13 +168,7 @@
by simp
also have
"\<dots> = (\<Sum>n\<in>{2::nat..2}. 1/real n) + 1"
- proof -
- have "(2::nat)^0 = 1" by simp
- then have "(2::nat)^0+1 = 2" by simp
- moreover have "(2::nat)^1 = 2" by simp
- ultimately have "{((2::nat)^0)+1..2^1} = {2::nat..2}" by auto
- thus ?thesis by simp
- qed
+ by (auto simp: atLeastAtMost_singleton')
also have
"\<dots> = 1/2 + 1"
by simp
--- a/src/Pure/General/pretty.scala Wed May 12 15:25:02 2010 +0200
+++ b/src/Pure/General/pretty.scala Wed May 12 15:25:23 2010 +0200
@@ -7,6 +7,9 @@
package isabelle
+import java.awt.FontMetrics
+
+
object Pretty
{
/* markup trees with physical blocks and breaks */
@@ -45,32 +48,6 @@
/* formatted output */
- private case class Text(tx: List[XML.Tree] = Nil, val pos: Int = 0, val nl: Int = 0)
- {
- def newline: Text = copy(tx = FBreak :: tx, pos = 0, nl = nl + 1)
- def string(s: String): Text = copy(tx = XML.Text(s) :: tx, pos = pos + s.length)
- def blanks(wd: Int): Text = string(Symbol.spaces(wd))
- def content: List[XML.Tree] = tx.reverse
- }
-
- private def breakdist(trees: List[XML.Tree], after: Int): Int =
- trees match {
- case Break(_) :: _ => 0
- case FBreak :: _ => 0
- case XML.Elem(_, _, body) :: ts =>
- (0 /: body)(_ + XML.content_length(_)) + breakdist(ts, after)
- case XML.Text(s) :: ts => s.length + breakdist(ts, after)
- case Nil => after
- }
-
- private def forcenext(trees: List[XML.Tree]): List[XML.Tree] =
- trees match {
- case Nil => Nil
- case FBreak :: _ => trees
- case Break(_) :: ts => FBreak :: ts
- case t :: ts => t :: forcenext(ts)
- }
-
private def standard_format(tree: XML.Tree): List[XML.Tree] =
tree match {
case XML.Elem(name, atts, body) => List(XML.Elem(name, atts, body.flatMap(standard_format)))
@@ -79,14 +56,53 @@
Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString)))
}
- private val margin_default = 76
+ case class Text(tx: List[XML.Tree] = Nil, val pos: Double = 0.0, val nl: Int = 0)
+ {
+ def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
+ def string(s: String, len: Double): Text = copy(tx = XML.Text(s) :: tx, pos = pos + len)
+ def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble)
+ def content: List[XML.Tree] = tx.reverse
+ }
- def formatted(input: List[XML.Tree], margin: Int = margin_default): List[XML.Tree] =
+ private val margin_default = 76
+ private def metric_default(s: String) = s.length.toDouble
+
+ def font_metric(metrics: FontMetrics): String => Double =
+ if (metrics == null) ((s: String) => s.length.toDouble)
+ else {
+ val unit = metrics.charWidth(Symbol.spc).toDouble
+ ((s: String) => if (s == "\n") 1.0 else metrics.stringWidth(s) / unit)
+ }
+
+ def formatted(input: List[XML.Tree], margin: Int = margin_default,
+ metric: String => Double = metric_default): List[XML.Tree] =
{
val breakgain = margin / 20
val emergencypos = margin / 2
- def format(trees: List[XML.Tree], blockin: Int, after: Int, text: Text): Text =
+ def content_length(tree: XML.Tree): Double =
+ tree match {
+ case XML.Elem(_, _, body) => (0.0 /: body)(_ + content_length(_))
+ case XML.Text(s) => metric(s)
+ }
+
+ def breakdist(trees: List[XML.Tree], after: Double): Double =
+ trees match {
+ case Break(_) :: _ => 0.0
+ case FBreak :: _ => 0.0
+ case t :: ts => content_length(t) + breakdist(ts, after)
+ case Nil => after
+ }
+
+ def forcenext(trees: List[XML.Tree]): List[XML.Tree] =
+ trees match {
+ case Nil => Nil
+ case FBreak :: _ => trees
+ case Break(_) :: ts => FBreak :: ts
+ case t :: ts => t :: forcenext(ts)
+ }
+
+ def format(trees: List[XML.Tree], blockin: Double, after: Double, text: Text): Text =
trees match {
case Nil => text
@@ -103,20 +119,21 @@
case Break(wd) :: ts =>
if (text.pos + wd <= (margin - breakdist(ts, after)).max(blockin + breakgain))
format(ts, blockin, after, text.blanks(wd))
- else format(ts, blockin, after, text.newline.blanks(blockin))
- case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin))
+ else format(ts, blockin, after, text.newline.blanks(blockin.toInt))
+ case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin.toInt))
case XML.Elem(name, atts, body) :: ts =>
val btext = format(body, blockin, breakdist(ts, after), text.copy(tx = Nil))
val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
val btext1 = btext.copy(tx = XML.Elem(name, atts, btext.content) :: text.tx)
format(ts1, blockin, after, btext1)
- case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s))
+ case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s, metric(s)))
}
- format(input.flatMap(standard_format), 0, 0, Text()).content
+ format(input.flatMap(standard_format), 0.0, 0.0, Text()).content
}
- def string_of(input: List[XML.Tree], margin: Int = margin_default): String =
+ def string_of(input: List[XML.Tree], margin: Int = margin_default,
+ metric: String => Double = metric_default): String =
formatted(input).iterator.flatMap(XML.content).mkString
@@ -128,7 +145,7 @@
tree match {
case Block(_, body) => body.flatMap(fmt)
case Break(wd) => List(XML.Text(Symbol.spaces(wd)))
- case FBreak => List(XML.Text(" "))
+ case FBreak => List(XML.Text(Symbol.space))
case XML.Elem(name, atts, body) => List(XML.Elem(name, atts, body.flatMap(fmt)))
case XML.Text(_) => List(tree)
}
--- a/src/Pure/General/symbol.scala Wed May 12 15:25:02 2010 +0200
+++ b/src/Pure/General/symbol.scala Wed May 12 15:25:23 2010 +0200
@@ -15,13 +15,16 @@
{
/* spaces */
- private val static_spaces = " " * 4000
+ val spc = ' '
+ val space = " "
+
+ private val static_spaces = space * 4000
def spaces(k: Int): String =
{
require(k >= 0)
if (k < static_spaces.length) static_spaces.substring(0, k)
- else " " * k
+ else space * k
}
@@ -278,7 +281,7 @@
"\\<^isub>", "\\<^isup>")
private val blanks =
- Decode_Set(" ", "\t", "\n", "\u000B", "\f", "\r", "\\<spacespace>", "\\<^newline>")
+ Decode_Set(space, "\t", "\n", "\u000B", "\f", "\r", "\\<spacespace>", "\\<^newline>")
private val sym_chars =
Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
--- a/src/Pure/General/xml.scala Wed May 12 15:25:02 2010 +0200
+++ b/src/Pure/General/xml.scala Wed May 12 15:25:23 2010 +0200
@@ -92,12 +92,6 @@
}
}
- def content_length(tree: XML.Tree): Int =
- tree match {
- case Elem(_, _, body) => (0 /: body)(_ + content_length(_))
- case Text(s) => s.length
- }
-
/* cache for partial sharing -- NOT THREAD SAFE */
--- a/src/Tools/jEdit/plugin/Isabelle.props Wed May 12 15:25:02 2010 +0200
+++ b/src/Tools/jEdit/plugin/Isabelle.props Wed May 12 15:25:23 2010 +0200
@@ -27,8 +27,6 @@
options.isabelle.logic.title=Logic
options.isabelle.relative-font-size.title=Relative Font Size
options.isabelle.relative-font-size=100
-options.isabelle.relative-margin.title=Relative Margin
-options.isabelle.relative-margin=90
options.isabelle.startup-timeout=10000
#menu actions
--- a/src/Tools/jEdit/src/jedit/html_panel.scala Wed May 12 15:25:02 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala Wed May 12 15:25:23 2010 +0200
@@ -10,7 +10,7 @@
import isabelle._
import java.io.StringReader
-import java.awt.{BorderLayout, Dimension, GraphicsEnvironment, Toolkit}
+import java.awt.{BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics}
import java.awt.event.MouseEvent
import javax.swing.{JButton, JPanel, JScrollPane}
@@ -40,13 +40,23 @@
class HTML_Panel(
sys: Isabelle_System,
- font_size0: Int, relative_margin0: Int,
+ initial_font_size: Int,
handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel
{
// global logging
Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
+ /* pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize */
+
+ val screen_resolution =
+ if (GraphicsEnvironment.isHeadless()) 72
+ else Toolkit.getDefaultToolkit().getScreenResolution()
+
+ def lobo_px(raw_px: Int): Int = raw_px * 96 / screen_resolution
+ def raw_px(lobo_px: Int): Int = (lobo_px * screen_resolution + 95) / 96
+
+
/* document template */
private def try_file(name: String): String =
@@ -57,14 +67,6 @@
private def template(font_size: Int): String =
{
- // re-adjustment according to org.lobobrowser.html.style.HtmlValues.getFontSize
- val dpi =
- if (GraphicsEnvironment.isHeadless()) 72
- else Toolkit.getDefaultToolkit().getScreenResolution()
-
- val size0 = font_size * dpi / 96
- val size = if (size0 * 96 / dpi == font_size) size0 else size0 + 1
-
"""<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
@@ -74,7 +76,7 @@
""" +
try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
- "body { font-family: " + sys.font_family + "; font-size: " + size + "px }" +
+ "body { font-family: " + sys.font_family + "; font-size: " + raw_px(font_size) + "px }" +
"""
</style>
</head>
@@ -83,15 +85,13 @@
"""
}
+ private def font_metrics(font_size: Int): FontMetrics =
+ Swing_Thread.now { getFontMetrics(sys.get_font(font_size)) }
- def panel_width(font_size: Int, relative_margin: Int): Int =
- {
- val font = sys.get_font(font_size)
+ private def panel_width(font_size: Int): Int =
Swing_Thread.now {
- val char_width = (getFontMetrics(font).stringWidth("mix") / 3) max 1
- ((getWidth() * relative_margin) / (100 * char_width)) max 20
+ (getWidth() / (font_metrics(font_size).charWidth(Symbol.spc) max 1) - 4) max 20
}
- }
/* actor with local state */
@@ -118,8 +118,8 @@
private val builder = new DocumentBuilderImpl(ucontext, rcontext)
- private case class Init(font_size: Int, relative_margin: Int)
- private case class Render(body: List[XML.Tree])
+ private case class Init(font_size: Int)
+ private case class Render(divs: List[XML.Tree])
private val main_actor = actor {
// crude double buffering
@@ -127,13 +127,13 @@
var doc2: org.w3c.dom.Document = null
var current_font_size = 16
- var current_relative_margin = 90
+ var current_font_metrics: FontMetrics = null
loop {
react {
- case Init(font_size, relative_margin) =>
+ case Init(font_size) =>
current_font_size = font_size
- current_relative_margin = relative_margin
+ current_font_metrics = font_metrics(lobo_px(raw_px(font_size)))
val src = template(font_size)
def parse() =
@@ -141,12 +141,14 @@
doc1 = parse()
doc2 = parse()
Swing_Thread.now { setDocument(doc1, rcontext) }
-
- case Render(body) =>
+
+ case Render(divs) =>
val doc = doc2
val html_body =
- Pretty.formatted(body, panel_width(current_font_size, current_relative_margin))
- .map(t => XML.elem(HTML.PRE, HTML.spans(t)))
+ divs.flatMap(div =>
+ Pretty.formatted(List(div), panel_width(current_font_size),
+ Pretty.font_metric(current_font_metrics))
+ .map(t => XML.elem(HTML.PRE, HTML.spans(t))))
val node = XML.document_node(doc, XML.elem(HTML.BODY, html_body))
doc.removeChild(doc.getLastChild())
doc.appendChild(node)
@@ -161,9 +163,9 @@
/* main method wrappers */
-
- def init(font_size: Int, relative_margin: Int) { main_actor ! Init(font_size, relative_margin) }
- def render(body: List[XML.Tree]) { main_actor ! Render(body) }
- init(font_size0, relative_margin0)
+ def init(font_size: Int) { main_actor ! Init(font_size) }
+ def render(divs: List[XML.Tree]) { main_actor ! Render(divs) }
+
+ init(initial_font_size)
}
--- a/src/Tools/jEdit/src/jedit/isabelle_options.scala Wed May 12 15:25:02 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala Wed May 12 15:25:23 2010 +0200
@@ -16,7 +16,6 @@
{
private val logic_name = new JComboBox()
private val relative_font_size = new JSpinner()
- private val relative_margin = new JSpinner()
private class List_Item(val name: String, val descr: String) {
def this(name: String) = this(name, name)
@@ -41,11 +40,6 @@
relative_font_size.setValue(Isabelle.Int_Property("relative-font-size"))
relative_font_size
})
-
- addComponent(Isabelle.Property("relative-margin.title"), {
- relative_margin.setValue(Isabelle.Int_Property("relative-margin"))
- relative_margin
- })
}
override def _save()
@@ -55,8 +49,5 @@
Isabelle.Int_Property("relative-font-size") =
relative_font_size.getValue().asInstanceOf[Int]
-
- Isabelle.Int_Property("relative-margin") =
- relative_margin.getValue().asInstanceOf[Int]
}
}
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Wed May 12 15:25:02 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Wed May 12 15:25:23 2010 +0200
@@ -24,9 +24,7 @@
if (position == DockableWindowManager.FLOATING)
setPreferredSize(new Dimension(500, 250))
- val html_panel =
- new HTML_Panel(Isabelle.system,
- Isabelle.font_size(), Isabelle.Int_Property("relative-margin"), null)
+ val html_panel = new HTML_Panel(Isabelle.system, Isabelle.font_size(), null)
add(html_panel, BorderLayout.CENTER)
@@ -43,8 +41,7 @@
html_panel.render(body)
}
- case Session.Global_Settings =>
- html_panel.init(Isabelle.font_size(), Isabelle.Int_Property("relative-margin"))
+ case Session.Global_Settings => html_panel.init(Isabelle.font_size())
case bad => System.err.println("output_actor: ignoring bad message " + bad)
}