new version of HOL/IMP with curried function application
authorclasohm
Fri Mar 03 12:04:16 1995 +0100 (1995-03-03)
changeset 924806721cfbf46
parent 923 ff1574a81019
child 925 15539deb6863
new version of HOL/IMP with curried function application
src/HOL/IMP/Com.ML
src/HOL/IMP/Com.thy
src/HOL/IMP/Denotation.ML
src/HOL/IMP/Denotation.thy
src/HOL/IMP/Equiv.ML
src/HOL/IMP/Equiv.thy
src/HOL/IMP/Properties.ML
src/HOL/IMP/Properties.thy
src/HOL/IMP/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/IMP/Com.ML	Fri Mar 03 12:04:16 1995 +0100
     1.3 @@ -0,0 +1,30 @@
     1.4 +(*  Title: 	HOL/IMP/Com.ML
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
     1.7 +    Copyright   1994 TUM
     1.8 +*)
     1.9 +
    1.10 +open Com;
    1.11 +
    1.12 +val evala_elim_cases = map (evala.mk_cases aexp.simps)
    1.13 +   ["<N(n),sigma> -a-> i", "<X(x),sigma> -a-> i",
    1.14 +    "<Op1 f e,sigma> -a-> i", "<Op2 f a1 a2,sigma>  -a-> i"
    1.15 +   ];
    1.16 +
    1.17 +val evalb_elim_cases = map (evalb.mk_cases bexp.simps)
    1.18 +   ["<true,sigma> -b-> x", "<false,sigma> -b-> x",
    1.19 +    "<ROp f a0 a1,sigma> -b-> x", "<noti(b),sigma> -b-> x",
    1.20 +    "<b0 andi b1,sigma> -b-> x", "<b0 ori b1,sigma> -b-> x"
    1.21 +   ];
    1.22 +
    1.23 +val evalb_simps = map (fn s => prove_goal Com.thy s
    1.24 +    (fn _ => [fast_tac (HOL_cs addSIs evalb.intrs addSEs evalb_elim_cases) 1]))
    1.25 +  ["(<true,sigma> -b-> w) = (w=True)",
    1.26 +   "(<false,sigma> -b-> w) = (w=False)",
    1.27 +   "(<ROp f a0 a1,sigma> -b-> w) = \
    1.28 +\   (? m. <a0,sigma> -a-> m & (? n. <a1,sigma> -a-> n & w = f m n))",
    1.29 +   "(<noti(b),sigma> -b-> w) = (? x. <b,sigma> -b-> x & w = (~x))",
    1.30 +   "(<b0 andi b1,sigma> -b-> w) = \
    1.31 +\   (? x. <b0,sigma> -b-> x & (? y. <b1,sigma> -b-> y & w = (x&y)))",
    1.32 +   "(<b0 ori b1,sigma> -b-> w) = \
    1.33 +\   (? x. <b0,sigma> -b-> x & (? y. <b1,sigma> -b-> y & w = (x|y)))"];
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/IMP/Com.thy	Fri Mar 03 12:04:16 1995 +0100
     2.3 @@ -0,0 +1,112 @@
     2.4 +(*  Title: 	HOL/IMP/Com.thy
     2.5 +    ID:         $Id$
     2.6 +    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
     2.7 +    Copyright   1994 TUM
     2.8 +
     2.9 +Arithmetic expressions, Boolean expressions, Commands
    2.10 +
    2.11 +And their Operational semantics
    2.12 +*)
    2.13 +
    2.14 +Com = Arith +
    2.15 +
    2.16 +(** Arithmetic expressions **)
    2.17 +types loc
    2.18 +      state = "loc => nat"
    2.19 +      n2n = "nat => nat"
    2.20 +      n2n2n = "nat => nat => nat"
    2.21 +
    2.22 +arities loc :: term
    2.23 +
    2.24 +datatype
    2.25 +  aexp = N (nat)
    2.26 +       | X (loc)
    2.27 +       | Op1 (n2n, aexp)
    2.28 +       | Op2 (n2n2n, aexp, aexp)
    2.29 +
    2.30 +(** Evaluation of arithmetic expressions **)
    2.31 +consts  evala    :: "(aexp*state*nat)set"
    2.32 +       "@evala"  :: "[aexp,state,nat] => bool"	("<_,_>/ -a-> _"  [0,0,50] 50)
    2.33 +translations
    2.34 +    "<ae,sig> -a-> n" == "<ae,sig,n> : evala"
    2.35 +inductive "evala"
    2.36 +  intrs 
    2.37 +    N   "<N(n),s> -a-> n"
    2.38 +    X  	"<X(x),s> -a-> s(x)"
    2.39 +    Op1 "<e,s> -a-> n ==> <Op1 f e,s> -a-> f(n)"
    2.40 +    Op2 "[| <e0,s> -a-> n0;  <e1,s>  -a-> n1 |] \
    2.41 +\           ==> <Op2 f e0 e1,s> -a-> f n0 n1"
    2.42 +
    2.43 +types n2n2b = "[nat,nat] => bool"
    2.44 +
    2.45 +(** Boolean expressions **)
    2.46 +
    2.47 +datatype
    2.48 +  bexp = true
    2.49 +       | false
    2.50 +       | ROp  (n2n2b, aexp, aexp)
    2.51 +       | noti (bexp)
    2.52 +       | andi (bexp,bexp)	(infixl 60)
    2.53 +       | ori  (bexp,bexp)	(infixl 60)
    2.54 +
    2.55 +(** Evaluation of boolean expressions **)
    2.56 +consts evalb	:: "(bexp*state*bool)set"	
    2.57 +       "@evalb" :: "[bexp,state,bool] => bool"	("<_,_>/ -b-> _"  [0,0,50] 50)
    2.58 +
    2.59 +translations
    2.60 +    "<be,sig> -b-> b" == "<be,sig,b> : evalb"
    2.61 +
    2.62 +inductive "evalb"
    2.63 + intrs (*avoid clash with ML constructors true, false*)
    2.64 +    tru   "<true,s> -b-> True"
    2.65 +    fls   "<false,s> -b-> False"
    2.66 +    ROp   "[| <a0,s> -a-> n0; <a1,s> -a-> n1 |] \
    2.67 +\	   ==> <ROp f a0 a1,s> -b-> f n0 n1"
    2.68 +    noti  "<b,s> -b-> w ==> <noti(b),s> -b-> (~w)"
    2.69 +    andi  "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] \
    2.70 +\          ==> <b0 andi b1,s> -b-> (w0 & w1)"
    2.71 +    ori   "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] \
    2.72 +\	    ==> <b0 ori b1,s> -b-> (w0 | w1)"
    2.73 +
    2.74 +(** Commands **)
    2.75 +
    2.76 +datatype
    2.77 +  com = skip
    2.78 +      | ":="   (loc,aexp)	 (infixl  60)
    2.79 +      | semic  (com,com)	 ("_; _"  [60, 60] 10)
    2.80 +      | whileC (bexp,com)	 ("while _ do _"  60)
    2.81 +      | ifC    (bexp, com, com)	 ("ifc _ then _ else _"  60)
    2.82 +
    2.83 +(** Execution of commands **)
    2.84 +consts  evalc    :: "(com*state*state)set"
    2.85 +        "@evalc" :: "[com,state,state] => bool"  ("<_,_>/ -c-> _" [0,0,50] 50)
    2.86 +	"assign" :: "[state,nat,loc] => state"   ("_[_'/_]"       [95,0,0] 95)
    2.87 +
    2.88 +translations
    2.89 +       "<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
    2.90 +
    2.91 +rules 
    2.92 +	assign_def	"s[m/x] == (%y. if (y=x) m (s y))"
    2.93 +
    2.94 +inductive "evalc"
    2.95 +  intrs
    2.96 +    skip    "<skip,s> -c-> s"
    2.97 +
    2.98 +    assign  "<a,s> -a-> m ==> <x := a,s> -c-> s[m/x]"
    2.99 +
   2.100 +    semi    "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] \
   2.101 +\            ==> <c0 ; c1, s> -c-> s1"
   2.102 +
   2.103 +    ifcTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] \
   2.104 +\            ==> <ifc b then c0 else c1, s> -c-> s1"
   2.105 +
   2.106 +    ifcFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] \
   2.107 +\             ==> <ifc b then c0 else c1, s> -c-> s1"
   2.108 +
   2.109 +    whileFalse "<b, s> -b-> False ==> <while b do c,s> -c-> s"
   2.110 +
   2.111 +    whileTrue  "[| <b,s> -b-> True; <c,s> -c-> s2; \
   2.112 +\                  <while b do c, s2> -c-> s1 |] \
   2.113 +\               ==> <while b do c, s> -c-> s1 "
   2.114 + 
   2.115 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/IMP/Denotation.ML	Fri Mar 03 12:04:16 1995 +0100
     3.3 @@ -0,0 +1,24 @@
     3.4 +(*  Title: 	HOL/IMP/Denotation.ML
     3.5 +    ID:         $Id$
     3.6 +    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
     3.7 +    Copyright   1994 TUM
     3.8 +*)
     3.9 +
    3.10 +open Denotation;
    3.11 +
    3.12 +(**** Rewrite Rules for A,B,C ****)
    3.13 +
    3.14 +val A_simps =
    3.15 +     [A_nat,A_loc,A_op1,A_op2];
    3.16 +
    3.17 +val B_simps = map (fn t => t RS eq_reflection)
    3.18 +     [B_true,B_false,B_op,B_not,B_and,B_or]
    3.19 +
    3.20 +val C_simps = map (fn t => t RS eq_reflection)
    3.21 +  [C_skip,C_assign,C_comp,C_if,C_while]; 
    3.22 +
    3.23 +(**** mono (Gamma(b,c)) ****)
    3.24 +
    3.25 +qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def]
    3.26 +	"mono (Gamma b c)"
    3.27 +     (fn _ => [(best_tac comp_cs 1)]);
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/IMP/Denotation.thy	Fri Mar 03 12:04:16 1995 +0100
     4.3 @@ -0,0 +1,46 @@
     4.4 +(*  Title: 	HOL/IMP/Denotation.thy
     4.5 +    ID:         $Id$
     4.6 +    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
     4.7 +    Copyright   1994 TUM
     4.8 +
     4.9 +Denotational semantics of expressions & commands
    4.10 +*)
    4.11 +
    4.12 +Denotation = Com + 
    4.13 +
    4.14 +types com_den = "(state*state)set"
    4.15 +consts
    4.16 +  A     :: "aexp => state => nat"
    4.17 +  B     :: "bexp => state => bool"
    4.18 +  C     :: "com => com_den"
    4.19 +  Gamma :: "[bexp,com_den] => (com_den => com_den)"
    4.20 +
    4.21 +primrec A aexp
    4.22 +  A_nat	"A(N(n)) = (%s. n)"
    4.23 +  A_loc	"A(X(x)) = (%s. s(x))" 
    4.24 +  A_op1	"A(Op1 f a) = (%s. f(A a s))"
    4.25 +  A_op2	"A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
    4.26 +
    4.27 +primrec B bexp
    4.28 +  B_true  "B(true) = (%s. True)"
    4.29 +  B_false "B(false) = (%s. False)"
    4.30 +  B_op	  "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))" 
    4.31 +  B_not	  "B(noti(b)) = (%s. ~(B b s))"
    4.32 +  B_and	  "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
    4.33 +  B_or	  "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
    4.34 +
    4.35 +defs
    4.36 +  Gamma_def	"Gamma b cd ==   \
    4.37 +\		   (%phi.{st. st : (phi O cd) & B b (fst st)} Un \
    4.38 +\	                 {st. st : id & ~B b (fst st)})"
    4.39 +
    4.40 +primrec C com
    4.41 +  C_skip    "C(skip) = id"
    4.42 +  C_assign  "C(x := a) = {st . snd(st) = fst(st)[A a (fst st)/x]}"
    4.43 +  C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
    4.44 +  C_if	    "C(ifc b then c0 else c1) =   \
    4.45 +\		   {st. st:C(c0) & (B b (fst st))} Un \
    4.46 +\	           {st. st:C(c1) & ~(B b (fst st))}"
    4.47 +  C_while   "C(while b do c) = lfp (Gamma b (C c))"
    4.48 +
    4.49 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/IMP/Equiv.ML	Fri Mar 03 12:04:16 1995 +0100
     5.3 @@ -0,0 +1,85 @@
     5.4 +(*  Title: 	HOL/IMP/Equiv.ML
     5.5 +    ID:         $Id$
     5.6 +    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
     5.7 +    Copyright   1994 TUM
     5.8 +*)
     5.9 +
    5.10 +goal Equiv.thy "!n. (<a,s> -a-> n) = (n = A a s)";
    5.11 +by (aexp.induct_tac "a" 1);                		  (* struct. ind. *)
    5.12 +by (ALLGOALS(simp_tac (HOL_ss addsimps A_simps)));	  (* rewr. Den.   *)
    5.13 +by (TRYALL (fast_tac (set_cs addSIs (evala.intrs@prems)
    5.14 +                             addSEs evala_elim_cases)));
    5.15 +bind_thm("aexp_iff", result() RS spec);
    5.16 +
    5.17 +goal Equiv.thy "!w. (<b,s> -b-> w) = (w = B b s)";
    5.18 +by (bexp.induct_tac "b" 1);
    5.19 +by (ALLGOALS(asm_simp_tac (HOL_ss addcongs [conj_cong]
    5.20 +              addsimps (aexp_iff::B_simps@evalb_simps))));
    5.21 +bind_thm("bexp_iff", result() RS spec);
    5.22 +
    5.23 +val bexp1 = bexp_iff RS iffD1;
    5.24 +val bexp2 = bexp_iff RS iffD2;
    5.25 +
    5.26 +val BfstI = read_instantiate_sg (sign_of Equiv.thy)
    5.27 +              [("P","%x.B ?b x")] (fst_conv RS ssubst);
    5.28 +val BfstD = read_instantiate_sg (sign_of Equiv.thy)
    5.29 +              [("P","%x.B ?b x")] (fst_conv RS subst);
    5.30 +
    5.31 +goal Equiv.thy "!!c. <c,s> -c-> t ==> <s,t> : C(c)";
    5.32 +
    5.33 +(* start with rule induction *)
    5.34 +be (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1;
    5.35 +by (rewrite_tac (Gamma_def::C_simps));
    5.36 +  (* simplification with HOL_ss again too agressive *)
    5.37 +(* skip *)
    5.38 +by (fast_tac comp_cs 1);
    5.39 +(* assign *)
    5.40 +by (asm_full_simp_tac (prod_ss addsimps [aexp_iff]) 1);
    5.41 +(* comp *)
    5.42 +by (fast_tac comp_cs 1);
    5.43 +(* if *)
    5.44 +by(fast_tac (set_cs addSIs [BfstI] addSDs [BfstD,bexp1]) 1);
    5.45 +by(fast_tac (set_cs addSIs [BfstI] addSDs [BfstD,bexp1]) 1);
    5.46 +(* while *)
    5.47 +by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1);
    5.48 +by (fast_tac (comp_cs addSIs [bexp1,BfstI] addSDs [BfstD,bexp1]) 1);
    5.49 +by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1);
    5.50 +by (fast_tac (comp_cs addSIs [bexp1,BfstI] addSDs [BfstD,bexp1]) 1);
    5.51 +
    5.52 +qed "com1";
    5.53 +
    5.54 +
    5.55 +val com_ss = prod_ss addsimps (aexp_iff::bexp_iff::evalc.intrs);
    5.56 +
    5.57 +goal Equiv.thy "!io:C(c). <c,fst(io)> -c-> snd(io)";
    5.58 +by (com.induct_tac "c" 1);
    5.59 +by (rewrite_tac C_simps);
    5.60 +by (safe_tac comp_cs);
    5.61 +by (ALLGOALS (asm_full_simp_tac com_ss));
    5.62 +
    5.63 +(* comp *)
    5.64 +by (REPEAT (EVERY [(dtac bspec 1),(atac 1)]));
    5.65 +by (asm_full_simp_tac com_ss 1);
    5.66 +
    5.67 +(* while *)
    5.68 +by (etac (Gamma_mono RSN (2,induct)) 1);
    5.69 +by (rewrite_goals_tac [Gamma_def]);  
    5.70 +by (safe_tac comp_cs);
    5.71 +by (EVERY1 [dtac bspec, atac]);
    5.72 +by (ALLGOALS (asm_full_simp_tac com_ss));
    5.73 +
    5.74 +qed "com2";
    5.75 +
    5.76 +
    5.77 +(**** Proof of Equivalence ****)
    5.78 +
    5.79 +val com_iff_cs = set_cs addEs [com2 RS bspec] addDs [com1];
    5.80 +
    5.81 +goal Equiv.thy "C(c) = {io . <c,fst(io)> -c-> snd(io)}";
    5.82 +by (rtac equalityI 1);
    5.83 +(* => *)
    5.84 +by (fast_tac com_iff_cs 1);
    5.85 +(* <= *)
    5.86 +by (REPEAT (step_tac com_iff_cs 1));
    5.87 +by (asm_full_simp_tac (prod_ss addsimps [surjective_pairing RS sym])1);
    5.88 +qed "com_equivalence";
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/IMP/Equiv.thy	Fri Mar 03 12:04:16 1995 +0100
     6.3 @@ -0,0 +1,7 @@
     6.4 +(*  Title: 	HOL/IMP/Equiv.thy
     6.5 +    ID:         $Id$
     6.6 +    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
     6.7 +    Copyright   1994 TUM
     6.8 +*)
     6.9 +
    6.10 +Equiv = Denotation
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/IMP/Properties.ML	Fri Mar 03 12:04:16 1995 +0100
     7.3 @@ -0,0 +1,41 @@
     7.4 +(*  Title: 	HOL/IMP/Properties.ML
     7.5 +    ID:         $Id$
     7.6 +    Author: 	Tobias Nipkow, TUM
     7.7 +    Copyright   1994 TUM
     7.8 +
     7.9 +IMP is deterministic.
    7.10 +*)
    7.11 +
    7.12 +(* evaluation of aexp is deterministic *)
    7.13 +goal Com.thy "!m n. <a,s> -a-> m & <a,s> -a-> n --> m=n";
    7.14 +by(res_inst_tac[("aexp","a")]Com.aexp.induct 1);
    7.15 +by(REPEAT(fast_tac (HOL_cs addSIs evala.intrs addSEs evala_elim_cases) 1));
    7.16 +bind_thm("aexp_detD", conjI RS (result() RS spec RS spec RS mp));
    7.17 +
    7.18 +(* evaluation of bexp is deterministic *)
    7.19 +goal Com.thy "!v w. <b,s> -b-> v & <b,s> -b-> w --> v=w";
    7.20 +by(res_inst_tac[("bexp","b")]Com.bexp.induct 1);
    7.21 +by(REPEAT(fast_tac (HOL_cs addSIs evalb.intrs addSEs evalb_elim_cases
    7.22 +                           addDs [aexp_detD]) 1));
    7.23 +bind_thm("bexp_detD", conjI RS (result() RS spec RS spec RS mp));
    7.24 +
    7.25 +
    7.26 +val evalc_elim_cases = map (evalc.mk_cases com.simps)
    7.27 +   ["<skip,s> -c-> t", "<x:=a,s> -c-> t", "<c1;c2, s> -c-> t",
    7.28 +    "<ifc b then c1 else c2, s> -c-> t", "<while b do c,s> -c-> t"];
    7.29 +
    7.30 +(* evaluation of com is deterministic *)
    7.31 +goal Com.thy "!!c. <c,s> -c-> t ==> !u. <c,s> -c-> u --> u=t";
    7.32 +(* start with rule induction *)
    7.33 +be (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1;
    7.34 +by(fast_tac (set_cs addSEs evalc_elim_cases) 1);
    7.35 +by(fast_tac (set_cs addSEs evalc_elim_cases addDs [aexp_detD]) 1);
    7.36 +by(fast_tac (set_cs addSEs evalc_elim_cases) 1);
    7.37 +by(fast_tac (set_cs addSEs evalc_elim_cases addDs [bexp_detD]) 1);
    7.38 +by(fast_tac (set_cs addSEs evalc_elim_cases addDs [bexp_detD]) 1);
    7.39 +by(EVERY1[strip_tac, eresolve_tac evalc_elim_cases,
    7.40 +          atac, dtac bexp_detD, atac, etac False_neq_True]);
    7.41 +by(EVERY1[strip_tac, eresolve_tac evalc_elim_cases,
    7.42 +          dtac bexp_detD, atac, etac (sym RS False_neq_True),
    7.43 +          fast_tac HOL_cs]);
    7.44 +result();
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/IMP/Properties.thy	Fri Mar 03 12:04:16 1995 +0100
     8.3 @@ -0,0 +1,1 @@
     8.4 +Properties = "Com"
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/IMP/ROOT.ML	Fri Mar 03 12:04:16 1995 +0100
     9.3 @@ -0,0 +1,21 @@
     9.4 +(*  Title: 	CHOL/IMP/ROOT.ML
     9.5 +    ID:         $Id$
     9.6 +    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
     9.7 +    Copyright   1994 TUM
     9.8 +
     9.9 +Executes the formalization of the denotational and operational semantics of a
    9.10 +simple while-language, including an equivalence proof. The whole development
    9.11 +essentially formalizes/transcribes chapters 2 and 5 of
    9.12 +
    9.13 +Glynn Winskel. The Formal Semantics of Programming Languages.
    9.14 +MIT Press, 1993.
    9.15 +
    9.16 +*)
    9.17 +
    9.18 +CHOL_build_completed;	(*Make examples fail if CHOL did*)
    9.19 +
    9.20 +writeln"Root file for CHOL/IMP";
    9.21 +proof_timing := true;
    9.22 +loadpath := [".","IMP"];
    9.23 +time_use_thy "Properties";
    9.24 +time_use_thy "Equiv";