author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45151  2dd44cd8f963 
child 51304  0e71a248cacb 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/Basis.thy 
12854  2 
Author: David von Oheimb 
3 
*) 

4 
header {* Definitions extending HOL as logical basis of Bali *} 

5 

45151  6 
theory Basis 
7 
imports Main "~~/src/HOL/Library/Old_Recdef" 

8 
begin 

12854  9 

10 
section "misc" 

11 

12 
declare split_if_asm [split] option.split [split] option.split_asm [split] 

24019  13 
declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *} 
12854  14 
declare if_weak_cong [cong del] option.weak_case_cong [cong del] 
18447  15 
declare length_Suc_conv [iff] 
16 

12854  17 
lemma Collect_split_eq: "{p. P (split f p)} = {(a,b). P (f a b)}" 
45151  18 
by auto 
12854  19 

45151  20 
lemma subset_insertD: "A \<subseteq> insert x B \<Longrightarrow> A \<subseteq> B \<and> x \<notin> A \<or> (\<exists>B'. A = insert x B' \<and> B' \<subseteq> B)" 
21 
apply (case_tac "x \<in> A") 

22 
apply (rule disjI2) 

23 
apply (rule_tac x = "A  {x}" in exI) 

24 
apply fast+ 

25 
done 

12854  26 

45151  27 
abbreviation nat3 :: nat ("3") where "3 \<equiv> Suc 2" 
28 
abbreviation nat4 :: nat ("4") where "4 \<equiv> Suc 3" 

12854  29 

13867  30 
(* irrefl_tranclI in Transitive_Closure.thy is more general *) 
45151  31 
lemma irrefl_tranclI': "r\<inverse> \<inter> r\<^sup>+ = {} \<Longrightarrow> \<forall>x. (x, x) \<notin> r\<^sup>+" 
32 
by (blast elim: tranclE dest: trancl_into_rtrancl) 

13867  33 

12854  34 

45151  35 
lemma trancl_rtrancl_trancl: "\<lbrakk>(x, y) \<in> r\<^sup>+; (y, z) \<in> r\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> r\<^sup>+" 
36 
by (auto dest: tranclD rtrancl_trans rtrancl_into_trancl2) 

12854  37 

45151  38 
lemma rtrancl_into_trancl3: "\<lbrakk>(a, b) \<in> r\<^sup>*; a \<noteq> b\<rbrakk> \<Longrightarrow> (a, b) \<in> r\<^sup>+" 
39 
apply (drule rtranclD) 

40 
apply auto 

41 
done 

12854  42 

45151  43 
lemma rtrancl_into_rtrancl2: "\<lbrakk>(a, b) \<in> r; (b, c) \<in> r\<^sup>*\<rbrakk> \<Longrightarrow> (a, c) \<in> r\<^sup>*" 
44 
by (auto intro: rtrancl_trans) 

12854  45 

46 
lemma triangle_lemma: 

45151  47 
assumes unique: "\<And>a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b = c" 
48 
and ax: "(a,x)\<in>r\<^sup>*" and ay: "(a,y)\<in>r\<^sup>*" 

49 
shows "(x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*" 

50 
using ax ay 

51 
proof (induct rule: converse_rtrancl_induct) 

52 
assume "(x,y)\<in>r\<^sup>*" 

53 
then show ?thesis by blast 

54 
next 

55 
fix a v 

56 
assume a_v_r: "(a, v) \<in> r" 

57 
and v_x_rt: "(v, x) \<in> r\<^sup>*" 

58 
and a_y_rt: "(a, y) \<in> r\<^sup>*" 

59 
and hyp: "(v, y) \<in> r\<^sup>* \<Longrightarrow> (x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*" 

60 
from a_y_rt show "(x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*" 

61 
proof (cases rule: converse_rtranclE) 

62 
assume "a = y" 

63 
with a_v_r v_x_rt have "(y,x) \<in> r\<^sup>*" 

