src/HOL/Subst/Unifier.ML
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 5278 a903b66822e2
permissions -rw-r--r--
import -> imports
paulson@3268
     1
(*  Title:      HOL/Subst/Unifier.ML
clasohm@1266
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Martin Coen, Cambridge University Computer Laboratory
clasohm@968
     4
    Copyright   1993  University of Cambridge
clasohm@968
     5
clasohm@968
     6
Properties of unifiers.
clasohm@968
     7
*)
clasohm@968
     8
clasohm@968
     9
open Unifier;
clasohm@968
    10
paulson@3192
    11
val unify_defs = [Unifier_def, MoreGeneral_def, MGUnifier_def];
paulson@3192
    12
paulson@3192
    13
(*---------------------------------------------------------------------------
paulson@3192
    14
 * Unifiers 
paulson@3192
    15
 *---------------------------------------------------------------------------*)
clasohm@968
    16
paulson@5278
    17
Goal "Unifier s (Comb t u) (Comb v w) = (Unifier s t v & Unifier s u w)";
wenzelm@4089
    18
by (simp_tac (simpset() addsimps [Unifier_def]) 1);
paulson@3192
    19
qed "Unifier_Comb";
clasohm@968
    20
paulson@3192
    21
AddIffs [Unifier_Comb];
clasohm@968
    22
paulson@5278
    23
Goal "[| v ~: vars_of t; v ~: vars_of u; Unifier s t u |] ==> \
nipkow@5119
    24
\  Unifier ((v,r)#s) t u";
wenzelm@4089
    25
by (asm_full_simp_tac (simpset() addsimps [Unifier_def, repl_invariance]) 1);
paulson@3192
    26
qed "Cons_Unifier";
paulson@3192
    27
clasohm@968
    28
paulson@3192
    29
(*---------------------------------------------------------------------------
paulson@3192
    30
 * Most General Unifiers 
paulson@3192
    31
 *---------------------------------------------------------------------------*)
clasohm@968
    32
wenzelm@5069
    33
Goalw unify_defs "MGUnifier s t u = MGUnifier s u t";
wenzelm@4089
    34
by (blast_tac (claset() addIs [sym]) 1);
paulson@3192
    35
qed "mgu_sym";
clasohm@968
    36
clasohm@968
    37
wenzelm@5069
    38
Goal  "[] >> s";
wenzelm@4089
    39
by (simp_tac (simpset() addsimps [MoreGeneral_def]) 1);
paulson@3192
    40
by (Blast_tac 1);
clasohm@968
    41
qed "MoreGen_Nil";
clasohm@968
    42
paulson@3192
    43
AddIffs [MoreGen_Nil];
clasohm@968
    44
wenzelm@5069
    45
Goalw unify_defs
paulson@3192
    46
    "MGUnifier s t u = (ALL r. Unifier r t u = s >> r)";
wenzelm@4089
    47
by (auto_tac (claset() addIs [ssubst_subst2, subst_comp_Nil], simpset()));
paulson@3192
    48
qed "MGU_iff";
paulson@2088
    49
paulson@2088
    50
paulson@5278
    51
Goal "~ Var v <: t ==> MGUnifier [(v,t)] (Var v) t";
wenzelm@4089
    52
by (simp_tac(simpset() addsimps [MGU_iff, Unifier_def, MoreGeneral_def]
paulson@3192
    53
	              delsimps [subst_Var]) 1);
paulson@3724
    54
by Safe_tac;
paulson@3457
    55
by (rtac exI 1);
paulson@3192
    56
by (etac subst 1 THEN rtac (Cons_trivial RS subst_sym) 1);
paulson@3192
    57
by (etac ssubst_subst2 1);
wenzelm@4089
    58
by (asm_simp_tac (simpset() addsimps [Var_not_occs]) 1);
paulson@3192
    59
qed "MGUnifier_Var";
clasohm@968
    60
paulson@3192
    61
AddSIs [MGUnifier_Var];
clasohm@968
    62
clasohm@968
    63
paulson@3192
    64
(*---------------------------------------------------------------------------
paulson@3192
    65
 * Idempotence.
paulson@3192
    66
 *---------------------------------------------------------------------------*)
clasohm@968
    67
wenzelm@5069
    68
Goalw [Idem_def] "Idem([])";
paulson@3192
    69
by (Simp_tac 1);
paulson@3192
    70
qed "Idem_Nil";
paulson@3192
    71
paulson@3192
    72
AddIffs [Idem_Nil];
paulson@3192
    73
wenzelm@5069
    74
Goalw [Idem_def] "Idem(s) = (sdom(s) Int srange(s) = {})";
wenzelm@4089
    75
by (simp_tac (simpset() addsimps [subst_eq_iff, invariance, 
paulson@3192
    76
				 dom_range_disjoint]) 1);
paulson@3192
    77
qed "Idem_iff";
clasohm@968
    78
wenzelm@5069
    79
Goal "~ (Var(v) <: t) --> Idem([(v,t)])";
wenzelm@4089
    80
by (simp_tac (simpset() addsimps [vars_iff_occseq, Idem_iff, srange_iff, 
oheimb@4719
    81
				  empty_iff_all_not]) 1);
paulson@3192
    82
qed_spec_mp "Var_Idem";
paulson@3192
    83
paulson@3192
    84
AddSIs [Var_Idem];
clasohm@968
    85
wenzelm@5069
    86
Goalw [Idem_def]
nipkow@5119
    87
  "[| Idem(r); Unifier s (t<|r) (u<|r) |] \
nipkow@5119
    88
\  ==> Unifier (r <> s) (t <| r) (u <| r)";
wenzelm@4089
    89
by (asm_full_simp_tac (simpset() addsimps [Unifier_def, comp_subst_subst]) 1);
paulson@3192
    90
qed "Unifier_Idem_subst";
paulson@3192
    91
paulson@3192
    92
val [idemr,unifier,minor] = goal Unifier.thy
paulson@3192
    93
     "[| Idem(r);  Unifier s (t <| r) (u <| r); \
paulson@3192
    94
\        !!q. Unifier q (t <| r) (u <| r) ==> s <> q =$= q \
paulson@3192
    95
\     |] ==> Idem(r <> s)";
paulson@3192
    96
by (cut_facts_tac [idemr,
paulson@3192
    97
                   unifier RS (idemr RS Unifier_Idem_subst RS minor)] 1);
wenzelm@4089
    98
by (asm_full_simp_tac (simpset() addsimps [Idem_def, subst_eq_iff]) 1);
paulson@3192
    99
qed "Idem_comp";