summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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.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