64 
by (auto intro: rtrancl_trans) 

65 
then show ?thesis by blast 

12854  66 
next 
45151  67 
fix w 
68 
assume a_w_r: "(a, w) \<in> r" 

69 
and w_y_rt: "(w, y) \<in> r\<^sup>*" 

70 
from a_v_r a_w_r unique have "v=w" by auto 

71 
with w_y_rt hyp show ?thesis by blast 

12854  72 
qed 
73 
qed 

74 

75 

45151  76 
lemma rtrancl_cases: 
77 
assumes "(a,b)\<in>r\<^sup>*" 

78 
obtains (Refl) "a = b" 

79 
 (Trancl) "(a,b)\<in>r\<^sup>+" 

80 
apply (rule rtranclE [OF assms]) 

81 
apply (auto dest: rtrancl_into_trancl1) 

82 
done 

12854  83 

45151  84 
lemma Ball_weaken: "\<lbrakk>Ball s P; \<And> x. P x\<longrightarrow>Q x\<rbrakk>\<Longrightarrow>Ball s Q" 
85 
by auto 

12854  86 

45151  87 
lemma finite_SetCompr2: 
88 
"finite (Collect P) \<Longrightarrow> \<forall>y. P y \<longrightarrow> finite (range (f y)) \<Longrightarrow> 

89 
finite {f y x x y. P y}" 

90 
apply (subgoal_tac "{f y x x y. P y} = UNION (Collect P) (\<lambda>y. range (f y))") 

91 
prefer 2 apply fast 

92 
apply (erule ssubst) 

93 
apply (erule finite_UN_I) 

94 
apply fast 

95 
done 

12854  96 

45151  97 
lemma list_all2_trans: "\<forall>a b c. P1 a b \<longrightarrow> P2 b c \<longrightarrow> P3 a c \<Longrightarrow> 
98 
\<forall>xs2 xs3. list_all2 P1 xs1 xs2 \<longrightarrow> list_all2 P2 xs2 xs3 \<longrightarrow> list_all2 P3 xs1 xs3" 

99 
apply (induct_tac xs1) 

100 
apply simp 

101 
apply (rule allI) 

102 
apply (induct_tac xs2) 

103 
apply simp 

104 
apply (rule allI) 

105 
apply (induct_tac xs3) 

106 
apply auto 

107 
done 

12854  108 

109 

110 
section "pairs" 

111 

45151  112 
lemma surjective_pairing5: 
113 
"p = (fst p, fst (snd p), fst (snd (snd p)), fst (snd (snd (snd p))), 

114 
snd (snd (snd (snd p))))" 

115 
by auto 

12854  116 

45151  117 
lemma fst_splitE [elim!]: 
118 
assumes "fst s' = x'" 

119 
obtains x s where "s' = (x,s)" and "x = x'" 

