Theory AssocLists

(*File: AssocLists.thy
  Author: L Beringer & M Hofmann, LMU Munich
  Date: 05/12/2008
  Purpose: Representation of partial maps by association lists         
*)
(*<*)
theory AssocLists imports Main begin
(*>*)

section‹Preliminaries: association lists \label{sec:preliminaries}›

text‹Finite maps are used frequently, both in the representation of
syntax and in the program logics. Instead of restricting Isabelle's
partial map type $\alpha \rightharpoonup \beta$ to finite domains, we
found it easier for the present development to use the following adhoc
data type of association lists.›

type_synonym ('a,'b) AssList = "('a × 'b) list"

primrec lookup::"('a, 'b) AssList  'a  ('b option)" ("__" [90,0] 90)
where
"lookup [] l = None" |
"lookup (h # t) l = (if fst h = l then Some(snd h) else lookup t l)"

(*<*)
lemma AL_lookup1[rule_format]:" a b . (La = Some b)  ((a,b)  set L)"
by (induct L, simp_all)(* add: set_mem_eq)*)

lemma AL_Triv1:"a=b  La = Lb" by simp

lemma AL_Triv2: "La = X; La = Y  X=Y" by simp

lemma AL_Triv3:"L=M ; Mb = X  Lb = X" by clarsimp

lemma AL_Triv4:"L=M ; Lb = X  Mb = X" by clarsimp
(*>*)

text‹The statement following the type declaration of lookup›
indicates that we may use the infix notation L↓a› for the
lookup operation, and asserts some precedence for bracketing. In a
similar way, shorthands are introduced for various operations
throughout this document.›

primrec delete::"('a, 'b) AssList  'a  ('a, 'b) AssList"
where
"delete [] a = []" |
"delete (h # t) a = (if (fst h) = a then delete t a else (h # (delete t a)))"

(*<*)
lemma AL_delete1: "(delete L a)  a = None"
by (induct L, auto)

lemma AL_delete2[rule_format]:"b  a  (delete l a)b = lb"
by (induct l, simp, simp)

lemma AL_delete3: "La = None  delete L a = L"
apply (induct L)
apply simp
apply clarsimp
apply (subgoal_tac "La = None", clarsimp)
apply (case_tac "aa=a", clarsimp) apply clarsimp
done

lemma AL_delete4[simp]: "length(delete t a) < Suc(length t)"
by (induct t, simp+) 

lemma AL_delete5[rule_format]:"[|b  a; lb = x|] ==> (delete l a)b = x"
by (drule_tac l=l in AL_delete2, simp)

lemma AL_delete_idempotent: "delete M x = delete (delete M x) x"
by (induct M, auto)

lemma AL_delete_commutative: "delete (delete M c) x = delete (delete M x) c"
apply (induct M)
apply simp
apply simp
done
(*>*)

definition upd::"('a, 'b) AssList  'a  'b  ('a, 'b) AssList"
         ("_[__]" [1000,0,0] 1000)
where "upd L a b = (a,b) # (delete L a)"
(*<*)
lemma AL_update1: "(L::('a, 'b) AssList)[ab]a = Some b"
by (simp add: upd_def)

lemma AL_update1a: "a=c  (L::('a, 'b) AssList)[ab]c = Some b" by (simp add: AL_update1)

lemma AL_update2: "a  b  (L::('a, 'b) AssList)[av]b = Lb"
by (induct L, simp_all add: upd_def)

lemma AL_update3: "(L::('a, 'b) AssList)[av]b = X; a  b  Lb=X"
by (subgoal_tac "(L::('a, 'b) AssList)[av]b = Lb", clarsimp,erule AL_update2) 

lemma AL_update4:" (L::('a, 'b) AssList)b = Some X; a  b L[av]b = Some X"
by (subgoal_tac "(L::('a, 'b) AssList)[av]b = Lb", clarsimp, erule AL_update2)

