9791
|
1 |
(* Title: HOL/BCV/DFAandWTI.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 2000 TUM
|
|
5 |
*)
|
|
6 |
|
|
7 |
Goalw [wti_is_stable_topless_def]
|
|
8 |
"[| wti_is_stable_topless r T step wti succs n A; \
|
|
9 |
\ ss : list n A; !p<n. ss!p ~= T; p < n |] ==> \
|
|
10 |
\ wti ss p = stable r step succs ss p";
|
|
11 |
by (Asm_simp_tac 1);
|
|
12 |
qed "wti_is_stable_toplessD";
|
|
13 |
|
|
14 |
Goalw [is_dfa_def]
|
|
15 |
"[| is_dfa r dfa step succs n A; ss : list n A |] ==> \
|
|
16 |
\ dfa ss:list n A & stables r step succs (dfa ss) & ss <=[r] dfa ss & \
|
|
17 |
\ (!ts: list n A. stables r step succs ts & ss <=[r] ts \
|
|
18 |
\ --> dfa ss <=[r] ts)";
|
|
19 |
by (Asm_full_simp_tac 1);
|
|
20 |
qed "is_dfaD";
|
|
21 |
|
|
22 |
Goalw [is_bcv_def,welltyping_def,stables_def]
|
|
23 |
"[| order r; top r T; \
|
|
24 |
\ wti_is_stable_topless r T step wti succs n A; \
|
|
25 |
\ is_dfa r dfa step succs n A |] ==> is_bcv r T wti n A dfa";
|
10172
|
26 |
by (Clarify_tac 1);
|
9791
|
27 |
by (dtac is_dfaD 1);
|
|
28 |
by (assume_tac 1);
|
10172
|
29 |
by (Clarify_tac 1);
|
|
30 |
by (rtac iffI 1);
|
|
31 |
by (rtac bexI 1);
|
|
32 |
by (rtac conjI 1);
|
|
33 |
by (assume_tac 1);
|
9791
|
34 |
by (asm_full_simp_tac
|
|
35 |
(simpset() addsimps[wti_is_stable_toplessD,stables_def]) 1);
|
10172
|
36 |
by (assume_tac 1);
|
|
37 |
by (Clarify_tac 1);
|
|
38 |
by (asm_full_simp_tac
|
9791
|
39 |
(simpset() addsimps [imp_conjR,all_conj_distrib,wti_is_stable_toplessD,
|
|
40 |
stables_def] addcongs [conj_cong]) 1);
|
10172
|
41 |
by (dres_inst_tac [("x","ts")] bspec 1);
|
|
42 |
by (assume_tac 1);
|
9791
|
43 |
by (force_tac (claset()addDs [le_listD],simpset()) 1);
|
|
44 |
qed "is_bcv_dfa";
|
|
45 |
|
|
46 |
(*
|
|
47 |
Goal
|
|
48 |
"x:M ==> replicate n x : list n M";
|
|
49 |
by (induct_tac "n" 1);
|
|
50 |
by (Simp_tac 1);
|
|
51 |
by (asm_simp_tac (simpset() addsimps [in_list_Suc_iff,Bex_def]) 1);
|
|
52 |
qed "replicate_in_list";
|
|
53 |
Addsimps [replicate_in_list];
|
|
54 |
|
|
55 |
Goal "!ys. replicate n x <= ys = (length ys = n & (!y:set ys. x <= y))";
|
|
56 |
by (induct_tac "n" 1);
|
|
57 |
by (Force_tac 1);
|
|
58 |
by (asm_full_simp_tac (simpset() addsimps [Cons_le_iff,length_Suc_conv]) 1);
|
|
59 |
by (Force_tac 1);
|
|
60 |
qed_spec_mp "replicate_le_conv";
|
|
61 |
AddIffs [replicate_le_conv];
|
|
62 |
|
|
63 |
Goal
|
|
64 |
"[| wti_is_stable_topless step wti succs n A; is_dfa dfa step succs n A; \
|
|
65 |
\ 0 < n; init : (option A) |] ==> \
|
|
66 |
\ dfa (init # replicate (n-1) None) = \
|
|
67 |
\ (? tos : list n (option A). init <= tos!0 & welltyping wti tos)";
|
|
68 |
by (subgoal_tac "? m. n = m+1" 1);
|
|
69 |
by (res_inst_tac [("x","n-1")] exI 2);
|
|
70 |
by (arith_tac 2);
|
|
71 |
by (Clarify_tac 1);
|
|
72 |
by (Asm_full_simp_tac 1);
|
|
73 |
by (dtac dfa_iff_welltyping 1);
|
|
74 |
by (assume_tac 1);
|
|
75 |
by (etac trans 2);
|
|
76 |
by (asm_simp_tac (simpset() addsimps [in_list_Suc_iff,Bex_def]) 1);
|
|
77 |
by (asm_full_simp_tac (simpset() addsimps [Cons_le_iff]) 1);
|
|
78 |
by (rtac iffI 1);
|
|
79 |
by (Clarify_tac 1);
|
|
80 |
by (rtac bexI 1);
|
|
81 |
by (rtac conjI 1);
|
|
82 |
by (assume_tac 2);
|
|
83 |
by (assume_tac 2);
|
|
84 |
by (Asm_simp_tac 1);
|
|
85 |
by (Clarify_tac 1);
|
|
86 |
by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff,Bex_def]) 1);
|
|
87 |
by (Clarify_tac 1);
|
|
88 |
by (asm_full_simp_tac (simpset() addsimps []) 1);
|
|
89 |
by (rtac exI 1);
|
|
90 |
by (rtac conjI 1);
|
|
91 |
by (rtac conjI 2);
|
|
92 |
by (assume_tac 3);
|
|
93 |
by (Blast_tac 1);
|
|
94 |
by (Force_tac 1);
|
|
95 |
qed "dfa_iff_welltyping0";
|
|
96 |
*)
|