added proof of idempotence, roughly after HOL/Subst/Unify.thy
authorkrauss
Sun Aug 21 22:13:04 2011 +0200 (2011-08-21)
changeset 443713a10392fb8c3
parent 44370 03d91bfad83b
child 44372 f9825056dbab
added proof of idempotence, roughly after HOL/Subst/Unify.thy
src/HOL/ex/Unification.thy
     1.1 --- a/src/HOL/ex/Unification.thy	Sun Aug 21 22:13:04 2011 +0200
     1.2 +++ b/src/HOL/ex/Unification.thy	Sun Aug 21 22:13:04 2011 +0200
     1.3 @@ -118,6 +118,9 @@
     1.4  lemma subst_trans[trans]: "\<lbrakk>s1 \<doteq> s2; s2 \<doteq> s3\<rbrakk> \<Longrightarrow> s1 \<doteq> s3"
     1.5    by (auto simp:subst_eq_def)
     1.6  
     1.7 +lemma subst_no_occs: "\<not> Var v \<prec> t \<Longrightarrow> Var v \<noteq> t
     1.8 +  \<Longrightarrow> t \<lhd> [(v,s)] = t"
     1.9 +by (induct t) auto
    1.10  
    1.11  text {* Composition of Substitutions *}
    1.12  
    1.13 @@ -170,6 +173,9 @@
    1.14    "MGU \<sigma> s t \<Longrightarrow> MGU \<sigma> t s"
    1.15    by (auto simp:MGU_def Unifier_def)
    1.16  
    1.17 +lemma MGU_is_Unifier: "MGU \<sigma> t u \<Longrightarrow> Unifier \<sigma> t u"
    1.18 +unfolding MGU_def by (rule conjunct1)
    1.19 +
    1.20  lemma MGU_Var: 
    1.21    assumes "\<not> Var v \<prec> t"
    1.22    shows "MGU [(v,t)] (Var v) t"
    1.23 @@ -431,7 +437,6 @@
    1.24  
    1.25  lemma unify_computes_MGU:
    1.26    "unify M N = Some \<sigma> \<Longrightarrow> MGU \<sigma> M N"
    1.27 -using assms
    1.28  proof (induct M N arbitrary: \<sigma> rule: unify.induct)
    1.29    case (7 M N M' N' \<sigma>) -- "The interesting case"
    1.30  
    1.31 @@ -476,6 +481,62 @@
    1.32    qed
    1.33  qed (auto simp: MGU_Const intro: MGU_Var MGU_Var[symmetric] split: split_if_asm)
    1.34  
    1.35 +lemma Idem_Nil [iff]: "Idem []"
    1.36 +  by (simp add: Idem_def)
    1.37  
    1.38 +lemma Var_Idem: 
    1.39 +  assumes "~ (Var v \<prec> t)" shows "Idem [(v,t)]"
    1.40 +  unfolding Idem_def
    1.41 +proof
    1.42 +  from assms have [simp]: "t \<lhd> [(v, t)] = t"
    1.43 +    by (metis assoc.simps(2) subst.simps(1) subst_no_occs)
    1.44 +
    1.45 +  fix s show "s \<lhd> [(v, t)] \<lozenge> [(v, t)] = s \<lhd> [(v, t)]"
    1.46 +    by (induct s) auto
    1.47 +qed
    1.48 +
    1.49 +lemma Unifier_Idem_subst: 
    1.50 +  "Idem(r) \<Longrightarrow> Unifier s (t \<lhd> r) (u \<lhd> r) \<Longrightarrow>
    1.51 +    Unifier (r \<lozenge> s) (t \<lhd> r) (u \<lhd> r)"
    1.52 +by (simp add: Idem_def Unifier_def subst_eq_def)
    1.53 +
    1.54 +lemma Idem_comp:
    1.55 +  "Idem r \<Longrightarrow> Unifier s (t \<lhd> r) (u \<lhd> r) \<Longrightarrow>
    1.56 +      (!!q. Unifier q (t \<lhd> r) (u \<lhd> r) \<Longrightarrow> s \<lozenge> q \<doteq> q) \<Longrightarrow>
    1.57 +    Idem (r \<lozenge> s)"
    1.58 +  apply (frule Unifier_Idem_subst, blast) 
    1.59 +  apply (force simp add: Idem_def subst_eq_def)
    1.60 +  done
    1.61 +
    1.62 +theorem unify_gives_Idem:
    1.63 +  "unify M N  = Some \<sigma> \<Longrightarrow> Idem \<sigma>"
    1.64 +proof (induct M N arbitrary: \<sigma> rule: unify.induct)
    1.65 +  case (7 M M' N N' \<sigma>)
    1.66 +
    1.67 +  then obtain \<theta>1 \<theta>2 
    1.68 +    where "unify M N = Some \<theta>1"
    1.69 +    and \<theta>2: "unify (M' \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
    1.70 +    and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
    1.71 +    and "Idem \<theta>1" 
    1.72 +    and "Idem \<theta>2"
    1.73 +    by (auto split: option.split_asm)
    1.74 +
    1.75 +  from \<theta>2 have "Unifier \<theta>2 (M' \<lhd> \<theta>1) (N' \<lhd> \<theta>1)"
    1.76 +    by (rule unify_computes_MGU[THEN MGU_is_Unifier])
    1.77 +
    1.78 +  with `Idem \<theta>1`
    1.79 +  show "Idem \<sigma>" unfolding \<sigma>
    1.80 +  proof (rule Idem_comp)
    1.81 +    fix \<sigma> assume "Unifier \<sigma> (M' \<lhd> \<theta>1) (N' \<lhd> \<theta>1)"
    1.82 +    with \<theta>2 obtain \<gamma> where \<sigma>: "\<sigma> \<doteq> \<theta>2 \<lozenge> \<gamma>"
    1.83 +      using unify_computes_MGU MGU_def by blast
    1.84 +
    1.85 +    have "\<theta>2 \<lozenge> \<sigma> \<doteq> \<theta>2 \<lozenge> (\<theta>2 \<lozenge> \<gamma>)" by (rule subst_cong) (auto simp: \<sigma>)
    1.86 +    also have "... \<doteq> (\<theta>2 \<lozenge> \<theta>2) \<lozenge> \<gamma>" by (rule comp_assoc[symmetric])
    1.87 +    also have "... \<doteq> \<theta>2 \<lozenge> \<gamma>" by (rule subst_cong) (auto simp: `Idem \<theta>2`[unfolded Idem_def])
    1.88 +    also have "... \<doteq> \<sigma>" by (rule \<sigma>[symmetric])
    1.89 +    finally show "\<theta>2 \<lozenge> \<sigma> \<doteq> \<sigma>" .
    1.90 +  qed
    1.91 +qed (auto intro!: Var_Idem split: option.splits if_splits)
    1.92  
    1.93  end