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";