# HG changeset patch # User nipkow # Date 1323936803 -3600 # Node ID 19ee710d9c14116d3ecceaa1fde540ab7a539fbb # Parent dadd139192d172426b0a04d57b99cd1a239d8a07 tuned diff -r dadd139192d1 -r 19ee710d9c14 src/HOL/IMP/Collecting.thy --- a/src/HOL/IMP/Collecting.thy Tue Dec 13 21:15:38 2011 +0100 +++ b/src/HOL/IMP/Collecting.thy Thu Dec 15 09:13:23 2011 +0100 @@ -15,13 +15,13 @@ begin fun less_eq_acom :: "('a::order)acom \ 'a acom \ bool" where -"less_eq_acom (SKIP {S}) (SKIP {S'}) = (S \ S')" | -"less_eq_acom (x ::= e {S}) (x' ::= e' {S'}) = (x=x' \ e=e' \ S \ S')" | -"less_eq_acom (c1;c2) (c1';c2') = (less_eq_acom c1 c1' \ less_eq_acom c2 c2')" | -"less_eq_acom (IF b THEN c1 ELSE c2 {S}) (IF b' THEN c1' ELSE c2' {S'}) = - (b=b' \ less_eq_acom c1 c1' \ less_eq_acom c2 c2' \ S \ S')" | -"less_eq_acom ({Inv} WHILE b DO c {P}) ({Inv'} WHILE b' DO c' {P'}) = - (b=b' \ less_eq_acom c c' \ Inv \ Inv' \ P \ P')" | +"(SKIP {S}) \ (SKIP {S'}) = (S \ S')" | +"(x ::= e {S}) \ (x' ::= e' {S'}) = (x=x' \ e=e' \ S \ S')" | +"(c1;c2) \ (c1';c2') = (c1 \ c1' \ c2 \ c2')" | +"(IF b THEN c1 ELSE c2 {S}) \ (IF b' THEN c1' ELSE c2' {S'}) = + (b=b' \ c1 \ c1' \ c2 \ c2' \ S \ S')" | +"({Inv} WHILE b DO c {P}) \ ({Inv'} WHILE b' DO c' {P'}) = + (b=b' \ c \ c' \ Inv \ Inv' \ P \ P')" | "less_eq_acom _ _ = False" lemma SKIP_le: "SKIP {S} \ c \ (\S'. c = SKIP {S'} \ S \ S')" diff -r dadd139192d1 -r 19ee710d9c14 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Dec 13 21:15:38 2011 +0100 +++ b/src/HOL/IsaMakefile Thu Dec 15 09:13:23 2011 +0100 @@ -520,8 +520,8 @@ IMP/Abs_Int_Den/Abs_State_den.thy IMP/Abs_Int_Den/Abs_Int_den0.thy \ IMP/Abs_Int_Den/Abs_Int_den0_const.thy IMP/Abs_Int_Den/Abs_Int_den1.thy \ IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy IMP/Abs_Int_Den/Abs_Int_den2.thy \ - IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy \ - IMP/Big_Step.thy IMP/C_like.thy IMP/Com.thy IMP/Compiler.thy \ + IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy IMP/Big_Step.thy IMP/C_like.thy \ + IMP/Collecting.thy IMP/Collecting1.thy IMP/Com.thy IMP/Compiler.thy \ IMP/Comp_Rev.thy IMP/Def_Ass.thy IMP/Def_Ass_Big.thy IMP/Def_Ass_Exp.thy \ IMP/Def_Ass_Small.thy IMP/Def_Ass_Sound_Big.thy \ IMP/Def_Ass_Sound_Small.thy IMP/Denotation.thy IMP/Hoare.thy \