Theory Execute

(*  Author:     Stefan Berghofer, TU Muenchen, 2005; Lukas Bulwahn, TU Muenchen, 2009

theory Execute
imports POPLmarkRecord "HOL-Library.Code_Target_Numeral"

section ‹Executing the specification›

text ‹
An important criterion that a solution to the {\sc PoplMark} Challenge should
fulfill is the possibility to {\it animate} the specification. For example,
it should be possible to apply the reduction relation for the calculus to
example terms. Since the reduction relations are defined inductively, they can
be interpreted as a logic program in the style of {\sc Prolog}.
The definition of the single-step evaluation relation presented in \secref{sec:evaluation}
and \secref{sec:evaluation-rcd} is directly executable.

In order to compute the normal form of a term using the one-step evaluation
relation ⟼›, we introduce the inductive predicate t ⇓ u›,
denoting that u› is a normal form of t›.

inductive norm :: "trm  trm  bool"  (infixl "" 50)
  "t  value  t  t"
| "t  s  s  u  t  u"

definition normal_forms where
  "normal_forms t  {u. t  u}"

lemma [code_pred_intro Rcd_Nil]: "valuep (Rcd [])"
by (auto intro: valuep.intros)

lemma [code_pred_intro Rcd_Cons]: "valuep t  valuep (Rcd fs)  valuep (Rcd ((l, t) # fs))" 
by (auto intro!: valuep.intros elim!: valuep.cases)

lemmas valuep.intros(1)[code_pred_intro Abs'] valuep.intros(2)[code_pred_intro TAbs']

code_pred (modes: i => bool) valuep
proof -
  case valuep
  from valuep.prems show thesis
  proof (cases rule: valuep.cases)
    case (Rcd fs)
    from this valuep.Rcd_Nil valuep.Rcd_Cons show thesis
      by (cases fs) (auto intro: valuep.intros)
    case Abs
    with valuep.Abs' show thesis .
    case TAbs
    with valuep.TAbs' show thesis .

thm valuep.equation

code_pred (modes: i => i => bool, i => o => bool as normalize) norm .

thm norm.equation

lemma [code]:
  "normal_forms = set_of_pred o normalize"
unfolding set_of_pred_def o_def normal_forms_def [abs_def]
by (auto intro: set_eqI normalizeI elim: normalizeE)

lemma [code_unfold]: "x  value  valuep x"
  by (simp add: value_def)

  natT :: type where
  "natT  ∀<:Top. (∀<:TVar 0. (∀<:TVar 1. (TVar 2  TVar 1)  TVar 0  TVar 1))"

  fact2 :: trm where
   LET PVar natT =
     (λ<:Top. λ<:TVar 0. λ<:TVar 1. λ:TVar 2  TVar 1. λ: TVar 1. Var 1  Var 0)
   LET PRcd
     [(''pluspp'', PVar (natT  natT  natT)),
      (''multpp'', PVar (natT  natT  natT))] = Rcd
     [(''multpp'', λ:natT. λ:natT. λ<:Top. λ<:TVar 0. λ<:TVar 1. λ:TVar 2  TVar 1.
        Var 5 τ TVar 3 τ TVar 2 τ TVar 1  (Var 4 τ TVar 3 τ TVar 2 τ TVar 1)  Var 0),
      (''pluspp'', λ:natT. λ:natT. λ<:Top. λ<:TVar 0. λ<:TVar 1. λ:TVar 2  TVar 1. λ:TVar 1.
        Var 6 τ TVar 4 τ TVar 3 τ TVar 3  Var 1 
          (Var 5 τ TVar 4 τ TVar 3 τ TVar 2  Var 1  Var 0))]
     Var 0  (Var 1  Var 2  Var 2)  Var 2"

value "normal_forms fact2"

text ‹
Unfortunately, the definition based
on evaluation contexts from \secref{sec:evaluation-ctxt} is not directly executable.
The reason is that from the definition of evaluation contexts, the code generator
cannot immediately read off an algorithm that, given a term t›, computes a context
E› and a term t0 such that t = E t0. In order to do this, one
would have to extract the algorithm contained in the proof of the {\it decomposition lemma}
from \secref{sec:evaluation-ctxt}.

values "{u. norm fact2 u}"