equal
deleted
inserted
replaced
61 assumes "l:Lists(A)" |
61 assumes "l:Lists(A)" |
62 and "m:Lists(A)" |
62 and "m:Lists(A)" |
63 shows "map(f,l@m) = map(f,l) @ map(f,m)" |
63 shows "map(f,l@m) = map(f,l) @ map(f,m)" |
64 apply (tactic {* eq_coinduct3_tac @{context} |
64 apply (tactic {* eq_coinduct3_tac @{context} |
65 "{p. EX x y. p=<x,y> & (EX l:Lists (A). EX m:Lists (A). x=map (f,l@m) & y=map (f,l) @ map (f,m))}" 1 *}) |
65 "{p. EX x y. p=<x,y> & (EX l:Lists (A). EX m:Lists (A). x=map (f,l@m) & y=map (f,l) @ map (f,m))}" 1 *}) |
66 apply (blast intro: prems) |
66 apply (blast intro: assms) |
67 apply safe |
67 apply safe |
68 apply (drule ListsXH [THEN iffD1]) |
68 apply (drule ListsXH [THEN iffD1]) |
69 apply (tactic "EQgen_tac @{context} [] 1") |
69 apply (tactic "EQgen_tac @{context} [] 1") |
70 apply (drule ListsXH [THEN iffD1]) |
70 apply (drule ListsXH [THEN iffD1]) |
71 apply (tactic "EQgen_tac @{context} [] 1") |
71 apply (tactic "EQgen_tac @{context} [] 1") |
80 and "l:Lists(A)" |
80 and "l:Lists(A)" |
81 and "m:Lists(A)" |
81 and "m:Lists(A)" |
82 shows "k @ l @ m = (k @ l) @ m" |
82 shows "k @ l @ m = (k @ l) @ m" |
83 apply (tactic {* eq_coinduct3_tac @{context} |
83 apply (tactic {* eq_coinduct3_tac @{context} |
84 "{p. EX x y. p=<x,y> & (EX k:Lists (A). EX l:Lists (A). EX m:Lists (A). x=k @ l @ m & y= (k @ l) @ m) }" 1*}) |
84 "{p. EX x y. p=<x,y> & (EX k:Lists (A). EX l:Lists (A). EX m:Lists (A). x=k @ l @ m & y= (k @ l) @ m) }" 1*}) |
85 apply (blast intro: prems) |
85 apply (blast intro: assms) |
86 apply safe |
86 apply safe |
87 apply (drule ListsXH [THEN iffD1]) |
87 apply (drule ListsXH [THEN iffD1]) |
88 apply (tactic "EQgen_tac @{context} [] 1") |
88 apply (tactic "EQgen_tac @{context} [] 1") |
89 prefer 2 |
89 prefer 2 |
90 apply blast |
90 apply blast |
98 lemma ilist_append: |
98 lemma ilist_append: |
99 assumes "l:ILists(A)" |
99 assumes "l:ILists(A)" |
100 shows "l @ m = l" |
100 shows "l @ m = l" |
101 apply (tactic {* eq_coinduct3_tac @{context} |
101 apply (tactic {* eq_coinduct3_tac @{context} |
102 "{p. EX x y. p=<x,y> & (EX l:ILists (A) .EX m. x=l@m & y=l)}" 1 *}) |
102 "{p. EX x y. p=<x,y> & (EX l:ILists (A) .EX m. x=l@m & y=l)}" 1 *}) |
103 apply (blast intro: prems) |
103 apply (blast intro: assms) |
104 apply safe |
104 apply safe |
105 apply (drule IListsXH [THEN iffD1]) |
105 apply (drule IListsXH [THEN iffD1]) |
106 apply (tactic "EQgen_tac @{context} [] 1") |
106 apply (tactic "EQgen_tac @{context} [] 1") |
107 apply blast |
107 apply blast |
108 done |
108 done |