turned translation for 1::nat into def.
introduced 1' and replaced most occurrences of 1 by 1'.
--- a/src/HOL/Datatype_Universe.ML Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/Datatype_Universe.ML Mon Aug 06 13:43:24 2001 +0200
@@ -80,7 +80,8 @@
(** Scons vs Atom **)
-Goalw [Atom_def,Scons_def,Push_Node_def] "Scons M N ~= Atom(a)";
+Goalw [Atom_def,Scons_def,Push_Node_def,One_def]
+ "Scons M N ~= Atom(a)";
by (rtac notI 1);
by (etac (equalityD2 RS subsetD RS UnE) 1);
by (rtac singletonI 1);
@@ -140,11 +141,11 @@
(** Injectiveness of Scons **)
-Goalw [Scons_def] "Scons M N <= Scons M' N' ==> M<=M'";
+Goalw [Scons_def,One_def] "Scons M N <= Scons M' N' ==> M<=M'";
by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
qed "Scons_inject_lemma1";
-Goalw [Scons_def] "Scons M N <= Scons M' N' ==> N<=N'";
+Goalw [Scons_def,One_def] "Scons M N <= Scons M' N' ==> N<=N'";
by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
qed "Scons_inject_lemma2";
@@ -251,7 +252,7 @@
by (rtac ntrunc_Atom 1);
qed "ntrunc_Numb";
-Goalw [Scons_def,ntrunc_def]
+Goalw [Scons_def,ntrunc_def,One_def]
"ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)";
by (safe_tac (claset() addSIs [imageI]));
by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3));
@@ -265,7 +266,7 @@
(** Injection nodes **)
-Goalw [In0_def] "ntrunc 1 (In0 M) = {}";
+Goalw [In0_def] "ntrunc 1' (In0 M) = {}";
by (Simp_tac 1);
by (rewtac Scons_def);
by (Blast_tac 1);
@@ -276,7 +277,7 @@
by (Simp_tac 1);
qed "ntrunc_In0";
-Goalw [In1_def] "ntrunc 1 (In1 M) = {}";
+Goalw [In1_def] "ntrunc 1' (In1 M) = {}";
by (Simp_tac 1);
by (rewtac Scons_def);
by (Blast_tac 1);
@@ -338,7 +339,7 @@
(** Injection **)
-Goalw [In0_def,In1_def] "In0(M) ~= In1(N)";
+Goalw [In0_def,In1_def,One_def] "In0(M) ~= In1(N)";
by (rtac notI 1);
by (etac (Scons_inject1 RS Numb_inject RS Zero_neq_Suc) 1);
qed "In0_not_In1";
--- a/src/HOL/Divides.ML Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/Divides.ML Mon Aug 06 13:43:24 2001 +0200
@@ -65,7 +65,7 @@
by (asm_simp_tac (simpset() addsimps [mod_geq]) 1);
qed "mod_if";
-Goal "m mod 1 = (0::nat)";
+Goal "m mod 1' = 0";
by (induct_tac "m" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_geq])));
qed "mod_1";
@@ -387,7 +387,7 @@
(*** Further facts about div and mod ***)
-Goal "m div 1 = m";
+Goal "m div 1' = m";
by (induct_tac "m" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_geq])));
qed "div_1";
@@ -527,12 +527,12 @@
qed "dvd_0_left_iff";
AddIffs [dvd_0_left_iff];
-Goalw [dvd_def] "1 dvd (k::nat)";
+Goalw [dvd_def] "1' dvd k";
by (Simp_tac 1);
qed "dvd_1_left";
AddIffs [dvd_1_left];
-Goal "(m dvd 1) = (m = 1)";
+Goal "(m dvd 1') = (m = 1')";
by (simp_tac (simpset() addsimps [dvd_def]) 1);
qed "dvd_1_iff_1";
Addsimps [dvd_1_iff_1];
--- a/src/HOL/Hoare/Examples.ML Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/Hoare/Examples.ML Mon Aug 06 13:43:24 2001 +0200
@@ -175,7 +175,7 @@
Ambiguity warnings of parser are due to := being used
both for assignment and list update.
*)
-Goal "m - 1 < n ==> m < Suc n";
+Goal "m - 1' < n ==> m < Suc n";
by (arith_tac 1);
qed "lemma";
@@ -184,7 +184,7 @@
\ geq == %A i. !k. i<k & k<length A --> pivot <= A!k |] ==> \
\ |- VARS A u l.\
\ {0 < length(A::('a::order)list)} \
-\ l := 0; u := length A - 1; \
+\ l := 0; u := length A - 1'; \
\ WHILE l <= u \
\ INV {leq A l & geq A u & u<length A & l<=length A} \
\ DO WHILE l < length A & A!l <= pivot \
--- a/src/HOL/IMPP/EvenOdd.ML Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/IMPP/EvenOdd.ML Mon Aug 06 13:43:24 2001 +0200
@@ -11,7 +11,7 @@
qed "even_0";
Addsimps [even_0];
-Goalw [even_def] "even 1 = False";
+Goalw [even_def] "even 1' = False";
by (Simp_tac 1);
qed "not_even_1";
Addsimps [not_even_1];
@@ -50,7 +50,7 @@
section "verification";
-Goalw [odd_def] "{{Z=Arg+0}. BODY Even .{Res_ok}}|-{Z=Arg+1}. odd .{Res_ok}";
+Goalw [odd_def] "{{Z=Arg+0}. BODY Even .{Res_ok}}|-{Z=Arg+1'}. odd .{Res_ok}";
by (rtac hoare_derivs.If 1);
by (rtac (hoare_derivs.Ass RS conseq1) 1);
by (clarsimp_tac Arg_Res_css 1);
--- a/src/HOL/Induct/Com.thy Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/Induct/Com.thy Mon Aug 06 13:43:24 2001 +0200
@@ -52,10 +52,10 @@
IfTrue "[| (e,s) -|[eval]-> (0,s'); (c0,s') -[eval]-> s1 |]
==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
- IfFalse "[| (e,s) -|[eval]-> (1,s'); (c1,s') -[eval]-> s1 |]
+ IfFalse "[| (e,s) -|[eval]-> (1',s'); (c1,s') -[eval]-> s1 |]
==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
- WhileFalse "(e,s) -|[eval]-> (1,s1) ==> (WHILE e DO c, s) -[eval]-> s1"
+ WhileFalse "(e,s) -|[eval]-> (1',s1) ==> (WHILE e DO c, s) -[eval]-> s1"
WhileTrue "[| (e,s) -|[eval]-> (0,s1);
(c,s1) -[eval]-> s2; (WHILE e DO c, s2) -[eval]-> s3 |]
--- a/src/HOL/Induct/Mutil.thy Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/Induct/Mutil.thy Mon Aug 06 13:43:24 2001 +0200
@@ -110,7 +110,7 @@
Diff_Int_distrib [simp]
lemma tiling_domino_0_1:
- "t \<in> tiling domino ==> card (coloured 0 \<inter> t) = card (coloured 1 \<inter> t)"
+ "t \<in> tiling domino ==> card (coloured 0 \<inter> t) = card (coloured 1' \<inter> t)"
apply (erule tiling.induct)
apply (drule_tac [2] domino_singletons)
apply auto
@@ -131,7 +131,7 @@
apply (rule notI)
apply (subgoal_tac
"card (coloured 0 \<inter> (t - {(i, j)} - {(m, n)})) <
- card (coloured 1 \<inter> (t - {(i, j)} - {(m, n)}))")
+ card (coloured 1' \<inter> (t - {(i, j)} - {(m, n)}))")
apply (force simp only: tiling_domino_0_1)
apply (simp add: tiling_domino_0_1 [symmetric])
apply (simp add: coloured_def card_Diff2_less)
--- a/src/HOL/Integ/IntDef.ML Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/Integ/IntDef.ML Mon Aug 06 13:43:24 2001 +0200
@@ -326,7 +326,7 @@
by (asm_simp_tac (simpset() addsimps [zmult]) 1);
qed "zmult_int0";
-Goalw [int_def] "int 1 * z = z";
+Goalw [int_def] "int 1' * z = z";
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
by (asm_simp_tac (simpset() addsimps [zmult]) 1);
qed "zmult_int1";
@@ -335,7 +335,7 @@
by (rtac ([zmult_commute, zmult_int0] MRS trans) 1);
qed "zmult_int0_right";
-Goal "z * int 1 = z";
+Goal "z * int 1' = z";
by (rtac ([zmult_commute, zmult_int1] MRS trans) 1);
qed "zmult_int1_right";
--- a/src/HOL/Integ/NatBin.thy Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/Integ/NatBin.thy Mon Aug 06 13:43:24 2001 +0200
@@ -18,6 +18,10 @@
"number_of v == nat (number_of v)"
(*::bin=>nat ::bin=>int*)
+axioms
+neg_number_of_bin_pred_iff_0:
+ "neg (number_of (bin_pred v)) = (number_of v = (0::nat))"
+
use "nat_bin.ML" setup nat_bin_arith_setup
end
--- a/src/HOL/Integ/NatSimprocs.ML Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/Integ/NatSimprocs.ML Mon Aug 06 13:43:24 2001 +0200
@@ -14,13 +14,15 @@
(*Now just instantiating n to (number_of v) does the right simplification,
but with some redundant inequality tests.*)
-
+(*
Goal "neg (number_of (bin_pred v)) = (number_of v = (0::nat))";
by (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < 1)" 1);
by (Asm_simp_tac 1);
by (stac less_number_of_Suc 1);
by (Simp_tac 1);
qed "neg_number_of_bin_pred_iff_0";
+*)
+val neg_number_of_bin_pred_iff_0 = thm "neg_number_of_bin_pred_iff_0";
Goal "neg (number_of (bin_minus v)) ==> \
\ Suc m - (number_of v) = m - (number_of (bin_pred v))";
--- a/src/HOL/Integ/nat_bin.ML Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/Integ/nat_bin.ML Mon Aug 06 13:43:24 2001 +0200
@@ -495,7 +495,7 @@
by Auto_tac;
val lemma1 = result();
-Goal "m+m ~= int 1 + n + n";
+Goal "m+m ~= int 1' + n + n";
by Auto_tac;
by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1);
by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1);
--- a/src/HOL/Isar_examples/Fibonacci.thy Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/Isar_examples/Fibonacci.thy Mon Aug 06 13:43:24 2001 +0200
@@ -29,7 +29,7 @@
consts fib :: "nat => nat"
recdef fib less_than
"fib 0 = 0"
- "fib 1 = 1"
+ "fib 1' = 1"
"fib (Suc (Suc x)) = fib x + fib (Suc x)"
lemma [simp]: "0 < fib (Suc n)"
--- a/src/HOL/Library/Multiset.thy Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Aug 06 13:43:24 2001 +0200
@@ -16,7 +16,7 @@
typedef 'a multiset = "{f::'a => nat. finite {x . 0 < f x}}"
proof
- show "(\\<lambda>x. 0::nat) \\<in> ?multiset" by simp
+ show "(\<lambda>x. 0::nat) \<in> ?multiset" by simp
qed
lemmas multiset_typedef [simp] =
@@ -25,23 +25,23 @@
constdefs
Mempty :: "'a multiset" ("{#}")
- "{#} == Abs_multiset (\\<lambda>a. 0)"
+ "{#} == Abs_multiset (\<lambda>a. 0)"
single :: "'a => 'a multiset" ("{#_#}")
- "{#a#} == Abs_multiset (\\<lambda>b. if b = a then 1 else 0)"
+ "{#a#} == Abs_multiset (\<lambda>b. if b = a then 1' else 0)"
count :: "'a multiset => 'a => nat"
"count == Rep_multiset"
MCollect :: "'a multiset => ('a => bool) => 'a multiset"
- "MCollect M P == Abs_multiset (\\<lambda>x. if P x then Rep_multiset M x else 0)"
+ "MCollect M P == Abs_multiset (\<lambda>x. if P x then Rep_multiset M x else 0)"
syntax
"_Melem" :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50)
"_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset" ("(1{# _ : _./ _#})")
translations
"a :# M" == "0 < count M a"
- "{#x:M. P#}" == "MCollect M (\\<lambda>x. P)"
+ "{#x:M. P#}" == "MCollect M (\<lambda>x. P)"
constdefs
set_of :: "'a multiset => 'a set"
@@ -52,8 +52,8 @@
instance multiset :: ("term") zero ..
defs (overloaded)
- union_def: "M + N == Abs_multiset (\\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
- diff_def: "M - N == Abs_multiset (\\<lambda>a. Rep_multiset M a - Rep_multiset N a)"
+ union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
+ diff_def: "M - N == Abs_multiset (\<lambda>a. Rep_multiset M a - Rep_multiset N a)"
Zero_def [simp]: "0 == {#}"
size_def: "size M == setsum (count M) (set_of M)"
@@ -62,16 +62,16 @@
\medskip Preservation of the representing set @{term multiset}.
*}
-lemma const0_in_multiset [simp]: "(\\<lambda>a. 0) \\<in> multiset"
+lemma const0_in_multiset [simp]: "(\<lambda>a. 0) \<in> multiset"
apply (simp add: multiset_def)
done
-lemma only1_in_multiset [simp]: "(\\<lambda>b. if b = a then 1 else 0) \\<in> multiset"
+lemma only1_in_multiset [simp]: "(\<lambda>b. if b = a then 1' else 0) \<in> multiset"
apply (simp add: multiset_def)
done
lemma union_preserves_multiset [simp]:
- "M \\<in> multiset ==> N \\<in> multiset ==> (\\<lambda>a. M a + N a) \\<in> multiset"
+ "M \<in> multiset ==> N \<in> multiset ==> (\<lambda>a. M a + N a) \<in> multiset"
apply (unfold multiset_def)
apply simp
apply (drule finite_UnI)
@@ -80,7 +80,7 @@
done
lemma diff_preserves_multiset [simp]:
- "M \\<in> multiset ==> (\\<lambda>a. M a - N a) \\<in> multiset"
+ "M \<in> multiset ==> (\<lambda>a. M a - N a) \<in> multiset"
apply (unfold multiset_def)
apply simp
apply (rule finite_subset)
@@ -94,7 +94,7 @@
subsubsection {* Union *}
-theorem union_empty [simp]: "M + {#} = M \\<and> {#} + M = M"
+theorem union_empty [simp]: "M + {#} = M \<and> {#} + M = M"
apply (simp add: union_def Mempty_def)
done
@@ -124,7 +124,7 @@
subsubsection {* Difference *}
-theorem diff_empty [simp]: "M - {#} = M \\<and> {#} - M = {#}"
+theorem diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
apply (simp add: Mempty_def diff_def)
done
@@ -139,7 +139,7 @@
apply (simp add: count_def Mempty_def)
done
-theorem count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)"
+theorem count_single [simp]: "count {#b#} a = (if b = a then 1' else 0)"
apply (simp add: count_def single_def)
done
@@ -162,7 +162,7 @@
apply (simp add: set_of_def)
done
-theorem set_of_union [simp]: "set_of (M + N) = set_of M \\<union> set_of N"
+theorem set_of_union [simp]: "set_of (M + N) = set_of M \<union> set_of N"
apply (auto simp add: set_of_def)
done
@@ -170,7 +170,7 @@
apply (auto simp add: set_of_def Mempty_def count_def expand_fun_eq)
done
-theorem mem_set_of_iff [simp]: "(x \\<in> set_of M) = (x :# M)"
+theorem mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)"
apply (auto simp add: set_of_def)
done
@@ -191,7 +191,7 @@
done
theorem setsum_count_Int:
- "finite A ==> setsum (count N) (A \\<inter> set_of N) = setsum (count N) A"
+ "finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A"
apply (erule finite_induct)
apply simp
apply (simp add: Int_insert_left set_of_def)
@@ -199,7 +199,7 @@
theorem size_union [simp]: "size (M + N::'a multiset) = size M + size N"
apply (unfold size_def)
- apply (subgoal_tac "count (M + N) = (\\<lambda>a. count M a + count N a)")
+ apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)")
prefer 2
apply (rule ext)
apply simp
@@ -214,7 +214,7 @@
apply (simp add: set_of_def count_def expand_fun_eq)
done
-theorem size_eq_Suc_imp_elem: "size M = Suc n ==> \\<exists>a. a :# M"
+theorem size_eq_Suc_imp_elem: "size M = Suc n ==> \<exists>a. a :# M"
apply (unfold size_def)
apply (drule setsum_SucD)
apply auto
@@ -223,11 +223,11 @@
subsubsection {* Equality of multisets *}
-theorem multiset_eq_conv_count_eq: "(M = N) = (\\<forall>a. count M a = count N a)"
+theorem multiset_eq_conv_count_eq: "(M = N) = (\<forall>a. count M a = count N a)"
apply (simp add: count_def expand_fun_eq)
done
-theorem single_not_empty [simp]: "{#a#} \\<noteq> {#} \\<and> {#} \\<noteq> {#a#}"
+theorem single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
apply (simp add: single_def Mempty_def expand_fun_eq)
done
@@ -235,11 +235,11 @@
apply (auto simp add: single_def expand_fun_eq)
done
-theorem union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \\<and> N = {#})"
+theorem union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \<and> N = {#})"
apply (auto simp add: union_def Mempty_def expand_fun_eq)
done
-theorem empty_eq_union [iff]: "({#} = M + N) = (M = {#} \\<and> N = {#})"
+theorem empty_eq_union [iff]: "({#} = M + N) = (M = {#} \<and> N = {#})"
apply (auto simp add: union_def Mempty_def expand_fun_eq)
done
@@ -252,7 +252,7 @@
done
theorem union_is_single:
- "(M + N = {#a#}) = (M = {#a#} \\<and> N={#} \\<or> M = {#} \\<and> N = {#a#})"
+ "(M + N = {#a#}) = (M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#})"
apply (unfold Mempty_def single_def union_def)
apply (simp add: add_is_1 expand_fun_eq)
apply blast
@@ -260,16 +260,16 @@
theorem single_is_union:
"({#a#} = M + N) =
- ({#a#} = M \\<and> N = {#} \\<or> M = {#} \\<and> {#a#} = N)"
+ ({#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N)"
apply (unfold Mempty_def single_def union_def)
- apply (simp add: add_is_1 expand_fun_eq)
+ apply (simp add: add_is_1 one_is_add expand_fun_eq)
apply (blast dest: sym)
done
theorem add_eq_conv_diff:
"(M + {#a#} = N + {#b#}) =
- (M = N \\<and> a = b \\<or>
- M = N - {#a#} + {#b#} \\<and> N = M - {#b#} + {#a#})"
+ (M = N \<and> a = b \<or>
+ M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#})"
apply (unfold single_def union_def diff_def)
apply (simp (no_asm) add: expand_fun_eq)
apply (rule conjI)
@@ -291,7 +291,7 @@
(*
val prems = Goal
"[| !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> finite F --> P F";
-by (res_inst_tac [("a","F"),("f","\\<lambda>A. if finite A then card A else 0")]
+by (res_inst_tac [("a","F"),("f","\<lambda>A. if finite A then card A else 0")]
measure_induct 1);
by (Clarify_tac 1);
by (resolve_tac prems 1);
@@ -320,7 +320,7 @@
lemma setsum_decr:
"finite F ==> 0 < f a ==>
- setsum (f (a := f a - 1)) F = (if a \\<in> F then setsum f F - 1 else setsum f F)"
+ setsum (f (a := f a - 1')) F = (if a \<in> F then setsum f F - 1 else setsum f F)"
apply (erule finite_induct)
apply auto
apply (drule_tac a = a in mk_disjoint_insert)
@@ -328,8 +328,8 @@
done
lemma rep_multiset_induct_aux:
- "P (\\<lambda>a. 0) ==> (!!f b. f \\<in> multiset ==> P f ==> P (f (b := f b + 1)))
- ==> \\<forall>f. f \\<in> multiset --> setsum f {x. 0 < f x} = n --> P f"
+ "P (\<lambda>a. 0) ==> (!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1')))
+ ==> \<forall>f. f \<in> multiset --> setsum f {x. 0 < f x} = n --> P f"
proof -
case antecedent
note prems = this [unfolded multiset_def]
@@ -338,7 +338,7 @@
apply (induct_tac n)
apply simp
apply clarify
- apply (subgoal_tac "f = (\\<lambda>a.0)")
+ apply (subgoal_tac "f = (\<lambda>a.0)")
apply simp
apply (rule prems)
apply (rule ext)
@@ -347,14 +347,14 @@
apply (frule setsum_SucD)
apply clarify
apply (rename_tac a)
- apply (subgoal_tac "finite {x. 0 < (f (a := f a - 1)) x}")
+ apply (subgoal_tac "finite {x. 0 < (f (a := f a - 1')) x}")
prefer 2
apply (rule finite_subset)
prefer 2
apply assumption
apply simp
apply blast
- apply (subgoal_tac "f = (f (a := f a - 1))(a := (f (a := f a - 1)) a + 1)")
+ apply (subgoal_tac "f = (f (a := f a - 1'))(a := (f (a := f a - 1')) a + 1')")
prefer 2
apply (rule ext)
apply (simp (no_asm_simp))
@@ -363,10 +363,10 @@
apply (erule allE, erule impE, erule_tac [2] mp)
apply blast
apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply)
- apply (subgoal_tac "{x. x \\<noteq> a --> 0 < f x} = {x. 0 < f x}")
+ apply (subgoal_tac "{x. x \<noteq> a --> 0 < f x} = {x. 0 < f x}")
prefer 2
apply blast
- apply (subgoal_tac "{x. x \\<noteq> a \\<and> 0 < f x} = {x. 0 < f x} - {a}")
+ apply (subgoal_tac "{x. x \<noteq> a \<and> 0 < f x} = {x. 0 < f x} - {a}")
prefer 2
apply blast
apply (simp add: le_imp_diff_is_add setsum_diff1 cong: conj_cong)
@@ -374,8 +374,8 @@
qed
theorem rep_multiset_induct:
- "f \\<in> multiset ==> P (\\<lambda>a. 0) ==>
- (!!f b. f \\<in> multiset ==> P f ==> P (f (b := f b + 1))) ==> P f"
+ "f \<in> multiset ==> P (\<lambda>a. 0) ==>
+ (!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1'))) ==> P f"
apply (insert rep_multiset_induct_aux)
apply blast
done
@@ -390,7 +390,7 @@
apply (rule Rep_multiset_inverse [THEN subst])
apply (rule Rep_multiset [THEN rep_multiset_induct])
apply (rule prem1)
- apply (subgoal_tac "f (b := f b + 1) = (\\<lambda>a. f a + (if a = b then 1 else 0))")
+ apply (subgoal_tac "f (b := f b + 1') = (\<lambda>a. f a + (if a = b then 1' else 0))")
prefer 2
apply (simp add: expand_fun_eq)
apply (erule ssubst)
@@ -401,7 +401,7 @@
lemma MCollect_preserves_multiset:
- "M \\<in> multiset ==> (\\<lambda>x. if P x then M x else 0) \\<in> multiset"
+ "M \<in> multiset ==> (\<lambda>x. if P x then M x else 0) \<in> multiset"
apply (simp add: multiset_def)
apply (rule finite_subset)
apply auto
@@ -413,11 +413,11 @@
apply (simp add: MCollect_preserves_multiset)
done
-theorem set_of_MCollect [simp]: "set_of {# x:M. P x #} = set_of M \\<inter> {x. P x}"
+theorem set_of_MCollect [simp]: "set_of {# x:M. P x #} = set_of M \<inter> {x. P x}"
apply (auto simp add: set_of_def)
done
-theorem multiset_partition: "M = {# x:M. P x #} + {# x:M. \\<not> P x #}"
+theorem multiset_partition: "M = {# x:M. P x #} + {# x:M. \<not> P x #}"
apply (subst multiset_eq_conv_count_eq)
apply auto
done
@@ -427,7 +427,7 @@
theorem add_eq_conv_ex:
"(M + {#a#} = N + {#b#}) =
- (M = N \\<and> a = b \\<or> (\\<exists>K. M = K + {#b#} \\<and> N = K + {#a#}))"
+ (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))"
apply (auto simp add: add_eq_conv_diff)
done
@@ -437,41 +437,41 @@
subsubsection {* Well-foundedness *}
constdefs
- mult1 :: "('a \\<times> 'a) set => ('a multiset \\<times> 'a multiset) set"
+ mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set"
"mult1 r ==
- {(N, M). \\<exists>a M0 K. M = M0 + {#a#} \\<and> N = M0 + K \\<and>
- (\\<forall>b. b :# K --> (b, a) \\<in> r)}"
+ {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
+ (\<forall>b. b :# K --> (b, a) \<in> r)}"
- mult :: "('a \\<times> 'a) set => ('a multiset \\<times> 'a multiset) set"
+ mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set"
"mult r == (mult1 r)\<^sup>+"
-lemma not_less_empty [iff]: "(M, {#}) \\<notin> mult1 r"
+lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
by (simp add: mult1_def)
-lemma less_add: "(N, M0 + {#a#}) \\<in> mult1 r ==>
- (\\<exists>M. (M, M0) \\<in> mult1 r \\<and> N = M + {#a#}) \\<or>
- (\\<exists>K. (\\<forall>b. b :# K --> (b, a) \\<in> r) \\<and> N = M0 + K)"
- (concl is "?case1 (mult1 r) \\<or> ?case2")
+lemma less_add: "(N, M0 + {#a#}) \<in> mult1 r ==>
+ (\<exists>M. (M, M0) \<in> mult1 r \<and> N = M + {#a#}) \<or>
+ (\<exists>K. (\<forall>b. b :# K --> (b, a) \<in> r) \<and> N = M0 + K)"
+ (concl is "?case1 (mult1 r) \<or> ?case2")
proof (unfold mult1_def)
- let ?r = "\\<lambda>K a. \\<forall>b. b :# K --> (b, a) \\<in> r"
- let ?R = "\\<lambda>N M. \\<exists>a M0 K. M = M0 + {#a#} \\<and> N = M0 + K \\<and> ?r K a"
+ let ?r = "\<lambda>K a. \<forall>b. b :# K --> (b, a) \<in> r"
+ let ?R = "\<lambda>N M. \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and> ?r K a"
let ?case1 = "?case1 {(N, M). ?R N M}"
- assume "(N, M0 + {#a#}) \\<in> {(N, M). ?R N M}"
- hence "\\<exists>a' M0' K.
- M0 + {#a#} = M0' + {#a'#} \\<and> N = M0' + K \\<and> ?r K a'" by simp
- thus "?case1 \\<or> ?case2"
+ assume "(N, M0 + {#a#}) \<in> {(N, M). ?R N M}"
+ hence "\<exists>a' M0' K.
+ M0 + {#a#} = M0' + {#a'#} \<and> N = M0' + K \<and> ?r K a'" by simp
+ thus "?case1 \<or> ?case2"
proof (elim exE conjE)
fix a' M0' K
assume N: "N = M0' + K" and r: "?r K a'"
assume "M0 + {#a#} = M0' + {#a'#}"
- hence "M0 = M0' \\<and> a = a' \\<or>
- (\\<exists>K'. M0 = K' + {#a'#} \\<and> M0' = K' + {#a#})"
+ hence "M0 = M0' \<and> a = a' \<or>
+ (\<exists>K'. M0 = K' + {#a'#} \<and> M0' = K' + {#a#})"
by (simp only: add_eq_conv_ex)
thus ?thesis
proof (elim disjE conjE exE)
assume "M0 = M0'" "a = a'"
- with N r have "?r K a \\<and> N = M0 + K" by simp
+ with N r have "?r K a \<and> N = M0 + K" by simp
hence ?case2 .. thus ?thesis ..
next
fix K'
@@ -485,78 +485,78 @@
qed
qed
-lemma all_accessible: "wf r ==> \\<forall>M. M \\<in> acc (mult1 r)"
+lemma all_accessible: "wf r ==> \<forall>M. M \<in> acc (mult1 r)"
proof
let ?R = "mult1 r"
let ?W = "acc ?R"
{
fix M M0 a
- assume M0: "M0 \\<in> ?W"
- and wf_hyp: "\\<forall>b. (b, a) \\<in> r --> (\\<forall>M \\<in> ?W. M + {#b#} \\<in> ?W)"
- and acc_hyp: "\\<forall>M. (M, M0) \\<in> ?R --> M + {#a#} \\<in> ?W"
- have "M0 + {#a#} \\<in> ?W"
+ assume M0: "M0 \<in> ?W"
+ and wf_hyp: "\<forall>b. (b, a) \<in> r --> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
+ and acc_hyp: "\<forall>M. (M, M0) \<in> ?R --> M + {#a#} \<in> ?W"
+ have "M0 + {#a#} \<in> ?W"
proof (rule accI [of "M0 + {#a#}"])
fix N
- assume "(N, M0 + {#a#}) \\<in> ?R"
- hence "((\\<exists>M. (M, M0) \\<in> ?R \\<and> N = M + {#a#}) \\<or>
- (\\<exists>K. (\\<forall>b. b :# K --> (b, a) \\<in> r) \\<and> N = M0 + K))"
+ assume "(N, M0 + {#a#}) \<in> ?R"
+ hence "((\<exists>M. (M, M0) \<in> ?R \<and> N = M + {#a#}) \<or>
+ (\<exists>K. (\<forall>b. b :# K --> (b, a) \<in> r) \<and> N = M0 + K))"
by (rule less_add)
- thus "N \\<in> ?W"
+ thus "N \<in> ?W"
proof (elim exE disjE conjE)
- fix M assume "(M, M0) \\<in> ?R" and N: "N = M + {#a#}"
- from acc_hyp have "(M, M0) \\<in> ?R --> M + {#a#} \\<in> ?W" ..
- hence "M + {#a#} \\<in> ?W" ..
- thus "N \\<in> ?W" by (simp only: N)
+ fix M assume "(M, M0) \<in> ?R" and N: "N = M + {#a#}"
+ from acc_hyp have "(M, M0) \<in> ?R --> M + {#a#} \<in> ?W" ..
+ hence "M + {#a#} \<in> ?W" ..
+ thus "N \<in> ?W" by (simp only: N)
next
fix K
assume N: "N = M0 + K"
- assume "\\<forall>b. b :# K --> (b, a) \\<in> r"
- have "?this --> M0 + K \\<in> ?W" (is "?P K")
+ assume "\<forall>b. b :# K --> (b, a) \<in> r"
+ have "?this --> M0 + K \<in> ?W" (is "?P K")
proof (induct K)
- from M0 have "M0 + {#} \\<in> ?W" by simp
+ from M0 have "M0 + {#} \<in> ?W" by simp
thus "?P {#}" ..
fix K x assume hyp: "?P K"
show "?P (K + {#x#})"
proof
- assume a: "\\<forall>b. b :# (K + {#x#}) --> (b, a) \\<in> r"
- hence "(x, a) \\<in> r" by simp
- with wf_hyp have b: "\\<forall>M \\<in> ?W. M + {#x#} \\<in> ?W" by blast
+ assume a: "\<forall>b. b :# (K + {#x#}) --> (b, a) \<in> r"
+ hence "(x, a) \<in> r" by simp
+ with wf_hyp have b: "\<forall>M \<in> ?W. M + {#x#} \<in> ?W" by blast
- from a hyp have "M0 + K \\<in> ?W" by simp
- with b have "(M0 + K) + {#x#} \\<in> ?W" ..
- thus "M0 + (K + {#x#}) \\<in> ?W" by (simp only: union_assoc)
+ from a hyp have "M0 + K \<in> ?W" by simp
+ with b have "(M0 + K) + {#x#} \<in> ?W" ..
+ thus "M0 + (K + {#x#}) \<in> ?W" by (simp only: union_assoc)
qed
qed
- hence "M0 + K \\<in> ?W" ..
- thus "N \\<in> ?W" by (simp only: N)
+ hence "M0 + K \<in> ?W" ..
+ thus "N \<in> ?W" by (simp only: N)
qed
qed
} note tedious_reasoning = this
assume wf: "wf r"
fix M
- show "M \\<in> ?W"
+ show "M \<in> ?W"
proof (induct M)
- show "{#} \\<in> ?W"
+ show "{#} \<in> ?W"
proof (rule accI)
- fix b assume "(b, {#}) \\<in> ?R"
- with not_less_empty show "b \\<in> ?W" by contradiction
+ fix b assume "(b, {#}) \<in> ?R"
+ with not_less_empty show "b \<in> ?W" by contradiction
qed
- fix M a assume "M \\<in> ?W"
- from wf have "\\<forall>M \\<in> ?W. M + {#a#} \\<in> ?W"
+ fix M a assume "M \<in> ?W"
+ from wf have "\<forall>M \<in> ?W. M + {#a#} \<in> ?W"
proof induct
fix a
- assume "\\<forall>b. (b, a) \\<in> r --> (\\<forall>M \\<in> ?W. M + {#b#} \\<in> ?W)"
- show "\\<forall>M \\<in> ?W. M + {#a#} \\<in> ?W"
+ assume "\<forall>b. (b, a) \<in> r --> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
+ show "\<forall>M \<in> ?W. M + {#a#} \<in> ?W"
proof
- fix M assume "M \\<in> ?W"
- thus "M + {#a#} \\<in> ?W"
+ fix M assume "M \<in> ?W"
+ thus "M + {#a#} \<in> ?W"
by (rule acc_induct) (rule tedious_reasoning)
qed
qed
- thus "M + {#a#} \\<in> ?W" ..
+ thus "M + {#a#} \<in> ?W" ..
qed
qed
@@ -578,9 +578,9 @@
text {* One direction. *}
lemma mult_implies_one_step:
- "trans r ==> (M, N) \\<in> mult r ==>
- \\<exists>I J K. N = I + J \\<and> M = I + K \\<and> J \\<noteq> {#} \\<and>
- (\\<forall>k \\<in> set_of K. \\<exists>j \\<in> set_of J. (k, j) \\<in> r)"
+ "trans r ==> (M, N) \<in> mult r ==>
+ \<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and>
+ (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r)"
apply (unfold mult_def mult1_def set_of_def)
apply (erule converse_trancl_induct)
apply clarify
@@ -592,7 +592,7 @@
apply (simp (no_asm))
apply (rule_tac x = "(K - {#a#}) + Ka" in exI)
apply (simp (no_asm_simp) add: union_assoc [symmetric])
- apply (drule_tac f = "\\<lambda>M. M - {#a#}" in arg_cong)
+ apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong)
apply (simp add: diff_union_single_conv)
apply (simp (no_asm_use) add: trans_def)
apply blast
@@ -603,7 +603,7 @@
apply (rule conjI)
apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
apply (rule conjI)
- apply (drule_tac f = "\\<lambda>M. M - {#a#}" in arg_cong)
+ apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong)
apply simp
apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
apply (simp (no_asm_use) add: trans_def)
@@ -617,7 +617,7 @@
apply (simp add: multiset_eq_conv_count_eq)
done
-lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \\<exists>a N. M = N + {#a#}"
+lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \<exists>a N. M = N + {#a#}"
apply (erule size_eq_Suc_imp_elem [THEN exE])
apply (drule elem_imp_eq_diff_union)
apply auto
@@ -625,8 +625,8 @@
lemma one_step_implies_mult_aux:
"trans r ==>
- \\<forall>I J K. (size J = n \\<and> J \\<noteq> {#} \\<and> (\\<forall>k \\<in> set_of K. \\<exists>j \\<in> set_of J. (k, j) \\<in> r))
- --> (I + K, I + J) \\<in> mult r"
+ \<forall>I J K. (size J = n \<and> J \<noteq> {#} \<and> (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r))
+ --> (I + K, I + J) \<in> mult r"
apply (induct_tac n)
apply auto
apply (frule size_eq_Suc_imp_eq_union)
@@ -640,15 +640,15 @@
apply (rule r_into_trancl)
apply (simp add: mult1_def set_of_def)
apply blast
- txt {* Now we know @{term "J' \\<noteq> {#}"}. *}
- apply (cut_tac M = K and P = "\\<lambda>x. (x, a) \\<in> r" in multiset_partition)
- apply (erule_tac P = "\\<forall>k \\<in> set_of K. ?P k" in rev_mp)
+ txt {* Now we know @{term "J' \<noteq> {#}"}. *}
+ apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition)
+ apply (erule_tac P = "\<forall>k \<in> set_of K. ?P k" in rev_mp)
apply (erule ssubst)
apply (simp add: Ball_def)
apply auto
apply (subgoal_tac
- "((I + {# x : K. (x, a) \\<in> r #}) + {# x : K. (x, a) \\<notin> r #},
- (I + {# x : K. (x, a) \\<in> r #}) + J') \\<in> mult r")
+ "((I + {# x : K. (x, a) \<in> r #}) + {# x : K. (x, a) \<notin> r #},
+ (I + {# x : K. (x, a) \<in> r #}) + J') \<in> mult r")
prefer 2
apply force
apply (simp (no_asm_use) add: union_assoc [symmetric] mult_def)
@@ -661,8 +661,8 @@
done
theorem one_step_implies_mult:
- "trans r ==> J \\<noteq> {#} ==> \\<forall>k \\<in> set_of K. \\<exists>j \\<in> set_of J. (k, j) \\<in> r
- ==> (I + K, I + J) \\<in> mult r"
+ "trans r ==> J \<noteq> {#} ==> \<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r
+ ==> (I + K, I + J) \<in> mult r"
apply (insert one_step_implies_mult_aux)
apply blast
done
@@ -673,8 +673,8 @@
instance multiset :: ("term") ord ..
defs (overloaded)
- less_multiset_def: "M' < M == (M', M) \\<in> mult {(x', x). x' < x}"
- le_multiset_def: "M' <= M == M' = M \\<or> M' < (M::'a multiset)"
+ less_multiset_def: "M' < M == (M', M) \<in> mult {(x', x). x' < x}"
+ le_multiset_def: "M' <= M == M' = M \<or> M' < (M::'a multiset)"
lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
apply (unfold trans_def)
@@ -686,12 +686,12 @@
*}
lemma mult_irrefl_aux:
- "finite A ==> (\\<forall>x \\<in> A. \\<exists>y \\<in> A. x < (y::'a::order)) --> A = {}"
+ "finite A ==> (\<forall>x \<in> A. \<exists>y \<in> A. x < (y::'a::order)) --> A = {}"
apply (erule finite_induct)
apply (auto intro: order_less_trans)
done
-theorem mult_less_not_refl: "\\<not> M < (M::'a::order multiset)"
+theorem mult_less_not_refl: "\<not> M < (M::'a::order multiset)"
apply (unfold less_multiset_def)
apply auto
apply (drule trans_base_order [THEN mult_implies_one_step])
@@ -715,7 +715,7 @@
text {* Asymmetry. *}
-theorem mult_less_not_sym: "M < N ==> \\<not> N < (M::'a::order multiset)"
+theorem mult_less_not_sym: "M < N ==> \<not> N < (M::'a::order multiset)"
apply auto
apply (rule mult_less_not_refl [THEN notE])
apply (erule mult_less_trans)
@@ -723,7 +723,7 @@
done
theorem mult_less_asym:
- "M < N ==> (\\<not> P ==> N < (M::'a::order multiset)) ==> P"
+ "M < N ==> (\<not> P ==> N < (M::'a::order multiset)) ==> P"
apply (insert mult_less_not_sym)
apply blast
done
@@ -749,7 +749,7 @@
apply (blast intro: mult_less_trans)
done
-theorem mult_less_le: "M < N = (M <= N \\<and> M \\<noteq> (N::'a::order multiset))"
+theorem mult_less_le: "M < N = (M <= N \<and> M \<noteq> (N::'a::order multiset))"
apply (unfold le_multiset_def)
apply auto
done
@@ -770,7 +770,7 @@
subsubsection {* Monotonicity of multiset union *}
theorem mult1_union:
- "(B, D) \\<in> mult1 r ==> trans r ==> (C + B, C + D) \\<in> mult1 r"
+ "(B, D) \<in> mult1 r ==> trans r ==> (C + B, C + D) \<in> mult1 r"
apply (unfold mult1_def)
apply auto
apply (rule_tac x = a in exI)
@@ -806,7 +806,7 @@
apply (unfold le_multiset_def less_multiset_def)
apply (case_tac "M = {#}")
prefer 2
- apply (subgoal_tac "({#} + {#}, {#} + M) \\<in> mult (Collect (split op <))")
+ apply (subgoal_tac "({#} + {#}, {#} + M) \<in> mult (Collect (split op <))")
prefer 2
apply (rule one_step_implies_mult)
apply (simp only: trans_def)
--- a/src/HOL/Library/Primes.thy Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/Library/Primes.thy Mon Aug 06 13:43:24 2001 +0200
@@ -54,7 +54,7 @@
declare gcd.simps [simp del]
-lemma gcd_1 [simp]: "gcd (m, 1) = 1"
+lemma gcd_1 [simp]: "gcd (m, 1') = 1"
apply (simp add: gcd_non_0)
done
@@ -140,8 +140,8 @@
apply (simp add: gcd_commute [of 0])
done
-lemma gcd_1_left [simp]: "gcd (1, m) = 1"
- apply (simp add: gcd_commute [of 1])
+lemma gcd_1_left [simp]: "gcd (1', m) = 1"
+ apply (simp add: gcd_commute [of "1'"])
done
--- a/src/HOL/Nat.ML Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/Nat.ML Mon Aug 06 13:43:24 2001 +0200
@@ -68,7 +68,7 @@
by Auto_tac;
qed "less_Suc_eq_0_disj";
-val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
+val prems = Goal "[| P 0; P(1'); !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
by (rtac nat_less_induct 1);
by (case_tac "n" 1);
by (case_tac "nat" 2);
@@ -157,7 +157,7 @@
(* Could be (and is, below) generalized in various ways;
However, none of the generalizations are currently in the simpset,
and I dread to think what happens if I put them in *)
-Goal "0 < n ==> Suc(n-1) = n";
+Goal "0 < n ==> Suc(n-1') = n";
by (asm_simp_tac (simpset() addsplits [nat.split]) 1);
qed "Suc_pred";
Addsimps [Suc_pred];
@@ -238,11 +238,16 @@
qed "add_is_0";
AddIffs [add_is_0];
-Goal "!!m::nat. (m+n=1) = (m=1 & n=0 | m=0 & n=1)";
+Goal "(m+n=1') = (m=1' & n=0 | m=0 & n=1')";
by (case_tac "m" 1);
by (Auto_tac);
qed "add_is_1";
+Goal "(1' = m+n) = (m=1' & n=0 | m=0 & n=1')";
+by (case_tac "m" 1);
+by (Auto_tac);
+qed "one_is_add";
+
Goal "!!m::nat. (0<m+n) = (0<m | 0<n)";
by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
qed "add_gr_0";
@@ -633,14 +638,14 @@
qed "zero_less_mult_iff";
Addsimps [zero_less_mult_iff];
-Goal "(1 <= m*n) = (1<=m & 1<=n)";
+Goal "(1' <= m*n) = (1<=m & 1<=n)";
by (induct_tac "m" 1);
by (case_tac "n" 2);
by (ALLGOALS Asm_simp_tac);
qed "one_le_mult_iff";
Addsimps [one_le_mult_iff];
-Goal "(m*n = 1) = (m=1 & n=1)";
+Goal "(m*n = 1') = (m=1 & n=1)";
by (induct_tac "m" 1);
by (Simp_tac 1);
by (induct_tac "n" 1);
@@ -649,6 +654,12 @@
qed "mult_eq_1_iff";
Addsimps [mult_eq_1_iff];
+Goal "(1' = m*n) = (m=1 & n=1)";
+by(rtac (mult_eq_1_iff RSN (2,trans)) 1);
+by (fast_tac (claset() addss simpset()) 1);
+qed "one_eq_mult_iff";
+Addsimps [one_eq_mult_iff];
+
Goal "!!m::nat. (m*k < n*k) = (0<k & m<n)";
by (safe_tac (claset() addSIs [mult_less_mono1]));
by (case_tac "k" 1);
--- a/src/HOL/NatDef.ML Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/NatDef.ML Mon Aug 06 13:43:24 2001 +0200
@@ -4,6 +4,8 @@
Copyright 1991 University of Cambridge
*)
+Addsimps [One_def];
+
val rew = rewrite_rule [symmetric Nat_def];
(*** Induction ***)
--- a/src/HOL/NatDef.thy Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/NatDef.thy Mon Aug 06 13:43:24 2001 +0200
@@ -55,14 +55,15 @@
consts
Suc :: nat => nat
pred_nat :: "(nat * nat) set"
+ "1" :: nat ("1")
syntax
- "1" :: nat ("1")
+ "1'" :: nat ("1'")
"2" :: nat ("2")
translations
- "1" == "Suc 0"
- "2" == "Suc 1"
+ "1'" == "Suc 0"
+ "2" == "Suc 1'"
local
@@ -70,6 +71,7 @@
defs
Zero_def "0 == Abs_Nat(Zero_Rep)"
Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
+ One_def "1 == 1'"
(*nat operations*)
pred_nat_def "pred_nat == {(m,n). n = Suc m}"
--- a/src/HOL/Power.ML Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/Power.ML Mon Aug 06 13:43:24 2001 +0200
@@ -30,7 +30,7 @@
by Auto_tac;
qed "power_eq_0D";
-Goal "!!i::nat. 1 <= i ==> 1 <= i^n";
+Goal "!!i::nat. 1 <= i ==> 1' <= i^n";
by (induct_tac "n" 1);
by Auto_tac;
qed "one_le_power";
@@ -120,7 +120,7 @@
qed "binomial_Suc_n";
Addsimps [binomial_Suc_n];
-Goal "(n choose 1) = n";
+Goal "(n choose 1') = n";
by (induct_tac "n" 1);
by (ALLGOALS Asm_simp_tac);
qed "binomial_1";
--- a/src/HOL/Real/PNat.ML Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/Real/PNat.ML Mon Aug 06 13:43:24 2001 +0200
@@ -6,13 +6,13 @@
The positive naturals -- proofs mainly as in theory Nat.
*)
-Goal "mono(%X. {1} Un Suc`X)";
+Goal "mono(%X. {1'} Un Suc`X)";
by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1));
qed "pnat_fun_mono";
bind_thm ("pnat_unfold", pnat_fun_mono RS (pnat_def RS def_lfp_unfold));
-Goal "1 : pnat";
+Goal "1' : pnat";
by (stac pnat_unfold 1);
by (rtac (singletonI RS UnI1) 1);
qed "one_RepI";
@@ -31,7 +31,7 @@
(*** Induction ***)
val major::prems = Goal
- "[| i: pnat; P(1); \
+ "[| i: pnat; P(1'); \
\ !!j. [| j: pnat; P(j) |] ==> P(Suc(j)) |] ==> P(i)";
by (rtac ([pnat_def, pnat_fun_mono, major] MRS def_lfp_induct) 1);
by (blast_tac (claset() addIs prems) 1);
@@ -250,7 +250,7 @@
(*** Rep_pnat < 0 ==> P ***)
bind_thm ("Rep_pnat_less_zeroE",Rep_pnat_not_less0 RS notE);
-Goal "~ Rep_pnat y < 1";
+Goal "~ Rep_pnat y < 1'";
by (auto_tac (claset(),simpset() addsimps [less_Suc_eq,
Rep_pnat_gt_zero,less_not_refl2]));
qed "Rep_pnat_not_less_one";
@@ -259,7 +259,7 @@
bind_thm ("Rep_pnat_less_oneE",Rep_pnat_not_less_one RS notE);
Goalw [pnat_less_def]
- "x < (y::pnat) ==> Rep_pnat y ~= 1";
+ "x < (y::pnat) ==> Rep_pnat y ~= 1'";
by (auto_tac (claset(),simpset()
addsimps [Rep_pnat_not_less_one] delsimps [less_one]));
qed "Rep_pnat_gt_implies_not0";
@@ -270,7 +270,7 @@
by (fast_tac (claset() addIs [inj_Rep_pnat RS injD]) 1);
qed "pnat_less_linear";
-Goalw [le_def] "1 <= Rep_pnat x";
+Goalw [le_def] "1' <= Rep_pnat x";
by (rtac Rep_pnat_not_less_one 1);
qed "Rep_pnat_le_one";
@@ -416,12 +416,12 @@
Abs_pnat_inverse,mult_left_commute]) 1);
qed "pnat_mult_left_commute";
-Goalw [pnat_mult_def] "x * (Abs_pnat 1) = x";
+Goalw [pnat_mult_def] "x * (Abs_pnat 1') = x";
by (full_simp_tac (simpset() addsimps [one_RepI RS Abs_pnat_inverse,
Rep_pnat_inverse]) 1);
qed "pnat_mult_1";
-Goal "Abs_pnat 1 * x = x";
+Goal "Abs_pnat 1' * x = x";
by (full_simp_tac (simpset() addsimps [pnat_mult_1,
pnat_mult_commute]) 1);
qed "pnat_mult_1_left";
--- a/src/HOL/Real/PNat.thy Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/Real/PNat.thy Mon Aug 06 13:43:24 2001 +0200
@@ -9,7 +9,7 @@
PNat = Main +
typedef
- pnat = "lfp(%X. {1} Un Suc`X)" (lfp_def)
+ pnat = "lfp(%X. {1'} Un Suc`X)" (lfp_def)
instance
pnat :: {ord, plus, times}
@@ -27,7 +27,7 @@
defs
pnat_one_def
- "1p == Abs_pnat(1)"
+ "1p == Abs_pnat(1')"
pnat_Suc_def
"pSuc == (%n. Abs_pnat(Suc(Rep_pnat(n))))"
--- a/src/HOL/Real/PRat.ML Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/Real/PRat.ML Mon Aug 06 13:43:24 2001 +0200
@@ -128,7 +128,7 @@
qed "inj_qinv";
Goalw [prat_of_pnat_def]
- "qinv(prat_of_pnat (Abs_pnat 1)) = prat_of_pnat (Abs_pnat 1)";
+ "qinv(prat_of_pnat (Abs_pnat 1')) = prat_of_pnat (Abs_pnat 1')";
by (simp_tac (simpset() addsimps [qinv]) 1);
qed "qinv_1";
@@ -232,13 +232,13 @@
prat_mult_commute,prat_mult_left_commute]);
Goalw [prat_of_pnat_def]
- "(prat_of_pnat (Abs_pnat 1)) * z = z";
+ "(prat_of_pnat (Abs_pnat 1')) * z = z";
by (res_inst_tac [("z","z")] eq_Abs_prat 1);
by (asm_full_simp_tac (simpset() addsimps [prat_mult] @ pnat_mult_ac) 1);
qed "prat_mult_1";
Goalw [prat_of_pnat_def]
- "z * (prat_of_pnat (Abs_pnat 1)) = z";
+ "z * (prat_of_pnat (Abs_pnat 1')) = z";
by (res_inst_tac [("z","z")] eq_Abs_prat 1);
by (asm_full_simp_tac (simpset() addsimps [prat_mult] @ pnat_mult_ac) 1);
qed "prat_mult_1_right";
@@ -259,22 +259,22 @@
(*** prat_mult and qinv ***)
Goalw [prat_def,prat_of_pnat_def]
- "qinv (q) * q = prat_of_pnat (Abs_pnat 1)";
+ "qinv (q) * q = prat_of_pnat (Abs_pnat 1')";
by (res_inst_tac [("z","q")] eq_Abs_prat 1);
by (asm_full_simp_tac (simpset() addsimps [qinv,
prat_mult,pnat_mult_1,pnat_mult_1_left, pnat_mult_commute]) 1);
qed "prat_mult_qinv";
-Goal "q * qinv (q) = prat_of_pnat (Abs_pnat 1)";
+Goal "q * qinv (q) = prat_of_pnat (Abs_pnat 1')";
by (rtac (prat_mult_commute RS subst) 1);
by (simp_tac (simpset() addsimps [prat_mult_qinv]) 1);
qed "prat_mult_qinv_right";
-Goal "EX y. (x::prat) * y = prat_of_pnat (Abs_pnat 1)";
+Goal "EX y. (x::prat) * y = prat_of_pnat (Abs_pnat 1')";
by (fast_tac (claset() addIs [prat_mult_qinv_right]) 1);
qed "prat_qinv_ex";
-Goal "EX! y. (x::prat) * y = prat_of_pnat (Abs_pnat 1)";
+Goal "EX! y. (x::prat) * y = prat_of_pnat (Abs_pnat 1')";
by (auto_tac (claset() addIs [prat_mult_qinv_right],simpset()));
by (dres_inst_tac [("f","%x. ya*x")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [prat_mult_assoc RS sym]) 1);
@@ -282,7 +282,7 @@
prat_mult_1,prat_mult_1_right]) 1);
qed "prat_qinv_ex1";
-Goal "EX! y. y * (x::prat) = prat_of_pnat (Abs_pnat 1)";
+Goal "EX! y. y * (x::prat) = prat_of_pnat (Abs_pnat 1')";
by (auto_tac (claset() addIs [prat_mult_qinv],simpset()));
by (dres_inst_tac [("f","%x. x*ya")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [prat_mult_assoc]) 1);
@@ -290,7 +290,7 @@
prat_mult_1,prat_mult_1_right]) 1);
qed "prat_qinv_left_ex1";
-Goal "x * y = prat_of_pnat (Abs_pnat 1) ==> x = qinv y";
+Goal "x * y = prat_of_pnat (Abs_pnat 1') ==> x = qinv y";
by (cut_inst_tac [("q","y")] prat_mult_qinv 1);
by (res_inst_tac [("x1","y")] (prat_qinv_left_ex1 RS ex1E) 1);
by (Blast_tac 1);
@@ -506,7 +506,7 @@
by (cut_inst_tac [("x","q1"),("q1.0","qinv (q1)"), ("q2.0","qinv (q2)")]
prat_mult_left_less2_mono1 1);
by Auto_tac;
-by (dres_inst_tac [("q2.0","prat_of_pnat (Abs_pnat 1)")] prat_less_trans 1);
+by (dres_inst_tac [("q2.0","prat_of_pnat (Abs_pnat 1')")] prat_less_trans 1);
by (auto_tac (claset(),simpset() addsimps
[prat_less_not_refl]));
qed "lemma2_qinv_prat_less";
@@ -517,8 +517,8 @@
lemma2_qinv_prat_less],simpset()));
qed "qinv_prat_less";
-Goal "q1 < prat_of_pnat (Abs_pnat 1) \
-\ ==> prat_of_pnat (Abs_pnat 1) < qinv(q1)";
+Goal "q1 < prat_of_pnat (Abs_pnat 1') \
+\ ==> prat_of_pnat (Abs_pnat 1') < qinv(q1)";
by (dtac qinv_prat_less 1);
by (full_simp_tac (simpset() addsimps [qinv_1]) 1);
qed "prat_qinv_gt_1";
@@ -529,18 +529,18 @@
qed "prat_qinv_is_gt_1";
Goalw [prat_less_def]
- "prat_of_pnat (Abs_pnat 1) < prat_of_pnat (Abs_pnat 1) \
-\ + prat_of_pnat (Abs_pnat 1)";
+ "prat_of_pnat (Abs_pnat 1') < prat_of_pnat (Abs_pnat 1') \
+\ + prat_of_pnat (Abs_pnat 1')";
by (Fast_tac 1);
qed "prat_less_1_2";
-Goal "qinv(prat_of_pnat (Abs_pnat 1) + \
-\ prat_of_pnat (Abs_pnat 1)) < prat_of_pnat (Abs_pnat 1)";
+Goal "qinv(prat_of_pnat (Abs_pnat 1') + \
+\ prat_of_pnat (Abs_pnat 1')) < prat_of_pnat (Abs_pnat 1')";
by (cut_facts_tac [prat_less_1_2 RS qinv_prat_less] 1);
by (asm_full_simp_tac (simpset() addsimps [qinv_1]) 1);
qed "prat_less_qinv_2_1";
-Goal "!!(x::prat). x < y ==> x*qinv(y) < prat_of_pnat (Abs_pnat 1)";
+Goal "!!(x::prat). x < y ==> x*qinv(y) < prat_of_pnat (Abs_pnat 1')";
by (dres_inst_tac [("x","qinv(y)")] prat_mult_less2_mono1 1);
by (Asm_full_simp_tac 1);
qed "prat_mult_qinv_less_1";
@@ -701,19 +701,19 @@
pnat_mult_1]));
qed "Abs_prat_mult_qinv";
-Goal "Abs_prat(ratrel``{(x,y)}) <= Abs_prat(ratrel``{(x,Abs_pnat 1)})";
+Goal "Abs_prat(ratrel``{(x,y)}) <= Abs_prat(ratrel``{(x,Abs_pnat 1')})";
by (simp_tac (simpset() addsimps [Abs_prat_mult_qinv]) 1);
by (rtac prat_mult_left_le2_mono1 1);
by (rtac qinv_prat_le 1);
by (pnat_ind_tac "y" 1);
-by (dres_inst_tac [("x","prat_of_pnat (Abs_pnat 1)")] prat_add_le2_mono1 2);
+by (dres_inst_tac [("x","prat_of_pnat (Abs_pnat 1')")] prat_add_le2_mono1 2);
by (cut_facts_tac [prat_less_1_2 RS prat_less_imp_le] 2);
by (auto_tac (claset() addIs [prat_le_trans],
simpset() addsimps [prat_le_refl,
pSuc_is_plus_one,pnat_one_def,prat_of_pnat_add]));
qed "lemma_Abs_prat_le1";
-Goal "Abs_prat(ratrel``{(x,Abs_pnat 1)}) <= Abs_prat(ratrel``{(x*y,Abs_pnat 1)})";
+Goal "Abs_prat(ratrel``{(x,Abs_pnat 1')}) <= Abs_prat(ratrel``{(x*y,Abs_pnat 1')})";
by (simp_tac (simpset() addsimps [Abs_prat_mult_qinv]) 1);
by (rtac prat_mult_le2_mono1 1);
by (pnat_ind_tac "y" 1);
@@ -726,19 +726,19 @@
prat_of_pnat_add,prat_of_pnat_mult]));
qed "lemma_Abs_prat_le2";
-Goal "Abs_prat(ratrel``{(x,z)}) <= Abs_prat(ratrel``{(x*y,Abs_pnat 1)})";
+Goal "Abs_prat(ratrel``{(x,z)}) <= Abs_prat(ratrel``{(x*y,Abs_pnat 1')})";
by (fast_tac (claset() addIs [prat_le_trans,
lemma_Abs_prat_le1,lemma_Abs_prat_le2]) 1);
qed "lemma_Abs_prat_le3";
-Goal "Abs_prat(ratrel``{(x*y,Abs_pnat 1)}) * Abs_prat(ratrel``{(w,x)}) = \
-\ Abs_prat(ratrel``{(w*y,Abs_pnat 1)})";
+Goal "Abs_prat(ratrel``{(x*y,Abs_pnat 1')}) * Abs_prat(ratrel``{(w,x)}) = \
+\ Abs_prat(ratrel``{(w*y,Abs_pnat 1')})";
by (full_simp_tac (simpset() addsimps [prat_mult,
pnat_mult_1,pnat_mult_1_left] @ pnat_mult_ac) 1);
qed "pre_lemma_gleason9_34";
-Goal "Abs_prat(ratrel``{(y*x,Abs_pnat 1*y)}) = \
-\ Abs_prat(ratrel``{(x,Abs_pnat 1)})";
+Goal "Abs_prat(ratrel``{(y*x,Abs_pnat 1'*y)}) = \
+\ Abs_prat(ratrel``{(x,Abs_pnat 1')})";
by (auto_tac (claset(),
simpset() addsimps [pnat_mult_1,pnat_mult_1_left] @ pnat_mult_ac));
qed "pre_lemma_gleason9_34b";
@@ -760,42 +760,42 @@
(*** of preal type as defined using Dedekind Sections in PReal ***)
(*** Show that exists positive real `one' ***)
-Goal "EX q. q: {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
+Goal "EX q. q: {x::prat. x < prat_of_pnat (Abs_pnat 1')}";
by (fast_tac (claset() addIs [prat_less_qinv_2_1]) 1);
qed "lemma_prat_less_1_memEx";
-Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} ~= {}";
+Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1')} ~= {}";
by (rtac notI 1);
by (cut_facts_tac [lemma_prat_less_1_memEx] 1);
by (Asm_full_simp_tac 1);
qed "lemma_prat_less_1_set_non_empty";
-Goalw [psubset_def] "{} < {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
+Goalw [psubset_def] "{} < {x::prat. x < prat_of_pnat (Abs_pnat 1')}";
by (asm_full_simp_tac (simpset() addsimps
[lemma_prat_less_1_set_non_empty RS not_sym]) 1);
qed "empty_set_psubset_lemma_prat_less_1_set";
(*** exists rational not in set --- prat_of_pnat (Abs_pnat 1) itself ***)
-Goal "EX q. q ~: {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
-by (res_inst_tac [("x","prat_of_pnat (Abs_pnat 1)")] exI 1);
+Goal "EX q. q ~: {x::prat. x < prat_of_pnat (Abs_pnat 1')}";
+by (res_inst_tac [("x","prat_of_pnat (Abs_pnat 1')")] exI 1);
by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
qed "lemma_prat_less_1_not_memEx";
-Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} ~= UNIV";
+Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1')} ~= UNIV";
by (rtac notI 1);
by (cut_facts_tac [lemma_prat_less_1_not_memEx] 1);
by (Asm_full_simp_tac 1);
qed "lemma_prat_less_1_set_not_rat_set";
Goalw [psubset_def,subset_def]
- "{x::prat. x < prat_of_pnat (Abs_pnat 1)} < UNIV";
+ "{x::prat. x < prat_of_pnat (Abs_pnat 1')} < UNIV";
by (asm_full_simp_tac
(simpset() addsimps [lemma_prat_less_1_set_not_rat_set,
lemma_prat_less_1_not_memEx]) 1);
qed "lemma_prat_less_1_set_psubset_rat_set";
(*** prove non_emptiness of type ***)
-Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} : {A. {} < A & \
+Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1')} : {A. {} < A & \
\ A < UNIV & \
\ (!y: A. ((!z. z < y --> z: A) & \
\ (EX u: A. y < u)))}";
--- a/src/HOL/Real/PReal.ML Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/Real/PReal.ML Mon Aug 06 13:43:24 2001 +0200
@@ -30,7 +30,7 @@
Addsimps [empty_not_mem_preal];
-Goalw [preal_def] "{x::prat. x < prat_of_pnat (Abs_pnat 1)} : preal";
+Goalw [preal_def] "{x::prat. x < prat_of_pnat (Abs_pnat 1')} : preal";
by (rtac preal_1 1);
qed "one_set_mem_preal";
@@ -234,9 +234,9 @@
\ ALL z. z < y --> z : {w. EX x:Rep_preal R. EX y:Rep_preal S. w = x + y}";
by Auto_tac;
by (ftac prat_mult_qinv_less_1 1);
-by (forw_inst_tac [("x","x"),("q2.0","prat_of_pnat (Abs_pnat 1)")]
+by (forw_inst_tac [("x","x"),("q2.0","prat_of_pnat (Abs_pnat 1')")]
prat_mult_less2_mono1 1);
-by (forw_inst_tac [("x","ya"),("q2.0","prat_of_pnat (Abs_pnat 1)")]
+by (forw_inst_tac [("x","ya"),("q2.0","prat_of_pnat (Abs_pnat 1')")]
prat_mult_less2_mono1 1);
by (Asm_full_simp_tac 1);
by (REPEAT(dtac (Rep_preal RS prealE_lemma3a) 1));
@@ -367,7 +367,7 @@
(* Positive Real 1 is the multiplicative identity element *)
(* long *)
Goalw [preal_of_prat_def,preal_mult_def]
- "(preal_of_prat (prat_of_pnat (Abs_pnat 1))) * z = z";
+ "(preal_of_prat (prat_of_pnat (Abs_pnat 1'))) * z = z";
by (rtac (Rep_preal_inverse RS subst) 1);
by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
by (rtac (one_set_mem_preal RS Abs_preal_inverse RS ssubst) 1);
@@ -382,7 +382,7 @@
by (auto_tac (claset(),simpset() addsimps [prat_mult_assoc]));
qed "preal_mult_1";
-Goal "z * (preal_of_prat (prat_of_pnat (Abs_pnat 1))) = z";
+Goal "z * (preal_of_prat (prat_of_pnat (Abs_pnat 1'))) = z";
by (rtac (preal_mult_commute RS subst) 1);
by (rtac preal_mult_1 1);
qed "preal_mult_1_right";
@@ -563,7 +563,7 @@
(*more lemmas for inverse *)
Goal "x: Rep_preal(pinv(A)*A) ==> \
-\ x: Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat 1)))";
+\ x: Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat 1')))";
by (auto_tac (claset() addSDs [mem_Rep_preal_multD],
simpset() addsimps [pinv_def,preal_of_prat_def] ));
by (dtac (preal_mem_inv_set RS Abs_preal_inverse RS subst) 1);
@@ -583,8 +583,8 @@
qed "lemma1_gleason9_34";
Goal "Abs_prat (ratrel `` {(y, z)}) < xb + \
-\ Abs_prat (ratrel `` {(x*y, Abs_pnat 1)})*Abs_prat (ratrel `` {(w, x)})";
-by (res_inst_tac [("j","Abs_prat (ratrel `` {(x * y, Abs_pnat 1)}) *\
+\ Abs_prat (ratrel `` {(x*y, Abs_pnat 1')})*Abs_prat (ratrel `` {(w, x)})";
+by (res_inst_tac [("j","Abs_prat (ratrel `` {(x * y, Abs_pnat 1')}) *\
\ Abs_prat (ratrel `` {(w, x)})")] prat_le_less_trans 1);
by (rtac prat_self_less_add_right 2);
by (auto_tac (claset() addIs [lemma_Abs_prat_le3],
@@ -650,14 +650,14 @@
by Auto_tac;
qed "lemma_gleason9_36";
-Goal "prat_of_pnat (Abs_pnat 1) < x ==> \
+Goal "prat_of_pnat (Abs_pnat 1') < x ==> \
\ EX r: Rep_preal(A). r*x ~: Rep_preal(A)";
by (rtac lemma_gleason9_36 1);
by (asm_simp_tac (simpset() addsimps [pnat_one_def]) 1);
qed "lemma_gleason9_36a";
(*** Part 2 of existence of inverse ***)
-Goal "x: Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat 1))) \
+Goal "x: Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat 1'))) \
\ ==> x: Rep_preal(pinv(A)*A)";
by (auto_tac (claset() addSIs [mem_Rep_preal_multI],
simpset() addsimps [pinv_def,preal_of_prat_def] ));
@@ -677,12 +677,12 @@
prat_mult_left_commute]));
qed "preal_mem_mult_invI";
-Goal "pinv(A)*A = (preal_of_prat (prat_of_pnat (Abs_pnat 1)))";
+Goal "pinv(A)*A = (preal_of_prat (prat_of_pnat (Abs_pnat 1')))";
by (rtac (inj_Rep_preal RS injD) 1);
by (fast_tac (claset() addDs [preal_mem_mult_invD,preal_mem_mult_invI]) 1);
qed "preal_mult_inv";
-Goal "A*pinv(A) = (preal_of_prat (prat_of_pnat (Abs_pnat 1)))";
+Goal "A*pinv(A) = (preal_of_prat (prat_of_pnat (Abs_pnat 1')))";
by (rtac (preal_mult_commute RS subst) 1);
by (rtac preal_mult_inv 1);
qed "preal_mult_inv_right";
--- a/src/HOL/Real/RealOrd.ML Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/Real/RealOrd.ML Mon Aug 06 13:43:24 2001 +0200
@@ -269,7 +269,7 @@
symmetric real_one_def]) 1);
qed "real_of_posnat_one";
-Goalw [real_of_posnat_def] "real_of_posnat 1 = 1r + 1r";
+Goalw [real_of_posnat_def] "real_of_posnat 1' = 1r + 1r";
by (simp_tac (simpset() addsimps [real_of_preal_def,real_one_def,
pnat_two_eq,real_add,prat_of_pnat_add RS sym,
preal_of_prat_add RS sym] @ pnat_add_ac) 1);
@@ -306,7 +306,7 @@
by (simp_tac (simpset() addsimps [real_of_posnat_one]) 1);
qed "real_of_nat_zero";
-Goalw [real_of_nat_def] "real (1::nat) = 1r";
+Goalw [real_of_nat_def] "real (1') = 1r";
by (simp_tac (simpset() addsimps [real_of_posnat_two, real_add_assoc]) 1);
qed "real_of_nat_one";
Addsimps [real_of_nat_zero, real_of_nat_one];
--- a/src/HOL/arith_data.ML Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/arith_data.ML Mon Aug 06 13:43:24 2001 +0200
@@ -299,6 +299,7 @@
else poly(s,m,poly(t,ratneg m,pi))
| poly(Const("uminus",_) $ t, m, pi) = poly(t,ratneg m,pi)
| poly(Const("0",_), _, pi) = pi
+ | poly(Const("1",_), m, (p,i)) = (p,ratadd(i,m))
| poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,ratadd(i,m)))
| poly(t as Const("op *",_) $ _ $ _, m, pi as (p,i)) =
(case demult(t,m) of
@@ -363,7 +364,7 @@
(* reduce contradictory <= to False.
Most of the work is done by the cancel tactics.
*)
-val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq];
+val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq,One_def];
val add_mono_thms_nat = map (fn s => prove_goal (the_context ()) s
(fn prems => [cut_facts_tac prems 1,
--- a/src/HOL/ex/Primrec.thy Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/ex/Primrec.thy Mon Aug 06 13:43:24 2001 +0200
@@ -159,7 +159,7 @@
text {* PROPERTY A 8 *}
-lemma ack_1 [simp]: "ack (1, j) = j + #2"
+lemma ack_1 [simp]: "ack (1', j) = j + #2"
apply (induct j)
apply simp_all
done