diff -r 6c12f5e24e34 -r 0437dbc127b3 src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy	Sat Nov 27 16:08:10 2010 -0800
@@ -0,0 +1,129 @@
+(*  Title:      HOLCF/IOA/meta_theory/RefMappings.thy
+    Author:     Olaf Müller
+*)
+
+header {* Refinement Mappings in HOLCF/IOA *}
+
+theory RefMappings
+imports Traces
+begin
+
+default_sort type
+
+definition
+  move :: "[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool" where
+  "move ioa ex s a t =
+    (is_exec_frag ioa (s,ex) &  Finite ex &
+     laststate (s,ex)=t  &
+     mk_trace ioa$ex = (if a:ext(ioa) then a>>nil else nil))"
+
+definition
+  is_ref_map :: "[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where
+  "is_ref_map f C A =
+   ((!s:starts_of(C). f(s):starts_of(A)) &
+   (!s t a. reachable C s &
+            s -a--C-> t
+            --> (? ex. move A ex (f s) a (f t))))"
+
+definition
+  is_weak_ref_map :: "[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where
+  "is_weak_ref_map f C A =
+   ((!s:starts_of(C). f(s):starts_of(A)) &
+   (!s t a. reachable C s &
+            s -a--C-> t
+            --> (if a:ext(C)
+                 then (f s) -a--A-> (f t)
+                 else (f s)=(f t))))"
+
+
+subsection "transitions and moves"
+
+
+lemma transition_is_ex: "s -a--A-> t ==> ? ex. move A ex s a t"
+apply (rule_tac x = " (a,t) >>nil" in exI)
+apply (simp add: move_def)
+done
+
+
+lemma nothing_is_ex: "(~a:ext A) & s=t ==> ? ex. move A ex s a t"
+apply (rule_tac x = "nil" in exI)
+apply (simp add: move_def)
+done
+
+
+lemma ei_transitions_are_ex: "(s -a--A-> s') & (s' -a'--A-> s'') & (~a':ext A)  
+         ==> ? ex. move A ex s a s''"
+apply (rule_tac x = " (a,s') >> (a',s'') >>nil" in exI)
+apply (simp add: move_def)
+done
+
+
+lemma eii_transitions_are_ex: "(s1 -a1--A-> s2) & (s2 -a2--A-> s3) & (s3 -a3--A-> s4) & 
+      (~a2:ext A) & (~a3:ext A) ==>  
+      ? ex. move A ex s1 a1 s4"
+apply (rule_tac x = " (a1,s2) >> (a2,s3) >> (a3,s4) >>nil" in exI)
+apply (simp add: move_def)
+done
+
+
+subsection "weak_ref_map and ref_map"
+
+lemma weak_ref_map2ref_map:
+  "[| ext C = ext A;  
+     is_weak_ref_map f C A |] ==> is_ref_map f C A"
+apply (unfold is_weak_ref_map_def is_ref_map_def)
+apply auto
+apply (case_tac "a:ext A")
+apply (auto intro: transition_is_ex nothing_is_ex)
+done
+
+
+lemma imp_conj_lemma: "(P ==> Q-->R) ==> P&Q --> R"
+  by blast
+
+declare split_if [split del]
+declare if_weak_cong [cong del]
+
+lemma rename_through_pmap: "[| is_weak_ref_map f C A |]  
+      ==> (is_weak_ref_map f (rename C g) (rename A g))"
+apply (simp add: is_weak_ref_map_def)
+apply (rule conjI)
+(* 1: start states *)
+apply (simp add: rename_def rename_set_def starts_of_def)
+(* 2: reachable transitions *)
+apply (rule allI)+
+apply (rule imp_conj_lemma)
+apply (simp (no_asm) add: rename_def rename_set_def)
+apply (simp add: externals_def asig_inputs_def asig_outputs_def asig_of_def trans_of_def)
+apply safe
+apply (simplesubst split_if)
+ apply (rule conjI)
+ apply (rule impI)
+ apply (erule disjE)
+ apply (erule exE)
+apply (erule conjE)
+(* x is input *)
+ apply (drule sym)
+ apply (drule sym)
+apply simp
+apply hypsubst+
+apply (frule reachable_rename)
+apply simp
+(* x is output *)
+ apply (erule exE)
+apply (erule conjE)
+ apply (drule sym)
+ apply (drule sym)
+apply simp
+apply hypsubst+
+apply (frule reachable_rename)
+apply simp
+(* x is internal *)
+apply (frule reachable_rename)
+apply auto
+done
+
+declare split_if [split]
+declare if_weak_cong [cong]
+
+end