equal
deleted
inserted
replaced
64 done |
64 done |
65 |
65 |
66 lemma imp_conj_lemma: "(P \<Longrightarrow> Q \<longrightarrow> R) \<Longrightarrow> P \<and> Q \<longrightarrow> R" |
66 lemma imp_conj_lemma: "(P \<Longrightarrow> Q \<longrightarrow> R) \<Longrightarrow> P \<and> Q \<longrightarrow> R" |
67 by blast |
67 by blast |
68 |
68 |
69 declare split_if [split del] |
69 declare if_split [split del] |
70 declare if_weak_cong [cong del] |
70 declare if_weak_cong [cong del] |
71 |
71 |
72 lemma rename_through_pmap: |
72 lemma rename_through_pmap: |
73 "is_weak_ref_map f C A \<Longrightarrow> is_weak_ref_map f (rename C g) (rename A g)" |
73 "is_weak_ref_map f C A \<Longrightarrow> is_weak_ref_map f (rename C g) (rename A g)" |
74 apply (simp add: is_weak_ref_map_def) |
74 apply (simp add: is_weak_ref_map_def) |
79 apply (rule allI)+ |
79 apply (rule allI)+ |
80 apply (rule imp_conj_lemma) |
80 apply (rule imp_conj_lemma) |
81 apply (simp (no_asm) add: rename_def rename_set_def) |
81 apply (simp (no_asm) add: rename_def rename_set_def) |
82 apply (simp add: externals_def asig_inputs_def asig_outputs_def asig_of_def trans_of_def) |
82 apply (simp add: externals_def asig_inputs_def asig_outputs_def asig_of_def trans_of_def) |
83 apply safe |
83 apply safe |
84 apply (simplesubst split_if) |
84 apply (simplesubst if_split) |
85 apply (rule conjI) |
85 apply (rule conjI) |
86 apply (rule impI) |
86 apply (rule impI) |
87 apply (erule disjE) |
87 apply (erule disjE) |
88 apply (erule exE) |
88 apply (erule exE) |
89 apply (erule conjE) |
89 apply (erule conjE) |
106 text \<open>\<open>x\<close> is internal\<close> |
106 text \<open>\<open>x\<close> is internal\<close> |
107 apply (frule reachable_rename) |
107 apply (frule reachable_rename) |
108 apply auto |
108 apply auto |
109 done |
109 done |
110 |
110 |
111 declare split_if [split] |
111 declare if_split [split] |
112 declare if_weak_cong [cong] |
112 declare if_weak_cong [cong] |
113 |
113 |
114 end |
114 end |