equal
deleted
inserted
replaced
385 (rtac beta_cfun 1), |
385 (rtac beta_cfun 1), |
386 (contX_tacR 1), |
386 (contX_tacR 1), |
387 (rtac refl 1) |
387 (rtac refl 1) |
388 ]); |
388 ]); |
389 |
389 |
|
390 (* ------------------------------------------------------------------------ |
|
391 |
|
392 given the definition |
|
393 |
|
394 smap_def |
|
395 "smap = fix[LAM h f s. stream_when[LAM x l.scons[f[x]][h[f][l]]][s]]" |
|
396 |
|
397 use fix_prover for |
|
398 |
|
399 val smap_def2 = fix_prover Stream2.thy smap_def |
|
400 "smap = (LAM f s. stream_when[LAM x l.scons[f[x]][smap[f][l]]][s])"; |
|
401 |
|
402 ------------------------------------------------------------------------ *) |
390 |
403 |
391 (* ------------------------------------------------------------------------ *) |
404 (* ------------------------------------------------------------------------ *) |
392 (* better access to definitions *) |
405 (* better access to definitions *) |
393 (* ------------------------------------------------------------------------ *) |
406 (* ------------------------------------------------------------------------ *) |
394 |
407 |
879 (res_inst_tac [("s","False"),("t","Suc(ia) < Suc(i)")] ssubst 1), |
892 (res_inst_tac [("s","False"),("t","Suc(ia) < Suc(i)")] ssubst 1), |
880 (asm_simp_tac nat_ss 1), |
893 (asm_simp_tac nat_ss 1), |
881 (rtac iffI 1), |
894 (rtac iffI 1), |
882 (etac FalseE 2), |
895 (etac FalseE 2), |
883 (rtac notE 1), |
896 (rtac notE 1), |
884 (etac less_not_sym 1), |
897 (etac (less_not_sym RS mp) 1), |
885 (atac 1), |
898 (atac 1), |
886 (asm_simp_tac Cfun_ss 1), |
899 (asm_simp_tac Cfun_ss 1), |
887 (etac (is_chainE RS spec) 1), |
900 (etac (is_chainE RS spec) 1), |
888 (hyp_subst_tac 1), |
901 (hyp_subst_tac 1), |
889 (asm_simp_tac nat_ss 1), |
902 (asm_simp_tac nat_ss 1), |
919 ssubst 1), |
932 ssubst 1), |
920 (res_inst_tac [("s","False"),("t","n < Suc(i)")] ssubst 1), |
933 (res_inst_tac [("s","False"),("t","n < Suc(i)")] ssubst 1), |
921 (rtac iffI 1), |
934 (rtac iffI 1), |
922 (etac FalseE 2), |
935 (etac FalseE 2), |
923 (rtac notE 1), |
936 (rtac notE 1), |
924 (etac less_not_sym 1), |
937 (etac (less_not_sym RS mp) 1), |
925 (atac 1), |
938 (atac 1), |
926 (asm_simp_tac nat_ss 1), |
939 (asm_simp_tac nat_ss 1), |
927 (dtac spec 1), |
940 (dtac spec 1), |
928 (rtac mp 1), |
941 (rtac mp 1), |
929 (atac 1), |
942 (atac 1), |