Natural and Transition semantics.
authornipkow
Mon Apr 29 15:48:27 1996 +0200 (1996-04-29)
changeset 1700afd3b60660db
parent 1699 0bcc8cab3461
child 1701 a26fbeaaaabd
Natural and Transition semantics.
src/HOL/IMP/Natural.ML
src/HOL/IMP/Natural.thy
src/HOL/IMP/Transition.ML
src/HOL/IMP/Transition.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/IMP/Natural.ML	Mon Apr 29 15:48:27 1996 +0200
     1.3 @@ -0,0 +1,23 @@
     1.4 +(*  Title:      HOL/IMP/Natural.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow & Larry Paulson, TUM
     1.7 +    Copyright   1996 TUM
     1.8 +*)
     1.9 +
    1.10 +open Natural;
    1.11 +
    1.12 +val evalc_elim_cases = map (evalc.mk_cases com.simps)
    1.13 +   ["<SKIP,s> -c-> t", "<x:=a,s> -c-> t", "<c1;c2, s> -c-> t",
    1.14 +    "<IF b THEN c1 ELSE c2, s> -c-> t"];
    1.15 +
    1.16 +val evalc_WHILE_case = evalc.mk_cases com.simps "<WHILE b DO c,s> -c-> t";
    1.17 +
    1.18 +val evalc_cs = set_cs addSEs evalc_elim_cases
    1.19 +                      addEs  [evalc_WHILE_case];
    1.20 +
    1.21 +(* evaluation of com is deterministic *)
    1.22 +goal Natural.thy "!c s t. <c,s> -c-> t --> (!u. <c,s> -c-> u --> u=t)";
    1.23 +by (rtac evalc.mutual_induct 1);
    1.24 +by (eres_inst_tac [("V", "<?c,s2> -c-> s1")] thin_rl 7);
    1.25 +by (ALLGOALS (deepen_tac evalc_cs 4));
    1.26 +qed_spec_mp "com_det";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/IMP/Natural.thy	Mon Apr 29 15:48:27 1996 +0200
     2.3 @@ -0,0 +1,41 @@
     2.4 +(*  Title:      HOL/IMP/Natural.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Tobias Nipkow & Robert Sandner, TUM
     2.7 +    Copyright   1996 TUM
     2.8 +
     2.9 +Natural semantics of commands
    2.10 +*)
    2.11 +
    2.12 +Natural = Com +
    2.13 +
    2.14 +(** Execution of commands **)
    2.15 +consts  evalc    :: "(com*state*state)set"
    2.16 +        "@evalc" :: [com,state,state] => bool ("<_,_>/ -c-> _" [0,0,50] 50)
    2.17 +
    2.18 +translations  "<ce,sig> -c-> s" == "(ce,sig,s) : evalc"
    2.19 +
    2.20 +constdefs assign :: [state,val,loc] => state    ("_[_'/_]" [95,0,0] 95)
    2.21 +  "s[m/x] ==  (%y. if y=x then m else s y)"
    2.22 +
    2.23 +
    2.24 +inductive "evalc"
    2.25 +  intrs
    2.26 +    Skip    "<SKIP,s> -c-> s"
    2.27 +
    2.28 +    Assign  "<x := a,s> -c-> s[a(s)/x]"
    2.29 +
    2.30 +    Semi    "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] 
    2.31 +            ==> <c0 ; c1, s> -c-> s1"
    2.32 +
    2.33 +    IfTrue "[| b s; <c0,s> -c-> s1 |] 
    2.34 +            ==> <IF b THEN c0 ELSE c1, s> -c-> s1"
    2.35 +
    2.36 +    IfFalse "[| ~b s; <c1,s> -c-> s1 |] 
    2.37 +             ==> <IF b THEN c0 ELSE c1, s> -c-> s1"
    2.38 +
    2.39 +    WhileFalse "~b s ==> <WHILE b DO c,s> -c-> s"
    2.40 +
    2.41 +    WhileTrue  "[| b s;  <c,s> -c-> s2;  <WHILE b DO c, s2> -c-> s1 |] 
    2.42 +               ==> <WHILE b DO c, s> -c-> s1"
    2.43 +
    2.44 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/IMP/Transition.ML	Mon Apr 29 15:48:27 1996 +0200
     3.3 @@ -0,0 +1,123 @@
     3.4 +(*  Title:      HOL/IMP/Transition.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Tobias Nipkow & Robert Sandner, TUM
     3.7 +    Copyright   1996 TUM
     3.8 +
     3.9 +Equivalence of Natural and Transition semantics
    3.10 +*)
    3.11 +
    3.12 +open Transition;
    3.13 +
    3.14 +val relpow_cs = rel_cs addSEs [rel_pow_0_E];
    3.15 +
    3.16 +val evalc1_elim_cases = map (evalc1.mk_cases com.simps)
    3.17 +   ["(SKIP,s) -1-> t", "(x:=a,s) -1-> t", "(c1;c2, s) -1-> t",
    3.18 +    "(IF b THEN c1 ELSE c2, s) -1-> t", "(WHILE b DO c,s) -1-> t"];
    3.19 +
    3.20 +val evalc1_cs = relpow_cs addIs (evalc.intrs@evalc1.intrs);
    3.21 +
    3.22 +goal Transition.thy "!!c. (c,s) -(0)-> (SKIP,u) ==> c = SKIP & s = u";
    3.23 +by(fast_tac evalc1_cs 1);
    3.24 +val hlemma1 = result();
    3.25 +
    3.26 +goal Transition.thy "!!s. (SKIP,s) -(m)-> (SKIP,t) ==> s = t & m = 0";
    3.27 +be rel_pow_E2 1;
    3.28 +by (Asm_full_simp_tac 1);
    3.29 +by (eresolve_tac evalc1_elim_cases 1);
    3.30 +val hlemma2 = result();
    3.31 +
    3.32 +
    3.33 +goal Transition.thy
    3.34 +  "!s t u c d. (c,s) -(n)-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \
    3.35 +\              (c;d, s) -*-> (SKIP, u)";
    3.36 +by(nat_ind_tac "n" 1);
    3.37 + (* case n = 0 *)
    3.38 + by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2])1);
    3.39 +(* induction step *)
    3.40 +by (safe_tac (HOL_cs addSDs [rel_pow_Suc_D2]));
    3.41 +by(split_all_tac 1);
    3.42 +by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1);
    3.43 +qed_spec_mp "lemma1";
    3.44 +
    3.45 +
    3.46 +goal Transition.thy "!c s s1. <c,s> -c-> s1 --> (c,s) -*-> (SKIP,s1)";
    3.47 +br evalc.mutual_induct 1;
    3.48 +
    3.49 +(* SKIP *)
    3.50 +br rtrancl_refl 1;
    3.51 +
    3.52 +(* ASSIGN *)
    3.53 +by (fast_tac (evalc1_cs addSIs [r_into_rtrancl]) 1);
    3.54 +
    3.55 +(* SEMI *)
    3.56 +by (fast_tac (set_cs addDs [rtrancl_imp_UN_rel_pow] addIs [lemma1]) 1);
    3.57 +
    3.58 +(* IF *)
    3.59 +by (fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1);
    3.60 +by (fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1);
    3.61 +
    3.62 +(* WHILE *)
    3.63 +by (fast_tac (evalc1_cs addSIs [r_into_rtrancl]) 1);
    3.64 +by (fast_tac (evalc1_cs addDs [rtrancl_imp_UN_rel_pow]
    3.65 +                        addIs [rtrancl_into_rtrancl2,lemma1]) 1);
    3.66 +
    3.67 +qed_spec_mp "evalc_impl_evalc1";
    3.68 +
    3.69 +
    3.70 +goal Transition.thy
    3.71 +  "!c d s u. (c;d,s) -(n)-> (SKIP,u) --> \
    3.72 +\            (? t m. (c,s) -*-> (SKIP,t) & (d,t) -(m)-> (SKIP,u) & m <= n)";
    3.73 +by(nat_ind_tac "n" 1);
    3.74 + (* case n = 0 *)
    3.75 + by (fast_tac (HOL_cs addSDs [hlemma1] addss !simpset) 1);
    3.76 +(* induction step *)
    3.77 +by (fast_tac (HOL_cs addSIs [rtrancl_refl,le_SucI,le_refl]
    3.78 +                     addSDs [rel_pow_Suc_D2]
    3.79 +                     addSEs (evalc1_elim_cases@
    3.80 +                             [rel_pow_imp_rtrancl,rtrancl_into_rtrancl2])) 1);
    3.81 +qed_spec_mp "lemma2";
    3.82 +
    3.83 +goal Transition.thy "!s t. (c,s) -*-> (SKIP,t) --> <c,s> -c-> t";
    3.84 +by (com.induct_tac "c" 1);
    3.85 +by (safe_tac (evalc1_cs addSDs [rtrancl_imp_UN_rel_pow]));
    3.86 +
    3.87 +(* SKIP *)
    3.88 +by (fast_tac (evalc1_cs addSEs rel_pow_E2::evalc1_elim_cases) 1);
    3.89 +
    3.90 +(* ASSIGN *)
    3.91 +by (fast_tac (evalc1_cs addSDs [hlemma2]
    3.92 +                        addSEs rel_pow_E2::evalc1_elim_cases
    3.93 +                        addss !simpset) 1);
    3.94 +
    3.95 +(* SEMI *)
    3.96 +by (fast_tac (evalc1_cs addSDs [lemma2,rel_pow_imp_rtrancl]) 1);
    3.97 +
    3.98 +(* IF *)
    3.99 +be rel_pow_E2 1;
   3.100 +by (Asm_full_simp_tac 1);
   3.101 +by (fast_tac (evalc1_cs addSDs[rel_pow_imp_rtrancl]addEs evalc1_elim_cases) 1);
   3.102 +
   3.103 +(* WHILE, induction on the length of the computation *)
   3.104 +by(rotate_tac 1 1);
   3.105 +by (etac rev_mp 1);
   3.106 +by (res_inst_tac [("x","s")] spec 1);
   3.107 +by(res_inst_tac [("n","n")] less_induct 1);
   3.108 +by (strip_tac 1);
   3.109 +be rel_pow_E2 1;
   3.110 + by (Asm_full_simp_tac 1);
   3.111 +by (eresolve_tac evalc1_elim_cases 1);
   3.112 +
   3.113 +(* WhileFalse *)
   3.114 + by (fast_tac (evalc1_cs addSDs [hlemma2]) 1);
   3.115 +
   3.116 +(* WhileTrue *)
   3.117 +by(fast_tac(evalc1_cs addSDs[lemma2,le_imp_less_or_eq,less_Suc_eq RS iffD2])1);
   3.118 +
   3.119 +qed_spec_mp "evalc1_impl_evalc";
   3.120 +
   3.121 +
   3.122 +(**** proof of the equivalence of evalc and evalc1 ****)
   3.123 +
   3.124 +goal Transition.thy "((c, s) -*-> (SKIP, t)) = (<c,s> -c-> t)";
   3.125 +by (fast_tac (HOL_cs addSEs [evalc1_impl_evalc,evalc_impl_evalc1]) 1);
   3.126 +qed "evalc1_eq_evalc";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/IMP/Transition.thy	Mon Apr 29 15:48:27 1996 +0200
     4.3 @@ -0,0 +1,40 @@
     4.4 +(*  Title:      HOL/IMP/Transition.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Tobias Nipkow & Robert Sandner, TUM
     4.7 +    Copyright   1996 TUM
     4.8 +
     4.9 +Transition semantics of commands
    4.10 +*)
    4.11 +
    4.12 +Transition = Natural + RelPow +
    4.13 +
    4.14 +consts  evalc1    :: "((com*state)*(com*state))set"        
    4.15 +	"@evalc1" :: "[(com*state),(com*state)] => bool"   
    4.16 +				("_ -1-> _" [81,81] 100)
    4.17 +	"@evalcn" :: "[(com*state),(com*state)] => nat => bool"
    4.18 +				("_ -(_)-> _" [81,81] 100)
    4.19 +	"@evalc*" :: "[(com*state),(com*state)] => bool"   
    4.20 +				("_ -*-> _" [81,81] 100)
    4.21 +
    4.22 +translations
    4.23 +       	"cs0 -1-> cs1" == "(cs0,cs1) : evalc1"
    4.24 +        "x -(n)-> (y,z)" == "(x,y,z) : evalc1 ^ n" 
    4.25 +	"cs0 -(n)-> cs1" == "(cs0,cs1) : evalc1 ^ n"
    4.26 +	"x -*-> (y,z)" == "(x,y,z) : evalc1 ^*" 
    4.27 +	"cs0 -*-> cs1" == "(cs0,cs1) : evalc1 ^*"
    4.28 +
    4.29 +
    4.30 +inductive "evalc1"
    4.31 +  intrs
    4.32 +    Assign "(x := a,s) -1-> (SKIP,s[a s / x])"
    4.33 +
    4.34 +    Semi1   "(SKIP;c,s) -1-> (c,s)"	
    4.35 +    Semi2   "(c0,s) -1-> (c2,s1) ==> (c0;c1,s) -1-> (c2;c1,s1)"
    4.36 +
    4.37 +    IfTrue "b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c1,s)"
    4.38 +    IfFalse "~b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c2,s)"
    4.39 +
    4.40 +    WhileFalse "~b s ==> (WHILE b DO c,s) -1-> (SKIP,s)"
    4.41 +    WhileTrue "b s ==> (WHILE b DO c,s) -1-> (c;WHILE b DO c,s)"
    4.42 +
    4.43 +end