equal
deleted
inserted
replaced
2784 done |
2784 done |
2785 |
2785 |
2786 lemma wf_tm_from_abacus: |
2786 lemma wf_tm_from_abacus: |
2787 "tp = tm_of ap \<Longrightarrow> |
2787 "tp = tm_of ap \<Longrightarrow> |
2788 tm_wf (tp @ shift( mopup n) (length tp div 2), 0)" |
2788 tm_wf (tp @ shift( mopup n) (length tp div 2), 0)" |
2789 using length_start_of_tm[of ap] all_le_start_of[of ap] |
2789 using length_start_of_tm[of ap] all_le_start_of[of ap] |
2790 apply(auto simp: tm_wf.simps List.list_all_iff) |
2790 apply(auto simp: tm_wf.simps List.list_all_iff) |
2791 done |
2791 apply(case_tac n) |
|
2792 apply(simp add: mopup.simps) |
|
2793 apply(simp add: mopup.simps) |
|
2794 apply (metis mod_mult_right_eq mod_mult_self2 mod_mult_self2_is_0 mult_2_right nat_mult_commute numeral_Bit0) |
|
2795 sorry |
2792 |
2796 |
2793 lemma wf_tm_from_recf: |
2797 lemma wf_tm_from_recf: |
2794 assumes compile: "tp = tm_of_rec recf" |
2798 assumes compile: "tp = tm_of_rec recf" |
2795 shows "tm_wf0 tp" |
2799 shows "tm_wf0 tp" |
2796 proof - |
2800 proof - |