minimized class dependency, updated references
authornipkow
Sun Jan 05 18:59:29 2014 +0100 (2014-01-05 ago)
changeset 54930f2ec28292479
parent 54929 f1ded3cea58d
child 54931 88cf06038e37
minimized class dependency, updated references
src/HOL/IMP/Abs_State.thy
src/HOL/IMP/document/root.bib
src/HOL/IMP/document/root.tex
     1.1 --- a/src/HOL/IMP/Abs_State.thy	Fri Jan 03 22:04:44 2014 +0100
     1.2 +++ b/src/HOL/IMP/Abs_State.thy	Sun Jan 05 18:59:29 2014 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  type_synonym 'a st_rep = "(vname * 'a) list"
     1.6  
     1.7 -fun fun_rep :: "('a::order_top) st_rep \<Rightarrow> vname \<Rightarrow> 'a" where
     1.8 +fun fun_rep :: "('a::top) st_rep \<Rightarrow> vname \<Rightarrow> 'a" where
     1.9  "fun_rep [] = (\<lambda>x. \<top>)" |
    1.10  "fun_rep ((x,a)#ps) = (fun_rep ps) (x := a)"
    1.11  
    1.12 @@ -14,23 +14,23 @@
    1.13    "fun_rep ps = (%x. case map_of ps x of None \<Rightarrow> \<top> | Some a \<Rightarrow> a)"
    1.14  by(induction ps rule: fun_rep.induct) auto
    1.15  
    1.16 -definition eq_st :: "('a::order_top) st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
    1.17 +definition eq_st :: "('a::top) st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
    1.18  "eq_st S1 S2 = (fun_rep S1 = fun_rep S2)"
    1.19  
    1.20  hide_type st  --"hide previous def to avoid long names"
    1.21  
    1.22 -quotient_type 'a st = "('a::order_top) st_rep" / eq_st
    1.23 +quotient_type 'a st = "('a::top) st_rep" / eq_st
    1.24  morphisms rep_st St
    1.25  by (metis eq_st_def equivpI reflpI sympI transpI)
    1.26  
    1.27 -lift_definition update :: "('a::order_top) st \<Rightarrow> vname \<Rightarrow> 'a \<Rightarrow> 'a st"
    1.28 +lift_definition update :: "('a::top) st \<Rightarrow> vname \<Rightarrow> 'a \<Rightarrow> 'a st"
    1.29    is "\<lambda>ps x a. (x,a)#ps"
    1.30  by(auto simp: eq_st_def)
    1.31  
    1.32 -lift_definition "fun" :: "('a::order_top) st \<Rightarrow> vname \<Rightarrow> 'a" is fun_rep
    1.33 +lift_definition "fun" :: "('a::top) st \<Rightarrow> vname \<Rightarrow> 'a" is fun_rep
    1.34  by(simp add: eq_st_def)
    1.35  
    1.36 -definition show_st :: "vname set \<Rightarrow> ('a::order_top) st \<Rightarrow> (vname * 'a)set" where
    1.37 +definition show_st :: "vname set \<Rightarrow> ('a::top) st \<Rightarrow> (vname * 'a)set" where
    1.38  "show_st X S = (\<lambda>x. (x, fun S x)) ` X"
    1.39  
    1.40  definition "show_acom C = map_acom (Option.map (show_st (vars(strip C)))) C"
    1.41 @@ -39,10 +39,10 @@
    1.42  lemma fun_update[simp]: "fun (update S x y) = (fun S)(x:=y)"
    1.43  by transfer auto
    1.44  
    1.45 -definition \<gamma>_st :: "(('a::order_top) \<Rightarrow> 'b set) \<Rightarrow> 'a st \<Rightarrow> (vname \<Rightarrow> 'b) set" where
    1.46 +definition \<gamma>_st :: "(('a::top) \<Rightarrow> 'b set) \<Rightarrow> 'a st \<Rightarrow> (vname \<Rightarrow> 'b) set" where
    1.47  "\<gamma>_st \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(fun F x)}"
    1.48  
    1.49 -instantiation st :: ("{order,order_top}") order
    1.50 +instantiation st :: (order_top) order
    1.51  begin
    1.52  
    1.53  definition less_eq_st_rep :: "'a st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
    1.54 @@ -83,7 +83,7 @@
    1.55  lemma le_st_iff: "(F \<le> G) = (\<forall>x. fun F x \<le> fun G x)"
    1.56  by transfer (rule less_eq_st_rep_iff)
    1.57  
    1.58 -fun map2_st_rep :: "('a::order_top \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep" where
    1.59 +fun map2_st_rep :: "('a::top \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep" where
    1.60  "map2_st_rep f [] ps2 = map (%(x,y). (x, f \<top> y)) ps2" |
    1.61  "map2_st_rep f ((x,y)#ps1) ps2 =
    1.62    (let y2 = fun_rep ps2 x
     2.1 --- a/src/HOL/IMP/document/root.bib	Fri Jan 03 22:04:44 2014 +0100
     2.2 +++ b/src/HOL/IMP/document/root.bib	Sun Jan 05 18:59:29 2014 +0100
     2.3 @@ -14,3 +14,7 @@
     2.4  {Foundations of Software Technology and Theoretical Computer Science},
     2.5  editor={V. Chandru and V. Vinay},
     2.6  publisher=Springer,series=LNCS,volume=1180,year=1996,pages={180--192}}
     2.7 +
     2.8 +@book{ConcreteSemantics,author={Tobias Nipkow and Gerwin Klein},
     2.9 +title={Concrete Semantics. A Proof Assistant Approach},publisher=Springer,
    2.10 +note={To appear}}
     3.1 --- a/src/HOL/IMP/document/root.tex	Fri Jan 03 22:04:44 2014 +0100
     3.2 +++ b/src/HOL/IMP/document/root.tex	Sun Jan 05 18:59:29 2014 +0100
     3.3 @@ -20,7 +20,7 @@
     3.4  \begin{document}
     3.5  
     3.6  \title{Concrete Semantics}
     3.7 -\author{TN \& GK}
     3.8 +\author{Tobias Nipkow \& Gerwin Klein}
     3.9  \maketitle
    3.10  
    3.11  \setcounter{tocdepth}{2}
    3.12 @@ -31,6 +31,7 @@
    3.13  \input{session}
    3.14  
    3.15  \nocite{Nipkow}
    3.16 +\nocite{ConcreteSemantics}
    3.17  
    3.18  \bibliographystyle{abbrv}
    3.19  \bibliography{root}