--- a/doc-src/HOL/HOL.tex Mon May 11 13:19:28 2009 -0700
+++ b/doc-src/HOL/HOL.tex Mon May 11 21:55:30 2009 -0700
@@ -1427,7 +1427,7 @@
provides a decision procedure for \emph{linear arithmetic}: formulae involving
addition and subtraction. The simplifier invokes a weak version of this
decision procedure automatically. If this is not sufficent, you can invoke the
-full procedure \ttindex{linear_arith_tac} explicitly. It copes with arbitrary
+full procedure \ttindex{Lin_Arith.tac} explicitly. It copes with arbitrary
formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt-}, {\tt Suc}, {\tt
min}, {\tt max} and numerical constants. Other subterms are treated as
atomic, while subformulae not involving numerical types are ignored. Quantified
@@ -1438,10 +1438,10 @@
If {\tt k} is a numeral, then {\tt div k}, {\tt mod k} and
{\tt k dvd} are also supported. The former two are eliminated
by case distinctions, again blowing up the running time.
-If the formula involves explicit quantifiers, \texttt{linear_arith_tac} may take
+If the formula involves explicit quantifiers, \texttt{Lin_Arith.tac} may take
super-exponential time and space.
-If \texttt{linear_arith_tac} fails, try to find relevant arithmetic results in
+If \texttt{Lin_Arith.tac} fails, try to find relevant arithmetic results in
the library. The theories \texttt{Nat} and \texttt{NatArith} contain
theorems about {\tt<}, {\tt<=}, \texttt{+}, \texttt{-} and \texttt{*}.
Theory \texttt{Divides} contains theorems about \texttt{div} and
--- a/etc/isar-keywords-ZF.el Mon May 11 13:19:28 2009 -0700
+++ b/etc/isar-keywords-ZF.el Mon May 11 21:55:30 2009 -0700
@@ -18,7 +18,6 @@
"ML"
"ML_command"
"ML_prf"
- "ML_test"
"ML_val"
"ProofGeneral\\.inform_file_processed"
"ProofGeneral\\.inform_file_retracted"
@@ -349,7 +348,6 @@
(defconst isar-keywords-theory-decl
'("ML"
- "ML_test"
"abbreviation"
"arities"
"attribute_setup"
--- a/etc/isar-keywords.el Mon May 11 13:19:28 2009 -0700
+++ b/etc/isar-keywords.el Mon May 11 21:55:30 2009 -0700
@@ -18,7 +18,6 @@
"ML"
"ML_command"
"ML_prf"
- "ML_test"
"ML_val"
"ProofGeneral\\.inform_file_processed"
"ProofGeneral\\.inform_file_retracted"
@@ -64,6 +63,7 @@
"code_module"
"code_modulename"
"code_monad"
+ "code_pred"
"code_reserved"
"code_thms"
"code_type"
@@ -421,7 +421,6 @@
(defconst isar-keywords-theory-decl
'("ML"
- "ML_test"
"abbreviation"
"arities"
"atom_decl"
@@ -515,6 +514,7 @@
(defconst isar-keywords-theory-goal
'("ax_specification"
+ "code_pred"
"corollary"
"cpodef"
"function"
--- a/lib/jedit/isabelle.xml Mon May 11 13:19:28 2009 -0700
+++ b/lib/jedit/isabelle.xml Mon May 11 21:55:30 2009 -0700
@@ -45,7 +45,6 @@
<OPERATOR>ML</OPERATOR>
<LABEL>ML_command</LABEL>
<OPERATOR>ML_prf</OPERATOR>
- <OPERATOR>ML_test</OPERATOR>
<LABEL>ML_val</LABEL>
<OPERATOR>abbreviation</OPERATOR>
<KEYWORD4>actions</KEYWORD4>
@@ -95,6 +94,7 @@
<OPERATOR>code_module</OPERATOR>
<OPERATOR>code_modulename</OPERATOR>
<OPERATOR>code_monad</OPERATOR>
+ <OPERATOR>code_pred</OPERATOR>
<OPERATOR>code_reserved</OPERATOR>
<LABEL>code_thms</LABEL>
<OPERATOR>code_type</OPERATOR>
--- a/src/HOL/HoareParallel/OG_Examples.thy Mon May 11 13:19:28 2009 -0700
+++ b/src/HOL/HoareParallel/OG_Examples.thy Mon May 11 21:55:30 2009 -0700
@@ -443,7 +443,7 @@
--{* 32 subgoals left *}
apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
-apply(tactic {* TRYALL (linear_arith_tac @{context}) *})
+apply(tactic {* TRYALL (Lin_Arith.tac @{context}) *})
--{* 9 subgoals left *}
apply (force simp add:less_Suc_eq)
apply(drule sym)
--- a/src/HOL/Int.thy Mon May 11 13:19:28 2009 -0700
+++ b/src/HOL/Int.thy Mon May 11 21:55:30 2009 -0700
@@ -1521,6 +1521,7 @@
use "Tools/numeral_simprocs.ML"
use "Tools/int_arith.ML"
+setup {* Int_Arith.global_setup *}
declaration {* K Int_Arith.setup *}
setup {*
--- a/src/HOL/IsaMakefile Mon May 11 13:19:28 2009 -0700
+++ b/src/HOL/IsaMakefile Mon May 11 21:55:30 2009 -0700
@@ -295,8 +295,6 @@
Real.thy \
RealVector.thy \
Tools/float_syntax.ML \
- Tools/rat_arith.ML \
- Tools/real_arith.ML \
Tools/Qelim/ferrante_rackoff_data.ML \
Tools/Qelim/ferrante_rackoff.ML \
Tools/Qelim/langford_data.ML \
@@ -1051,7 +1049,6 @@
NSA/HyperDef.thy \
NSA/HyperNat.thy \
NSA/Hyperreal.thy \
- NSA/hypreal_arith.ML \
NSA/Filter.thy \
NSA/NatStar.thy \
NSA/NSA.thy \
--- a/src/HOL/NSA/HyperDef.thy Mon May 11 13:19:28 2009 -0700
+++ b/src/HOL/NSA/HyperDef.thy Mon May 11 21:55:30 2009 -0700
@@ -8,7 +8,6 @@
theory HyperDef
imports HyperNat Real
-uses ("hypreal_arith.ML")
begin
types hypreal = "real star"
@@ -343,8 +342,17 @@
Addsimps [symmetric hypreal_diff_def]
*)
-use "hypreal_arith.ML"
-declaration {* K hypreal_arith_setup *}
+declaration {*
+ K (Lin_Arith.add_inj_thms [@{thm star_of_le} RS iffD2,
+ @{thm star_of_less} RS iffD2, @{thm star_of_eq} RS iffD2]
+ #> Lin_Arith.add_simps [@{thm star_of_zero}, @{thm star_of_one},
+ @{thm star_of_number_of}, @{thm star_of_add}, @{thm star_of_minus},
+ @{thm star_of_diff}, @{thm star_of_mult}]
+ #> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"})
+ #> Simplifier.map_ss (fn simpset => simpset addsimprocs [Simplifier.simproc @{theory}
+ "fast_hypreal_arith" ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
+ (K Lin_Arith.simproc)]))
+*}
subsection {* Exponentials on the Hyperreals *}
--- a/src/HOL/NSA/hypreal_arith.ML Mon May 11 13:19:28 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-(* Title: HOL/NSA/hypreal_arith.ML
- Author: Tobias Nipkow, TU Muenchen
- Copyright 1999 TU Muenchen
-
-Simprocs for common factor cancellation & Rational coefficient handling
-
-Instantiation of the generic linear arithmetic package for type hypreal.
-*)
-
-local
-
-val simps = [thm "star_of_zero",
- thm "star_of_one",
- thm "star_of_number_of",
- thm "star_of_add",
- thm "star_of_minus",
- thm "star_of_diff",
- thm "star_of_mult"]
-
-val real_inj_thms = [thm "star_of_le" RS iffD2,
- thm "star_of_less" RS iffD2,
- thm "star_of_eq" RS iffD2]
-
-in
-
-val hyprealT = Type (@{type_name StarDef.star}, [HOLogic.realT]);
-
-val fast_hypreal_arith_simproc =
- Simplifier.simproc (the_context ())
- "fast_hypreal_arith"
- ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
- (K Lin_Arith.lin_arith_simproc);
-
-val hypreal_arith_setup =
- Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
- {add_mono_thms = add_mono_thms,
- mult_mono_thms = mult_mono_thms,
- inj_thms = real_inj_thms @ inj_thms,
- lessD = lessD, (*Can't change lessD: the hypreals are dense!*)
- neqE = neqE,
- simpset = simpset addsimps simps}) #>
- Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, HOLogic.realT --> hyprealT) #>
- Simplifier.map_ss (fn ss => ss addsimprocs [fast_hypreal_arith_simproc]);
-
-end;
--- a/src/HOL/Nat.thy Mon May 11 13:19:28 2009 -0700
+++ b/src/HOL/Nat.thy Mon May 11 21:55:30 2009 -0700
@@ -1410,6 +1410,7 @@
declaration {* K Nat_Arith.setup *}
use "Tools/lin_arith.ML"
+setup {* Lin_Arith.global_setup *}
declaration {* K Lin_Arith.setup *}
lemmas [arith_split] = nat_diff_split split_min split_max
--- a/src/HOL/Nat_Numeral.thy Mon May 11 13:19:28 2009 -0700
+++ b/src/HOL/Nat_Numeral.thy Mon May 11 21:55:30 2009 -0700
@@ -874,33 +874,21 @@
use "Tools/nat_numeral_simprocs.ML"
-declaration {*
-let
-
-val less_eq_rules = @{thms ring_distribs} @
- [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, @{thm nat_0}, @{thm nat_1},
- @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
- @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
- @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
- @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
- @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
- @{thm mult_Suc}, @{thm mult_Suc_right},
- @{thm add_Suc}, @{thm add_Suc_right},
- @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
- @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of}, @{thm if_True}, @{thm if_False}];
-
-val simprocs = Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals;
-
-in
-
-K (Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
- {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
- inj_thms = inj_thms, lessD = lessD, neqE = neqE,
- simpset = simpset addsimps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
- addsimps less_eq_rules
- addsimprocs simprocs}))
-
-end
+declaration {*
+ K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
+ #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1},
+ @{thm nat_0}, @{thm nat_1},
+ @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
+ @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
+ @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
+ @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
+ @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
+ @{thm mult_Suc}, @{thm mult_Suc_right},
+ @{thm add_Suc}, @{thm add_Suc_right},
+ @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
+ @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of},
+ @{thm if_True}, @{thm if_False}])
+ #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))
*}
--- a/src/HOL/Predicate.thy Mon May 11 13:19:28 2009 -0700
+++ b/src/HOL/Predicate.thy Mon May 11 21:55:30 2009 -0700
@@ -622,7 +622,10 @@
"pred_rec f P = f (eval P)"
by (cases P) simp
-text {* for evaluation of predicate enumerations *}
+inductive eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where "eq x x"
+
+lemma eq_is_eq: "eq x y \<equiv> (x = y)"
+ by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases)
ML {*
signature PREDICATE =
@@ -666,6 +669,12 @@
code_const Seq and Empty and Insert and Join
(Eval "Predicate.Seq" and "Predicate.Empty" and "Predicate.Insert/ (_,/ _)" and "Predicate.Join/ (_,/ _)")
+text {* dummy setup for @{text code_pred} keyword *}
+
+ML {*
+OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate"
+ OuterKeyword.thy_goal (OuterParse.term_group >> (K (Proof.theorem_i NONE (K I) [[]])))
+*}
no_notation
inf (infixl "\<sqinter>" 70) and
@@ -678,6 +687,6 @@
hide (open) type pred seq
hide (open) const Pred eval single bind if_pred not_pred
- Empty Insert Join Seq member pred_of_seq "apply" adjunct
+ Empty Insert Join Seq member pred_of_seq "apply" adjunct eq
end
--- a/src/HOL/Rational.thy Mon May 11 13:19:28 2009 -0700
+++ b/src/HOL/Rational.thy Mon May 11 21:55:30 2009 -0700
@@ -6,7 +6,6 @@
theory Rational
imports GCD Archimedean_Field
-uses ("Tools/rat_arith.ML")
begin
subsection {* Rational numbers as quotient *}
@@ -582,10 +581,25 @@
by (simp add: floor_unique)
-subsection {* Arithmetic setup *}
+subsection {* Linear arithmetic setup *}
-use "Tools/rat_arith.ML"
-declaration {* K rat_arith_setup *}
+declaration {*
+ K (Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2]
+ (* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *)
+ #> Lin_Arith.add_inj_thms [@{thm of_int_le_iff} RS iffD2, @{thm of_int_eq_iff} RS iffD2]
+ (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *)
+ #> Lin_Arith.add_simps [@{thm neg_less_iff_less},
+ @{thm True_implies_equals},
+ read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib},
+ @{thm divide_1}, @{thm divide_zero_left},
+ @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
+ @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
+ @{thm of_int_minus}, @{thm of_int_diff},
+ @{thm of_int_of_nat_eq}]
+ #> Lin_Arith.add_simprocs Numeral_Simprocs.field_cancel_numeral_factors
+ #> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat => rat"})
+ #> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int => rat"}))
+*}
subsection {* Embedding from Rationals to other Fields *}
--- a/src/HOL/RealDef.thy Mon May 11 13:19:28 2009 -0700
+++ b/src/HOL/RealDef.thy Mon May 11 21:55:30 2009 -0700
@@ -9,7 +9,6 @@
theory RealDef
imports PReal
-uses ("Tools/real_arith.ML")
begin
definition
@@ -960,10 +959,20 @@
(if neg (number_of v :: int) then 0
else (number_of v :: real))"
by (simp add: real_of_int_real_of_nat [symmetric] int_nat_number_of)
-
-use "Tools/real_arith.ML"
-declaration {* K real_arith_setup *}
+declaration {*
+ K (Lin_Arith.add_inj_thms [@{thm real_of_nat_le_iff} RS iffD2, @{thm real_of_nat_inject} RS iffD2]
+ (* not needed because x < (y::nat) can be rewritten as Suc x <= y: real_of_nat_less_iff RS iffD2 *)
+ #> Lin_Arith.add_inj_thms [@{thm real_of_int_le_iff} RS iffD2, @{thm real_of_int_inject} RS iffD2]
+ (* not needed because x < (y::int) can be rewritten as x + 1 <= y: real_of_int_less_iff RS iffD2 *)
+ #> Lin_Arith.add_simps [@{thm real_of_nat_zero}, @{thm real_of_nat_Suc}, @{thm real_of_nat_add},
+ @{thm real_of_nat_mult}, @{thm real_of_int_zero}, @{thm real_of_one},
+ @{thm real_of_int_add}, @{thm real_of_int_minus}, @{thm real_of_int_diff},
+ @{thm real_of_int_mult}, @{thm real_of_int_of_nat_eq},
+ @{thm real_of_nat_number_of}, @{thm real_number_of}]
+ #> Lin_Arith.add_inj_const (@{const_name real}, HOLogic.natT --> HOLogic.realT)
+ #> Lin_Arith.add_inj_const (@{const_name real}, HOLogic.intT --> HOLogic.realT))
+*}
subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}
--- a/src/HOL/Tools/Qelim/cooper.ML Mon May 11 13:19:28 2009 -0700
+++ b/src/HOL/Tools/Qelim/cooper.ML Mon May 11 21:55:30 2009 -0700
@@ -172,7 +172,7 @@
(* Canonical linear form for terms, formulae etc.. *)
fun provelin ctxt t = Goal.prove ctxt [] [] t
- (fn _ => EVERY [simp_tac lin_ss 1, TRY (linear_arith_tac ctxt 1)]);
+ (fn _ => EVERY [simp_tac lin_ss 1, TRY (Lin_Arith.tac ctxt 1)]);
fun linear_cmul 0 tm = zero
| linear_cmul n tm = case tm of
Const (@{const_name HOL.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
--- a/src/HOL/Tools/int_arith.ML Mon May 11 13:19:28 2009 -0700
+++ b/src/HOL/Tools/int_arith.ML Mon May 11 21:55:30 2009 -0700
@@ -5,8 +5,8 @@
signature INT_ARITH =
sig
- val fast_int_arith_simproc: simproc
val setup: Context.generic -> Context.generic
+ val global_setup: theory -> theory
end
structure Int_Arith : INT_ARITH =
@@ -49,17 +49,15 @@
make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
proc = proc1, identifier = []};
-val allowed_consts =
- [@{const_name "op ="}, @{const_name "HOL.times"}, @{const_name "HOL.uminus"},
- @{const_name "HOL.minus"}, @{const_name "HOL.plus"},
- @{const_name "HOL.zero"}, @{const_name "HOL.one"}, @{const_name "HOL.less"},
- @{const_name "HOL.less_eq"}];
-
-fun check t = case t of
- Const(s,t) => if s = @{const_name "HOL.one"} then not (t = @{typ int})
- else s mem_string allowed_consts
- | a$b => check a andalso check b
- | _ => false;
+fun check (Const (@{const_name "HOL.one"}, @{typ int})) = false
+ | check (Const (@{const_name "HOL.one"}, _)) = true
+ | check (Const (s, _)) = member (op =) [@{const_name "op ="},
+ @{const_name "HOL.times"}, @{const_name "HOL.uminus"},
+ @{const_name "HOL.minus"}, @{const_name "HOL.plus"},
+ @{const_name "HOL.zero"},
+ @{const_name "HOL.less"}, @{const_name "HOL.less_eq"}] s
+ | check (a $ b) = check a andalso check b
+ | check _ = false;
val conv =
Simplifier.rewrite
@@ -80,35 +78,24 @@
make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
proc = sproc, identifier = []}
-val add_rules =
- simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @
- @{thms int_arith_rules}
+val fast_int_arith_simproc =
+ Simplifier.simproc @{theory} "fast_int_arith"
+ ["(m::'a::{ordered_idom,number_ring}) < n",
+ "(m::'a::{ordered_idom,number_ring}) <= n",
+ "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.simproc);
-val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
-
-val numeral_base_simprocs = Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
- :: Numeral_Simprocs.combine_numerals
- :: Numeral_Simprocs.cancel_numerals;
+val global_setup = Simplifier.map_simpset
+ (fn simpset => simpset addsimprocs [fast_int_arith_simproc]);
val setup =
- Lin_Arith.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,
- inj_thms = nat_inj_thms @ inj_thms,
- lessD = lessD @ [@{thm zless_imp_add1_zle}],
- neqE = neqE,
- simpset = simpset addsimps add_rules
- addsimprocs numeral_base_simprocs}) #>
- Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
- Lin_Arith.add_discrete_type @{type_name Int.int}
-
-val fast_int_arith_simproc =
- Simplifier.simproc (the_context ())
- "fast_int_arith"
- ["(m::'a::{ordered_idom,number_ring}) < n",
- "(m::'a::{ordered_idom,number_ring}) <= n",
- "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.lin_arith_simproc);
+ Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
+ #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
+ #> Lin_Arith.add_simps (@{thms simp_thms} @ @{thms arith_simps} @ @{thms rel_simps}
+ @ @{thms arith_special} @ @{thms int_arith_rules})
+ #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
+ :: Numeral_Simprocs.combine_numerals
+ :: Numeral_Simprocs.cancel_numerals)
+ #> Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT)
+ #> Lin_Arith.add_discrete_type @{type_name Int.int}
end;
-
-Addsimprocs [Int_Arith.fast_int_arith_simproc];
--- a/src/HOL/Tools/lin_arith.ML Mon May 11 13:19:28 2009 -0700
+++ b/src/HOL/Tools/lin_arith.ML Mon May 11 21:55:30 2009 -0700
@@ -4,29 +4,20 @@
HOL setup for linear arithmetic (see Provers/Arith/fast_lin_arith.ML).
*)
-signature BASIC_LIN_ARITH =
-sig
- val arith_split_add: attribute
- val lin_arith_pre_tac: Proof.context -> int -> tactic
- val fast_arith_tac: Proof.context -> int -> tactic
- val fast_ex_arith_tac: Proof.context -> bool -> int -> tactic
- val lin_arith_simproc: simpset -> term -> thm option
- val fast_nat_arith_simproc: simproc
- val linear_arith_tac: Proof.context -> int -> tactic
-end;
-
signature LIN_ARITH =
sig
- include BASIC_LIN_ARITH
- val add_discrete_type: string -> Context.generic -> Context.generic
+ val pre_tac: Proof.context -> int -> tactic
+ val simple_tac: Proof.context -> int -> tactic
+ val tac: Proof.context -> int -> tactic
+ val simproc: simpset -> term -> thm option
+ val add_inj_thms: thm list -> Context.generic -> Context.generic
+ val add_lessD: thm -> Context.generic -> Context.generic
+ val add_simps: thm list -> Context.generic -> Context.generic
+ val add_simprocs: simproc list -> Context.generic -> Context.generic
val add_inj_const: string * typ -> Context.generic -> Context.generic
- val map_data:
- ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
- lessD: thm list, neqE: thm list, simpset: Simplifier.simpset} ->
- {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
- lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}) ->
- Context.generic -> Context.generic
+ val add_discrete_type: string -> Context.generic -> Context.generic
val setup: Context.generic -> Context.generic
+ val global_setup: theory -> theory
val split_limit: int Config.T
val neq_limit: int Config.T
val warning_count: int ref
@@ -47,37 +38,38 @@
val sym = sym;
val not_lessD = @{thm linorder_not_less} RS iffD1;
val not_leD = @{thm linorder_not_le} RS iffD1;
-val le0 = thm "le0";
-fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI);
+fun mk_Eq thm = thm RS Eq_FalseI handle THM _ => thm RS Eq_TrueI;
val mk_Trueprop = HOLogic.mk_Trueprop;
fun atomize thm = case Thm.prop_of thm of
- Const("Trueprop",_) $ (Const("op &",_) $ _ $ _) =>
- atomize(thm RS conjunct1) @ atomize(thm RS conjunct2)
+ Const ("Trueprop", _) $ (Const (@{const_name "op &"}, _) $ _ $ _) =>
+ atomize (thm RS conjunct1) @ atomize (thm RS conjunct2)
| _ => [thm];
-fun neg_prop ((TP as Const("Trueprop",_)) $ (Const("Not",_) $ t)) = TP $ t
- | neg_prop ((TP as Const("Trueprop",_)) $ t) = TP $ (HOLogic.Not $t)
+fun neg_prop ((TP as Const("Trueprop", _)) $ (Const (@{const_name "Not"}, _) $ t)) = TP $ t
+ | neg_prop ((TP as Const("Trueprop", _)) $ t) = TP $ (HOLogic.Not $t)
| neg_prop t = raise TERM ("neg_prop", [t]);
fun is_False thm =
let val _ $ t = Thm.prop_of thm
- in t = Const("False",HOLogic.boolT) end;
+ in t = HOLogic.false_const end;
fun is_nat t = (fastype_of1 t = HOLogic.natT);
-fun mk_nat_thm sg t =
- let val ct = cterm_of sg t and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
- in instantiate ([],[(cn,ct)]) le0 end;
+fun mk_nat_thm thy t =
+ let
+ val cn = cterm_of thy (Var (("n", 0), HOLogic.natT))
+ and ct = cterm_of thy t
+ in instantiate ([], [(cn, ct)]) @{thm le0} end;
end;
(* arith context data *)
-structure ArithContextData = GenericDataFun
+structure Lin_Arith_Data = GenericDataFun
(
type T = {splits: thm list,
inj_consts: (string * typ) list,
@@ -92,27 +84,25 @@
discrete = Library.merge (op =) (discrete1, discrete2)};
);
-val get_arith_data = ArithContextData.get o Context.Proof;
+val get_arith_data = Lin_Arith_Data.get o Context.Proof;
-val arith_split_add = Thm.declaration_attribute (fn thm =>
- ArithContextData.map (fn {splits, inj_consts, discrete} =>
- {splits = update Thm.eq_thm_prop thm splits,
- inj_consts = inj_consts, discrete = discrete}));
+fun add_split thm = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
+ {splits = update Thm.eq_thm_prop thm splits,
+ inj_consts = inj_consts, discrete = discrete});
-fun add_discrete_type d = ArithContextData.map (fn {splits, inj_consts, discrete} =>
+fun add_discrete_type d = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
{splits = splits, inj_consts = inj_consts,
discrete = update (op =) d discrete});
-fun add_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete} =>
+fun add_inj_const c = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
{splits = splits, inj_consts = update (op =) c inj_consts,
discrete = discrete});
-val (split_limit, setup1) = Attrib.config_int "linarith_split_limit" 9;
-val (neq_limit, setup2) = Attrib.config_int "linarith_neq_limit" 9;
-val setup_options = setup1 #> setup2;
+val (split_limit, setup_split_limit) = Attrib.config_int "linarith_split_limit" 9;
+val (neq_limit, setup_neq_limit) = Attrib.config_int "linarith_neq_limit" 9;
-structure LA_Data_Ref =
+structure LA_Data =
struct
val fast_arith_neq_limit = neq_limit;
@@ -243,15 +233,12 @@
end handle Rat.DIVZERO => NONE;
fun of_lin_arith_sort thy U =
- Sign.of_sort thy (U, ["Ring_and_Field.ordered_idom"]);
+ Sign.of_sort thy (U, @{sort Ring_and_Field.ordered_idom});
-fun allows_lin_arith sg (discrete : string list) (U as Type (D, [])) : bool * bool =
- if of_lin_arith_sort sg U then
- (true, D mem discrete)
- else (* special cases *)
- if D mem discrete then (true, true) else (false, false)
- | allows_lin_arith sg discrete U =
- (of_lin_arith_sort sg U, false);
+fun allows_lin_arith thy (discrete : string list) (U as Type (D, [])) : bool * bool =
+ if of_lin_arith_sort thy U then (true, member (op =) discrete D)
+ else if member (op =) discrete D then (true, true) else (false, false)
+ | allows_lin_arith sg discrete U = (of_lin_arith_sort sg U, false);
fun decomp_typecheck (thy, discrete, inj_consts) (T : typ, xxx) : decomp option =
case T of
@@ -287,7 +274,7 @@
| domain_is_nat (_ $ (Const ("Not", _) $ (Const (_, T) $ _ $ _))) = nT T
| domain_is_nat _ = false;
-fun number_of (n, T) = HOLogic.mk_number T n;
+val mk_number = HOLogic.mk_number;
(*---------------------------------------------------------------------------*)
(* the following code performs splitting of certain constants (e.g. min, *)
@@ -756,17 +743,34 @@
)
end;
-end; (* LA_Data_Ref *)
+end; (* LA_Data *)
-val lin_arith_pre_tac = LA_Data_Ref.pre_tac;
+val pre_tac = LA_Data.pre_tac;
-structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data_Ref);
+structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data);
val map_data = Fast_Arith.map_data;
-fun fast_arith_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
-val fast_ex_arith_tac = Fast_Arith.lin_arith_tac;
+fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =
+ {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms,
+ lessD = lessD, neqE = neqE, simpset = simpset};
+
+fun map_lessD f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =
+ {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
+ lessD = f lessD, neqE = neqE, simpset = simpset};
+
+fun map_simpset f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =
+ {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
+ lessD = lessD, neqE = neqE, simpset = f simpset};
+
+fun add_inj_thms thms = Fast_Arith.map_data (map_inj_thms (append thms));
+fun add_lessD thm = Fast_Arith.map_data (map_lessD (fn thms => thms @ [thm]));
+fun add_simps thms = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimps thms));
+fun add_simprocs procs = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimprocs procs));
+
+fun simple_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
+val lin_arith_tac = Fast_Arith.lin_arith_tac;
val trace = Fast_Arith.trace;
val warning_count = Fast_Arith.warning_count;
@@ -774,7 +778,7 @@
Most of the work is done by the cancel tactics. *)
val init_arith_data =
- map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
+ Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
{add_mono_thms = @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field} @ add_mono_thms,
mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
inj_thms = inj_thms,
@@ -797,17 +801,7 @@
fun add_arith_facts ss =
add_prems (Arith_Data.get_arith_facts (MetaSimplifier.the_context ss)) ss;
-val lin_arith_simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
-
-val fast_nat_arith_simproc =
- Simplifier.simproc (the_context ()) "fast_nat_arith"
- ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K lin_arith_simproc);
-
-(* Because of fast_nat_arith_simproc, the arithmetic solver is really only
-useful to detect inconsistencies among the premises for subgoals which are
-*not* themselves (in)equalities, because the latter activate
-fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
-solver all the time rather than add the additional check. *)
+val simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
(* generic refutation procedure *)
@@ -857,7 +851,7 @@
local
-fun raw_arith_tac ctxt ex =
+fun raw_tac ctxt ex =
(* FIXME: K true should be replaced by a sensible test (perhaps "isSome o
decomp sg"? -- but note that the test is applied to terms already before
they are split/normalized) to speed things up in case there are lots of
@@ -866,21 +860,21 @@
(l <= min m n + k) = (l <= m+k & l <= n+k)
*)
refute_tac (K true)
- (* Splitting is also done inside fast_arith_tac, but not completely -- *)
+ (* Splitting is also done inside simple_tac, but not completely -- *)
(* split_tac may use split theorems that have not been implemented in *)
- (* fast_arith_tac (cf. pre_decomp and split_once_items above), and *)
+ (* simple_tac (cf. pre_decomp and split_once_items above), and *)
(* split_limit may trigger. *)
- (* Therefore splitting outside of fast_arith_tac may allow us to prove *)
- (* some goals that fast_arith_tac alone would fail on. *)
+ (* Therefore splitting outside of simple_tac may allow us to prove *)
+ (* some goals that simple_tac alone would fail on. *)
(REPEAT_DETERM o split_tac (#splits (get_arith_data ctxt)))
- (fast_ex_arith_tac ctxt ex);
+ (lin_arith_tac ctxt ex);
in
-fun gen_linear_arith_tac ex ctxt = FIRST' [fast_arith_tac ctxt,
- ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt ex];
+fun gen_tac ex ctxt = FIRST' [simple_tac ctxt,
+ ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
-val linear_arith_tac = gen_linear_arith_tac true;
+val tac = gen_tac true;
end;
@@ -889,21 +883,25 @@
val setup =
init_arith_data #>
- Simplifier.map_ss (fn ss => ss addsimprocs [fast_nat_arith_simproc]
+ Simplifier.map_ss (fn ss => ss addsimprocs [Simplifier.simproc (@{theory}) "fast_nat_arith"
+ ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K simproc)]
+ (* Because of fast_nat_arith_simproc, the arithmetic solver is really only
+ useful to detect inconsistencies among the premises for subgoals which are
+ *not* themselves (in)equalities, because the latter activate
+ fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
+ solver all the time rather than add the additional check. *)
addSolver (mk_solver' "lin_arith"
- (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))) #>
- Context.mapping
- (setup_options #>
- Arith_Data.add_tactic "linear arithmetic" gen_linear_arith_tac #>
- Method.setup @{binding linarith}
- (Args.bang_facts >> (fn prems => fn ctxt =>
- METHOD (fn facts =>
- HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
- THEN' linear_arith_tac ctxt)))) "linear arithmetic" #>
- Attrib.setup @{binding arith_split} (Scan.succeed arith_split_add)
- "declaration of split rules for arithmetic procedure") I;
+ (add_arith_facts #> Fast_Arith.cut_lin_arith_tac)))
+
+val global_setup =
+ setup_split_limit #> setup_neq_limit #>
+ Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))
+ "declaration of split rules for arithmetic procedure" #>
+ Method.setup @{binding linarith}
+ (Args.bang_facts >> (fn prems => fn ctxt =>
+ METHOD (fn facts =>
+ HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
+ THEN' tac ctxt)))) "linear arithmetic" #>
+ Arith_Data.add_tactic "linear arithmetic" gen_tac;
end;
-
-structure Basic_Lin_Arith: BASIC_LIN_ARITH = Lin_Arith;
-open Basic_Lin_Arith;
--- a/src/HOL/Tools/numeral_simprocs.ML Mon May 11 13:19:28 2009 -0700
+++ b/src/HOL/Tools/numeral_simprocs.ML Mon May 11 21:55:30 2009 -0700
@@ -516,7 +516,7 @@
val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT);
val pos = less $ zero $ t and neg = less $ t $ zero
fun prove p =
- Option.map Eq_True_elim (Lin_Arith.lin_arith_simproc ss p)
+ Option.map Eq_True_elim (Lin_Arith.simproc ss p)
handle THM _ => NONE
in case prove pos of
SOME th => SOME(th RS pos_th)
--- a/src/HOL/Tools/rat_arith.ML Mon May 11 13:19:28 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-(* Title: HOL/Real/rat_arith.ML
- Author: Lawrence C Paulson
- Copyright 2004 University of Cambridge
-
-Simprocs for common factor cancellation & Rational coefficient handling
-
-Instantiation of the generic linear arithmetic package for type rat.
-*)
-
-local
-
-val simps =
- [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals},
- read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib},
- @{thm divide_1}, @{thm divide_zero_left},
- @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
- @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
- @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add},
- @{thm of_int_minus}, @{thm of_int_diff},
- @{thm of_int_mult}, @{thm of_int_of_nat_eq}]
-
-val nat_inj_thms = [@{thm of_nat_le_iff} RS iffD2,
- @{thm of_nat_eq_iff} RS iffD2]
-(* not needed because x < (y::nat) can be rewritten as Suc x <= y:
- of_nat_less_iff RS iffD2 *)
-
-val int_inj_thms = [@{thm of_int_le_iff} RS iffD2,
- @{thm of_int_eq_iff} RS iffD2]
-(* not needed because x < (y::int) can be rewritten as x + 1 <= y:
- of_int_less_iff RS iffD2 *)
-
-in
-
-val rat_arith_setup =
- Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
- {add_mono_thms = add_mono_thms,
- mult_mono_thms = mult_mono_thms,
- inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
- lessD = lessD, (*Can't change lessD: the rats are dense!*)
- neqE = neqE,
- simpset = simpset addsimps simps
- addsimprocs Numeral_Simprocs.field_cancel_numeral_factors}) #>
- Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat => rat"}) #>
- Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int => rat"})
-
-end;
--- a/src/HOL/Tools/real_arith.ML Mon May 11 13:19:28 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-(* Title: HOL/Real/real_arith.ML
- ID: $Id$
- Author: Tobias Nipkow, TU Muenchen
- Copyright 1999 TU Muenchen
-
-Simprocs for common factor cancellation & Rational coefficient handling
-
-Instantiation of the generic linear arithmetic package for type real.
-*)
-
-local
-
-val simps = [@{thm real_of_nat_zero}, @{thm real_of_nat_Suc}, @{thm real_of_nat_add},
- @{thm real_of_nat_mult}, @{thm real_of_int_zero}, @{thm real_of_one},
- @{thm real_of_int_add}, @{thm real_of_int_minus}, @{thm real_of_int_diff},
- @{thm real_of_int_mult}, @{thm real_of_int_of_nat_eq},
- @{thm real_of_nat_number_of}, @{thm real_number_of}]
-
-val nat_inj_thms = [@{thm real_of_nat_le_iff} RS iffD2,
- @{thm real_of_nat_inject} RS iffD2]
-(* not needed because x < (y::nat) can be rewritten as Suc x <= y:
- real_of_nat_less_iff RS iffD2 *)
-
-val int_inj_thms = [@{thm real_of_int_le_iff} RS iffD2,
- @{thm real_of_int_inject} RS iffD2]
-(* not needed because x < (y::int) can be rewritten as x + 1 <= y:
- real_of_int_less_iff RS iffD2 *)
-
-in
-
-val real_arith_setup =
- Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
- {add_mono_thms = add_mono_thms,
- mult_mono_thms = mult_mono_thms,
- inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
- lessD = lessD, (*Can't change lessD: the reals are dense!*)
- neqE = neqE,
- simpset = simpset addsimps simps}) #>
- Lin_Arith.add_inj_const (@{const_name real}, HOLogic.natT --> HOLogic.realT) #>
- Lin_Arith.add_inj_const (@{const_name real}, HOLogic.intT --> HOLogic.realT)
-
-end;
--- a/src/HOL/ex/Arith_Examples.thy Mon May 11 13:19:28 2009 -0700
+++ b/src/HOL/ex/Arith_Examples.thy Mon May 11 21:55:30 2009 -0700
@@ -13,18 +13,18 @@
distribution. This file merely contains some additional tests and special
corner cases. Some rather technical remarks:
- @{ML fast_arith_tac} is a very basic version of the tactic. It performs no
+ @{ML Lin_Arith.simple_tac} is a very basic version of the tactic. It performs no
meta-to-object-logic conversion, and only some splitting of operators.
- @{ML linear_arith_tac} performs meta-to-object-logic conversion, full
+ @{ML Lin_Arith.tac} performs meta-to-object-logic conversion, full
splitting of operators, and NNF normalization of the goal. The @{text arith}
method combines them both, and tries other methods (e.g.~@{text presburger})
as well. This is the one that you should use in your proofs!
An @{text arith}-based simproc is available as well (see @{ML
- Lin_Arith.lin_arith_simproc}), which---for performance
- reasons---however does even less splitting than @{ML fast_arith_tac}
+ Lin_Arith.simproc}), which---for performance
+ reasons---however does even less splitting than @{ML Lin_Arith.simple_tac}
at the moment (namely inequalities only). (On the other hand, it
- does take apart conjunctions, which @{ML fast_arith_tac} currently
+ does take apart conjunctions, which @{ML Lin_Arith.simple_tac} currently
does not do.)
*}
@@ -123,12 +123,12 @@
(* FIXME: need to replace 1 by its numeral representation *)
apply (subst numeral_1_eq_1 [symmetric])
(* FIXME: arith does not know about iszero *)
- apply (tactic {* lin_arith_pre_tac @{context} 1 *})
+ apply (tactic {* Lin_Arith.pre_tac @{context} 1 *})
oops
lemma "(i::int) mod 42 <= 41"
(* FIXME: arith does not know about iszero *)
- apply (tactic {* lin_arith_pre_tac @{context} 1 *})
+ apply (tactic {* Lin_Arith.pre_tac @{context} 1 *})
oops
lemma "-(i::int) * 1 = 0 ==> i = 0"
@@ -208,13 +208,13 @@
(* preprocessing negates the goal and tries to compute its negation *)
(* normal form, which creates lots of separate cases for this *)
(* disjunction of conjunctions *)
-(* by (tactic {* linear_arith_tac 1 *}) *)
+(* by (tactic {* Lin_Arith.tac 1 *}) *)
oops
lemma "2 * (x::nat) ~= 1"
(* FIXME: this is beyond the scope of the decision procedure at the moment, *)
(* because its negation is satisfiable in the rationals? *)
-(* by (tactic {* fast_arith_tac 1 *}) *)
+(* by (tactic {* Lin_Arith.simple_tac 1 *}) *)
oops
text {* Constants. *}
--- a/src/HOL/ex/Predicate_Compile.thy Mon May 11 13:19:28 2009 -0700
+++ b/src/HOL/ex/Predicate_Compile.thy Mon May 11 21:55:30 2009 -0700
@@ -7,6 +7,11 @@
setup {* Predicate_Compile.setup *}
+ML {*
+ OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate"
+ OuterKeyword.thy_goal (OuterParse.term_group >> Predicate_Compile.code_pred_cmd)
+*}
+
text {* Experimental code *}
@@ -83,4 +88,16 @@
ML_val {* Predicate.analyze_compr @{theory} @{term "{n. odd n}"} *}
+section {* Example for user interface *}
+
+inductive append2 :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
+ append2_Nil: "append2 [] xs xs"
+ | append2_Cons: "append2 xs ys zs \<Longrightarrow> append2 (x # xs) ys (x # zs)"
+
+(*code_pred append2
+ using assms by (rule append2.cases)
+
+thm append2_codegen
+thm append2_cases*)
+
end
\ No newline at end of file
--- a/src/HOL/ex/predicate_compile.ML Mon May 11 13:19:28 2009 -0700
+++ b/src/HOL/ex/predicate_compile.ML Mon May 11 21:55:30 2009 -0700
@@ -14,11 +14,15 @@
val strip_intro_concl : term -> int -> (term * (term list * term list))
val code_ind_intros_attrib : attribute
val code_ind_cases_attrib : attribute
- val print_alternative_rules : theory -> theory
val modename_of: theory -> string -> mode -> string
val modes_of: theory -> string -> mode list
val setup : theory -> theory
+ val code_pred : string -> Proof.context -> Proof.state
+ val code_pred_cmd : string -> Proof.context -> Proof.state
+ val print_alternative_rules : theory -> theory
val do_proofs: bool ref
+ val pred_intros : theory -> string -> thm list
+ val get_nparams : theory -> string -> int
end;
structure Predicate_Compile: PREDICATE_COMPILE =
@@ -739,15 +743,15 @@
Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct
| _ => error "Trueprop_conv"
-fun preprocess_intro thy rule = Thm.transfer thy rule (*FIXME preprocessor
+fun preprocess_intro thy rule =
Conv.fconv_rule
(imp_prems_conv
- (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @ {thm Predicate.eq_is_eq})))))
- (Thm.transfer thy rule) *)
+ (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
+ (Thm.transfer thy rule)
-fun preprocess_elim thy nargs elimrule = (*FIXME preprocessor -- let
+fun preprocess_elim thy nargs elimrule = let
fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
- HOLogic.mk_Trueprop (Const (@ {const_name Predicate.eq}, T) $ lhs $ rhs)
+ HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
| replace_eqs t = t
fun preprocess_case t = let
val params = Logic.strip_params t
@@ -759,10 +763,10 @@
val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule)
in
Thm.equal_elim
- (Thm.symmetric (Conv.implies_concl_conv (MetaSimplifier.rewrite true [@ {thm eq_is_eq}])
+ (Thm.symmetric (Conv.implies_concl_conv (MetaSimplifier.rewrite true [@{thm eq_is_eq}])
(cterm_of thy elimrule')))
elimrule
- end*) elimrule;
+ end;
(* returns true if t is an application of an datatype constructor *)
@@ -1354,6 +1358,57 @@
Attrib.setup @{binding code_ind_cases} (Scan.succeed code_ind_cases_attrib)
"adding alternative elimination rules for code generation of inductive predicates";
+(* generation of case rules from user-given introduction rules *)
+
+ fun mk_casesrule introrules nparams ctxt = let
+ val intros = map prop_of introrules
+ val (pred, (params, args)) = strip_intro_concl (hd intros) nparams
+ val ([propname], ctxt1) = Variable.variant_fixes ["thesis"] ctxt
+ val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
+ val (argnames, ctxt2) = Variable.variant_fixes
+ (map (fn i => "a" ^ string_of_int i) (1 upto (length args))) ctxt1
+ val argvs = map Free (argnames ~~ (map fastype_of args))
+ fun mk_case intro = let
+ val (_, (_, args)) = strip_intro_concl intro nparams
+ val prems = Logic.strip_imp_prems intro
+ val eqprems = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (argvs ~~ args)
+ val frees = (fold o fold_aterms)
+ (fn t as Free _ =>
+ if member (op aconv) params t then I else insert (op aconv) t
+ | _ => I) (args @ prems) []
+ in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
+ val assm = HOLogic.mk_Trueprop (list_comb (pred, params @ argvs))
+ val cases = map mk_case intros
+ val (_, ctxt3) = ProofContext.add_assms_i Assumption.assume_export
+ [((Binding.name AutoBind.assmsN, []), map (fn t => (t, [])) (assm :: cases))]
+ ctxt2
+ in (pred, prop, ctxt3) end;
+
+(* setup for user interface *)
+
+ fun generic_code_pred prep_const raw_const lthy =
+ let
+ val thy = (ProofContext.theory_of lthy)
+ val const = prep_const thy raw_const
+ val nparams = get_nparams thy const
+ val intro_rules = pred_intros thy const
+ val (((tfrees, frees), fact), lthy') =
+ Variable.import_thms true intro_rules lthy;
+ val (pred, prop, lthy'') = mk_casesrule fact nparams lthy'
+ val (predname, _) = dest_Const pred
+ fun after_qed [[th]] lthy'' =
+ LocalTheory.note Thm.theoremK
+ ((Binding.name (Long_Name.base_name predname ^ "_cases"), (* FIXME: other suffix *)
+ [Attrib.internal (K (code_ind_cases_attrib))]) , [th]) lthy''
+ |> snd
+ |> LocalTheory.theory (create_def_equation predname)
+ in
+ Proof.theorem_i NONE after_qed [[(prop, [])]] lthy''
+ end;
+
+ val code_pred = generic_code_pred (K I);
+ val code_pred_cmd = generic_code_pred Code_Unit.read_const
+
end;
fun pred_compile name thy = Predicate_Compile.create_def_equation
--- a/src/Provers/Arith/fast_lin_arith.ML Mon May 11 13:19:28 2009 -0700
+++ b/src/Provers/Arith/fast_lin_arith.ML Mon May 11 21:55:30 2009 -0700
@@ -56,7 +56,7 @@
(*preprocessing, performed on the goal -- must do the same as 'pre_decomp':*)
val pre_tac: Proof.context -> int -> tactic
- val number_of: int * typ -> term
+ val mk_number: typ -> int -> term
(*the limit on the number of ~= allowed; because each ~= is split
into two cases, this can lead to an explosion*)
@@ -86,6 +86,9 @@
signature FAST_LIN_ARITH =
sig
+ val cut_lin_arith_tac: simpset -> int -> tactic
+ val lin_arith_tac: Proof.context -> bool -> int -> tactic
+ val lin_arith_simproc: simpset -> term -> thm option
val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}
-> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
@@ -93,9 +96,6 @@
-> Context.generic -> Context.generic
val trace: bool ref
val warning_count: int ref;
- val cut_lin_arith_tac: simpset -> int -> tactic
- val lin_arith_tac: Proof.context -> bool -> int -> tactic
- val lin_arith_simproc: simpset -> term -> thm option
end;
functor Fast_Lin_Arith
@@ -429,7 +429,7 @@
(* FIXME OPTIMIZE!!!! (partly done already)
Addition/Multiplication need i*t representation rather than t+t+...
- Get rid of Mulitplied(2). For Nat LA_Data.number_of should return Suc^n
+ Get rid of Mulitplied(2). For Nat LA_Data.mk_number should return Suc^n
because Numerals are not known early enough.
Simplification may detect a contradiction 'prematurely' due to type
@@ -480,7 +480,7 @@
get_first (fn th => SOME(thm RS th) handle THM _ => NONE) mult_mono_thms
fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (Thm.theory_of_thm th) var;
val cv = cvar(mth, hd(prems_of mth));
- val ct = cterm_of thy (LA_Data.number_of(n,#T(rep_cterm cv)))
+ val ct = cterm_of thy (LA_Data.mk_number (#T (rep_cterm cv)) n)
in instantiate ([],[(cv,ct)]) mth end
fun simp thm =