# HG changeset patch
# User desharna
# Date 1656490414 -7200
# Node ID 3ba38a1197393da7331e46c4f9211a4a913dcbe7
# Parent  f5015fa7cb1909ad65b88c9cbdd5edff7e6eb6b4
added definition IMGU and lemmas IMGU_iff_Idem_and_MGU and unify_computes_IMGU

diff -r f5015fa7cb19 -r 3ba38a119739 src/HOL/ex/Unification.thy
--- a/src/HOL/ex/Unification.thy	Tue Jun 28 17:55:30 2022 +0200
+++ b/src/HOL/ex/Unification.thy	Wed Jun 29 10:13:34 2022 +0200
@@ -524,4 +524,18 @@
   qed
 qed (auto intro!: Var_Idem split: option.splits if_splits)
 
+
+subsection \<open>Idempotent Most General Unifier\<close>
+
+definition IMGU :: "'a subst \<Rightarrow> 'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" where
+  "IMGU \<mu> t u \<longleftrightarrow> Unifier \<mu> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u \<longrightarrow> \<theta> \<doteq> \<mu> \<lozenge> \<theta>)"
+
+lemma IMGU_iff_Idem_and_MGU: "IMGU \<mu> t u \<longleftrightarrow> Idem \<mu> \<and> MGU \<mu> t u"
+  unfolding IMGU_def Idem_def MGU_def
+  by (smt (verit, best) subst_comp subst_eq_def)
+
+lemma unify_computes_IMGU:
+  "unify M N = Some \<sigma> \<Longrightarrow> IMGU \<sigma> M N"
+  by (simp add: IMGU_iff_Idem_and_MGU unify_computes_MGU unify_gives_Idem)
+
 end