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