I have been able to get the length sample for HOLCONST from user013 to work, but when I try my own function, I get an error. Can anyone see what my problem is? I suspect it may be setting the correct proof context since I needed to add set_pc "hol2" to get the length function to work. I have tried several contexts such as "lin_arith", "R", "misc", but I have not seen how to find the correct one (if that is even the problem).
This one OK: :) force_delete_theory "cs113" handle Fail _ => (); val it = (): unit :) open_theory "hol"; new_theory "cs113"; val it = (): unit val it = (): unit :) set_pc "hol2"; val it = (): unit :) ⓈHOLCONST :# │ length:'a LIST→ℕ :# ├── :# │ length [] = 0 :# │ ∧ ∀ h t⦁ length (Cons h t) = length t + 1 :# │ :# ■ val it = ⊢ length [] = 0 ∧ (∀ h t⦁ length (Cons h t) = length t + 1): THM :) get_spec⌜length⌝; val it = ⊢ length [] = 0 ∧ (∀ h t⦁ length (Cons h t) = length t + 1): THM :) rewrite_conv[get_spec⌜length⌝] ⌜length [1;2;3;4]⌝; val it = ⊢ length [1; 2; 3; 4] = 4: THM But not this one: :) ⓈHOLCONST :# │ summ:ℕ→ℕ :# ├── :# │ summ 0 = 0 :# │ ∧ ∀n⦁ summ (n + 1) = (summ n) + (n + 1) :# │ :# ■ val it = ⊢ summ 0 = 0 ∧ (∀ n⦁ summ (n + 1) = summ n + n + 1): THM :# get_spec⌜summ⌝; val it = ⊢ summ 0 = 0 ∧ (∀ n⦁ summ (n + 1) = summ n + n + 1): THM :) rewrite_conv[get_spec⌜summ⌝] ⌜summ 2⌝; Exception Fail * no rewriting occurred [rewrite_conv.26001] * raised
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
