# HG changeset patch
# User paulson
# Date 863165938 -7200
# Node ID 49f2614732ea26d9abcb3c3aa1f50f3fb0d987e0
# Parent  922a604513828b874c068116f9f16a5693ea3a8d
New theorems about "assign"

diff -r 922a60451382 -r 49f2614732ea src/HOL/Induct/Com.ML
--- a/src/HOL/Induct/Com.ML	Fri May 09 10:18:07 1997 +0200
+++ b/src/HOL/Induct/Com.ML	Fri May 09 10:18:58 1997 +0200
@@ -41,3 +41,19 @@
 (*SLOW (23s) due to proof reconstruction; needs 60s if thin_tac is omitted*)
 by (REPEAT (blast_tac (!claset addEs [exec_WHILE_case]) 1));
 qed "Function_exec";
+
+
+goalw thy [assign_def] "(s[v/x])x = v";
+by (Simp_tac 1);
+qed "assign_same";
+
+goalw thy [assign_def] "!!y. y~=x ==> (s[v/x])y = s y";
+by (Asm_simp_tac 1);
+qed "assign_different";
+
+goalw thy [assign_def] "s[s x/x] = s";
+br ext 1;
+by (simp_tac (!simpset setloop split_tac[expand_if]) 1);
+qed "assign_triv";
+
+Addsimps [assign_same, assign_different, assign_triv];