[isabelle] Handling theory errors



Hi all!

When modifying a theory, for instance using "FundefPackage.add_fundef_i", how sould errors be handled? In particular, catching them and using the original theory results in stale theory errors?

This is the problematic theory:

(***************************************)
theory Test
imports Main
begin

datatype numero = Cero | Siguiente numero

ML {*
local
 val by_pat_completeness_simp =
   Proof.global_terminal_proof
     (Method.Basic (K FundefDatatype.pat_completeness, Position.none),
SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))));

 val termination_by_lexicographic_order =
   FundefPackage.setup_termination_proof NONE
   #> Proof.global_terminal_proof
(Method.Basic (LexicographicOrder.lexicographic_order [], Position.none), NONE);
in
 fun simple_function name eqs thy =
   let
     val group = serial_string ();
     val config = FundefCommon.FundefConfig
{sequential = false, default = "%x. arbitrary", domintros = false, tailrec = false};
   in
     tracing group;
     TheoryTarget.init NONE thy
     |> LocalTheory.set_group group
     |> FundefPackage.add_fundef_i
[(name, NONE, NoSyn)] (map (fn t => (("", []), t)) eqs) config []
     |> by_pat_completeness_simp
     |> LocalTheory.restore
     |> LocalTheory.set_group group
     |> termination_by_lexicographic_order
     |> ProofContext.theory_of
   end;
end;

fun activate_defs eqs thry =
  case eqs of
(name,eqns) :: teq => activate_defs teq (simple_function name eqns thry handle ERROR e => thry)
   |     _     => thry;

val eqs1 = [ at {prop "DEF1 x Cero = Siguiente x"},
@{prop "DEF1 (x::numero) (Siguiente y) = Siguiente (DEF1 x y)"}];

val eqs2 = [ at {prop "DEF2 x Cero = Siguiente x"},
@{prop "DEF2 x y = (DEF2::numero=>numero=>numero) x y"}];

val eqs3 = [ at {prop "DEF3 x Cero = (x::numero)"},
@{prop "DEF3 x (Siguiente y) = Siguiente (DEF3 (x::numero) y)"}];
*}


(* This generates the Stale theory error *)
setup{*
activate_defs [("DEF1",eqs1),("DEF2",eqs2),("DEF3",eqs3)]
*}

(* However swapping DEF1 and DEF2 generates no error *)
setup{*
activate_defs [("DEF2",eqs2),("DEF1",eqs1),("DEF3",eqs3)]
*}

(***************************************)

Thanks in advance!

Regards,
Omar Montano

--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.