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