turned translation for 1::nat into def.
authornipkow
Mon Aug 06 13:43:24 2001 +0200 (2001-08-06)
changeset 11464ddea204de5bc
parent 11463 96b5b27da55c
child 11465 45d156ede468
turned translation for 1::nat into def.
introduced 1' and replaced most occurrences of 1 by 1'.
src/HOL/Datatype_Universe.ML
src/HOL/Divides.ML
src/HOL/Hoare/Examples.ML
src/HOL/IMPP/EvenOdd.ML
src/HOL/Induct/Com.thy
src/HOL/Induct/Mutil.thy
src/HOL/Integ/IntDef.ML
src/HOL/Integ/NatBin.thy
src/HOL/Integ/NatSimprocs.ML
src/HOL/Integ/nat_bin.ML
src/HOL/Isar_examples/Fibonacci.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Primes.thy
src/HOL/Nat.ML
src/HOL/NatDef.ML
src/HOL/NatDef.thy
src/HOL/Power.ML
src/HOL/Real/PNat.ML
src/HOL/Real/PNat.thy
src/HOL/Real/PRat.ML
src/HOL/Real/PReal.ML
src/HOL/Real/RealOrd.ML
src/HOL/arith_data.ML
src/HOL/ex/Primrec.thy
     1.1 --- a/src/HOL/Datatype_Universe.ML	Mon Aug 06 13:12:06 2001 +0200
     1.2 +++ b/src/HOL/Datatype_Universe.ML	Mon Aug 06 13:43:24 2001 +0200
     1.3 @@ -80,7 +80,8 @@
     1.4  
     1.5  (** Scons vs Atom **)
     1.6  
     1.7 -Goalw [Atom_def,Scons_def,Push_Node_def] "Scons M N ~= Atom(a)";
     1.8 +Goalw [Atom_def,Scons_def,Push_Node_def,One_def]
     1.9 + "Scons M N ~= Atom(a)";
    1.10  by (rtac notI 1);
    1.11  by (etac (equalityD2 RS subsetD RS UnE) 1);
    1.12  by (rtac singletonI 1);
    1.13 @@ -140,11 +141,11 @@
    1.14  
    1.15  (** Injectiveness of Scons **)
    1.16  
    1.17 -Goalw [Scons_def] "Scons M N <= Scons M' N' ==> M<=M'";
    1.18 +Goalw [Scons_def,One_def] "Scons M N <= Scons M' N' ==> M<=M'";
    1.19  by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
    1.20  qed "Scons_inject_lemma1";
    1.21  
    1.22 -Goalw [Scons_def] "Scons M N <= Scons M' N' ==> N<=N'";
    1.23 +Goalw [Scons_def,One_def] "Scons M N <= Scons M' N' ==> N<=N'";
    1.24  by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
    1.25  qed "Scons_inject_lemma2";
    1.26  
    1.27 @@ -251,7 +252,7 @@
    1.28  by (rtac ntrunc_Atom 1);
    1.29  qed "ntrunc_Numb";
    1.30  
    1.31 -Goalw [Scons_def,ntrunc_def]
    1.32 +Goalw [Scons_def,ntrunc_def,One_def]
    1.33      "ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)";
    1.34  by (safe_tac (claset() addSIs [imageI]));
    1.35  by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3));
    1.36 @@ -265,7 +266,7 @@
    1.37  
    1.38  (** Injection nodes **)
    1.39  
    1.40 -Goalw [In0_def] "ntrunc 1 (In0 M) = {}";
    1.41 +Goalw [In0_def] "ntrunc 1' (In0 M) = {}";
    1.42  by (Simp_tac 1);
    1.43  by (rewtac Scons_def);
    1.44  by (Blast_tac 1);
    1.45 @@ -276,7 +277,7 @@
    1.46  by (Simp_tac 1);
    1.47  qed "ntrunc_In0";
    1.48  
    1.49 -Goalw [In1_def] "ntrunc 1 (In1 M) = {}";
    1.50 +Goalw [In1_def] "ntrunc 1' (In1 M) = {}";
    1.51  by (Simp_tac 1);
    1.52  by (rewtac Scons_def);
    1.53  by (Blast_tac 1);
    1.54 @@ -338,7 +339,7 @@
    1.55  
    1.56  (** Injection **)
    1.57  
    1.58 -Goalw [In0_def,In1_def] "In0(M) ~= In1(N)";
    1.59 +Goalw [In0_def,In1_def,One_def] "In0(M) ~= In1(N)";
    1.60  by (rtac notI 1);
    1.61  by (etac (Scons_inject1 RS Numb_inject RS Zero_neq_Suc) 1);
    1.62  qed "In0_not_In1";
     2.1 --- a/src/HOL/Divides.ML	Mon Aug 06 13:12:06 2001 +0200
     2.2 +++ b/src/HOL/Divides.ML	Mon Aug 06 13:43:24 2001 +0200
     2.3 @@ -65,7 +65,7 @@
     2.4  by (asm_simp_tac (simpset() addsimps [mod_geq]) 1);
     2.5  qed "mod_if";
     2.6  
     2.7 -Goal "m mod 1 = (0::nat)";
     2.8 +Goal "m mod 1' = 0";
     2.9  by (induct_tac "m" 1);
    2.10  by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_geq])));
    2.11  qed "mod_1";
    2.12 @@ -387,7 +387,7 @@
    2.13  
    2.14  (*** Further facts about div and mod ***)
    2.15  
    2.16 -Goal "m div 1 = m";
    2.17 +Goal "m div 1' = m";
    2.18  by (induct_tac "m" 1);
    2.19  by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_geq])));
    2.20  qed "div_1";
    2.21 @@ -527,12 +527,12 @@
    2.22  qed "dvd_0_left_iff";
    2.23  AddIffs [dvd_0_left_iff];
    2.24  
    2.25 -Goalw [dvd_def] "1 dvd (k::nat)";
    2.26 +Goalw [dvd_def] "1' dvd k";
    2.27  by (Simp_tac 1);
    2.28  qed "dvd_1_left";
    2.29  AddIffs [dvd_1_left];
    2.30  
    2.31 -Goal "(m dvd 1) = (m = 1)";
    2.32 +Goal "(m dvd 1') = (m = 1')";
    2.33  by (simp_tac (simpset() addsimps [dvd_def]) 1); 
    2.34  qed "dvd_1_iff_1";
    2.35  Addsimps [dvd_1_iff_1];
     3.1 --- a/src/HOL/Hoare/Examples.ML	Mon Aug 06 13:12:06 2001 +0200
     3.2 +++ b/src/HOL/Hoare/Examples.ML	Mon Aug 06 13:43:24 2001 +0200
     3.3 @@ -175,7 +175,7 @@
     3.4  Ambiguity warnings of parser are due to := being used
     3.5  both for assignment and list update.
     3.6  *)
     3.7 -Goal "m - 1 < n ==> m < Suc n";
     3.8 +Goal "m - 1' < n ==> m < Suc n";
     3.9  by (arith_tac 1);
    3.10  qed "lemma";
    3.11  
    3.12 @@ -184,7 +184,7 @@
    3.13  \   geq == %A i. !k. i<k & k<length A --> pivot <= A!k |] ==> \
    3.14  \ |- VARS A u l.\
    3.15  \ {0 < length(A::('a::order)list)} \
    3.16 -\ l := 0; u := length A - 1; \
    3.17 +\ l := 0; u := length A - 1'; \
    3.18  \ WHILE l <= u \
    3.19  \  INV {leq A l & geq A u & u<length A & l<=length A} \
    3.20  \  DO WHILE l < length A & A!l <= pivot \
     4.1 --- a/src/HOL/IMPP/EvenOdd.ML	Mon Aug 06 13:12:06 2001 +0200
     4.2 +++ b/src/HOL/IMPP/EvenOdd.ML	Mon Aug 06 13:43:24 2001 +0200
     4.3 @@ -11,7 +11,7 @@
     4.4  qed "even_0";
     4.5  Addsimps [even_0];
     4.6  
     4.7 -Goalw [even_def] "even 1 = False";
     4.8 +Goalw [even_def] "even 1' = False";
     4.9  by (Simp_tac 1);
    4.10  qed "not_even_1";
    4.11  Addsimps [not_even_1];
    4.12 @@ -50,7 +50,7 @@
    4.13  
    4.14  section "verification";
    4.15  
    4.16 -Goalw [odd_def] "{{Z=Arg+0}. BODY Even .{Res_ok}}|-{Z=Arg+1}. odd .{Res_ok}";
    4.17 +Goalw [odd_def] "{{Z=Arg+0}. BODY Even .{Res_ok}}|-{Z=Arg+1'}. odd .{Res_ok}";
    4.18  by (rtac hoare_derivs.If 1);
    4.19  by (rtac (hoare_derivs.Ass RS conseq1) 1);
    4.20  by  (clarsimp_tac Arg_Res_css 1);
     5.1 --- a/src/HOL/Induct/Com.thy	Mon Aug 06 13:12:06 2001 +0200
     5.2 +++ b/src/HOL/Induct/Com.thy	Mon Aug 06 13:43:24 2001 +0200
     5.3 @@ -52,10 +52,10 @@
     5.4      IfTrue "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |] 
     5.5              ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
     5.6  
     5.7 -    IfFalse "[| (e,s) -|[eval]->  (1,s');  (c1,s') -[eval]-> s1 |] 
     5.8 +    IfFalse "[| (e,s) -|[eval]->  (1',s');  (c1,s') -[eval]-> s1 |] 
     5.9               ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
    5.10  
    5.11 -    WhileFalse "(e,s) -|[eval]-> (1,s1) ==> (WHILE e DO c, s) -[eval]-> s1"
    5.12 +    WhileFalse "(e,s) -|[eval]-> (1',s1) ==> (WHILE e DO c, s) -[eval]-> s1"
    5.13  
    5.14      WhileTrue  "[| (e,s) -|[eval]-> (0,s1);
    5.15                  (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |] 
     6.1 --- a/src/HOL/Induct/Mutil.thy	Mon Aug 06 13:12:06 2001 +0200
     6.2 +++ b/src/HOL/Induct/Mutil.thy	Mon Aug 06 13:43:24 2001 +0200
     6.3 @@ -110,7 +110,7 @@
     6.4    Diff_Int_distrib [simp]
     6.5  
     6.6  lemma tiling_domino_0_1:
     6.7 -  "t \<in> tiling domino ==> card (coloured 0 \<inter> t) = card (coloured 1 \<inter> t)"
     6.8 +  "t \<in> tiling domino ==> card (coloured 0 \<inter> t) = card (coloured 1' \<inter> t)"
     6.9    apply (erule tiling.induct)
    6.10     apply (drule_tac [2] domino_singletons)
    6.11     apply auto
    6.12 @@ -131,7 +131,7 @@
    6.13    apply (rule notI)
    6.14    apply (subgoal_tac
    6.15      "card (coloured 0 \<inter> (t - {(i, j)} - {(m, n)})) <
    6.16 -      card (coloured 1 \<inter> (t - {(i, j)} - {(m, n)}))")
    6.17 +      card (coloured 1' \<inter> (t - {(i, j)} - {(m, n)}))")
    6.18     apply (force simp only: tiling_domino_0_1)
    6.19    apply (simp add: tiling_domino_0_1 [symmetric])
    6.20    apply (simp add: coloured_def card_Diff2_less)
     7.1 --- a/src/HOL/Integ/IntDef.ML	Mon Aug 06 13:12:06 2001 +0200
     7.2 +++ b/src/HOL/Integ/IntDef.ML	Mon Aug 06 13:43:24 2001 +0200
     7.3 @@ -326,7 +326,7 @@
     7.4  by (asm_simp_tac (simpset() addsimps [zmult]) 1);
     7.5  qed "zmult_int0";
     7.6  
     7.7 -Goalw [int_def] "int 1 * z = z";
     7.8 +Goalw [int_def] "int 1' * z = z";
     7.9  by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
    7.10  by (asm_simp_tac (simpset() addsimps [zmult]) 1);
    7.11  qed "zmult_int1";
    7.12 @@ -335,7 +335,7 @@
    7.13  by (rtac ([zmult_commute, zmult_int0] MRS trans) 1);
    7.14  qed "zmult_int0_right";
    7.15  
    7.16 -Goal "z * int 1 = z";
    7.17 +Goal "z * int 1' = z";
    7.18  by (rtac ([zmult_commute, zmult_int1] MRS trans) 1);
    7.19  qed "zmult_int1_right";
    7.20  
     8.1 --- a/src/HOL/Integ/NatBin.thy	Mon Aug 06 13:12:06 2001 +0200
     8.2 +++ b/src/HOL/Integ/NatBin.thy	Mon Aug 06 13:43:24 2001 +0200
     8.3 @@ -18,6 +18,10 @@
     8.4      "number_of v == nat (number_of v)"
     8.5       (*::bin=>nat        ::bin=>int*)
     8.6  
     8.7 +axioms
     8.8 +neg_number_of_bin_pred_iff_0:
     8.9 +  "neg (number_of (bin_pred v)) = (number_of v = (0::nat))"
    8.10 +
    8.11  use "nat_bin.ML"	setup nat_bin_arith_setup
    8.12  
    8.13  end
     9.1 --- a/src/HOL/Integ/NatSimprocs.ML	Mon Aug 06 13:12:06 2001 +0200
     9.2 +++ b/src/HOL/Integ/NatSimprocs.ML	Mon Aug 06 13:43:24 2001 +0200
     9.3 @@ -14,13 +14,15 @@
     9.4  
     9.5  (*Now just instantiating n to (number_of v) does the right simplification,
     9.6    but with some redundant inequality tests.*)
     9.7 -
     9.8 +(*
     9.9  Goal "neg (number_of (bin_pred v)) = (number_of v = (0::nat))";
    9.10  by (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < 1)" 1);
    9.11  by (Asm_simp_tac 1);
    9.12  by (stac less_number_of_Suc 1);
    9.13  by (Simp_tac 1);
    9.14  qed "neg_number_of_bin_pred_iff_0";
    9.15 +*)
    9.16 +val neg_number_of_bin_pred_iff_0 = thm "neg_number_of_bin_pred_iff_0";
    9.17  
    9.18  Goal "neg (number_of (bin_minus v)) ==> \
    9.19  \     Suc m - (number_of v) = m - (number_of (bin_pred v))";
    10.1 --- a/src/HOL/Integ/nat_bin.ML	Mon Aug 06 13:12:06 2001 +0200
    10.2 +++ b/src/HOL/Integ/nat_bin.ML	Mon Aug 06 13:43:24 2001 +0200
    10.3 @@ -495,7 +495,7 @@
    10.4  by Auto_tac;
    10.5  val lemma1 = result();
    10.6  
    10.7 -Goal "m+m ~= int 1 + n + n";
    10.8 +Goal "m+m ~= int 1' + n + n";
    10.9  by Auto_tac;
   10.10  by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1);
   10.11  by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
    11.1 --- a/src/HOL/Isar_examples/Fibonacci.thy	Mon Aug 06 13:12:06 2001 +0200
    11.2 +++ b/src/HOL/Isar_examples/Fibonacci.thy	Mon Aug 06 13:43:24 2001 +0200
    11.3 @@ -29,7 +29,7 @@
    11.4  consts fib :: "nat => nat"
    11.5  recdef fib less_than
    11.6   "fib 0 = 0"
    11.7 - "fib 1 = 1"
    11.8 + "fib 1' = 1"
    11.9   "fib (Suc (Suc x)) = fib x + fib (Suc x)"
   11.10  
   11.11  lemma [simp]: "0 < fib (Suc n)"
    12.1 --- a/src/HOL/Library/Multiset.thy	Mon Aug 06 13:12:06 2001 +0200
    12.2 +++ b/src/HOL/Library/Multiset.thy	Mon Aug 06 13:43:24 2001 +0200
    12.3 @@ -16,7 +16,7 @@
    12.4  
    12.5  typedef 'a multiset = "{f::'a => nat. finite {x . 0 < f x}}"
    12.6  proof
    12.7 -  show "(\\<lambda>x. 0::nat) \\<in> ?multiset" by simp
    12.8 +  show "(\<lambda>x. 0::nat) \<in> ?multiset" by simp
    12.9  qed
   12.10  
   12.11  lemmas multiset_typedef [simp] =
   12.12 @@ -25,23 +25,23 @@
   12.13  
   12.14  constdefs
   12.15    Mempty :: "'a multiset"    ("{#}")
   12.16 -  "{#} == Abs_multiset (\\<lambda>a. 0)"
   12.17 +  "{#} == Abs_multiset (\<lambda>a. 0)"
   12.18  
   12.19    single :: "'a => 'a multiset"    ("{#_#}")
   12.20 -  "{#a#} == Abs_multiset (\\<lambda>b. if b = a then 1 else 0)"
   12.21 +  "{#a#} == Abs_multiset (\<lambda>b. if b = a then 1' else 0)"
   12.22  
   12.23    count :: "'a multiset => 'a => nat"
   12.24    "count == Rep_multiset"
   12.25  
   12.26    MCollect :: "'a multiset => ('a => bool) => 'a multiset"
   12.27 -  "MCollect M P == Abs_multiset (\\<lambda>x. if P x then Rep_multiset M x else 0)"
   12.28 +  "MCollect M P == Abs_multiset (\<lambda>x. if P x then Rep_multiset M x else 0)"
   12.29  
   12.30  syntax
   12.31    "_Melem" :: "'a => 'a multiset => bool"    ("(_/ :# _)" [50, 51] 50)
   12.32    "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset"    ("(1{# _ : _./ _#})")
   12.33  translations
   12.34    "a :# M" == "0 < count M a"
   12.35 -  "{#x:M. P#}" == "MCollect M (\\<lambda>x. P)"
   12.36 +  "{#x:M. P#}" == "MCollect M (\<lambda>x. P)"
   12.37  
   12.38  constdefs
   12.39    set_of :: "'a multiset => 'a set"
   12.40 @@ -52,8 +52,8 @@
   12.41  instance multiset :: ("term") zero ..
   12.42  
   12.43  defs (overloaded)
   12.44 -  union_def: "M + N == Abs_multiset (\\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
   12.45 -  diff_def: "M - N == Abs_multiset (\\<lambda>a. Rep_multiset M a - Rep_multiset N a)"
   12.46 +  union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
   12.47 +  diff_def: "M - N == Abs_multiset (\<lambda>a. Rep_multiset M a - Rep_multiset N a)"
   12.48    Zero_def [simp]: "0 == {#}"
   12.49    size_def: "size M == setsum (count M) (set_of M)"
   12.50  
   12.51 @@ -62,16 +62,16 @@
   12.52   \medskip Preservation of the representing set @{term multiset}.
   12.53  *}
   12.54  
   12.55 -lemma const0_in_multiset [simp]: "(\\<lambda>a. 0) \\<in> multiset"
   12.56 +lemma const0_in_multiset [simp]: "(\<lambda>a. 0) \<in> multiset"
   12.57    apply (simp add: multiset_def)
   12.58    done
   12.59  
   12.60 -lemma only1_in_multiset [simp]: "(\\<lambda>b. if b = a then 1 else 0) \\<in> multiset"
   12.61 +lemma only1_in_multiset [simp]: "(\<lambda>b. if b = a then 1' else 0) \<in> multiset"
   12.62    apply (simp add: multiset_def)
   12.63    done
   12.64  
   12.65  lemma union_preserves_multiset [simp]:
   12.66 -    "M \\<in> multiset ==> N \\<in> multiset ==> (\\<lambda>a. M a + N a) \\<in> multiset"
   12.67 +    "M \<in> multiset ==> N \<in> multiset ==> (\<lambda>a. M a + N a) \<in> multiset"
   12.68    apply (unfold multiset_def)
   12.69    apply simp
   12.70    apply (drule finite_UnI)
   12.71 @@ -80,7 +80,7 @@
   12.72    done
   12.73  
   12.74  lemma diff_preserves_multiset [simp]:
   12.75 -    "M \\<in> multiset ==> (\\<lambda>a. M a - N a) \\<in> multiset"
   12.76 +    "M \<in> multiset ==> (\<lambda>a. M a - N a) \<in> multiset"
   12.77    apply (unfold multiset_def)
   12.78    apply simp
   12.79    apply (rule finite_subset)
   12.80 @@ -94,7 +94,7 @@
   12.81  
   12.82  subsubsection {* Union *}
   12.83  
   12.84 -theorem union_empty [simp]: "M + {#} = M \\<and> {#} + M = M"
   12.85 +theorem union_empty [simp]: "M + {#} = M \<and> {#} + M = M"
   12.86    apply (simp add: union_def Mempty_def)
   12.87    done
   12.88  
   12.89 @@ -124,7 +124,7 @@
   12.90  
   12.91  subsubsection {* Difference *}
   12.92  
   12.93 -theorem diff_empty [simp]: "M - {#} = M \\<and> {#} - M = {#}"
   12.94 +theorem diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
   12.95    apply (simp add: Mempty_def diff_def)
   12.96    done
   12.97  
   12.98 @@ -139,7 +139,7 @@
   12.99    apply (simp add: count_def Mempty_def)
  12.100    done
  12.101  
  12.102 -theorem count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)"
  12.103 +theorem count_single [simp]: "count {#b#} a = (if b = a then 1' else 0)"
  12.104    apply (simp add: count_def single_def)
  12.105    done
  12.106  
  12.107 @@ -162,7 +162,7 @@
  12.108    apply (simp add: set_of_def)
  12.109    done
  12.110  
  12.111 -theorem set_of_union [simp]: "set_of (M + N) = set_of M \\<union> set_of N"
  12.112 +theorem set_of_union [simp]: "set_of (M + N) = set_of M \<union> set_of N"
  12.113    apply (auto simp add: set_of_def)
  12.114    done
  12.115  
  12.116 @@ -170,7 +170,7 @@
  12.117    apply (auto simp add: set_of_def Mempty_def count_def expand_fun_eq)
  12.118    done
  12.119  
  12.120 -theorem mem_set_of_iff [simp]: "(x \\<in> set_of M) = (x :# M)"
  12.121 +theorem mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)"
  12.122    apply (auto simp add: set_of_def)
  12.123    done
  12.124  
  12.125 @@ -191,7 +191,7 @@
  12.126    done
  12.127  
  12.128  theorem setsum_count_Int:
  12.129 -    "finite A ==> setsum (count N) (A \\<inter> set_of N) = setsum (count N) A"
  12.130 +    "finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A"
  12.131    apply (erule finite_induct)
  12.132     apply simp
  12.133    apply (simp add: Int_insert_left set_of_def)
  12.134 @@ -199,7 +199,7 @@
  12.135  
  12.136  theorem size_union [simp]: "size (M + N::'a multiset) = size M + size N"
  12.137    apply (unfold size_def)
  12.138 -  apply (subgoal_tac "count (M + N) = (\\<lambda>a. count M a + count N a)")
  12.139 +  apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)")
  12.140     prefer 2
  12.141     apply (rule ext)
  12.142     apply simp
  12.143 @@ -214,7 +214,7 @@
  12.144    apply (simp add: set_of_def count_def expand_fun_eq)
  12.145    done
  12.146  
  12.147 -theorem size_eq_Suc_imp_elem: "size M = Suc n ==> \\<exists>a. a :# M"
  12.148 +theorem size_eq_Suc_imp_elem: "size M = Suc n ==> \<exists>a. a :# M"
  12.149    apply (unfold size_def)
  12.150    apply (drule setsum_SucD)
  12.151    apply auto
  12.152 @@ -223,11 +223,11 @@
  12.153  
  12.154  subsubsection {* Equality of multisets *}
  12.155  
  12.156 -theorem multiset_eq_conv_count_eq: "(M = N) = (\\<forall>a. count M a = count N a)"
  12.157 +theorem multiset_eq_conv_count_eq: "(M = N) = (\<forall>a. count M a = count N a)"
  12.158    apply (simp add: count_def expand_fun_eq)
  12.159    done
  12.160  
  12.161 -theorem single_not_empty [simp]: "{#a#} \\<noteq> {#} \\<and> {#} \\<noteq> {#a#}"
  12.162 +theorem single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
  12.163    apply (simp add: single_def Mempty_def expand_fun_eq)
  12.164    done
  12.165  
  12.166 @@ -235,11 +235,11 @@
  12.167    apply (auto simp add: single_def expand_fun_eq)
  12.168    done
  12.169  
  12.170 -theorem union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \\<and> N = {#})"
  12.171 +theorem union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \<and> N = {#})"
  12.172    apply (auto simp add: union_def Mempty_def expand_fun_eq)
  12.173    done
  12.174  
  12.175 -theorem empty_eq_union [iff]: "({#} = M + N) = (M = {#} \\<and> N = {#})"
  12.176 +theorem empty_eq_union [iff]: "({#} = M + N) = (M = {#} \<and> N = {#})"
  12.177    apply (auto simp add: union_def Mempty_def expand_fun_eq)
  12.178    done
  12.179  
  12.180 @@ -252,7 +252,7 @@
  12.181    done
  12.182  
  12.183  theorem union_is_single:
  12.184 -    "(M + N = {#a#}) = (M = {#a#} \\<and> N={#} \\<or> M = {#} \\<and> N = {#a#})"
  12.185 +    "(M + N = {#a#}) = (M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#})"
  12.186    apply (unfold Mempty_def single_def union_def)
  12.187    apply (simp add: add_is_1 expand_fun_eq)
  12.188    apply blast
  12.189 @@ -260,16 +260,16 @@
  12.190  
  12.191  theorem single_is_union:
  12.192    "({#a#} = M + N) =
  12.193 -    ({#a#} = M \\<and> N = {#} \\<or> M = {#} \\<and> {#a#} = N)"
  12.194 +    ({#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N)"
  12.195    apply (unfold Mempty_def single_def union_def)
  12.196 -  apply (simp add: add_is_1 expand_fun_eq)
  12.197 +  apply (simp add: add_is_1 one_is_add expand_fun_eq)
  12.198    apply (blast dest: sym)
  12.199    done
  12.200  
  12.201  theorem add_eq_conv_diff:
  12.202    "(M + {#a#} = N + {#b#}) =
  12.203 -    (M = N \\<and> a = b \\<or>
  12.204 -      M = N - {#a#} + {#b#} \\<and> N = M - {#b#} + {#a#})"
  12.205 +    (M = N \<and> a = b \<or>
  12.206 +      M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#})"
  12.207    apply (unfold single_def union_def diff_def)
  12.208    apply (simp (no_asm) add: expand_fun_eq)
  12.209    apply (rule conjI)
  12.210 @@ -291,7 +291,7 @@
  12.211  (*
  12.212  val prems = Goal
  12.213   "[| !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> finite F --> P F";
  12.214 -by (res_inst_tac [("a","F"),("f","\\<lambda>A. if finite A then card A else 0")]
  12.215 +by (res_inst_tac [("a","F"),("f","\<lambda>A. if finite A then card A else 0")]
  12.216       measure_induct 1);
  12.217  by (Clarify_tac 1);
  12.218  by (resolve_tac prems 1);
  12.219 @@ -320,7 +320,7 @@
  12.220  
  12.221  lemma setsum_decr:
  12.222    "finite F ==> 0 < f a ==>
  12.223 -    setsum (f (a := f a - 1)) F = (if a \\<in> F then setsum f F - 1 else setsum f F)"
  12.224 +    setsum (f (a := f a - 1')) F = (if a \<in> F then setsum f F - 1 else setsum f F)"
  12.225    apply (erule finite_induct)
  12.226     apply auto
  12.227    apply (drule_tac a = a in mk_disjoint_insert)
  12.228 @@ -328,8 +328,8 @@
  12.229    done
  12.230  
  12.231  lemma rep_multiset_induct_aux:
  12.232 -  "P (\\<lambda>a. 0) ==> (!!f b. f \\<in> multiset ==> P f ==> P (f (b := f b + 1)))
  12.233 -    ==> \\<forall>f. f \\<in> multiset --> setsum f {x. 0 < f x} = n --> P f"
  12.234 +  "P (\<lambda>a. 0) ==> (!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1')))
  12.235 +    ==> \<forall>f. f \<in> multiset --> setsum f {x. 0 < f x} = n --> P f"
  12.236  proof -
  12.237    case antecedent
  12.238    note prems = this [unfolded multiset_def]
  12.239 @@ -338,7 +338,7 @@
  12.240      apply (induct_tac n)
  12.241       apply simp
  12.242       apply clarify
  12.243 -     apply (subgoal_tac "f = (\\<lambda>a.0)")
  12.244 +     apply (subgoal_tac "f = (\<lambda>a.0)")
  12.245        apply simp
  12.246        apply (rule prems)
  12.247       apply (rule ext)
  12.248 @@ -347,14 +347,14 @@
  12.249      apply (frule setsum_SucD)
  12.250      apply clarify
  12.251      apply (rename_tac a)
  12.252 -    apply (subgoal_tac "finite {x. 0 < (f (a := f a - 1)) x}")
  12.253 +    apply (subgoal_tac "finite {x. 0 < (f (a := f a - 1')) x}")
  12.254       prefer 2
  12.255       apply (rule finite_subset)
  12.256        prefer 2
  12.257        apply assumption
  12.258       apply simp
  12.259       apply blast
  12.260 -    apply (subgoal_tac "f = (f (a := f a - 1))(a := (f (a := f a - 1)) a + 1)")
  12.261 +    apply (subgoal_tac "f = (f (a := f a - 1'))(a := (f (a := f a - 1')) a + 1')")
  12.262       prefer 2
  12.263       apply (rule ext)
  12.264       apply (simp (no_asm_simp))
  12.265 @@ -363,10 +363,10 @@
  12.266      apply (erule allE, erule impE, erule_tac [2] mp)
  12.267       apply blast
  12.268      apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply)
  12.269 -    apply (subgoal_tac "{x. x \\<noteq> a --> 0 < f x} = {x. 0 < f x}")
  12.270 +    apply (subgoal_tac "{x. x \<noteq> a --> 0 < f x} = {x. 0 < f x}")
  12.271       prefer 2
  12.272       apply blast
  12.273 -    apply (subgoal_tac "{x. x \\<noteq> a \\<and> 0 < f x} = {x. 0 < f x} - {a}")
  12.274 +    apply (subgoal_tac "{x. x \<noteq> a \<and> 0 < f x} = {x. 0 < f x} - {a}")
  12.275       prefer 2
  12.276       apply blast
  12.277      apply (simp add: le_imp_diff_is_add setsum_diff1 cong: conj_cong)
  12.278 @@ -374,8 +374,8 @@
  12.279  qed
  12.280  
  12.281  theorem rep_multiset_induct:
  12.282 -  "f \\<in> multiset ==> P (\\<lambda>a. 0) ==>
  12.283 -    (!!f b. f \\<in> multiset ==> P f ==> P (f (b := f b + 1))) ==> P f"
  12.284 +  "f \<in> multiset ==> P (\<lambda>a. 0) ==>
  12.285 +    (!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1'))) ==> P f"
  12.286    apply (insert rep_multiset_induct_aux)
  12.287    apply blast
  12.288    done
  12.289 @@ -390,7 +390,7 @@
  12.290      apply (rule Rep_multiset_inverse [THEN subst])
  12.291      apply (rule Rep_multiset [THEN rep_multiset_induct])
  12.292       apply (rule prem1)
  12.293 -    apply (subgoal_tac "f (b := f b + 1) = (\\<lambda>a. f a + (if a = b then 1 else 0))")
  12.294 +    apply (subgoal_tac "f (b := f b + 1') = (\<lambda>a. f a + (if a = b then 1' else 0))")
  12.295       prefer 2
  12.296       apply (simp add: expand_fun_eq)
  12.297      apply (erule ssubst)
  12.298 @@ -401,7 +401,7 @@
  12.299  
  12.300  
  12.301  lemma MCollect_preserves_multiset:
  12.302 -    "M \\<in> multiset ==> (\\<lambda>x. if P x then M x else 0) \\<in> multiset"
  12.303 +    "M \<in> multiset ==> (\<lambda>x. if P x then M x else 0) \<in> multiset"
  12.304    apply (simp add: multiset_def)
  12.305    apply (rule finite_subset)
  12.306     apply auto
  12.307 @@ -413,11 +413,11 @@
  12.308    apply (simp add: MCollect_preserves_multiset)
  12.309    done
  12.310  
  12.311 -theorem set_of_MCollect [simp]: "set_of {# x:M. P x #} = set_of M \\<inter> {x. P x}"
  12.312 +theorem set_of_MCollect [simp]: "set_of {# x:M. P x #} = set_of M \<inter> {x. P x}"
  12.313    apply (auto simp add: set_of_def)
  12.314    done
  12.315  
  12.316 -theorem multiset_partition: "M = {# x:M. P x #} + {# x:M. \\<not> P x #}"
  12.317 +theorem multiset_partition: "M = {# x:M. P x #} + {# x:M. \<not> P x #}"
  12.318    apply (subst multiset_eq_conv_count_eq)
  12.319    apply auto
  12.320    done
  12.321 @@ -427,7 +427,7 @@
  12.322  
  12.323  theorem add_eq_conv_ex:
  12.324    "(M + {#a#} = N + {#b#}) =
  12.325 -    (M = N \\<and> a = b \\<or> (\\<exists>K. M = K + {#b#} \\<and> N = K + {#a#}))"
  12.326 +    (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))"
  12.327    apply (auto simp add: add_eq_conv_diff)
  12.328    done
  12.329  
  12.330 @@ -437,41 +437,41 @@
  12.331  subsubsection {* Well-foundedness *}
  12.332  
  12.333  constdefs
  12.334 -  mult1 :: "('a \\<times> 'a) set => ('a multiset \\<times> 'a multiset) set"
  12.335 +  mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set"
  12.336    "mult1 r ==
  12.337 -    {(N, M). \\<exists>a M0 K. M = M0 + {#a#} \\<and> N = M0 + K \\<and>
  12.338 -      (\\<forall>b. b :# K --> (b, a) \\<in> r)}"
  12.339 +    {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
  12.340 +      (\<forall>b. b :# K --> (b, a) \<in> r)}"
  12.341  
  12.342 -  mult :: "('a \\<times> 'a) set => ('a multiset \\<times> 'a multiset) set"
  12.343 +  mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set"
  12.344    "mult r == (mult1 r)\<^sup>+"
  12.345  
  12.346 -lemma not_less_empty [iff]: "(M, {#}) \\<notin> mult1 r"
  12.347 +lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
  12.348    by (simp add: mult1_def)
  12.349  
  12.350 -lemma less_add: "(N, M0 + {#a#}) \\<in> mult1 r ==>
  12.351 -    (\\<exists>M. (M, M0) \\<in> mult1 r \\<and> N = M + {#a#}) \\<or>
  12.352 -    (\\<exists>K. (\\<forall>b. b :# K --> (b, a) \\<in> r) \\<and> N = M0 + K)"
  12.353 -  (concl is "?case1 (mult1 r) \\<or> ?case2")
  12.354 +lemma less_add: "(N, M0 + {#a#}) \<in> mult1 r ==>
  12.355 +    (\<exists>M. (M, M0) \<in> mult1 r \<and> N = M + {#a#}) \<or>
  12.356 +    (\<exists>K. (\<forall>b. b :# K --> (b, a) \<in> r) \<and> N = M0 + K)"
  12.357 +  (concl is "?case1 (mult1 r) \<or> ?case2")
  12.358  proof (unfold mult1_def)
  12.359 -  let ?r = "\\<lambda>K a. \\<forall>b. b :# K --> (b, a) \\<in> r"
  12.360 -  let ?R = "\\<lambda>N M. \\<exists>a M0 K. M = M0 + {#a#} \\<and> N = M0 + K \\<and> ?r K a"
  12.361 +  let ?r = "\<lambda>K a. \<forall>b. b :# K --> (b, a) \<in> r"
  12.362 +  let ?R = "\<lambda>N M. \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and> ?r K a"
  12.363    let ?case1 = "?case1 {(N, M). ?R N M}"
  12.364  
  12.365 -  assume "(N, M0 + {#a#}) \\<in> {(N, M). ?R N M}"
  12.366 -  hence "\\<exists>a' M0' K.
  12.367 -      M0 + {#a#} = M0' + {#a'#} \\<and> N = M0' + K \\<and> ?r K a'" by simp
  12.368 -  thus "?case1 \\<or> ?case2"
  12.369 +  assume "(N, M0 + {#a#}) \<in> {(N, M). ?R N M}"
  12.370 +  hence "\<exists>a' M0' K.
  12.371 +      M0 + {#a#} = M0' + {#a'#} \<and> N = M0' + K \<and> ?r K a'" by simp
  12.372 +  thus "?case1 \<or> ?case2"
  12.373    proof (elim exE conjE)
  12.374      fix a' M0' K
  12.375      assume N: "N = M0' + K" and r: "?r K a'"
  12.376      assume "M0 + {#a#} = M0' + {#a'#}"
  12.377 -    hence "M0 = M0' \\<and> a = a' \\<or>
  12.378 -        (\\<exists>K'. M0 = K' + {#a'#} \\<and> M0' = K' + {#a#})"
  12.379 +    hence "M0 = M0' \<and> a = a' \<or>
  12.380 +        (\<exists>K'. M0 = K' + {#a'#} \<and> M0' = K' + {#a#})"
  12.381        by (simp only: add_eq_conv_ex)
  12.382      thus ?thesis
  12.383      proof (elim disjE conjE exE)
  12.384        assume "M0 = M0'" "a = a'"
  12.385 -      with N r have "?r K a \\<and> N = M0 + K" by simp
  12.386 +      with N r have "?r K a \<and> N = M0 + K" by simp
  12.387        hence ?case2 .. thus ?thesis ..
  12.388      next
  12.389        fix K'
  12.390 @@ -485,78 +485,78 @@
  12.391    qed
  12.392  qed
  12.393  
  12.394 -lemma all_accessible: "wf r ==> \\<forall>M. M \\<in> acc (mult1 r)"
  12.395 +lemma all_accessible: "wf r ==> \<forall>M. M \<in> acc (mult1 r)"
  12.396  proof
  12.397    let ?R = "mult1 r"
  12.398    let ?W = "acc ?R"
  12.399    {
  12.400      fix M M0 a
  12.401 -    assume M0: "M0 \\<in> ?W"
  12.402 -      and wf_hyp: "\\<forall>b. (b, a) \\<in> r --> (\\<forall>M \\<in> ?W. M + {#b#} \\<in> ?W)"
  12.403 -      and acc_hyp: "\\<forall>M. (M, M0) \\<in> ?R --> M + {#a#} \\<in> ?W"
  12.404 -    have "M0 + {#a#} \\<in> ?W"
  12.405 +    assume M0: "M0 \<in> ?W"
  12.406 +      and wf_hyp: "\<forall>b. (b, a) \<in> r --> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
  12.407 +      and acc_hyp: "\<forall>M. (M, M0) \<in> ?R --> M + {#a#} \<in> ?W"
  12.408 +    have "M0 + {#a#} \<in> ?W"
  12.409      proof (rule accI [of "M0 + {#a#}"])
  12.410        fix N
  12.411 -      assume "(N, M0 + {#a#}) \\<in> ?R"
  12.412 -      hence "((\\<exists>M. (M, M0) \\<in> ?R \\<and> N = M + {#a#}) \\<or>
  12.413 -          (\\<exists>K. (\\<forall>b. b :# K --> (b, a) \\<in> r) \\<and> N = M0 + K))"
  12.414 +      assume "(N, M0 + {#a#}) \<in> ?R"
  12.415 +      hence "((\<exists>M. (M, M0) \<in> ?R \<and> N = M + {#a#}) \<or>
  12.416 +          (\<exists>K. (\<forall>b. b :# K --> (b, a) \<in> r) \<and> N = M0 + K))"
  12.417          by (rule less_add)
  12.418 -      thus "N \\<in> ?W"
  12.419 +      thus "N \<in> ?W"
  12.420        proof (elim exE disjE conjE)
  12.421 -        fix M assume "(M, M0) \\<in> ?R" and N: "N = M + {#a#}"
  12.422 -        from acc_hyp have "(M, M0) \\<in> ?R --> M + {#a#} \\<in> ?W" ..
  12.423 -        hence "M + {#a#} \\<in> ?W" ..
  12.424 -        thus "N \\<in> ?W" by (simp only: N)
  12.425 +        fix M assume "(M, M0) \<in> ?R" and N: "N = M + {#a#}"
  12.426 +        from acc_hyp have "(M, M0) \<in> ?R --> M + {#a#} \<in> ?W" ..
  12.427 +        hence "M + {#a#} \<in> ?W" ..
  12.428 +        thus "N \<in> ?W" by (simp only: N)
  12.429        next
  12.430          fix K
  12.431          assume N: "N = M0 + K"
  12.432 -        assume "\\<forall>b. b :# K --> (b, a) \\<in> r"
  12.433 -        have "?this --> M0 + K \\<in> ?W" (is "?P K")
  12.434 +        assume "\<forall>b. b :# K --> (b, a) \<in> r"
  12.435 +        have "?this --> M0 + K \<in> ?W" (is "?P K")
  12.436          proof (induct K)
  12.437 -          from M0 have "M0 + {#} \\<in> ?W" by simp
  12.438 +          from M0 have "M0 + {#} \<in> ?W" by simp
  12.439            thus "?P {#}" ..
  12.440  
  12.441            fix K x assume hyp: "?P K"
  12.442            show "?P (K + {#x#})"
  12.443            proof
  12.444 -            assume a: "\\<forall>b. b :# (K + {#x#}) --> (b, a) \\<in> r"
  12.445 -            hence "(x, a) \\<in> r" by simp
  12.446 -            with wf_hyp have b: "\\<forall>M \\<in> ?W. M + {#x#} \\<in> ?W" by blast
  12.447 +            assume a: "\<forall>b. b :# (K + {#x#}) --> (b, a) \<in> r"
  12.448 +            hence "(x, a) \<in> r" by simp
  12.449 +            with wf_hyp have b: "\<forall>M \<in> ?W. M + {#x#} \<in> ?W" by blast
  12.450  
  12.451 -            from a hyp have "M0 + K \\<in> ?W" by simp
  12.452 -            with b have "(M0 + K) + {#x#} \\<in> ?W" ..
  12.453 -            thus "M0 + (K + {#x#}) \\<in> ?W" by (simp only: union_assoc)
  12.454 +            from a hyp have "M0 + K \<in> ?W" by simp
  12.455 +            with b have "(M0 + K) + {#x#} \<in> ?W" ..
  12.456 +            thus "M0 + (K + {#x#}) \<in> ?W" by (simp only: union_assoc)
  12.457            qed
  12.458          qed
  12.459 -        hence "M0 + K \\<in> ?W" ..
  12.460 -        thus "N \\<in> ?W" by (simp only: N)
  12.461 +        hence "M0 + K \<in> ?W" ..
  12.462 +        thus "N \<in> ?W" by (simp only: N)
  12.463        qed
  12.464      qed
  12.465    } note tedious_reasoning = this
  12.466  
  12.467    assume wf: "wf r"
  12.468    fix M
  12.469 -  show "M \\<in> ?W"
  12.470 +  show "M \<in> ?W"
  12.471    proof (induct M)
  12.472 -    show "{#} \\<in> ?W"
  12.473 +    show "{#} \<in> ?W"
  12.474      proof (rule accI)
  12.475 -      fix b assume "(b, {#}) \\<in> ?R"
  12.476 -      with not_less_empty show "b \\<in> ?W" by contradiction
  12.477 +      fix b assume "(b, {#}) \<in> ?R"
  12.478 +      with not_less_empty show "b \<in> ?W" by contradiction
  12.479      qed
  12.480  
  12.481 -    fix M a assume "M \\<in> ?W"
  12.482 -    from wf have "\\<forall>M \\<in> ?W. M + {#a#} \\<in> ?W"
  12.483 +    fix M a assume "M \<in> ?W"
  12.484 +    from wf have "\<forall>M \<in> ?W. M + {#a#} \<in> ?W"
  12.485      proof induct
  12.486        fix a
  12.487 -      assume "\\<forall>b. (b, a) \\<in> r --> (\\<forall>M \\<in> ?W. M + {#b#} \\<in> ?W)"
  12.488 -      show "\\<forall>M \\<in> ?W. M + {#a#} \\<in> ?W"
  12.489 +      assume "\<forall>b. (b, a) \<in> r --> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
  12.490 +      show "\<forall>M \<in> ?W. M + {#a#} \<in> ?W"
  12.491        proof
  12.492 -        fix M assume "M \\<in> ?W"
  12.493 -        thus "M + {#a#} \\<in> ?W"
  12.494 +        fix M assume "M \<in> ?W"
  12.495 +        thus "M + {#a#} \<in> ?W"
  12.496            by (rule acc_induct) (rule tedious_reasoning)
  12.497        qed
  12.498      qed
  12.499 -    thus "M + {#a#} \\<in> ?W" ..
  12.500 +    thus "M + {#a#} \<in> ?W" ..
  12.501    qed
  12.502  qed
  12.503  
  12.504 @@ -578,9 +578,9 @@
  12.505  text {* One direction. *}
  12.506  
  12.507  lemma mult_implies_one_step:
  12.508 -  "trans r ==> (M, N) \\<in> mult r ==>
  12.509 -    \\<exists>I J K. N = I + J \\<and> M = I + K \\<and> J \\<noteq> {#} \\<and>
  12.510 -    (\\<forall>k \\<in> set_of K. \\<exists>j \\<in> set_of J. (k, j) \\<in> r)"
  12.511 +  "trans r ==> (M, N) \<in> mult r ==>
  12.512 +    \<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and>
  12.513 +    (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r)"
  12.514    apply (unfold mult_def mult1_def set_of_def)
  12.515    apply (erule converse_trancl_induct)
  12.516    apply clarify
  12.517 @@ -592,7 +592,7 @@
  12.518     apply (simp (no_asm))
  12.519     apply (rule_tac x = "(K - {#a#}) + Ka" in exI)
  12.520     apply (simp (no_asm_simp) add: union_assoc [symmetric])
  12.521 -   apply (drule_tac f = "\\<lambda>M. M - {#a#}" in arg_cong)
  12.522 +   apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong)
  12.523     apply (simp add: diff_union_single_conv)
  12.524     apply (simp (no_asm_use) add: trans_def)
  12.525     apply blast
  12.526 @@ -603,7 +603,7 @@
  12.527     apply (rule conjI)
  12.528      apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
  12.529     apply (rule conjI)
  12.530 -    apply (drule_tac f = "\\<lambda>M. M - {#a#}" in arg_cong)
  12.531 +    apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong)
  12.532      apply simp
  12.533      apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
  12.534     apply (simp (no_asm_use) add: trans_def)
  12.535 @@ -617,7 +617,7 @@
  12.536    apply (simp add: multiset_eq_conv_count_eq)
  12.537    done
  12.538  
  12.539 -lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \\<exists>a N. M = N + {#a#}"
  12.540 +lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \<exists>a N. M = N + {#a#}"
  12.541    apply (erule size_eq_Suc_imp_elem [THEN exE])
  12.542    apply (drule elem_imp_eq_diff_union)
  12.543    apply auto
  12.544 @@ -625,8 +625,8 @@
  12.545  
  12.546  lemma one_step_implies_mult_aux:
  12.547    "trans r ==>
  12.548 -    \\<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))
  12.549 -      --> (I + K, I + J) \\<in> mult r"
  12.550 +    \<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))
  12.551 +      --> (I + K, I + J) \<in> mult r"
  12.552    apply (induct_tac n)
  12.553     apply auto
  12.554    apply (frule size_eq_Suc_imp_eq_union)
  12.555 @@ -640,15 +640,15 @@
  12.556     apply (rule r_into_trancl)
  12.557     apply (simp add: mult1_def set_of_def)
  12.558     apply blast
  12.559 -  txt {* Now we know @{term "J' \\<noteq> {#}"}. *}
  12.560 -  apply (cut_tac M = K and P = "\\<lambda>x. (x, a) \\<in> r" in multiset_partition)
  12.561 -  apply (erule_tac P = "\\<forall>k \\<in> set_of K. ?P k" in rev_mp)
  12.562 +  txt {* Now we know @{term "J' \<noteq> {#}"}. *}
  12.563 +  apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition)
  12.564 +  apply (erule_tac P = "\<forall>k \<in> set_of K. ?P k" in rev_mp)
  12.565    apply (erule ssubst)
  12.566    apply (simp add: Ball_def)
  12.567    apply auto
  12.568    apply (subgoal_tac
  12.569 -    "((I + {# x : K. (x, a) \\<in> r #}) + {# x : K. (x, a) \\<notin> r #},
  12.570 -      (I + {# x : K. (x, a) \\<in> r #}) + J') \\<in> mult r")
  12.571 +    "((I + {# x : K. (x, a) \<in> r #}) + {# x : K. (x, a) \<notin> r #},
  12.572 +      (I + {# x : K. (x, a) \<in> r #}) + J') \<in> mult r")
  12.573     prefer 2
  12.574     apply force
  12.575    apply (simp (no_asm_use) add: union_assoc [symmetric] mult_def)
  12.576 @@ -661,8 +661,8 @@
  12.577    done
  12.578  
  12.579  theorem one_step_implies_mult:
  12.580 -  "trans r ==> J \\<noteq> {#} ==> \\<forall>k \\<in> set_of K. \\<exists>j \\<in> set_of J. (k, j) \\<in> r
  12.581 -    ==> (I + K, I + J) \\<in> mult r"
  12.582 +  "trans r ==> J \<noteq> {#} ==> \<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r
  12.583 +    ==> (I + K, I + J) \<in> mult r"
  12.584    apply (insert one_step_implies_mult_aux)
  12.585    apply blast
  12.586    done
  12.587 @@ -673,8 +673,8 @@
  12.588  instance multiset :: ("term") ord ..
  12.589  
  12.590  defs (overloaded)
  12.591 -  less_multiset_def: "M' < M == (M', M) \\<in> mult {(x', x). x' < x}"
  12.592 -  le_multiset_def: "M' <= M == M' = M \\<or> M' < (M::'a multiset)"
  12.593 +  less_multiset_def: "M' < M == (M', M) \<in> mult {(x', x). x' < x}"
  12.594 +  le_multiset_def: "M' <= M == M' = M \<or> M' < (M::'a multiset)"
  12.595  
  12.596  lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
  12.597    apply (unfold trans_def)
  12.598 @@ -686,12 +686,12 @@
  12.599  *}
  12.600  
  12.601  lemma mult_irrefl_aux:
  12.602 -    "finite A ==> (\\<forall>x \\<in> A. \\<exists>y \\<in> A. x < (y::'a::order)) --> A = {}"
  12.603 +    "finite A ==> (\<forall>x \<in> A. \<exists>y \<in> A. x < (y::'a::order)) --> A = {}"
  12.604    apply (erule finite_induct)
  12.605     apply (auto intro: order_less_trans)
  12.606    done
  12.607  
  12.608 -theorem mult_less_not_refl: "\\<not> M < (M::'a::order multiset)"
  12.609 +theorem mult_less_not_refl: "\<not> M < (M::'a::order multiset)"
  12.610    apply (unfold less_multiset_def)
  12.611    apply auto
  12.612    apply (drule trans_base_order [THEN mult_implies_one_step])
  12.613 @@ -715,7 +715,7 @@
  12.614  
  12.615  text {* Asymmetry. *}
  12.616  
  12.617 -theorem mult_less_not_sym: "M < N ==> \\<not> N < (M::'a::order multiset)"
  12.618 +theorem mult_less_not_sym: "M < N ==> \<not> N < (M::'a::order multiset)"
  12.619    apply auto
  12.620    apply (rule mult_less_not_refl [THEN notE])
  12.621    apply (erule mult_less_trans)
  12.622 @@ -723,7 +723,7 @@
  12.623    done
  12.624  
  12.625  theorem mult_less_asym:
  12.626 -    "M < N ==> (\\<not> P ==> N < (M::'a::order multiset)) ==> P"
  12.627 +    "M < N ==> (\<not> P ==> N < (M::'a::order multiset)) ==> P"
  12.628    apply (insert mult_less_not_sym)
  12.629    apply blast
  12.630    done
  12.631 @@ -749,7 +749,7 @@
  12.632    apply (blast intro: mult_less_trans)
  12.633    done
  12.634  
  12.635 -theorem mult_less_le: "M < N = (M <= N \\<and> M \\<noteq> (N::'a::order multiset))"
  12.636 +theorem mult_less_le: "M < N = (M <= N \<and> M \<noteq> (N::'a::order multiset))"
  12.637    apply (unfold le_multiset_def)
  12.638    apply auto
  12.639    done
  12.640 @@ -770,7 +770,7 @@
  12.641  subsubsection {* Monotonicity of multiset union *}
  12.642  
  12.643  theorem mult1_union:
  12.644 -    "(B, D) \\<in> mult1 r ==> trans r ==> (C + B, C + D) \\<in> mult1 r"
  12.645 +    "(B, D) \<in> mult1 r ==> trans r ==> (C + B, C + D) \<in> mult1 r"
  12.646    apply (unfold mult1_def)
  12.647    apply auto
  12.648    apply (rule_tac x = a in exI)
  12.649 @@ -806,7 +806,7 @@
  12.650    apply (unfold le_multiset_def less_multiset_def)
  12.651    apply (case_tac "M = {#}")
  12.652     prefer 2
  12.653 -   apply (subgoal_tac "({#} + {#}, {#} + M) \\<in> mult (Collect (split op <))")
  12.654 +   apply (subgoal_tac "({#} + {#}, {#} + M) \<in> mult (Collect (split op <))")
  12.655      prefer 2
  12.656      apply (rule one_step_implies_mult)
  12.657        apply (simp only: trans_def)
    13.1 --- a/src/HOL/Library/Primes.thy	Mon Aug 06 13:12:06 2001 +0200
    13.2 +++ b/src/HOL/Library/Primes.thy	Mon Aug 06 13:43:24 2001 +0200
    13.3 @@ -54,7 +54,7 @@
    13.4  
    13.5  declare gcd.simps [simp del]
    13.6  
    13.7 -lemma gcd_1 [simp]: "gcd (m, 1) = 1"
    13.8 +lemma gcd_1 [simp]: "gcd (m, 1') = 1"
    13.9    apply (simp add: gcd_non_0)
   13.10    done
   13.11  
   13.12 @@ -140,8 +140,8 @@
   13.13    apply (simp add: gcd_commute [of 0])
   13.14    done
   13.15  
   13.16 -lemma gcd_1_left [simp]: "gcd (1, m) = 1"
   13.17 -  apply (simp add: gcd_commute [of 1])
   13.18 +lemma gcd_1_left [simp]: "gcd (1', m) = 1"
   13.19 +  apply (simp add: gcd_commute [of "1'"])
   13.20    done
   13.21  
   13.22  
    14.1 --- a/src/HOL/Nat.ML	Mon Aug 06 13:12:06 2001 +0200
    14.2 +++ b/src/HOL/Nat.ML	Mon Aug 06 13:43:24 2001 +0200
    14.3 @@ -68,7 +68,7 @@
    14.4  by Auto_tac;
    14.5  qed "less_Suc_eq_0_disj";
    14.6  
    14.7 -val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
    14.8 +val prems = Goal "[| P 0; P(1'); !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
    14.9  by (rtac nat_less_induct 1);
   14.10  by (case_tac "n" 1);
   14.11  by (case_tac "nat" 2);
   14.12 @@ -157,7 +157,7 @@
   14.13  (* Could be (and is, below) generalized in various ways;
   14.14     However, none of the generalizations are currently in the simpset,
   14.15     and I dread to think what happens if I put them in *)
   14.16 -Goal "0 < n ==> Suc(n-1) = n";
   14.17 +Goal "0 < n ==> Suc(n-1') = n";
   14.18  by (asm_simp_tac (simpset() addsplits [nat.split]) 1);
   14.19  qed "Suc_pred";
   14.20  Addsimps [Suc_pred];
   14.21 @@ -238,11 +238,16 @@
   14.22  qed "add_is_0";
   14.23  AddIffs [add_is_0];
   14.24  
   14.25 -Goal "!!m::nat. (m+n=1) = (m=1 & n=0 | m=0 & n=1)";
   14.26 +Goal "(m+n=1') = (m=1' & n=0 | m=0 & n=1')";
   14.27  by (case_tac "m" 1);
   14.28  by (Auto_tac);
   14.29  qed "add_is_1";
   14.30  
   14.31 +Goal "(1' = m+n) = (m=1' & n=0 | m=0 & n=1')";
   14.32 +by (case_tac "m" 1);
   14.33 +by (Auto_tac);
   14.34 +qed "one_is_add";
   14.35 +
   14.36  Goal "!!m::nat. (0<m+n) = (0<m | 0<n)";
   14.37  by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
   14.38  qed "add_gr_0";
   14.39 @@ -633,14 +638,14 @@
   14.40  qed "zero_less_mult_iff";
   14.41  Addsimps [zero_less_mult_iff];
   14.42  
   14.43 -Goal "(1 <= m*n) = (1<=m & 1<=n)";
   14.44 +Goal "(1' <= m*n) = (1<=m & 1<=n)";
   14.45  by (induct_tac "m" 1);
   14.46  by (case_tac "n" 2);
   14.47  by (ALLGOALS Asm_simp_tac);
   14.48  qed "one_le_mult_iff";
   14.49  Addsimps [one_le_mult_iff];
   14.50  
   14.51 -Goal "(m*n = 1) = (m=1 & n=1)";
   14.52 +Goal "(m*n = 1') = (m=1 & n=1)";
   14.53  by (induct_tac "m" 1);
   14.54  by (Simp_tac 1);
   14.55  by (induct_tac "n" 1);
   14.56 @@ -649,6 +654,12 @@
   14.57  qed "mult_eq_1_iff";
   14.58  Addsimps [mult_eq_1_iff];
   14.59  
   14.60 +Goal "(1' = m*n) = (m=1 & n=1)";
   14.61 +by(rtac (mult_eq_1_iff RSN (2,trans)) 1);
   14.62 +by (fast_tac (claset() addss simpset()) 1);
   14.63 +qed "one_eq_mult_iff";
   14.64 +Addsimps [one_eq_mult_iff];
   14.65 +
   14.66  Goal "!!m::nat. (m*k < n*k) = (0<k & m<n)";
   14.67  by (safe_tac (claset() addSIs [mult_less_mono1]));
   14.68  by (case_tac "k" 1);
    15.1 --- a/src/HOL/NatDef.ML	Mon Aug 06 13:12:06 2001 +0200
    15.2 +++ b/src/HOL/NatDef.ML	Mon Aug 06 13:43:24 2001 +0200
    15.3 @@ -4,6 +4,8 @@
    15.4      Copyright   1991  University of Cambridge
    15.5  *)
    15.6  
    15.7 +Addsimps [One_def];
    15.8 +
    15.9  val rew = rewrite_rule [symmetric Nat_def];
   15.10  
   15.11  (*** Induction ***)
    16.1 --- a/src/HOL/NatDef.thy	Mon Aug 06 13:12:06 2001 +0200
    16.2 +++ b/src/HOL/NatDef.thy	Mon Aug 06 13:43:24 2001 +0200
    16.3 @@ -55,14 +55,15 @@
    16.4  consts
    16.5    Suc       :: nat => nat
    16.6    pred_nat  :: "(nat * nat) set"
    16.7 +  "1"       :: nat                ("1")
    16.8  
    16.9  syntax
   16.10 -  "1"       :: nat                ("1")
   16.11 +  "1'"       :: nat                ("1'")
   16.12    "2"       :: nat                ("2")
   16.13  
   16.14  translations
   16.15 -  "1"  == "Suc 0"
   16.16 -  "2"  == "Suc 1"
   16.17 +  "1'"  == "Suc 0"
   16.18 +  "2"  == "Suc 1'"
   16.19  
   16.20  
   16.21  local
   16.22 @@ -70,6 +71,7 @@
   16.23  defs
   16.24    Zero_def      "0 == Abs_Nat(Zero_Rep)"
   16.25    Suc_def       "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
   16.26 +  One_def	"1 == 1'"
   16.27  
   16.28    (*nat operations*)
   16.29    pred_nat_def  "pred_nat == {(m,n). n = Suc m}"
    17.1 --- a/src/HOL/Power.ML	Mon Aug 06 13:12:06 2001 +0200
    17.2 +++ b/src/HOL/Power.ML	Mon Aug 06 13:43:24 2001 +0200
    17.3 @@ -30,7 +30,7 @@
    17.4  by Auto_tac;  
    17.5  qed "power_eq_0D";
    17.6  
    17.7 -Goal "!!i::nat. 1 <= i ==> 1 <= i^n";
    17.8 +Goal "!!i::nat. 1 <= i ==> 1' <= i^n";
    17.9  by (induct_tac "n" 1);
   17.10  by Auto_tac;
   17.11  qed "one_le_power";
   17.12 @@ -120,7 +120,7 @@
   17.13  qed "binomial_Suc_n";
   17.14  Addsimps [binomial_Suc_n];
   17.15  
   17.16 -Goal "(n choose 1) = n";
   17.17 +Goal "(n choose 1') = n";
   17.18  by (induct_tac "n" 1);
   17.19  by (ALLGOALS Asm_simp_tac);
   17.20  qed "binomial_1";
    18.1 --- a/src/HOL/Real/PNat.ML	Mon Aug 06 13:12:06 2001 +0200
    18.2 +++ b/src/HOL/Real/PNat.ML	Mon Aug 06 13:43:24 2001 +0200
    18.3 @@ -6,13 +6,13 @@
    18.4  The positive naturals -- proofs mainly as in theory Nat.
    18.5  *)
    18.6  
    18.7 -Goal "mono(%X. {1} Un Suc`X)";
    18.8 +Goal "mono(%X. {1'} Un Suc`X)";
    18.9  by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1));
   18.10  qed "pnat_fun_mono";
   18.11  
   18.12  bind_thm ("pnat_unfold", pnat_fun_mono RS (pnat_def RS def_lfp_unfold));
   18.13  
   18.14 -Goal "1 : pnat";
   18.15 +Goal "1' : pnat";
   18.16  by (stac pnat_unfold 1);
   18.17  by (rtac (singletonI RS UnI1) 1);
   18.18  qed "one_RepI";
   18.19 @@ -31,7 +31,7 @@
   18.20  (*** Induction ***)
   18.21  
   18.22  val major::prems = Goal
   18.23 -    "[| i: pnat;  P(1);   \
   18.24 +    "[| i: pnat;  P(1');   \
   18.25  \       !!j. [| j: pnat; P(j) |] ==> P(Suc(j)) |]  ==> P(i)";
   18.26  by (rtac ([pnat_def, pnat_fun_mono, major] MRS def_lfp_induct) 1);
   18.27  by (blast_tac (claset() addIs prems) 1);
   18.28 @@ -250,7 +250,7 @@
   18.29  (*** Rep_pnat < 0 ==> P ***)
   18.30  bind_thm ("Rep_pnat_less_zeroE",Rep_pnat_not_less0 RS notE);
   18.31  
   18.32 -Goal "~ Rep_pnat y < 1";
   18.33 +Goal "~ Rep_pnat y < 1'";
   18.34  by (auto_tac (claset(),simpset() addsimps [less_Suc_eq,
   18.35                    Rep_pnat_gt_zero,less_not_refl2]));
   18.36  qed "Rep_pnat_not_less_one";
   18.37 @@ -259,7 +259,7 @@
   18.38  bind_thm ("Rep_pnat_less_oneE",Rep_pnat_not_less_one RS notE);
   18.39  
   18.40  Goalw [pnat_less_def] 
   18.41 -     "x < (y::pnat) ==> Rep_pnat y ~= 1";
   18.42 +     "x < (y::pnat) ==> Rep_pnat y ~= 1'";
   18.43  by (auto_tac (claset(),simpset() 
   18.44      addsimps [Rep_pnat_not_less_one] delsimps [less_one]));
   18.45  qed "Rep_pnat_gt_implies_not0";
   18.46 @@ -270,7 +270,7 @@
   18.47  by (fast_tac (claset() addIs [inj_Rep_pnat RS injD]) 1);
   18.48  qed "pnat_less_linear";
   18.49  
   18.50 -Goalw [le_def] "1 <= Rep_pnat x";
   18.51 +Goalw [le_def] "1' <= Rep_pnat x";
   18.52  by (rtac Rep_pnat_not_less_one 1);
   18.53  qed "Rep_pnat_le_one";
   18.54  
   18.55 @@ -416,12 +416,12 @@
   18.56            Abs_pnat_inverse,mult_left_commute]) 1);
   18.57  qed "pnat_mult_left_commute";
   18.58  
   18.59 -Goalw [pnat_mult_def] "x * (Abs_pnat 1) = x";
   18.60 +Goalw [pnat_mult_def] "x * (Abs_pnat 1') = x";
   18.61  by (full_simp_tac (simpset() addsimps [one_RepI RS Abs_pnat_inverse,
   18.62                     Rep_pnat_inverse]) 1);
   18.63  qed "pnat_mult_1";
   18.64  
   18.65 -Goal "Abs_pnat 1 * x = x";
   18.66 +Goal "Abs_pnat 1' * x = x";
   18.67  by (full_simp_tac (simpset() addsimps [pnat_mult_1,
   18.68                     pnat_mult_commute]) 1);
   18.69  qed "pnat_mult_1_left";
    19.1 --- a/src/HOL/Real/PNat.thy	Mon Aug 06 13:12:06 2001 +0200
    19.2 +++ b/src/HOL/Real/PNat.thy	Mon Aug 06 13:43:24 2001 +0200
    19.3 @@ -9,7 +9,7 @@
    19.4  PNat = Main +
    19.5  
    19.6  typedef
    19.7 -  pnat = "lfp(%X. {1} Un Suc`X)"   (lfp_def)
    19.8 +  pnat = "lfp(%X. {1'} Un Suc`X)"   (lfp_def)
    19.9  
   19.10  instance
   19.11     pnat :: {ord, plus, times}
   19.12 @@ -27,7 +27,7 @@
   19.13  defs
   19.14  
   19.15    pnat_one_def      
   19.16 -       "1p == Abs_pnat(1)"
   19.17 +       "1p == Abs_pnat(1')"
   19.18    pnat_Suc_def      
   19.19         "pSuc == (%n. Abs_pnat(Suc(Rep_pnat(n))))"
   19.20  
    20.1 --- a/src/HOL/Real/PRat.ML	Mon Aug 06 13:12:06 2001 +0200
    20.2 +++ b/src/HOL/Real/PRat.ML	Mon Aug 06 13:43:24 2001 +0200
    20.3 @@ -128,7 +128,7 @@
    20.4  qed "inj_qinv";
    20.5  
    20.6  Goalw [prat_of_pnat_def] 
    20.7 -      "qinv(prat_of_pnat  (Abs_pnat 1)) = prat_of_pnat (Abs_pnat 1)";
    20.8 +      "qinv(prat_of_pnat  (Abs_pnat 1')) = prat_of_pnat (Abs_pnat 1')";
    20.9  by (simp_tac (simpset() addsimps [qinv]) 1);
   20.10  qed "qinv_1";
   20.11  
   20.12 @@ -232,13 +232,13 @@
   20.13                      prat_mult_commute,prat_mult_left_commute]);
   20.14  
   20.15  Goalw [prat_of_pnat_def] 
   20.16 -      "(prat_of_pnat (Abs_pnat 1)) * z = z";
   20.17 +      "(prat_of_pnat (Abs_pnat 1')) * z = z";
   20.18  by (res_inst_tac [("z","z")] eq_Abs_prat 1);
   20.19  by (asm_full_simp_tac (simpset() addsimps [prat_mult] @ pnat_mult_ac) 1);
   20.20  qed "prat_mult_1";
   20.21  
   20.22  Goalw [prat_of_pnat_def] 
   20.23 -      "z * (prat_of_pnat (Abs_pnat 1)) = z";
   20.24 +      "z * (prat_of_pnat (Abs_pnat 1')) = z";
   20.25  by (res_inst_tac [("z","z")] eq_Abs_prat 1);
   20.26  by (asm_full_simp_tac (simpset() addsimps [prat_mult] @ pnat_mult_ac) 1);
   20.27  qed "prat_mult_1_right";
   20.28 @@ -259,22 +259,22 @@
   20.29  (*** prat_mult and qinv ***)
   20.30  
   20.31  Goalw [prat_def,prat_of_pnat_def] 
   20.32 -      "qinv (q) * q = prat_of_pnat (Abs_pnat 1)";
   20.33 +      "qinv (q) * q = prat_of_pnat (Abs_pnat 1')";
   20.34  by (res_inst_tac [("z","q")] eq_Abs_prat 1);
   20.35  by (asm_full_simp_tac (simpset() addsimps [qinv,
   20.36          prat_mult,pnat_mult_1,pnat_mult_1_left, pnat_mult_commute]) 1);
   20.37  qed "prat_mult_qinv";
   20.38  
   20.39 -Goal "q * qinv (q) = prat_of_pnat (Abs_pnat 1)";
   20.40 +Goal "q * qinv (q) = prat_of_pnat (Abs_pnat 1')";
   20.41  by (rtac (prat_mult_commute RS subst) 1);
   20.42  by (simp_tac (simpset() addsimps [prat_mult_qinv]) 1);
   20.43  qed "prat_mult_qinv_right";
   20.44  
   20.45 -Goal "EX y. (x::prat) * y = prat_of_pnat (Abs_pnat 1)";
   20.46 +Goal "EX y. (x::prat) * y = prat_of_pnat (Abs_pnat 1')";
   20.47  by (fast_tac (claset() addIs [prat_mult_qinv_right]) 1);
   20.48  qed "prat_qinv_ex";
   20.49  
   20.50 -Goal "EX! y. (x::prat) * y = prat_of_pnat (Abs_pnat 1)";
   20.51 +Goal "EX! y. (x::prat) * y = prat_of_pnat (Abs_pnat 1')";
   20.52  by (auto_tac (claset() addIs [prat_mult_qinv_right],simpset()));
   20.53  by (dres_inst_tac [("f","%x. ya*x")] arg_cong 1);
   20.54  by (asm_full_simp_tac (simpset() addsimps [prat_mult_assoc RS sym]) 1);
   20.55 @@ -282,7 +282,7 @@
   20.56      prat_mult_1,prat_mult_1_right]) 1);
   20.57  qed "prat_qinv_ex1";
   20.58  
   20.59 -Goal "EX! y. y * (x::prat) = prat_of_pnat (Abs_pnat 1)";
   20.60 +Goal "EX! y. y * (x::prat) = prat_of_pnat (Abs_pnat 1')";
   20.61  by (auto_tac (claset() addIs [prat_mult_qinv],simpset()));
   20.62  by (dres_inst_tac [("f","%x. x*ya")] arg_cong 1);
   20.63  by (asm_full_simp_tac (simpset() addsimps [prat_mult_assoc]) 1);
   20.64 @@ -290,7 +290,7 @@
   20.65      prat_mult_1,prat_mult_1_right]) 1);
   20.66  qed "prat_qinv_left_ex1";
   20.67  
   20.68 -Goal "x * y = prat_of_pnat (Abs_pnat 1) ==> x = qinv y";
   20.69 +Goal "x * y = prat_of_pnat (Abs_pnat 1') ==> x = qinv y";
   20.70  by (cut_inst_tac [("q","y")] prat_mult_qinv 1);
   20.71  by (res_inst_tac [("x1","y")] (prat_qinv_left_ex1 RS ex1E) 1);
   20.72  by (Blast_tac 1);
   20.73 @@ -506,7 +506,7 @@
   20.74  by (cut_inst_tac [("x","q1"),("q1.0","qinv (q1)"), ("q2.0","qinv (q2)")] 
   20.75      prat_mult_left_less2_mono1 1);
   20.76  by Auto_tac;
   20.77 -by (dres_inst_tac [("q2.0","prat_of_pnat (Abs_pnat 1)")] prat_less_trans 1);
   20.78 +by (dres_inst_tac [("q2.0","prat_of_pnat (Abs_pnat 1')")] prat_less_trans 1);
   20.79  by (auto_tac (claset(),simpset() addsimps 
   20.80      [prat_less_not_refl]));
   20.81  qed "lemma2_qinv_prat_less";
   20.82 @@ -517,8 +517,8 @@
   20.83                   lemma2_qinv_prat_less],simpset()));
   20.84  qed "qinv_prat_less";
   20.85  
   20.86 -Goal "q1 < prat_of_pnat (Abs_pnat 1) \
   20.87 -\     ==> prat_of_pnat (Abs_pnat 1) < qinv(q1)";
   20.88 +Goal "q1 < prat_of_pnat (Abs_pnat 1') \
   20.89 +\     ==> prat_of_pnat (Abs_pnat 1') < qinv(q1)";
   20.90  by (dtac qinv_prat_less 1);
   20.91  by (full_simp_tac (simpset() addsimps [qinv_1]) 1);
   20.92  qed "prat_qinv_gt_1";
   20.93 @@ -529,18 +529,18 @@
   20.94  qed "prat_qinv_is_gt_1";
   20.95  
   20.96  Goalw [prat_less_def] 
   20.97 -      "prat_of_pnat (Abs_pnat 1) < prat_of_pnat (Abs_pnat 1) \
   20.98 -\                   + prat_of_pnat (Abs_pnat 1)";
   20.99 +      "prat_of_pnat (Abs_pnat 1') < prat_of_pnat (Abs_pnat 1') \
  20.100 +\                   + prat_of_pnat (Abs_pnat 1')";
  20.101  by (Fast_tac 1); 
  20.102  qed "prat_less_1_2";
  20.103  
  20.104 -Goal "qinv(prat_of_pnat (Abs_pnat 1) + \
  20.105 -\     prat_of_pnat (Abs_pnat 1)) < prat_of_pnat (Abs_pnat 1)";
  20.106 +Goal "qinv(prat_of_pnat (Abs_pnat 1') + \
  20.107 +\     prat_of_pnat (Abs_pnat 1')) < prat_of_pnat (Abs_pnat 1')";
  20.108  by (cut_facts_tac [prat_less_1_2 RS qinv_prat_less] 1);
  20.109  by (asm_full_simp_tac (simpset() addsimps [qinv_1]) 1);
  20.110  qed "prat_less_qinv_2_1";
  20.111  
  20.112 -Goal "!!(x::prat). x < y ==> x*qinv(y) < prat_of_pnat (Abs_pnat 1)";
  20.113 +Goal "!!(x::prat). x < y ==> x*qinv(y) < prat_of_pnat (Abs_pnat 1')";
  20.114  by (dres_inst_tac [("x","qinv(y)")] prat_mult_less2_mono1 1);
  20.115  by (Asm_full_simp_tac 1);
  20.116  qed "prat_mult_qinv_less_1";
  20.117 @@ -701,19 +701,19 @@
  20.118      pnat_mult_1]));
  20.119  qed "Abs_prat_mult_qinv";
  20.120  
  20.121 -Goal "Abs_prat(ratrel``{(x,y)}) <= Abs_prat(ratrel``{(x,Abs_pnat 1)})";
  20.122 +Goal "Abs_prat(ratrel``{(x,y)}) <= Abs_prat(ratrel``{(x,Abs_pnat 1')})";
  20.123  by (simp_tac (simpset() addsimps [Abs_prat_mult_qinv]) 1);
  20.124  by (rtac prat_mult_left_le2_mono1 1);
  20.125  by (rtac qinv_prat_le 1);
  20.126  by (pnat_ind_tac "y" 1);
  20.127 -by (dres_inst_tac [("x","prat_of_pnat (Abs_pnat 1)")] prat_add_le2_mono1 2);
  20.128 +by (dres_inst_tac [("x","prat_of_pnat (Abs_pnat 1')")] prat_add_le2_mono1 2);
  20.129  by (cut_facts_tac [prat_less_1_2 RS prat_less_imp_le] 2);
  20.130  by (auto_tac (claset() addIs [prat_le_trans],
  20.131      simpset() addsimps [prat_le_refl,
  20.132      pSuc_is_plus_one,pnat_one_def,prat_of_pnat_add]));
  20.133  qed "lemma_Abs_prat_le1";
  20.134  
  20.135 -Goal "Abs_prat(ratrel``{(x,Abs_pnat 1)}) <= Abs_prat(ratrel``{(x*y,Abs_pnat 1)})";
  20.136 +Goal "Abs_prat(ratrel``{(x,Abs_pnat 1')}) <= Abs_prat(ratrel``{(x*y,Abs_pnat 1')})";
  20.137  by (simp_tac (simpset() addsimps [Abs_prat_mult_qinv]) 1);
  20.138  by (rtac prat_mult_le2_mono1 1);
  20.139  by (pnat_ind_tac "y" 1);
  20.140 @@ -726,19 +726,19 @@
  20.141  			prat_of_pnat_add,prat_of_pnat_mult]));
  20.142  qed "lemma_Abs_prat_le2";
  20.143  
  20.144 -Goal "Abs_prat(ratrel``{(x,z)}) <= Abs_prat(ratrel``{(x*y,Abs_pnat 1)})";
  20.145 +Goal "Abs_prat(ratrel``{(x,z)}) <= Abs_prat(ratrel``{(x*y,Abs_pnat 1')})";
  20.146  by (fast_tac (claset() addIs [prat_le_trans,
  20.147  			      lemma_Abs_prat_le1,lemma_Abs_prat_le2]) 1);
  20.148  qed "lemma_Abs_prat_le3";
  20.149  
  20.150 -Goal "Abs_prat(ratrel``{(x*y,Abs_pnat 1)}) * Abs_prat(ratrel``{(w,x)}) = \
  20.151 -\         Abs_prat(ratrel``{(w*y,Abs_pnat 1)})";
  20.152 +Goal "Abs_prat(ratrel``{(x*y,Abs_pnat 1')}) * Abs_prat(ratrel``{(w,x)}) = \
  20.153 +\         Abs_prat(ratrel``{(w*y,Abs_pnat 1')})";
  20.154  by (full_simp_tac (simpset() addsimps [prat_mult,
  20.155      pnat_mult_1,pnat_mult_1_left] @ pnat_mult_ac) 1);
  20.156  qed "pre_lemma_gleason9_34";
  20.157  
  20.158 -Goal "Abs_prat(ratrel``{(y*x,Abs_pnat 1*y)}) = \
  20.159 -\         Abs_prat(ratrel``{(x,Abs_pnat 1)})";
  20.160 +Goal "Abs_prat(ratrel``{(y*x,Abs_pnat 1'*y)}) = \
  20.161 +\         Abs_prat(ratrel``{(x,Abs_pnat 1')})";
  20.162  by (auto_tac (claset(),
  20.163  	      simpset() addsimps [pnat_mult_1,pnat_mult_1_left] @ pnat_mult_ac));
  20.164  qed "pre_lemma_gleason9_34b";
  20.165 @@ -760,42 +760,42 @@
  20.166  (*** of preal type as defined using Dedekind Sections in PReal  ***)
  20.167  (*** Show that exists positive real `one' ***)
  20.168  
  20.169 -Goal "EX q. q: {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
  20.170 +Goal "EX q. q: {x::prat. x < prat_of_pnat (Abs_pnat 1')}";
  20.171  by (fast_tac (claset() addIs [prat_less_qinv_2_1]) 1);
  20.172  qed "lemma_prat_less_1_memEx";
  20.173  
  20.174 -Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} ~= {}";
  20.175 +Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1')} ~= {}";
  20.176  by (rtac notI 1);
  20.177  by (cut_facts_tac [lemma_prat_less_1_memEx] 1);
  20.178  by (Asm_full_simp_tac 1);
  20.179  qed "lemma_prat_less_1_set_non_empty";
  20.180  
  20.181 -Goalw [psubset_def] "{} < {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
  20.182 +Goalw [psubset_def] "{} < {x::prat. x < prat_of_pnat (Abs_pnat 1')}";
  20.183  by (asm_full_simp_tac (simpset() addsimps 
  20.184           [lemma_prat_less_1_set_non_empty RS not_sym]) 1);
  20.185  qed "empty_set_psubset_lemma_prat_less_1_set";
  20.186  
  20.187  (*** exists rational not in set --- prat_of_pnat (Abs_pnat 1) itself ***)
  20.188 -Goal "EX q. q ~: {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
  20.189 -by (res_inst_tac [("x","prat_of_pnat (Abs_pnat 1)")] exI 1);
  20.190 +Goal "EX q. q ~: {x::prat. x < prat_of_pnat (Abs_pnat 1')}";
  20.191 +by (res_inst_tac [("x","prat_of_pnat (Abs_pnat 1')")] exI 1);
  20.192  by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
  20.193  qed "lemma_prat_less_1_not_memEx";
  20.194  
  20.195 -Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} ~= UNIV";
  20.196 +Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1')} ~= UNIV";
  20.197  by (rtac notI 1);
  20.198  by (cut_facts_tac [lemma_prat_less_1_not_memEx] 1);
  20.199  by (Asm_full_simp_tac 1);
  20.200  qed "lemma_prat_less_1_set_not_rat_set";
  20.201  
  20.202  Goalw [psubset_def,subset_def] 
  20.203 -      "{x::prat. x < prat_of_pnat (Abs_pnat 1)} < UNIV";
  20.204 +      "{x::prat. x < prat_of_pnat (Abs_pnat 1')} < UNIV";
  20.205  by (asm_full_simp_tac
  20.206      (simpset() addsimps [lemma_prat_less_1_set_not_rat_set,
  20.207  			 lemma_prat_less_1_not_memEx]) 1);
  20.208  qed "lemma_prat_less_1_set_psubset_rat_set";
  20.209  
  20.210  (*** prove non_emptiness of type ***)
  20.211 -Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} : {A. {} < A & \
  20.212 +Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1')} : {A. {} < A & \
  20.213  \               A < UNIV & \
  20.214  \               (!y: A. ((!z. z < y --> z: A) & \
  20.215  \               (EX u: A. y < u)))}";
    21.1 --- a/src/HOL/Real/PReal.ML	Mon Aug 06 13:12:06 2001 +0200
    21.2 +++ b/src/HOL/Real/PReal.ML	Mon Aug 06 13:43:24 2001 +0200
    21.3 @@ -30,7 +30,7 @@
    21.4  
    21.5  Addsimps [empty_not_mem_preal];
    21.6  
    21.7 -Goalw [preal_def] "{x::prat. x < prat_of_pnat (Abs_pnat 1)} : preal";
    21.8 +Goalw [preal_def] "{x::prat. x < prat_of_pnat (Abs_pnat 1')} : preal";
    21.9  by (rtac preal_1 1);
   21.10  qed "one_set_mem_preal";
   21.11  
   21.12 @@ -234,9 +234,9 @@
   21.13  \         ALL z. z < y --> z : {w. EX x:Rep_preal R. EX y:Rep_preal S. w = x + y}";
   21.14  by Auto_tac;
   21.15  by (ftac prat_mult_qinv_less_1 1);
   21.16 -by (forw_inst_tac [("x","x"),("q2.0","prat_of_pnat (Abs_pnat 1)")] 
   21.17 +by (forw_inst_tac [("x","x"),("q2.0","prat_of_pnat (Abs_pnat 1')")] 
   21.18      prat_mult_less2_mono1 1);
   21.19 -by (forw_inst_tac [("x","ya"),("q2.0","prat_of_pnat (Abs_pnat 1)")] 
   21.20 +by (forw_inst_tac [("x","ya"),("q2.0","prat_of_pnat (Abs_pnat 1')")] 
   21.21      prat_mult_less2_mono1 1);
   21.22  by (Asm_full_simp_tac 1);
   21.23  by (REPEAT(dtac (Rep_preal RS prealE_lemma3a) 1));
   21.24 @@ -367,7 +367,7 @@
   21.25  (* Positive Real 1 is the multiplicative identity element *) 
   21.26  (* long *)
   21.27  Goalw [preal_of_prat_def,preal_mult_def] 
   21.28 -      "(preal_of_prat (prat_of_pnat (Abs_pnat 1))) * z = z";
   21.29 +      "(preal_of_prat (prat_of_pnat (Abs_pnat 1'))) * z = z";
   21.30  by (rtac (Rep_preal_inverse RS subst) 1);
   21.31  by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
   21.32  by (rtac (one_set_mem_preal RS Abs_preal_inverse RS ssubst) 1);
   21.33 @@ -382,7 +382,7 @@
   21.34  by (auto_tac (claset(),simpset() addsimps [prat_mult_assoc]));
   21.35  qed "preal_mult_1";
   21.36  
   21.37 -Goal "z * (preal_of_prat (prat_of_pnat (Abs_pnat 1))) = z";
   21.38 +Goal "z * (preal_of_prat (prat_of_pnat (Abs_pnat 1'))) = z";
   21.39  by (rtac (preal_mult_commute RS subst) 1);
   21.40  by (rtac preal_mult_1 1);
   21.41  qed "preal_mult_1_right";
   21.42 @@ -563,7 +563,7 @@
   21.43  
   21.44  (*more lemmas for inverse *)
   21.45  Goal "x: Rep_preal(pinv(A)*A) ==> \
   21.46 -\     x: Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat 1)))";
   21.47 +\     x: Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat 1')))";
   21.48  by (auto_tac (claset() addSDs [mem_Rep_preal_multD],
   21.49                simpset() addsimps [pinv_def,preal_of_prat_def] ));
   21.50  by (dtac (preal_mem_inv_set RS Abs_preal_inverse RS subst) 1);
   21.51 @@ -583,8 +583,8 @@
   21.52  qed "lemma1_gleason9_34";
   21.53  
   21.54  Goal "Abs_prat (ratrel `` {(y, z)}) < xb + \
   21.55 -\         Abs_prat (ratrel `` {(x*y, Abs_pnat 1)})*Abs_prat (ratrel `` {(w, x)})";
   21.56 -by (res_inst_tac [("j","Abs_prat (ratrel `` {(x * y, Abs_pnat 1)}) *\
   21.57 +\         Abs_prat (ratrel `` {(x*y, Abs_pnat 1')})*Abs_prat (ratrel `` {(w, x)})";
   21.58 +by (res_inst_tac [("j","Abs_prat (ratrel `` {(x * y, Abs_pnat 1')}) *\
   21.59  \                   Abs_prat (ratrel `` {(w, x)})")] prat_le_less_trans 1);
   21.60  by (rtac prat_self_less_add_right 2);
   21.61  by (auto_tac (claset() addIs [lemma_Abs_prat_le3],
   21.62 @@ -650,14 +650,14 @@
   21.63  by Auto_tac;
   21.64  qed "lemma_gleason9_36";
   21.65  
   21.66 -Goal "prat_of_pnat (Abs_pnat 1) < x ==> \
   21.67 +Goal "prat_of_pnat (Abs_pnat 1') < x ==> \
   21.68  \     EX r: Rep_preal(A). r*x ~: Rep_preal(A)";
   21.69  by (rtac lemma_gleason9_36 1);
   21.70  by (asm_simp_tac (simpset() addsimps [pnat_one_def]) 1);
   21.71  qed "lemma_gleason9_36a";
   21.72  
   21.73  (*** Part 2 of existence of inverse ***)
   21.74 -Goal "x: Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat 1))) \
   21.75 +Goal "x: Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat 1'))) \
   21.76  \     ==> x: Rep_preal(pinv(A)*A)";
   21.77  by (auto_tac (claset() addSIs [mem_Rep_preal_multI],
   21.78                simpset() addsimps [pinv_def,preal_of_prat_def] ));
   21.79 @@ -677,12 +677,12 @@
   21.80      prat_mult_left_commute]));
   21.81  qed "preal_mem_mult_invI";
   21.82  
   21.83 -Goal "pinv(A)*A = (preal_of_prat (prat_of_pnat (Abs_pnat 1)))";
   21.84 +Goal "pinv(A)*A = (preal_of_prat (prat_of_pnat (Abs_pnat 1')))";
   21.85  by (rtac (inj_Rep_preal RS injD) 1);
   21.86  by (fast_tac (claset() addDs [preal_mem_mult_invD,preal_mem_mult_invI]) 1);
   21.87  qed "preal_mult_inv";
   21.88  
   21.89 -Goal "A*pinv(A) = (preal_of_prat (prat_of_pnat (Abs_pnat 1)))";
   21.90 +Goal "A*pinv(A) = (preal_of_prat (prat_of_pnat (Abs_pnat 1')))";
   21.91  by (rtac (preal_mult_commute RS subst) 1);
   21.92  by (rtac preal_mult_inv 1);
   21.93  qed "preal_mult_inv_right";
    22.1 --- a/src/HOL/Real/RealOrd.ML	Mon Aug 06 13:12:06 2001 +0200
    22.2 +++ b/src/HOL/Real/RealOrd.ML	Mon Aug 06 13:43:24 2001 +0200
    22.3 @@ -269,7 +269,7 @@
    22.4                         symmetric real_one_def]) 1);
    22.5  qed "real_of_posnat_one";
    22.6  
    22.7 -Goalw [real_of_posnat_def] "real_of_posnat 1 = 1r + 1r";
    22.8 +Goalw [real_of_posnat_def] "real_of_posnat 1' = 1r + 1r";
    22.9  by (simp_tac (simpset() addsimps [real_of_preal_def,real_one_def,
   22.10                                 pnat_two_eq,real_add,prat_of_pnat_add RS sym,
   22.11                                 preal_of_prat_add RS sym] @ pnat_add_ac) 1);
   22.12 @@ -306,7 +306,7 @@
   22.13  by (simp_tac (simpset() addsimps [real_of_posnat_one]) 1);
   22.14  qed "real_of_nat_zero";
   22.15  
   22.16 -Goalw [real_of_nat_def] "real (1::nat) = 1r";
   22.17 +Goalw [real_of_nat_def] "real (1') = 1r";
   22.18  by (simp_tac (simpset() addsimps [real_of_posnat_two, real_add_assoc]) 1);
   22.19  qed "real_of_nat_one";
   22.20  Addsimps [real_of_nat_zero, real_of_nat_one];
    23.1 --- a/src/HOL/arith_data.ML	Mon Aug 06 13:12:06 2001 +0200
    23.2 +++ b/src/HOL/arith_data.ML	Mon Aug 06 13:43:24 2001 +0200
    23.3 @@ -299,6 +299,7 @@
    23.4        else poly(s,m,poly(t,ratneg m,pi))
    23.5    | poly(Const("uminus",_) $ t, m, pi) = poly(t,ratneg m,pi)
    23.6    | poly(Const("0",_), _, pi) = pi
    23.7 +  | poly(Const("1",_), m, (p,i)) = (p,ratadd(i,m))
    23.8    | poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,ratadd(i,m)))
    23.9    | poly(t as Const("op *",_) $ _ $ _, m, pi as (p,i)) =
   23.10        (case demult(t,m) of
   23.11 @@ -363,7 +364,7 @@
   23.12  (* reduce contradictory <= to False.
   23.13     Most of the work is done by the cancel tactics.
   23.14  *)
   23.15 -val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq];
   23.16 +val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq,One_def];
   23.17  
   23.18  val add_mono_thms_nat = map (fn s => prove_goal (the_context ()) s
   23.19   (fn prems => [cut_facts_tac prems 1,
    24.1 --- a/src/HOL/ex/Primrec.thy	Mon Aug 06 13:12:06 2001 +0200
    24.2 +++ b/src/HOL/ex/Primrec.thy	Mon Aug 06 13:43:24 2001 +0200
    24.3 @@ -159,7 +159,7 @@
    24.4  
    24.5  text {* PROPERTY A 8 *}
    24.6  
    24.7 -lemma ack_1 [simp]: "ack (1, j) = j + #2"
    24.8 +lemma ack_1 [simp]: "ack (1', j) = j + #2"
    24.9    apply (induct j)
   24.10     apply simp_all
   24.11    done