--- a/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy Thu Dec 31 12:37:16 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,129 +0,0 @@
-(* Title: HOL/HOLCF/IOA/meta_theory/RefMappings.thy
- Author: Olaf Müller
-*)
-
-section \<open>Refinement Mappings in HOLCF/IOA\<close>
-
-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\<leadsto>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 \<midarrow>a\<midarrow>C\<rightarrow> 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 \<midarrow>a\<midarrow>C\<rightarrow> t
- --> (if a:ext(C)
- then (f s) \<midarrow>a\<midarrow>A\<rightarrow> (f t)
- else (f s)=(f t))))"
-
-
-subsection "transitions and moves"
-
-
-lemma transition_is_ex: "s \<midarrow>a\<midarrow>A\<rightarrow> t ==> ? ex. move A ex s a t"
-apply (rule_tac x = " (a,t) \<leadsto>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 \<midarrow>a\<midarrow>A\<rightarrow> s') & (s' \<midarrow>a'\<midarrow>A\<rightarrow> s'') & (~a':ext A)
- ==> ? ex. move A ex s a s''"
-apply (rule_tac x = " (a,s') \<leadsto> (a',s'') \<leadsto>nil" in exI)
-apply (simp add: move_def)
-done
-
-
-lemma eii_transitions_are_ex: "(s1 \<midarrow>a1\<midarrow>A\<rightarrow> s2) & (s2 \<midarrow>a2\<midarrow>A\<rightarrow> s3) & (s3 \<midarrow>a3\<midarrow>A\<rightarrow> s4) &
- (~a2:ext A) & (~a3:ext A) ==>
- ? ex. move A ex s1 a1 s4"
-apply (rule_tac x = " (a1,s2) \<leadsto> (a2,s3) \<leadsto> (a3,s4) \<leadsto>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