% CAFR WS2007/08
% 2007-12-17
% normalization of if expressions

% if expressions are given by the grammar
%   e ::= x | true | false | if e1 then e2 else e3
% where x ranges over variables

% we represent if expressions by an abstract datatype, leaving
% the type t of variable names abstract

ifexp[t:TYPE] : DATATYPE
  BEGIN
    ident(x:t) : ident?
    const(b:boolean) : const?
    ifthenelse(c,t,e:ifexp) : ifthenelse?
  END ifexp

% the goal is to normalize if expressions into decision trees
% i.e., conditions are only variables
% we call decision trees "normal if expressions"

normalize_if[t:TYPE] : THEORY
BEGIN

  IMPORTING ifexp_adt 

  height : [ifexp[t] -> nat] 
    = reduce_nat(LAMBDA(x:t):0, 
                 LAMBDA(c:boolean):0, 
                 LAMBDA(c,t,e:nat) : 1 + max(max(c,t),e))

  % the meaning of an if-expression is given by eval

  eval(e:ifexp[t],rho:[t -> boolean]) : RECURSIVE boolean =
    CASES e OF
      ident(x) : rho(x) ,
      const(b) : b ,
      ifthenelse(c,t,e) : IF eval(c,rho) THEN eval(t,rho) ELSE eval(e,rho) ENDIF
    ENDCASES 
  MEASURE height(e)

  % an expression is normal if for every subexpression of the form if(e1,e2,e3)
  %   e1 is a variable

  % give a recursive definition of

  normal(e:ifexp[t]) : RECURSIVE boolean = ...
  MEASURE height(e)

  % subtype of normal if expressions

  nifexp : TYPE = (normal)

  % this is short for
  %   nifexp : TYPE = { e : ifexp[t] | normal(e) }

  % define a normalizer for if expressions

  normalize(e:ifexp[t]) : RECURSIVE nifexp = ...

  % you might need an auxiliary function...

  % you might need a lemma about your auxiliary function
  % try and prove it with (induct-and-simplify "...")

  norm_correct : THEOREM
   FORALL (e:ifexp[t]) : FORALL (rho:[t->boolean]): 
     eval(normalize(e),rho) = eval(e,rho)

  % prove correctness of the normalizer with 
  % (auto-rewrite "lemma...")
  % (induct-and-simplify "e")
    
END semantics