equal
deleted
inserted
replaced
81 val lemma = result(); |
81 val lemma = result(); |
82 qed_spec_mp "Cons_acc_step1I"; |
82 qed_spec_mp "Cons_acc_step1I"; |
83 AddSIs [Cons_acc_step1I]; |
83 AddSIs [Cons_acc_step1I]; |
84 |
84 |
85 Goal "xs : lists(acc r) ==> xs : acc(step1 r)"; |
85 Goal "xs : lists(acc r) ==> xs : acc(step1 r)"; |
86 be lists.induct 1; |
86 by (etac lists.induct 1); |
87 by (rtac accI 1); |
87 by (rtac accI 1); |
88 by (asm_full_simp_tac (simpset() addsimps [step1_def]) 1); |
88 by (asm_full_simp_tac (simpset() addsimps [step1_def]) 1); |
89 by (rtac accI 1); |
89 by (rtac accI 1); |
90 by (fast_tac (claset() addDs [acc_downward]) 1); |
90 by (fast_tac (claset() addDs [acc_downward]) 1); |
91 qed "lists_accD"; |
91 qed "lists_accD"; |