author | wenzelm |
Mon, 03 Apr 2000 14:02:40 +0200 | |
changeset 8662 | f9679ddbc492 |
parent 8442 | 96023903c2df |
permissions | -rw-r--r-- |
7626 | 1 |
(* Title: HOL/BCV/Machine.ML |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1999 TUM |
|
5 |
*) |
|
6 |
||
7 |
Addsimps [Let_def]; |
|
8 |
||
9 |
Addsimps [stype_def]; |
|
10 |
||
11 |
||
12 |
(*** Machine specific ***) |
|
13 |
||
14 |
Goal "!p. p<size(bs) --> maxreg(bs!p) < maxregs(bs)"; |
|
7961 | 15 |
by (induct_tac "bs" 1); |
16 |
by (auto_tac (claset(), simpset() addsimps [nth_Cons,less_max_iff_disj] |
|
7626 | 17 |
addsplits [nat.split])); |
18 |
qed_spec_mp "maxreg_less_maxregs"; |
|
19 |
||
20 |
Goalw [le_typ] "(t <= Ctyp) = (t = Ctyp)"; |
|
7961 | 21 |
by (Simp_tac 1); |
7626 | 22 |
qed "le_Ctyp_conv"; |
23 |
||
24 |
Goalw [le_typ] "(t ~= Top) = (t = Atyp | t = Btyp | t = Ctyp)"; |
|
7961 | 25 |
by (induct_tac "t" 1); |
26 |
by (ALLGOALS Simp_tac); |
|
7626 | 27 |
qed "le_Top_conv"; |
28 |
||
29 |
Goalw [step_pres_type_def,listsn_def,exec_def,stype_def] |
|
30 |
"step_pres_type (%p. exec (bs!p)) (length bs) (stype bs)"; |
|
7961 | 31 |
by (force_tac (claset(), simpset() addsplits [instr.split_asm,split_if_asm]) 1); |
7626 | 32 |
qed "exec_pres_type"; |
33 |
||
34 |
Goalw [wti_is_fix_step_def,stable_def,wt_instr_def,exec_def,succs_def] |
|
35 |
"wti_is_fix_step (%p. exec (bs!p)) (%u. wt_instr (bs ! u) u) \ |
|
36 |
\ (%p. succs (bs ! p) p) (length bs) (stype bs)"; |
|
7961 | 37 |
by (force_tac (claset() addDs [maxreg_less_maxregs, |
7626 | 38 |
le_Top_conv RS iffD1,le_Ctyp_conv RS iffD1], |
39 |
simpset() addsplits [option.split,instr.split]) 1); |
|
40 |
qed "wt_instr_is_fix_exec"; |
|
41 |
||
42 |
||
43 |
Goalw [step_mono_None_def,exec_def,succs_def,le_list] |
|
44 |
"step_mono_None (%p. exec (bs!p)) (length bs) (stype bs)"; |
|
7961 | 45 |
by (Clarify_tac 1); |
46 |
by (ftac maxreg_less_maxregs 1); |
|
47 |
by (split_asm_tac [instr.split_asm] 1); |
|
7626 | 48 |
|
7961 | 49 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsplits [split_if_asm]))); |
7626 | 50 |
|
7961 | 51 |
by (rotate_tac 1 1); |
52 |
by (Asm_full_simp_tac 1); |
|
53 |
by (blast_tac (claset() addIs [order_trans]) 1); |
|
7626 | 54 |
|
7961 | 55 |
by (rotate_tac 1 1); |
56 |
by (Asm_full_simp_tac 1); |
|
57 |
by (blast_tac (claset() addIs [order_trans]) 1); |
|
7626 | 58 |
|
7961 | 59 |
by (rotate_tac 1 1); |
60 |
by (Asm_full_simp_tac 1); |
|
61 |
by (blast_tac (claset() addIs [order_trans]) 1); |
|
7626 | 62 |
|
7961 | 63 |
by (rotate_tac 1 1); |
64 |
by (Asm_full_simp_tac 1); |
|
65 |
by (subgoal_tac "s!nat1 <= t!nat1" 1); |
|
66 |
by (Blast_tac 2); |
|
67 |
by (subgoal_tac "s!nat2 <= t!nat2" 1); |
|
68 |
by (Blast_tac 2); |
|
69 |
by (etac thin_rl 1); |
|
70 |
by (asm_full_simp_tac (simpset() addsimps [le_typ])1); |
|
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
71 |
by (case_tac "t!nat1" 1); |
7961 | 72 |
by (ALLGOALS Asm_full_simp_tac); |
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
73 |
by (case_tac "t!nat2" 1); |
7961 | 74 |
by (ALLGOALS Asm_full_simp_tac); |
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
75 |
by (case_tac "t!nat2" 1); |
7961 | 76 |
by (ALLGOALS Asm_full_simp_tac); |
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
77 |
by (case_tac "s!nat1" 1); |
7961 | 78 |
by (ALLGOALS Asm_full_simp_tac); |
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
79 |
by (case_tac "t!nat2" 1); |
7961 | 80 |
by (ALLGOALS Asm_full_simp_tac); |
7626 | 81 |
|
82 |
qed "exec_mono_None"; |
|
83 |
||
84 |
Goalw [step_mono_def,exec_def,succs_def] |
|
85 |
"step_mono (%p. exec (bs!p)) (length bs) (stype bs)"; |
|
7961 | 86 |
by (Clarify_tac 1); |
87 |
by (ftac maxreg_less_maxregs 1); |
|
88 |
by (split_asm_tac [instr.split_asm] 1); |
|
89 |
by (ALLGOALS |
|
7626 | 90 |
(fast_tac (claset() addIs [list_update_le_cong,le_listD] |
91 |
addss (simpset() addsplits [split_if_asm])))); |
|
92 |
||
93 |
qed_spec_mp "exec_mono_Some"; |
|
94 |
||
95 |
Goalw [stype_def] "semilat(stype bs)"; |
|
7961 | 96 |
by (Blast_tac 1); |
7626 | 97 |
qed "lat_stype"; |
98 |
||
99 |
Goalw [stype_def] "acc(stype bs)"; |
|
7961 | 100 |
by (Simp_tac 1); |
7626 | 101 |
qed "acc_stype"; |
102 |
||
103 |
Delsimps [stype_def]; |
|
104 |
||
105 |
Goal |
|
106 |
"[| is_next next; \ |
|
107 |
\ succs_bounded (%p. succs (bs!p) p) (size bs); \ |
|
108 |
\ sos : listsn (size bs) (option(stype bs)) |] ==> \ |
|
109 |
\ fix(next (%p. exec (bs!p)) (%p. succs (bs!p) p), sos) = \ |
|
110 |
\ (? tos : listsn (size bs) (option(stype bs)). \ |
|
111 |
\ sos <= tos & welltyping (%p. wt_instr (bs!p) p) tos)"; |
|
7961 | 112 |
by (simp_tac (simpset() delsimps [not_None_eq]) 1); |
113 |
by (REPEAT(ares_tac [fix_next_iff_welltyping,exec_pres_type, |
|
7626 | 114 |
exec_mono_None,exec_mono_Some, |
115 |
wt_instr_is_fix_exec,lat_stype,acc_stype] 1)); |
|
116 |
||
117 |
qed "fix_iff_welltyped"; |