This GitLab instance reached the end of its service life. It won't be possible to create new users or projects.

Please read the deprecation notice for more information concerning the deprecation timeline

Visit migration.git.tu-berlin.de (internal network only) to import your old projects to the new GitLab platform 📥

Transition_Systems.thy 5.19 KB
Newer Older
benkeks committed
1
subsection \<open>Labeled Transition Systems\<close>
2 3

theory Transition_Systems
benkeks committed
4
  imports Finite_Partial_Order
5 6 7 8
begin
  
locale lts =
fixes
benkeks committed
9 10
  trans :: \<open>'s \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool\<close>

11 12
begin

benkeks committed
13 14 15
abbreviation step_pred :: \<open>'s \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 's \<Rightarrow> bool\<close>
  where
  \<open>step_pred p af q \<equiv> \<exists> a. af a \<and> trans p a q\<close>
16 17

abbreviation step :: 
benkeks committed
18 19
  \<open>'s \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool\<close>
   ("_ \<longmapsto>_  _" [70, 70, 70] 80)
20
where
benkeks committed
21 22 23 24
  \<open>p \<longmapsto>a  q \<equiv> trans p a q\<close>
   
inductive steps :: \<open>'s \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 's \<Rightarrow> bool\<close>
     ("_ \<longmapsto>* _  _" [70, 70, 70] 80)
25
where
benkeks committed
26
  refl: \<open>p \<longmapsto>* A p\<close> | step: \<open>p \<longmapsto>* A q1 \<Longrightarrow> q1 \<longmapsto>a q \<Longrightarrow> A a \<Longrightarrow> (p \<longmapsto>* A q)\<close>
27 28 29

lemma steps_one_step: 
  assumes
benkeks committed
30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48
    \<open>p \<longmapsto>a p'\<close>
     \<open>A a\<close>
   shows
    \<open>p \<longmapsto>* A p'\<close> using steps.step[of p A p a p'] steps.refl[of p A] assms .

lemma steps_concat: 
  assumes
    \<open>p' \<longmapsto>* A p''\<close>
     \<open>p \<longmapsto>* A p'\<close>
   shows
    \<open>p \<longmapsto>* A p''\<close> using assms
