src/HOL/MicroJava/J/JBasis.thy
author haftmann
Mon Mar 01 13:40:23 2010 +0100 (2010-03-01 ago)
changeset 35416 d8d7d1b785af
parent 24783 5a3e336a2e37
child 41589 bbd861837ebc
permissions -rw-r--r--
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
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
 
haftmann@35416
    18
definition unique :: "('a \<times> 'b) list => bool" where
nipkow@12888
    19
  "unique  == distinct \<circ> map fst"
nipkow@8011
    20
oheimb@11026
    21
oheimb@11026
    22
lemma fst_in_set_lemma [rule_format (no_asm)]: 
oheimb@11026
    23
      "(x, y) : set xys --> x : fst ` set xys"
oheimb@11026
    24
apply (induct_tac "xys")
oheimb@11026
    25
apply  auto
oheimb@11026
    26
done
oheimb@11026
    27
oheimb@11026
    28
lemma unique_Nil [simp]: "unique []"
oheimb@11026
    29
apply (unfold unique_def)
oheimb@11026
    30
apply (simp (no_asm))
oheimb@11026
    31
done
oheimb@11026
    32
oheimb@11026
    33
lemma unique_Cons [simp]: "unique ((x,y)#l) = (unique l & (!y. (x,y) ~: set l))"
oheimb@11026
    34
apply (unfold unique_def)
oheimb@11026
    35
apply (auto dest: fst_in_set_lemma)
oheimb@11026
    36
done
oheimb@11026
    37
oheimb@11026
    38
lemma unique_append [rule_format (no_asm)]: "unique l' ==> unique l --> 
oheimb@11026
    39
 (!(x,y):set l. !(x',y'):set l'. x' ~= x) --> unique (l @ l')"
oheimb@11026
    40
apply (induct_tac "l")
oheimb@11026
    41
apply  (auto dest: fst_in_set_lemma)
oheimb@11026
    42
done
oheimb@11026
    43
oheimb@11026
    44
lemma unique_map_inj [rule_format (no_asm)]: 
oheimb@11026
    45
  "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)"
oheimb@11026
    46
apply (induct_tac "l")
oheimb@11026
    47
apply  (auto dest: fst_in_set_lemma simp add: inj_eq)
oheimb@11026
    48
done
oheimb@11026
    49
oheimb@11026
    50
section "More about Maps"
oheimb@11026
    51
oheimb@11026
    52
lemma map_of_SomeI [rule_format (no_asm)]: 
oheimb@11026
    53
  "unique l --> (k, x) : set l --> map_of l k = Some x"
oheimb@11026
    54
apply (induct_tac "l")
oheimb@11026
    55
apply  auto
oheimb@11026
    56
done
oheimb@11026
    57
wenzelm@24783
    58
lemma Ball_set_table': 
oheimb@11070
    59
  "(\<forall>(x,y)\<in>set l. P x y) --> (\<forall>x. \<forall>y. map_of l x = Some y --> P x y)"
oheimb@11026
    60
apply(induct_tac "l")
oheimb@11026
    61
apply(simp_all (no_asm))
oheimb@11026
    62
apply safe
oheimb@11026
    63
apply auto
oheimb@11026
    64
done
wenzelm@24783
    65
lemmas Ball_set_table = Ball_set_table' [THEN mp];
oheimb@11026
    66
oheimb@11026
    67
lemma table_of_remap_SomeD [rule_format (no_asm)]: 
oheimb@11026
    68
"map_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> 
oheimb@11026
    69
 map_of t (k, k') = Some x"
oheimb@11026
    70
apply (induct_tac "t")
oheimb@11026
    71
apply  auto
oheimb@11026
    72
done
oheimb@11026
    73
nipkow@8011
    74
end