disambiguated := ; added Examples (factorial)
authoroheimb
Tue Jul 04 10:54:46 2000 +0200 (2000-07-04)
changeset 9241f961c1fdff50
parent 9240 f4d76cb26433
child 9242 c472ed4edded
disambiguated := ; added Examples (factorial)
src/HOL/IMP/Com.thy
src/HOL/IMP/Denotation.thy
src/HOL/IMP/Hoare.ML
src/HOL/IMP/Hoare.thy
src/HOL/IMP/Natural.ML
src/HOL/IMP/Natural.thy
src/HOL/IMP/ROOT.ML
src/HOL/IMP/Transition.ML
src/HOL/IMP/Transition.thy
src/HOL/IMP/VC.thy
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/IMP/Com.thy	Tue Jul 04 10:54:32 2000 +0200
     1.2 +++ b/src/HOL/IMP/Com.thy	Tue Jul 04 10:54:46 2000 +0200
     1.3 @@ -9,18 +9,18 @@
     1.4  
     1.5  Com = Main +
     1.6  
     1.7 -types 
     1.8 -      val
     1.9 +types
    1.10        loc
    1.11 -      state = "loc => val"
    1.12 -      aexp  = "state => val"
    1.13 +      val   = nat (* or anything else, nat used in examples *)
    1.14 +      state = loc => val
    1.15 +      aexp  = state => val
    1.16        bexp  = state => bool
    1.17  
    1.18 -arities loc,val :: term
    1.19 +arities loc :: term
    1.20  
    1.21  datatype
    1.22    com = SKIP
    1.23 -      | ":="  loc aexp         (infixl  60)
    1.24 +      | ":=="  loc aexp         (infixl  60)
    1.25        | Semi  com com          ("_; _"  [60, 60] 10)
    1.26        | Cond  bexp com com     ("IF _ THEN _ ELSE _"  60)
    1.27        | While bexp com         ("WHILE _ DO _"  60)
     2.1 --- a/src/HOL/IMP/Denotation.thy	Tue Jul 04 10:54:32 2000 +0200
     2.2 +++ b/src/HOL/IMP/Denotation.thy	Tue Jul 04 10:54:46 2000 +0200
     2.3 @@ -20,7 +20,7 @@
     2.4  
     2.5  primrec
     2.6    C_skip    "C(SKIP) = Id"
     2.7 -  C_assign  "C(x := a) = {(s,t). t = s[x:=a(s)]}"
     2.8 +  C_assign  "C(x :== a) = {(s,t). t = s[x::=a(s)]}"
     2.9    C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
    2.10    C_if      "C(IF b THEN c1 ELSE c2) = {(s,t). (s,t) : C(c1) & b(s)} Un
    2.11                                         {(s,t). (s,t) : C(c2) & ~ b(s)}"
     3.1 --- a/src/HOL/IMP/Hoare.ML	Tue Jul 04 10:54:32 2000 +0200
     3.2 +++ b/src/HOL/IMP/Hoare.ML	Tue Jul 04 10:54:46 2000 +0200
     3.3 @@ -35,7 +35,7 @@
     3.4  by (Simp_tac 1);
     3.5  qed "wp_SKIP";
     3.6  
     3.7 -Goalw [wp_def] "wp (x:=a) Q = (%s. Q(s[x:=a s]))";
     3.8 +Goalw [wp_def] "wp (x:==a) Q = (%s. Q(s[x::=a s]))";
     3.9  by (Simp_tac 1);
    3.10  qed "wp_Ass";
    3.11  
     4.1 --- a/src/HOL/IMP/Hoare.thy	Tue Jul 04 10:54:32 2000 +0200
     4.2 +++ b/src/HOL/IMP/Hoare.thy	Tue Jul 04 10:54:46 2000 +0200
     4.3 @@ -20,7 +20,7 @@
     4.4  inductive hoare
     4.5  intrs
     4.6    skip "|- {P}SKIP{P}"
     4.7 -  ass  "|- {%s. P(s[x:=a s])} x:=a {P}"
     4.8 +  ass  "|- {%s. P(s[x::=a s])} x:==a {P}"
     4.9    semi "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
    4.10    If "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
    4.11        |- {P} IF b THEN c ELSE d {Q}"
     5.1 --- a/src/HOL/IMP/Natural.ML	Tue Jul 04 10:54:32 2000 +0200
     5.2 +++ b/src/HOL/IMP/Natural.ML	Tue Jul 04 10:54:46 2000 +0200
     5.3 @@ -11,7 +11,7 @@
     5.4  val evalc_elim_cases = 
     5.5      map evalc.mk_cases
     5.6         ["<SKIP,s> -c-> t", 
     5.7 -	"<x:=a,s> -c-> t", 
     5.8 +	"<x:==a,s> -c-> t", 
     5.9  	"<c1;c2, s> -c-> t",
    5.10  	"<IF b THEN c1 ELSE c2, s> -c-> t"];
    5.11  
    5.12 @@ -23,7 +23,7 @@
    5.13  Goal "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
    5.14  by (etac evalc.induct 1);
    5.15  by (thin_tac "<?c,s2> -c-> s1" 7);
    5.16 -(*blast_tac needs Unify.search_bound, trace_bound := 40*)
    5.17 +(*blast_tac needs Unify.search_bound, trace_bound ::= 40*)
    5.18  by (ALLGOALS (best_tac (claset() addEs [evalc_WHILE_case])));
    5.19  qed_spec_mp "com_det";
    5.20  
     6.1 --- a/src/HOL/IMP/Natural.thy	Tue Jul 04 10:54:32 2000 +0200
     6.2 +++ b/src/HOL/IMP/Natural.thy	Tue Jul 04 10:54:46 2000 +0200
     6.3 @@ -16,17 +16,17 @@
     6.4  
     6.5  consts
     6.6    update  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
     6.7 -           ("_/[_/:=/_]" [900,0,0] 900)
     6.8 +           ("_/[_/::=/_]" [900,0,0] 900)
     6.9  (* update is NOT defined, only declared!
    6.10     Thus the whole theory is independent of its meaning!
    6.11 -   If theory Update is included, proofs break.
    6.12 +   If the definition (update == fun_upd) is included, proofs break.
    6.13  *)
    6.14  
    6.15  inductive evalc
    6.16    intrs
    6.17      Skip    "<SKIP,s> -c-> s"
    6.18  
    6.19 -    Assign  "<x := a,s> -c-> s[x:=a(s)]"
    6.20 +    Assign  "<x :== a,s> -c-> s[x::=a s]"
    6.21  
    6.22      Semi    "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] 
    6.23              ==> <c0 ; c1, s> -c-> s1"
     7.1 --- a/src/HOL/IMP/ROOT.ML	Tue Jul 04 10:54:32 2000 +0200
     7.2 +++ b/src/HOL/IMP/ROOT.ML	Tue Jul 04 10:54:46 2000 +0200
     7.3 @@ -7,3 +7,4 @@
     7.4  time_use_thy "Expr";
     7.5  time_use_thy "Transition";
     7.6  time_use_thy "VC";
     7.7 +time_use_thy "Examples";
     8.1 --- a/src/HOL/IMP/Transition.ML	Tue Jul 04 10:54:32 2000 +0200
     8.2 +++ b/src/HOL/IMP/Transition.ML	Tue Jul 04 10:54:46 2000 +0200
     8.3 @@ -13,7 +13,7 @@
     8.4  val evalc1_SEs = 
     8.5      map evalc1.mk_cases
     8.6         ["(SKIP,s) -1-> t", 
     8.7 -	"(x:=a,s) -1-> t",
     8.8 +	"(x:==a,s) -1-> t",
     8.9  	"(c1;c2, s) -1-> t", 
    8.10  	"(IF b THEN c1 ELSE c2, s) -1-> t",
    8.11          "(WHILE b DO c, s) -1-> t"];
     9.1 --- a/src/HOL/IMP/Transition.thy	Tue Jul 04 10:54:32 2000 +0200
     9.2 +++ b/src/HOL/IMP/Transition.thy	Tue Jul 04 10:54:46 2000 +0200
     9.3 @@ -31,7 +31,7 @@
     9.4  
     9.5  inductive evalc1
     9.6    intrs
     9.7 -    Assign "(x := a,s) -1-> (SKIP,s[x := a s])"
     9.8 +    Assign "(x :== a,s) -1-> (SKIP,s[x ::= a s])"
     9.9  
    9.10      Semi1   "(SKIP;c,s) -1-> (c,s)"     
    9.11      Semi2   "(c0,s) -1-> (c2,s1) ==> (c0;c1,s) -1-> (c2;c1,s1)"
    10.1 --- a/src/HOL/IMP/VC.thy	Tue Jul 04 10:54:32 2000 +0200
    10.2 +++ b/src/HOL/IMP/VC.thy	Tue Jul 04 10:54:46 2000 +0200
    10.3 @@ -23,7 +23,7 @@
    10.4  
    10.5  primrec
    10.6    "awp Askip Q = Q"
    10.7 -  "awp (Aass x a) Q = (%s. Q(s[x:=a s]))"
    10.8 +  "awp (Aass x a) Q = (%s. Q(s[x::=a s]))"
    10.9    "awp (Asemi c d) Q = awp c (awp d Q)"
   10.10    "awp (Aif b c d) Q = (%s. (b s-->awp c Q s) & (~b s-->awp d Q s))" 
   10.11    "awp (Awhile b I c) Q = I"
   10.12 @@ -38,7 +38,7 @@
   10.13  
   10.14  primrec
   10.15    "astrip Askip = SKIP"
   10.16 -  "astrip (Aass x a) = (x:=a)"
   10.17 +  "astrip (Aass x a) = (x:==a)"
   10.18    "astrip (Asemi c d) = (astrip c;astrip d)"
   10.19    "astrip (Aif b c d) = (IF b THEN astrip c ELSE astrip d)"
   10.20    "astrip (Awhile b I c) = (WHILE b DO astrip c)"
   10.21 @@ -46,7 +46,7 @@
   10.22  (* simultaneous computation of vc and awp: *)
   10.23  primrec
   10.24    "vcawp Askip Q = (%s. True, Q)"
   10.25 -  "vcawp (Aass x a) Q = (%s. True, %s. Q(s[x:=a s]))"
   10.26 +  "vcawp (Aass x a) Q = (%s. True, %s. Q(s[x::=a s]))"
   10.27    "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
   10.28                                (vcc,wpc) = vcawp c wpd
   10.29                            in (%s. vcc s & vcd s, wpc))"
    11.1 --- a/src/HOL/IsaMakefile	Tue Jul 04 10:54:32 2000 +0200
    11.2 +++ b/src/HOL/IsaMakefile	Tue Jul 04 10:54:46 2000 +0200
    11.3 @@ -151,7 +151,7 @@
    11.4  
    11.5  $(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Denotation.ML \
    11.6    IMP/Denotation.thy IMP/Expr.ML IMP/Expr.thy IMP/Hoare.ML IMP/Hoare.thy \
    11.7 -  IMP/Natural.ML IMP/Natural.thy IMP/ROOT.ML IMP/Transition.ML \
    11.8 +  IMP/Natural.ML IMP/Natural.thy IMP/Example.thy IMP/ROOT.ML IMP/Transition.ML \
    11.9    IMP/Transition.thy IMP/VC.ML IMP/VC.thy
   11.10  	@$(ISATOOL) usedir $(OUT)/HOL IMP
   11.11