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