equal
deleted
inserted
replaced
81 done |
81 done |
82 |
82 |
83 lemma subcls1_irrefl_lemma1: "ws_prog \<Longrightarrow> subcls1^-1 \<inter> subcls1^+ = {}" |
83 lemma subcls1_irrefl_lemma1: "ws_prog \<Longrightarrow> subcls1^-1 \<inter> subcls1^+ = {}" |
84 by (fast dest: subcls1D ws_progD) |
84 by (fast dest: subcls1D ws_progD) |
85 |
85 |
86 (* context (theory "Transitive_Closure") *) |
86 (* irrefl_tranclI in Transitive_Closure.thy is more general *) |
87 lemma irrefl_tranclI': "r^-1 Int r^+ = {} ==> !x. (x, x) ~: r^+" |
87 lemma irrefl_tranclI': "r^-1 Int r^+ = {} ==> !x. (x, x) ~: r^+" |
88 apply (rule allI) |
88 by(blast elim: tranclE dest: trancl_into_rtrancl) |
89 apply (erule irrefl_tranclI) |
89 |
90 done |
|
91 |
90 |
92 lemmas subcls1_irrefl_lemma2 = subcls1_irrefl_lemma1 [THEN irrefl_tranclI'] |
91 lemmas subcls1_irrefl_lemma2 = subcls1_irrefl_lemma1 [THEN irrefl_tranclI'] |
93 |
92 |
94 lemma subcls1_irrefl: "\<lbrakk>(x, y) \<in> subcls1; ws_prog\<rbrakk> \<Longrightarrow> x \<noteq> y" |
93 lemma subcls1_irrefl: "\<lbrakk>(x, y) \<in> subcls1; ws_prog\<rbrakk> \<Longrightarrow> x \<noteq> y" |
95 apply (rule irrefl_trancl_rD) |
94 apply (rule irrefl_trancl_rD) |