[isabelle] Code generation for inductive predicates



Hi all,

I tried out code generation for inductive predicates, and wonder when
the generated code will terminate.

In the code below, I inductively formulate the reflexive, transitive
closure of a transition relation.
No I want code to enumerate all the words that lead from one state to
another. This works well
if there exists such words. However, if there exists no such word, the
generated code simply does not terminate.
This is the same for the predicate w_nempty, that checks whether there
exists a word between two given states.

So what happens here? When does the generated code terminate? And is
there a simple way to generate code for "w_nempty" that terminates?

Many thanks in advance for any hints,
  Peter


  -- "A transition relation"
  inductive_set d1 :: "(nat * char * nat) set" where
    "(1,CHR ''a'',2) : d1" |
    "(2,CHR ''b'',2) : d1"

  -- "Reflexive, transitive closure"
  inductive word where
    "word \<delta> q [] q" |
    "[| (q,a,qh):\<delta>; word \<delta> qh w q' |] ==> word \<delta> q
(a#w) q'"

  -- "Whether a word from q to q' exists"
  inductive w_nempty where
    "word \<delta> q w q' ==> w_nempty \<delta> q q'"

  code_module test
    contains
      test1 = "word d1 1 _ 2"
      test2 = "word d1 2 _ 1"
      test3 = "%d q q'. w_nempty d q q'"
  (*
    test4 = "w_nempty d1 2 1"  However, with this, code generation does
not terminate.
  *)
  
  -- "These behave as expected: "
  ML {*
    DSeq.pull (test.test1);
    *}

  ML {*
    let val d = [(0,(#"a",1)), (1,(#"b",1))] in
      test.test3 d 0 1
    end
    *}

  -- "These does not terminate:"
  ML {*
    DSeq.pull (test.test2);
    *}
  ML {*
    let val d = [(0,(#"a",1)), (1,(#"b",1))] in
      test.test3 d 1 0
    end
    *}






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