src/HOL/Subst/UTerm.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;
     1 (*  ID:         $Id$
     2     Author:     Martin Coen, Cambridge University Computer Laboratory
     3     Copyright   1993  University of Cambridge
     4 *)
     5 
     6 header{*Simple Term Structure for Unification*}
     7 
     8 theory UTerm
     9 imports Main
    10 begin
    11 
    12 text{*Binary trees with leaves that are constants or variables.*}
    13 
    14 datatype 'a uterm =
    15     Var 'a
    16   | Const 'a
    17   | Comb "'a uterm" "'a uterm"
    18 
    19 consts vars_of :: "'a uterm => 'a set"
    20 primrec
    21   vars_of_Var:   "vars_of (Var v) = {v}"
    22   vars_of_Const: "vars_of (Const c) = {}"
    23   vars_of_Comb:  "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
    24 
    25 consts occs :: "'a uterm => 'a uterm => bool"   (infixl "<:" 54) 
    26 notation (xsymbols)
    27   occs  (infixl "\<prec>" 54)
    28 primrec
    29   occs_Var:   "u \<prec> (Var v) = False"
    30   occs_Const: "u \<prec> (Const c) = False"
    31   occs_Comb:  "u \<prec> (Comb M N) = (u=M | u=N | u \<prec> M | u \<prec> N)"
    32 
    33 consts
    34   uterm_size ::  "'a uterm => nat"
    35 primrec
    36   uterm_size_Var:   "uterm_size (Var v) = 0"
    37   uterm_size_Const: "uterm_size (Const c) = 0"
    38   uterm_size_Comb:  "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)"
    39 
    40 
    41 lemma vars_var_iff: "(v \<in> vars_of(Var(w))) = (w=v)"
    42   by auto
    43 
    44 lemma vars_iff_occseq: "(x \<in> vars_of(t)) = (Var(x) \<prec> t | Var(x) = t)"
    45   by (induct t) auto
    46 
    47 
    48 text{* Not used, but perhaps useful in other proofs *}
    49 lemma occs_vars_subset: "M\<prec>N \<Longrightarrow> vars_of(M) \<subseteq> vars_of(N)"
    50   by (induct N) auto
    51 
    52 
    53 lemma monotone_vars_of:
    54     "vars_of M Un vars_of N \<subseteq> (vars_of M Un A) Un (vars_of N Un B)"
    55   by blast
    56 
    57 lemma finite_vars_of: "finite(vars_of M)"
    58   by (induct M) auto
    59 
    60 end