src/HOL/MicroJava/J/JBasis.thy
author nipkow
Thu Feb 14 12:06:07 2002 +0100 (2002-02-14)
changeset 12888 f6c1e7306c40
parent 12517 360e3215f029
child 12911 704713ca07ea
permissions -rw-r--r--
nodups -> distinct
     1 (*  Title:      HOL/MicroJava/J/JBasis.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     Copyright   1999 TU Muenchen
     5 *)
     6 
     7 header "Some Auxiliary Definitions"
     8 
     9 theory JBasis = Main: 
    10 
    11 lemmas [simp] = Let_def
    12 
    13 section "unique"
    14  
    15 constdefs
    16   unique  :: "('a \<times> 'b) list => bool"
    17   "unique  == distinct \<circ> map fst"
    18 
    19 
    20 lemma fst_in_set_lemma [rule_format (no_asm)]: 
    21       "(x, y) : set xys --> x : fst ` set xys"
    22 apply (induct_tac "xys")
    23 apply  auto
    24 done
    25 
    26 lemma unique_Nil [simp]: "unique []"
    27 apply (unfold unique_def)
    28 apply (simp (no_asm))
    29 done
    30 
    31 lemma unique_Cons [simp]: "unique ((x,y)#l) = (unique l & (!y. (x,y) ~: set l))"
    32 apply (unfold unique_def)
    33 apply (auto dest: fst_in_set_lemma)
    34 done
    35 
    36 lemma unique_append [rule_format (no_asm)]: "unique l' ==> unique l --> 
    37  (!(x,y):set l. !(x',y'):set l'. x' ~= x) --> unique (l @ l')"
    38 apply (induct_tac "l")
    39 apply  (auto dest: fst_in_set_lemma)
    40 done
    41 
    42 lemma unique_map_inj [rule_format (no_asm)]: 
    43   "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)"
    44 apply (induct_tac "l")
    45 apply  (auto dest: fst_in_set_lemma simp add: inj_eq)
    46 done
    47 
    48 section "More about Maps"
    49 
    50 lemma map_of_SomeI [rule_format (no_asm)]: 
    51   "unique l --> (k, x) : set l --> map_of l k = Some x"
    52 apply (induct_tac "l")
    53 apply  auto
    54 done
    55 
    56 lemma Ball_set_table_: 
    57   "(\<forall>(x,y)\<in>set l. P x y) --> (\<forall>x. \<forall>y. map_of l x = Some y --> P x y)"
    58 apply(induct_tac "l")
    59 apply(simp_all (no_asm))
    60 apply safe
    61 apply auto
    62 done
    63 lemmas Ball_set_table = Ball_set_table_ [THEN mp];
    64 
    65 lemma table_of_remap_SomeD [rule_format (no_asm)]: 
    66 "map_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> 
    67  map_of t (k, k') = Some x"
    68 apply (induct_tac "t")
    69 apply  auto
    70 done
    71 
    72 end