renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
1.1 --- a/NEWS Fri Mar 10 12:28:38 2006 +0100
1.2 +++ b/NEWS Fri Mar 10 15:33:48 2006 +0100
1.3 @@ -340,6 +340,33 @@
1.4 25 like -->); output depends on the "iff" print_mode, the default is
1.5 "A = B" (with priority 50).
1.6
1.7 +* Renamed some (legacy-named) constants in HOL.thy:
1.8 + op + ~> HOL.plus
1.9 + op - ~> HOL.minus
1.10 + uminus ~> HOL.uminus
1.11 + op * ~> HOL.times
1.12 +
1.13 +Adaptions may be required in the following cases:
1.14 +
1.15 +a) User-defined constants using any of the names "plus", "minus", or "times"
1.16 +The standard syntax translations for "+", "-" and "*" may go wrong.
1.17 +INCOMPATIBILITY: use more specific names.
1.18 +
1.19 +b) Variables named "plus", "minus", or "times"
1.20 +INCOMPATIBILITY: use more specific names.
1.21 +
1.22 +c) Commutative equations theorems (e. g. "a + b = b + a")
1.23 +Since the changing of names also changes the order of terms, commutative rewrites
1.24 +perhaps will be applied when not applied before or the other way round.
1.25 +Experience shows that thiis is rarely the case (only two adaptions in the whole
1.26 +Isabelle distribution).
1.27 +INCOMPATIBILITY: rewrite proof; sometimes already an exchange of a distributive
1.28 +law may suffice.
1.29 +
1.30 +d) ML code directly refering to constant names
1.31 +This in general only affects hand-written proof tactics, simprocs and so on.
1.32 +INCOMPATIBILITY: grep your sourcecode and replace names.
1.33 +
1.34 * "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only).
1.35
1.36 * In the context of the assumption "~(s = t)" the Simplifier rewrites
2.1 --- a/src/HOL/Algebra/CRing.thy Fri Mar 10 12:28:38 2006 +0100
2.2 +++ b/src/HOL/Algebra/CRing.thy Fri Mar 10 15:33:48 2006 +0100
2.3 @@ -20,7 +20,7 @@
2.4 a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
2.5 "a_inv R == m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
2.6
2.7 - minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
2.8 + a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
2.9 "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y == x \<oplus> (\<ominus> y)"
2.10
2.11 locale abelian_monoid = struct G +
2.12 @@ -95,7 +95,7 @@
2.13
2.14 lemma (in abelian_group) minus_closed [intro, simp]:
2.15 "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<ominus> y \<in> carrier G"
2.16 - by (simp add: minus_def)
2.17 + by (simp add: a_minus_def)
2.18
2.19 lemma (in abelian_group) a_l_cancel [simp]:
2.20 "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
2.21 @@ -431,7 +431,7 @@
2.22
2.23 lemma (in ring) minus_eq:
2.24 "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
2.25 - by (simp only: minus_def)
2.26 + by (simp only: a_minus_def)
2.27
2.28 lemmas (in ring) ring_simprules =
2.29 a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
3.1 --- a/src/HOL/Algebra/abstract/order.ML Fri Mar 10 12:28:38 2006 +0100
3.2 +++ b/src/HOL/Algebra/abstract/order.ML Fri Mar 10 15:33:48 2006 +0100
3.3 @@ -8,7 +8,7 @@
3.4 (*** Term order for commutative rings ***)
3.5
3.6 fun ring_ord a =
3.7 - find_index_eq a ["0", "op +", "uminus", "op -", "1", "op *"];
3.8 + find_index (fn a' => a = a') ["0", "HOL.plus", "HOL.uminus", "HOL.minus", "1", "HOL.times"];
3.9
3.10 fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS);
3.11
3.12 @@ -18,9 +18,9 @@
3.13 val a = Free ("a", intT);
3.14 val b = Free ("b", intT);
3.15 val c = Free ("c", intT);
3.16 -val plus = Const ("op +", [intT, intT]--->intT);
3.17 -val mult = Const ("op *", [intT, intT]--->intT);
3.18 -val uminus = Const ("uminus", intT-->intT);
3.19 +val plus = Const ("HOL.plus", [intT, intT]--->intT);
3.20 +val mult = Const ("HOL.times", [intT, intT]--->intT);
3.21 +val uminus = Const ("HOL.uminus", intT-->intT);
3.22 val one = Const ("1", intT);
3.23 val f = Const("f", intT-->intT);
3.24
4.1 --- a/src/HOL/Auth/Guard/Extensions.thy Fri Mar 10 12:28:38 2006 +0100
4.2 +++ b/src/HOL/Auth/Guard/Extensions.thy Fri Mar 10 15:33:48 2006 +0100
4.3 @@ -27,15 +27,15 @@
4.4
4.5 subsection{*Extensions to Theory @{text List}*}
4.6
4.7 -subsubsection{*"minus l x" erase the first element of "l" equal to "x"*}
4.8 +subsubsection{*"remove l x" erase the first element of "l" equal to "x"*}
4.9
4.10 -consts minus :: "'a list => 'a => 'a list"
4.11 +consts remove :: "'a list => 'a => 'a list"
4.12
4.13 primrec
4.14 -"minus [] y = []"
4.15 -"minus (x#xs) y = (if x=y then xs else x # minus xs y)"
4.16 +"remove [] y = []"
4.17 +"remove (x#xs) y = (if x=y then xs else x # remove xs y)"
4.18
4.19 -lemma set_minus: "set (minus l x) <= set l"
4.20 +lemma set_remove: "set (remove l x) <= set l"
4.21 by (induct l, auto)
4.22
4.23 subsection{*Extensions to Theory @{text Message}*}
5.1 --- a/src/HOL/Auth/Guard/Guard.thy Fri Mar 10 12:28:38 2006 +0100
5.2 +++ b/src/HOL/Auth/Guard/Guard.thy Fri Mar 10 15:33:48 2006 +0100
5.3 @@ -208,7 +208,7 @@
5.4
5.5 lemmas mem_cnb_minus_substI = mem_cnb_minus [THEN ssubst]
5.6
5.7 -lemma cnb_minus [simp]: "x mem l ==> cnb (minus l x) = cnb l - crypt_nb x"
5.8 +lemma cnb_minus [simp]: "x mem l ==> cnb (remove l x) = cnb l - crypt_nb x"
5.9 apply (induct l, auto)
5.10 by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp)
5.11
5.12 @@ -242,7 +242,7 @@
5.13 subsection{*list corresponding to "decrypt"*}
5.14
5.15 constdefs decrypt' :: "msg list => key => msg => msg list"
5.16 -"decrypt' l K Y == Y # minus l (Crypt K Y)"
5.17 +"decrypt' l K Y == Y # remove l (Crypt K Y)"
5.18
5.19 declare decrypt'_def [simp]
5.20
5.21 @@ -278,7 +278,7 @@
5.22 apply (subgoal_tac "Crypt K Y:parts (set l)")
5.23 apply (drule parts_cnb, rotate_tac -1, simp)
5.24 apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub)
5.25 -apply (rule insert_mono, rule set_minus)
5.26 +apply (rule insert_mono, rule set_remove)
5.27 apply (simp add: analz_insertD, blast)
5.28 (* Crypt K Y:parts (set l) *)
5.29 apply (blast dest: kparts_parts)
5.30 @@ -288,7 +288,7 @@
5.31 apply (rule_tac K=K in guard_Crypt, simp add: Guard_def, simp)
5.32 apply (drule_tac t="set l'" in sym, simp)
5.33 apply (rule Guard_kparts, simp, simp)
5.34 -apply (rule_tac B="set l'" in subset_trans, rule set_minus, blast)
5.35 +apply (rule_tac B="set l'" in subset_trans, rule set_remove, blast)
5.36 by (rule kparts_set)
5.37
5.38 lemma Guard_invKey_finite: "[| Nonce n:analz G; Guard n Ks G; finite G |]
6.1 --- a/src/HOL/Auth/Guard/GuardK.thy Fri Mar 10 12:28:38 2006 +0100
6.2 +++ b/src/HOL/Auth/Guard/GuardK.thy Fri Mar 10 15:33:48 2006 +0100
6.3 @@ -204,7 +204,7 @@
6.4
6.5 lemmas mem_cnb_minus_substI = mem_cnb_minus [THEN ssubst]
6.6
6.7 -lemma cnb_minus [simp]: "x mem l ==> cnb (minus l x) = cnb l - crypt_nb x"
6.8 +lemma cnb_minus [simp]: "x mem l ==> cnb (remove l x) = cnb l - crypt_nb x"
6.9 apply (induct l, auto)
6.10 by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp)
6.11
6.12 @@ -238,7 +238,7 @@
6.13 subsection{*list corresponding to "decrypt"*}
6.14
6.15 constdefs decrypt' :: "msg list => key => msg => msg list"
6.16 -"decrypt' l K Y == Y # minus l (Crypt K Y)"
6.17 +"decrypt' l K Y == Y # remove l (Crypt K Y)"
6.18
6.19 declare decrypt'_def [simp]
6.20
6.21 @@ -274,7 +274,7 @@
6.22 apply (subgoal_tac "Crypt K Y:parts (set l)")
6.23 apply (drule parts_cnb, rotate_tac -1, simp)
6.24 apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub)
6.25 -apply (rule insert_mono, rule set_minus)
6.26 +apply (rule insert_mono, rule set_remove)
6.27 apply (simp add: analz_insertD, blast)
6.28 (* Crypt K Y:parts (set l) *)
6.29 apply (blast dest: kparts_parts)
6.30 @@ -284,7 +284,7 @@
6.31 apply (rule_tac K=K in guardK_Crypt, simp add: GuardK_def, simp)
6.32 apply (drule_tac t="set l'" in sym, simp)
6.33 apply (rule GuardK_kparts, simp, simp)
6.34 -apply (rule_tac B="set l'" in subset_trans, rule set_minus, blast)
6.35 +apply (rule_tac B="set l'" in subset_trans, rule set_remove, blast)
6.36 by (rule kparts_set)
6.37
6.38 lemma GuardK_invKey_finite: "[| Key n:analz G; GuardK n Ks G; finite G |]
7.1 --- a/src/HOL/Complex/CLim.thy Fri Mar 10 12:28:38 2006 +0100
7.2 +++ b/src/HOL/Complex/CLim.thy Fri Mar 10 15:33:48 2006 +0100
7.3 @@ -976,7 +976,7 @@
7.4 apply (simp add: diff_minus)
7.5 apply (drule_tac f = g in CDERIV_inverse_fun)
7.6 apply (drule_tac [2] CDERIV_mult, assumption+)
7.7 -apply (simp add: divide_inverse right_distrib power_inverse minus_mult_left
7.8 +apply (simp add: divide_inverse left_distrib power_inverse minus_mult_left
7.9 mult_ac
7.10 del: minus_mult_right [symmetric] minus_mult_left [symmetric]
7.11 complexpow_Suc)
8.1 --- a/src/HOL/HOL.thy Fri Mar 10 12:28:38 2006 +0100
8.2 +++ b/src/HOL/HOL.thy Fri Mar 10 15:33:48 2006 +0100
8.3 @@ -198,15 +198,20 @@
8.4 axclass times < type
8.5 axclass inverse < type
8.6
8.7 +consts
8.8 + plus :: "['a::plus, 'a] => 'a" (infixl "+" 65)
8.9 + uminus :: "'a::minus => 'a" ("- _" [81] 80)
8.10 + minus :: "['a::minus, 'a] => 'a" (infixl "-" 65)
8.11 + abs :: "'a::minus => 'a"
8.12 + times :: "['a::times, 'a] => 'a" (infixl "*" 70)
8.13 + inverse :: "'a::inverse => 'a"
8.14 + divide :: "['a::inverse, 'a] => 'a" (infixl "'/" 70)
8.15 +
8.16 global
8.17
8.18 consts
8.19 "0" :: "'a::zero" ("0")
8.20 "1" :: "'a::one" ("1")
8.21 - "+" :: "['a::plus, 'a] => 'a" (infixl 65)
8.22 - - :: "['a::minus, 'a] => 'a" (infixl 65)
8.23 - uminus :: "['a::minus] => 'a" ("- _" [81] 80)
8.24 - * :: "['a::times, 'a] => 'a" (infixl 70)
8.25
8.26 syntax
8.27 "_index1" :: index ("\<^sub>1")
8.28 @@ -223,12 +228,6 @@
8.29 in [tr' "0", tr' "1"] end;
8.30 *} -- {* show types that are presumably too general *}
8.31
8.32 -
8.33 -consts
8.34 - abs :: "'a::minus => 'a"
8.35 - inverse :: "'a::inverse => 'a"
8.36 - divide :: "['a::inverse, 'a] => 'a" (infixl "'/" 70)
8.37 -
8.38 syntax (xsymbols)
8.39 abs :: "'a::minus => 'a" ("\<bar>_\<bar>")
8.40 syntax (HTML output)
8.41 @@ -1408,11 +1407,7 @@
8.42 "op -->" "HOL.op_implies"
8.43 "op &" "HOL.op_and"
8.44 "op |" "HOL.op_or"
8.45 - "op +" "HOL.op_add"
8.46 - "op -" "HOL.op_minus"
8.47 - "op *" "HOL.op_times"
8.48 Not "HOL.not"
8.49 - uminus "HOL.uminus"
8.50 arbitrary "HOL.arbitrary"
8.51
8.52 code_syntax_const
9.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Fri Mar 10 12:28:38 2006 +0100
9.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Fri Mar 10 15:33:48 2006 +0100
9.3 @@ -182,9 +182,9 @@
9.4 ">=" > HOL4Compat.nat_ge
9.5 FUNPOW > HOL4Compat.FUNPOW
9.6 "<=" > "op <=" :: "[nat,nat]=>bool"
9.7 - "+" > "op +" :: "[nat,nat]=>nat"
9.8 - "*" > "op *" :: "[nat,nat]=>nat"
9.9 - "-" > "op -" :: "[nat,nat]=>nat"
9.10 + "+" > "HOL.plus" :: "[nat,nat]=>nat"
9.11 + "*" > "HOL.times" :: "[nat,nat]=>nat"
9.12 + "-" > "HOL.minus" :: "[nat,nat]=>nat"
9.13 MIN > Orderings.min :: "[nat,nat]=>nat"
9.14 MAX > Orderings.max :: "[nat,nat]=>nat"
9.15 DIV > "Divides.op div" :: "[nat,nat]=>nat"
10.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Fri Mar 10 12:28:38 2006 +0100
10.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Fri Mar 10 15:33:48 2006 +0100
10.3 @@ -21,8 +21,8 @@
10.4 real_1 > 1 :: real
10.5 real_neg > uminus :: "real => real"
10.6 inv > HOL.inverse :: "real => real"
10.7 - real_add > "op +" :: "[real,real] => real"
10.8 - real_mul > "op *" :: "[real,real] => real"
10.9 + real_add > HOL.plus :: "[real,real] => real"
10.10 + real_mul > HOL.times :: "[real,real] => real"
10.11 real_lt > "op <" :: "[real,real] => bool";
10.12
10.13 ignore_thms
10.14 @@ -52,7 +52,7 @@
10.15 real_gt > HOL4Compat.real_gt
10.16 real_ge > HOL4Compat.real_ge
10.17 real_lte > "op <=" :: "[real,real] => bool"
10.18 - real_sub > "op -" :: "[real,real] => real"
10.19 + real_sub > HOL.minus :: "[real,real] => real"
10.20 "/" > HOL.divide :: "[real,real] => real"
10.21 pow > Nat.power :: "[real,nat] => real"
10.22 abs > HOL.abs :: "real => real"
11.1 --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Fri Mar 10 12:28:38 2006 +0100
11.2 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Fri Mar 10 15:33:48 2006 +0100
11.3 @@ -76,9 +76,9 @@
11.4 SUC > Suc
11.5 PRE > HOLLightCompat.Pred
11.6 NUMERAL > HOL4Compat.NUMERAL
11.7 - "+" > "op +" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
11.8 - "*" > "op *" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
11.9 - "-" > "op -" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
11.10 + "+" > HOL.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
11.11 + "*" > HOL.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
11.12 + "-" > HOL.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
11.13 BIT0 > HOLLightCompat.NUMERAL_BIT0
11.14 BIT1 > HOL4Compat.NUMERAL_BIT1
11.15 INL > Sum_Type.Inl
12.1 --- a/src/HOL/Import/HOL/arithmetic.imp Fri Mar 10 12:28:38 2006 +0100
12.2 +++ b/src/HOL/Import/HOL/arithmetic.imp Fri Mar 10 15:33:48 2006 +0100
12.3 @@ -24,9 +24,9 @@
12.4 ">=" > "HOL4Compat.nat_ge"
12.5 ">" > "HOL4Compat.nat_gt"
12.6 "<=" > "op <=" :: "nat => nat => bool"
12.7 - "-" > "op -" :: "nat => nat => nat"
12.8 - "+" > "op +" :: "nat => nat => nat"
12.9 - "*" > "op *" :: "nat => nat => nat"
12.10 + "-" > "HOL.minus" :: "nat => nat => nat"
12.11 + "+" > "HOL.plus" :: "nat => nat => nat"
12.12 + "*" > "HOL.times" :: "nat => nat => nat"
12.13
12.14 thm_maps
12.15 "num_case_def" > "HOL4Compat.num_case_def"
13.1 --- a/src/HOL/Import/HOL/real.imp Fri Mar 10 12:28:38 2006 +0100
13.2 +++ b/src/HOL/Import/HOL/real.imp Fri Mar 10 15:33:48 2006 +0100
13.3 @@ -10,7 +10,7 @@
13.4 const_maps
13.5 "sup" > "HOL4Real.real.sup"
13.6 "sum" > "HOL4Real.real.sum"
13.7 - "real_sub" > "op -" :: "real => real => real"
13.8 + "real_sub" > "HOL.minus" :: "real => real => real"
13.9 "real_of_num" > "RealDef.real" :: "nat => real"
13.10 "real_lte" > "op <=" :: "real => real => bool"
13.11 "real_gt" > "HOL4Compat.real_gt"
14.1 --- a/src/HOL/Import/HOL/realax.imp Fri Mar 10 12:28:38 2006 +0100
14.2 +++ b/src/HOL/Import/HOL/realax.imp Fri Mar 10 15:33:48 2006 +0100
14.3 @@ -27,10 +27,10 @@
14.4 "treal_add" > "HOL4Real.realax.treal_add"
14.5 "treal_1" > "HOL4Real.realax.treal_1"
14.6 "treal_0" > "HOL4Real.realax.treal_0"
14.7 - "real_neg" > "uminus" :: "real => real"
14.8 - "real_mul" > "op *" :: "real => real => real"
14.9 + "real_neg" > "HOL.uminus" :: "real => real"
14.10 + "real_mul" > "HOL.times" :: "real => real => real"
14.11 "real_lt" > "op <" :: "real => real => bool"
14.12 - "real_add" > "op +" :: "real => real => real"
14.13 + "real_add" > "HOL.plus" :: "real => real => real"
14.14 "real_1" > "1" :: "real"
14.15 "real_0" > "0" :: "real"
14.16 "inv" > "HOL.inverse" :: "real => real"
15.1 --- a/src/HOL/Import/HOLLight/HOLLight.thy Fri Mar 10 12:28:38 2006 +0100
15.2 +++ b/src/HOL/Import/HOLLight/HOLLight.thy Fri Mar 10 15:33:48 2006 +0100
15.3 @@ -1119,37 +1119,37 @@
15.4 (%x::nat.
15.5 (All::(nat => bool) => bool)
15.6 (%xa::nat.
15.7 - (op =::nat => nat => bool) ((op +::nat => nat => nat) x xa)
15.8 - ((op +::nat => nat => nat) x xa))))
15.9 + (op =::nat => nat => bool) ((HOL.plus::nat => nat => nat) x xa)
15.10 + ((HOL.plus::nat => nat => nat) x xa))))
15.11 ((op &::bool => bool => bool)
15.12 - ((op =::nat => nat => bool) ((op +::nat => nat => nat) (0::nat) (0::nat))
15.13 + ((op =::nat => nat => bool) ((HOL.plus::nat => nat => nat) (0::nat) (0::nat))
15.14 (0::nat))
15.15 ((op &::bool => bool => bool)
15.16 ((All::(nat => bool) => bool)
15.17 (%x::nat.
15.18 (op =::nat => nat => bool)
15.19 - ((op +::nat => nat => nat) (0::nat)
15.20 + ((HOL.plus::nat => nat => nat) (0::nat)
15.21 ((NUMERAL_BIT0::nat => nat) x))
15.22 ((NUMERAL_BIT0::nat => nat) x)))
15.23 ((op &::bool => bool => bool)
15.24 ((All::(nat => bool) => bool)
15.25 (%x::nat.
15.26 (op =::nat => nat => bool)
15.27 - ((op +::nat => nat => nat) (0::nat)
15.28 + ((HOL.plus::nat => nat => nat) (0::nat)
15.29 ((NUMERAL_BIT1::nat => nat) x))
15.30 ((NUMERAL_BIT1::nat => nat) x)))
15.31 ((op &::bool => bool => bool)
15.32 ((All::(nat => bool) => bool)
15.33 (%x::nat.
15.34 (op =::nat => nat => bool)
15.35 - ((op +::nat => nat => nat) ((NUMERAL_BIT0::nat => nat) x)
15.36 + ((HOL.plus::nat => nat => nat) ((NUMERAL_BIT0::nat => nat) x)
15.37 (0::nat))
15.38 ((NUMERAL_BIT0::nat => nat) x)))
15.39 ((op &::bool => bool => bool)
15.40 ((All::(nat => bool) => bool)
15.41 (%x::nat.
15.42 (op =::nat => nat => bool)
15.43 - ((op +::nat => nat => nat) ((NUMERAL_BIT1::nat => nat) x)
15.44 + ((HOL.plus::nat => nat => nat) ((NUMERAL_BIT1::nat => nat) x)
15.45 (0::nat))
15.46 ((NUMERAL_BIT1::nat => nat) x)))
15.47 ((op &::bool => bool => bool)
15.48 @@ -1158,44 +1158,44 @@
15.49 (All::(nat => bool) => bool)
15.50 (%xa::nat.
15.51 (op =::nat => nat => bool)
15.52 - ((op +::nat => nat => nat)
15.53 + ((HOL.plus::nat => nat => nat)
15.54 ((NUMERAL_BIT0::nat => nat) x)
15.55 ((NUMERAL_BIT0::nat => nat) xa))
15.56 ((NUMERAL_BIT0::nat => nat)
15.57 - ((op +::nat => nat => nat) x xa)))))
15.58 + ((HOL.plus::nat => nat => nat) x xa)))))
15.59 ((op &::bool => bool => bool)
15.60 ((All::(nat => bool) => bool)
15.61 (%x::nat.
15.62 (All::(nat => bool) => bool)
15.63 (%xa::nat.
15.64 (op =::nat => nat => bool)
15.65 - ((op +::nat => nat => nat)
15.66 + ((HOL.plus::nat => nat => nat)
15.67 ((NUMERAL_BIT0::nat => nat) x)
15.68 ((NUMERAL_BIT1::nat => nat) xa))
15.69 ((NUMERAL_BIT1::nat => nat)
15.70 - ((op +::nat => nat => nat) x xa)))))
15.71 + ((HOL.plus::nat => nat => nat) x xa)))))
15.72 ((op &::bool => bool => bool)
15.73 ((All::(nat => bool) => bool)
15.74 (%x::nat.
15.75 (All::(nat => bool) => bool)
15.76 (%xa::nat.
15.77 (op =::nat => nat => bool)
15.78 - ((op +::nat => nat => nat)
15.79 + ((HOL.plus::nat => nat => nat)
15.80 ((NUMERAL_BIT1::nat => nat) x)
15.81 ((NUMERAL_BIT0::nat => nat) xa))
15.82 ((NUMERAL_BIT1::nat => nat)
15.83 - ((op +::nat => nat => nat) x xa)))))
15.84 + ((HOL.plus::nat => nat => nat) x xa)))))
15.85 ((All::(nat => bool) => bool)
15.86 (%x::nat.
15.87 (All::(nat => bool) => bool)
15.88 (%xa::nat.
15.89 (op =::nat => nat => bool)
15.90 - ((op +::nat => nat => nat)
15.91 + ((HOL.plus::nat => nat => nat)
15.92 ((NUMERAL_BIT1::nat => nat) x)
15.93 ((NUMERAL_BIT1::nat => nat) xa))
15.94 ((NUMERAL_BIT0::nat => nat)
15.95 ((Suc::nat => nat)
15.96 - ((op +::nat => nat => nat) x
15.97 + ((HOL.plus::nat => nat => nat) x
15.98 xa))))))))))))))"
15.99 by (import hollight ARITH_ADD)
15.100
15.101 @@ -1258,7 +1258,7 @@
15.102 ((op *::nat => nat => nat)
15.103 ((NUMERAL_BIT0::nat => nat) x)
15.104 ((NUMERAL_BIT1::nat => nat) xa))
15.105 - ((op +::nat => nat => nat)
15.106 + ((HOL.plus::nat => nat => nat)
15.107 ((NUMERAL_BIT0::nat => nat) x)
15.108 ((NUMERAL_BIT0::nat => nat)
15.109 ((NUMERAL_BIT0::nat => nat)
15.110 @@ -1272,7 +1272,7 @@
15.111 ((op *::nat => nat => nat)
15.112 ((NUMERAL_BIT1::nat => nat) x)
15.113 ((NUMERAL_BIT0::nat => nat) xa))
15.114 - ((op +::nat => nat => nat)
15.115 + ((HOL.plus::nat => nat => nat)
15.116 ((NUMERAL_BIT0::nat => nat) xa)
15.117 ((NUMERAL_BIT0::nat => nat)
15.118 ((NUMERAL_BIT0::nat => nat)
15.119 @@ -1285,9 +1285,9 @@
15.120 ((op *::nat => nat => nat)
15.121 ((NUMERAL_BIT1::nat => nat) x)
15.122 ((NUMERAL_BIT1::nat => nat) xa))
15.123 - ((op +::nat => nat => nat)
15.124 + ((HOL.plus::nat => nat => nat)
15.125 ((NUMERAL_BIT1::nat => nat) x)
15.126 - ((op +::nat => nat => nat)
15.127 + ((HOL.plus::nat => nat => nat)
15.128 ((NUMERAL_BIT0::nat => nat) xa)
15.129 ((NUMERAL_BIT0::nat => nat)
15.130 ((NUMERAL_BIT0::nat => nat)
15.131 @@ -7462,7 +7462,7 @@
15.132 (%i::nat.
15.133 ($::('A::type, ('M::type, 'N::type) finite_sum) cart
15.134 => nat => 'A::type)
15.135 - u ((op +::nat => nat => nat) i
15.136 + u ((HOL.plus::nat => nat => nat) i
15.137 ((dimindex::('M::type => bool) => nat)
15.138 (hollight.UNIV::'M::type => bool)))))"
15.139
15.140 @@ -7478,14 +7478,14 @@
15.141 (%i::nat.
15.142 ($::('A::type, ('M::type, 'N::type) finite_sum) cart
15.143 => nat => 'A::type)
15.144 - u ((op +::nat => nat => nat) i
15.145 + u ((HOL.plus::nat => nat => nat) i
15.146 ((dimindex::('M::type => bool) => nat)
15.147 (hollight.UNIV::'M::type => bool)))))"
15.148 by (import hollight DEF_sndcart)
15.149
15.150 lemma DIMINDEX_HAS_SIZE_FINITE_SUM: "(HAS_SIZE::(('M::type, 'N::type) finite_sum => bool) => nat => bool)
15.151 (hollight.UNIV::('M::type, 'N::type) finite_sum => bool)
15.152 - ((op +::nat => nat => nat)
15.153 + ((HOL.plus::nat => nat => nat)
15.154 ((dimindex::('M::type => bool) => nat) (hollight.UNIV::'M::type => bool))
15.155 ((dimindex::('N::type => bool) => nat)
15.156 (hollight.UNIV::'N::type => bool)))"
15.157 @@ -7494,7 +7494,7 @@
15.158 lemma DIMINDEX_FINITE_SUM: "(op =::nat => nat => bool)
15.159 ((dimindex::(('M::type, 'N::type) finite_sum => bool) => nat)
15.160 (hollight.UNIV::('M::type, 'N::type) finite_sum => bool))
15.161 - ((op +::nat => nat => nat)
15.162 + ((HOL.plus::nat => nat => nat)
15.163 ((dimindex::('M::type => bool) => nat) (hollight.UNIV::'M::type => bool))
15.164 ((dimindex::('N::type => bool) => nat)
15.165 (hollight.UNIV::'N::type => bool)))"
15.166 @@ -8025,7 +8025,7 @@
15.167 (nsum::('q_51017::type => bool) => ('q_51017::type => nat) => nat)
15.168 ((iterate::(nat => nat => nat)
15.169 => ('q_51017::type => bool) => ('q_51017::type => nat) => nat)
15.170 - (op +::nat => nat => nat))"
15.171 + (HOL.plus::nat => nat => nat))"
15.172
15.173 lemma DEF_nsum: "(op =::(('q_51017::type => bool) => ('q_51017::type => nat) => nat)
15.174 => (('q_51017::type => bool) => ('q_51017::type => nat) => nat)
15.175 @@ -8033,17 +8033,17 @@
15.176 (nsum::('q_51017::type => bool) => ('q_51017::type => nat) => nat)
15.177 ((iterate::(nat => nat => nat)
15.178 => ('q_51017::type => bool) => ('q_51017::type => nat) => nat)
15.179 - (op +::nat => nat => nat))"
15.180 + (HOL.plus::nat => nat => nat))"
15.181 by (import hollight DEF_nsum)
15.182
15.183 lemma NEUTRAL_ADD: "(op =::nat => nat => bool)
15.184 - ((neutral::(nat => nat => nat) => nat) (op +::nat => nat => nat)) (0::nat)"
15.185 + ((neutral::(nat => nat => nat) => nat) (HOL.plus::nat => nat => nat)) (0::nat)"
15.186 by (import hollight NEUTRAL_ADD)
15.187
15.188 lemma NEUTRAL_MUL: "neutral op * = NUMERAL_BIT1 0"
15.189 by (import hollight NEUTRAL_MUL)
15.190
15.191 -lemma MONOIDAL_ADD: "(monoidal::(nat => nat => nat) => bool) (op +::nat => nat => nat)"
15.192 +lemma MONOIDAL_ADD: "(monoidal::(nat => nat => nat) => bool) (HOL.plus::nat => nat => nat)"
15.193 by (import hollight MONOIDAL_ADD)
15.194
15.195 lemma MONOIDAL_MUL: "(monoidal::(nat => nat => nat) => bool) (op *::nat => nat => nat)"
15.196 @@ -8068,7 +8068,7 @@
15.197 by (import hollight NSUM_DIFF)
15.198
15.199 lemma NSUM_SUPPORT: "ALL (x::'q_51214::type => nat) xa::'q_51214::type => bool.
15.200 - FINITE (support op + x xa) --> nsum (support op + x xa) x = nsum xa x"
15.201 + FINITE (support HOL.plus x xa) --> nsum (support HOL.plus x xa) x = nsum xa x"
15.202 by (import hollight NSUM_SUPPORT)
15.203
15.204 lemma NSUM_ADD: "ALL (f::'q_51260::type => nat) (g::'q_51260::type => nat)
16.1 --- a/src/HOL/Import/HOLLight/hollight.imp Fri Mar 10 12:28:38 2006 +0100
16.2 +++ b/src/HOL/Import/HOLLight/hollight.imp Fri Mar 10 15:33:48 2006 +0100
16.3 @@ -238,10 +238,10 @@
16.4 "<=" > "HOLLight.hollight.<="
16.5 "<" > "HOLLight.hollight.<"
16.6 "/\\" > "op &"
16.7 - "-" > "op -" :: "nat => nat => nat"
16.8 + "-" > "HOL.minus" :: "nat => nat => nat"
16.9 "," > "Pair"
16.10 - "+" > "op +" :: "nat => nat => nat"
16.11 - "*" > "op *" :: "nat => nat => nat"
16.12 + "+" > "HOL.plus" :: "nat => nat => nat"
16.13 + "*" > "HOL.times" :: "nat => nat => nat"
16.14 "$" > "HOLLight.hollight.$"
16.15 "!" > "All"
16.16
17.1 --- a/src/HOL/Integ/IntDef.thy Fri Mar 10 12:28:38 2006 +0100
17.2 +++ b/src/HOL/Integ/IntDef.thy Fri Mar 10 15:33:48 2006 +0100
17.3 @@ -886,14 +886,14 @@
17.4 by (simp add: nat_aux_def)
17.5
17.6 consts_code
17.7 - "0" :: "int" ("0")
17.8 - "1" :: "int" ("1")
17.9 - "uminus" :: "int => int" ("~")
17.10 - "op +" :: "int => int => int" ("(_ +/ _)")
17.11 - "op *" :: "int => int => int" ("(_ */ _)")
17.12 - "op <" :: "int => int => bool" ("(_ </ _)")
17.13 - "op <=" :: "int => int => bool" ("(_ <=/ _)")
17.14 - "neg" ("(_ < 0)")
17.15 + "0" :: "int" ("0")
17.16 + "1" :: "int" ("1")
17.17 + "HOL.uminus" :: "int => int" ("~")
17.18 + "HOL.plus" :: "int => int => int" ("(_ +/ _)")
17.19 + "HOL.times" :: "int => int => int" ("(_ */ _)")
17.20 + "op <" :: "int => int => bool" ("(_ </ _)")
17.21 + "op <=" :: "int => int => bool" ("(_ <=/ _)")
17.22 + "neg" ("(_ < 0)")
17.23
17.24 code_syntax_tyco int
17.25 ml (target_atom "IntInf.int")
18.1 --- a/src/HOL/Integ/cooper_dec.ML Fri Mar 10 12:28:38 2006 +0100
18.2 +++ b/src/HOL/Integ/cooper_dec.ML Fri Mar 10 15:33:48 2006 +0100
18.3 @@ -116,8 +116,8 @@
18.4
18.5 fun linear_cmul n tm = if n = 0 then zero else let fun times n k = n*k in
18.6 ( case tm of
18.7 - (Const("op +",T) $ (Const ("op *",T1 ) $c1 $ x1) $ rest) =>
18.8 - Const("op +",T) $ ((Const("op *",T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest)
18.9 + (Const("HOL.plus",T) $ (Const ("HOL.times",T1 ) $c1 $ x1) $ rest) =>
18.10 + Const("HOL.plus",T) $ ((Const("HOL.times",T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest)
18.11 |_ => numeral1 (times n) tm)
18.12 end ;
18.13
18.14 @@ -139,23 +139,23 @@
18.15 fun linear_add vars tm1 tm2 =
18.16 let fun addwith x y = x + y in
18.17 (case (tm1,tm2) of
18.18 - ((Const ("op +",T1) $ ( Const("op *",T2) $ c1 $ x1) $ rest1),(Const
18.19 - ("op +",T3)$( Const("op *",T4) $ c2 $ x2) $ rest2)) =>
18.20 + ((Const ("HOL.plus",T1) $ ( Const("HOL.times",T2) $ c1 $ x1) $ rest1),(Const
18.21 + ("HOL.plus",T3)$( Const("HOL.times",T4) $ c2 $ x2) $ rest2)) =>
18.22 if x1 = x2 then
18.23 let val c = (numeral2 (addwith) c1 c2)
18.24 in
18.25 if c = zero then (linear_add vars rest1 rest2)
18.26 - else (Const("op +",T1) $ (Const("op *",T2) $ c $ x1) $ (linear_add vars rest1 rest2))
18.27 + else (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c $ x1) $ (linear_add vars rest1 rest2))
18.28 end
18.29 else
18.30 - if earlierv vars x1 x2 then (Const("op +",T1) $
18.31 - (Const("op *",T2)$ c1 $ x1) $ (linear_add vars rest1 tm2))
18.32 - else (Const("op +",T1) $ (Const("op *",T2) $ c2 $ x2) $ (linear_add vars tm1 rest2))
18.33 - |((Const("op +",T1) $ (Const("op *",T2) $ c1 $ x1) $ rest1) ,_) =>
18.34 - (Const("op +",T1)$ (Const("op *",T2) $ c1 $ x1) $ (linear_add vars
18.35 + if earlierv vars x1 x2 then (Const("HOL.plus",T1) $
18.36 + (Const("HOL.times",T2)$ c1 $ x1) $ (linear_add vars rest1 tm2))
18.37 + else (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c2 $ x2) $ (linear_add vars tm1 rest2))
18.38 + |((Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c1 $ x1) $ rest1) ,_) =>
18.39 + (Const("HOL.plus",T1)$ (Const("HOL.times",T2) $ c1 $ x1) $ (linear_add vars
18.40 rest1 tm2))
18.41 - |(_, (Const("op +",T1) $(Const("op *",T2) $ c2 $ x2) $ rest2)) =>
18.42 - (Const("op +",T1) $ (Const("op *",T2) $ c2 $ x2) $ (linear_add vars tm1
18.43 + |(_, (Const("HOL.plus",T1) $(Const("HOL.times",T2) $ c2 $ x2) $ rest2)) =>
18.44 + (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c2 $ x2) $ (linear_add vars tm1
18.45 rest2))
18.46 | (_,_) => numeral2 (addwith) tm1 tm2)
18.47
18.48 @@ -180,13 +180,13 @@
18.49 Free(x,T)*)
18.50
18.51 fun lint vars tm = if is_numeral tm then tm else case tm of
18.52 - (Free (x,T)) => (HOLogic.mk_binop "op +" ((HOLogic.mk_binop "op *" ((mk_numeral 1),Free (x,T))), zero))
18.53 - |(Bound i) => (Const("op +",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $
18.54 - (Const("op *",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_numeral 1) $ (Bound i)) $ zero)
18.55 - |(Const("uminus",_) $ t ) => (linear_neg (lint vars t))
18.56 - |(Const("op +",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t))
18.57 - |(Const("op -",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t))
18.58 - |(Const ("op *",_) $ s $ t) =>
18.59 + (Free (x,T)) => (HOLogic.mk_binop "HOL.plus" ((HOLogic.mk_binop "HOL.times" ((mk_numeral 1),Free (x,T))), zero))
18.60 + |(Bound i) => (Const("HOL.plus",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $
18.61 + (Const("HOL.times",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_numeral 1) $ (Bound i)) $ zero)
18.62 + |(Const("HOL.uminus",_) $ t ) => (linear_neg (lint vars t))
18.63 + |(Const("HOL.plus",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t))
18.64 + |(Const("HOL.minus",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t))
18.65 + |(Const ("HOL.times",_) $ s $ t) =>
18.66 let val s' = lint vars s
18.67 val t' = lint vars t
18.68 in
18.69 @@ -212,14 +212,14 @@
18.70 end
18.71 else (warning "Nonlinear term --- Non numeral leftside at dvd"
18.72 ;raise COOPER)
18.73 - |linform vars (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) )
18.74 - |linform vars (Const("op <",_)$ s $t ) = (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
18.75 - |linform vars (Const("op >",_) $ s $ t ) = (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t))
18.76 + |linform vars (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) )
18.77 + |linform vars (Const("op <",_)$ s $t ) = (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
18.78 + |linform vars (Const("op >",_) $ s $ t ) = (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t))
18.79 |linform vars (Const("op <=",_)$ s $ t ) =
18.80 - (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("op +",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s))
18.81 + (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s))
18.82 |linform vars (Const("op >=",_)$ s $ t ) =
18.83 - (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT -->
18.84 - HOLogic.intT) $ (Const("op +",HOLogic.intT --> HOLogic.intT -->
18.85 + (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT -->
18.86 + HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT -->
18.87 HOLogic.intT) $s $(mk_numeral 1)) $ t))
18.88
18.89 |linform vars fm = fm;
18.90 @@ -246,7 +246,7 @@
18.91 fun lcm_num a b = (abs a*b) div (gcd (abs a) (abs b));
18.92
18.93 fun formlcm x fm = case fm of
18.94 - (Const (p,_)$ _ $(Const ("op +", _)$(Const ("op *",_)$ c $ y ) $z ) ) => if
18.95 + (Const (p,_)$ _ $(Const ("HOL.plus", _)$(Const ("HOL.times",_)$ c $ y ) $z ) ) => if
18.96 (is_arith_rel fm) andalso (x = y) then (abs(dest_numeral c)) else 1
18.97 | ( Const ("Not", _) $p) => formlcm x p
18.98 | ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q)
18.99 @@ -259,13 +259,13 @@
18.100
18.101 fun adjustcoeff x l fm =
18.102 case fm of
18.103 - (Const(p,_) $d $( Const ("op +", _)$(Const ("op *",_) $
18.104 + (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $
18.105 c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then
18.106 let val m = l div (dest_numeral c)
18.107 val n = (if p = "op <" then abs(m) else m)
18.108 - val xtm = HOLogic.mk_binop "op *" ((mk_numeral (m div n)), x)
18.109 + val xtm = HOLogic.mk_binop "HOL.times" ((mk_numeral (m div n)), x)
18.110 in
18.111 - (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) ))))
18.112 + (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
18.113 end
18.114 else fm
18.115 |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeff x l p)
18.116 @@ -282,8 +282,8 @@
18.117 val fm' = adjustcoeff x l fm in
18.118 if l = 1 then fm'
18.119 else
18.120 - let val xp = (HOLogic.mk_binop "op +"
18.121 - ((HOLogic.mk_binop "op *" ((mk_numeral 1), x )), zero))
18.122 + let val xp = (HOLogic.mk_binop "HOL.plus"
18.123 + ((HOLogic.mk_binop "HOL.times" ((mk_numeral 1), x )), zero))
18.124 in
18.125 HOLogic.conj $(HOLogic.mk_binrel "Divides.op dvd" ((mk_numeral l) , xp )) $ (adjustcoeff x l fm)
18.126 end
18.127 @@ -294,12 +294,12 @@
18.128 (*
18.129 fun adjustcoeffeq x l fm =
18.130 case fm of
18.131 - (Const(p,_) $d $( Const ("op +", _)$(Const ("op *",_) $
18.132 + (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $
18.133 c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then
18.134 let val m = l div (dest_numeral c)
18.135 val n = (if p = "op <" then abs(m) else m)
18.136 - val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x))
18.137 - in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) ))))
18.138 + val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x))
18.139 + in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
18.140 end
18.141 else fm
18.142 |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeffeq x l p)
18.143 @@ -315,11 +315,11 @@
18.144 (* ------------------------------------------------------------------------- *)
18.145
18.146 fun minusinf x fm = case fm of
18.147 - (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
18.148 + (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
18.149 if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const
18.150 else fm
18.151
18.152 - |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z
18.153 + |(Const("op <",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
18.154 )) => if (x = y)
18.155 then if (pm1 = one) andalso (c = zero) then HOLogic.false_const
18.156 else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.true_const
18.157 @@ -336,11 +336,11 @@
18.158 (* ------------------------------------------------------------------------- *)
18.159
18.160 fun plusinf x fm = case fm of
18.161 - (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
18.162 + (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
18.163 if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const
18.164 else fm
18.165
18.166 - |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z
18.167 + |(Const("op <",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
18.168 )) => if (x = y)
18.169 then if (pm1 = one) andalso (c = zero) then HOLogic.true_const
18.170 else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.false_const
18.171 @@ -356,7 +356,7 @@
18.172 (* The LCM of all the divisors that involve x. *)
18.173 (* ------------------------------------------------------------------------- *)
18.174
18.175 -fun divlcm x (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z ) ) =
18.176 +fun divlcm x (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) =
18.177 if x = y then abs(dest_numeral d) else 1
18.178 |divlcm x ( Const ("Not", _) $ p) = divlcm x p
18.179 |divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q)
18.180 @@ -370,15 +370,15 @@
18.181 fun bset x fm = case fm of
18.182 (Const ("Not", _) $ p) => if (is_arith_rel p) then
18.183 (case p of
18.184 - (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $c2 $y) $a ) )
18.185 + (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $c2 $y) $a ) )
18.186 => if (is_arith_rel p) andalso (x= y) andalso (c2 = one) andalso (c1 = zero)
18.187 then [linear_neg a]
18.188 else bset x p
18.189 |_ =>[])
18.190
18.191 else bset x p
18.192 - |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +",_) $ (Const ("op *",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_numeral 1))] else []
18.193 - |(Const ("op <",_) $ c1$ (Const ("op +",_) $(Const ("op *",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else []
18.194 + |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_numeral 1))] else []
18.195 + |(Const ("op <",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else []
18.196 |(Const ("op &",_) $ p $ q) => (bset x p) union (bset x q)
18.197 |(Const ("op |",_) $ p $ q) => (bset x p) union (bset x q)
18.198 |_ => [];
18.199 @@ -390,15 +390,15 @@
18.200 fun aset x fm = case fm of
18.201 (Const ("Not", _) $ p) => if (is_arith_rel p) then
18.202 (case p of
18.203 - (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $c2 $y) $a ) )
18.204 + (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $c2 $y) $a ) )
18.205 => if (x= y) andalso (c2 = one) andalso (c1 = zero)
18.206 then [linear_neg a]
18.207 else []
18.208 |_ =>[])
18.209
18.210 else aset x p
18.211 - |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +",_) $ (Const ("op *",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_numeral 1) a] else []
18.212 - |(Const ("op <",_) $ c1$ (Const ("op +",_) $(Const ("op *",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_numeral (~1))) then [a] else []
18.213 + |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_numeral 1) a] else []
18.214 + |(Const ("op <",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_numeral (~1))) then [a] else []
18.215 |(Const ("op &",_) $ p $ q) => (aset x p) union (aset x q)
18.216 |(Const ("op |",_) $ p $ q) => (aset x p) union (aset x q)
18.217 |_ => [];
18.218 @@ -409,7 +409,7 @@
18.219 (* ------------------------------------------------------------------------- *)
18.220
18.221 fun linrep vars x t fm = case fm of
18.222 - ((Const(p,_)$ d $ (Const("op +",_)$(Const("op *",_)$ c $ y) $ z))) =>
18.223 + ((Const(p,_)$ d $ (Const("HOL.plus",_)$(Const("HOL.times",_)$ c $ y) $ z))) =>
18.224 if (x = y) andalso (is_arith_rel fm)
18.225 then
18.226 let val ct = linear_cmul (dest_numeral c) t
18.227 @@ -435,8 +435,8 @@
18.228 val dn = dest_numeral d
18.229 fun coeffs_of x = case x of
18.230 Const(p,_) $ tl $ tr =>
18.231 - if p = "op +" then (coeffs_of tl) union (coeffs_of tr)
18.232 - else if p = "op *"
18.233 + if p = "HOL.plus" then (coeffs_of tl) union (coeffs_of tr)
18.234 + else if p = "HOL.times"
18.235 then if (is_numeral tr)
18.236 then [(dest_numeral tr) * (dest_numeral tl)]
18.237 else [dest_numeral tl]
19.1 --- a/src/HOL/Integ/cooper_proof.ML Fri Mar 10 12:28:38 2006 +0100
19.2 +++ b/src/HOL/Integ/cooper_proof.ML Fri Mar 10 15:33:48 2006 +0100
19.3 @@ -165,11 +165,11 @@
19.4 (* ------------------------------------------------------------------------- *)
19.5
19.6 fun norm_zero_one fm = case fm of
19.7 - (Const ("op *",_) $ c $ t) =>
19.8 + (Const ("HOL.times",_) $ c $ t) =>
19.9 if c = one then (norm_zero_one t)
19.10 else if (dest_numeral c = ~1)
19.11 - then (Const("uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
19.12 - else (HOLogic.mk_binop "op *" (norm_zero_one c,norm_zero_one t))
19.13 + then (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
19.14 + else (HOLogic.mk_binop "HOL.times" (norm_zero_one c,norm_zero_one t))
19.15 |(node $ rest) => ((norm_zero_one node)$(norm_zero_one rest))
19.16 |(Abs(x,T,p)) => (Abs(x,T,(norm_zero_one p)))
19.17 |_ => fm;
19.18 @@ -255,13 +255,13 @@
19.19 (*==================================================*)
19.20
19.21 fun decomp_adjustcoeffeq sg x l fm = case fm of
19.22 - (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("op +", _)$(Const ("op *",_) $ c $ y ) $z )))) =>
19.23 + (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $ c $ y ) $z )))) =>
19.24 let
19.25 val m = l div (dest_numeral c)
19.26 val n = if (x = y) then abs (m) else 1
19.27 - val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x))
19.28 + val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x))
19.29 val rs = if (x = y)
19.30 - then (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) ))))
19.31 + then (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
19.32 else HOLogic.mk_binrel "op <" (zero,linear_sub [] one rt )
19.33 val ck = cterm_of sg (mk_numeral n)
19.34 val cc = cterm_of sg c
19.35 @@ -273,14 +273,14 @@
19.36 in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
19.37 end
19.38
19.39 - |(Const(p,_) $a $( Const ("op +", _)$(Const ("op *",_) $
19.40 + |(Const(p,_) $a $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $
19.41 c $ y ) $t )) =>
19.42 if (is_arith_rel fm) andalso (x = y)
19.43 then
19.44 let val m = l div (dest_numeral c)
19.45 val k = (if p = "op <" then abs(m) else m)
19.46 - val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div k)*l) ), x))
19.47 - val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul k t) ))))
19.48 + val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div k)*l) ), x))
19.49 + val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul k t) ))))
19.50
19.51 val ck = cterm_of sg (mk_numeral k)
19.52 val cc = cterm_of sg c
19.53 @@ -335,28 +335,28 @@
19.54 val cfalse = cterm_of sg HOLogic.false_const
19.55 val fm = norm_zero_one fm1
19.56 in case fm1 of
19.57 - (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
19.58 + (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
19.59 if (x=y) andalso (c1= zero) andalso (c2= one) then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
19.60 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
19.61
19.62 - |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
19.63 + |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
19.64 if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one)
19.65 then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf))
19.66 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
19.67
19.68 - |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
19.69 + |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
19.70 if (y=x) andalso (c1 = zero) then
19.71 if (pm1 = one) then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf)) else
19.72 (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
19.73 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
19.74
19.75 - |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
19.76 + |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
19.77 if y=x then let val cz = cterm_of sg (norm_zero_one z)
19.78 val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
19.79 in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf)))
19.80 end
19.81 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
19.82 - |(Const("Divides.op dvd",_)$ d $ (db as (Const ("op +",_) $ (Const ("op *",_) $
19.83 + |(Const("Divides.op dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
19.84 c $ y ) $ z))) =>
19.85 if y=x then let val cz = cterm_of sg (norm_zero_one z)
19.86 val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
19.87 @@ -373,22 +373,22 @@
19.88 let
19.89 val fm = norm_zero_one fm1
19.90 in case fm1 of
19.91 - (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
19.92 + (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
19.93 if (x=y) andalso (c1=zero) andalso (c2=one)
19.94 then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_minf))
19.95 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
19.96
19.97 - |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
19.98 + |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
19.99 if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
19.100 then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_minf))
19.101 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
19.102
19.103 - |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
19.104 + |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
19.105 if (y=x) andalso (c1 =zero) then
19.106 if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else
19.107 (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_minf))
19.108 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
19.109 - |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
19.110 + |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
19.111 if y=x then let val cd = cterm_of sg (norm_zero_one d)
19.112 val cz = cterm_of sg (norm_zero_one z)
19.113 in(instantiate' [] [SOME cd, SOME cz] (not_dvd_eq_minf))
19.114 @@ -396,7 +396,7 @@
19.115
19.116 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
19.117
19.118 - |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
19.119 + |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
19.120 if y=x then let val cd = cterm_of sg (norm_zero_one d)
19.121 val cz = cterm_of sg (norm_zero_one z)
19.122 in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_minf))
19.123 @@ -431,30 +431,30 @@
19.124 val cfalse = cterm_of sg HOLogic.false_const
19.125 val fm = norm_zero_one fm1
19.126 in case fm1 of
19.127 - (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
19.128 + (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
19.129 if ((x=y) andalso (c1= zero) andalso (c2= one))
19.130 then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf))
19.131 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
19.132
19.133 - |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
19.134 + |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
19.135 if ((is_arith_rel fm) andalso (x = y) andalso (c1 = zero) andalso (c2 = one))
19.136 then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
19.137 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
19.138
19.139 - |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
19.140 + |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
19.141 if ((y=x) andalso (c1 = zero)) then
19.142 if (pm1 = one)
19.143 then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf))
19.144 else (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
19.145 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
19.146
19.147 - |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
19.148 + |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
19.149 if y=x then let val cz = cterm_of sg (norm_zero_one z)
19.150 val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
19.151 in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf)))
19.152 end
19.153 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
19.154 - |(Const("Divides.op dvd",_)$ d $ (db as (Const ("op +",_) $ (Const ("op *",_) $
19.155 + |(Const("Divides.op dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
19.156 c $ y ) $ z))) =>
19.157 if y=x then let val cz = cterm_of sg (norm_zero_one z)
19.158 val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
19.159 @@ -472,22 +472,22 @@
19.160 let
19.161 val fm = norm_zero_one fm1
19.162 in case fm1 of
19.163 - (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
19.164 + (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
19.165 if (x=y) andalso (c1=zero) andalso (c2=one)
19.166 then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_pinf))
19.167 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
19.168
19.169 - |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
19.170 + |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
19.171 if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
19.172 then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_pinf))
19.173 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
19.174
19.175 - |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
19.176 + |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
19.177 if (y=x) andalso (c1 =zero) then
19.178 if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else
19.179 (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_pinf))
19.180 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
19.181 - |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
19.182 + |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
19.183 if y=x then let val cd = cterm_of sg (norm_zero_one d)
19.184 val cz = cterm_of sg (norm_zero_one z)
19.185 in(instantiate' [] [SOME cd, SOME cz] (not_dvd_eq_pinf))
19.186 @@ -495,7 +495,7 @@
19.187
19.188 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
19.189
19.190 - |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
19.191 + |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
19.192 if y=x then let val cd = cterm_of sg (norm_zero_one d)
19.193 val cz = cterm_of sg (norm_zero_one z)
19.194 in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_pinf))
19.195 @@ -567,31 +567,31 @@
19.196 val cat = cterm_of sg (norm_zero_one at)
19.197 in
19.198 case at of
19.199 - (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
19.200 + (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
19.201 if (x=y) andalso (c1=zero) andalso (c2=one)
19.202 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
19.203 - val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
19.204 + val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
19.205 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
19.206 in (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_bst_p_ne)))
19.207 end
19.208 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
19.209
19.210 - |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", T) $(Const ("op *",_) $ c2 $ y) $z)) =>
19.211 + |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
19.212 if (is_arith_rel at) andalso (x=y)
19.213 then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_numeral 1)))
19.214 in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
19.215 - val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("op -",T) $ (Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
19.216 + val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("HOL.minus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
19.217 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
19.218 in (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_bst_p_eq)))
19.219 end
19.220 end
19.221 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
19.222
19.223 - |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
19.224 + |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
19.225 if (y=x) andalso (c1 =zero) then
19.226 if pm1 = one then
19.227 let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
19.228 - val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
19.229 + val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
19.230 in (instantiate' [] [SOME cfma, SOME cdlcm]([th1,th2] MRS (not_bst_p_gt)))
19.231 end
19.232 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
19.233 @@ -599,7 +599,7 @@
19.234 end
19.235 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
19.236
19.237 - |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
19.238 + |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
19.239 if y=x then
19.240 let val cz = cterm_of sg (norm_zero_one z)
19.241 val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
19.242 @@ -607,7 +607,7 @@
19.243 end
19.244 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
19.245
19.246 - |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
19.247 + |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
19.248 if y=x then
19.249 let val cz = cterm_of sg (norm_zero_one z)
19.250 val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
19.251 @@ -658,26 +658,26 @@
19.252 val cat = cterm_of sg (norm_zero_one at)
19.253 in
19.254 case at of
19.255 - (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
19.256 + (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
19.257 if (x=y) andalso (c1=zero) andalso (c2=one)
19.258 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ A)
19.259 - val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
19.260 + val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
19.261 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
19.262 in (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_ast_p_ne)))
19.263 end
19.264 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
19.265
19.266 - |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", T) $(Const ("op *",_) $ c2 $ y) $z)) =>
19.267 + |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
19.268 if (is_arith_rel at) andalso (x=y)
19.269 then let val ast_z = norm_zero_one (linear_sub [] one z )
19.270 val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ ast_z $ A)
19.271 - val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("op +",T) $ (Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
19.272 + val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("HOL.plus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
19.273 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
19.274 in (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_ast_p_eq)))
19.275 end
19.276 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
19.277
19.278 - |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
19.279 + |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
19.280 if (y=x) andalso (c1 =zero) then
19.281 if pm1 = (mk_numeral ~1) then
19.282 let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A)
19.283 @@ -689,7 +689,7 @@
19.284 end
19.285 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
19.286
19.287 - |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
19.288 + |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
19.289 if y=x then
19.290 let val cz = cterm_of sg (norm_zero_one z)
19.291 val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
19.292 @@ -697,7 +697,7 @@
19.293 end
19.294 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
19.295
19.296 - |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
19.297 + |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
19.298 if y=x then
19.299 let val cz = cterm_of sg (norm_zero_one z)
19.300 val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
20.1 --- a/src/HOL/Integ/int_arith1.ML Fri Mar 10 12:28:38 2006 +0100
20.2 +++ b/src/HOL/Integ/int_arith1.ML Fri Mar 10 15:33:48 2006 +0100
20.3 @@ -197,11 +197,11 @@
20.4 handle TERM _ => find_first_numeral (t::past) terms)
20.5 | find_first_numeral past [] = raise TERM("find_first_numeral", []);
20.6
20.7 -val mk_plus = HOLogic.mk_binop "op +";
20.8 +val mk_plus = HOLogic.mk_binop "HOL.plus";
20.9
20.10 fun mk_minus t =
20.11 let val T = Term.fastype_of t
20.12 - in Const ("uminus", T --> T) $ t
20.13 + in Const ("HOL.uminus", T --> T) $ t
20.14 end;
20.15
20.16 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
20.17 @@ -213,22 +213,22 @@
20.18 fun long_mk_sum T [] = mk_numeral T 0
20.19 | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
20.20
20.21 -val dest_plus = HOLogic.dest_bin "op +" Term.dummyT;
20.22 +val dest_plus = HOLogic.dest_bin "HOL.plus" Term.dummyT;
20.23
20.24 (*decompose additions AND subtractions as a sum*)
20.25 -fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) =
20.26 +fun dest_summing (pos, Const ("HOL.plus", _) $ t $ u, ts) =
20.27 dest_summing (pos, t, dest_summing (pos, u, ts))
20.28 - | dest_summing (pos, Const ("op -", _) $ t $ u, ts) =
20.29 + | dest_summing (pos, Const ("HOL.minus", _) $ t $ u, ts) =
20.30 dest_summing (pos, t, dest_summing (not pos, u, ts))
20.31 | dest_summing (pos, t, ts) =
20.32 if pos then t::ts else mk_minus t :: ts;
20.33
20.34 fun dest_sum t = dest_summing (true, t, []);
20.35
20.36 -val mk_diff = HOLogic.mk_binop "op -";
20.37 -val dest_diff = HOLogic.dest_bin "op -" Term.dummyT;
20.38 +val mk_diff = HOLogic.mk_binop "HOL.minus";
20.39 +val dest_diff = HOLogic.dest_bin "HOL.minus" Term.dummyT;
20.40
20.41 -val mk_times = HOLogic.mk_binop "op *";
20.42 +val mk_times = HOLogic.mk_binop "HOL.times";
20.43
20.44 fun mk_prod T =
20.45 let val one = mk_numeral T 1
20.46 @@ -241,7 +241,7 @@
20.47 fun long_mk_prod T [] = mk_numeral T 1
20.48 | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
20.49
20.50 -val dest_times = HOLogic.dest_bin "op *" Term.dummyT;
20.51 +val dest_times = HOLogic.dest_bin "HOL.times" Term.dummyT;
20.52
20.53 fun dest_prod t =
20.54 let val (t,u) = dest_times t
20.55 @@ -252,7 +252,7 @@
20.56 fun mk_coeff (k, t) = mk_times (mk_numeral (Term.fastype_of t) k, t);
20.57
20.58 (*Express t as a product of (possibly) a numeral with other sorted terms*)
20.59 -fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t
20.60 +fun dest_coeff sign (Const ("HOL.uminus", _) $ t) = dest_coeff (~sign) t
20.61 | dest_coeff sign t =
20.62 let val ts = sort Term.term_ord (dest_prod t)
20.63 val (n, ts') = find_first_numeral [] ts
21.1 --- a/src/HOL/Integ/nat_simprocs.ML Fri Mar 10 12:28:38 2006 +0100
21.2 +++ b/src/HOL/Integ/nat_simprocs.ML Fri Mar 10 15:33:48 2006 +0100
21.3 @@ -39,7 +39,7 @@
21.4 | find_first_numeral past [] = raise TERM("find_first_numeral", []);
21.5
21.6 val zero = mk_numeral 0;
21.7 -val mk_plus = HOLogic.mk_binop "op +";
21.8 +val mk_plus = HOLogic.mk_binop "HOL.plus";
21.9
21.10 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
21.11 fun mk_sum [] = zero
21.12 @@ -50,7 +50,7 @@
21.13 fun long_mk_sum [] = HOLogic.zero
21.14 | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
21.15
21.16 -val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
21.17 +val dest_plus = HOLogic.dest_bin "HOL.plus" HOLogic.natT;
21.18
21.19 (*extract the outer Sucs from a term and convert them to a binary numeral*)
21.20 fun dest_Sucs (k, Const ("Suc", _) $ t) = dest_Sucs (k+1, t)
21.21 @@ -85,14 +85,14 @@
21.22 (*** CancelNumerals simprocs ***)
21.23
21.24 val one = mk_numeral 1;
21.25 -val mk_times = HOLogic.mk_binop "op *";
21.26 +val mk_times = HOLogic.mk_binop "HOL.times";
21.27
21.28 fun mk_prod [] = one
21.29 | mk_prod [t] = t
21.30 | mk_prod (t :: ts) = if t = one then mk_prod ts
21.31 else mk_times (t, mk_prod ts);
21.32
21.33 -val dest_times = HOLogic.dest_bin "op *" HOLogic.natT;
21.34 +val dest_times = HOLogic.dest_bin "HOL.times" HOLogic.natT;
21.35
21.36 fun dest_prod t =
21.37 let val (t,u) = dest_times t
21.38 @@ -213,8 +213,8 @@
21.39 structure DiffCancelNumerals = CancelNumeralsFun
21.40 (open CancelNumeralsCommon
21.41 val prove_conv = Bin_Simprocs.prove_conv
21.42 - val mk_bal = HOLogic.mk_binop "op -"
21.43 - val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT
21.44 + val mk_bal = HOLogic.mk_binop "HOL.minus"
21.45 + val dest_bal = HOLogic.dest_bin "HOL.minus" HOLogic.natT
21.46 val bal_add1 = nat_diff_add_eq1 RS trans
21.47 val bal_add2 = nat_diff_add_eq2 RS trans
21.48 );
22.1 --- a/src/HOL/Integ/presburger.ML Fri Mar 10 12:28:38 2006 +0100
22.2 +++ b/src/HOL/Integ/presburger.ML Fri Mar 10 15:33:48 2006 +0100
22.3 @@ -139,11 +139,11 @@
22.4 ("Divides.op dvd", iT --> iT --> bT),
22.5 ("Divides.op div", iT --> iT --> iT),
22.6 ("Divides.op mod", iT --> iT --> iT),
22.7 - ("op +", iT --> iT --> iT),
22.8 - ("op -", iT --> iT --> iT),
22.9 - ("op *", iT --> iT --> iT),
22.10 + ("HOL.plus", iT --> iT --> iT),
22.11 + ("HOL.minus", iT --> iT --> iT),
22.12 + ("HOL.times", iT --> iT --> iT),
22.13 ("HOL.abs", iT --> iT),
22.14 - ("uminus", iT --> iT),
22.15 + ("HOL.uminus", iT --> iT),
22.16 ("HOL.max", iT --> iT --> iT),
22.17 ("HOL.min", iT --> iT --> iT),
22.18
22.19 @@ -153,9 +153,9 @@
22.20 ("Divides.op dvd", nT --> nT --> bT),
22.21 ("Divides.op div", nT --> nT --> nT),
22.22 ("Divides.op mod", nT --> nT --> nT),
22.23 - ("op +", nT --> nT --> nT),
22.24 - ("op -", nT --> nT --> nT),
22.25 - ("op *", nT --> nT --> nT),
22.26 + ("HOL.plus", nT --> nT --> nT),
22.27 + ("HOL.minus", nT --> nT --> nT),
22.28 + ("HOL.times", nT --> nT --> nT),
22.29 ("Suc", nT --> nT),
22.30 ("HOL.max", nT --> nT --> nT),
22.31 ("HOL.min", nT --> nT --> nT),
23.1 --- a/src/HOL/Integ/reflected_cooper.ML Fri Mar 10 12:28:38 2006 +0100
23.2 +++ b/src/HOL/Integ/reflected_cooper.ML Fri Mar 10 15:33:48 2006 +0100
23.3 @@ -16,10 +16,10 @@
23.4 | Const("0",iT) => Cst 0
23.5 | Const("1",iT) => Cst 1
23.6 | Bound i => Var (nat (IntInf.fromInt i))
23.7 - | Const("uminus",_)$t' => Neg (i_of_term vs t')
23.8 - | Const ("op +",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
23.9 - | Const ("op -",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
23.10 - | Const ("op *",_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
23.11 + | Const("HOL.uminus",_)$t' => Neg (i_of_term vs t')
23.12 + | Const ("HOL.plus",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
23.13 + | Const ("HOL.minus",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
23.14 + | Const ("HOL.times",_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
23.15 | Const ("Numeral.number_of",_)$t' => Cst (HOLogic.dest_binum t')
23.16 | _ => error "i_of_term: unknown term";
23.17
23.18 @@ -77,12 +77,12 @@
23.19 case t of
23.20 Cst i => CooperDec.mk_numeral i
23.21 | Var n => valOf (myassoc2 vs n)
23.22 - | Neg t' => Const("uminus",iT --> iT)$(term_of_i vs t')
23.23 - | Add(t1,t2) => Const("op +",[iT,iT] ---> iT)$
23.24 + | Neg t' => Const("HOL.uminus",iT --> iT)$(term_of_i vs t')
23.25 + | Add(t1,t2) => Const("HOL.plus",[iT,iT] ---> iT)$
23.26 (term_of_i vs t1)$(term_of_i vs t2)
23.27 - | Sub(t1,t2) => Const("op -",[iT,iT] ---> iT)$
23.28 + | Sub(t1,t2) => Const("HOL.minus",[iT,iT] ---> iT)$
23.29 (term_of_i vs t1)$(term_of_i vs t2)
23.30 - | Mult(t1,t2) => Const("op *",[iT,iT] ---> iT)$
23.31 + | Mult(t1,t2) => Const("HOL.times",[iT,iT] ---> iT)$
23.32 (term_of_i vs t1)$(term_of_i vs t2);
23.33
23.34 fun term_of_qf vs t =
24.1 --- a/src/HOL/Library/ExecutableRat.thy Fri Mar 10 12:28:38 2006 +0100
24.2 +++ b/src/HOL/Library/ExecutableRat.thy Fri Mar 10 15:33:48 2006 +0100
24.3 @@ -15,13 +15,13 @@
24.4
24.5 datatype erat = Rat bool int int
24.6
24.7 -instance erat :: zero by intro_classes
24.8 -instance erat :: one by intro_classes
24.9 -instance erat :: plus by intro_classes
24.10 -instance erat :: minus by intro_classes
24.11 -instance erat :: times by intro_classes
24.12 -instance erat :: inverse by intro_classes
24.13 -instance erat :: ord by intro_classes
24.14 +instance erat :: zero ..
24.15 +instance erat :: one ..
24.16 +instance erat :: plus ..
24.17 +instance erat :: minus ..
24.18 +instance erat :: times ..
24.19 +instance erat :: inverse ..
24.20 +instance erat :: ord ..
24.21
24.22 consts
24.23 norm :: "erat \<Rightarrow> erat"
24.24 @@ -85,12 +85,6 @@
24.25 ml (target_atom "{*erat*}")
24.26 haskell (target_atom "{*erat*}")
24.27
24.28 -code_alias
24.29 - (* an intermediate solution until name resolving of ad-hoc overloaded
24.30 - constants is refined *)
24.31 - "HOL.inverse" "Rational.inverse"
24.32 - "HOL.divide" "Rational.divide"
24.33 -
24.34 code_syntax_const
24.35 Fract
24.36 ml ("{*of_quotient*}")
24.37 @@ -103,7 +97,7 @@
24.38 haskell ("{*1::erat*}")
24.39 "op + :: rat \<Rightarrow> rat \<Rightarrow> rat"
24.40 ml ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
24.41 - haskell ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
24.42 + haskell ("{*HOL.plus :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
24.43 "uminus :: rat \<Rightarrow> rat"
24.44 ml ("{*uminus :: erat \<Rightarrow> erat*}")
24.45 haskell ("{*uminus :: erat \<Rightarrow> erat*}")
25.1 --- a/src/HOL/Library/ExecutableSet.thy Fri Mar 10 12:28:38 2006 +0100
25.2 +++ b/src/HOL/Library/ExecutableSet.thy Fri Mar 10 15:33:48 2006 +0100
25.3 @@ -40,7 +40,7 @@
25.4 "insert" ("(_ ins _)")
25.5 "op Un" ("(_ union _)")
25.6 "op Int" ("(_ inter _)")
25.7 - "op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("(_ \\\\ _)")
25.8 + "HOL.minus" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("(_ \\\\ _)")
25.9 "image" ("\<module>image")
25.10 attach {*
25.11 fun image f S = distinct (map f S);
26.1 --- a/src/HOL/Library/comm_ring.ML Fri Mar 10 12:28:38 2006 +0100
26.2 +++ b/src/HOL/Library/comm_ring.ML Fri Mar 10 15:33:48 2006 +0100
26.3 @@ -77,13 +77,13 @@
26.4 (* reification of polynom expressions *)
26.5 fun reif_polex T vs t =
26.6 case t of
26.7 - Const("op +",_)$a$b => (polex_add T)
26.8 + Const("HOL.plus",_)$a$b => (polex_add T)
26.9 $ (reif_polex T vs a)$(reif_polex T vs b)
26.10 - | Const("op -",_)$a$b => (polex_sub T)
26.11 + | Const("HOL.minus",_)$a$b => (polex_sub T)
26.12 $ (reif_polex T vs a)$(reif_polex T vs b)
26.13 - | Const("op *",_)$a$b => (polex_mul T)
26.14 + | Const("HOL.times",_)$a$b => (polex_mul T)
26.15 $ (reif_polex T vs a)$ (reif_polex T vs b)
26.16 - | Const("uminus",_)$a => (polex_neg T)
26.17 + | Const("HOL.uminus",_)$a => (polex_neg T)
26.18 $ (reif_polex T vs a)
26.19 | (Const("Nat.power",_)$a$n) => (polex_pow T) $ (reif_polex T vs a) $ n
26.20
27.1 --- a/src/HOL/OrderedGroup.ML Fri Mar 10 12:28:38 2006 +0100
27.2 +++ b/src/HOL/OrderedGroup.ML Fri Mar 10 15:33:48 2006 +0100
27.3 @@ -8,7 +8,7 @@
27.4
27.5 (*** Term order for abelian groups ***)
27.6
27.7 -fun agrp_ord a = find_index_eq a ["0", "op +", "uminus", "op -"];
27.8 +fun agrp_ord a = find_index (fn a' => a = a') ["0", "HOL.plus", "HOL.uminus", "HOL.minus"];
27.9
27.10 fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
27.11
27.12 @@ -16,9 +16,9 @@
27.13 val ac1 = mk_meta_eq (thm "add_assoc");
27.14 val ac2 = mk_meta_eq (thm "add_commute");
27.15 val ac3 = mk_meta_eq (thm "add_left_commute");
27.16 - fun solve_add_ac thy _ (_ $ (Const ("op +",_) $ _ $ _) $ _) =
27.17 + fun solve_add_ac thy _ (_ $ (Const ("HOL.plus",_) $ _ $ _) $ _) =
27.18 SOME ac1
27.19 - | solve_add_ac thy _ (_ $ x $ (Const ("op +",_) $ y $ z)) =
27.20 + | solve_add_ac thy _ (_ $ x $ (Const ("HOL.plus",_) $ y $ z)) =
27.21 if termless_agrp (y, x) then SOME ac3 else NONE
27.22 | solve_add_ac thy _ (_ $ x $ y) =
27.23 if termless_agrp (y, x) then SOME ac2 else NONE
28.1 --- a/src/HOL/OrderedGroup.thy Fri Mar 10 12:28:38 2006 +0100
28.2 +++ b/src/HOL/OrderedGroup.thy Fri Mar 10 15:33:48 2006 +0100
28.3 @@ -899,8 +899,7 @@
28.4 lemma abs_triangle_ineq: "abs(a+b) \<le> abs a + abs(b::'a::lordered_ab_group_abs)"
28.5 proof -
28.6 have g:"abs a + abs b = join (a+b) (join (-a-b) (join (-a+b) (a + (-b))))" (is "_=join ?m ?n")
28.7 - apply (simp add: abs_lattice add_meet_join_distribs join_aci)
28.8 - by (simp only: diff_minus)
28.9 + by (simp add: abs_lattice add_meet_join_distribs join_aci diff_minus)
28.10 have a:"a+b <= join ?m ?n" by (simp add: meet_join_le)
28.11 have b:"-a-b <= ?n" by (simp add: meet_join_le)
28.12 have c:"?n <= join ?m ?n" by (simp add: meet_join_le)
29.1 --- a/src/HOL/Real/Float.ML Fri Mar 10 12:28:38 2006 +0100
29.2 +++ b/src/HOL/Real/Float.ML Fri Mar 10 15:33:48 2006 +0100
29.3 @@ -330,10 +330,10 @@
29.4
29.5 val float_const = Const ("Float.float", HOLogic.mk_prodT (HOLogic.intT, HOLogic.intT) --> HOLogic.realT)
29.6
29.7 -val float_add_const = Const ("op +", HOLogic.realT --> HOLogic.realT --> HOLogic.realT)
29.8 -val float_diff_const = Const ("op -", HOLogic.realT --> HOLogic.realT --> HOLogic.realT)
29.9 -val float_mult_const = Const ("op *", HOLogic.realT --> HOLogic.realT --> HOLogic.realT)
29.10 -val float_uminus_const = Const ("uminus", HOLogic.realT --> HOLogic.realT)
29.11 +val float_add_const = Const ("HOL.plus", HOLogic.realT --> HOLogic.realT --> HOLogic.realT)
29.12 +val float_diff_const = Const ("HOL.minus", HOLogic.realT --> HOLogic.realT --> HOLogic.realT)
29.13 +val float_mult_const = Const ("HOL.times", HOLogic.realT --> HOLogic.realT --> HOLogic.realT)
29.14 +val float_uminus_const = Const ("HOL.uminus", HOLogic.realT --> HOLogic.realT)
29.15 val float_abs_const = Const ("HOL.abs", HOLogic.realT --> HOLogic.realT)
29.16 val float_le_const = Const ("op <=", HOLogic.realT --> HOLogic.realT --> HOLogic.boolT)
29.17 val float_pprt_const = Const ("OrderedGroup.pprt", HOLogic.realT --> HOLogic.realT)
30.1 --- a/src/HOL/Set.thy Fri Mar 10 12:28:38 2006 +0100
30.2 +++ b/src/HOL/Set.thy Fri Mar 10 15:33:48 2006 +0100
30.3 @@ -958,7 +958,7 @@
30.4 outer-level constant, which in this case is just "op :"; we instead need
30.5 to use term-nets to associate patterns with rules. Also, if a rule fails to
30.6 apply, then the formula should be kept.
30.7 - [("uminus", Compl_iff RS iffD1), ("op -", [Diff_iff RS iffD1]),
30.8 + [("HOL.uminus", Compl_iff RS iffD1), ("HOL.minus", [Diff_iff RS iffD1]),
30.9 ("op Int", [IntD1,IntD2]),
30.10 ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
30.11 *)
31.1 --- a/src/HOL/Tools/Presburger/cooper_dec.ML Fri Mar 10 12:28:38 2006 +0100
31.2 +++ b/src/HOL/Tools/Presburger/cooper_dec.ML Fri Mar 10 15:33:48 2006 +0100
31.3 @@ -116,8 +116,8 @@
31.4
31.5 fun linear_cmul n tm = if n = 0 then zero else let fun times n k = n*k in
31.6 ( case tm of
31.7 - (Const("op +",T) $ (Const ("op *",T1 ) $c1 $ x1) $ rest) =>
31.8 - Const("op +",T) $ ((Const("op *",T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest)
31.9 + (Const("HOL.plus",T) $ (Const ("HOL.times",T1 ) $c1 $ x1) $ rest) =>
31.10 + Const("HOL.plus",T) $ ((Const("HOL.times",T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest)
31.11 |_ => numeral1 (times n) tm)
31.12 end ;
31.13
31.14 @@ -139,23 +139,23 @@
31.15 fun linear_add vars tm1 tm2 =
31.16 let fun addwith x y = x + y in
31.17 (case (tm1,tm2) of
31.18 - ((Const ("op +",T1) $ ( Const("op *",T2) $ c1 $ x1) $ rest1),(Const
31.19 - ("op +",T3)$( Const("op *",T4) $ c2 $ x2) $ rest2)) =>
31.20 + ((Const ("HOL.plus",T1) $ ( Const("HOL.times",T2) $ c1 $ x1) $ rest1),(Const
31.21 + ("HOL.plus",T3)$( Const("HOL.times",T4) $ c2 $ x2) $ rest2)) =>
31.22 if x1 = x2 then
31.23 let val c = (numeral2 (addwith) c1 c2)
31.24 in
31.25 if c = zero then (linear_add vars rest1 rest2)
31.26 - else (Const("op +",T1) $ (Const("op *",T2) $ c $ x1) $ (linear_add vars rest1 rest2))
31.27 + else (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c $ x1) $ (linear_add vars rest1 rest2))
31.28 end
31.29 else
31.30 - if earlierv vars x1 x2 then (Const("op +",T1) $
31.31 - (Const("op *",T2)$ c1 $ x1) $ (linear_add vars rest1 tm2))
31.32 - else (Const("op +",T1) $ (Const("op *",T2) $ c2 $ x2) $ (linear_add vars tm1 rest2))
31.33 - |((Const("op +",T1) $ (Const("op *",T2) $ c1 $ x1) $ rest1) ,_) =>
31.34 - (Const("op +",T1)$ (Const("op *",T2) $ c1 $ x1) $ (linear_add vars
31.35 + if earlierv vars x1 x2 then (Const("HOL.plus",T1) $
31.36 + (Const("HOL.times",T2)$ c1 $ x1) $ (linear_add vars rest1 tm2))
31.37 + else (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c2 $ x2) $ (linear_add vars tm1 rest2))
31.38 + |((Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c1 $ x1) $ rest1) ,_) =>
31.39 + (Const("HOL.plus",T1)$ (Const("HOL.times",T2) $ c1 $ x1) $ (linear_add vars
31.40 rest1 tm2))
31.41 - |(_, (Const("op +",T1) $(Const("op *",T2) $ c2 $ x2) $ rest2)) =>
31.42 - (Const("op +",T1) $ (Const("op *",T2) $ c2 $ x2) $ (linear_add vars tm1
31.43 + |(_, (Const("HOL.plus",T1) $(Const("HOL.times",T2) $ c2 $ x2) $ rest2)) =>
31.44 + (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c2 $ x2) $ (linear_add vars tm1
31.45 rest2))
31.46 | (_,_) => numeral2 (addwith) tm1 tm2)
31.47
31.48 @@ -180,13 +180,13 @@
31.49 Free(x,T)*)
31.50
31.51 fun lint vars tm = if is_numeral tm then tm else case tm of
31.52 - (Free (x,T)) => (HOLogic.mk_binop "op +" ((HOLogic.mk_binop "op *" ((mk_numeral 1),Free (x,T))), zero))
31.53 - |(Bound i) => (Const("op +",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $
31.54 - (Const("op *",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_numeral 1) $ (Bound i)) $ zero)
31.55 - |(Const("uminus",_) $ t ) => (linear_neg (lint vars t))
31.56 - |(Const("op +",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t))
31.57 - |(Const("op -",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t))
31.58 - |(Const ("op *",_) $ s $ t) =>
31.59 + (Free (x,T)) => (HOLogic.mk_binop "HOL.plus" ((HOLogic.mk_binop "HOL.times" ((mk_numeral 1),Free (x,T))), zero))
31.60 + |(Bound i) => (Const("HOL.plus",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $
31.61 + (Const("HOL.times",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_numeral 1) $ (Bound i)) $ zero)
31.62 + |(Const("HOL.uminus",_) $ t ) => (linear_neg (lint vars t))
31.63 + |(Const("HOL.plus",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t))
31.64 + |(Const("HOL.minus",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t))
31.65 + |(Const ("HOL.times",_) $ s $ t) =>
31.66 let val s' = lint vars s
31.67 val t' = lint vars t
31.68 in
31.69 @@ -212,14 +212,14 @@
31.70 end
31.71 else (warning "Nonlinear term --- Non numeral leftside at dvd"
31.72 ;raise COOPER)
31.73 - |linform vars (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) )
31.74 - |linform vars (Const("op <",_)$ s $t ) = (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
31.75 - |linform vars (Const("op >",_) $ s $ t ) = (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t))
31.76 + |linform vars (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) )
31.77 + |linform vars (Const("op <",_)$ s $t ) = (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
31.78 + |linform vars (Const("op >",_) $ s $ t ) = (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t))
31.79 |linform vars (Const("op <=",_)$ s $ t ) =
31.80 - (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("op +",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s))
31.81 + (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s))
31.82 |linform vars (Const("op >=",_)$ s $ t ) =
31.83 - (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT -->
31.84 - HOLogic.intT) $ (Const("op +",HOLogic.intT --> HOLogic.intT -->
31.85 + (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT -->
31.86 + HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT -->
31.87 HOLogic.intT) $s $(mk_numeral 1)) $ t))
31.88
31.89 |linform vars fm = fm;
31.90 @@ -246,7 +246,7 @@
31.91 fun lcm_num a b = (abs a*b) div (gcd (abs a) (abs b));
31.92
31.93 fun formlcm x fm = case fm of
31.94 - (Const (p,_)$ _ $(Const ("op +", _)$(Const ("op *",_)$ c $ y ) $z ) ) => if
31.95 + (Const (p,_)$ _ $(Const ("HOL.plus", _)$(Const ("HOL.times",_)$ c $ y ) $z ) ) => if
31.96 (is_arith_rel fm) andalso (x = y) then (abs(dest_numeral c)) else 1
31.97 | ( Const ("Not", _) $p) => formlcm x p
31.98 | ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q)
31.99 @@ -259,13 +259,13 @@
31.100
31.101 fun adjustcoeff x l fm =
31.102 case fm of
31.103 - (Const(p,_) $d $( Const ("op +", _)$(Const ("op *",_) $
31.104 + (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $
31.105 c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then
31.106 let val m = l div (dest_numeral c)
31.107 val n = (if p = "op <" then abs(m) else m)
31.108 - val xtm = HOLogic.mk_binop "op *" ((mk_numeral (m div n)), x)
31.109 + val xtm = HOLogic.mk_binop "HOL.times" ((mk_numeral (m div n)), x)
31.110 in
31.111 - (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) ))))
31.112 + (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
31.113 end
31.114 else fm
31.115 |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeff x l p)
31.116 @@ -282,8 +282,8 @@
31.117 val fm' = adjustcoeff x l fm in
31.118 if l = 1 then fm'
31.119 else
31.120 - let val xp = (HOLogic.mk_binop "op +"
31.121 - ((HOLogic.mk_binop "op *" ((mk_numeral 1), x )), zero))
31.122 + let val xp = (HOLogic.mk_binop "HOL.plus"
31.123 + ((HOLogic.mk_binop "HOL.times" ((mk_numeral 1), x )), zero))
31.124 in
31.125 HOLogic.conj $(HOLogic.mk_binrel "Divides.op dvd" ((mk_numeral l) , xp )) $ (adjustcoeff x l fm)
31.126 end
31.127 @@ -294,12 +294,12 @@
31.128 (*
31.129 fun adjustcoeffeq x l fm =
31.130 case fm of
31.131 - (Const(p,_) $d $( Const ("op +", _)$(Const ("op *",_) $
31.132 + (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $
31.133 c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then
31.134 let val m = l div (dest_numeral c)
31.135 val n = (if p = "op <" then abs(m) else m)
31.136 - val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x))
31.137 - in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) ))))
31.138 + val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x))
31.139 + in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
31.140 end
31.141 else fm
31.142 |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeffeq x l p)
31.143 @@ -315,11 +315,11 @@
31.144 (* ------------------------------------------------------------------------- *)
31.145
31.146 fun minusinf x fm = case fm of
31.147 - (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
31.148 + (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
31.149 if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const
31.150 else fm
31.151
31.152 - |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z
31.153 + |(Const("op <",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
31.154 )) => if (x = y)
31.155 then if (pm1 = one) andalso (c = zero) then HOLogic.false_const
31.156 else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.true_const
31.157 @@ -336,11 +336,11 @@
31.158 (* ------------------------------------------------------------------------- *)
31.159
31.160 fun plusinf x fm = case fm of
31.161 - (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
31.162 + (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
31.163 if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const
31.164 else fm
31.165
31.166 - |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z
31.167 + |(Const("op <",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
31.168 )) => if (x = y)
31.169 then if (pm1 = one) andalso (c = zero) then HOLogic.true_const
31.170 else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.false_const
31.171 @@ -356,7 +356,7 @@
31.172 (* The LCM of all the divisors that involve x. *)
31.173 (* ------------------------------------------------------------------------- *)
31.174
31.175 -fun divlcm x (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z ) ) =
31.176 +fun divlcm x (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) =
31.177 if x = y then abs(dest_numeral d) else 1
31.178 |divlcm x ( Const ("Not", _) $ p) = divlcm x p
31.179 |divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q)
31.180 @@ -370,15 +370,15 @@
31.181 fun bset x fm = case fm of
31.182 (Const ("Not", _) $ p) => if (is_arith_rel p) then
31.183 (case p of
31.184 - (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $c2 $y) $a ) )
31.185 + (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $c2 $y) $a ) )
31.186 => if (is_arith_rel p) andalso (x= y) andalso (c2 = one) andalso (c1 = zero)
31.187 then [linear_neg a]
31.188 else bset x p
31.189 |_ =>[])
31.190
31.191 else bset x p
31.192 - |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +",_) $ (Const ("op *",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_numeral 1))] else []
31.193 - |(Const ("op <",_) $ c1$ (Const ("op +",_) $(Const ("op *",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else []
31.194 + |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_numeral 1))] else []
31.195 + |(Const ("op <",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else []
31.196 |(Const ("op &",_) $ p $ q) => (bset x p) union (bset x q)
31.197 |(Const ("op |",_) $ p $ q) => (bset x p) union (bset x q)
31.198 |_ => [];
31.199 @@ -390,15 +390,15 @@
31.200 fun aset x fm = case fm of
31.201 (Const ("Not", _) $ p) => if (is_arith_rel p) then
31.202 (case p of
31.203 - (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $c2 $y) $a ) )
31.204 + (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $c2 $y) $a ) )
31.205 => if (x= y) andalso (c2 = one) andalso (c1 = zero)
31.206 then [linear_neg a]
31.207 else []
31.208 |_ =>[])
31.209
31.210 else aset x p
31.211 - |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +",_) $ (Const ("op *",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_numeral 1) a] else []
31.212 - |(Const ("op <",_) $ c1$ (Const ("op +",_) $(Const ("op *",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_numeral (~1))) then [a] else []
31.213 + |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_numeral 1) a] else []
31.214 + |(Const ("op <",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_numeral (~1))) then [a] else []
31.215 |(Const ("op &",_) $ p $ q) => (aset x p) union (aset x q)
31.216 |(Const ("op |",_) $ p $ q) => (aset x p) union (aset x q)
31.217 |_ => [];
31.218 @@ -409,7 +409,7 @@
31.219 (* ------------------------------------------------------------------------- *)
31.220
31.221 fun linrep vars x t fm = case fm of
31.222 - ((Const(p,_)$ d $ (Const("op +",_)$(Const("op *",_)$ c $ y) $ z))) =>
31.223 + ((Const(p,_)$ d $ (Const("HOL.plus",_)$(Const("HOL.times",_)$ c $ y) $ z))) =>
31.224 if (x = y) andalso (is_arith_rel fm)
31.225 then
31.226 let val ct = linear_cmul (dest_numeral c) t
31.227 @@ -435,8 +435,8 @@
31.228 val dn = dest_numeral d
31.229 fun coeffs_of x = case x of
31.230 Const(p,_) $ tl $ tr =>
31.231 - if p = "op +" then (coeffs_of tl) union (coeffs_of tr)
31.232 - else if p = "op *"
31.233 + if p = "HOL.plus" then (coeffs_of tl) union (coeffs_of tr)
31.234 + else if p = "HOL.times"
31.235 then if (is_numeral tr)
31.236 then [(dest_numeral tr) * (dest_numeral tl)]
31.237 else [dest_numeral tl]
32.1 --- a/src/HOL/Tools/Presburger/cooper_proof.ML Fri Mar 10 12:28:38 2006 +0100
32.2 +++ b/src/HOL/Tools/Presburger/cooper_proof.ML Fri Mar 10 15:33:48 2006 +0100
32.3 @@ -165,11 +165,11 @@
32.4 (* ------------------------------------------------------------------------- *)
32.5
32.6 fun norm_zero_one fm = case fm of
32.7 - (Const ("op *",_) $ c $ t) =>
32.8 + (Const ("HOL.times",_) $ c $ t) =>
32.9 if c = one then (norm_zero_one t)
32.10 else if (dest_numeral c = ~1)
32.11 - then (Const("uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
32.12 - else (HOLogic.mk_binop "op *" (norm_zero_one c,norm_zero_one t))
32.13 + then (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
32.14 + else (HOLogic.mk_binop "HOL.times" (norm_zero_one c,norm_zero_one t))
32.15 |(node $ rest) => ((norm_zero_one node)$(norm_zero_one rest))
32.16 |(Abs(x,T,p)) => (Abs(x,T,(norm_zero_one p)))
32.17 |_ => fm;
32.18 @@ -255,13 +255,13 @@
32.19 (*==================================================*)
32.20
32.21 fun decomp_adjustcoeffeq sg x l fm = case fm of
32.22 - (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("op +", _)$(Const ("op *",_) $ c $ y ) $z )))) =>
32.23 + (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $ c $ y ) $z )))) =>
32.24 let
32.25 val m = l div (dest_numeral c)
32.26 val n = if (x = y) then abs (m) else 1
32.27 - val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x))
32.28 + val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x))
32.29 val rs = if (x = y)
32.30 - then (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) ))))
32.31 + then (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
32.32 else HOLogic.mk_binrel "op <" (zero,linear_sub [] one rt )
32.33 val ck = cterm_of sg (mk_numeral n)
32.34 val cc = cterm_of sg c
32.35 @@ -273,14 +273,14 @@
32.36 in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
32.37 end
32.38
32.39 - |(Const(p,_) $a $( Const ("op +", _)$(Const ("op *",_) $
32.40 + |(Const(p,_) $a $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $
32.41 c $ y ) $t )) =>
32.42 if (is_arith_rel fm) andalso (x = y)
32.43 then
32.44 let val m = l div (dest_numeral c)
32.45 val k = (if p = "op <" then abs(m) else m)
32.46 - val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div k)*l) ), x))
32.47 - val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul k t) ))))
32.48 + val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div k)*l) ), x))
32.49 + val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul k t) ))))
32.50
32.51 val ck = cterm_of sg (mk_numeral k)
32.52 val cc = cterm_of sg c
32.53 @@ -335,28 +335,28 @@
32.54 val cfalse = cterm_of sg HOLogic.false_const
32.55 val fm = norm_zero_one fm1
32.56 in case fm1 of
32.57 - (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
32.58 + (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
32.59 if (x=y) andalso (c1= zero) andalso (c2= one) then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
32.60 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
32.61
32.62 - |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
32.63 + |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
32.64 if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one)
32.65 then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf))
32.66 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
32.67
32.68 - |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
32.69 + |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
32.70 if (y=x) andalso (c1 = zero) then
32.71 if (pm1 = one) then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf)) else
32.72 (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
32.73 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
32.74
32.75 - |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
32.76 + |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
32.77 if y=x then let val cz = cterm_of sg (norm_zero_one z)
32.78 val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
32.79 in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf)))
32.80 end
32.81 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
32.82 - |(Const("Divides.op dvd",_)$ d $ (db as (Const ("op +",_) $ (Const ("op *",_) $
32.83 + |(Const("Divides.op dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
32.84 c $ y ) $ z))) =>
32.85 if y=x then let val cz = cterm_of sg (norm_zero_one z)
32.86 val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
32.87 @@ -373,22 +373,22 @@
32.88 let
32.89 val fm = norm_zero_one fm1
32.90 in case fm1 of
32.91 - (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
32.92 + (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
32.93 if (x=y) andalso (c1=zero) andalso (c2=one)
32.94 then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_minf))
32.95 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
32.96
32.97 - |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
32.98 + |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
32.99 if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
32.100 then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_minf))
32.101 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
32.102
32.103 - |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
32.104 + |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
32.105 if (y=x) andalso (c1 =zero) then
32.106 if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else
32.107 (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_minf))
32.108 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
32.109 - |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
32.110 + |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
32.111 if y=x then let val cd = cterm_of sg (norm_zero_one d)
32.112 val cz = cterm_of sg (norm_zero_one z)
32.113 in(instantiate' [] [SOME cd, SOME cz] (not_dvd_eq_minf))
32.114 @@ -396,7 +396,7 @@
32.115
32.116 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
32.117
32.118 - |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
32.119 + |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
32.120 if y=x then let val cd = cterm_of sg (norm_zero_one d)
32.121 val cz = cterm_of sg (norm_zero_one z)
32.122 in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_minf))
32.123 @@ -431,30 +431,30 @@
32.124 val cfalse = cterm_of sg HOLogic.false_const
32.125 val fm = norm_zero_one fm1
32.126 in case fm1 of
32.127 - (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
32.128 + (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
32.129 if ((x=y) andalso (c1= zero) andalso (c2= one))
32.130 then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf))
32.131 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
32.132
32.133 - |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
32.134 + |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
32.135 if ((is_arith_rel fm) andalso (x = y) andalso (c1 = zero) andalso (c2 = one))
32.136 then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
32.137 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
32.138
32.139 - |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
32.140 + |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
32.141 if ((y=x) andalso (c1 = zero)) then
32.142 if (pm1 = one)
32.143 then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf))
32.144 else (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
32.145 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
32.146
32.147 - |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
32.148 + |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
32.149 if y=x then let val cz = cterm_of sg (norm_zero_one z)
32.150 val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
32.151 in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf)))
32.152 end
32.153 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
32.154 - |(Const("Divides.op dvd",_)$ d $ (db as (Const ("op +",_) $ (Const ("op *",_) $
32.155 + |(Const("Divides.op dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
32.156 c $ y ) $ z))) =>
32.157 if y=x then let val cz = cterm_of sg (norm_zero_one z)
32.158 val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
32.159 @@ -472,22 +472,22 @@
32.160 let
32.161 val fm = norm_zero_one fm1
32.162 in case fm1 of
32.163 - (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
32.164 + (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
32.165 if (x=y) andalso (c1=zero) andalso (c2=one)
32.166 then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_pinf))
32.167 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
32.168
32.169 - |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
32.170 + |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
32.171 if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
32.172 then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_pinf))
32.173 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
32.174
32.175 - |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
32.176 + |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
32.177 if (y=x) andalso (c1 =zero) then
32.178 if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else
32.179 (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_pinf))
32.180 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
32.181 - |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
32.182 + |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
32.183 if y=x then let val cd = cterm_of sg (norm_zero_one d)
32.184 val cz = cterm_of sg (norm_zero_one z)
32.185 in(instantiate' [] [SOME cd, SOME cz] (not_dvd_eq_pinf))
32.186 @@ -495,7 +495,7 @@
32.187
32.188 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
32.189
32.190 - |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
32.191 + |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
32.192 if y=x then let val cd = cterm_of sg (norm_zero_one d)
32.193 val cz = cterm_of sg (norm_zero_one z)
32.194 in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_pinf))
32.195 @@ -567,31 +567,31 @@
32.196 val cat = cterm_of sg (norm_zero_one at)
32.197 in
32.198 case at of
32.199 - (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
32.200 + (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
32.201 if (x=y) andalso (c1=zero) andalso (c2=one)
32.202 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
32.203 - val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
32.204 + val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
32.205 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
32.206 in (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_bst_p_ne)))
32.207 end
32.208 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
32.209
32.210 - |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", T) $(Const ("op *",_) $ c2 $ y) $z)) =>
32.211 + |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
32.212 if (is_arith_rel at) andalso (x=y)
32.213 then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_numeral 1)))
32.214 in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
32.215 - val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("op -",T) $ (Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
32.216 + val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("HOL.minus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
32.217 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
32.218 in (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_bst_p_eq)))
32.219 end
32.220 end
32.221 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
32.222
32.223 - |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
32.224 + |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
32.225 if (y=x) andalso (c1 =zero) then
32.226 if pm1 = one then
32.227 let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
32.228 - val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
32.229 + val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
32.230 in (instantiate' [] [SOME cfma, SOME cdlcm]([th1,th2] MRS (not_bst_p_gt)))
32.231 end
32.232 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
32.233 @@ -599,7 +599,7 @@
32.234 end
32.235 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
32.236
32.237 - |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
32.238 + |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
32.239 if y=x then
32.240 let val cz = cterm_of sg (norm_zero_one z)
32.241 val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
32.242 @@ -607,7 +607,7 @@
32.243 end
32.244 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
32.245
32.246 - |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
32.247 + |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
32.248 if y=x then
32.249 let val cz = cterm_of sg (norm_zero_one z)
32.250 val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
32.251 @@ -658,26 +658,26 @@
32.252 val cat = cterm_of sg (norm_zero_one at)
32.253 in
32.254 case at of
32.255 - (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
32.256 + (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) =>
32.257 if (x=y) andalso (c1=zero) andalso (c2=one)
32.258 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ A)
32.259 - val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
32.260 + val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
32.261 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
32.262 in (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_ast_p_ne)))
32.263 end
32.264 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
32.265
32.266 - |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", T) $(Const ("op *",_) $ c2 $ y) $z)) =>
32.267 + |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
32.268 if (is_arith_rel at) andalso (x=y)
32.269 then let val ast_z = norm_zero_one (linear_sub [] one z )
32.270 val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ ast_z $ A)
32.271 - val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("op +",T) $ (Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
32.272 + val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("HOL.plus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
32.273 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
32.274 in (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_ast_p_eq)))
32.275 end
32.276 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
32.277
32.278 - |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
32.279 + |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
32.280 if (y=x) andalso (c1 =zero) then
32.281 if pm1 = (mk_numeral ~1) then
32.282 let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A)
32.283 @@ -689,7 +689,7 @@
32.284 end
32.285 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
32.286
32.287 - |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
32.288 + |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
32.289 if y=x then
32.290 let val cz = cterm_of sg (norm_zero_one z)
32.291 val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
32.292 @@ -697,7 +697,7 @@
32.293 end
32.294 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
32.295
32.296 - |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
32.297 + |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
32.298 if y=x then
32.299 let val cz = cterm_of sg (norm_zero_one z)
32.300 val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
33.1 --- a/src/HOL/Tools/Presburger/presburger.ML Fri Mar 10 12:28:38 2006 +0100
33.2 +++ b/src/HOL/Tools/Presburger/presburger.ML Fri Mar 10 15:33:48 2006 +0100
33.3 @@ -139,11 +139,11 @@
33.4 ("Divides.op dvd", iT --> iT --> bT),
33.5 ("Divides.op div", iT --> iT --> iT),
33.6 ("Divides.op mod", iT --> iT --> iT),
33.7 - ("op +", iT --> iT --> iT),
33.8 - ("op -", iT --> iT --> iT),
33.9 - ("op *", iT --> iT --> iT),
33.10 + ("HOL.plus", iT --> iT --> iT),
33.11 + ("HOL.minus", iT --> iT --> iT),
33.12 + ("HOL.times", iT --> iT --> iT),
33.13 ("HOL.abs", iT --> iT),
33.14 - ("uminus", iT --> iT),
33.15 + ("HOL.uminus", iT --> iT),
33.16 ("HOL.max", iT --> iT --> iT),
33.17 ("HOL.min", iT --> iT --> iT),
33.18
33.19 @@ -153,9 +153,9 @@
33.20 ("Divides.op dvd", nT --> nT --> bT),
33.21 ("Divides.op div", nT --> nT --> nT),
33.22 ("Divides.op mod", nT --> nT --> nT),
33.23 - ("op +", nT --> nT --> nT),
33.24 - ("op -", nT --> nT --> nT),
33.25 - ("op *", nT --> nT --> nT),
33.26 + ("HOL.plus", nT --> nT --> nT),
33.27 + ("HOL.minus", nT --> nT --> nT),
33.28 + ("HOL.times", nT --> nT --> nT),
33.29 ("Suc", nT --> nT),
33.30 ("HOL.max", nT --> nT --> nT),
33.31 ("HOL.min", nT --> nT --> nT),
34.1 --- a/src/HOL/Tools/Presburger/reflected_cooper.ML Fri Mar 10 12:28:38 2006 +0100
34.2 +++ b/src/HOL/Tools/Presburger/reflected_cooper.ML Fri Mar 10 15:33:48 2006 +0100
34.3 @@ -16,10 +16,10 @@
34.4 | Const("0",iT) => Cst 0
34.5 | Const("1",iT) => Cst 1
34.6 | Bound i => Var (nat (IntInf.fromInt i))
34.7 - | Const("uminus",_)$t' => Neg (i_of_term vs t')
34.8 - | Const ("op +",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
34.9 - | Const ("op -",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
34.10 - | Const ("op *",_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
34.11 + | Const("HOL.uminus",_)$t' => Neg (i_of_term vs t')
34.12 + | Const ("HOL.plus",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
34.13 + | Const ("HOL.minus",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
34.14 + | Const ("HOL.times",_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
34.15 | Const ("Numeral.number_of",_)$t' => Cst (HOLogic.dest_binum t')
34.16 | _ => error "i_of_term: unknown term";
34.17
34.18 @@ -77,12 +77,12 @@
34.19 case t of
34.20 Cst i => CooperDec.mk_numeral i
34.21 | Var n => valOf (myassoc2 vs n)
34.22 - | Neg t' => Const("uminus",iT --> iT)$(term_of_i vs t')
34.23 - | Add(t1,t2) => Const("op +",[iT,iT] ---> iT)$
34.24 + | Neg t' => Const("HOL.uminus",iT --> iT)$(term_of_i vs t')
34.25 + | Add(t1,t2) => Const("HOL.plus",[iT,iT] ---> iT)$
34.26 (term_of_i vs t1)$(term_of_i vs t2)
34.27 - | Sub(t1,t2) => Const("op -",[iT,iT] ---> iT)$
34.28 + | Sub(t1,t2) => Const("HOL.minus",[iT,iT] ---> iT)$
34.29 (term_of_i vs t1)$(term_of_i vs t2)
34.30 - | Mult(t1,t2) => Const("op *",[iT,iT] ---> iT)$
34.31 + | Mult(t1,t2) => Const("HOL.times",[iT,iT] ---> iT)$
34.32 (term_of_i vs t1)$(term_of_i vs t2);
34.33
34.34 fun term_of_qf vs t =
35.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML Fri Mar 10 12:28:38 2006 +0100
35.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Fri Mar 10 15:33:48 2006 +0100
35.3 @@ -404,7 +404,7 @@
35.4 val def_names = map (fn s => s ^ "_def") (DatatypeProp.indexify_names
35.5 (map (fn T => name_of_typ T ^ "_size") recTs));
35.6
35.7 - fun plus (t1, t2) = Const ("op +", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
35.8 + fun plus (t1, t2) = Const ("HOL.plus", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
35.9
35.10 fun make_sizefun (_, cargs) =
35.11 let
36.1 --- a/src/HOL/Tools/datatype_prop.ML Fri Mar 10 12:28:38 2006 +0100
36.2 +++ b/src/HOL/Tools/datatype_prop.ML Fri Mar 10 15:33:48 2006 +0100
36.3 @@ -366,7 +366,7 @@
36.4 val size_consts = map (fn (s, T) =>
36.5 Const (s, T --> HOLogic.natT)) (size_names ~~ recTs);
36.6
36.7 - fun plus (t1, t2) = Const ("op +", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
36.8 + fun plus (t1, t2) = Const ("HOL.plus", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
36.9
36.10 fun make_size_eqn size_const T (cname, cargs) =
36.11 let
37.1 --- a/src/HOL/Tools/refute.ML Fri Mar 10 12:28:38 2006 +0100
37.2 +++ b/src/HOL/Tools/refute.ML Fri Mar 10 15:33:48 2006 +0100
37.3 @@ -622,9 +622,9 @@
37.4 | Const ("Finite_Set.card", T) => collect_type_axioms (axs, T)
37.5 | Const ("Finite_Set.Finites", T) => collect_type_axioms (axs, T)
37.6 | Const ("op <", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => collect_type_axioms (axs, T)
37.7 - | Const ("op +", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
37.8 - | Const ("op -", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
37.9 - | Const ("op *", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
37.10 + | Const ("HOL.plus", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
37.11 + | Const ("HOL.minus", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
37.12 + | Const ("HOL.times", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
37.13 | Const ("List.op @", T) => collect_type_axioms (axs, T)
37.14 | Const ("Lfp.lfp", T) => collect_type_axioms (axs, T)
37.15 | Const ("Gfp.gfp", T) => collect_type_axioms (axs, T)
37.16 @@ -2162,13 +2162,13 @@
37.17
37.18 (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
37.19
37.20 - (* only an optimization: 'op +' could in principle be interpreted with *)
37.21 + (* only an optimization: 'HOL.plus' could in principle be interpreted with*)
37.22 (* interpreters available already (using its definition), but the code *)
37.23 (* below is more efficient *)
37.24
37.25 fun Nat_plus_interpreter thy model args t =
37.26 case t of
37.27 - Const ("op +", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
37.28 + Const ("HOL.plus", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
37.29 let
37.30 val (i_nat, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
37.31 val size_nat = size_of_type i_nat
37.32 @@ -2196,7 +2196,7 @@
37.33
37.34 fun Nat_minus_interpreter thy model args t =
37.35 case t of
37.36 - Const ("op -", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
37.37 + Const ("HOL.minus", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
37.38 let
37.39 val (i_nat, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
37.40 val size_nat = size_of_type i_nat
37.41 @@ -2215,13 +2215,13 @@
37.42
37.43 (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
37.44
37.45 - (* only an optimization: 'op *' could in principle be interpreted with *)
37.46 - (* interpreters available already (using its definition), but the code *)
37.47 - (* below is more efficient *)
37.48 + (* only an optimization: 'HOL.times' could in principle be interpreted with *)
37.49 + (* interpreters available already (using its definition), but the code *)
37.50 + (* below is more efficient *)
37.51
37.52 fun Nat_mult_interpreter thy model args t =
37.53 case t of
37.54 - Const ("op *", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
37.55 + Const ("HOL.times", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
37.56 let
37.57 val (i_nat, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
37.58 val size_nat = size_of_type i_nat
38.1 --- a/src/HOL/Tools/res_clause.ML Fri Mar 10 12:28:38 2006 +0100
38.2 +++ b/src/HOL/Tools/res_clause.ML Fri Mar 10 15:33:48 2006 +0100
38.3 @@ -94,9 +94,9 @@
38.4 ("op <", "less"),
38.5 ("op &", "and"),
38.6 ("op |", "or"),
38.7 - ("op +", "plus"),
38.8 - ("op -", "minus"),
38.9 - ("op *", "times"),
38.10 + ("HOL.plus", "plus"),
38.11 + ("HOL.minus", "minus"),
38.12 + ("HOL.times", "times"),
38.13 ("Divides.op div", "div"),
38.14 ("HOL.divide", "divide"),
38.15 ("op -->", "implies"),
39.1 --- a/src/HOL/arith_data.ML Fri Mar 10 12:28:38 2006 +0100
39.2 +++ b/src/HOL/arith_data.ML Fri Mar 10 15:33:48 2006 +0100
39.3 @@ -17,7 +17,7 @@
39.4 (* mk_sum, mk_norm_sum *)
39.5
39.6 val one = HOLogic.mk_nat 1;
39.7 -val mk_plus = HOLogic.mk_binop "op +";
39.8 +val mk_plus = HOLogic.mk_binop "HOL.plus";
39.9
39.10 fun mk_sum [] = HOLogic.zero
39.11 | mk_sum [t] = t
39.12 @@ -32,7 +32,7 @@
39.13
39.14 (* dest_sum *)
39.15
39.16 -val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
39.17 +val dest_plus = HOLogic.dest_bin "HOL.plus" HOLogic.natT;
39.18
39.19 fun dest_sum tm =
39.20 if HOLogic.is_zero tm then []
39.21 @@ -137,8 +137,8 @@
39.22 structure DiffCancelSums = CancelSumsFun
39.23 (struct
39.24 open Sum;
39.25 - val mk_bal = HOLogic.mk_binop "op -";
39.26 - val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT;
39.27 + val mk_bal = HOLogic.mk_binop "HOL.minus";
39.28 + val dest_bal = HOLogic.dest_bin "HOL.minus" HOLogic.natT;
39.29 val uncancel_tac = gen_uncancel_tac diff_cancel;
39.30 end);
39.31
39.32 @@ -267,14 +267,14 @@
39.33
39.34 fun demult inj_consts =
39.35 let
39.36 -fun demult((mC as Const("op *",_)) $ s $ t,m) = ((case s of
39.37 +fun demult((mC as Const("HOL.times",_)) $ s $ t,m) = ((case s of
39.38 Const("Numeral.number_of",_)$n
39.39 => demult(t,Rat.mult(m,Rat.rat_of_intinf(HOLogic.dest_binum n)))
39.40 - | Const("uminus",_)$(Const("Numeral.number_of",_)$n)
39.41 + | Const("HOL.uminus",_)$(Const("Numeral.number_of",_)$n)
39.42 => demult(t,Rat.mult(m,Rat.rat_of_intinf(~(HOLogic.dest_binum n))))
39.43 | Const("Suc",_) $ _
39.44 => demult(t,Rat.mult(m,Rat.rat_of_int(number_of_Sucs s)))
39.45 - | Const("op *",_) $ s1 $ s2 => demult(mC $ s1 $ (mC $ s2 $ t),m)
39.46 + | Const("HOL.times",_) $ s1 $ s2 => demult(mC $ s1 $ (mC $ s2 $ t),m)
39.47 | Const("HOL.divide",_) $ numt $ (Const("Numeral.number_of",_)$dent) =>
39.48 let val den = HOLogic.dest_binum dent
39.49 in if den = 0 then raise Zero
39.50 @@ -291,7 +291,7 @@
39.51 | demult(t as Const("Numeral.number_of",_)$n,m) =
39.52 ((NONE,Rat.mult(m,Rat.rat_of_intinf(HOLogic.dest_binum n)))
39.53 handle TERM _ => (SOME t,m))
39.54 - | demult(Const("uminus",_)$t, m) = demult(t,Rat.mult(m,Rat.rat_of_int(~1)))
39.55 + | demult(Const("HOL.uminus",_)$t, m) = demult(t,Rat.mult(m,Rat.rat_of_int(~1)))
39.56 | demult(t as Const f $ x, m) =
39.57 (if f mem inj_consts then SOME x else SOME t,m)
39.58 | demult(atom,m) = (SOME atom,m)
39.59 @@ -303,15 +303,15 @@
39.60 fun decomp2 inj_consts (rel,lhs,rhs) =
39.61 let
39.62 (* Turn term into list of summand * multiplicity plus a constant *)
39.63 -fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi))
39.64 - | poly(all as Const("op -",T) $ s $ t, m, pi) =
39.65 +fun poly(Const("HOL.plus",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi))
39.66 + | poly(all as Const("HOL.minus",T) $ s $ t, m, pi) =
39.67 if nT T then add_atom(all,m,pi) else poly(s,m,poly(t,Rat.neg m,pi))
39.68 - | poly(all as Const("uminus",T) $ t, m, pi) =
39.69 + | poly(all as Const("HOL.uminus",T) $ t, m, pi) =
39.70 if nT T then add_atom(all,m,pi) else poly(t,Rat.neg m,pi)
39.71 | poly(Const("0",_), _, pi) = pi
39.72 | poly(Const("1",_), m, (p,i)) = (p,Rat.add(i,m))
39.73 | poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,Rat.add(i,m)))
39.74 - | poly(t as Const("op *",_) $ _ $ _, m, pi as (p,i)) =
39.75 + | poly(t as Const("HOL.times",_) $ _ $ _, m, pi as (p,i)) =
39.76 (case demult inj_consts (t,m) of
39.77 (NONE,m') => (p,Rat.add(i,m))
39.78 | (SOME u,m') => add_atom(u,m',pi))
40.1 --- a/src/HOL/ex/SVC_Oracle.ML Fri Mar 10 12:28:38 2006 +0100
40.2 +++ b/src/HOL/ex/SVC_Oracle.ML Fri Mar 10 15:33:48 2006 +0100
40.3 @@ -46,21 +46,21 @@
40.4 | lit (t as Const("Numeral.number_of", _) $ w) = t
40.5 | lit t = replace t
40.6 (*abstraction of a real/rational expression*)
40.7 - fun rat ((c as Const("op +", _)) $ x $ y) = c $ (rat x) $ (rat y)
40.8 - | rat ((c as Const("op -", _)) $ x $ y) = c $ (rat x) $ (rat y)
40.9 - | rat ((c as Const("op /", _)) $ x $ y) = c $ (rat x) $ (rat y)
40.10 - | rat ((c as Const("op *", _)) $ x $ y) = c $ (rat x) $ (rat y)
40.11 - | rat ((c as Const("uminus", _)) $ x) = c $ (rat x)
40.12 + fun rat ((c as Const("HOL.plus", _)) $ x $ y) = c $ (rat x) $ (rat y)
40.13 + | rat ((c as Const("HOL.minus", _)) $ x $ y) = c $ (rat x) $ (rat y)
40.14 + | rat ((c as Const("HOL.divide", _)) $ x $ y) = c $ (rat x) $ (rat y)
40.15 + | rat ((c as Const("HOL.times", _)) $ x $ y) = c $ (rat x) $ (rat y)
40.16 + | rat ((c as Const("HOL.uminus", _)) $ x) = c $ (rat x)
40.17 | rat t = lit t
40.18 (*abstraction of an integer expression: no div, mod*)
40.19 - fun int ((c as Const("op +", _)) $ x $ y) = c $ (int x) $ (int y)
40.20 - | int ((c as Const("op -", _)) $ x $ y) = c $ (int x) $ (int y)
40.21 - | int ((c as Const("op *", _)) $ x $ y) = c $ (int x) $ (int y)
40.22 - | int ((c as Const("uminus", _)) $ x) = c $ (int x)
40.23 + fun int ((c as Const("HOL.plus", _)) $ x $ y) = c $ (int x) $ (int y)
40.24 + | int ((c as Const("HOL.minus", _)) $ x $ y) = c $ (int x) $ (int y)
40.25 + | int ((c as Const("HOL.times", _)) $ x $ y) = c $ (int x) $ (int y)
40.26 + | int ((c as Const("HOL.uminus", _)) $ x) = c $ (int x)
40.27 | int t = lit t
40.28 (*abstraction of a natural number expression: no minus*)
40.29 - fun nat ((c as Const("op +", _)) $ x $ y) = c $ (nat x) $ (nat y)
40.30 - | nat ((c as Const("op *", _)) $ x $ y) = c $ (nat x) $ (nat y)
40.31 + fun nat ((c as Const("HOL.plus", _)) $ x $ y) = c $ (nat x) $ (nat y)
40.32 + | nat ((c as Const("HOL.times", _)) $ x $ y) = c $ (nat x) $ (nat y)
40.33 | nat ((c as Const("Suc", _)) $ x) = c $ (nat x)
40.34 | nat t = lit t
40.35 (*abstraction of a relation: =, <, <=*)
41.1 --- a/src/HOL/ex/mesontest2.ML Fri Mar 10 12:28:38 2006 +0100
41.2 +++ b/src/HOL/ex/mesontest2.ML Fri Mar 10 15:33:48 2006 +0100
41.3 @@ -547,9 +547,9 @@
41.4 \ (has(p4::'a,goto(out))) & \
41.5 \ (follows(p5::'a,p4)) & \
41.6 \ (follows(p6::'a,p3)) & \
41.7 -\ (has(p6::'a,assign(register_k::'a,times(num2::'a,register_k)))) & \
41.8 +\ (has(p6::'a,assign(register_k::'a,mtimes(num2::'a,register_k)))) & \
41.9 \ (follows(p7::'a,p6)) & \
41.10 -\ (has(p7::'a,assign(register_j::'a,plus(register_j::'a,num1)))) & \
41.11 +\ (has(p7::'a,assign(register_j::'a,mplus(register_j::'a,num1)))) & \
41.12 \ (follows(p8::'a,p7)) & \
41.13 \ (has(p8::'a,goto(loop))) & \
41.14 \ (~succeeds(p3::'a,p3)) --> False",
41.15 @@ -570,9 +570,9 @@
41.16 \ (has(p4::'a,goto(out))) & \
41.17 \ (follows(p5::'a,p4)) & \
41.18 \ (follows(p6::'a,p3)) & \
41.19 -\ (has(p6::'a,assign(register_k::'a,times(num2::'a,register_k)))) & \
41.20 +\ (has(p6::'a,assign(register_k::'a,mtimes(num2::'a,register_k)))) & \
41.21 \ (follows(p7::'a,p6)) & \
41.22 -\ (has(p7::'a,assign(register_j::'a,plus(register_j::'a,num1)))) & \
41.23 +\ (has(p7::'a,assign(register_j::'a,mplus(register_j::'a,num1)))) & \
41.24 \ (follows(p8::'a,p7)) & \
41.25 \ (has(p8::'a,goto(loop))) & \
41.26 \ (fails(p3::'a,p3)) --> False",
41.27 @@ -768,7 +768,6 @@
41.28 \ (\\<forall>X V1 V2 V3 V4 Y V5. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,V4,X,V5),continuous(V1::'a,V2,V3,V4,Y,V5))) & \
41.29 \ (\\<forall>X V1 V2 V3 V4 V5 Y. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,V4,V5,X),continuous(V1::'a,V2,V3,V4,V5,Y)))";
41.30
41.31 -
41.32 (*4272 inferences so far. Searching to depth 10. 29.4 secs*)
41.33 val GEO017_2 = prove_hard
41.34 (EQU001_0_ax ^ "&" ^ GEO002_ax_eq ^ " & \
41.35 @@ -1224,26 +1223,26 @@
41.36
41.37 (*73 inferences so far. Searching to depth 10. 0.2 secs*)
41.38 val MSC003_1 = prove
41.39 - ("(\\<forall>Number_of_small_parts Small_part Big_part Number_of_mid_parts Mid_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) --> in'(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Mid_part) | has_parts(Big_part::'a,times(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) & \
41.40 -\ (\\<forall>Big_part Mid_part Number_of_mid_parts Number_of_small_parts Small_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) & has_parts(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Number_of_small_parts,Small_part) --> has_parts(Big_part::'a,times(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) & \
41.41 + ("(\\<forall>Number_of_small_parts Small_part Big_part Number_of_mid_parts Mid_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) --> in'(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Mid_part) | has_parts(Big_part::'a,mtimes(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) & \
41.42 +\ (\\<forall>Big_part Mid_part Number_of_mid_parts Number_of_small_parts Small_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) & has_parts(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Number_of_small_parts,Small_part) --> has_parts(Big_part::'a,mtimes(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) & \
41.43 \ (in'(john::'a,boy)) & \
41.44 \ (\\<forall>X. in'(X::'a,boy) --> in'(X::'a,human)) & \
41.45 \ (\\<forall>X. in'(X::'a,hand) --> has_parts(X::'a,num5,fingers)) & \
41.46 \ (\\<forall>X. in'(X::'a,human) --> has_parts(X::'a,num2,arm)) & \
41.47 \ (\\<forall>X. in'(X::'a,arm) --> has_parts(X::'a,num1,hand)) & \
41.48 -\ (~has_parts(john::'a,times(num2::'a,num1),hand)) --> False",
41.49 +\ (~has_parts(john::'a,mtimes(num2::'a,num1),hand)) --> False",
41.50 meson_tac 1);
41.51
41.52 (*1486 inferences so far. Searching to depth 20. 1.2 secs*)
41.53 val MSC004_1 = prove
41.54 - ("(\\<forall>Number_of_small_parts Small_part Big_part Number_of_mid_parts Mid_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) --> in'(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Mid_part) | has_parts(Big_part::'a,times(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) & \
41.55 -\ (\\<forall>Big_part Mid_part Number_of_mid_parts Number_of_small_parts Small_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) & has_parts(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Number_of_small_parts,Small_part) --> has_parts(Big_part::'a,times(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) & \
41.56 + ("(\\<forall>Number_of_small_parts Small_part Big_part Number_of_mid_parts Mid_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) --> in'(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Mid_part) | has_parts(Big_part::'a,mtimes(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) & \
41.57 +\ (\\<forall>Big_part Mid_part Number_of_mid_parts Number_of_small_parts Small_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) & has_parts(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Number_of_small_parts,Small_part) --> has_parts(Big_part::'a,mtimes(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) & \
41.58 \ (in'(john::'a,boy)) & \
41.59 \ (\\<forall>X. in'(X::'a,boy) --> in'(X::'a,human)) & \
41.60 \ (\\<forall>X. in'(X::'a,hand) --> has_parts(X::'a,num5,fingers)) & \
41.61 \ (\\<forall>X. in'(X::'a,human) --> has_parts(X::'a,num2,arm)) & \
41.62 \ (\\<forall>X. in'(X::'a,arm) --> has_parts(X::'a,num1,hand)) & \
41.63 -\ (~has_parts(john::'a,times(times(num2::'a,num1),num5),fingers)) --> False",
41.64 +\ (~has_parts(john::'a,mtimes(mtimes(num2::'a,num1),num5),fingers)) --> False",
41.65 meson_tac 1);
41.66
41.67 (*100 inferences so far. Searching to depth 12. 0.1 secs*)
42.1 --- a/src/HOL/ex/svc_funcs.ML Fri Mar 10 12:28:38 2006 +0100
42.2 +++ b/src/HOL/ex/svc_funcs.ML Fri Mar 10 15:33:48 2006 +0100
42.3 @@ -154,16 +154,16 @@
42.4 | lit (Const("0", _)) = 0
42.5 | lit (Const("1", _)) = 1
42.6 (*translation of a literal expression [no variables]*)
42.7 - fun litExp (Const("op +", T) $ x $ y) =
42.8 + fun litExp (Const("HOL.plus", T) $ x $ y) =
42.9 if is_numeric_op T then (litExp x) + (litExp y)
42.10 else fail t
42.11 - | litExp (Const("op -", T) $ x $ y) =
42.12 + | litExp (Const("HOL.minus", T) $ x $ y) =
42.13 if is_numeric_op T then (litExp x) - (litExp y)
42.14 else fail t
42.15 - | litExp (Const("op *", T) $ x $ y) =
42.16 + | litExp (Const("HOL.times", T) $ x $ y) =
42.17 if is_numeric_op T then (litExp x) * (litExp y)
42.18 else fail t
42.19 - | litExp (Const("uminus", T) $ x) =
42.20 + | litExp (Const("HOL.uminus", T) $ x) =
42.21 if is_numeric_op T then ~(litExp x)
42.22 else fail t
42.23 | litExp t = lit t
42.24 @@ -171,21 +171,21 @@
42.25 (*translation of a real/rational expression*)
42.26 fun suc t = Interp("+", [Int 1, t])
42.27 fun tm (Const("Suc", T) $ x) = suc (tm x)
42.28 - | tm (Const("op +", T) $ x $ y) =
42.29 + | tm (Const("HOL.plus", T) $ x $ y) =
42.30 if is_numeric_op T then Interp("+", [tm x, tm y])
42.31 else fail t
42.32 - | tm (Const("op -", T) $ x $ y) =
42.33 + | tm (Const("HOL.minus", T) $ x $ y) =
42.34 if is_numeric_op T then
42.35 Interp("+", [tm x, Interp("*", [Int ~1, tm y])])
42.36 else fail t
42.37 - | tm (Const("op *", T) $ x $ y) =
42.38 + | tm (Const("HOL.times", T) $ x $ y) =
42.39 if is_numeric_op T then Interp("*", [tm x, tm y])
42.40 else fail t
42.41 | tm (Const("RealDef.rinv", T) $ x) =
42.42 if domain_type T = HOLogic.realT then
42.43 Rat(1, litExp x)
42.44 else fail t
42.45 - | tm (Const("uminus", T) $ x) =
42.46 + | tm (Const("HOL.uminus", T) $ x) =
42.47 if is_numeric_op T then Interp("*", [Int ~1, tm x])
42.48 else fail t
42.49 | tm t = Int (lit t)
43.1 --- a/src/Provers/Arith/abel_cancel.ML Fri Mar 10 12:28:38 2006 +0100
43.2 +++ b/src/Provers/Arith/abel_cancel.ML Fri Mar 10 15:33:48 2006 +0100
43.3 @@ -31,28 +31,28 @@
43.4 open Data;
43.5
43.6 fun zero t = Const ("0", t);
43.7 - fun minus t = Const ("uminus", t --> t);
43.8 + fun minus t = Const ("HOL.uminus", t --> t);
43.9
43.10 - fun add_terms pos (Const ("op +", _) $ x $ y, ts) =
43.11 + fun add_terms pos (Const ("HOL.plus", _) $ x $ y, ts) =
43.12 add_terms pos (x, add_terms pos (y, ts))
43.13 - | add_terms pos (Const ("op -", _) $ x $ y, ts) =
43.14 + | add_terms pos (Const ("HOL.minus", _) $ x $ y, ts) =
43.15 add_terms pos (x, add_terms (not pos) (y, ts))
43.16 - | add_terms pos (Const ("uminus", _) $ x, ts) =
43.17 + | add_terms pos (Const ("HOL.uminus", _) $ x, ts) =
43.18 add_terms (not pos) (x, ts)
43.19 | add_terms pos (x, ts) = (pos,x) :: ts;
43.20
43.21 fun terms fml = add_terms true (fml, []);
43.22
43.23 -fun zero1 pt (u as (c as Const("op +",_)) $ x $ y) =
43.24 +fun zero1 pt (u as (c as Const("HOL.plus",_)) $ x $ y) =
43.25 (case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE
43.26 | SOME z => SOME(c $ x $ z))
43.27 | SOME z => SOME(c $ z $ y))
43.28 - | zero1 (pos,t) (u as (c as Const("op -",_)) $ x $ y) =
43.29 + | zero1 (pos,t) (u as (c as Const("HOL.minus",_)) $ x $ y) =
43.30 (case zero1 (pos,t) x of
43.31 NONE => (case zero1 (not pos,t) y of NONE => NONE
43.32 | SOME z => SOME(c $ x $ z))
43.33 | SOME z => SOME(c $ z $ y))
43.34 - | zero1 (pos,t) (u as (c as Const("uminus",_)) $ x) =
43.35 + | zero1 (pos,t) (u as (c as Const("HOL.uminus",_)) $ x) =
43.36 (case zero1 (not pos,t) x of NONE => NONE
43.37 | SOME z => SOME(c $ z))
43.38 | zero1 (pos,t) u =
43.39 @@ -77,7 +77,7 @@
43.40 then tracing ("Abel cancel: " ^ string_of_cterm (cterm_of sg t))
43.41 else ()
43.42 val c $ lhs $ rhs = t
43.43 - val opp = case c of Const("op +",_) => true | _ => false;
43.44 + val opp = case c of Const("HOL.plus",_) => true | _ => false;
43.45 val (pos,l) = find_common opp (terms lhs) (terms rhs)
43.46 val posr = if opp then not pos else pos
43.47 val t' = c $ (the(zero1 (pos,l) lhs)) $ (the(zero1 (posr,l) rhs))
44.1 --- a/src/Provers/Arith/cancel_div_mod.ML Fri Mar 10 12:28:38 2006 +0100
44.2 +++ b/src/Provers/Arith/cancel_div_mod.ML Fri Mar 10 15:33:48 2006 +0100
44.3 @@ -6,8 +6,8 @@
44.4
44.5 A + n*(m div n) + B + (m mod n) + C == A + B + C + m
44.6
44.7 -Is parameterized but assumes for simplicity that + and * are called
44.8 -"op +" and "op *"
44.9 +FIXME: Is parameterized but assumes for simplicity that + and * are called
44.10 +"HOL.plus" and "HOL.minus"
44.11 *)
44.12
44.13 signature CANCEL_DIV_MOD_DATA =
44.14 @@ -35,12 +35,12 @@
44.15 functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
44.16 struct
44.17
44.18 -fun coll_div_mod (Const("op +",_) $ s $ t) dms =
44.19 +fun coll_div_mod (Const("HOL.plus",_) $ s $ t) dms =
44.20 coll_div_mod t (coll_div_mod s dms)
44.21 - | coll_div_mod (Const("op *",_) $ m $ (Const(d,_) $ s $ n))
44.22 + | coll_div_mod (Const("HOL.times",_) $ m $ (Const(d,_) $ s $ n))
44.23 (dms as (divs,mods)) =
44.24 if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
44.25 - | coll_div_mod (Const("op *",_) $ (Const(d,_) $ s $ n) $ m)
44.26 + | coll_div_mod (Const("HOL.times",_) $ (Const(d,_) $ s $ n) $ m)
44.27 (dms as (divs,mods)) =
44.28 if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
44.29 | coll_div_mod (Const(m,_) $ s $ n) (dms as (divs,mods)) =
44.30 @@ -56,8 +56,8 @@
44.31 ==> thesis by transitivity
44.32 *)
44.33
44.34 -val mk_plus = Data.mk_binop "op +"
44.35 -val mk_times = Data.mk_binop "op *"
44.36 +val mk_plus = Data.mk_binop "HOL.plus"
44.37 +val mk_times = Data.mk_binop "HOL.times"
44.38
44.39 fun rearrange t pq =
44.40 let val ts = Data.dest_sum t;
45.1 --- a/src/Pure/Tools/class_package.ML Fri Mar 10 12:28:38 2006 +0100
45.2 +++ b/src/Pure/Tools/class_package.ML Fri Mar 10 15:33:48 2006 +0100
45.3 @@ -623,18 +623,10 @@
45.4 val typ_def = Type.varifyT raw_typ_def;
45.5 val typ_use = Type.varifyT raw_typ_use;
45.6 val match_tab = Sign.typ_match thy (typ_def, typ_use) Vartab.empty;
45.7 - fun get_first_index f =
45.8 - let
45.9 - fun get _ [] = NONE
45.10 - | get i (x::xs) =
45.11 - case f x
45.12 - of NONE => get (i+1) xs
45.13 - | SOME y => SOME (i, y)
45.14 - in get 0 end;
45.15 fun tab_lookup vname = (the o Vartab.lookup match_tab) (vname, 0);
45.16 fun mk_class_deriv thy subclasses superclass =
45.17 let
45.18 - val (i, (subclass::deriv)) = (the oo get_first_index) (fn subclass =>
45.19 + val (i, (subclass::deriv)) = (the oo get_index) (fn subclass =>
45.20 get_superclass_derivation thy (subclass, superclass)
45.21 ) subclasses;
45.22 val i' = if length subclasses = 1 then ~1 else i;
46.1 --- a/src/Pure/library.ML Fri Mar 10 12:28:38 2006 +0100
46.2 +++ b/src/Pure/library.ML Fri Mar 10 15:33:48 2006 +0100
46.3 @@ -126,6 +126,7 @@
46.4 val find_index: ('a -> bool) -> 'a list -> int
46.5 val find_index_eq: ''a -> ''a list -> int
46.6 val find_first: ('a -> bool) -> 'a list -> 'a option
46.7 + val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
46.8 val get_first: ('a -> 'b option) -> 'a list -> 'b option
46.9 val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
46.10 val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
46.11 @@ -632,6 +633,15 @@
46.12 NONE => get_first f xs
46.13 | some => some);
46.14
46.15 +fun get_index f =
46.16 + let
46.17 + fun get _ [] = NONE
46.18 + | get i (x::xs) =
46.19 + case f x
46.20 + of NONE => get (i+1) xs
46.21 + | SOME y => SOME (i, y)
46.22 + in get 0 end;
46.23 +
46.24 (*flatten a list of lists to a list*)
46.25 val flat = List.concat;
46.26