58 subsection "Non-repeating paths" |
58 subsection "Non-repeating paths" |
59 |
59 |
60 definition distPath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool" |
60 definition distPath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool" |
61 where "distPath h x as y \<longleftrightarrow> Path h x as y \<and> distinct as" |
61 where "distPath h x as y \<longleftrightarrow> Path h x as y \<and> distinct as" |
62 |
62 |
63 text{* The term @{term"distPath h x as y"} expresses the fact that a |
63 text\<open>The term @{term"distPath h x as y"} expresses the fact that a |
64 non-repeating path @{term as} connects location @{term x} to location |
64 non-repeating path @{term as} connects location @{term x} to location |
65 @{term y} by means of the @{term h} field. In the case where @{text "x |
65 @{term y} by means of the @{term h} field. In the case where \<open>x |
66 = y"}, and there is a cycle from @{term x} to itself, @{term as} can |
66 = y\<close>, and there is a cycle from @{term x} to itself, @{term as} can |
67 be both @{term "[]"} and the non-repeating list of nodes in the |
67 be both @{term "[]"} and the non-repeating list of nodes in the |
68 cycle. *} |
68 cycle.\<close> |
69 |
69 |
70 lemma neq_dP: "p \<noteq> q \<Longrightarrow> Path h p Ps q \<Longrightarrow> distinct Ps \<Longrightarrow> |
70 lemma neq_dP: "p \<noteq> q \<Longrightarrow> Path h p Ps q \<Longrightarrow> distinct Ps \<Longrightarrow> |
71 EX a Qs. p = Ref a & Ps = a#Qs & a \<notin> set Qs" |
71 EX a Qs. p = Ref a & Ps = a#Qs & a \<notin> set Qs" |
72 by (case_tac Ps, auto) |
72 by (case_tac Ps, auto) |
73 |
73 |