# HG changeset patch # User paulson # Date 880559291 -3600 # Node ID b69eedd3aa6cacd4bca2ba55364444720925feb7 # Parent 5defc2105cc890d18eb1bb8230f4a76bf8defb8e Tidying and modification to cope with iffCE diff -r 5defc2105cc8 -r b69eedd3aa6c src/ZF/IMP/Denotation.ML --- a/src/ZF/IMP/Denotation.ML Wed Nov 26 16:45:54 1997 +0100 +++ b/src/ZF/IMP/Denotation.ML Wed Nov 26 16:48:11 1997 +0100 @@ -6,43 +6,37 @@ open Denotation; -(**** Rewrite Rules for A,B,C ****) - -val A_rewrite_rules = - [A_nat_def,A_loc_def,A_op1_def,A_op2_def]; +(** Rewrite Rules for A,B,C **) +Addsimps [A_nat_def,A_loc_def,A_op1_def,A_op2_def]; +Addsimps [B_true_def,B_false_def,B_op_def,B_not_def,B_and_def,B_or_def]; +Addsimps [C_skip_def,C_assign_def,C_comp_def,C_if_def,C_while_def]; -val B_rewrite_rules = - [B_true_def,B_false_def,B_op_def,B_not_def,B_and_def,B_or_def] - -val C_rewrite_rules = - [C_skip_def,C_assign_def,C_comp_def,C_if_def,C_while_def]; - -(**** Type_intr for A ****) +(** Type_intr for A **) val A_type = prove_goal Denotation.thy "!!a.[|a:aexp; sigma:loc->nat|] ==> A(a,sigma):nat" (fn _ => [(etac aexp.induct 1), - (rewrite_goals_tac A_rewrite_rules), + (ALLGOALS Asm_simp_tac), (ALLGOALS (fast_tac (claset() addSIs [apply_type])))]); -(**** Type_intr for B ****) +(** Type_intr for B **) val B_type = prove_goal Denotation.thy "!!b. [|b:bexp; sigma:loc->nat|] ==> B(b,sigma):bool" (fn _ => [(etac bexp.induct 1), - (rewrite_goals_tac B_rewrite_rules), + (ALLGOALS Asm_simp_tac), (ALLGOALS (fast_tac (claset() addSIs [apply_type,A_type]@bool_typechecks)))]); -(**** C_subset ****) +(** C_subset **) val C_subset = prove_goal Denotation.thy "!!c. c:com ==> C(c) <= (loc->nat)*(loc->nat)" (fn _ => [(etac com.induct 1), - (rewrite_tac C_rewrite_rules), + (ALLGOALS Asm_simp_tac), (ALLGOALS (fast_tac (claset() addDs [lfp_subset RS subsetD])))]); -(**** Type_elims for C ****) +(** Type_elims for C **) val C_type = prove_goal Denotation.thy "[| :C(c); c:com; \ @@ -64,10 +58,10 @@ (Asm_simp_tac 1)]); -(**** bnd_mono (nat->nat*nat->nat,Gamma(b,c) ****) +(** bnd_mono (nat->nat*nat->nat,Gamma(b,c) **) val Gamma_bnd_mono = prove_goalw Denotation.thy [bnd_mono_def,Gamma_def] "!!c. c:com ==> bnd_mono ((loc->nat)*(loc->nat),Gamma(b,c))" (fn prems => [(best_tac (claset() addEs [C_type]) 1)]); -(**** End ***) +(** End ***) diff -r 5defc2105cc8 -r b69eedd3aa6c src/ZF/IMP/Equiv.ML --- a/src/ZF/IMP/Equiv.ML Wed Nov 26 16:45:54 1997 +0100 +++ b/src/ZF/IMP/Equiv.ML Wed Nov 26 16:48:11 1997 +0100 @@ -4,21 +4,18 @@ Copyright 1994 TUM *) -val prems = goal Equiv.thy "[| a: aexp; sigma: loc -> nat |] ==> \ -\ -a-> n <-> A(a,sigma) = n"; +val prems = goal Equiv.thy + "!!a. [| 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 (TRYALL (fast_tac (claset() addSIs (evala.intrs@prems) - addSEs aexp_elim_cases))); +by (etac aexp.induct 1); +by (ALLGOALS (fast_tac (claset() addSIs evala.intrs + addSEs aexp_elim_cases + addss (simpset())))); qed "aexp_iff"; -val aexp1 = prove_goal Equiv.thy - "[| -a-> n; a: aexp; sigma: loc -> nat |] \ - \ ==> A(a,sigma) = n" (* destruction rule *) - (fn prems => [(fast_tac (claset() addSIs ((aexp_iff RS iffD1)::prems)) 1)]); +val aexp1 = aexp_iff RS iffD1; val aexp2 = aexp_iff RS iffD2; @@ -33,86 +30,64 @@ ]; -val prems = goal Equiv.thy "[| b: bexp; sigma: loc -> nat |] ==> \ -\ -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 (rewrite_goals_tac B_rewrite_rules); (* rewr. Den. *) -by (TRYALL (fast_tac (claset() addSIs (evalb.intrs@prems@[aexp2]) - addSDs [aexp1] addSEs bexp_elim_cases))); +val prems = goal Equiv.thy + "!!b. [| b: bexp; sigma: loc -> nat |] ==> \ +\ -b-> w <-> B(b,sigma) = w"; +by (res_inst_tac [("x","w")] spec 1); +by (etac bexp.induct 1); +by (ALLGOALS (fast_tac (claset() addSIs evalb.intrs + addSEs bexp_elim_cases + addss (simpset() addsimps [aexp_iff])))); qed "bexp_iff"; -val bexp1 = prove_goal Equiv.thy - "[| -b-> w; b: bexp; sigma: loc -> nat |]\ - \ ==> B(b,sigma) = w" - (fn prems => [(fast_tac (claset() addSIs ((bexp_iff RS iffD1)::prems)) 1)]); +val bexp1 = bexp_iff RS iffD1; val bexp2 = bexp_iff RS iffD2; + goal Equiv.thy "!!c. -c-> sigma' ==> : C(c)"; - -(* start with rule induction *) by (etac evalc.induct 1); - -by (rewrite_tac (Gamma_def::C_rewrite_rules)); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [bexp1]))); (* skip *) by (Fast_tac 1); - (* assign *) -by (asm_full_simp_tac (simpset() addsimps [aexp1,assign_type] @ op_type_intrs) 1); - +by (asm_full_simp_tac (simpset() addsimps + [aexp1, assign_type] @ op_type_intrs) 1); (* comp *) by (Fast_tac 1); - -(* if *) -by (asm_simp_tac (simpset() addsimps [bexp1]) 1); -by (asm_simp_tac (simpset() addsimps [bexp1]) 1); - (* while *) -by (etac (rewrite_rule [Gamma_def] - (Gamma_bnd_mono RS lfp_Tarski RS ssubst)) 1); -by (asm_simp_tac (simpset() addsimps [bexp1]) 1); -by (fast_tac (claset() addSIs [bexp1,idI]@evalb_type_intrs) 1); - -by (etac (rewrite_rule [Gamma_def] - (Gamma_bnd_mono RS lfp_Tarski RS ssubst)) 1); -by (asm_simp_tac (simpset() addsimps [bexp1]) 1); -by (fast_tac (claset() addSIs [bexp1,compI]@evalb_type_intrs) 1); - +by (etac (Gamma_bnd_mono RS lfp_Tarski RS ssubst) 1); +by (asm_simp_tac (simpset() addsimps [Gamma_def, bexp1]) 1); +by (blast_tac (claset() addSIs [bexp1]@evalb_type_intrs) 1); +(* recursive case of while *) +by (etac (Gamma_bnd_mono RS lfp_Tarski RS ssubst) 1); +by (asm_full_simp_tac (simpset() addsimps [Gamma_def, bexp1]) 1); +by (blast_tac (claset() addSIs [bexp1]@evalb_type_intrs) 1); val com1 = result(); AddSIs [aexp2,bexp2,B_type,A_type]; -AddIs evalc.intrs; -AddEs [C_type,C_type_fst]; +AddIs evalc.intrs; +AddEs [C_type,C_type_fst]; + -val [prem] = goal Equiv.thy - "c : com ==> ALL x:C(c). -c-> snd(x)"; -by (rtac (prem RS com.induct) 1); -by (rewrite_tac C_rewrite_rules); +goal Equiv.thy "!!c. c : com ==> ALL x:C(c). -c-> snd(x)"; +by (etac com.induct 1); +(* skip *) +by (fast_tac (claset() addss (simpset())) 1); +(* assign *) +by (fast_tac (claset() addss (simpset())) 1); +(* comp *) +by (best_tac (claset() addss (simpset())) 1); +(* while *) by Safe_tac; by (ALLGOALS Asm_full_simp_tac); - -(* skip *) -by (Fast_tac 1); - -(* assign *) -by (Fast_tac 1); - -(* comp *) -by (REPEAT (EVERY [(dtac bspec 1),(atac 1)])); -by (Asm_full_simp_tac 1); -by (Fast_tac 1); - -(* while *) by (EVERY1 [forward_tac [Gamma_bnd_mono], etac induct, atac]); by (rewtac Gamma_def); by Safe_tac; by (EVERY1 [dtac bspec, atac]); by (ALLGOALS Asm_full_simp_tac); - (* while, if *) -by (ALLGOALS Fast_tac); +by (ALLGOALS Blast_tac); val com2 = result(); @@ -121,7 +96,7 @@ goal Equiv.thy "ALL c:com. C(c) = {io:(loc->nat)*(loc->nat). -c-> snd(io)}"; by (fast_tac (claset() addIs [C_subset RS subsetD] - addEs [com2 RS bspec] - addDs [com1] - addss (simpset())) 1); + addEs [com2 RS bspec] + addDs [com1] + addss (simpset())) 1); val com_equivalence = result();