# HG changeset patch # User lcp # Date 776679607 -7200 # Node ID b2be4790da7a6ea29693317eda32d916b8780fe7 # Parent 093665669f520e71dce6eddb1ba0f0d31a604526 re-organized using new theory sections diff -r 093665669f52 -r b2be4790da7a src/ZF/IMP/Com.ML --- 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-> n ==> a:aexp","!!a. -a-> n ==> sigma:loc->nat", + "!!a. -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-> w ==> b:bexp","!!b. -b-> w ==> sigma:loc->nat", + "!!b. -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:com", + "!!c. -c-> sigma' ==> sigma:loc->nat", + "!!c. -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 " -a-> i", + evala.mk_cases aexp.con_defs " -a-> i", + evala.mk_cases aexp.con_defs " -a-> i", + evala.mk_cases aexp.con_defs " -a-> i" + ]; diff -r 093665669f52 -r b2be4790da7a src/ZF/IMP/Com.thy --- 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 + " -a-> n" == " : evala" +inductive + domains "evala" <= "aexp * (loc -> nat) * nat" + intrs + N "[| n:nat ; sigma:loc->nat |] ==> -a-> n" + X "[| x:loc; sigma:loc->nat |] ==> -a-> sigma`x" + Op1 "[| -a-> n; f: nat -> nat |] ==> -a-> f`n" + Op2 "[| -a-> n0; -a-> n1; f: (nat*nat) -> nat |] \ +\ ==> -a-> f`" + + 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 + " -b-> b" == " : evalb" + +inductive + domains "evalb" <= "bexp * (loc -> nat) * bool" + intrs (*avoid clash with ML constructors true, false*) + tru "[| sigma:loc -> nat |] ==> -b-> 1" + fls "[| sigma:loc -> nat |] ==> -b-> 0" + ROp "[| -a-> n0; -a-> n1; f: (nat*nat)->bool |] \ +\ ==> -b-> f` " + noti "[| -b-> w |] ==> -b-> not(w)" + andi "[| -b-> w0; -b-> w1 |] \ +\ ==> -b-> (w0 and w1)" + ori "[| -b-> w0; -b-> w1 |] \ +\ ==> -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 + " -c-> 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 |] ==> -c-> sigma" + + assign "[| m: nat; x: loc; -a-> m |] ==> \ +\ -c-> sigma[m/x]" + + semi "[| -c-> sigma2; -c-> sigma1 |] ==> \ +\ -c-> sigma1" + + ifc1 "[| c1: com; -b-> 1; -c-> sigma1 |] ==> \ +\ -c-> sigma1" + + ifc0 "[| c0 : com; -b-> 0; -c-> sigma1 |] ==> \ +\ -c-> sigma1" + + while0 "[| c: com; -b-> 0 |] ==> \ +\ -c-> sigma " + + while1 "[| c : com; -b-> 1; -c-> sigma2; \ +\ -c-> sigma1 |] ==> \ +\ -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 diff -r 093665669f52 -r b2be4790da7a src/ZF/IMP/Denotation.ML --- 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])))]); diff -r 093665669f52 -r b2be4790da7a src/ZF/IMP/Denotation.thy --- 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`)" - - - 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_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`)" - 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`)" - 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 - - - - - - diff -r 093665669f52 -r b2be4790da7a src/ZF/IMP/Equiv.ML --- 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-> n ==> a:aexp","!!a. -a-> n ==> sigma:loc->nat", - "!!a. -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-> w ==> b:bexp","!!b. -b-> w ==> sigma:loc->nat", - "!!b. -b-> w ==> w:bool"]; +val prems = goal Equiv.thy "[| a: aexp; sigma: loc -> nat |] ==> \ +\ -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:com", - "!!c. -c-> sigma' ==> sigma:loc->nat", - "!!c. -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 " -a-> i", - Evala.mk_cases Aexp.con_defs " -a-> i", - Evala.mk_cases Aexp.con_defs " -a-> i", - Evala.mk_cases Aexp.con_defs " -a-> i" - ]; - - -val prems = goal Equiv.thy "[| a: aexp; sigma: loc -> nat |] ==> \ -\ -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-> 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-> 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 " -b-> x", - Evalb.mk_cases Bexp.con_defs " -b-> x", - Evalb.mk_cases Bexp.con_defs " -b-> x", - Evalb.mk_cases Bexp.con_defs " -b-> x", - Evalb.mk_cases Bexp.con_defs " -b-> x", - Evalb.mk_cases Bexp.con_defs " -b-> x" + evalb.mk_cases bexp.con_defs " -b-> x", + evalb.mk_cases bexp.con_defs " -b-> x", + evalb.mk_cases bexp.con_defs " -b-> x", + evalb.mk_cases bexp.con_defs " -b-> x", + evalb.mk_cases bexp.con_defs " -b-> x", + evalb.mk_cases bexp.con_defs " -b-> x" ]; val prems = goal Equiv.thy "[| b: bexp; sigma: loc -> nat |] ==> \ -\ -b-> w <-> B(b,sigma) = w"; +\ -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-> 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-> 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-> 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(c)"; + + +val prems = goal Equiv.thy + " -c-> 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-> snd(io)"; - -be Com.induct 1; +val [prem] = goal Equiv.thy + "c : com ==> ALL x. x:C(c) --> -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-> snd(io)}"; +goal Equiv.thy + "ALL c:com. C(c) = {io:(loc->nat)*(loc->nat). -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(); diff -r 093665669f52 -r b2be4790da7a src/ZF/IMP/Equiv.thy --- 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