author | bulwahn |
Fri, 11 Mar 2011 15:21:13 +0100 | |
changeset 41919 | e180c2a9873b |
parent 38140 | 05691ad74079 |
permissions | -rw-r--r-- |
38140 | 1 |
(* Title: HOL/Subst/UTerm.thy |
1476 | 2 |
Author: Martin Coen, Cambridge University Computer Laboratory |
968 | 3 |
Copyright 1993 University of Cambridge |
4 |
*) |
|
5 |
||
38140 | 6 |
header {* Simple Term Structure for Unification *} |
15635 | 7 |
|
8 |
theory UTerm |
|
9 |
imports Main |
|
10 |
begin |
|
11 |
||
38140 | 12 |
text {* Binary trees with leaves that are constants or variables. *} |
15635 | 13 |
|
24823 | 14 |
datatype 'a uterm = |
15 |
Var 'a |
|
16 |
| Const 'a |
|
17 |
| Comb "'a uterm" "'a uterm" |
|
968 | 18 |
|
38140 | 19 |
primrec vars_of :: "'a uterm => 'a set" |
20 |
where |
|
15635 | 21 |
vars_of_Var: "vars_of (Var v) = {v}" |
38140 | 22 |
| vars_of_Const: "vars_of (Const c) = {}" |
23 |
| vars_of_Comb: "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))" |
|
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
24 |
|
38140 | 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 |
||
24823 | 31 |
notation (xsymbols) |
32 |
occs (infixl "\<prec>" 54) |
|
968 | 33 |
|
38140 | 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)" |
|
15635 | 39 |
|
40 |
||
38140 | 41 |
lemma vars_var_iff: "(v \<in> vars_of (Var w)) = (w = v)" |
24823 | 42 |
by auto |
15635 | 43 |
|
38140 | 44 |
lemma vars_iff_occseq: "(x \<in> vars_of t) = (Var x \<prec> t | Var x = t)" |
24823 | 45 |
by (induct t) auto |
15635 | 46 |
|
968 | 47 |
|
15648 | 48 |
text{* Not used, but perhaps useful in other proofs *} |
38140 | 49 |
lemma occs_vars_subset: "M \<prec> N \<Longrightarrow> vars_of M \<subseteq> vars_of N" |
24823 | 50 |
by (induct N) auto |
15635 | 51 |
|
52 |
||
15648 | 53 |
lemma monotone_vars_of: |
24823 | 54 |
"vars_of M Un vars_of N \<subseteq> (vars_of M Un A) Un (vars_of N Un B)" |
55 |
by blast |
|
15635 | 56 |
|
38140 | 57 |
lemma finite_vars_of: "finite (vars_of M)" |
24823 | 58 |
by (induct M) auto |
968 | 59 |
|
60 |
end |