--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Fri Mar 13 15:50:06 2009 +0100
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Fri Mar 13 15:52:23 2009 +0100
@@ -92,7 +92,7 @@
the $n$th element of @{text xs}.
\item Human readers are good at converting automatically from lists to
-sets. Hence \texttt{OptionalSugar} contains syntax for supressing the
+sets. Hence \texttt{OptionalSugar} contains syntax for suppressing the
conversion function @{const set}: for example, @{prop[source]"x \<in> set xs"}
becomes @{prop"x \<in> set xs"}.
@@ -106,6 +106,17 @@
\end{itemize}
*}
+subsection{* Numbers *}
+
+text{* Coercions between numeric types are alien to mathematicians who
+consider, for example, @{typ nat} as a subset of @{typ int}.
+\texttt{OptionalSugar} contains syntax for suppressing numeric coercions such
+as @{const int} @{text"::"} @{typ"nat \<Rightarrow> int"}. For example,
+@{term[source]"int 5"} is printed as @{term "int 5"}. Embeddings of types
+@{typ nat}, @{typ int}, @{typ real} are covered; non-injective coercions such
+as @{const nat} @{text"::"} @{typ"int \<Rightarrow> nat"} are not and should not be
+hidden. *}
+
section "Printing theorems"
subsection "Question marks"
@@ -126,7 +137,7 @@
at the beginning of your file \texttt{ROOT.ML}.
The rest of this document is produced with this flag reset.
-Hint: Resetting \verb!show_question_marks! only supresses question
+Hint: Resetting \verb!show_question_marks! only suppresses question
marks; variables that end in digits, e.g. @{text"x1"}, are still
printed with a trailing @{text".0"}, e.g. @{text"x1.0"}, their
internal index. This can be avoided by turning the last digit into a
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Fri Mar 13 15:50:06 2009 +0100
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Fri Mar 13 15:52:23 2009 +0100
@@ -120,7 +120,7 @@
the $n$th element of \isa{xs}.
\item Human readers are good at converting automatically from lists to
-sets. Hence \texttt{OptionalSugar} contains syntax for supressing the
+sets. Hence \texttt{OptionalSugar} contains syntax for suppressing the
conversion function \isa{set}: for example, \isa{{\isachardoublequote}x\ {\isasymin}\ set\ xs{\isachardoublequote}}
becomes \isa{x\ {\isasymin}\ xs}.
@@ -137,6 +137,22 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{Numbers%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Coercions between numeric types are alien to mathematicians who
+consider, for example, \isa{nat} as a subset of \isa{int}.
+\texttt{OptionalSugar} contains syntax for suppressing numeric coercions such
+as \isa{int} \isa{{\isacharcolon}{\isacharcolon}} \isa{nat\ {\isasymRightarrow}\ int}. For example,
+\isa{{\isachardoublequote}int\ {\isadigit{5}}{\isachardoublequote}} is printed as \isa{{\isadigit{5}}}. Embeddings of types
+\isa{nat}, \isa{int}, \isa{real} are covered; non-injective coercions such
+as \isa{nat} \isa{{\isacharcolon}{\isacharcolon}} \isa{int\ {\isasymRightarrow}\ nat} are not and should not be
+hidden.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsection{Printing theorems%
}
\isamarkuptrue%
@@ -162,7 +178,7 @@
at the beginning of your file \texttt{ROOT.ML}.
The rest of this document is produced with this flag reset.
-Hint: Resetting \verb!show_question_marks! only supresses question
+Hint: Resetting \verb!show_question_marks! only suppresses question
marks; variables that end in digits, e.g. \isa{x{\isadigit{1}}}, are still
printed with a trailing \isa{{\isachardot}{\isadigit{0}}}, e.g. \isa{x{\isadigit{1}}{\isachardot}{\isadigit{0}}}, their
internal index. This can be avoided by turning the last digit into a
--- a/lib/Tools/codegen Fri Mar 13 15:50:06 2009 +0100
+++ b/lib/Tools/codegen Fri Mar 13 15:52:23 2009 +0100
@@ -33,8 +33,8 @@
## main
-THY=$(echo $THY | sed -e 's/\\/\\\\"/g; s/"/\\\"/g')
-ISAR="theory Codegen imports \"$THY\" begin export_code $CMD end"
+CODE_CMD=$(echo $CMD | perl -pe 's/\\/\\\\/g; s/"/\\\"/g')
+CTXT_CMD="ML_Context.eval_in (SOME (ProofContext.init (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
+FULL_CMD="val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
-echo "$ISAR" | "$ISABELLE_PROCESS" -I "$IMAGE"
-exit ${PIPESTATUS[1]}
+"$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1
--- a/src/HOL/Divides.thy Fri Mar 13 15:50:06 2009 +0100
+++ b/src/HOL/Divides.thy Fri Mar 13 15:52:23 2009 +0100
@@ -593,8 +593,8 @@
val div_name = @{const_name div};
val mod_name = @{const_name mod};
val mk_binop = HOLogic.mk_binop;
-val mk_sum = ArithData.mk_sum;
-val dest_sum = ArithData.dest_sum;
+val mk_sum = Nat_Arith.mk_sum;
+val dest_sum = Nat_Arith.dest_sum;
(*logic*)
@@ -604,7 +604,7 @@
val prove_eq_sums =
let val simps = @{thm add_0} :: @{thm add_0_right} :: @{thms add_ac}
- in ArithData.prove_conv all_tac (ArithData.simp_all_tac simps) end;
+ in Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac simps) end;
end;
--- a/src/HOL/Int.thy Fri Mar 13 15:50:06 2009 +0100
+++ b/src/HOL/Int.thy Fri Mar 13 15:52:23 2009 +0100
@@ -1527,7 +1527,7 @@
use "~~/src/Provers/Arith/assoc_fold.ML"
use "Tools/int_arith.ML"
-declaration {* K int_arith_setup *}
+declaration {* K Int_Arith.setup *}
subsection{*Lemmas About Small Numerals*}
--- a/src/HOL/IntDiv.thy Fri Mar 13 15:50:06 2009 +0100
+++ b/src/HOL/IntDiv.thy Fri Mar 13 15:52:23 2009 +0100
@@ -261,7 +261,7 @@
val prove_eq_sums =
let
val simps = @{thm diff_int_def} :: Int_Numeral_Simprocs.add_0s @ @{thms zadd_ac}
- in ArithData.prove_conv all_tac (ArithData.simp_all_tac simps) end;
+ in Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac simps) end;
end)
in
--- a/src/HOL/IsaMakefile Fri Mar 13 15:50:06 2009 +0100
+++ b/src/HOL/IsaMakefile Fri Mar 13 15:52:23 2009 +0100
@@ -175,6 +175,7 @@
Tools/inductive_realizer.ML \
Tools/inductive_set_package.ML \
Tools/lin_arith.ML \
+ Tools/nat_arith.ML \
Tools/old_primrec_package.ML \
Tools/primrec_package.ML \
Tools/prop_logic.ML \
--- a/src/HOL/Library/Numeral_Type.thy Fri Mar 13 15:50:06 2009 +0100
+++ b/src/HOL/Library/Numeral_Type.thy Fri Mar 13 15:52:23 2009 +0100
@@ -36,7 +36,7 @@
typed_print_translation {*
let
- fun card_univ_tr' show_sorts _ [Const (@{const_name UNIV}, Type(_,[T,_]))] =
+ fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_,[T,_]))] =
Syntax.const "_type_card" $ Syntax.term_of_typ show_sorts T;
in [(@{const_syntax card}, card_univ_tr')]
end
--- a/src/HOL/Library/OptionalSugar.thy Fri Mar 13 15:50:06 2009 +0100
+++ b/src/HOL/Library/OptionalSugar.thy Fri Mar 13 15:52:23 2009 +0100
@@ -18,6 +18,8 @@
"n" <= "real n"
"n" <= "CONST real_of_nat n"
"n" <= "CONST real_of_int n"
+ "n" <= "CONST of_real n"
+ "n" <= "CONST complex_of_real n"
(* append *)
syntax (latex output)
@@ -27,6 +29,7 @@
"appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)"
+(* deprecated, use thm_style instead, will be removed *)
(* aligning equations *)
notation (tab output)
"op =" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
--- a/src/HOL/Library/Random.thy Fri Mar 13 15:50:06 2009 +0100
+++ b/src/HOL/Library/Random.thy Fri Mar 13 15:52:23 2009 +0100
@@ -21,6 +21,7 @@
fun log :: "index \<Rightarrow> index \<Rightarrow> index" where
"log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
+
subsection {* Random seeds *}
types seed = "index \<times> index"
@@ -57,29 +58,17 @@
subsection {* Base selectors *}
-function range_aux :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where
- "range_aux k l s = (if k = 0 then (l, s) else
- let (v, s') = next s
- in range_aux (k - 1) (v + l * 2147483561) s')"
-by pat_completeness auto
-termination
- by (relation "measure (Code_Index.nat_of o fst)")
- (auto simp add: index)
+fun iterate :: "index \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
+ "iterate k f x = (if k = 0 then Pair x else f x o\<rightarrow> iterate (k - 1) f)"
definition range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where
- "range k = range_aux (log 2147483561 k) 1
+ "range k = iterate (log 2147483561 k)
+ (\<lambda>l. next o\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
o\<rightarrow> (\<lambda>v. Pair (v mod k))"
lemma range:
- assumes "k > 0"
- shows "fst (range k s) < k"
-proof -
- obtain v w where range_aux:
- "range_aux (log 2147483561 k) 1 s = (v, w)"
- by (cases "range_aux (log 2147483561 k) 1 s")
- with assms show ?thesis
- by (simp add: scomp_apply range_def del: range_aux.simps log.simps)
-qed
+ "k > 0 \<Longrightarrow> fst (range k s) < k"
+ by (simp add: range_def scomp_apply split_def del: log.simps iterate.simps)
definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
"select xs = range (Code_Index.of_nat (length xs))
--- a/src/HOL/NSA/NSA.thy Fri Mar 13 15:50:06 2009 +0100
+++ b/src/HOL/NSA/NSA.thy Fri Mar 13 15:52:23 2009 +0100
@@ -684,7 +684,7 @@
in
val approx_reorient_simproc =
- Int_Numeral_Base_Simprocs.prep_simproc
+ Arith_Data.prep_simproc
("reorient_simproc", ["0@=x", "1@=x", "number_of w @= x"], reorient_proc);
end;
--- a/src/HOL/Nat.thy Fri Mar 13 15:50:06 2009 +0100
+++ b/src/HOL/Nat.thy Fri Mar 13 15:52:23 2009 +0100
@@ -2,7 +2,7 @@
Author: Tobias Nipkow and Lawrence C Paulson and Markus Wenzel
Type "nat" is a linear order, and a datatype; arithmetic operators + -
-and * (for div, mod and dvd, see theory Divides).
+and * (for div and mod, see theory Divides).
*)
header {* Natural numbers *}
@@ -12,7 +12,8 @@
uses
"~~/src/Tools/rat.ML"
"~~/src/Provers/Arith/cancel_sums.ML"
- ("Tools/arith_data.ML")
+ "Tools/arith_data.ML"
+ ("Tools/nat_arith.ML")
"~~/src/Provers/Arith/fast_lin_arith.ML"
("Tools/lin_arith.ML")
begin
@@ -1344,8 +1345,8 @@
shows "u = s"
using 2 1 by (rule trans)
-use "Tools/arith_data.ML"
-declaration {* K ArithData.setup *}
+use "Tools/nat_arith.ML"
+declaration {* K Nat_Arith.setup *}
ML{*
structure ArithFacts =
--- a/src/HOL/NatBin.thy Fri Mar 13 15:50:06 2009 +0100
+++ b/src/HOL/NatBin.thy Fri Mar 13 15:52:23 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/NatBin.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1999 University of Cambridge
*)
--- a/src/HOL/Tools/arith_data.ML Fri Mar 13 15:50:06 2009 +0100
+++ b/src/HOL/Tools/arith_data.ML Fri Mar 13 15:52:23 2009 +0100
@@ -1,155 +1,39 @@
(* Title: HOL/arith_data.ML
Author: Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
-Basic arithmetic proof tools.
+Common arithmetic proof auxiliary.
*)
signature ARITH_DATA =
sig
- val prove_conv: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
+ val prove_conv_nohyps: tactic list -> Proof.context -> term * term -> thm option
+ val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
+ val prove_conv2: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
val simp_all_tac: thm list -> simpset -> tactic
-
- val mk_sum: term list -> term
- val mk_norm_sum: term list -> term
- val dest_sum: term -> term list
-
- val nat_cancel_sums_add: simproc list
- val nat_cancel_sums: simproc list
- val setup: Context.generic -> Context.generic
+ val prep_simproc: string * string list * (theory -> simpset -> term -> thm option)
+ -> simproc
end;
-structure ArithData: ARITH_DATA =
+structure Arith_Data: ARITH_DATA =
struct
-(** generic proof tools **)
+fun prove_conv_nohyps tacs ctxt (t, u) =
+ if t aconv u then NONE
+ else let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
+ in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end;
-(* prove conversions *)
+fun prove_conv tacs ctxt (_: thm list) = prove_conv_nohyps tacs ctxt;
-fun prove_conv expand_tac norm_tac ss tu = (* FIXME avoid standard *)
+fun prove_conv2 expand_tac norm_tac ss tu = (*FIXME avoid standard*)
mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] []
(HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
(K (EVERY [expand_tac, norm_tac ss]))));
-(* rewriting *)
-
fun simp_all_tac rules =
let val ss0 = HOL_ss addsimps rules
in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
-
-(** abstract syntax of structure nat: 0, Suc, + **)
-
-local
-
-val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
-val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
-
-in
-
-fun mk_sum [] = HOLogic.zero
- | mk_sum [t] = t
- | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
-
-(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
-fun mk_norm_sum ts =
- let val (ones, sums) = List.partition (equal HOLogic.Suc_zero) ts in
- funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
- end;
-
-
-fun dest_sum tm =
- if HOLogic.is_zero tm then []
- else
- (case try HOLogic.dest_Suc tm of
- SOME t => HOLogic.Suc_zero :: dest_sum t
- | NONE =>
- (case try dest_plus tm of
- SOME (t, u) => dest_sum t @ dest_sum u
- | NONE => [tm]));
+fun prep_simproc (name, pats, proc) = (*FIXME avoid the_context*)
+ Simplifier.simproc (the_context ()) name pats proc;
end;
-
-
-(** cancel common summands **)
-
-structure Sum =
-struct
- val mk_sum = mk_norm_sum;
- val dest_sum = dest_sum;
- val prove_conv = prove_conv;
- val norm_tac1 = simp_all_tac [@{thm "add_Suc"}, @{thm "add_Suc_right"},
- @{thm "add_0"}, @{thm "add_0_right"}];
- val norm_tac2 = simp_all_tac @{thms add_ac};
- fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
-end;
-
-fun gen_uncancel_tac rule ct =
- rtac (instantiate' [] [NONE, SOME ct] (rule RS @{thm subst_equals})) 1;
-
-
-(* nat eq *)
-
-structure EqCancelSums = CancelSumsFun
-(struct
- open Sum;
- val mk_bal = HOLogic.mk_eq;
- val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
- val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
-end);
-
-
-(* nat less *)
-
-structure LessCancelSums = CancelSumsFun
-(struct
- open Sum;
- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less};
- val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT;
- val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
-end);
-
-
-(* nat le *)
-
-structure LeCancelSums = CancelSumsFun
-(struct
- open Sum;
- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq};
- val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT;
- val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
-end);
-
-
-(* nat diff *)
-
-structure DiffCancelSums = CancelSumsFun
-(struct
- open Sum;
- val mk_bal = HOLogic.mk_binop @{const_name HOL.minus};
- val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT;
- val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
-end);
-
-
-(* prepare nat_cancel simprocs *)
-
-val nat_cancel_sums_add =
- [Simplifier.simproc (the_context ()) "nateq_cancel_sums"
- ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
- (K EqCancelSums.proc),
- Simplifier.simproc (the_context ()) "natless_cancel_sums"
- ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
- (K LessCancelSums.proc),
- Simplifier.simproc (the_context ()) "natle_cancel_sums"
- ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
- (K LeCancelSums.proc)];
-
-val nat_cancel_sums = nat_cancel_sums_add @
- [Simplifier.simproc (the_context ()) "natdiff_cancel_sums"
- ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
- (K DiffCancelSums.proc)];
-
-val setup =
- Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums);
-
-end;
--- a/src/HOL/Tools/int_arith.ML Fri Mar 13 15:50:06 2009 +0100
+++ b/src/HOL/Tools/int_arith.ML Fri Mar 13 15:52:23 2009 +0100
@@ -1,59 +1,32 @@
-(* Title: HOL/Tools/int_arith1.ML
- Authors: Larry Paulson and Tobias Nipkow
-
-Simprocs and decision procedure for linear arithmetic.
-*)
-
-structure Int_Numeral_Base_Simprocs =
- struct
- fun prove_conv tacs ctxt (_: thm list) (t, u) =
- if t aconv u then NONE
- else
- let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
- in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end
-
- fun prove_conv_nohyps tacs sg = prove_conv tacs sg [];
-
- fun prep_simproc (name, pats, proc) =
- Simplifier.simproc (the_context()) name pats proc;
-
- fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true
- | is_numeral _ = false
-
- fun simplify_meta_eq f_number_of_eq f_eq =
- mk_meta_eq ([f_eq, f_number_of_eq] MRS trans)
+(* Authors: Larry Paulson and Tobias Nipkow
- (*reorientation simprules using ==, for the following simproc*)
- val meta_zero_reorient = @{thm zero_reorient} RS eq_reflection
- val meta_one_reorient = @{thm one_reorient} RS eq_reflection
- val meta_number_of_reorient = @{thm number_of_reorient} RS eq_reflection
-
- (*reorientation simplification procedure: reorients (polymorphic)
- 0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a Int.*)
- fun reorient_proc sg _ (_ $ t $ u) =
- case u of
- Const(@{const_name HOL.zero}, _) => NONE
- | Const(@{const_name HOL.one}, _) => NONE
- | Const(@{const_name Int.number_of}, _) $ _ => NONE
- | _ => SOME (case t of
- Const(@{const_name HOL.zero}, _) => meta_zero_reorient
- | Const(@{const_name HOL.one}, _) => meta_one_reorient
- | Const(@{const_name Int.number_of}, _) $ _ => meta_number_of_reorient)
-
- val reorient_simproc =
- prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc)
-
- end;
-
-
-Addsimprocs [Int_Numeral_Base_Simprocs.reorient_simproc];
-
+Simprocs and decision procedure for numerals and linear arithmetic.
+*)
structure Int_Numeral_Simprocs =
struct
-(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in Int_Numeral_Base_Simprocs
- isn't complicated by the abstract 0 and 1.*)
+(*reorientation simprules using ==, for the following simproc*)
+val meta_zero_reorient = @{thm zero_reorient} RS eq_reflection
+val meta_one_reorient = @{thm one_reorient} RS eq_reflection
+val meta_number_of_reorient = @{thm number_of_reorient} RS eq_reflection
+
+(*reorientation simplification procedure: reorients (polymorphic)
+ 0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a Int.*)
+fun reorient_proc sg _ (_ $ t $ u) =
+ case u of
+ Const(@{const_name HOL.zero}, _) => NONE
+ | Const(@{const_name HOL.one}, _) => NONE
+ | Const(@{const_name Int.number_of}, _) $ _ => NONE
+ | _ => SOME (case t of
+ Const(@{const_name HOL.zero}, _) => meta_zero_reorient
+ | Const(@{const_name HOL.one}, _) => meta_one_reorient
+ | Const(@{const_name Int.number_of}, _) $ _ => meta_number_of_reorient)
+
+val reorient_simproc =
+ Arith_Data.prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc);
+
+(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];
(** New term ordering so that AC-rewriting brings numerals to the front **)
@@ -88,7 +61,7 @@
fun numtermless tu = (numterm_ord tu = LESS);
-(*Defined in this file, but perhaps needed only for Int_Numeral_Base_Simprocs of type nat.*)
+(*Defined in this file, but perhaps needed only for Int_Numeral_Simprocs of type nat.*)
val num_ss = HOL_ss settermless numtermless;
@@ -213,7 +186,7 @@
val divide_1s = [@{thm divide_numeral_1}];
(*To perform binary arithmetic. The "left" rewriting handles patterns
- created by the Int_Numeral_Base_Simprocs, such as 3 * (5 * x). *)
+ created by the Int_Numeral_Simprocs, such as 3 * (5 * x). *)
val simps = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym,
@{thm add_number_of_left}, @{thm mult_number_of_left}] @
@{thms arith_simps} @ @{thms rel_simps};
@@ -279,7 +252,7 @@
structure EqCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
val bal_add1 = @{thm eq_add_iff1} RS trans
@@ -288,7 +261,7 @@
structure LessCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
val bal_add1 = @{thm less_add_iff1} RS trans
@@ -297,7 +270,7 @@
structure LeCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
val bal_add1 = @{thm le_add_iff1} RS trans
@@ -305,7 +278,7 @@
);
val cancel_numerals =
- map Int_Numeral_Base_Simprocs.prep_simproc
+ map Arith_Data.prep_simproc
[("inteq_cancel_numerals",
["(l::'a::number_ring) + m = n",
"(l::'a::number_ring) = m + n",
@@ -342,7 +315,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
val left_distrib = @{thm combine_common_factor} RS trans
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv_nohyps
+ val prove_conv = Arith_Data.prove_conv_nohyps
val trans_tac = fn _ => trans_tac
val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
@@ -372,7 +345,7 @@
val mk_coeff = mk_fcoeff
val dest_coeff = dest_fcoeff 1
val left_distrib = @{thm combine_common_factor} RS trans
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv_nohyps
+ val prove_conv = Arith_Data.prove_conv_nohyps
val trans_tac = fn _ => trans_tac
val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
@@ -392,23 +365,42 @@
structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);
val combine_numerals =
- Int_Numeral_Base_Simprocs.prep_simproc
+ Arith_Data.prep_simproc
("int_combine_numerals",
["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"],
K CombineNumerals.proc);
val field_combine_numerals =
- Int_Numeral_Base_Simprocs.prep_simproc
+ Arith_Data.prep_simproc
("field_combine_numerals",
["(i::'a::{number_ring,field,division_by_zero}) + j",
"(i::'a::{number_ring,field,division_by_zero}) - j"],
K FieldCombineNumerals.proc);
+(** Constant folding for multiplication in semirings **)
+
+(*We do not need folding for addition: combine_numerals does the same thing*)
+
+structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
+struct
+ val assoc_ss = HOL_ss addsimps @{thms mult_ac}
+ val eq_reflection = eq_reflection
end;
+structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
+
+val assoc_fold_simproc =
+ Arith_Data.prep_simproc
+ ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
+ K Semiring_Times_Assoc.proc);
+
+end;
+
+Addsimprocs [Int_Numeral_Simprocs.reorient_simproc];
Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
Addsimprocs [Int_Numeral_Simprocs.combine_numerals];
Addsimprocs [Int_Numeral_Simprocs.field_combine_numerals];
+Addsimprocs [Int_Numeral_Simprocs.assoc_fold_simproc];
(*examples:
print_depth 22;
@@ -447,29 +439,6 @@
test "(i + j + -12 + (k::int)) - -15 = y";
*)
-
-(** Constant folding for multiplication in semirings **)
-
-(*We do not need folding for addition: combine_numerals does the same thing*)
-
-structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
-struct
- val assoc_ss = HOL_ss addsimps @{thms mult_ac}
- val eq_reflection = eq_reflection
-end;
-
-structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
-
-val assoc_fold_simproc =
- Int_Numeral_Base_Simprocs.prep_simproc
- ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
- K Semiring_Times_Assoc.proc);
-
-Addsimprocs [assoc_fold_simproc];
-
-
-
-
(*** decision procedure for linear arithmetic ***)
(*---------------------------------------------------------------------------*)
@@ -480,8 +449,10 @@
Instantiation of the generic linear arithmetic package for int.
*)
+structure Int_Arith =
+struct
+
(* Update parameters of arithmetic prover *)
-local
(* reduce contradictory =/</<= to False *)
@@ -489,25 +460,31 @@
and m and n are ground terms over rings (roughly speaking).
That is, m and n consist only of 1s combined with "+", "-" and "*".
*)
-local
+
val zeroth = (symmetric o mk_meta_eq) @{thm of_int_0};
+
val lhss0 = [@{cpat "0::?'a::ring"}];
+
fun proc0 phi ss ct =
let val T = ctyp_of_term ct
in if typ_of T = @{typ int} then NONE else
SOME (instantiate' [SOME T] [] zeroth)
end;
+
val zero_to_of_int_zero_simproc =
make_simproc {lhss = lhss0, name = "zero_to_of_int_zero_simproc",
proc = proc0, identifier = []};
val oneth = (symmetric o mk_meta_eq) @{thm of_int_1};
+
val lhss1 = [@{cpat "1::?'a::ring_1"}];
+
fun proc1 phi ss ct =
let val T = ctyp_of_term ct
in if typ_of T = @{typ int} then NONE else
SOME (instantiate' [SOME T] [] oneth)
end;
+
val one_to_of_int_one_simproc =
make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
proc = proc1, identifier = []};
@@ -533,15 +510,15 @@
addsimprocs [zero_to_of_int_zero_simproc,one_to_of_int_one_simproc]);
fun sproc phi ss ct = if check (term_of ct) then SOME (conv ct) else NONE
+
val lhss' =
[@{cpat "(?x::?'a::ring_char_0) = (?y::?'a)"},
@{cpat "(?x::?'a::ordered_idom) < (?y::?'a)"},
@{cpat "(?x::?'a::ordered_idom) <= (?y::?'a)"}]
-in
+
val zero_one_idom_simproc =
make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
proc = sproc, identifier = []}
-end;
val add_rules =
simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @
@@ -556,13 +533,11 @@
val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
-val Int_Numeral_Base_Simprocs = assoc_fold_simproc :: zero_one_idom_simproc
+val int_numeral_base_simprocs = Int_Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
:: Int_Numeral_Simprocs.combine_numerals
:: Int_Numeral_Simprocs.cancel_numerals;
-in
-
-val int_arith_setup =
+val setup =
LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
{add_mono_thms = add_mono_thms,
mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
@@ -570,13 +545,11 @@
lessD = lessD @ [@{thm zless_imp_add1_zle}],
neqE = neqE,
simpset = simpset addsimps add_rules
- addsimprocs Int_Numeral_Base_Simprocs
+ addsimprocs int_numeral_base_simprocs
addcongs [if_weak_cong]}) #>
arith_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
arith_discrete @{type_name Int.int}
-end;
-
val fast_int_arith_simproc =
Simplifier.simproc (the_context ())
"fast_int_arith"
@@ -584,4 +557,6 @@
"(m::'a::{ordered_idom,number_ring}) <= n",
"(m::'a::{ordered_idom,number_ring}) = n"] (K LinArith.lin_arith_simproc);
-Addsimprocs [fast_int_arith_simproc];
+end;
+
+Addsimprocs [Int_Arith.fast_int_arith_simproc];
--- a/src/HOL/Tools/int_factor_simprocs.ML Fri Mar 13 15:50:06 2009 +0100
+++ b/src/HOL/Tools/int_factor_simprocs.ML Fri Mar 13 15:52:23 2009 +0100
@@ -49,7 +49,7 @@
(*Version for integer division*)
structure IntDivCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
val cancel = @{thm zdiv_zmult_zmult1} RS trans
@@ -59,7 +59,7 @@
(*Version for fields*)
structure DivideCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name HOL.divide}
val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
val cancel = @{thm mult_divide_mult_cancel_left} RS trans
@@ -68,7 +68,7 @@
structure EqCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
val cancel = @{thm mult_cancel_left} RS trans
@@ -77,7 +77,7 @@
structure LessCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
val cancel = @{thm mult_less_cancel_left} RS trans
@@ -86,7 +86,7 @@
structure LeCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
val cancel = @{thm mult_le_cancel_left} RS trans
@@ -94,7 +94,7 @@
)
val cancel_numeral_factors =
- map Int_Numeral_Base_Simprocs.prep_simproc
+ map Arith_Data.prep_simproc
[("ring_eq_cancel_numeral_factor",
["(l::'a::{idom,number_ring}) * m = n",
"(l::'a::{idom,number_ring}) = m * n"],
@@ -118,7 +118,7 @@
(* referenced by rat_arith.ML *)
val field_cancel_numeral_factors =
- map Int_Numeral_Base_Simprocs.prep_simproc
+ map Arith_Data.prep_simproc
[("field_eq_cancel_numeral_factor",
["(l::'a::{field,number_ring}) * m = n",
"(l::'a::{field,number_ring}) = m * n"],
@@ -236,7 +236,7 @@
(*mult_cancel_left requires a ring with no zero divisors.*)
structure EqCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
val simplify_meta_eq = cancel_simplify_meta_eq @{thm mult_cancel_left}
@@ -245,7 +245,7 @@
(*zdiv_zmult_zmult1_if is for integer division (div).*)
structure IntDivCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
val simplify_meta_eq = cancel_simplify_meta_eq @{thm zdiv_zmult_zmult1_if}
@@ -253,7 +253,7 @@
structure IntModCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name Divides.mod}
val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} HOLogic.intT
val simplify_meta_eq = cancel_simplify_meta_eq @{thm zmod_zmult_zmult1}
@@ -261,7 +261,7 @@
structure IntDvdCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT
val simplify_meta_eq = cancel_simplify_meta_eq @{thm dvd_mult_cancel_left}
@@ -270,14 +270,14 @@
(*Version for all fields, including unordered ones (type complex).*)
structure DivideCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name HOL.divide}
val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
val simplify_meta_eq = cancel_simplify_meta_eq @{thm mult_divide_mult_cancel_left_if}
);
val cancel_factors =
- map Int_Numeral_Base_Simprocs.prep_simproc
+ map Arith_Data.prep_simproc
[("ring_eq_cancel_factor",
["(l::'a::{idom}) * m = n",
"(l::'a::{idom}) = m * n"],
--- a/src/HOL/Tools/lin_arith.ML Fri Mar 13 15:50:06 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML Fri Mar 13 15:52:23 2009 +0100
@@ -811,7 +811,7 @@
@{thm "not_one_less_zero"}]
addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
(*abel_cancel helps it work in abstract algebraic domains*)
- addsimprocs ArithData.nat_cancel_sums_add}) #>
+ addsimprocs Nat_Arith.nat_cancel_sums_add}) #>
arith_discrete "nat";
fun add_arith_facts ss =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/nat_arith.ML Fri Mar 13 15:52:23 2009 +0100
@@ -0,0 +1,112 @@
+(* Author: Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
+
+Basic arithmetic for natural numbers.
+*)
+
+signature NAT_ARITH =
+sig
+ val mk_sum: term list -> term
+ val mk_norm_sum: term list -> term
+ val dest_sum: term -> term list
+
+ val nat_cancel_sums_add: simproc list
+ val nat_cancel_sums: simproc list
+ val setup: Context.generic -> Context.generic
+end;
+
+structure Nat_Arith: NAT_ARITH =
+struct
+
+(** abstract syntax of structure nat: 0, Suc, + **)
+
+val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
+val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
+
+fun mk_sum [] = HOLogic.zero
+ | mk_sum [t] = t
+ | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+
+(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
+fun mk_norm_sum ts =
+ let val (ones, sums) = List.partition (equal HOLogic.Suc_zero) ts in
+ funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
+ end;
+
+fun dest_sum tm =
+ if HOLogic.is_zero tm then []
+ else
+ (case try HOLogic.dest_Suc tm of
+ SOME t => HOLogic.Suc_zero :: dest_sum t
+ | NONE =>
+ (case try dest_plus tm of
+ SOME (t, u) => dest_sum t @ dest_sum u
+ | NONE => [tm]));
+
+
+(** cancel common summands **)
+
+structure CommonCancelSums =
+struct
+ val mk_sum = mk_norm_sum;
+ val dest_sum = dest_sum;
+ val prove_conv = Arith_Data.prove_conv2;
+ val norm_tac1 = Arith_Data.simp_all_tac [@{thm "add_Suc"}, @{thm "add_Suc_right"},
+ @{thm "add_0"}, @{thm "add_0_right"}];
+ val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac};
+ fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
+ fun gen_uncancel_tac rule = let val rule' = rule RS @{thm subst_equals}
+ in fn ct => rtac (instantiate' [] [NONE, SOME ct] rule') 1 end;
+end;
+
+structure EqCancelSums = CancelSumsFun
+(struct
+ open CommonCancelSums;
+ val mk_bal = HOLogic.mk_eq;
+ val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
+ val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
+end);
+
+structure LessCancelSums = CancelSumsFun
+(struct
+ open CommonCancelSums;
+ val mk_bal = HOLogic.mk_binrel @{const_name HOL.less};
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT;
+ val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
+end);
+
+structure LeCancelSums = CancelSumsFun
+(struct
+ open CommonCancelSums;
+ val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq};
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT;
+ val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
+end);
+
+structure DiffCancelSums = CancelSumsFun
+(struct
+ open CommonCancelSums;
+ val mk_bal = HOLogic.mk_binop @{const_name HOL.minus};
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT;
+ val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
+end);
+
+val nat_cancel_sums_add =
+ [Simplifier.simproc (the_context ()) "nateq_cancel_sums"
+ ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
+ (K EqCancelSums.proc),
+ Simplifier.simproc (the_context ()) "natless_cancel_sums"
+ ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
+ (K LessCancelSums.proc),
+ Simplifier.simproc (the_context ()) "natle_cancel_sums"
+ ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
+ (K LeCancelSums.proc)];
+
+val nat_cancel_sums = nat_cancel_sums_add @
+ [Simplifier.simproc (the_context ()) "natdiff_cancel_sums"
+ ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
+ (K DiffCancelSums.proc)];
+
+val setup =
+ Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums);
+
+end;
--- a/src/HOL/Tools/nat_simprocs.ML Fri Mar 13 15:50:06 2009 +0100
+++ b/src/HOL/Tools/nat_simprocs.ML Fri Mar 13 15:52:23 2009 +0100
@@ -8,8 +8,7 @@
struct
(*Maps n to #n for n = 0, 1, 2*)
-val numeral_syms =
- [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym];
+val numeral_syms = [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym];
val numeral_sym_ss = HOL_ss addsimps numeral_syms;
fun rename_numerals th =
@@ -53,9 +52,6 @@
@{thm Let_number_of}, @{thm nat_number_of}] @
@{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps};
-fun prep_simproc (name, pats, proc) =
- Simplifier.simproc (the_context ()) name pats proc;
-
(*** CancelNumerals simprocs ***)
@@ -169,7 +165,7 @@
structure EqCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
val bal_add1 = @{thm nat_eq_add_iff1} RS trans
@@ -178,7 +174,7 @@
structure LessCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
val bal_add1 = @{thm nat_less_add_iff1} RS trans
@@ -187,7 +183,7 @@
structure LeCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
val bal_add1 = @{thm nat_le_add_iff1} RS trans
@@ -196,7 +192,7 @@
structure DiffCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name HOL.minus}
val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT
val bal_add1 = @{thm nat_diff_add_eq1} RS trans
@@ -205,7 +201,7 @@
val cancel_numerals =
- map prep_simproc
+ map Arith_Data.prep_simproc
[("nateq_cancel_numerals",
["(l::nat) + m = n", "(l::nat) = m + n",
"(l::nat) * m = n", "(l::nat) = m * n",
@@ -240,7 +236,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val left_distrib = @{thm left_add_mult_distrib} RS trans
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv_nohyps
+ val prove_conv = Arith_Data.prove_conv_nohyps
val trans_tac = fn _ => trans_tac
val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
@@ -257,7 +253,7 @@
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
val combine_numerals =
- prep_simproc ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc);
+ Arith_Data.prep_simproc ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc);
(*** Applying CancelNumeralFactorFun ***)
@@ -282,7 +278,7 @@
structure DivCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
val cancel = @{thm nat_mult_div_cancel1} RS trans
@@ -291,7 +287,7 @@
structure DvdCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
val cancel = @{thm nat_mult_dvd_cancel1} RS trans
@@ -300,7 +296,7 @@
structure EqCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
val cancel = @{thm nat_mult_eq_cancel1} RS trans
@@ -309,7 +305,7 @@
structure LessCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
val cancel = @{thm nat_mult_less_cancel1} RS trans
@@ -318,7 +314,7 @@
structure LeCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
val cancel = @{thm nat_mult_le_cancel1} RS trans
@@ -326,7 +322,7 @@
)
val cancel_numeral_factors =
- map prep_simproc
+ map Arith_Data.prep_simproc
[("nateq_cancel_numeral_factors",
["(l::nat) * m = n", "(l::nat) = m * n"],
K EqCancelNumeralFactor.proc),
@@ -379,7 +375,7 @@
structure EqCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_eq_cancel_disj}
@@ -387,7 +383,7 @@
structure LessCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_less_cancel_disj}
@@ -395,7 +391,7 @@
structure LeCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_le_cancel_disj}
@@ -403,7 +399,7 @@
structure DivideCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_div_cancel_disj}
@@ -411,14 +407,14 @@
structure DvdCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+ val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_dvd_cancel_disj}
);
val cancel_factor =
- map prep_simproc
+ map Arith_Data.prep_simproc
[("nat_eq_cancel_factor",
["(l::nat) * m = n", "(l::nat) = m * n"],
K EqCancelFactor.proc),
--- a/src/HOL/Tools/rat_arith.ML Fri Mar 13 15:50:06 2009 +0100
+++ b/src/HOL/Tools/rat_arith.ML Fri Mar 13 15:52:23 2009 +0100
@@ -34,8 +34,6 @@
in
-val ratT = Type ("Rational.rat", [])
-
val rat_arith_setup =
LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
{add_mono_thms = add_mono_thms,
@@ -45,7 +43,7 @@
neqE = neqE,
simpset = simpset addsimps simps
addsimprocs simprocs}) #>
- arith_inj_const (@{const_name of_nat}, HOLogic.natT --> ratT) #>
- arith_inj_const (@{const_name of_int}, HOLogic.intT --> ratT)
+ arith_inj_const (@{const_name of_nat}, @{typ "nat => rat"}) #>
+ arith_inj_const (@{const_name of_int}, @{typ "int => rat"})
end;
--- a/src/HOLCF/Universal.thy Fri Mar 13 15:50:06 2009 +0100
+++ b/src/HOLCF/Universal.thy Fri Mar 13 15:52:23 2009 +0100
@@ -13,35 +13,35 @@
definition
node :: "nat \<Rightarrow> ubasis \<Rightarrow> ubasis set \<Rightarrow> ubasis"
where
- "node i x A = Suc (prod2nat (i, prod2nat (x, set2nat A)))"
+ "node i a S = Suc (prod2nat (i, prod2nat (a, set2nat S)))"
-lemma node_not_0 [simp]: "node i x A \<noteq> 0"
+lemma node_not_0 [simp]: "node i a S \<noteq> 0"
unfolding node_def by simp
-lemma node_gt_0 [simp]: "0 < node i x A"
+lemma node_gt_0 [simp]: "0 < node i a S"
unfolding node_def by simp
lemma node_inject [simp]:
- "\<lbrakk>finite A; finite B\<rbrakk>
- \<Longrightarrow> node i x A = node j y B \<longleftrightarrow> i = j \<and> x = y \<and> A = B"
+ "\<lbrakk>finite S; finite T\<rbrakk>
+ \<Longrightarrow> node i a S = node j b T \<longleftrightarrow> i = j \<and> a = b \<and> S = T"
unfolding node_def by simp
-lemma node_gt0: "i < node i x A"
+lemma node_gt0: "i < node i a S"
unfolding node_def less_Suc_eq_le
by (rule le_prod2nat_1)
-lemma node_gt1: "x < node i x A"
+lemma node_gt1: "a < node i a S"
unfolding node_def less_Suc_eq_le
by (rule order_trans [OF le_prod2nat_1 le_prod2nat_2])
lemma nat_less_power2: "n < 2^n"
by (induct n) simp_all
-lemma node_gt2: "\<lbrakk>finite A; y \<in> A\<rbrakk> \<Longrightarrow> y < node i x A"
+lemma node_gt2: "\<lbrakk>finite S; b \<in> S\<rbrakk> \<Longrightarrow> b < node i a S"
unfolding node_def less_Suc_eq_le set2nat_def
apply (rule order_trans [OF _ le_prod2nat_2])
apply (rule order_trans [OF _ le_prod2nat_2])
-apply (rule order_trans [where y="setsum (op ^ 2) {y}"])
+apply (rule order_trans [where y="setsum (op ^ 2) {b}"])
apply (simp add: nat_less_power2 [THEN order_less_imp_le])
apply (erule setsum_mono2, simp, simp)
done
@@ -52,7 +52,7 @@
lemma node_cases:
assumes 1: "x = 0 \<Longrightarrow> P"
- assumes 2: "\<And>i y A. \<lbrakk>finite A; x = node i y A\<rbrakk> \<Longrightarrow> P"
+ assumes 2: "\<And>i a S. \<lbrakk>finite S; x = node i a S\<rbrakk> \<Longrightarrow> P"
shows "P"
apply (cases x)
apply (erule 1)
@@ -65,7 +65,7 @@
lemma node_induct:
assumes 1: "P 0"
- assumes 2: "\<And>i x A. \<lbrakk>P x; finite A; \<forall>y\<in>A. P y\<rbrakk> \<Longrightarrow> P (node i x A)"
+ assumes 2: "\<And>i a S. \<lbrakk>P a; finite S; \<forall>b\<in>S. P b\<rbrakk> \<Longrightarrow> P (node i a S)"
shows "P x"
apply (induct x rule: nat_less_induct)
apply (case_tac n rule: node_cases)
@@ -78,13 +78,13 @@
inductive
ubasis_le :: "nat \<Rightarrow> nat \<Rightarrow> bool"
where
- ubasis_le_refl: "ubasis_le x x"
+ ubasis_le_refl: "ubasis_le a a"
| ubasis_le_trans:
- "\<lbrakk>ubasis_le x y; ubasis_le y z\<rbrakk> \<Longrightarrow> ubasis_le x z"
+ "\<lbrakk>ubasis_le a b; ubasis_le b c\<rbrakk> \<Longrightarrow> ubasis_le a c"
| ubasis_le_lower:
- "finite A \<Longrightarrow> ubasis_le x (node i x A)"
+ "finite S \<Longrightarrow> ubasis_le a (node i a S)"
| ubasis_le_upper:
- "\<lbrakk>finite A; y \<in> A; ubasis_le x y\<rbrakk> \<Longrightarrow> ubasis_le (node i x A) y"
+ "\<lbrakk>finite S; b \<in> S; ubasis_le a b\<rbrakk> \<Longrightarrow> ubasis_le (node i a S) b"
lemma ubasis_le_minimal: "ubasis_le 0 x"
apply (induct x rule: node_induct)
@@ -99,8 +99,8 @@
ubasis_until :: "(ubasis \<Rightarrow> bool) \<Rightarrow> ubasis \<Rightarrow> ubasis"
where
"ubasis_until P 0 = 0"
-| "finite A \<Longrightarrow> ubasis_until P (node i x A) =
- (if P (node i x A) then node i x A else ubasis_until P x)"
+| "finite S \<Longrightarrow> ubasis_until P (node i a S) =
+ (if P (node i a S) then node i a S else ubasis_until P a)"
apply clarify
apply (rule_tac x=b in node_cases)
apply simp
@@ -157,8 +157,8 @@
done
lemma ubasis_until_mono:
- assumes "\<And>i x A y. \<lbrakk>finite A; P (node i x A); y \<in> A; ubasis_le x y\<rbrakk> \<Longrightarrow> P y"
- shows "ubasis_le x y \<Longrightarrow> ubasis_le (ubasis_until P x) (ubasis_until P y)"
+ assumes "\<And>i a S b. \<lbrakk>finite S; P (node i a S); b \<in> S; ubasis_le a b\<rbrakk> \<Longrightarrow> P b"
+ shows "ubasis_le a b \<Longrightarrow> ubasis_le (ubasis_until P a) (ubasis_until P b)"
apply (induct set: ubasis_le)
apply (rule ubasis_le_refl)
apply (erule (1) ubasis_le_trans)
@@ -510,6 +510,12 @@
lemma rank_le_iff: "rank x \<le> n \<longleftrightarrow> cb_take n x = x"
by (rule iffI [OF rank_leD rank_leI])
+lemma rank_compact_bot [simp]: "rank compact_bot = 0"
+using rank_leI [of 0 compact_bot] by simp
+
+lemma rank_eq_0_iff [simp]: "rank x = 0 \<longleftrightarrow> x = compact_bot"
+using rank_le_iff [of x 0] by auto
+
definition
rank_le :: "'a compact_basis \<Rightarrow> 'a compact_basis set"
where
@@ -558,15 +564,15 @@
lemma rank_lt_Un_rank_eq: "rank_lt x \<union> rank_eq x = rank_le x"
unfolding rank_lt_def rank_eq_def rank_le_def by auto
-subsubsection {* Reordering of basis elements *}
+subsubsection {* Sequencing basis elements *}
definition
- reorder :: "'a compact_basis \<Rightarrow> nat"
+ place :: "'a compact_basis \<Rightarrow> nat"
where
- "reorder x = card (rank_lt x) + choose_pos (rank_eq x) x"
+ "place x = card (rank_lt x) + choose_pos (rank_eq x) x"
-lemma reorder_bounded: "reorder x < card (rank_le x)"
-unfolding reorder_def
+lemma place_bounded: "place x < card (rank_le x)"
+unfolding place_def
apply (rule ord_less_eq_trans)
apply (rule add_strict_left_mono)
apply (rule choose_pos_bounded)
@@ -579,53 +585,77 @@
apply (simp add: rank_lt_Un_rank_eq)
done
-lemma reorder_ge: "card (rank_lt x) \<le> reorder x"
-unfolding reorder_def by simp
+lemma place_ge: "card (rank_lt x) \<le> place x"
+unfolding place_def by simp
-lemma reorder_rank_mono:
+lemma place_rank_mono:
fixes x y :: "'a compact_basis"
- shows "rank x < rank y \<Longrightarrow> reorder x < reorder y"
-apply (rule less_le_trans [OF reorder_bounded])
-apply (rule order_trans [OF _ reorder_ge])
+ shows "rank x < rank y \<Longrightarrow> place x < place y"
+apply (rule less_le_trans [OF place_bounded])
+apply (rule order_trans [OF _ place_ge])
apply (rule card_mono)
apply (rule finite_rank_lt)
apply (simp add: rank_le_def rank_lt_def subset_eq)
done
-lemma reorder_eqD: "reorder x = reorder y \<Longrightarrow> x = y"
+lemma place_eqD: "place x = place y \<Longrightarrow> x = y"
apply (rule linorder_cases [where x="rank x" and y="rank y"])
- apply (drule reorder_rank_mono, simp)
- apply (simp add: reorder_def)
+ apply (drule place_rank_mono, simp)
+ apply (simp add: place_def)
apply (rule inj_on_choose_pos [where A="rank_eq x", THEN inj_onD])
apply (rule finite_rank_eq)
apply (simp cong: rank_lt_cong rank_eq_cong)
apply (simp add: rank_eq_def)
apply (simp add: rank_eq_def)
- apply (drule reorder_rank_mono, simp)
+ apply (drule place_rank_mono, simp)
done
-lemma inj_reorder: "inj reorder"
-by (rule inj_onI, erule reorder_eqD)
+lemma inj_place: "inj place"
+by (rule inj_onI, erule place_eqD)
subsubsection {* Embedding and projection on basis elements *}
+definition
+ sub :: "'a compact_basis \<Rightarrow> 'a compact_basis"
+where
+ "sub x = (case rank x of 0 \<Rightarrow> compact_bot | Suc k \<Rightarrow> cb_take k x)"
+
+lemma rank_sub_less: "x \<noteq> compact_bot \<Longrightarrow> rank (sub x) < rank x"
+unfolding sub_def
+apply (cases "rank x", simp)
+apply (simp add: less_Suc_eq_le)
+apply (rule rank_leI)
+apply (rule cb_take_idem)
+done
+
+lemma place_sub_less: "x \<noteq> compact_bot \<Longrightarrow> place (sub x) < place x"
+apply (rule place_rank_mono)
+apply (erule rank_sub_less)
+done
+
+lemma sub_below: "sub x \<sqsubseteq> x"
+unfolding sub_def by (cases "rank x", simp_all add: cb_take_less)
+
+lemma rank_less_imp_below_sub: "\<lbrakk>x \<sqsubseteq> y; rank x < rank y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> sub y"
+unfolding sub_def
+apply (cases "rank y", simp)
+apply (simp add: less_Suc_eq_le)
+apply (subgoal_tac "cb_take nat x \<sqsubseteq> cb_take nat y")
+apply (simp add: rank_leD)
+apply (erule cb_take_mono)
+done
+
function
basis_emb :: "'a compact_basis \<Rightarrow> ubasis"
where
"basis_emb x = (if x = compact_bot then 0 else
- node
- (reorder x)
- (case rank x of 0 \<Rightarrow> 0 | Suc k \<Rightarrow> basis_emb (cb_take k x))
- (basis_emb ` {y. reorder y < reorder x \<and> x \<sqsubseteq> y}))"
+ node (place x) (basis_emb (sub x))
+ (basis_emb ` {y. place y < place x \<and> x \<sqsubseteq> y}))"
by auto
termination basis_emb
-apply (relation "measure reorder", simp)
-apply simp
-apply (rule reorder_rank_mono)
-apply (simp add: less_Suc_eq_le)
-apply (rule rank_leI)
-apply (rule cb_take_idem)
+apply (relation "measure place", simp)
+apply (simp add: place_sub_less)
apply simp
done
@@ -634,101 +664,68 @@
lemma basis_emb_compact_bot [simp]: "basis_emb compact_bot = 0"
by (simp add: basis_emb.simps)
-lemma fin1: "finite {y. reorder y < reorder x \<and> x \<sqsubseteq> y}"
+lemma fin1: "finite {y. place y < place x \<and> x \<sqsubseteq> y}"
apply (subst Collect_conj_eq)
apply (rule finite_Int)
apply (rule disjI1)
-apply (subgoal_tac "finite (reorder -` {n. n < reorder x})", simp)
-apply (rule finite_vimageI [OF _ inj_reorder])
+apply (subgoal_tac "finite (place -` {n. n < place x})", simp)
+apply (rule finite_vimageI [OF _ inj_place])
apply (simp add: lessThan_def [symmetric])
done
-lemma fin2: "finite (basis_emb ` {y. reorder y < reorder x \<and> x \<sqsubseteq> y})"
+lemma fin2: "finite (basis_emb ` {y. place y < place x \<and> x \<sqsubseteq> y})"
by (rule finite_imageI [OF fin1])
-lemma basis_emb_mono [OF refl]:
- "\<lbrakk>n = max (reorder x) (reorder y); x \<sqsubseteq> y\<rbrakk>
- \<Longrightarrow> ubasis_le (basis_emb x) (basis_emb y)"
-proof (induct n arbitrary: x y rule: less_induct)
+lemma rank_place_mono:
+ "\<lbrakk>place x < place y; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> rank x < rank y"
+apply (rule linorder_cases, assumption)
+apply (simp add: place_def cong: rank_lt_cong rank_eq_cong)
+apply (drule choose_pos_lessD)
+apply (rule finite_rank_eq)
+apply (simp add: rank_eq_def)
+apply (simp add: rank_eq_def)
+apply simp
+apply (drule place_rank_mono, simp)
+done
+
+lemma basis_emb_mono:
+ "x \<sqsubseteq> y \<Longrightarrow> ubasis_le (basis_emb x) (basis_emb y)"
+proof (induct n \<equiv> "max (place x) (place y)" arbitrary: x y rule: less_induct)
case (less n)
- assume IH:
- "\<And>(m::nat) (x::'a compact_basis) y.
- \<lbrakk>m < n; m = max (reorder x) (reorder y); x \<sqsubseteq> y\<rbrakk>
- \<Longrightarrow> ubasis_le (basis_emb x) (basis_emb y)"
- assume n: "n = max (reorder x) (reorder y)"
- assume less: "x \<sqsubseteq> y"
- show ?case
- proof (cases)
- assume "x = compact_bot"
- thus ?case by (simp add: ubasis_le_minimal)
- next
- assume x_neq [simp]: "x \<noteq> compact_bot"
- with less have y_neq [simp]: "y \<noteq> compact_bot"
- apply clarify
- apply (drule antisym_less [OF compact_bot_minimal])
- apply simp
+ hence IH:
+ "\<And>(a::'a compact_basis) b.
+ \<lbrakk>max (place a) (place b) < max (place x) (place y); a \<sqsubseteq> b\<rbrakk>
+ \<Longrightarrow> ubasis_le (basis_emb a) (basis_emb b)"
+ by simp
+ show ?case proof (rule linorder_cases)
+ assume "place x < place y"
+ then have "rank x < rank y"
+ using `x \<sqsubseteq> y` by (rule rank_place_mono)
+ with `place x < place y` show ?case
+ apply (case_tac "y = compact_bot", simp)
+ apply (simp add: basis_emb.simps [of y])
+ apply (rule ubasis_le_trans [OF _ ubasis_le_lower [OF fin2]])
+ apply (rule IH)
+ apply (simp add: less_max_iff_disj)
+ apply (erule place_sub_less)
+ apply (erule rank_less_imp_below_sub [OF `x \<sqsubseteq> y`])
done
- show ?case
- proof (rule linorder_cases)
- assume 1: "reorder x < reorder y"
- show ?case
- proof (rule linorder_cases)
- assume "rank x < rank y"
- with 1 show ?case
- apply (case_tac "rank y", simp)
- apply (subst basis_emb.simps [where x=y])
- apply simp
- apply (rule ubasis_le_trans [OF _ ubasis_le_lower [OF fin2]])
- apply (rule IH [OF _ refl, unfolded n])
- apply (simp add: less_max_iff_disj)
- apply (rule reorder_rank_mono)
- apply (simp add: less_Suc_eq_le)
- apply (rule rank_leI)
- apply (rule cb_take_idem)
- apply (simp add: less_Suc_eq_le)
- apply (subgoal_tac "cb_take nat x \<sqsubseteq> cb_take nat y")
- apply (simp add: rank_leD)
- apply (rule cb_take_mono [OF less])
- done
- next
- assume "rank x = rank y"
- with 1 show ?case
- apply (simp add: reorder_def)
- apply (simp cong: rank_lt_cong rank_eq_cong)
- apply (drule choose_pos_lessD)
- apply (rule finite_rank_eq)
- apply (simp add: rank_eq_def)
- apply (simp add: rank_eq_def)
- apply (simp add: less)
- done
- next
- assume "rank x > rank y"
- hence "reorder x > reorder y"
- by (rule reorder_rank_mono)
- with 1 show ?case by simp
- qed
- next
- assume "reorder x = reorder y"
- hence "x = y" by (rule reorder_eqD)
- thus ?case by (simp add: ubasis_le_refl)
- next
- assume "reorder x > reorder y"
- with less show ?case
- apply (simp add: basis_emb.simps [where x=x])
- apply (rule ubasis_le_upper [OF fin2], simp)
- apply (cases "rank x")
- apply (simp add: ubasis_le_minimal)
- apply simp
- apply (rule IH [OF _ refl, unfolded n])
- apply (simp add: less_max_iff_disj)
- apply (rule reorder_rank_mono)
- apply (simp add: less_Suc_eq_le)
- apply (rule rank_leI)
- apply (rule cb_take_idem)
- apply (erule rev_trans_less)
- apply (rule cb_take_less)
- done
- qed
+ next
+ assume "place x = place y"
+ hence "x = y" by (rule place_eqD)
+ thus ?case by (simp add: ubasis_le_refl)
+ next
+ assume "place x > place y"
+ with `x \<sqsubseteq> y` show ?case
+ apply (case_tac "x = compact_bot", simp add: ubasis_le_minimal)
+ apply (simp add: basis_emb.simps [of x])
+ apply (rule ubasis_le_upper [OF fin2], simp)
+ apply (rule IH)
+ apply (simp add: less_max_iff_disj)
+ apply (erule place_sub_less)
+ apply (erule rev_trans_less)
+ apply (rule sub_below)
+ done
qed
qed
@@ -740,14 +737,14 @@
apply (simp add: basis_emb.simps)
apply (simp add: basis_emb.simps)
apply (simp add: basis_emb.simps)
- apply (simp add: fin2 inj_eq [OF inj_reorder])
+ apply (simp add: fin2 inj_eq [OF inj_place])
done
definition
- basis_prj :: "nat \<Rightarrow> 'a compact_basis"
+ basis_prj :: "ubasis \<Rightarrow> 'a compact_basis"
where
"basis_prj x = inv basis_emb
- (ubasis_until (\<lambda>x. x \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)) x)"
+ (ubasis_until (\<lambda>x. x \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> ubasis)) x)"
lemma basis_prj_basis_emb: "\<And>x. basis_prj (basis_emb x) = x"
unfolding basis_prj_def
@@ -758,8 +755,8 @@
done
lemma basis_prj_node:
- "\<lbrakk>finite A; node i x A \<notin> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)\<rbrakk>
- \<Longrightarrow> basis_prj (node i x A) = (basis_prj x :: 'a compact_basis)"
+ "\<lbrakk>finite S; node i a S \<notin> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)\<rbrakk>
+ \<Longrightarrow> basis_prj (node i a S) = (basis_prj a :: 'a compact_basis)"
unfolding basis_prj_def by simp
lemma basis_prj_0: "basis_prj 0 = compact_bot"
@@ -767,32 +764,41 @@
apply (rule basis_prj_basis_emb)
done
-lemma basis_prj_mono: "ubasis_le x y \<Longrightarrow> basis_prj x \<sqsubseteq> basis_prj y"
- apply (erule ubasis_le.induct)
- apply (rule refl_less)
- apply (erule (1) trans_less)
- apply (case_tac "node i x A \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)")
- apply (erule rangeE, rename_tac a)
- apply (case_tac "a = compact_bot", simp)
- apply (simp add: basis_prj_basis_emb)
- apply (simp add: basis_emb.simps)
- apply (clarsimp simp add: fin2)
- apply (case_tac "rank a", simp)
- apply (simp add: basis_prj_0)
- apply (simp add: basis_prj_basis_emb)
- apply (rule cb_take_less)
- apply (simp add: basis_prj_node)
- apply (case_tac "node i x A \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)")
- apply (erule rangeE, rename_tac a)
- apply (case_tac "a = compact_bot", simp)
- apply (simp add: basis_prj_basis_emb)
- apply (simp add: basis_emb.simps)
- apply (clarsimp simp add: fin2)
- apply (case_tac "rank a", simp add: basis_prj_basis_emb)
- apply (simp add: basis_prj_basis_emb)
- apply (simp add: basis_prj_node)
+lemma node_eq_basis_emb_iff:
+ "finite S \<Longrightarrow> node i a S = basis_emb x \<longleftrightarrow>
+ x \<noteq> compact_bot \<and> i = place x \<and> a = basis_emb (sub x) \<and>
+ S = basis_emb ` {y. place y < place x \<and> x \<sqsubseteq> y}"
+apply (cases "x = compact_bot", simp)
+apply (simp add: basis_emb.simps [of x])
+apply (simp add: fin2)
done
+lemma basis_prj_mono: "ubasis_le a b \<Longrightarrow> basis_prj a \<sqsubseteq> basis_prj b"
+proof (induct a b rule: ubasis_le.induct)
+ case (ubasis_le_refl a) show ?case by (rule refl_less)
+next
+ case (ubasis_le_trans a b c) thus ?case by - (rule trans_less)
+next
+ case (ubasis_le_lower S a i) thus ?case
+ apply (case_tac "node i a S \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)")
+ apply (erule rangeE, rename_tac x)
+ apply (simp add: basis_prj_basis_emb)
+ apply (simp add: node_eq_basis_emb_iff)
+ apply (simp add: basis_prj_basis_emb)
+ apply (rule sub_below)
+ apply (simp add: basis_prj_node)
+ done
+next
+ case (ubasis_le_upper S b a i) thus ?case
+ apply (case_tac "node i a S \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)")
+ apply (erule rangeE, rename_tac x)
+ apply (simp add: basis_prj_basis_emb)
+ apply (clarsimp simp add: node_eq_basis_emb_iff)
+ apply (simp add: basis_prj_basis_emb)
+ apply (simp add: basis_prj_node)
+ done
+qed
+
lemma basis_emb_prj_less: "ubasis_le (basis_emb (basis_prj x)) x"
unfolding basis_prj_def
apply (subst f_inv_f [where f=basis_emb])
@@ -806,7 +812,8 @@
node
choose
choose_pos
- reorder
+ place
+ sub
subsubsection {* EP-pair from any bifinite domain into @{typ udom} *}
--- a/src/Tools/code/code_target.ML Fri Mar 13 15:50:06 2009 +0100
+++ b/src/Tools/code/code_target.ML Fri Mar 13 15:52:23 2009 +0100
@@ -37,6 +37,7 @@
val string: string list -> serialization -> string
val code_of: theory -> string -> string
-> string list -> (Code_Thingol.naming -> string list) -> string
+ val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
val code_width: int ref
val allow_abort: string -> theory -> theory
@@ -527,13 +528,13 @@
val (inK, module_nameK, fileK) = ("in", "module_name", "file");
-fun code_exprP cmd =
+val code_exprP =
(Scan.repeat P.term_group
-- Scan.repeat (P.$$$ inK |-- P.name
-- Scan.option (P.$$$ module_nameK |-- P.name)
-- Scan.option (P.$$$ fileK |-- P.name)
-- Scan.optional (P.$$$ "(" |-- Args.parse --| P.$$$ ")") []
- ) >> (fn (raw_cs, seris) => cmd raw_cs seris));
+ ) >> (fn (raw_cs, seris) => export_code_cmd raw_cs seris));
val _ = List.app OuterKeyword.keyword [inK, module_nameK, fileK];
@@ -594,7 +595,14 @@
val _ =
OuterSyntax.command "export_code" "generate executable code for constants"
- K.diag (P.!!! (code_exprP export_code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
+ K.diag (P.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
+
+fun shell_command thyname cmd = Toplevel.program (fn _ =>
+ (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! code_exprP)
+ ((filter OuterLex.is_proper o OuterSyntax.scan Position.none) cmd)
+ of SOME f => (writeln "Now generating code..."; f (theory thyname))
+ | NONE => error ("Bad directive " ^ quote cmd)))
+ handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
end; (*local*)