Theory JBasis

Up to index of Isabelle/HOL/exceptions

(*  Title:      HOL/MicroJava/J/JBasis.thy
    ID:         $Id: JBasis.html,v 1.1 2002/11/28 13:16:31 kleing Exp $
    Author:     David von Oheimb
    Copyright   1999 TU Muenchen
*)

header {* 
  \chapter{Program Structure and Declarations}\label{cha:j}
  \isaheader{Some Auxiliary Definitions}
*}

theory JBasis = Main: 

lemmas [simp] = Let_def

section "unique"
 
constdefs
  unique  :: "('a × 'b) list => bool"
  "unique  == distinct \<circ> map fst"


lemma fst_in_set_lemma [rule_format (no_asm)]: 
      "(x, y) : set xys --> x : fst ` set xys"
apply (induct_tac "xys")
apply  auto
done

lemma unique_Nil [simp]: "unique []"
apply (unfold unique_def)
apply (simp (no_asm))
done

lemma unique_Cons [simp]: "unique ((x,y)#l) = (unique l & (!y. (x,y) ~: set l))"
apply (unfold unique_def)
apply (auto dest: fst_in_set_lemma)
done

lemma unique_append [rule_format (no_asm)]: "unique l' ==> unique l --> 
 (!(x,y):set l. !(x',y'):set l'. x' ~= x) --> unique (l @ l')"
apply (induct_tac "l")
apply  (auto dest: fst_in_set_lemma)
done

lemma unique_map_inj [rule_format (no_asm)]: 
  "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)"
apply (induct_tac "l")
apply  (auto dest: fst_in_set_lemma simp add: inj_eq)
done

section "More about Maps"

lemma map_of_SomeI [rule_format (no_asm)]: 
  "unique l --> (k, x) : set l --> map_of l k = Some x"
apply (induct_tac "l")
apply  auto
done

lemma Ball_set_table_: 
  "(\<forall>(x,y)\<in>set l. P x y) --> (\<forall>x. \<forall>y. map_of l x = Some y --> P x y)"
apply(induct_tac "l")
apply(simp_all (no_asm))
apply safe
apply auto
done
lemmas Ball_set_table = Ball_set_table_ [THEN mp];

lemma table_of_remap_SomeD [rule_format (no_asm)]: 
"map_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> 
 map_of t (k, k') = Some x"
apply (induct_tac "t")
apply  auto
done

end

lemmas

  Let s f == f s

unique

lemma fst_in_set_lemma:

  (x, y) : set xys ==> x : fst ` set xys

lemma unique_Nil:

  unique []

lemma unique_Cons:

  unique ((x, y) # l) = (unique l & (ALL y. (x, y) ~: set l))

lemma unique_append:

  [| unique l'; unique l; ALL (x, y):set l. ALL (x', y'):set l'. x' ~= x |]
  ==> unique (l @ l')

lemma unique_map_inj:

  [| unique l; inj f |] ==> unique (map (%(k, x). (f k, g k x)) l)

More about Maps

lemma map_of_SomeI:

  [| unique l; (k, x) : set l |] ==> map_of l k = Some x

lemma Ball_set_table_:

  Ball (set l) (split P) --> (ALL x y. map_of l x = Some y --> P x y)

lemmas Ball_set_table:

  Ball (set l_1) (split P_1) ==> ALL x y. map_of l_1 x = Some y --> P_1 x y

lemma table_of_remap_SomeD:

  map_of (map (%((k, k'), x). (k, k', x)) t) k = Some (k', x)
  ==> map_of t (k, k') = Some x