# HG changeset patch
# User wenzelm
# Date 1149635213 -7200
# Node ID c2860c37e574d02dd2514c69acfa12404ef6b384
# Parent  b2af2549efd1146fc4621006975cccbcbbbefc4a
removed obsolete ML files;

diff -r b2af2549efd1 -r c2860c37e574 src/HOL/Hoare/Arith2.ML
--- a/src/HOL/Hoare/Arith2.ML	Wed Jun 07 00:57:14 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,66 +0,0 @@
-(*  Title:      HOL/Hoare/Arith2.ML
-    ID:         $Id$
-    Author:     Norbert Galm
-    Copyright   1995 TUM
-
-More arithmetic lemmas.
-*)
-
-(*** cd ***)
-
-Goalw [cd_def] "0<n ==> cd n n n";
-by (Asm_simp_tac 1);
-qed "cd_nnn";
-
-Goalw [cd_def] "[| cd x m n; 0<m; 0<n |] ==> x<=m & x<=n";
-by (blast_tac (claset() addIs [dvd_imp_le]) 1);
-qed "cd_le";
-
-Goalw [cd_def] "cd x m n = cd x n m";
-by (Fast_tac 1);
-qed "cd_swap";
-
-Goalw [cd_def] "n<=m ==> cd x m n = cd x (m-n) n";
-by (blast_tac (claset() addIs [dvd_diff] addDs [dvd_diffD]) 1);
-qed "cd_diff_l";
-
-Goalw [cd_def] "m<=n ==> cd x m n = cd x m (n-m)";
-by (blast_tac (claset() addIs [dvd_diff] addDs [dvd_diffD]) 1);
-qed "cd_diff_r";
-
-
-(*** gcd ***)
-
-Goalw [gcd_def] "0<n ==> n = gcd n n";
-by (ftac cd_nnn 1);
-by (rtac (some_equality RS sym) 1);
-by (blast_tac (claset() addDs [cd_le]) 1);
-by (blast_tac (claset() addIs [le_anti_sym] addDs [cd_le]) 1);
-qed "gcd_nnn";
-
-val prems = goalw (the_context ()) [gcd_def] "gcd m n = gcd n m";
-by (simp_tac (simpset() addsimps [cd_swap]) 1);
-qed "gcd_swap";
-
-Goalw [gcd_def] "n<=m ==> gcd m n = gcd (m-n) n";
-by (subgoal_tac "n<=m ==> !x. cd x m n = cd x (m-n) n" 1);
-by (Asm_simp_tac 1);
-by (rtac allI 1);
-by (etac cd_diff_l 1);
-qed "gcd_diff_l";
-
-Goalw [gcd_def] "m<=n ==> gcd m n = gcd m (n-m)";
-by (subgoal_tac "m<=n ==> !x. cd x m n = cd x m (n-m)" 1);
-by (Asm_simp_tac 1);
-by (rtac allI 1);
-by (etac cd_diff_r 1);
-qed "gcd_diff_r";
-
-
-(*** pow ***)
-
-Goal "m mod 2 = 0 ==> ((n::nat)*n)^(m div 2) = n^m";
-by (asm_simp_tac (simpset() addsimps [power2_eq_square RS sym, 
-                   power_mult RS sym, mult_div_cancel]) 1);
-qed "sq_pow_div2";
-Addsimps [sq_pow_div2];
diff -r b2af2549efd1 -r c2860c37e574 src/HOL/Hoare/Arith2.thy
--- a/src/HOL/Hoare/Arith2.thy	Wed Jun 07 00:57:14 2006 +0200
+++ b/src/HOL/Hoare/Arith2.thy	Wed Jun 07 01:06:53 2006 +0200
@@ -23,6 +23,70 @@
   "fac 0 = Suc 0"
   "fac(Suc n) = (Suc n)*fac(n)"
 
-ML {* use_legacy_bindings (the_context ()) *}
+
+subsubsection {* cd *}
+
+lemma cd_nnn: "0<n ==> cd n n n"
+  apply (simp add: cd_def)
+  done
+
+lemma cd_le: "[| cd x m n; 0<m; 0<n |] ==> x<=m & x<=n"
+  apply (unfold cd_def)
+  apply (blast intro: dvd_imp_le)
+  done
+
+lemma cd_swap: "cd x m n = cd x n m"
+  apply (unfold cd_def)
+  apply blast
+  done
+
+lemma cd_diff_l: "n<=m ==> cd x m n = cd x (m-n) n"
+  apply (unfold cd_def)
+  apply (blast intro: dvd_diff dest: dvd_diffD)
+  done
+
+lemma cd_diff_r: "m<=n ==> cd x m n = cd x m (n-m)"
+  apply (unfold cd_def)
+  apply (blast intro: dvd_diff dest: dvd_diffD)
+  done
+
+
+subsubsection {* gcd *}
+
+lemma gcd_nnn: "0<n ==> n = gcd n n"
+  apply (unfold gcd_def)
+  apply (frule cd_nnn)
+  apply (rule some_equality [symmetric])
+  apply (blast dest: cd_le)
+  apply (blast intro: le_anti_sym dest: cd_le)
+  done
+
+lemma gcd_swap: "gcd m n = gcd n m"
+  apply (simp add: gcd_def cd_swap)
+  done
+
+lemma gcd_diff_l: "n<=m ==> gcd m n = gcd (m-n) n"
+  apply (unfold gcd_def)
+  apply (subgoal_tac "n<=m ==> !x. cd x m n = cd x (m-n) n")
+  apply simp
+  apply (rule allI)
+  apply (erule cd_diff_l)
+  done
+
+lemma gcd_diff_r: "m<=n ==> gcd m n = gcd m (n-m)"
+  apply (unfold gcd_def)
+  apply (subgoal_tac "m<=n ==> !x. cd x m n = cd x m (n-m) ")
+  apply simp
+  apply (rule allI)
+  apply (erule cd_diff_r)
+  done
+
+
+subsubsection {* pow *}
+
+lemma sq_pow_div2 [simp]:
+    "m mod 2 = 0 ==> ((n::nat)*n)^(m div 2) = n^m"
+  apply (simp add: power2_eq_square [symmetric] power_mult [symmetric] mult_div_cancel)
+  done
 
 end
diff -r b2af2549efd1 -r c2860c37e574 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Jun 07 00:57:14 2006 +0200
+++ b/src/HOL/IsaMakefile	Wed Jun 07 01:06:53 2006 +0200
@@ -345,7 +345,7 @@
 
 HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz
 
-$(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.ML Hoare/Arith2.thy \
+$(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy \
   Hoare/Examples.thy Hoare/hoare.ML Hoare/Hoare.thy \
   Hoare/Heap.thy Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy \
   Hoare/ROOT.ML Hoare/ExamplesAbort.thy  Hoare/HeapSyntaxAbort.thy \