--- a/src/ZF/IMP/Com.ML Mon Aug 08 16:45:08 1994 +0200
+++ b/src/ZF/IMP/Com.ML Fri Aug 12 10:20:07 1994 +0200
@@ -4,36 +4,48 @@
Copyright 1994 TUM
*)
-structure Com = Datatype_Fun
- (
- val thy = Bexp.thy;
- val thy_name = "Com";
- val rec_specs =
- [
- (
- "com", "univ(aexp Un bexp)",
- [
- (["skip"], "i", NoSyn),
- ([":="], "[i,i] => i", Infixl 60),
- ([";"], "[i,i] => i", Infixl 60),
- (["whileC"], "[i,i] => i", Mixfix("while _ do _",[],60)),
- (["ifC"], "[i,i,i] => i",
- Mixfix("ifc _ then _ else _",[],60))
- ]
- )
- ];
+open Com;
+
+val assign_type = prove_goalw Com.thy [assign_def]
+ "!!n. [| sigma:loc -> nat; n:nat |] ==> sigma[n/x] : loc -> nat"
+ (fn _ => [ fast_tac (ZF_cs addIs [apply_type,lam_type,if_type]) 1 ]);
+
+val type_cs = ZF_cs addSEs [make_elim(evala.dom_subset RS subsetD),
+ make_elim(evalb.dom_subset RS subsetD),
+ make_elim(evalc.dom_subset RS subsetD)];
+
+(********** type_intrs for evala **********)
+
+val evala_type_intrs =
+ map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)]))
+ ["!!a.<a,sigma> -a-> n ==> a:aexp","!!a.<a,sigma> -a-> n ==> sigma:loc->nat",
+ "!!a.<a,sigma> -a-> n ==> n:nat"];
+
+
+(********** type_intrs for evalb **********)
- val rec_styp = "i";
+val evalb_type_intrs =
+ map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)]))
+ ["!!b.<b,sigma> -b-> w ==> b:bexp","!!b.<b,sigma> -b-> w ==> sigma:loc->nat",
+ "!!b.<b,sigma> -b-> w ==> w:bool"];
+
+
+(********** type_intrs for evalb **********)
- val sintrs =
- [
- "skip : com",
- "[| x:loc; a:aexp|] ==> X(x) := a : com",
- "[| c0:com; c1:com|] ==> c0 ; c1 : com",
- "[| b:bexp; c:com|] ==> while b do c : com",
- "[| b:bexp; c0:com; c1:com|] ==> ifc b then c0 else c1 : com"
- ];
- val monos = [];
- val type_intrs = datatype_intrs@Aexp.intrs;
- val type_elims = datatype_elims
- );
+val evalc_type_intrs =
+ map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)]))
+ ["!!c.<c,sigma> -c-> sigma' ==> c:com",
+ "!!c.<c,sigma> -c-> sigma' ==> sigma:loc->nat",
+ "!!c.<c,sigma> -c-> sigma' ==> sigma':loc->nat"];
+
+
+val op_type_intrs = evala_type_intrs@evalb_type_intrs@evalc_type_intrs;
+
+
+val aexp_elim_cases =
+ [
+ evala.mk_cases aexp.con_defs "<N(n),sigma> -a-> i",
+ evala.mk_cases aexp.con_defs "<X(x),sigma> -a-> i",
+ evala.mk_cases aexp.con_defs "<Op1(f,e),sigma> -a-> i",
+ evala.mk_cases aexp.con_defs "<Op2(f,a1,a2),sigma> -a-> i"
+ ];
--- a/src/ZF/IMP/Com.thy Mon Aug 08 16:45:08 1994 +0200
+++ b/src/ZF/IMP/Com.thy Fri Aug 12 10:20:07 1994 +0200
@@ -3,7 +3,126 @@
Author: Heiko Loetzbeyer & Robert Sandner, TUM
Copyright 1994 TUM
-Dummy theory merely recording dependence
+Arithmetic expressions, Boolean expressions, Commands
+
+And their Operational semantics
*)
-Com = Bexp
+Com = Univ + "Datatype" +
+
+(** Arithmetic expressions **)
+consts loc :: "i"
+ aexp :: "i"
+
+datatype <= "univ(loc Un (nat->nat) Un ((nat*nat) -> nat) )"
+ "aexp" = N ("n: nat")
+ | X ("x: loc")
+ | Op1 ("f: nat -> nat", "a : aexp")
+ | Op2 ("f: (nat*nat) -> nat", "a0 : aexp", "a1 : aexp")
+
+
+(** Evaluation of arithmetic expressions **)
+consts evala :: "i"
+ "@evala" :: "[i,i,i] => o" ("<_,_>/ -a-> _")
+translations
+ "<ae,sig> -a-> n" == "<ae,sig,n> : evala"
+inductive
+ domains "evala" <= "aexp * (loc -> nat) * nat"
+ intrs
+ N "[| n:nat ; sigma:loc->nat |] ==> <N(n),sigma> -a-> n"
+ X "[| x:loc; sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
+ Op1 "[| <e,sigma> -a-> n; f: nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n"
+ Op2 "[| <e0,sigma> -a-> n0; <e1,sigma> -a-> n1; f: (nat*nat) -> nat |] \
+\ ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"
+
+ type_intrs "aexp.intrs@[apply_funtype]"
+
+
+(** Boolean expressions **)
+consts bexp :: "i"
+
+datatype <= "univ(aexp Un ((nat*nat)->bool) )"
+ "bexp" = true
+ | false
+ | ROp ("f: (nat*nat)->bool", "a0 : aexp", "a1 : aexp")
+ | noti ("b : bexp")
+ | andi ("b0 : bexp", "b1 : bexp") (infixl 60)
+ | ori ("b0 : bexp", "b1 : bexp") (infixl 60)
+
+
+(** Evaluation of boolean expressions **)
+consts evalb :: "i"
+ "@evalb" :: "[i,i,i] => o" ("<_,_>/ -b-> _")
+
+translations
+ "<be,sig> -b-> b" == "<be,sig,b> : evalb"
+
+inductive
+ domains "evalb" <= "bexp * (loc -> nat) * bool"
+ intrs (*avoid clash with ML constructors true, false*)
+ tru "[| sigma:loc -> nat |] ==> <true,sigma> -b-> 1"
+ fls "[| sigma:loc -> nat |] ==> <false,sigma> -b-> 0"
+ ROp "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f: (nat*nat)->bool |] \
+\ ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
+ noti "[| <b,sigma> -b-> w |] ==> <noti(b),sigma> -b-> not(w)"
+ andi "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] \
+\ ==> <b0 andi b1,sigma> -b-> (w0 and w1)"
+ ori "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] \
+\ ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
+
+ type_intrs "bexp.intrs @ [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
+ type_elims "[make_elim(evala.dom_subset RS subsetD)]"
+
+
+(** Commands **)
+consts com :: "i"
+
+datatype <= "univ(loc Un aexp Un bexp)"
+ "com" = skip
+ | ":=" ("x:loc", "a:aexp") (infixl 60)
+ | ";" ("c0:com", "c1:com") (infixl 60)
+ | while ("b:bexp", "c:com") ("while _ do _" 60)
+ | ifc ("b:bexp", "c0:com", "c1:com") ("ifc _ then _ else _" 60)
+ type_intrs "aexp.intrs"
+
+
+(** Execution of commands **)
+consts evalc :: "i"
+ "@evalc" :: "[i,i,i] => o" ("<_,_>/ -c-> _")
+ "assign" :: "[i,i,i] => i" ("_[_'/_]" [900,0,0] 900)
+
+translations
+ "<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
+
+rules
+ assign_def "sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)"
+
+inductive
+ domains "evalc" <= "com * (loc -> nat) * (loc -> nat)"
+ intrs
+ skip "[| sigma: loc -> nat |] ==> <skip,sigma> -c-> sigma"
+
+ assign "[| m: nat; x: loc; <a,sigma> -a-> m |] ==> \
+\ <x := a,sigma> -c-> sigma[m/x]"
+
+ semi "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] ==> \
+\ <c0 ; c1, sigma> -c-> sigma1"
+
+ ifc1 "[| c1: com; <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> \
+\ <ifc b then c0 else c1, sigma> -c-> sigma1"
+
+ ifc0 "[| c0 : com; <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> \
+\ <ifc b then c0 else c1, sigma> -c-> sigma1"
+
+ while0 "[| c: com; <b, sigma> -b-> 0 |] ==> \
+\ <while b do c,sigma> -c-> sigma "
+
+ while1 "[| c : com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2; \
+\ <while b do c, sigma2> -c-> sigma1 |] ==> \
+\ <while b do c, sigma> -c-> sigma1 "
+
+ con_defs "[assign_def]"
+ type_intrs "bexp.intrs @ com.intrs @ [if_type,lam_type,apply_type]"
+ type_elims "[make_elim(evala.dom_subset RS subsetD), make_elim(evalb.dom_subset RS subsetD) ]"
+
+end
--- a/src/ZF/IMP/Denotation.ML Mon Aug 08 16:45:08 1994 +0200
+++ b/src/ZF/IMP/Denotation.ML Fri Aug 12 10:20:07 1994 +0200
@@ -6,7 +6,7 @@
open Denotation;
-(**** Rewrite Rules fuer A,B,C ****)
+(**** Rewrite Rules for A,B,C ****)
val A_rewrite_rules =
[A_nat_def,A_loc_def,A_op1_def,A_op2_def];
@@ -21,7 +21,7 @@
val A_type = prove_goal Denotation.thy
"!!a.[|a:aexp; sigma:loc->nat|] ==> A(a,sigma):nat"
- (fn _ => [(etac Aexp.induct 1),
+ (fn _ => [(etac aexp.induct 1),
(rewrite_goals_tac A_rewrite_rules),
(ALLGOALS (fast_tac (ZF_cs addSIs [apply_type])))]);
@@ -29,7 +29,7 @@
val B_type = prove_goal Denotation.thy
"!!b. [|b:bexp; sigma:loc->nat|] ==> B(b,sigma):bool"
- (fn _ => [(etac Bexp.induct 1),
+ (fn _ => [(etac bexp.induct 1),
(rewrite_goals_tac B_rewrite_rules),
(ALLGOALS (fast_tac (ZF_cs
addSIs [apply_type,A_type]@bool_typechecks)))]);
@@ -38,7 +38,7 @@
val C_subset = prove_goal Denotation.thy
"!!c. c:com ==> C(c) <= (loc->nat)*(loc->nat)"
- (fn _ => [(etac Com.induct 1),
+ (fn _ => [(etac com.induct 1),
(rewrite_tac C_rewrite_rules),
(ALLGOALS (fast_tac (comp_cs addDs [lfp_subset RS subsetD])))]);
--- a/src/ZF/IMP/Denotation.thy Mon Aug 08 16:45:08 1994 +0200
+++ b/src/ZF/IMP/Denotation.thy Fri Aug 12 10:20:07 1994 +0200
@@ -2,52 +2,45 @@
ID: $Id$
Author: Heiko Loetzbeyer & Robert Sandner, TUM
Copyright 1994 TUM
+
+Denotational semantics of expressions & commands
*)
-Denotation = ZF + Assign + Aexp + Bexp + Com +
+Denotation = Com +
consts
- A :: "i => i => i"
- B :: "i => i => i"
- C :: "i => i"
- Gamma :: "[i,i,i] => i"
+ A :: "i => i => i"
+ B :: "i => i => i"
+ C :: "i => i"
+ Gamma :: "[i,i,i] => i"
rules
- A_nat_def "A(N(n)) == (%sigma. n)"
- A_loc_def "A(X(x)) == (%sigma. sigma`x)"
- A_op1_def "A(Op1(f,a)) == (%sigma. f`A(a,sigma))"
- A_op2_def "A(Op2(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
-
-
- B_true_def "B(true) == (%sigma. 1)"
- B_false_def "B(false) == (%sigma. 0)"
- B_op_def "B(ROp(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
+ A_nat_def "A(N(n)) == (%sigma. n)"
+ A_loc_def "A(X(x)) == (%sigma. sigma`x)"
+ A_op1_def "A(Op1(f,a)) == (%sigma. f`A(a,sigma))"
+ A_op2_def "A(Op2(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
- B_not_def "B(noti(b)) == (%sigma. not(B(b,sigma)))"
- B_and_def "B(b0 andi b1) == (%sigma. B(b0,sigma) and B(b1,sigma))"
- B_or_def "B(b0 ori b1) == (%sigma. B(b0,sigma) or B(b1,sigma))"
+ B_true_def "B(true) == (%sigma. 1)"
+ B_false_def "B(false) == (%sigma. 0)"
+ B_op_def "B(ROp(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
- C_skip_def "C(skip) == id(loc->nat)"
- C_assign_def "C(X(x) := a) == {io:(loc->nat)*(loc->nat). \
-\ snd(io) = fst(io)[A(a,fst(io))/x]}"
+ B_not_def "B(noti(b)) == (%sigma. not(B(b,sigma)))"
+ B_and_def "B(b0 andi b1) == (%sigma. B(b0,sigma) and B(b1,sigma))"
+ B_or_def "B(b0 ori b1) == (%sigma. B(b0,sigma) or B(b1,sigma))"
+
+ C_skip_def "C(skip) == id(loc->nat)"
+ C_assign_def "C(x := a) == {io:(loc->nat)*(loc->nat). \
+\ snd(io) = fst(io)[A(a,fst(io))/x]}"
- C_comp_def "C(c0 ; c1) == C(c1) O C(c0)"
- C_if_def "C(ifc b then c0 else c1) == {io:C(c0). B(b,fst(io))=1} \
-\ Un {io:C(c1). B(b,fst(io))=0}"
+ C_comp_def "C(c0 ; c1) == C(c1) O C(c0)"
+ C_if_def "C(ifc b then c0 else c1) == {io:C(c0). B(b,fst(io))=1} Un \
+\ {io:C(c1). B(b,fst(io))=0}"
- Gamma_def "Gamma(b,c) == (%phi.{io : (phi O C(c)). B(b,fst(io))=1} Un \
-\ {io : id(loc->nat). B(b,fst(io))=0})"
+ Gamma_def "Gamma(b,c) == (%phi.{io : (phi O C(c)). B(b,fst(io))=1} Un \
+\ {io : id(loc->nat). B(b,fst(io))=0})"
- C_while_def "C(while b do c) == lfp((loc->nat)*(loc->nat), \
-\ Gamma(b,c))"
-
+ C_while_def "C(while b do c) == lfp((loc->nat)*(loc->nat), Gamma(b,c))"
end
-
-
-
-
-
-
--- a/src/ZF/IMP/Equiv.ML Mon Aug 08 16:45:08 1994 +0200
+++ b/src/ZF/IMP/Equiv.ML Fri Aug 12 10:20:07 1994 +0200
@@ -4,99 +4,73 @@
Copyright 1994 TUM
*)
-val type_cs = ZF_cs addSEs [make_elim(Evala.dom_subset RS subsetD),
- make_elim(Evalb.dom_subset RS subsetD),
- make_elim(Evalc.dom_subset RS subsetD)];
-
-(********** type_intrs fuer Evala **********)
-
-val Evala_type_intrs =
- map (fn s => prove_goal Evala.thy s (fn _ => [(fast_tac type_cs 1)]))
- ["!!a.<a,sigma> -a-> n ==> a:aexp","!!a.<a,sigma> -a-> n ==> sigma:loc->nat",
- "!!a.<a,sigma> -a-> n ==> n:nat"];
-
-
-(********** type_intrs fuer Evalb **********)
-
-val Evalb_type_intrs =
- map (fn s => prove_goal Evalb.thy s (fn _ => [(fast_tac type_cs 1)]))
- ["!!b.<b,sigma> -b-> w ==> b:bexp","!!b.<b,sigma> -b-> w ==> sigma:loc->nat",
- "!!b.<b,sigma> -b-> w ==> w:bool"];
+val prems = goal Equiv.thy "[| a: aexp; sigma: loc -> nat |] ==> \
+\ <a,sigma> -a-> n <-> n = A(a,sigma) ";
+by (res_inst_tac [("x","n")] spec 1); (* quantify n *)
+by (res_inst_tac [("x","a")] aexp.induct 1); (* struct. ind. *)
+by (resolve_tac prems 1); (* type prem. *)
+by (safe_tac ZF_cs); (* allI,-->,<-- *)
+by (rewrite_goals_tac A_rewrite_rules); (* rewr. Den. *)
+by (TRYALL (fast_tac (ZF_cs addSIs (evala.intrs@prems)) )); (* <== *)
+by (TRYALL (fast_tac (ZF_cs addSEs aexp_elim_cases))); (* ==> *)
+val aexp_iff = result();
-(********** type_intrs fuer Evalb **********)
-
-val Evalc_type_intrs =
- map (fn s => prove_goal Evalc.thy s (fn _ => [(fast_tac type_cs 1)]))
- ["!!c.<c,sigma> -c-> sigma' ==> c:com",
- "!!c.<c,sigma> -c-> sigma' ==> sigma:loc->nat",
- "!!c.<c,sigma> -c-> sigma' ==> sigma':loc->nat"];
-
-
-val op_type_intrs = Evala_type_intrs@Evalb_type_intrs@Evalc_type_intrs;
+val aexp_rew_rules_cs = ZF_cs addIs op_type_intrs@[aexp_iff RS iffD1 RS sym];
-val Aexp_elim_cases =
- [
- Evala.mk_cases Aexp.con_defs "<N(n),sigma> -a-> i",
- Evala.mk_cases Aexp.con_defs "<X(x),sigma> -a-> i",
- Evala.mk_cases Aexp.con_defs "<Op1(f,e),sigma> -a-> i",
- Evala.mk_cases Aexp.con_defs "<Op2(f,a1,a2),sigma> -a-> i"
- ];
-
-
-val prems = goal Equiv.thy "[| a: aexp; sigma: loc -> nat |] ==> \
-\ <a,sigma> -a-> n <-> A(a,sigma) = n";
-
-by (res_inst_tac [("x","n")] spec 1); (* quantify n *)
-by (res_inst_tac [("x","a")] Aexp.induct 1); (* struct. ind. *)
-by (resolve_tac prems 1); (* type prem. *)
-by (rewrite_goals_tac A_rewrite_rules); (* rewr. Den. *)
-by (ALLGOALS (fast_tac (ZF_cs addSIs (Evala.intrs@prems)
- addSEs Aexp_elim_cases)));
-
-val aexp_iff = result();
-
-val aexp1 = prove_goal Equiv.thy (* destr. rule *)
- "[| <a,sigma> -a-> n; a: aexp; sigma: loc -> nat |] ==> A(a,sigma) = n"
- (fn prems => [fast_tac (ZF_cs addSIs ((aexp_iff RS iffD1)::prems)) 1]);
+val aexp1 = prove_goal Equiv.thy (* elim the prems *)
+ "<a,sigma> -a-> n ==> A(a,sigma) = n" (* destruction rule *)
+ (fn prems => [(fast_tac (aexp_rew_rules_cs addSIs prems) 1)]);
val aexp2 = aexp_iff RS iffD2;
-val Bexp_elim_cases =
+val bexp_elim_cases =
[
- Evalb.mk_cases Bexp.con_defs "<true,sigma> -b-> x",
- Evalb.mk_cases Bexp.con_defs "<false,sigma> -b-> x",
- Evalb.mk_cases Bexp.con_defs "<ROp(f,a0,a1),sigma> -b-> x",
- Evalb.mk_cases Bexp.con_defs "<noti(b),sigma> -b-> x",
- Evalb.mk_cases Bexp.con_defs "<b0 andi b1,sigma> -b-> x",
- Evalb.mk_cases Bexp.con_defs "<b0 ori b1,sigma> -b-> x"
+ evalb.mk_cases bexp.con_defs "<true,sigma> -b-> x",
+ evalb.mk_cases bexp.con_defs "<false,sigma> -b-> x",
+ evalb.mk_cases bexp.con_defs "<ROp(f,a0,a1),sigma> -b-> x",
+ evalb.mk_cases bexp.con_defs "<noti(b),sigma> -b-> x",
+ evalb.mk_cases bexp.con_defs "<b0 andi b1,sigma> -b-> x",
+ evalb.mk_cases bexp.con_defs "<b0 ori b1,sigma> -b-> x"
];
val prems = goal Equiv.thy "[| b: bexp; sigma: loc -> nat |] ==> \
-\ <b,sigma> -b-> w <-> B(b,sigma) = w";
+\ <b,sigma> -b-> w <-> w = B(b,sigma) ";
by (res_inst_tac [("x","w")] spec 1); (* quantify w *)
-by (res_inst_tac [("x","b")] Bexp.induct 1); (* struct. ind. *)
+by (res_inst_tac [("x","b")] bexp.induct 1); (* struct. ind. *)
by (resolve_tac prems 1); (* type prem. *)
+by (safe_tac ZF_cs); (* allI,-->,<-- *)
by (rewrite_goals_tac B_rewrite_rules); (* rewr. Den. *)
-by (ALLGOALS (fast_tac (ZF_cs addSIs (Evalb.intrs@prems@[aexp2])
- addSEs Bexp_elim_cases addSDs [aexp1])));
-
+by (TRYALL (fast_tac (* <== *)
+ (ZF_cs addSIs (evalb.intrs@prems@[aexp2])) ));
+by (TRYALL (fast_tac ((ZF_cs addSDs [aexp1]) addSEs bexp_elim_cases)));
+ (* ==> *)
val bexp_iff = result();
-val bexp1 = prove_goal Equiv.thy
- "[| <b,sigma> -b-> w; b : bexp; sigma : loc -> nat |] ==> B(b,sigma) = w"
- (fn prems => [fast_tac (ZF_cs addIs ((bexp_iff RS iffD1)::prems)) 1]);
+val bexp_rew_rules_cs = ZF_cs addIs op_type_intrs@[bexp_iff RS iffD1 RS sym];
+
+val bexp1 = prove_goal Equiv.thy
+ "<b,sigma> -b-> w ==> B(b,sigma) = w"
+ (fn prems => [(fast_tac (bexp_rew_rules_cs addSIs prems) 1)]);
-val bexp2 = bexp_iff RS iffD2;
+val bexp2 = prove_goal Equiv.thy
+ "[| B(b,sigma) = w; b : bexp; sigma : loc -> nat |] ==> <b,sigma> -b-> w"
+ (fn prems =>
+ [(cut_facts_tac prems 1),
+ (fast_tac (ZF_cs addIs ([bexp_iff RS iffD2])) 1)]);
-goal Equiv.thy "!!c. <c,sigma> -c-> sigma' ==> <sigma,sigma'> : C(c)";
+
+
+val prems = goal Equiv.thy
+ "<c,sigma> -c-> sigma' ==> <sigma,sigma'> : C(c)";
+by (cut_facts_tac prems 1);
(* start with rule induction *)
-be (Evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1;
+be (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1;
by (rewrite_tac (Gamma_def::C_rewrite_rules));
(* skip *)
@@ -113,25 +87,25 @@
by (fast_tac (ZF_cs addSIs [bexp1] addIs [(fst_conv RS ssubst)]) 1);
(* while *)
-by (etac (rewrite_rule [Gamma_def] (Gamma_bnd_mono RS lfp_Tarski RS ssubst))1);
-by (fast_tac (comp_cs addSIs [bexp1,idI]@Evalb_type_intrs
+by (etac (rewrite_rule [Gamma_def] (Gamma_bnd_mono RS lfp_Tarski RS ssubst)) 1);
+by (fast_tac (comp_cs addSIs [bexp1,idI]@evalb_type_intrs
addIs [(fst_conv RS ssubst)]) 1);
-by (etac (rewrite_rule [Gamma_def] (Gamma_bnd_mono RS lfp_Tarski RS ssubst))1);
-by (fast_tac (comp_cs addSIs [bexp1,compI]@Evalb_type_intrs
+by (etac (rewrite_rule [Gamma_def] (Gamma_bnd_mono RS lfp_Tarski RS ssubst)) 1);
+by (fast_tac (comp_cs addSIs [bexp1,compI]@evalb_type_intrs
addIs [(fst_conv RS ssubst)]) 1);
val com1 = result();
val com_cs = ZF_cs addSIs [aexp2,bexp2,B_type,A_type]
- addIs Evalc.intrs
+ addIs evalc.intrs
addSEs [idE,compE]
addEs [C_type,C_type_fst];
-goal Equiv.thy "!!c. c : com ==> ALL io:C(c). <c,fst(io)> -c-> snd(io)";
-
-be Com.induct 1;
+val [prem] = goal Equiv.thy
+ "c : com ==> ALL x. x:C(c) --> <c,fst(x)> -c-> snd(x)";
+br (prem RS com.induct) 1;
by (rewrite_tac C_rewrite_rules);
by (safe_tac com_cs);
by (ALLGOALS (asm_full_simp_tac ZF_ss));
@@ -143,38 +117,35 @@
by (fast_tac com_cs 1);
(* comp *)
-by (REPEAT (EVERY [dtac bspec 1, atac 1]));
+by (REPEAT (EVERY [(etac allE 1),(etac impE 1),(atac 1)]));
by (asm_full_simp_tac ZF_ss 1);
by (fast_tac com_cs 1);
(* while *)
-by (EVERY [forward_tac [Gamma_bnd_mono] 1, etac induct 1,(atac 1)]);
+by (EVERY [(forward_tac [Gamma_bnd_mono] 1),(etac induct 1),(atac 1)]);
by (rewrite_goals_tac [Gamma_def]);
by (safe_tac com_cs);
-by (EVERY [dtac bspec 1, atac 1]);
+by (EVERY [(etac allE 1),(etac impE 1),(atac 1)]);
by (ALLGOALS (asm_full_simp_tac ZF_ss));
-(* while und if *)
+(* while, if *)
by (ALLGOALS (fast_tac com_cs));
val com2 = result();
-(**** Beweis der Aequivalenz ****)
+(**** Proof of Equivalence ****)
val com_iff_cs = ZF_cs addIs [C_subset RS subsetD]
- addEs [com2 RS bspec]
+ addEs [com2 RS spec RS impE]
addDs [com1];
-goal Equiv.thy "ALL c:com.\
-\ C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}";
+goal Equiv.thy
+ "ALL c:com. C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}";
by (rtac ballI 1);
by (rtac equalityI 1);
-
(* => *)
by (fast_tac com_iff_cs 1);
-
(* <= *)
by (REPEAT (step_tac com_iff_cs 1));
by (asm_full_simp_tac ZF_ss 1);
-
-val Com_equivalence = result();
+val com_equivalence = result();
--- a/src/ZF/IMP/Equiv.thy Mon Aug 08 16:45:08 1994 +0200
+++ b/src/ZF/IMP/Equiv.thy Fri Aug 12 10:20:07 1994 +0200
@@ -4,4 +4,4 @@
Copyright 1994 TUM
*)
-Equiv = Denotation + Evalc
+Equiv = Denotation + Com