author | paulson <lp15@cam.ac.uk> |
Wed, 24 Apr 2024 20:56:26 +0100 | |
changeset 80149 | 40a3fc07a587 |
parent 67613 | ce654b0e6d69 |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/J/JBasis.thy |
41589 | 2 |
Author: David von Oheimb, TU Muenchen |
11070 | 3 |
*) |
8011 | 4 |
|
61361 | 5 |
chapter \<open>Java Source Language \label{cha:j}\<close> |
58886 | 6 |
|
61361 | 7 |
section \<open>Some Auxiliary Definitions\<close> |
8011 | 8 |
|
63258 | 9 |
theory JBasis |
10 |
imports |
|
11 |
Main |
|
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
63258
diff
changeset
|
12 |
"HOL-Library.Transitive_Closure_Table" |
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
63258
diff
changeset
|
13 |
"HOL-Eisbach.Eisbach" |
63258 | 14 |
begin |
8011 | 15 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
16 |
lemmas [simp] = Let_def |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
17 |
|
58886 | 18 |
subsection "unique" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
19 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
24783
diff
changeset
|
20 |
definition unique :: "('a \<times> 'b) list => bool" where |
45634 | 21 |
"unique == distinct \<circ> map fst" |
8011 | 22 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
23 |
|
67613 | 24 |
lemma fst_in_set_lemma: "(x, y) \<in> set xys \<Longrightarrow> x \<in> fst ` set xys" |
45634 | 25 |
by (induct xys) auto |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
26 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
27 |
lemma unique_Nil [simp]: "unique []" |
45634 | 28 |
by (simp add: unique_def) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
29 |
|
67613 | 30 |
lemma unique_Cons [simp]: "unique ((x,y)#l) = (unique l & (\<forall>y. (x,y) \<notin> set l))" |
45634 | 31 |
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
|
32 |
|
67613 | 33 |
lemma unique_append: "unique l' \<Longrightarrow> unique l \<Longrightarrow> |
34 |
(\<forall>(x,y) \<in> set l. \<forall>(x',y') \<in> set l'. x' \<noteq> x) \<Longrightarrow> unique (l @ l')" |
|
45634 | 35 |
by (induct l) (auto dest: fst_in_set_lemma) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
36 |
|
45634 | 37 |
lemma unique_map_inj: "unique l ==> inj f ==> unique (map (%(k,x). (f k, g k x)) l)" |
38 |
by (induct l) (auto dest: fst_in_set_lemma simp add: inj_eq) |
|
39 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
40 |
|
58886 | 41 |
subsection "More about Maps" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
42 |
|
67613 | 43 |
lemma map_of_SomeI: "unique l \<Longrightarrow> (k, x) \<in> set l \<Longrightarrow> map_of l k = Some x" |
45634 | 44 |
by (induct l) auto |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
45 |
|
45634 | 46 |
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)" |
47 |
by (induct l) auto |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
48 |
|
45634 | 49 |
lemma table_of_remap_SomeD: |
50 |
"map_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) ==> |
|
51 |
map_of t (k, k') = Some x" |
|
52 |
by (atomize (full), induct t) auto |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
53 |
|
8011 | 54 |
end |