diff -r e7dcf3c07865 -r 41bf53133ba6 IMP/Equiv.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/IMP/Equiv.ML Wed Aug 31 15:15:54 1994 +0200 @@ -0,0 +1,104 @@ +(* Title: ZF/IMP/Equiv.ML + ID: $Id$ + Author: Heiko Loetzbeyer & Robert Sandner, TUM + Copyright 1994 TUM +*) + +goal Equiv.thy "( -a-> n) = (A(a,sigma) = n)"; +by (res_inst_tac [("x","n")] spec 1); (* quantify n *) +by (aexp.induct_tac "a" 1); (* struct. ind. *) +by (rewrite_goals_tac A_rewrite_rules); (* rewr. Den. *) +by (TRYALL (fast_tac (set_cs addSIs (evala.intrs@prems) + addSEs aexp_elim_cases))); +val aexp_iff = result(); + +val aexp1 = aexp_iff RS iffD1; +val aexp2 = aexp_iff RS iffD2; + + +goal Equiv.thy "( -b-> w) = (B(b,sigma) = w)"; +by (res_inst_tac [("x","w")] spec 1); (* quantify w *) +by (bexp.induct_tac "b" 1); (* struct. ind. *) +by (rewrite_goals_tac B_rewrite_rules); (* rewr. Den. *) +by (safe_tac (HOL_cs addSIs (aexp2::evalb.intrs) + addSDs [aexp1] addSEs bexp_elim_cases) + THEN ALLGOALS(best_tac HOL_cs)); + +val bexp_iff = result(); + +val bexp1 = bexp_iff RS iffD1; +val bexp2 = bexp_iff RS iffD2; + +val BfstI = read_instantiate_sg (sign_of Equiv.thy) + [("P","%x.B(?b,x)")] (fst_conv RS ssubst); +val BfstD = read_instantiate_sg (sign_of Equiv.thy) + [("P","%x.B(?b,x)")] (fst_conv RS subst); + +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; + +by (rewrite_tac (Gamma_def::C_rewrite_rules)); +(* skip *) +by (fast_tac comp_cs 1); +(* assign *) +by (asm_full_simp_tac (prod_ss addsimps [aexp1]) 1); +(* comp *) +by (fast_tac comp_cs 1); +(* if *) +by(fast_tac (set_cs addSIs [BfstI] addSDs [BfstD,bexp1]) 1); +by(fast_tac (set_cs addSIs [BfstI] addSDs [BfstD,bexp1]) 1); +(* while *) +by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1); +by (fast_tac (comp_cs addSIs [bexp1,BfstI] addSDs [BfstD,bexp1]) 1); +by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1); +by (fast_tac (comp_cs addSIs [bexp1,BfstI] addSDs [BfstD,bexp1]) 1); + +val com1 = result(); + + +val com_cs = comp_cs addSIs [aexp2,bexp2] addIs evalc.intrs; + +goal Equiv.thy "!x:C(c). -c-> snd(x)"; +by (com.induct_tac "c" 1); +by (rewrite_tac C_rewrite_rules); +by (safe_tac com_cs); +by (ALLGOALS (asm_full_simp_tac prod_ss)); + +(* skip *) +by (fast_tac com_cs 1); + +(* assign *) +by (fast_tac com_cs 1); + +(* comp *) +by (REPEAT (EVERY [(dtac bspec 1),(atac 1)])); +by (asm_full_simp_tac prod_ss 1); +by (fast_tac com_cs 1); + +(* while *) +by (etac (Gamma_mono RSN (2,induct)) 1); +by (rewrite_goals_tac [Gamma_def]); +by (safe_tac com_cs); +by (EVERY1 [dtac bspec, atac]); +by (ALLGOALS (asm_full_simp_tac prod_ss)); + +(* while, if *) +by (ALLGOALS (fast_tac com_cs)); +val com2 = result(); + + +(**** Proof of Equivalence ****) + +val com_iff_cs = set_cs addEs [com2 RS bspec] + addDs [com1]; + +goal Equiv.thy "C(c) = {io . -c-> snd(io)}"; +by (rtac equalityI 1); +(* => *) +by (fast_tac com_iff_cs 1); +(* <= *) +by (REPEAT (step_tac com_iff_cs 1)); +by (asm_full_simp_tac (prod_ss addsimps [surjective_pairing RS sym])1); +val com_equivalence = result();