# HG changeset patch
# User nipkow
# Date 1388944769 -3600
# Node ID f2ec2829247960143f4fa5d68817de14110d6a0e
# Parent  f1ded3cea58de780d4353bb5c446423038c24cf0
minimized class dependency, updated references

diff -r f1ded3cea58d -r f2ec28292479 src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Fri Jan 03 22:04:44 2014 +0100
+++ b/src/HOL/IMP/Abs_State.thy	Sun Jan 05 18:59:29 2014 +0100
@@ -6,7 +6,7 @@
 
 type_synonym 'a st_rep = "(vname * 'a) list"
 
-fun fun_rep :: "('a::order_top) st_rep \<Rightarrow> vname \<Rightarrow> 'a" where
+fun fun_rep :: "('a::top) st_rep \<Rightarrow> vname \<Rightarrow> 'a" where
 "fun_rep [] = (\<lambda>x. \<top>)" |
 "fun_rep ((x,a)#ps) = (fun_rep ps) (x := a)"
 
@@ -14,23 +14,23 @@
   "fun_rep ps = (%x. case map_of ps x of None \<Rightarrow> \<top> | Some a \<Rightarrow> a)"
 by(induction ps rule: fun_rep.induct) auto
 
-definition eq_st :: "('a::order_top) st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
+definition eq_st :: "('a::top) st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
 "eq_st S1 S2 = (fun_rep S1 = fun_rep S2)"
 
 hide_type st  --"hide previous def to avoid long names"
 
-quotient_type 'a st = "('a::order_top) st_rep" / eq_st
+quotient_type 'a st = "('a::top) st_rep" / eq_st
 morphisms rep_st St
 by (metis eq_st_def equivpI reflpI sympI transpI)
 
-lift_definition update :: "('a::order_top) st \<Rightarrow> vname \<Rightarrow> 'a \<Rightarrow> 'a st"
+lift_definition update :: "('a::top) st \<Rightarrow> vname \<Rightarrow> 'a \<Rightarrow> 'a st"
   is "\<lambda>ps x a. (x,a)#ps"
 by(auto simp: eq_st_def)
 
-lift_definition "fun" :: "('a::order_top) st \<Rightarrow> vname \<Rightarrow> 'a" is fun_rep
+lift_definition "fun" :: "('a::top) st \<Rightarrow> vname \<Rightarrow> 'a" is fun_rep
 by(simp add: eq_st_def)
 
-definition show_st :: "vname set \<Rightarrow> ('a::order_top) st \<Rightarrow> (vname * 'a)set" where
+definition show_st :: "vname set \<Rightarrow> ('a::top) st \<Rightarrow> (vname * 'a)set" where
 "show_st X S = (\<lambda>x. (x, fun S x)) ` X"
 
 definition "show_acom C = map_acom (Option.map (show_st (vars(strip C)))) C"
@@ -39,10 +39,10 @@
 lemma fun_update[simp]: "fun (update S x y) = (fun S)(x:=y)"
 by transfer auto
 
-definition \<gamma>_st :: "(('a::order_top) \<Rightarrow> 'b set) \<Rightarrow> 'a st \<Rightarrow> (vname \<Rightarrow> 'b) set" where
+definition \<gamma>_st :: "(('a::top) \<Rightarrow> 'b set) \<Rightarrow> 'a st \<Rightarrow> (vname \<Rightarrow> 'b) set" where
 "\<gamma>_st \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(fun F x)}"
 
-instantiation st :: ("{order,order_top}") order
+instantiation st :: (order_top) order
 begin
 
 definition less_eq_st_rep :: "'a st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
@@ -83,7 +83,7 @@
 lemma le_st_iff: "(F \<le> G) = (\<forall>x. fun F x \<le> fun G x)"
 by transfer (rule less_eq_st_rep_iff)
 
-fun map2_st_rep :: "('a::order_top \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep" where
+fun map2_st_rep :: "('a::top \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep" where
 "map2_st_rep f [] ps2 = map (%(x,y). (x, f \<top> y)) ps2" |
 "map2_st_rep f ((x,y)#ps1) ps2 =
   (let y2 = fun_rep ps2 x
diff -r f1ded3cea58d -r f2ec28292479 src/HOL/IMP/document/root.bib
--- a/src/HOL/IMP/document/root.bib	Fri Jan 03 22:04:44 2014 +0100
+++ b/src/HOL/IMP/document/root.bib	Sun Jan 05 18:59:29 2014 +0100
@@ -14,3 +14,7 @@
 {Foundations of Software Technology and Theoretical Computer Science},
 editor={V. Chandru and V. Vinay},
 publisher=Springer,series=LNCS,volume=1180,year=1996,pages={180--192}}
+
+@book{ConcreteSemantics,author={Tobias Nipkow and Gerwin Klein},
+title={Concrete Semantics. A Proof Assistant Approach},publisher=Springer,
+note={To appear}}
diff -r f1ded3cea58d -r f2ec28292479 src/HOL/IMP/document/root.tex
--- a/src/HOL/IMP/document/root.tex	Fri Jan 03 22:04:44 2014 +0100
+++ b/src/HOL/IMP/document/root.tex	Sun Jan 05 18:59:29 2014 +0100
@@ -20,7 +20,7 @@
 \begin{document}
 
 \title{Concrete Semantics}
-\author{TN \& GK}
+\author{Tobias Nipkow \& Gerwin Klein}
 \maketitle
 
 \setcounter{tocdepth}{2}
@@ -31,6 +31,7 @@
 \input{session}
 
 \nocite{Nipkow}
+\nocite{ConcreteSemantics}
 
 \bibliographystyle{abbrv}
 \bibliography{root}