src/HOL/Subst/Unifier.thy
author wenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549 d2d7874648bd
parent 24823 bfb619994060
child 38140 05691ad74079
permissions -rw-r--r--
simplified method setup;
paulson@15635
     1
(*  ID:         $Id$
clasohm@1476
     2
    Author:     Martin Coen, Cambridge University Computer Laboratory
clasohm@968
     3
    Copyright   1993  University of Cambridge
clasohm@968
     4
clasohm@968
     5
*)
clasohm@968
     6
paulson@15635
     7
header{*Definition of Most General Unifier*}
paulson@15635
     8
paulson@15635
     9
theory Unifier
paulson@15635
    10
imports Subst
paulson@15635
    11
begin
clasohm@968
    12
wenzelm@24823
    13
definition
wenzelm@24823
    14
  Unifier   :: "[('a * 'a uterm)list, 'a uterm, 'a uterm] => bool" where
wenzelm@24823
    15
  "Unifier s t u \<longleftrightarrow> t <| s = u <| s"
clasohm@968
    16
wenzelm@24823
    17
definition
wenzelm@24823
    18
  MoreGeneral :: "[('a * 'a uterm)list, ('a * 'a uterm)list] => bool" (infixr ">>" 52) where
wenzelm@24823
    19
  "r >> s \<longleftrightarrow> (\<exists>q. s =$= r <> q)"
clasohm@968
    20
wenzelm@24823
    21
definition
wenzelm@24823
    22
  MGUnifier :: "[('a * 'a uterm)list, 'a uterm, 'a uterm] => bool" where
wenzelm@24823
    23
  "MGUnifier s t u \<longleftrightarrow> Unifier s t u & (\<forall>r. Unifier r t u --> s >> r)"
clasohm@968
    24
wenzelm@24823
    25
definition
wenzelm@24823
    26
  Idem :: "('a * 'a uterm)list => bool" where
wenzelm@24823
    27
  "Idem s \<longleftrightarrow> (s <> s) =$= s"
paulson@15635
    28
paulson@15635
    29
paulson@15635
    30
lemmas unify_defs = Unifier_def MoreGeneral_def MGUnifier_def
paulson@15635
    31
paulson@15635
    32
paulson@15635
    33
subsection{*Unifiers*}
paulson@15635
    34
paulson@15635
    35
lemma Unifier_Comb [iff]: "Unifier s (Comb t u) (Comb v w) = (Unifier s t v & Unifier s u w)"
wenzelm@24823
    36
  by (simp add: Unifier_def)
paulson@15635
    37
paulson@15635
    38
paulson@15635
    39
lemma Cons_Unifier: "[| v ~: vars_of t; v ~: vars_of u; Unifier s t u |] ==> Unifier ((v,r)#s) t u"
wenzelm@24823
    40
  by (simp add: Unifier_def repl_invariance)
paulson@15635
    41
paulson@15635
    42
paulson@15635
    43
subsection{* Most General Unifiers*}
paulson@15635
    44
paulson@15635
    45
lemma mgu_sym: "MGUnifier s t u = MGUnifier s u t"
wenzelm@24823
    46
  by (simp add: unify_defs eq_commute)
paulson@15635
    47
paulson@15635
    48
paulson@15635
    49
lemma MoreGen_Nil [iff]: "[] >> s"
wenzelm@24823
    50
  by (auto simp add: MoreGeneral_def)
paulson@15635
    51
paulson@15635
    52
lemma MGU_iff: "MGUnifier s t u = (ALL r. Unifier r t u = s >> r)"
wenzelm@24823
    53
  apply (unfold unify_defs)
wenzelm@24823
    54
  apply (auto intro: ssubst_subst2 subst_comp_Nil)
wenzelm@24823
    55
  done
paulson@15635
    56
wenzelm@24823
    57
lemma MGUnifier_Var [intro!]: "~ Var v <: t ==> MGUnifier [(v,t)] (Var v) t"
wenzelm@24823
    58
  apply (simp (no_asm) add: MGU_iff Unifier_def MoreGeneral_def del: subst_Var)
wenzelm@24823
    59
  apply safe
wenzelm@24823
    60
   apply (rule exI)
wenzelm@24823
    61
   apply (erule subst, rule Cons_trivial [THEN subst_sym])
wenzelm@24823
    62
  apply (erule ssubst_subst2)
wenzelm@24823
    63
  apply (simp (no_asm_simp) add: Var_not_occs)
wenzelm@24823
    64
  done
paulson@15635
    65
paulson@15635
    66
paulson@15635
    67
subsection{*Idempotence*}
paulson@15635
    68
paulson@15635
    69
lemma Idem_Nil [iff]: "Idem([])"
wenzelm@24823
    70
  by (simp add: Idem_def)
paulson@15635
    71
paulson@15635
    72
lemma Idem_iff: "Idem(s) = (sdom(s) Int srange(s) = {})"
wenzelm@24823
    73
  by (simp add: Idem_def subst_eq_iff invariance dom_range_disjoint)
paulson@15635
    74
paulson@15635
    75
lemma Var_Idem [intro!]: "~ (Var(v) <: t) ==> Idem([(v,t)])"
wenzelm@24823
    76
  by (simp add: vars_iff_occseq Idem_iff srange_iff empty_iff_all_not)
paulson@15635
    77
paulson@15635
    78
lemma Unifier_Idem_subst: 
paulson@15635
    79
  "[| Idem(r); Unifier s (t<|r) (u<|r) |]  
wenzelm@24823
    80
    ==> Unifier (r <> s) (t <| r) (u <| r)"
wenzelm@24823
    81
  by (simp add: Idem_def Unifier_def comp_subst_subst)
paulson@15635
    82
paulson@15635
    83
lemma Idem_comp:
wenzelm@24823
    84
  "[| Idem(r);  Unifier s (t <| r) (u <| r);  
wenzelm@24823
    85
      !!q. Unifier q (t <| r) (u <| r) ==> s <> q =$= q  
wenzelm@24823
    86
    |] ==> Idem(r <> s)"
wenzelm@24823
    87
  apply (frule Unifier_Idem_subst, blast) 
wenzelm@24823
    88
  apply (force simp add: Idem_def subst_eq_iff)
wenzelm@24823
    89
  done
paulson@15635
    90
clasohm@968
    91
end