--- a/src/HOL/Induct/QuoNestedDataType.thy Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Induct/QuoNestedDataType.thy Fri Nov 17 02:20:03 2006 +0100
@@ -21,7 +21,7 @@
consts exprel :: "(freeExp * freeExp) set"
abbreviation
- exp_rel :: "[freeExp, freeExp] => bool" (infixl "~~" 50)
+ exp_rel :: "[freeExp, freeExp] => bool" (infixl "~~" 50) where
"X ~~ Y == (X,Y) \<in> exprel"
notation (xsymbols)
@@ -160,14 +160,16 @@
text{*The abstract message constructors*}
definition
- Var :: "nat \<Rightarrow> exp"
+ Var :: "nat \<Rightarrow> exp" where
"Var N = Abs_Exp(exprel``{VAR N})"
- Plus :: "[exp,exp] \<Rightarrow> exp"
+definition
+ Plus :: "[exp,exp] \<Rightarrow> exp" where
"Plus X Y =
Abs_Exp (\<Union>U \<in> Rep_Exp X. \<Union>V \<in> Rep_Exp Y. exprel``{PLUS U V})"
- FnCall :: "[nat, exp list] \<Rightarrow> exp"
+definition
+ FnCall :: "[nat, exp list] \<Rightarrow> exp" where
"FnCall F Xs =
Abs_Exp (\<Union>Us \<in> listset (map Rep_Exp Xs). exprel `` {FNCALL F Us})"
@@ -207,7 +209,7 @@
list of concrete expressions*}
definition
- Abs_ExpList :: "freeExp list => exp list"
+ Abs_ExpList :: "freeExp list => exp list" where
"Abs_ExpList Xs = map (%U. Abs_Exp(exprel``{U})) Xs"
lemma Abs_ExpList_Nil [simp]: "Abs_ExpList [] == []"
@@ -285,7 +287,7 @@
subsection{*The Abstract Function to Return the Set of Variables*}
definition
- vars :: "exp \<Rightarrow> nat set"
+ vars :: "exp \<Rightarrow> nat set" where
"vars X = (\<Union>U \<in> Rep_Exp X. freevars U)"
lemma vars_respects: "freevars respects exprel"
@@ -351,7 +353,7 @@
subsection{*Injectivity of @{term FnCall}*}
definition
- "fun" :: "exp \<Rightarrow> nat"
+ "fun" :: "exp \<Rightarrow> nat" where
"fun X = contents (\<Union>U \<in> Rep_Exp X. {freefun U})"
lemma fun_respects: "(%U. {freefun U}) respects exprel"
@@ -363,7 +365,7 @@
done
definition
- args :: "exp \<Rightarrow> exp list"
+ args :: "exp \<Rightarrow> exp list" where
"args X = contents (\<Union>U \<in> Rep_Exp X. {Abs_ExpList (freeargs U)})"
text{*This result can probably be generalized to arbitrary equivalence
@@ -398,7 +400,7 @@
function in order to prove discrimination theorems.*}
definition
- discrim :: "exp \<Rightarrow> int"
+ discrim :: "exp \<Rightarrow> int" where
"discrim X = contents (\<Union>U \<in> Rep_Exp X. {freediscrim U})"
lemma discrim_respects: "(\<lambda>U. {freediscrim U}) respects exprel"