# HG changeset patch
# User desharna
# Date 1656668646 -7200
# Node ID a7e0129b8b2d3093c11a4ab5899c8d9011af3c74
# Parent  3b5a2e01b73b4125b8643cf03406d52b30776ad9
tuned proofs

diff -r 3b5a2e01b73b -r a7e0129b8b2d src/HOL/ex/Unification.thy
--- a/src/HOL/ex/Unification.thy	Thu Jun 30 22:49:47 2022 +0200
+++ b/src/HOL/ex/Unification.thy	Fri Jul 01 11:44:06 2022 +0200
@@ -530,7 +530,7 @@
 qed (auto intro!: Var_Idem split: option.splits if_splits)
 
 
-subsection \<open>Unification Returns Substitution With Minimal Range \<close>
+subsection \<open>Unification Returns Substitution With Minimal Domain And Range\<close>
 
 definition range_vars where
   "range_vars \<sigma> = \<Union> {vars_of (Var x \<lhd> \<sigma>) |x. Var x \<lhd> \<sigma> \<noteq> Var x}"
@@ -541,15 +541,15 @@
   thus "x \<in> vars_of N \<union> range_vars \<sigma>"
   proof (induction N)
     case (Var y)
-    then show ?case
-      unfolding range_vars_def vars_of.simps
-      by force
+    thus ?case
+      unfolding range_vars_def vars_of.simps by force
   next
     case (Const y)
-    then show ?case by simp
+    thus ?case
+      by simp
   next
     case (Comb N1 N2)
-    then show ?case
+    thus ?case
       by auto
   qed
 qed
@@ -672,8 +672,10 @@
     by (simp add: dom_def)
 next
   case (6 c d)
-  then show ?case
-    by (cases "c = d") simp_all
+  hence "\<sigma> = []"
+    by (metis option.distinct(1) option.sel unify.simps(6))
+  thus ?case
+    by simp
 next
   case (7 M N M' N')
   from "7.prems" obtain \<theta>\<^sub>1 \<theta>\<^sub>2 where
@@ -694,9 +696,9 @@
   also have "... = fst ` set \<theta>\<^sub>1 \<union> fst ` set \<theta>\<^sub>2"
     by (auto simp: domain_comp)
   also have "... \<subseteq> vars_of M \<union> vars_of M' \<union> fst ` set \<theta>\<^sub>2"
-    using dom_\<theta>\<^sub>1 by (auto simp: dom_map_of_conv_image_fst)
+    using dom_\<theta>\<^sub>1 by auto
   also have "... \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of N \<union> vars_of N' \<union> range_vars \<theta>\<^sub>1"
-    using dom_\<theta>\<^sub>2 by (auto simp: dom_map_of_conv_image_fst)
+    using dom_\<theta>\<^sub>2 by auto
   also have "... \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of N \<union> vars_of N'"
     using unify_gives_minimal_range[OF \<open>unify M M' = Some \<theta>\<^sub>1\<close>] by auto
   finally show ?case