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