45 apply (erule beta.induct) |
45 apply (erule beta.induct) |
46 apply (clarify del: disjCI) |
46 apply (clarify del: disjCI) |
47 apply (case_tac r) |
47 apply (case_tac r) |
48 apply simp |
48 apply simp |
49 apply (simp add: App_eq_foldl_conv) |
49 apply (simp add: App_eq_foldl_conv) |
50 apply (split (asm) split_if_asm) |
50 apply (split split_if_asm) |
51 apply simp |
51 apply simp |
52 apply blast |
52 apply blast |
53 apply simp |
53 apply simp |
54 apply (simp add: App_eq_foldl_conv) |
54 apply (simp add: App_eq_foldl_conv) |
55 apply (split (asm) split_if_asm) |
55 apply (split split_if_asm) |
56 apply simp |
56 apply simp |
57 apply simp |
57 apply simp |
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 (asm) 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 (asm) 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 (auto 0 3 intro: disjI2 [THEN append_step1I]) |
70 done |
70 done |
71 |
71 |