equal
deleted
inserted
replaced
62 apply auto |
62 apply auto |
63 apply blast |
63 apply blast |
64 apply (blast intro: append_eq_appendI) |
64 apply (blast intro: append_eq_appendI) |
65 done |
65 done |
66 |
66 |
67 lemma Cons_step1E [rulified, elim!]: |
67 lemma Cons_step1E [rule_format, elim!]: |
68 "[| (ys, x # xs) \<in> step1 r; |
68 "[| (ys, x # xs) \<in> step1 r; |
69 \<forall>y. ys = y # xs --> (y, x) \<in> r --> R; |
69 \<forall>y. ys = y # xs --> (y, x) \<in> r --> R; |
70 \<forall>zs. ys = x # zs --> (zs, xs) \<in> step1 r --> R |
70 \<forall>zs. ys = x # zs --> (zs, xs) \<in> step1 r --> R |
71 |] ==> R" |
71 |] ==> R" |
72 apply (case_tac ys) |
72 apply (case_tac ys) |
85 apply force |
85 apply force |
86 apply simp |
86 apply simp |
87 apply blast |
87 apply blast |
88 done |
88 done |
89 |
89 |
90 lemma Cons_acc_step1I [rulified, intro!]: |
90 lemma Cons_acc_step1I [rule_format, intro!]: |
91 "x \<in> acc r ==> \<forall>xs. xs \<in> acc (step1 r) --> x # xs \<in> acc (step1 r)" |
91 "x \<in> acc r ==> \<forall>xs. xs \<in> acc (step1 r) --> x # xs \<in> acc (step1 r)" |
92 apply (erule acc_induct) |
92 apply (erule acc_induct) |
93 apply (erule thin_rl) |
93 apply (erule thin_rl) |
94 apply clarify |
94 apply clarify |
95 apply (erule acc_induct) |
95 apply (erule acc_induct) |