author | haftmann |
Mon, 01 Mar 2010 13:40:23 +0100 | |
changeset 35416 | d8d7d1b785af |
parent 24783 | 5a3e336a2e37 |
child 41589 | bbd861837ebc |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/J/JBasis.thy |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb |
|
4 |
Copyright 1999 TU Muenchen |
|
11070 | 5 |
*) |
8011 | 6 |
|
12911 | 7 |
header {* |
8 |
\chapter{Java Source Language}\label{cha:j} |
|
9 |
\isaheader{Some Auxiliary Definitions} |
|
10 |
*} |
|
8011 | 11 |
|
16417 | 12 |
theory JBasis imports Main begin |
8011 | 13 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
14 |
lemmas [simp] = Let_def |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
15 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
16 |
section "unique" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
17 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
24783
diff
changeset
|
18 |
definition unique :: "('a \<times> 'b) list => bool" where |
12888 | 19 |
"unique == distinct \<circ> map fst" |
8011 | 20 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
21 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
22 |
lemma fst_in_set_lemma [rule_format (no_asm)]: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
23 |
"(x, y) : set xys --> x : fst ` set xys" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
24 |
apply (induct_tac "xys") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
25 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
26 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
27 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
28 |
lemma unique_Nil [simp]: "unique []" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
29 |
apply (unfold unique_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
30 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
31 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
32 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
33 |
lemma unique_Cons [simp]: "unique ((x,y)#l) = (unique l & (!y. (x,y) ~: set l))" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
34 |
apply (unfold unique_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
35 |
apply (auto dest: fst_in_set_lemma) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
36 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
37 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
38 |
lemma unique_append [rule_format (no_asm)]: "unique l' ==> unique l --> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
39 |
(!(x,y):set l. !(x',y'):set l'. x' ~= x) --> unique (l @ l')" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
40 |
apply (induct_tac "l") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
41 |
apply (auto dest: fst_in_set_lemma) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
42 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
43 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
44 |
lemma unique_map_inj [rule_format (no_asm)]: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
45 |
"unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
46 |
apply (induct_tac "l") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
47 |
apply (auto dest: fst_in_set_lemma simp add: inj_eq) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
48 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
49 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
50 |
section "More about Maps" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
51 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
52 |
lemma map_of_SomeI [rule_format (no_asm)]: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
53 |
"unique l --> (k, x) : set l --> map_of l k = Some x" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
54 |
apply (induct_tac "l") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
55 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
56 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
57 |
|
24783 | 58 |
lemma Ball_set_table': |
11070 | 59 |
"(\<forall>(x,y)\<in>set l. P x y) --> (\<forall>x. \<forall>y. map_of l x = Some y --> P x y)" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
60 |
apply(induct_tac "l") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
61 |
apply(simp_all (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
62 |
apply safe |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
63 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
64 |
done |
24783 | 65 |
lemmas Ball_set_table = Ball_set_table' [THEN mp]; |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
66 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
67 |
lemma table_of_remap_SomeD [rule_format (no_asm)]: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
68 |
"map_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
69 |
map_of t (k, k') = Some x" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
70 |
apply (induct_tac "t") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
71 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
72 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10042
diff
changeset
|
73 |
|
8011 | 74 |
end |