equal
deleted
inserted
replaced
126 |
126 |
127 lemma trcl_step: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z" |
127 lemma trcl_step: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z" |
128 apply (unfold trcl_def) |
128 apply (unfold trcl_def) |
129 apply (rule allI impI)+ |
129 apply (rule allI impI)+ |
130 proof - |
130 proof - |
131 case goal1 |
131 case (goal1 P) |
132 show ?case |
132 have g1: "R x y" by fact |
133 apply (rule goal1(4) [rule_format]) |
133 have g2: "\<forall>P. (\<forall>x. P x x) \<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P y z" by fact |
134 apply (rule goal1(1)) |
134 have g3: "\<forall>x. P x x" by fact |
135 apply (rule goal1(2) [THEN spec [where x=P], THEN mp, THEN mp, |
135 have g4: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact |
136 OF goal1(3-4)]) |
136 show ?case |
|
137 apply (rule g4 [rule_format]) |
|
138 apply (rule g1) |
|
139 apply (rule g2 [THEN spec [where x=P], THEN mp, THEN mp, OF g3, OF g4]) |
137 done |
140 done |
138 qed |
141 qed |
139 |
142 |
140 text {* |
143 text {* |
141 |
144 |