The problem is that ⌜n + 1⌝ can't be matched with a numeric literal. It
may be possible to add such a matching capability but this is easily
worked around by converting the operand first. For a numeric literal,
as in your example, plus1_conv can be used. With this, you can build up
a conversion evaluate your summ function. I've included my steps below
to build up such a conversion. Hopefully you can see what's going on at
each step.
Phil
(* Use plus1_conv to get the operand in the right form *)
plus1_conv ⌜3⌝;
(*
* val it = ⊢ 3 = 2 + 1: THM
*)
(* Convert the argument if non-zero then rewrite *)
(RAND_C (TRY_C plus1_conv) THEN_C pure_once_rewrite_conv [get_spec
⌜summ⌝]) ⌜summ 0⌝;
(RAND_C (TRY_C plus1_conv) THEN_C pure_once_rewrite_conv [get_spec
⌜summ⌝]) ⌜summ 3⌝;
(*
* val it = ⊢ summ 0 = 0: THM
* val it = ⊢ summ 3 = summ 2 + 2 + 1: THM
*)
(* Give this conversion a name and define a conversion that
* recursively applies it to the left operand of the resulting
* '+' term until is fails *)
val summ_step_conv =
RAND_C (TRY_C plus1_conv) THEN_C pure_once_rewrite_conv [get_spec
⌜summ⌝];
fun summ_conv t = (summ_step_conv THEN_TRY_C LEFT_C summ_conv) t;
summ_conv ⌜summ 0⌝;
summ_conv ⌜summ 3⌝;
(*
* val it = ⊢ summ 0 = 0: THM
* val it = ⊢ summ 3 = ((0 + 0 + 1) + 1 + 1) + 2 + 1: THM
*)
(* Add up the resulting '+' tree *)
(summ_conv THEN_C MAP_C plus_conv) ⌜summ 3⌝;
(*
* val it = ⊢ summ 3 = 6: THM
*)
(* We want summ_conv to reduce the '+' terms so sum as we go.
* Redefine the above. *)
val summ_step_conv =
RAND_C (TRY_C plus1_conv) THEN_C pure_once_rewrite_conv [get_spec
⌜summ⌝] THEN_C TRY_C (RIGHT_C plus_conv);
summ_step_conv ⌜summ 0⌝;
summ_step_conv ⌜summ 3⌝;
(*
* val it = ⊢ summ 0 = 0: THM
* val it = ⊢ summ 3 = summ 2 + 3: THM
*)
fun summ_conv t =
(summ_step_conv THEN_TRY_C (LEFT_C summ_conv THEN_C plus_conv)) t;
summ_conv ⌜summ 0⌝;
summ_conv ⌜summ 3⌝;
(*
* val it = ⊢ summ 0 = 0: THM
* val it = ⊢ summ 3 = 6: THM
*)
map summ_conv (map (fn n => mk_app (⌜summ⌝, mk_ℕ (integer_of_int n)))
(interval 0 50));
(*
* val it =
* [⊢ summ 0 = 0, ⊢ summ 1 = 1, ⊢ summ 2 = 3, ⊢ summ 3 = 6,
* ⊢ summ 4 = 10, ⊢ summ 5 = 15, ⊢ summ 6 = 21, ⊢ summ 7 = 28,
* ⊢ summ 8 = 36, ⊢ summ 9 = 45, ⊢ summ 10 = 55,
* ⊢ summ 11 = 66, ⊢ summ 12 = 78, ⊢ summ 13 = 91,
* ⊢ summ 14 = 105, ⊢ summ 15 = 120, ⊢ summ 16 = 136,
* ⊢ summ 17 = 153, ⊢ summ 18 = 171, ⊢ summ 19 = 190,
* ⊢ summ 20 = 210, ⊢ summ 21 = 231, ⊢ summ 22 = 253,
* ⊢ summ 23 = 276, ⊢ summ 24 = 300, ⊢ summ 25 = 325,
* ⊢ summ 26 = 351, ⊢ summ 27 = 378, ⊢ summ 28 = 406,
* ⊢ summ 29 = 435, ⊢ summ 30 = 465, ⊢ summ 31 = 496,
* ⊢ summ 32 = 528, ⊢ summ 33 = 561, ⊢ summ 34 = 595,
* ⊢ summ 35 = 630, ⊢ summ 36 = 666, ⊢ summ 37 = 703,
* ⊢ summ 38 = 741, ⊢ summ 39 = 780, ⊢ summ 40 = 820,
* ⊢ summ 41 = 861, ⊢ summ 42 = 903, ⊢ summ 43 = 946,
* ⊢ summ 44 = 990, ⊢ summ 45 = 1035, ⊢ summ 46 = 1081,
* ⊢ summ 47 = 1128, ⊢ summ 48 = 1176, ⊢ summ 49 = 1225,
* ⊢ summ 50 = 1275]: THM list
*)
On 31/03/20 17:09, David Topham wrote:
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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