lemma AL_update5: "(L::('a, 'b) AssList)b = M; a  b  L[aX]b = M"
apply (subgoal_tac "(L::('a, 'b) AssList)[aX]b = Lb", simp)
apply (erule AL_update2)
done
(*>*)

text‹The empty map is represented by the empty list.›

definition emp::"('a, 'b)AssList"
where "emp = []"
(*<*)
lemma AL_emp1: "empa = None"
by (simp add: emp_def)

definition AL_isEmp::"('a,'b) AssList  bool"
where "AL_isEmp l = ( a . la = None)"
(*>*)

definition contained::"('a,'b) AssList  ('a,'b) AssList  bool"
where "contained L M = ( a b . La = Some b  Ma = Some b)"

text‹The following operation defined the cardinality of a map.›

fun AL_Size :: "('a, 'b) AssList  nat"  ("|_|" [1000] 1000) where
  "AL_Size [] = 0"
| "AL_Size (h # t) = Suc (AL_Size (delete t (fst h)))"

(*<*)
lemma AL_Size_Zero: "|L| = 0  None = La"
by (induct L, simp, simp)

lemma AL_Size_Suc: " n . |L| = Suc n  ( a b . La = Some b)"
apply (induct L)
apply clarsimp 
apply clarsimp
apply (rule_tac x=a in exI, simp)
done

lemma AL_Size_UpdateSuc:"La = None  |L[ab]| = Suc |L|"
apply (induct L)
apply (simp add: upd_def)
apply (simp add: upd_def)
apply clarsimp
apply (case_tac "aa=a", clarsimp) 
apply clarsimp
apply (drule AL_delete3) apply clarsimp
done

lemma AL_Size_SucSplit[rule_format]:
" n . |L| = Suc n  
  ( a b M . |M| = n  Ma = None  La = Some b  ( c . c a  Mc = Lc))"
apply (induct L)
apply clarsimp
apply clarsimp
apply (rule_tac x=a in exI)  apply simp
apply (rule_tac x="delete L a" in exI, clarsimp)
  apply rule  apply (rule AL_delete1)
apply clarsimp apply (erule AL_delete2)
done

lemma updSizeAux[rule_format]: 
" h a obj obj1 . |h[aobj1]| = n  ha = Some obj  |h| = n"
apply (induct n)
apply clarsimp
  apply (drule_tac a=a in AL_Size_Zero) apply (simp add: AL_update1)
apply clarify
  apply (case_tac h, clarify) apply (erule thin_rl) apply (simp add: AL_emp1)
  apply clarify
  apply (case_tac "aa=a", clarify) apply (erule thin_rl) apply (simp add: upd_def)
    apply (subgoal_tac "(delete list a) = (delete (delete list a) a)", simp) 
    apply (rule AL_delete_idempotent)
  apply (erule_tac x="delete list aa" in allE, erule_tac x=a in allE)
  apply (erule_tac x=obj in allE, erule_tac x=obj1 in allE)
  apply (erule impE) apply (simp add: upd_def)
    apply (subgoal_tac "(delete (delete (delete list aa) a) a) = (delete (delete (delete list a) a) aa)", simp)
    apply (subgoal_tac "(delete (delete list a) a) = (delete list a)", simp)
      apply (subgoal_tac "delete (delete (delete list aa) a) a = delete (delete list aa) a", simp)
        apply (rule AL_delete_commutative)
      apply (subgoal_tac "delete (delete list aa) a = delete (delete (delete list aa) a) a", simp)
      apply (rule AL_delete_idempotent)
    apply (subgoal_tac "delete list a = delete (delete list a) a", simp)
    apply (rule AL_delete_idempotent)
  apply (erule impE) apply (simp add: upd_def) apply (rule AL_delete5) apply fast apply assumption
  apply simp
done

lemma updSize: "ha = Some obj  |h[aobj1]| = |h|"
by (insert updSizeAux [of h a obj1 "|h[aobj1]|" obj], simp)
(*>*)

text‹Some obvious basic properties of association lists and their
operations are easily proven, but have been suppressed
during the document preparation.›

(*<*)
end
(*>*)