title: How to define functions with overlapping patterns?
body: <p>I'm trying to define a conjunction function for 4-valued logic (false, true, null, and error):</p>
  
  <pre><code>datatype 'a maybe = Just "'a" | Nothing | Error
  type_synonym bool4 = "bool maybe"
  
  abbreviation JF :: "bool4" where "JF ≡ Just False"
  abbreviation JT :: "bool4" where "JT ≡ Just True"
  abbreviation BN :: "bool4" where "BN ≡ Nothing"
  abbreviation BE :: "bool4" where "BE ≡ Error"
  
  fun and4 :: "bool4 ⇒ bool4 ⇒ bool4" where
    "and4 JF b = JF"
  | "and4 a JF = JF"
  | "and4 BE b = BE"
  | "and4 a BE = BE"
  | "and4 BN b = BN"
  | "and4 a BN = BN"
  | "and4 a b  = JT"
  </code></pre>
  
  <p>I expect that the first patterns have a priority over the last patterns.</p>
  
  <p>It seems that the definition is wrong. I'm trying to evaluate the following expressions:</p>
  
  <pre><code>value "and4 JF b"
  value "and4 a JF"
  </code></pre>
  
  <p>The first one returns JF as expected. But the second one can't be simplified.</p>
  
  <p>As result I can't prove commutativity of the conjunction:</p>
  
  <pre><code>lemma and4_commut:
    "and4 a b = and4 b a"
  </code></pre>
  
  <p>It's recomended to use <code>function</code> instead of <code>fun</code> in <a href="https://isabelle.in.tum.de/doc/functions.pdf" rel="nofollow noreferrer">"Defining Recursive Functions in Isabelle/HOL" by Alexander Krauss</a>. But I get 12 false subgoals:</p>
  
  <pre><code>function and4 :: "bool4 ⇒ bool4 ⇒ bool4" where
    "and4 JF b = JF"
  | "and4 a JF = JF"
  | "and4 BE b = BE"
  | "and4 a BE = BE"
  | "and4 BN b = BN"
  | "and4 a BN = BN"
  | "and4 a b  = JT"
    apply pat_completeness
    apply auto
  </code></pre>
  
  <p>I guess it's because the function has conflicting patterns. For example, <code>and4 JF BE</code> are matched by the 1st and 4th patterns. And the result of conjuction could be either JF or BE.</p>
  
  <p>What is a right way to define such a functions? And how to prove its commutativity? I can use a <code>case of</code> construction but it complicates the function definition.</p>