IMP/Equiv.ML

minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections;

(*  Title: 	HOL/IMP/Equiv.ML
    ID:         $Id$
    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
    Copyright   1994 TUM
*)

goal Equiv.thy "(<a,s> -a-> n) = (A(a,s) = n)";
by (res_inst_tac [("x","n")] spec 1);                     (* quantify n *)
by (aexp.induct_tac "a" 1);                		  (* struct. ind. *)
by (ALLGOALS(simp_tac (HOL_ss addsimps A_simps)));	  (* 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 "!w. (<b,s> -b-> w) --> (B(b,s) = w)";
by (bexp.induct_tac "b" 1);
by (rewrite_goals_tac B_simps);		(*denotational semantics*)
by (ALLGOALS (fast_tac (HOL_cs addSDs [aexp1] addSEs bexp_elim_cases)));
val bexp_imp1 = result();

goal Equiv.thy "!w. (B(b,s) = w) --> (<b,s> -b-> w)";
by (bexp.induct_tac "b" 1);
by (rewrite_goals_tac B_simps);		(*denotational semantics*)
by (ALLGOALS (best_tac (HOL_cs addSIs (aexp2::evalb.intrs))));
val bexp_imp2 = result();

val bexp1 = bexp_imp1 RS spec RS mp |> standard;
val bexp2 = bexp_imp2 RS spec RS mp |> standard;

goal Equiv.thy "(<b,s> -b-> w) = (B(b,s) = w)";
by (fast_tac (HOL_cs addSEs [bexp1,bexp2]) 1);
val bexp_iff = result();

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,s> -c-> t ==> <s,t> : 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_simps));
  (* simplification with HOL_ss again too agressive *)
(* 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 "!io:C(c). <c,fst(io)> -c-> snd(io)";
by (com.induct_tac "c" 1);
by (rewrite_tac C_simps);
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,fst(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();