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