author | wenzelm |
Fri, 25 Nov 2011 21:27:16 +0100 | |
changeset 45634 | b3dce535960f |
parent 44035 | 322d1657c40c |
child 58886 | 8a6cac7c7247 |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/J/JBasis.thy |
41589 | 2 |
Author: David von Oheimb, TU Muenchen |
11070 | 3 |
*) |
8011 | 4 |
|
12911 | 5 |
header {* |
6 |
\chapter{Java Source Language}\label{cha:j} |
|
7 |
\isaheader{Some Auxiliary Definitions} |
|
8 |
*} |
|
8011 | 9 |
|
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41589
diff
changeset
|
10 |
theory JBasis imports Main "~~/src/HOL/Library/Transitive_Closure_Table" begin |
8011 | 11 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
12 |
lemmas [simp] = Let_def |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
13 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
14 |
section "unique" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
15 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
24783
diff
changeset
|
16 |
definition unique :: "('a \<times> 'b) list => bool" where |
45634 | 17 |
"unique == distinct \<circ> map fst" |
8011 | 18 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
19 |
|
45634 | 20 |
lemma fst_in_set_lemma: "(x, y) : set xys ==> x : fst ` set xys" |
21 |
by (induct xys) auto |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
22 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
23 |
lemma unique_Nil [simp]: "unique []" |
45634 | 24 |
by (simp add: unique_def) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
25 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
26 |
lemma unique_Cons [simp]: "unique ((x,y)#l) = (unique l & (!y. (x,y) ~: set l))" |
45634 | 27 |
by (auto simp: unique_def dest: fst_in_set_lemma) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
28 |
|
45634 | 29 |
lemma unique_append: "unique l' ==> unique l ==> |
30 |
(!(x,y):set l. !(x',y'):set l'. x' ~= x) ==> unique (l @ l')" |
|
31 |
by (induct l) (auto dest: fst_in_set_lemma) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
32 |
|
45634 | 33 |
lemma unique_map_inj: "unique l ==> inj f ==> unique (map (%(k,x). (f k, g k x)) l)" |
34 |
by (induct l) (auto dest: fst_in_set_lemma simp add: inj_eq) |
|
35 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
36 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
37 |
section "More about Maps" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
38 |
|
45634 | 39 |
lemma map_of_SomeI: "unique l ==> (k, x) : set l ==> map_of l k = Some x" |
40 |
by (induct l) auto |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
41 |
|
45634 | 42 |
lemma Ball_set_table: "(\<forall>(x,y)\<in>set l. P x y) ==> (\<forall>x. \<forall>y. map_of l x = Some y --> P x y)" |
43 |
by (induct l) auto |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
44 |
|
45634 | 45 |
lemma table_of_remap_SomeD: |
46 |
"map_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) ==> |
|
47 |
map_of t (k, k') = Some x" |
|
48 |
by (atomize (full), induct t) auto |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
49 |
|
8011 | 50 |
end |