proof (induct arbitrary: p)
  case (refl p'' A p')
  then show ?case by auto
next
  case (step p' A p'' a pp p)
  hence \<open>p \<longmapsto>* A  p''\<close> by simp
  show ?case using steps.step[OF `p \<longmapsto>* A  p''` step(3,4)] .
qed
49 50 51

lemma steps_left:
  assumes
benkeks committed
52 53 54 55 56 57
    \<open>p \<noteq> p'\<close>
     \<open>p \<longmapsto>* A p'\<close>
   shows
    \<open>\<exists>p'' a . p \<longmapsto>a p'' \<and> A a \<and> p'' \<longmapsto>* A p'\<close>
   using assms(1) 
  by (induct rule:steps.induct[OF assms(2)], blast, metis refl steps_concat steps_one_step) 
58 59 60
  
lemma steps_no_step:
  assumes
benkeks committed
61 62 63 64 65 66
    \<open>\<And> a p' . p \<longmapsto>a p' \<Longrightarrow> \<not>A a\<close>
     \<open>p \<noteq> p''\<close>
     \<open>p \<longmapsto>* A p''\<close>
   shows
    \<open>False\<close>
   using steps_left[OF assms(2,3)] assms(1) by blast
67 68 69
    
lemma steps_no_step_pos:
  assumes
benkeks committed
70 71 72 73 74
    \<open>\<And> a p' . p \<longmapsto>a p' \<Longrightarrow> \<not>A a\<close>
     \<open>p \<longmapsto>* A p'\<close>
   shows
    \<open>p = p'\<close>
   using assms steps_no_step by blast
75 76 77
    
lemma steps_loop:
  assumes
benkeks committed
78 79 80 81 82 83
    \<open>\<And> a p' . p \<longmapsto>a p' \<Longrightarrow> p = p'\<close>
     \<open>p \<noteq> p''\<close>
     \<open>p \<longmapsto>* A p''\<close>
   shows
    \<open>False\<close>
   using assms(3,1,2) by (induct, auto)
84
    
benkeks committed
85 86 87 88

corollary steps_transp:
  \<open>transp (\<lambda> p p'. p \<longmapsto>* A p')\<close>
   using steps_concat unfolding transp_def by blast
89 90 91
  
lemma steps_spec: 
  assumes
benkeks committed
92 93 94 95 96
    \<open>p \<longmapsto>* A' p'\<close>
     \<open>\<And> a . A' a \<Longrightarrow> A a\<close>
   shows
    \<open>p \<longmapsto>* A p'\<close> using assms(1,2)
proof induct
97 98 99 100
  case (refl p)
  show ?case using steps.refl .
next
  case (step p A' pp a pp')
benkeks committed
101
  hence \<open>p \<longmapsto>* A  pp\<close> by simp 
102 103 104
  then show ?case using step(3,4,5) steps.step by auto
qed

benkeks committed
105 106 107 108
interpretation preorder \<open>(\<lambda> p p'. p \<longmapsto>* A p')\<close> \<open>\<lambda> p p'. p \<longmapsto>* A p' \<and> \<not>(p' \<longmapsto>* A p)\<close>
  by (standard, simp, simp add: steps.refl, metis steps_concat)

text\<open>If one can reach only a finite portion of the graph following @{text \<open>\<longmapsto>* A\<close>},
109 110 111 112
  and all cycles are loops, then there must be nodes which are maximal wrt. \<open>\<longmapsto>* A\<close>.\<close>
lemma step_max_deadlock:
  fixes A q
  assumes
benkeks committed
113 114 115 116
    antiysmm: \<open>\<And> r1 r2. r1 \<longmapsto>* A r2 \<and> r2 \<longmapsto>* A r1 \<Longrightarrow> r1 = r2\<close> and
    finite: \<open>finite {q'. q \<longmapsto>* A q'}\<close> and
    no_max: \<open>\<forall> q'. q \<longmapsto>* A q' \<longrightarrow> (\<exists>q''. q' \<longmapsto>* A q'' \<and> q' \<noteq> q'')\<close>
   shows
117
    False
benkeks committed
118 119 120 121 122 123
proof -
  interpret order \<open>(\<lambda> p p'. p \<longmapsto>* A p')\<close> \<open>\<lambda> p p'. p \<longmapsto>* A p' \<and> \<not>(p' \<longmapsto>* A p)\<close>
    by (standard, simp add: assms(1))
  show ?thesis using local.finite_max assms local.order_trans mem_Collect_eq by metis
qed

benkeks committed
124
end \<comment>\<open>end of lts\<close>
125 126 127
  
lemma lts_impl_steps2:
  assumes
benkeks committed
128 129 130 131 132
    \<open>lts.steps step1 p1 ap p2\<close>
     \<open>\<And> p1 a p2 . step1 p1 a p2 \<and> P p1 a p2 \<Longrightarrow> step2 p1 a p2\<close>
     \<open>\<And> p1 a p2 . P p1 a p2\<close>
   shows
    \<open>lts.steps step2 p1 ap p2\<close>
133 134 135 136 137
proof (induct rule: lts.steps.induct[OF assms(1)])
  case (1 p af)
  show ?case using lts.steps.refl[of step2 p af] by blast
next
  case (2 p af q1 a q)
benkeks committed
138
  hence \<open>step2 q1 a q\<close> using assms(2,3) by blast
139 140 141 142 143
  thus ?case using lts.step[OF 2(2) _ 2(4)] by blast
qed 
  
lemma lts_impl_steps:
  assumes
benkeks committed
144 145 146 147 148
    \<open>lts.steps step1 p1 ap p2\<close>
     \<open>\<And> p1 a p2 . step1 p1 a p2 \<Longrightarrow> step2 p1 a p2\<close>
   shows
    \<open>lts.steps step2 p1 ap p2\<close>
   using assms lts_impl_steps2[OF assms] by auto 
149 150
  
end