src/HOL/BCV/DFAandWTI.ML

A new theory: a model of bytecode verification.

(*  Title:      HOL/BCV/DFAandWTI.ML
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1999 TUM
*)

Goalw [wti_is_fix_step_def]
 "[| wti_is_fix_step step wti succs n L; \
\    sos : listsn n (option L); p < n |] ==> \
\ wti p sos = stable step succs p sos";
by(Asm_simp_tac 1);
qed "wti_is_fix_stepD";

Goalw [is_dfa_def]
 "[| is_dfa dfa step succs n L; sos : listsn n (option L) |] ==> \
\ dfa sos = (? tos : listsn (size sos) (option L). \
\             sos <= tos & (!p < size tos. stable step succs p tos))";
by(Asm_simp_tac 1);
qed "is_dfaD";

Goalw [welltyping_def]
 "[| wti_is_fix_step step wti succs n L; is_dfa dfa step succs n L; \
\    sos : listsn n (option L) |] ==> \
\ dfa sos = (? tos : listsn n (option L). sos <= tos & welltyping wti tos)";
bd is_dfaD 1;
ba 1;
by(Asm_full_simp_tac 1);
by(blast_tac (claset() addDs [wti_is_fix_stepD]) 1);
qed "dfa_iff_welltyping";

Goal
 "x:M ==> replicate n x : listsn n M";
by(induct_tac "n" 1);
by(Simp_tac 1);
by(asm_simp_tac (simpset() addsimps [in_listsn_Suc_iff,Bex_def]) 1);
qed "replicate_in_listsn";
Addsimps [replicate_in_listsn];

Goal "!ys. replicate n x <= ys = (length ys = n & (!y:set ys. x <= y))";
by(induct_tac "n" 1);
 by(Force_tac 1);
by(asm_full_simp_tac (simpset() addsimps [Cons_le_iff,length_Suc_conv]) 1);
by(Force_tac 1);
qed_spec_mp "replicate_le_conv";
AddIffs [replicate_le_conv];

Goal
 "[| wti_is_fix_step step wti succs n L; is_dfa dfa step succs n L; \
\    0 < n; init : (option L) |] ==> \
\ dfa (init # replicate (n-1) None) = \
\ (? tos : listsn n (option L). init <= tos!0 & welltyping wti tos)";
by(subgoal_tac "? m. n = m+1" 1);
 by(res_inst_tac [("x","n-1")] exI 2);
 by(arith_tac 2);
by(Clarify_tac 1);
by(Asm_full_simp_tac 1);
bd dfa_iff_welltyping 1;
  ba 1;
 be trans 2;
 by(asm_simp_tac (simpset() addsimps [in_listsn_Suc_iff,Bex_def]) 1);
by(asm_full_simp_tac (simpset() addsimps [Cons_le_iff]) 1);
br iffI 1;
 by(Clarify_tac 1);
 br bexI 1;
  br conjI 1;
   ba 2;
  ba 2;
 by(Asm_simp_tac 1);
by(Clarify_tac 1);
by(asm_full_simp_tac (simpset() addsimps [in_listsn_Suc_iff,Bex_def]) 1);
by(Clarify_tac 1);
by(asm_full_simp_tac (simpset() addsimps []) 1);
br exI 1;
br conjI 1;
 br conjI 2;
  ba 3;
 by(Blast_tac 1);
by(Force_tac 1);
qed "dfa_iff_welltyping0";