equal
deleted
inserted
replaced
58 apply (clarify del: disjCI) |
58 apply (clarify del: disjCI) |
59 apply (drule App_eq_foldl_conv [THEN iffD1]) |
59 apply (drule App_eq_foldl_conv [THEN iffD1]) |
60 apply (split split_if_asm) |
60 apply (split split_if_asm) |
61 apply simp |
61 apply simp |
62 apply blast |
62 apply blast |
63 apply (force intro: disjI1 [THEN append_step1I]) |
63 apply (force intro!: disjI1 [THEN append_step1I]) |
64 apply (clarify del: disjCI) |
64 apply (clarify del: disjCI) |
65 apply (drule App_eq_foldl_conv [THEN iffD1]) |
65 apply (drule App_eq_foldl_conv [THEN iffD1]) |
66 apply (split split_if_asm) |
66 apply (split split_if_asm) |
67 apply simp |
67 apply simp |
68 apply blast |
68 apply blast |
69 apply (auto 0 3 intro: disjI2 [THEN append_step1I]) |
69 apply (clarify, auto 0 3 intro!: exI intro: append_step1I) |
70 done |
70 done |
71 |
71 |
72 lemma apps_betasE [elim!]: |
72 lemma apps_betasE [elim!]: |
73 "[| r $$ rs -> s; !!r'. [| r -> r'; s = r' $$ rs |] ==> R; |
73 "[| r $$ rs -> s; !!r'. [| r -> r'; s = r' $$ rs |] ==> R; |
74 !!rs'. [| rs => rs'; s = r $$ rs' |] ==> R; |
74 !!rs'. [| rs => rs'; s = r $$ rs' |] ==> R; |