induct: proper separation of initial and terminal step;
authorwenzelm
Tue Aug 28 11:25:29 2007 +0200 (2007-08-28)
changeset 24444448978b61556
parent 24443 ab6206ccb570
child 24445 cad0644294a9
induct: proper separation of initial and terminal step;
avoid unspecific prems;
src/HOL/ex/Unification.thy
     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.11  
    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.20  
    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