|
12516
|
1 |
(* Title: HOL/MicroJava/BV/Kildall_Lift.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Gerwin Klein
|
|
|
4 |
Copyright 2001 TUM
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
theory Kildall_Lift = Kildall + Typing_Framework_err:
|
|
|
8 |
|
|
|
9 |
constdefs
|
|
|
10 |
app_mono :: "'s ord \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
|
|
|
11 |
"app_mono r app n A ==
|
|
|
12 |
\<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> app p t \<longrightarrow> app p s"
|
|
|
13 |
|
|
13066
|
14 |
lemma bounded_lift:
|
|
|
15 |
"bounded step n \<Longrightarrow> bounded (err_step n app step) n"
|
|
|
16 |
apply (unfold bounded_def err_step_def error_def)
|
|
|
17 |
apply clarify
|
|
|
18 |
apply (erule allE, erule impE, assumption)
|
|
|
19 |
apply (case_tac s)
|
|
|
20 |
apply (auto simp add: map_snd_def split: split_if_asm)
|
|
|
21 |
done
|
|
12516
|
22 |
|
|
|
23 |
lemma le_list_map_OK [simp]:
|
|
|
24 |
"\<And>b. map OK a <=[Err.le r] map OK b = (a <=[r] b)"
|
|
|
25 |
apply (induct a)
|
|
|
26 |
apply simp
|
|
|
27 |
apply simp
|
|
|
28 |
apply (case_tac b)
|
|
|
29 |
apply simp
|
|
|
30 |
apply simp
|
|
|
31 |
done
|
|
|
32 |
|
|
13066
|
33 |
|
|
|
34 |
lemma map_snd_lessI:
|
|
|
35 |
"x <=|r| y \<Longrightarrow> map_snd OK x <=|Err.le r| map_snd OK y"
|
|
|
36 |
apply (induct x)
|
|
|
37 |
apply (unfold lesubstep_type_def map_snd_def)
|
|
|
38 |
apply auto
|
|
|
39 |
done
|
|
|
40 |
|
|
|
41 |
|
|
12516
|
42 |
lemma mono_lift:
|
|
13066
|
43 |
"order r \<Longrightarrow> app_mono r app n A \<Longrightarrow> bounded (err_step n app step) n \<Longrightarrow>
|
|
12516
|
44 |
\<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> app p t \<longrightarrow> step p s <=|r| step p t \<Longrightarrow>
|
|
13066
|
45 |
mono (Err.le r) (err_step n app step) n (err A)"
|
|
12516
|
46 |
apply (unfold app_mono_def mono_def err_step_def)
|
|
|
47 |
apply clarify
|
|
|
48 |
apply (case_tac s)
|
|
13066
|
49 |
apply simp
|
|
12516
|
50 |
apply simp
|
|
|
51 |
apply (case_tac t)
|
|
|
52 |
apply simp
|
|
|
53 |
apply clarify
|
|
13066
|
54 |
apply (simp add: lesubstep_type_def error_def)
|
|
|
55 |
apply clarify
|
|
|
56 |
apply (drule in_map_sndD)
|
|
12516
|
57 |
apply clarify
|
|
13067
|
58 |
apply (drule bounded_err_stepD, assumption+)
|
|
13066
|
59 |
apply (rule exI [of _ Err])
|
|
|
60 |
apply simp
|
|
|
61 |
apply simp
|
|
|
62 |
apply (erule allE, erule allE, erule allE, erule impE)
|
|
|
63 |
apply (rule conjI, assumption)
|
|
|
64 |
apply (rule conjI, assumption)
|
|
|
65 |
apply assumption
|
|
12516
|
66 |
apply (rule conjI)
|
|
13066
|
67 |
apply clarify
|
|
|
68 |
apply (erule allE, erule allE, erule allE, erule impE)
|
|
|
69 |
apply (rule conjI, assumption)
|
|
|
70 |
apply (rule conjI, assumption)
|
|
|
71 |
apply assumption
|
|
|
72 |
apply (erule impE, assumption)
|
|
|
73 |
apply (rule map_snd_lessI, assumption)
|
|
12516
|
74 |
apply clarify
|
|
13066
|
75 |
apply (simp add: lesubstep_type_def error_def)
|
|
|
76 |
apply clarify
|
|
|
77 |
apply (drule in_map_sndD)
|
|
|
78 |
apply clarify
|
|
13067
|
79 |
apply (drule bounded_err_stepD, assumption+)
|
|
13066
|
80 |
apply (rule exI [of _ Err])
|
|
|
81 |
apply simp
|
|
12516
|
82 |
done
|
|
|
83 |
|
|
13066
|
84 |
lemma in_errorD:
|
|
|
85 |
"(x,y) \<in> set (error n) \<Longrightarrow> y = Err"
|
|
|
86 |
by (auto simp add: error_def)
|
|
12516
|
87 |
|
|
|
88 |
lemma pres_type_lift:
|
|
|
89 |
"\<forall>s\<in>A. \<forall>p. p < n \<longrightarrow> app p s \<longrightarrow> (\<forall>(q, s')\<in>set (step p s). s' \<in> A)
|
|
13066
|
90 |
\<Longrightarrow> pres_type (err_step n app step) n (err A)"
|
|
12516
|
91 |
apply (unfold pres_type_def err_step_def)
|
|
|
92 |
apply clarify
|
|
|
93 |
apply (case_tac b)
|
|
|
94 |
apply simp
|
|
|
95 |
apply (case_tac s)
|
|
13066
|
96 |
apply simp
|
|
|
97 |
apply (drule in_errorD)
|
|
12516
|
98 |
apply simp
|
|
13066
|
99 |
apply (simp add: map_snd_def split: split_if_asm)
|
|
|
100 |
apply fast
|
|
|
101 |
apply (drule in_errorD)
|
|
12516
|
102 |
apply simp
|
|
|
103 |
done
|
|
|
104 |
|
|
|
105 |
end
|