# HG changeset patch # User nipkow # Date 1325500430 -3600 # Node ID 4869f1389333a27df91e46e8537e26d6eb5069f3 # Parent b9d4ec0f79acacaca504a2d0d33ad89df1ab96a6 removed unnecessary lemmas diff -r b9d4ec0f79ac -r 4869f1389333 src/HOL/IMP/Collecting.thy --- a/src/HOL/IMP/Collecting.thy Mon Jan 02 10:51:28 2012 +0100 +++ b/src/HOL/IMP/Collecting.thy Mon Jan 02 11:33:50 2012 +0100 @@ -136,27 +136,6 @@ lemma le_post: "c \ d \ post c \ post d" by(induction c d rule: less_eq_acom.induct) auto -lemma le_strip: "c \ d \ strip c = strip d" -by(induction c d rule: less_eq_acom.induct) auto - -lemma le_SKIP_iff: "c \ SKIP {P'} \ (EX P. c = SKIP {P} \ P \ P')" -by (cases c) simp_all - -lemma le_Assign_iff: "c \ x::=e {P'} \ (EX P. c = x::=e {P} \ P \ P')" -by (cases c) simp_all - -lemma le_Semi_iff: "c \ d1;d2 \ (EX c1 c2. c = c1;c2 \ c1 \ d1 \ c2 \ d2)" -by (cases c) simp_all - -lemma le_If_iff: "c \ IF b THEN d1 ELSE d2 {P'} \ - (EX c1 c2 P. c = IF b THEN c1 ELSE c2 {P} \ c1 \ d1 \ c2 \ d2 \ P \ P')" -by (cases c) simp_all - -lemma le_While_iff: "c \ {I'} WHILE b DO d {P'} \ - (EX I c' P. c = {I} WHILE b DO c' {P} \ I \ I' \ c' \ d \ P \ P')" -by (cases c) auto - - subsubsection "Collecting semantics" fun step :: "state set \ state set acom \ state set acom" where