From 667bb82437c0b8b3915efe96c657703bcaa508af Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Johannes=20=C3=85man=20Pohjola?= <j.amanpohjola@unsw.edu.au>
Date: Fri, 10 Nov 2023 21:04:50 +1100
Subject: [PATCH] Add case_elim thm for nterm

---
 .../triangular/nominal/ntermScript.sml         | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/examples/algorithms/unification/triangular/nominal/ntermScript.sml b/examples/algorithms/unification/triangular/nominal/ntermScript.sml
index db1fed8b14..8d7738e1f8 100644
--- a/examples/algorithms/unification/triangular/nominal/ntermScript.sml
+++ b/examples/algorithms/unification/triangular/nominal/ntermScript.sml
@@ -257,6 +257,23 @@ val nterm_case_eq = Q.store_thm(
   ‘∀p. p == c2 <=> p == c1’ suffices_by simp[] >>
   metis_tac[permeq_def]);
 
+val nterm_case_elim = Q.store_thm(
+  "nterm_case_elim",
+  ‘∀f. (f(nterm_CASE n nmf sf tf pf cf) ⇔
+     (∃a. (n = Nom a) ∧ f(nmf a)) ∨
+     (∃p w. (n = Sus p w) ∧ f(sf (@p'. p' == p) w)) ∨
+     (∃a t. (n = Tie a t) ∧ f(tf a t)) ∨
+     (∃t1 t2. (n = nPair t1 t2) ∧ f(pf t1 t2)) ∨
+     (∃c. (n = nConst c) ∧ f(cf c)))’,
+  strip_tac >>
+  Q.ISPEC_THEN ‘n’ STRUCT_CASES_TAC nterm_nchotomy >>
+  simp[nterm_case_rewrites, Sus_case1] >> eq_tac >> rw[]
+  >- (first_x_assum $ irule_at $ Pos last >> rw[]) >>
+  pop_assum mp_tac >>
+  rename [‘_ (_ (@p'. p' == c1) _) ⇒ _(_ (@p'. p' == c2) _)’] >>
+  ‘∀p. p == c2 <=> p == c1’ suffices_by simp[] >>
+  metis_tac[permeq_def]);
+
 local open TypeBase TypeBasePure Drule
 in
 val _ = export [
@@ -268,6 +285,7 @@ val _ = export [
                   in n::Sus_case1::rest end),
       case_cong = nterm_case_cong,
       case_eq = nterm_case_eq,
+      case_elim = nterm_case_elim,
       nchotomy = nterm_nchotomy,
       size = SOME (``nterm_size``,ORIG nterm_size_def),
       encode = NONE,