Define tail-recursive, guard-less unify function; show it correct

HOL-Theorem-Prover · Nov 28, 2023 · 1a1f92b · 1a1f92b
1 parent 33c555b
commit 1a1f92b
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 1 deletion.
diff --git a/examples/algorithms/unification/triangular/first-order/compilation/tcallUnifScript.sml b/examples/algorithms/unification/triangular/first-order/compilation/tcallUnifScript.sml
@@ -768,4 +768,18 @@ Theorem tunifywl_thm =
                               sum_CASE_COND, sum_CASE_pair_CASE]
                      |> SRULE[GSYM tunifywl_def]
 
+Theorem tunify_correct =
+        kunify_cleaned
+          |> SRULE [GSYM tunifywl_def, FORALL_PROD, kunifywl_def]
+          |> Q.SPECL [‘s’, ‘[(t1,t2)]’]
+          |> SRULE[GSYM abs_EQ_apply_unifkont, dfkunify_def, kunify_def,
+                   cwc_def]
+          |> SRULE[apply_unifkont_thm, sunify_def]
+          |> Q.INST [‘s’ |-> ‘fm2sp σ’]
+          |> SRULE[swfs_def]
+          |> UNDISCH
+          |> Q.AP_TERM ‘OPTION_MAP sp2fm’
+          |> SRULE[OPTION_MAP_COMPOSE, combinTheory.o_DEF]
+          |> DISCH_ALL
+
 val _ = export_theory();
diff --git a/src/parallel_builds/core/Holmakefile b/src/parallel_builds/core/Holmakefile
@@ -67,7 +67,7 @@ INCLUDES += ../../tfl/examples $(patsubst %,../../quotient/%,$(QUOTDIRS)) \
 ifneq($(HOLSELFTESTLEVEL),1)
 EX2DIRS = AKS algebra algorithms/boyer_moore \
             algorithms/unification/triangular/nominal \
-            algorithms/unification/triangular/first-order \
+            algorithms/unification/triangular/first-order/compilation \
             arm/arm6-verification/correctness \
             arm/v4 arm/v7 \
           balanced_bst \