120 
using assms by (cases s') auto 

12854  121 

45151  122 
lemma fst_in_set_lemma: "(x, y) : set l \<Longrightarrow> x : fst ` set l" 
123 
by (induct l) auto 

12854  124 

125 

126 
section "quantifiers" 

127 

45151  128 
lemma All_Ex_refl_eq2 [simp]: "(\<forall>x. (\<exists>b. x = f b \<and> Q b) \<longrightarrow> P x) = (\<forall>b. Q b \<longrightarrow> P (f b))" 
129 
by auto 

12854  130 

45151  131 
lemma ex_ex_miniscope1 [simp]: "(\<exists>w v. P w v \<and> Q v) = (\<exists>v. (\<exists>w. P w v) \<and> Q v)" 
132 
by auto 

12854  133 

45151  134 
lemma ex_miniscope2 [simp]: "(\<exists>v. P v \<and> Q \<and> R v) = (Q \<and> (\<exists>v. P v \<and> R v))" 
135 
by auto 

12854  136 

137 
lemma ex_reorder31: "(\<exists>z x y. P x y z) = (\<exists>x y z. P x y z)" 

45151  138 
by auto 
12854  139 

45151  140 
lemma All_Ex_refl_eq1 [simp]: "(\<forall>x. (\<exists>b. x = f b) \<longrightarrow> P x) = (\<forall>b. P (f b))" 
141 
by auto 

12854  142 

143 

144 
section "sums" 

145 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
35431
diff
changeset

146 
hide_const In0 In1 
12854  147 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34915
diff
changeset

148 
notation sum_case (infixr "'(+')"80) 
12854  149 

45151  150 
primrec the_Inl :: "'a + 'b \<Rightarrow> 'a" 
37956  151 
where "the_Inl (Inl a) = a" 
152 

45151  153 
primrec the_Inr :: "'a + 'b \<Rightarrow> 'b" 
37956  154 
where "the_Inr (Inr b) = b" 
12854  155 

156 
datatype ('a, 'b, 'c) sum3 = In1 'a  In2 'b  In3 'c 

157 

45151  158 
primrec the_In1 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a" 
37956  159 
where "the_In1 (In1 a) = a" 
160 

45151  161 
primrec the_In2 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'b" 
37956  162 
where "the_In2 (In2 b) = b" 
163 

45151  164 
primrec the_In3 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'c" 
37956  165 
where "the_In3 (In3 c) = c" 
12854  166 

45151  167 
abbreviation In1l :: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3" 
168 
where "In1l e \<equiv> In1 (Inl e)" 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34915
diff
changeset

169 

45151  170 
abbreviation In1r :: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3" 
171 
where "In1r c \<equiv> In1 (Inr c)" 

12854  172 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34915
diff
changeset

173 
abbreviation the_In1l :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'al" 
45151  174 
where "the_In1l \<equiv> the_Inl \<circ> the_In1" 
35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34915
diff
changeset

175 

af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34915
diff
changeset

176 
abbreviation the_In1r :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'ar" 
45151  177 
where "the_In1r \<equiv> the_Inr \<circ> the_In1" 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13462
diff
changeset

178 

12854  179 
ML {* 
27226  180 
fun sum3_instantiate ctxt thm = map (fn s => 
45151  181 
simplify (simpset_of ctxt delsimps [@{thm not_None_eq}]) 
27239  182 
(read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"] 
12854  183 
*} 
184 
(* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *) 

185 

186 

187 
section "quantifiers for option type" 

188 

189 
syntax 

45151  190 
"_Oall" :: "[pttrn, 'a option, bool] \<Rightarrow> bool" ("(3! _:_:/ _)" [0,0,10] 10) 
191 
"_Oex" :: "[pttrn, 'a option, bool] \<Rightarrow> bool" ("(3? _:_:/ _)" [0,0,10] 10) 

12854  192 

193 
syntax (symbols) 

45151  194 
"_Oall" :: "[pttrn, 'a option, bool] \<Rightarrow> bool" ("(3\<forall>_\<in>_:/ _)" [0,0,10] 10) 
195 
"_Oex" :: "[pttrn, 'a option, bool] \<Rightarrow> bool" ("(3\<exists>_\<in>_:/ _)" [0,0,10] 10) 

12854  196 

197 
translations 

45151  198 
"\<forall>x\<in>A: P" \<rightleftharpoons> "\<forall>x\<in>CONST Option.set A. P" 
199 
"\<exists>x\<in>A: P" \<rightleftharpoons> "\<exists>x\<in>CONST Option.set A. P" 

200 

12854  201 

19323  202 
section "Special map update" 
203 

204 
text{* Deemed too special for theory Map. *} 

205 

45151  206 
definition chg_map :: "('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" 
207 
where "chg_map f a m = (case m a of None \<Rightarrow> m  Some b \<Rightarrow> m(a\<mapsto>f b))" 

19323  208 

45151  209 
lemma chg_map_new[simp]: "m a = None \<Longrightarrow> chg_map f a m = m" 
210 
unfolding chg_map_def by auto 

19323  211 

45151  212 
lemma chg_map_upd[simp]: "m a = Some b \<Longrightarrow> chg_map f a m = m(a\<mapsto>f b)" 
213 
unfolding chg_map_def by auto 

19323  214 

215 
lemma chg_map_other [simp]: "a \<noteq> b \<Longrightarrow> chg_map f a m b = m b" 

45151  216 
by (auto simp: chg_map_def) 
19323  217 

12854  218 

219 
section "unique association lists" 

220 

45151  221 
definition unique :: "('a \<times> 'b) list \<Rightarrow> bool" 
37956  222 
where "unique = distinct \<circ> map fst" 
12854  223 

45151  224 
lemma uniqueD: "unique l \<Longrightarrow> (x, y) \<in> set l \<Longrightarrow> (x', y') \<in> set l \<Longrightarrow> x = x' \<Longrightarrow> y = y'" 
225 
unfolding unique_def o_def 

226 
by (induct l) (auto dest: fst_in_set_lemma) 

12854  227 

228 
lemma unique_Nil [simp]: "unique []" 

45151  229 
by (simp add: unique_def) 
12854  230 

45151  231 
lemma unique_Cons [simp]: "unique ((x,y)#l) = (unique l \<and> (\<forall>y. (x,y) \<notin> set l))" 
232 
by (auto simp: unique_def dest: fst_in_set_lemma) 

12854  233 

45151  234 
lemma unique_ConsD: "unique (x#xs) \<Longrightarrow> unique xs" 
235 
by (simp add: unique_def) 

12854  236 

45151  237 
lemma unique_single [simp]: "\<And>p. unique [p]" 
238 
by simp 

12854  239 

45151  240 
lemma unique_append [rule_format (no_asm)]: "unique l' \<Longrightarrow> unique l \<Longrightarrow> 
241 
(\<forall>(x,y)\<in>set l. \<forall>(x',y')\<in>set l'. x' \<noteq> x) \<longrightarrow> unique (l @ l')" 

242 
by (induct l) (auto dest: fst_in_set_lemma) 

12854  243 

45151  244 
lemma unique_map_inj: "unique l \<Longrightarrow> inj f \<Longrightarrow> unique (map (\<lambda>(k,x). (f k, g k x)) l)" 
245 
by (induct l) (auto dest: fst_in_set_lemma simp add: inj_eq) 

246 

247 
lemma map_of_SomeI: "unique l \<Longrightarrow> (k, x) : set l \<Longrightarrow> map_of l k = Some x" 

248 
by (induct l) auto 

12854  249 

250 

251 
section "list patterns" 

252 

45151  253 
definition lsplit :: "[['a, 'a list] \<Rightarrow> 'b, 'a list] \<Rightarrow> 'b" 
254 
where "lsplit = (\<lambda>f l. f (hd l) (tl l))" 

37956  255 

256 
text {* list patterns  extends predefined type "pttrn" used in abstractions *} 

12854  257 
syntax 
45151  258 
"_lpttrn" :: "[pttrn, pttrn] \<Rightarrow> pttrn" ("_#/_" [901,900] 900) 
12854  259 
translations 
45151  260 
"\<lambda>y # x # xs. b" \<rightleftharpoons> "CONST lsplit (\<lambda>y x # xs. b)" 
261 
"\<lambda>x # xs. b" \<rightleftharpoons> "CONST lsplit (\<lambda>x xs. b)" 

12854  262 

263 
lemma lsplit [simp]: "lsplit c (x#xs) = c x xs" 

45151  264 
by (simp add: lsplit_def) 
12854  265 

266 
lemma lsplit2 [simp]: "lsplit P (x#xs) y z = P x xs y z" 

45151  267 
by (simp add: lsplit_def) 
12854  268 

269 
end 