disambiguated := ; added Examples (factorial)
authoroheimb
Tue Jul 04 14:04:56 2000 +0200 (2000-07-04)
changeset 924322b460a0b676
parent 9242 c472ed4edded
child 9244 7edd3e5f26d4
disambiguated := ; added Examples (factorial)
src/HOL/IMP/Examples.ML
src/HOL/IMP/Examples.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/IMP/Examples.ML	Tue Jul 04 14:04:56 2000 +0200
     1.3 @@ -0,0 +1,45 @@
     1.4 +(*  Title:      HOL/IMP/Examples.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     David von Oheimb, TUM
     1.7 +    Copyright   2000 TUM
     1.8 +*)
     1.9 +
    1.10 +(*###should go to Fun.ML*)
    1.11 +Goal "f(x:=y,a:=b,x:=z) = f(a:=b,x:=z)";
    1.12 +by (rtac ext 1);
    1.13 +by (Simp_tac 1);
    1.14 +qed "fun_upd_upd2";
    1.15 +Addsimps [fun_upd_upd2];
    1.16 +
    1.17 +Addsimps[update_def];
    1.18 +
    1.19 +section "Examples";
    1.20 +
    1.21 +val step = resolve_tac evalc.intrs 1;
    1.22 +val simp = Asm_simp_tac 1;
    1.23 +Goalw [factorial_def] "a~=b ==> \
    1.24 +\ <factorial a b, Mem(a:=#3)>  -c-> Mem(b:=#6,a:=#0)";
    1.25 +by (ftac not_sym 1);
    1.26 +by step;
    1.27 +by  step;
    1.28 +by step;
    1.29 +by   simp;
    1.30 +by  step;
    1.31 +by   step;
    1.32 +by  step;
    1.33 +by simp;
    1.34 +by step;
    1.35 +by   simp;
    1.36 +by  step;
    1.37 +by   step;
    1.38 +by  step;
    1.39 +by simp;
    1.40 +by step;
    1.41 +by   simp;
    1.42 +by  step;
    1.43 +by   step;
    1.44 +by  step;
    1.45 +by simp;
    1.46 +by step;
    1.47 +by simp;
    1.48 +qed "factorial_3";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/IMP/Examples.thy	Tue Jul 04 14:04:56 2000 +0200
     2.3 @@ -0,0 +1,20 @@
     2.4 +(*  Title:      HOL/IMP/Examples.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     David von Oheimb, TUM
     2.7 +    Copyright   2000 TUM
     2.8 +*)
     2.9 +
    2.10 +Examples = Natural +
    2.11 +
    2.12 +defs (* bring up the deferred definition for update *)
    2.13 +
    2.14 + update_def "update == fun_upd"
    2.15 +
    2.16 +constdefs
    2.17 +  
    2.18 +  factorial :: loc => loc => com
    2.19 + "factorial a b == b :== (%s. 1);
    2.20 +               WHILE (%s. s a ~= 0) DO
    2.21 +                 (b :== (%s. s b * s a); a :== (%s. s a - 1))"
    2.22 +  
    2.23 +end