src/HOL/Subst/UTerm.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/UTerm.thy
     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 primrec vars_of :: "'a uterm => 'a set"
    20 where
    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 primrec occs :: "'a uterm => 'a uterm => bool"   (infixl "<:" 54) 
    26 where
    27   occs_Var: "u <: (Var v) = False"
    28 | occs_Const: "u <: (Const c) = False"
    29 | occs_Comb: "u <: (Comb M N) = (u = M | u = N | u <: M | u <: N)"
    30 
    31 notation (xsymbols)
    32   occs  (infixl "\<prec>" 54)
    33 
    34 primrec uterm_size ::  "'a uterm => nat"
    35 where
    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