equal
deleted
inserted
replaced
7 begin |
7 begin |
8 |
8 |
9 text {* @{text "the_preced"} is also the same as @{text "preced"}, the only |
9 text {* @{text "the_preced"} is also the same as @{text "preced"}, the only |
10 difference is the order of arguemts. *} |
10 difference is the order of arguemts. *} |
11 definition "the_preced s th = preced th s" |
11 definition "the_preced s th = preced th s" |
|
12 |
|
13 lemma inj_the_preced: |
|
14 "inj_on (the_preced s) (threads s)" |
|
15 by (metis inj_onI preced_unique the_preced_def) |
12 |
16 |
13 text {* @{term "the_thread"} extracts thread out of RAG node. *} |
17 text {* @{term "the_thread"} extracts thread out of RAG node. *} |
14 fun the_thread :: "node \<Rightarrow> thread" where |
18 fun the_thread :: "node \<Rightarrow> thread" where |
15 "the_thread (Th th) = th" |
19 "the_thread (Th th) = th" |
16 |
20 |