equal
deleted
inserted
replaced
106 "{p. EX x y.p=<x,y> & (EX n:Nat.x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}" |
106 "{p. EX x y.p=<x,y> & (EX n:Nat.x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}" |
107 1); |
107 1); |
108 by (fast_tac (type_cs addSIs [napplyBzero RS sym, |
108 by (fast_tac (type_cs addSIs [napplyBzero RS sym, |
109 napplyBzero RS sym RS arg_cong]) 1); |
109 napplyBzero RS sym RS arg_cong]) 1); |
110 by (EQgen_tac list_ss [iter1B,iter2Blemma] 1); |
110 by (EQgen_tac list_ss [iter1B,iter2Blemma] 1); |
111 by (assume_tac 1); (*should EQgen_tac call asm_simp_tac?*) |
|
112 by (rtac (napply_f RS ssubst) 1 THEN atac 1); |
111 by (rtac (napply_f RS ssubst) 1 THEN atac 1); |
113 by (res_inst_tac [("f1","f")] (napplyBsucc RS subst) 1); |
112 by (res_inst_tac [("f1","f")] (napplyBsucc RS subst) 1); |
114 by (fast_tac type_cs 1); |
113 by (fast_tac type_cs 1); |
115 val iter1_iter2_eq = result(); |
114 val iter1_iter2_eq = result(); |