src/HOL/ex/Unification.thy
 changeset 24444 448978b61556 parent 23777 60b7800338d5 child 30909 bd4f255837e5
1.1 --- a/src/HOL/ex/Unification.thy	Tue Aug 28 03:58:37 2007 +0200
1.2 +++ b/src/HOL/ex/Unification.thy	Tue Aug 28 11:25:29 2007 +0200
1.3 @@ -178,7 +178,7 @@
1.4    show "\<theta> =\<^sub>s [(v,t)] \<bullet> \<theta>"
1.5    proof
1.6      fix s show "s \<triangleleft> \<theta> = s \<triangleleft> [(v,t)] \<bullet> \<theta>" using th
1.7 -      by (induct s, auto)
1.8 +      by (induct s) auto
1.9    qed
1.10  qed
1.12 @@ -194,7 +194,7 @@
1.13    assumes "unify_dom (M, N)"
1.14    assumes "unify M N = Some \<sigma>"
1.15    shows "MGU \<sigma> M N"
1.16 -using prems
1.17 +using assms
1.18  proof (induct M N arbitrary: \<sigma>)
1.19    case (7 M N M' N' \<sigma>) -- "The interesting case"
1.21 @@ -357,21 +357,21 @@
1.22    assumes "unify M N = Some \<sigma>"
1.23    shows "vars_of (t \<triangleleft> \<sigma>) \<subseteq> vars_of M \<union> vars_of N \<union> vars_of t"
1.24    (is "?P M N \<sigma> t")
1.25 -using prems
1.26 +using assms
1.27  proof (induct M N arbitrary:\<sigma> t)
1.28    case (3 c v)
1.29    hence "\<sigma> = [(v, Const c)]" by simp
1.30 -  thus ?case by (induct t, auto)
1.31 +  thus ?case by (induct t) auto
1.32  next
1.33    case (4 M N v)
1.34    hence "\<not>occ (Var v) (M\<cdot>N)" by (cases "occ (Var v) (M\<cdot>N)", auto)
1.35 -  with prems have "\<sigma> = [(v, M\<cdot>N)]" by simp
1.36 -  thus ?case by (induct t, auto)
1.37 +  with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
1.38 +  thus ?case by (induct t) auto
1.39  next
1.40    case (5 v M)
1.41    hence "\<not>occ (Var v) M" by (cases "occ (Var v) M", auto)
1.42 -  with prems have "\<sigma> = [(v, M)]" by simp
1.43 -  thus ?case by (induct t, auto)
1.44 +  with 5 have "\<sigma> = [(v, M)]" by simp
1.45 +  thus ?case by (induct t) auto
1.46  next
1.47    case (7 M N M' N' \<sigma>)
1.48    then obtain \<theta>1 \<theta>2
1.49 @@ -420,7 +420,7 @@
1.50    assumes "unify M N = Some \<sigma>"
1.51    shows "(\<exists>v\<in>vars_of M \<union> vars_of N. elim \<sigma> v) \<or> \<sigma> =\<^sub>s []"
1.52    (is "?P M N \<sigma>")
1.53 -using prems
1.54 +using assms
1.55  proof (induct M N arbitrary:\<sigma>)
1.56    case 1 thus ?case by simp
1.57  next
1.58 @@ -428,19 +428,19 @@
1.59  next
1.60    case (3 c v)
1.61    have no_occ: "\<not> occ (Var v) (Const c)" by simp
1.62 -  with prems have "\<sigma> = [(v, Const c)]" by simp
1.63 +  with 3 have "\<sigma> = [(v, Const c)]" by simp
1.64    with occ_elim[OF no_occ]
1.65    show ?case by auto
1.66  next
1.67    case (4 M N v)
1.68    hence no_occ: "\<not>occ (Var v) (M\<cdot>N)" by (cases "occ (Var v) (M\<cdot>N)", auto)
1.69 -  with prems have "\<sigma> = [(v, M\<cdot>N)]" by simp
1.70 +  with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
1.71    with occ_elim[OF no_occ]
1.72    show ?case by auto
1.73  next
1.74    case (5 v M)
1.75    hence no_occ: "\<not>occ (Var v) M" by (cases "occ (Var v) M", auto)
1.76 -  with prems have "\<sigma> = [(v, M)]" by simp
1.77 +  with 5 have "\<sigma> = [(v, M)]" by simp
1.78    with occ_elim[OF no_occ]
1.79    show ?case by auto
1.80  next