In this paper we propose a Weak Lambda Calculus called λP
w having explicit operators for Pattern Matching and Substitution. This formalism is able to specify functions defined by cases via pattern matching constructors as done by most modern functional
programming languages such as OCAML. We show the main property enjoyed by λP
w, namely subject reduction, confluence and strong normalization.