# HG changeset patch # User nipkow # Date 776357108 -7200 # Node ID 093665669f520e71dce6eddb1ba0f0d31a604526 # Parent 8a2bcbd8479d4de1aa593c61e6aa47ed109ec35a Simplified some proofs. Added some type assumptions to the introduction rules. diff -r 8a2bcbd8479d -r 093665669f52 src/ZF/IMP/Equiv.ML --- a/src/ZF/IMP/Equiv.ML Thu Aug 04 12:39:28 1994 +0200 +++ b/src/ZF/IMP/Equiv.ML Mon Aug 08 16:45:08 1994 +0200 @@ -45,24 +45,20 @@ val prems = goal Equiv.thy "[| a: aexp; sigma: loc -> nat |] ==> \ -\ -a-> n <-> n = A(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 (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))); (* ==> *) +by (ALLGOALS (fast_tac (ZF_cs addSIs (Evala.intrs@prems) + addSEs Aexp_elim_cases))); val aexp_iff = result(); - -val Aexp_rew_rules_cs = ZF_cs addIs op_type_intrs@[aexp_iff RS iffD1 RS sym]; - -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 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 aexp2 = aexp_iff RS iffD2; @@ -79,38 +75,25 @@ val prems = goal Equiv.thy "[| b: bexp; sigma: loc -> nat |] ==> \ -\ -b-> w <-> w = B(b,sigma) "; +\ -b-> w <-> B(b,sigma) = w"; -by (res_inst_tac [("x","w")] spec 1); (* quantify w *) -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 (TRYALL (fast_tac (* <== *) - (ZF_cs addSIs (Evalb.intrs@prems@[aexp2])) )); -by (TRYALL (fast_tac ((ZF_cs addSDs [aexp1]) addSEs Bexp_elim_cases))); - (* ==> *) +by (res_inst_tac [("x","w")] spec 1); (* quantify w *) +by (res_inst_tac [("x","b")] Bexp.induct 1); (* struct. ind. *) +by (resolve_tac prems 1); (* type prem. *) +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]))); val bexp_iff = result(); -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 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 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)]); +val bexp2 = bexp_iff RS iffD2; - - -val prems = goal Equiv.thy - " -c-> sigma' ==> : C(c)"; -by (cut_facts_tac prems 1); +goal Equiv.thy "!!c. -c-> sigma' ==> : C(c)"; (* start with rule induction *) be (Evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1; @@ -130,11 +113,11 @@ 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 (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 (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); @@ -146,10 +129,9 @@ addSEs [idE,compE] addEs [C_type,C_type_fst]; -val [prem] = goal Equiv.thy "c : com ==> ALL x. x:C(c) \ -\ --> -c-> snd(x)"; +goal Equiv.thy "!!c. c : com ==> ALL io:C(c). -c-> snd(io)"; -br (prem RS Com.induct) 1; +be Com.induct 1; by (rewrite_tac C_rewrite_rules); by (safe_tac com_cs); by (ALLGOALS (asm_full_simp_tac ZF_ss)); @@ -161,15 +143,15 @@ by (fast_tac com_cs 1); (* comp *) -by (REPEAT (EVERY [(etac allE 1),(etac impE 1),(atac 1)])); +by (REPEAT (EVERY [dtac bspec 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 [(etac allE 1),(etac impE 1),(atac 1)]); +by (EVERY [dtac bspec 1, atac 1]); by (ALLGOALS (asm_full_simp_tac ZF_ss)); (* while und if *) @@ -180,7 +162,7 @@ (**** Beweis der Aequivalenz ****) val com_iff_cs = ZF_cs addIs [C_subset RS subsetD] - addEs [com2 RS spec RS impE] + addEs [com2 RS bspec] addDs [com1]; goal Equiv.thy "ALL c:com.\ @@ -196,22 +178,3 @@ by (asm_full_simp_tac ZF_ss 1); val Com_equivalence = result(); - - - - - - - - - - - - - - - - - - - diff -r 8a2bcbd8479d -r 093665669f52 src/ZF/IMP/Evalc.ML --- a/src/ZF/IMP/Evalc.ML Thu Aug 04 12:39:28 1994 +0200 +++ b/src/ZF/IMP/Evalc.ML Mon Aug 08 16:45:08 1994 +0200 @@ -12,17 +12,19 @@ val sintrs = [ "[| sigma: loc -> nat |] ==> -c-> sigma", - "[| m: nat; x: loc; -a-> m |] ==> \ + "[| m: nat; x: loc; a:aexp; -a-> m |] ==> \ \ -c-> sigma[m/x]" , "[| -c-> sigma2; -c-> sigma1 |] ==> \ \ -c-> sigma1", - "[| c1: com; -b-> 1; -c-> sigma1 |] ==> \ -\ -c-> sigma1 ", - "[| c0 : com; -b-> 0; -c-> sigma1 |] ==> \ -\ -c-> sigma1 ", - "[| c: com; -b-> 0 |] ==> \ + "[| b:bexp; c1:com; sigma:loc->nat;\ +\ -b-> 1; -c-> sigma1 |] ==> \ +\ -c-> sigma1 ", + "[| b:bexp; c0:com; sigma:loc->nat;\ +\ -b-> 0; -c-> sigma1 |] ==> \ +\ -c-> sigma1 ", + "[| b:bexp; c:com; -b-> 0 |] ==> \ \ -c-> sigma ", - "[| c : com; -b-> 1; -c-> sigma2; \ + "[| b:bexp; c:com; -b-> 1; -c-> sigma2; \ \ -c-> sigma1 |] ==> \ \ -c-> sigma1 "];