# HG changeset patch
# User nipkow
# Date 1347793975 -7200
# Node ID 4f9585401f1a7a043b157b53d386512f632cebc6
# Parent  73fb17ed2e08c3a63ae814611431c402d84209c7
got rid of ad-hoc lift function

diff -r 73fb17ed2e08 -r 4f9585401f1a src/HOL/IMP/Collecting.thy
--- a/src/HOL/IMP/Collecting.thy	Sun Sep 16 11:50:03 2012 +0200
+++ b/src/HOL/IMP/Collecting.thy	Sun Sep 16 13:12:55 2012 +0200
@@ -82,24 +82,24 @@
 "anno\<^isub>2({I} WHILE b DO {P} C {Q}) = P"
 
 
-fun lift :: "('a set \<Rightarrow> 'b) \<Rightarrow> com \<Rightarrow> 'a acom set \<Rightarrow> 'b acom"
-where
-"lift F com.SKIP M = (SKIP {F (post ` M)})" |
-"lift F (x ::= a) M = (x ::= a {F (post ` M)})" |
-"lift F (c1;c2) M =
-  lift F c1 (sub\<^isub>1 ` M); lift F c2 (sub\<^isub>2 ` M)" |
-"lift F (IF b THEN c1 ELSE c2) M =
-  IF b THEN {F (anno\<^isub>1 ` M)} lift F c1 (sub\<^isub>1 ` M) ELSE {F (anno\<^isub>2 ` M)} lift F c2 (sub\<^isub>2 ` M)
-  {F (post ` M)}" |
-"lift F (WHILE b DO c) M =
- {F (anno\<^isub>1 ` M)}
- WHILE b DO {F (anno\<^isub>2 ` M)} lift F c (sub\<^isub>1 ` M)
- {F (post ` M)}"
+fun Union_acom :: "com \<Rightarrow> 'a acom set \<Rightarrow> 'a set acom" where
+"Union_acom com.SKIP M = (SKIP {post ` M})" |
+"Union_acom (x ::= a) M = (x ::= a {post ` M})" |
+"Union_acom (c1;c2) M =
+  Union_acom c1 (sub\<^isub>1 ` M); Union_acom c2 (sub\<^isub>2 ` M)" |
+"Union_acom (IF b THEN c1 ELSE c2) M =
+  IF b THEN {anno\<^isub>1 ` M} Union_acom c1 (sub\<^isub>1 ` M) ELSE {anno\<^isub>2 ` M} Union_acom c2 (sub\<^isub>2 ` M)
+  {post ` M}" |
+"Union_acom (WHILE b DO c) M =
+ {anno\<^isub>1 ` M}
+ WHILE b DO {anno\<^isub>2 ` M} Union_acom c (sub\<^isub>1 ` M)
+ {post ` M}"
 
-interpretation Complete_Lattice "{C. strip C = c}" "lift Inter c" for c
+interpretation
+  Complete_Lattice "{C. strip C = c}" "map_acom Inter o (Union_acom c)" for c
 proof
   case goal1
-  have "a:A \<Longrightarrow> lift Inter (strip a) A \<le> a"
+  have "a:A \<Longrightarrow> map_acom Inter (Union_acom (strip a) A) \<le> a"
   proof(induction a arbitrary: A)
     case Seq from Seq.prems show ?case by(force intro!: Seq.IH)
   next
@@ -124,7 +124,7 @@
   qed
 next
   case goal3
-  have "strip(lift Inter c A) = c"
+  have "strip(Union_acom c A) = c"
   proof(induction c arbitrary: A)
     case Seq from Seq.prems show ?case by (fastforce simp: strip_eq_Seq subset_iff intro!: Seq.IH)
   next