--- a/src/HOL/Subst/UTerm.thy Wed Oct 03 00:03:01 2007 +0200
+++ b/src/HOL/Subst/UTerm.thy Wed Oct 03 19:36:05 2007 +0200
@@ -7,34 +7,31 @@
theory UTerm
imports Main
-
begin
text{*Binary trees with leaves that are constants or variables.*}
-datatype 'a uterm = Var 'a
- | Const 'a
- | Comb "'a uterm" "'a uterm"
+datatype 'a uterm =
+ Var 'a
+ | Const 'a
+ | Comb "'a uterm" "'a uterm"
-consts
- vars_of :: "'a uterm => 'a set"
- "<:" :: "'a uterm => 'a uterm => bool" (infixl 54)
- uterm_size :: "'a uterm => nat"
-
-syntax (xsymbols)
- "op <:" :: "'a uterm => 'a uterm => bool" (infixl "\<prec>" 54)
-
-
+consts vars_of :: "'a uterm => 'a set"
primrec
vars_of_Var: "vars_of (Var v) = {v}"
vars_of_Const: "vars_of (Const c) = {}"
vars_of_Comb: "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
+consts occs :: "'a uterm => 'a uterm => bool" (infixl "<:" 54)
+notation (xsymbols)
+ occs (infixl "\<prec>" 54)
primrec
occs_Var: "u \<prec> (Var v) = False"
occs_Const: "u \<prec> (Const c) = False"
occs_Comb: "u \<prec> (Comb M N) = (u=M | u=N | u \<prec> M | u \<prec> N)"
+consts
+ uterm_size :: "'a uterm => nat"
primrec
uterm_size_Var: "uterm_size (Var v) = 0"
uterm_size_Const: "uterm_size (Const c) = 0"
@@ -42,23 +39,22 @@
lemma vars_var_iff: "(v \<in> vars_of(Var(w))) = (w=v)"
-by auto
+ by auto
lemma vars_iff_occseq: "(x \<in> vars_of(t)) = (Var(x) \<prec> t | Var(x) = t)"
-by (induct_tac "t", auto)
+ by (induct t) auto
text{* Not used, but perhaps useful in other proofs *}
-lemma occs_vars_subset [rule_format]: "M\<prec>N --> vars_of(M) \<subseteq> vars_of(N)"
-by (induct_tac "N", auto)
+lemma occs_vars_subset: "M\<prec>N \<Longrightarrow> vars_of(M) \<subseteq> vars_of(N)"
+ by (induct N) auto
lemma monotone_vars_of:
- "vars_of M Un vars_of N \<subseteq> (vars_of M Un A) Un (vars_of N Un B)"
-by blast
+ "vars_of M Un vars_of N \<subseteq> (vars_of M Un A) Un (vars_of N Un B)"
+ by blast
lemma finite_vars_of: "finite(vars_of M)"
-by (induct_tac "M", auto)
-
+ by (induct M) auto
end