# HG changeset patch
# User oheimb
# Date 962712296 -7200
# Node ID 22b460a0b67679173f8d2bd51e342500f3ed15bd
# Parent  c472ed4edded6de2fb234bc032326a652385fc42
disambiguated := ; added Examples (factorial)

diff -r c472ed4edded -r 22b460a0b676 src/HOL/IMP/Examples.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Examples.ML	Tue Jul 04 14:04:56 2000 +0200
@@ -0,0 +1,45 @@
+(*  Title:      HOL/IMP/Examples.ML
+    ID:         $Id$
+    Author:     David von Oheimb, TUM
+    Copyright   2000 TUM
+*)
+
+(*###should go to Fun.ML*)
+Goal "f(x:=y,a:=b,x:=z) = f(a:=b,x:=z)";
+by (rtac ext 1);
+by (Simp_tac 1);
+qed "fun_upd_upd2";
+Addsimps [fun_upd_upd2];
+
+Addsimps[update_def];
+
+section "Examples";
+
+val step = resolve_tac evalc.intrs 1;
+val simp = Asm_simp_tac 1;
+Goalw [factorial_def] "a~=b ==> \
+\ <factorial a b, Mem(a:=#3)>  -c-> Mem(b:=#6,a:=#0)";
+by (ftac not_sym 1);
+by step;
+by  step;
+by step;
+by   simp;
+by  step;
+by   step;
+by  step;
+by simp;
+by step;
+by   simp;
+by  step;
+by   step;
+by  step;
+by simp;
+by step;
+by   simp;
+by  step;
+by   step;
+by  step;
+by simp;
+by step;
+by simp;
+qed "factorial_3";
diff -r c472ed4edded -r 22b460a0b676 src/HOL/IMP/Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Examples.thy	Tue Jul 04 14:04:56 2000 +0200
@@ -0,0 +1,20 @@
+(*  Title:      HOL/IMP/Examples.thy
+    ID:         $Id$
+    Author:     David von Oheimb, TUM
+    Copyright   2000 TUM
+*)
+
+Examples = Natural +
+
+defs (* bring up the deferred definition for update *)
+
+ update_def "update == fun_upd"
+
+constdefs
+  
+  factorial :: loc => loc => com
+ "factorial a b == b :== (%s. 1);
+               WHILE (%s. s a ~= 0) DO
+                 (b :== (%s. s b * s a); a :== (%s. s a - 1))"
+  
+end