minor improvements of formulation and proofs
authoroheimb
Fri Nov 21 11:57:58 1997 +0100 (1997-11-21)
changeset 42645e21f41ccd21
parent 4263 a434327aef8b
child 4265 70fc6e05120c
minor improvements of formulation and proofs
src/HOL/Induct/Com.thy
src/HOL/Induct/Exp.ML
src/HOL/Induct/Exp.thy
     1.1 --- a/src/HOL/Induct/Com.thy	Fri Nov 21 11:54:23 1997 +0100
     1.2 +++ b/src/HOL/Induct/Com.thy	Fri Nov 21 11:57:58 1997 +0100
     1.3 @@ -34,6 +34,12 @@
     1.4  
     1.5  translations  "csig -[eval]-> s" == "(csig,s) : exec eval"
     1.6  
     1.7 +syntax  eval'   :: "[exp*state,nat*state] => 
     1.8 +		    ((exp*state) * (nat*state)) set => bool"
     1.9 +						   ("_/ -|[_]-> _" [50,0,50] 50)
    1.10 +translations
    1.11 +    "esig -|[eval]-> ns" => "(esig,ns) : eval"
    1.12 +
    1.13  constdefs assign :: [state,nat,loc] => state    ("_[_'/_]" [95,0,0] 95)
    1.14    "s[m/x] ==  (%y. if y=x then m else s y)"
    1.15  
    1.16 @@ -43,20 +49,20 @@
    1.17    intrs
    1.18      Skip    "(SKIP,s) -[eval]-> s"
    1.19  
    1.20 -    Assign  "((e,s), (v,s')) : eval ==> (x := e, s) -[eval]-> s'[v/x]"
    1.21 +    Assign  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'[v/x]"
    1.22  
    1.23      Semi    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] 
    1.24              ==> (c0 ;; c1, s) -[eval]-> s1"
    1.25  
    1.26 -    IfTrue "[| ((e,s), (0,s')) : eval;  (c0,s') -[eval]-> s1 |] 
    1.27 +    IfTrue "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |] 
    1.28              ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
    1.29  
    1.30 -    IfFalse "[| ((e,s), (1,s')) : eval;  (c1,s') -[eval]-> s1 |] 
    1.31 +    IfFalse "[| (e,s) -|[eval]->  (1,s');  (c1,s') -[eval]-> s1 |] 
    1.32               ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
    1.33  
    1.34 -    WhileFalse "((e,s), (1,s1)) : eval ==> (WHILE e DO c, s) -[eval]-> s1"
    1.35 +    WhileFalse "(e,s) -|[eval]-> (1,s1) ==> (WHILE e DO c, s) -[eval]-> s1"
    1.36  
    1.37 -    WhileTrue  "[| ((e,s), (0,s1)) : eval;
    1.38 +    WhileTrue  "[| (e,s) -|[eval]-> (0,s1);
    1.39                  (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |] 
    1.40                  ==> (WHILE e DO c, s) -[eval]-> s3"
    1.41  
     2.1 --- a/src/HOL/Induct/Exp.ML	Fri Nov 21 11:54:23 1997 +0100
     2.2 +++ b/src/HOL/Induct/Exp.ML	Fri Nov 21 11:57:58 1997 +0100
     2.3 @@ -57,7 +57,7 @@
     2.4  by (blast_tac (claset() addIs prems) 1);
     2.5  by (blast_tac (claset() addIs prems) 1);
     2.6  by (forward_tac [impOfSubs (Int_lower1 RS exec_mono)] 1);
     2.7 -by (fast_tac (claset() addIs prems addss (simpset() addsimps [split_lemma])) 1);
     2.8 +by (auto_tac (claset() addIs prems,simpset() addsimps [split_lemma]));
     2.9  qed "eval_induct";
    2.10  
    2.11  
    2.12 @@ -87,10 +87,9 @@
    2.13  
    2.14  
    2.15  (*Expression evaluation is functional, or deterministic*)
    2.16 -goal thy "Function eval";
    2.17 -by (simp_tac (simpset() addsimps [Function_def]) 1);
    2.18 -by (REPEAT (rtac allI 1));
    2.19 -by (rtac impI 1);
    2.20 +goalw thy [Function_def] "Function eval";
    2.21 +by (strip_tac 1);
    2.22 +by (split_all_tac 1);
    2.23  by (etac eval_induct 1);
    2.24  by (dtac com_Unique 4);
    2.25  by (ALLGOALS (full_simp_tac (simpset() addsimps [Unique_def])));
     3.1 --- a/src/HOL/Induct/Exp.thy	Fri Nov 21 11:54:23 1997 +0100
     3.2 +++ b/src/HOL/Induct/Exp.thy	Fri Nov 21 11:57:58 1997 +0100
     3.3 @@ -13,7 +13,7 @@
     3.4         "-|->"   :: "[exp*state,nat*state] => bool"         (infixl 50)
     3.5  translations
     3.6      "esig -|-> (n,s)" <= "(esig,n,s) : eval"
     3.7 -    "esig -|-> ns"    == "(esig,ns) : eval"
     3.8 +    "esig -|-> ns"    == "(esig,ns ) : eval"
     3.9    
    3.10  inductive eval
    3.11    intrs