//
// Karlsruhe Institute of Technology
// Institute for Theoretical Computer Science
// Prof. Dr. Bernhard Beckert
// Dr. Vladimir Klebanov
//
// Formale Systeme WS 2009/10

// Praxisübungsblatt 2

// This a problem file to be used with the KeY verification tool.

// =========================================================
//  Don't forget to fill in the blanks indicated with "..."
// =========================================================

// We use two sorts in this problem file: 
// * int  for integers (already built in) and
// * lst  for lists of integers
\sorts {
  lst;
}

\functions {
   lst nil;
   lst cons(int, lst);

   lst insert(int, lst);
   lst sort(lst);

   int count(int, lst);
}

\predicates {
   least(int, lst);
   sorted(lst);
}


// These schema variables are needed to define the rule schemata
// in the next section
\schemaVariables {
   \term int n, m, v;
   \term lst l;

   \variables lst vl;
   \variables int vn;
}


// This section contains extra rules for the sequent calculus.
// They are all explained on the assignment sheet.
\rules {

  listInduction { 
     \schemaVar \variables lst nv;
     \schemaVar \variables int val;
     \schemaVar \formula b;
     \find( ==> (\forall nv; b) )
     \varcond(\notFreeIn(val, b))

     "Base Case": \replacewith ( ==> {\subst nv; nil}(b) );
     "Step Case": \replacewith ( ==> \forall nv ; \forall val ; (b -> {\subst nv; cons(val, nv)}b) )
  };


  leastNil {
     \find( least(n, nil) )
     \replacewith( true )
     \heuristics(simplify)
  };

  leastCons {
     \find( least(n, cons(m, l)) )
     \replacewith( n<=m & least(n,l) )
     \heuristics(simplify)
  };


  sortedNil {
     \find( sorted(nil) )
     \replacewith( true )
     \heuristics(simplify)
  };

  sortedCons {
     \find( sorted(cons(n, l)) )
     \replacewith( least(n,l) & sorted(l) )
     \heuristics(simplify)
  };


  insertNil {
     \find( insert(n, nil) )
     \replacewith( cons(n, nil) )
     \heuristics(simplify)
  };

  insertCons {
     \find( insert(n, cons(m, l)) )
     \replacewith( ... )
     \heuristics(simplify)
  };

  
  sortNil {
     \find( sort(nil) )
     \replacewith( nil )
     \heuristics(simplify)
  };

  sortCons {
     \find( sort(cons(n, l)) )
     \replacewith( ... )
     \heuristics(simplify)
  };


  countNil {
     \find( count(n,nil) )
     \replacewith( 0 )
     \heuristics(simplify)
  };

  countCons {
     \find( count(n, cons(m, l)) )
     \replacewith( count(n,l) + \if(n = m) \then(1) \else(0) )
     \heuristics(simplify)
  };

}


// This is what you need to prove:
\problem {

  \forall lst l;  (sorted(sort(l)) & \forall int n; (count(n,sort(l))=count(n,l)))

}