--- a/src/HOL/Bali/Trans.thy Mon Jun 28 15:32:08 2010 +0200
+++ b/src/HOL/Bali/Trans.thy Mon Jun 28 15:32:13 2010 +0200
@@ -10,7 +10,7 @@
theory Trans imports Evaln begin
definition groundVar :: "var \<Rightarrow> bool" where
-"groundVar v \<equiv> (case v of
+"groundVar v \<longleftrightarrow> (case v of
LVar ln \<Rightarrow> True
| {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
| e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
@@ -35,19 +35,15 @@
qed
definition groundExprs :: "expr list \<Rightarrow> bool" where
-"groundExprs es \<equiv> list_all (\<lambda> e. \<exists> v. e=Lit v) es"
+ "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)"
-consts the_val:: "expr \<Rightarrow> val"
-primrec
-"the_val (Lit v) = v"
+primrec the_val:: "expr \<Rightarrow> val" where
+ "the_val (Lit v) = v"
-consts the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)"
-primrec
-"the_var G s (LVar ln) =(lvar ln (store s),s)"
-the_var_FVar_def:
-"the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
-the_var_AVar_def:
-"the_var G s(a.[i]) =avar G (the_val i) (the_val a) s"
+primrec the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)" where
+ "the_var G s (LVar ln) =(lvar ln (store s),s)"
+| the_var_FVar_def: "the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
+| the_var_AVar_def: "the_var G s(a.[i]) =avar G (the_val i) (the_val a) s"
lemma the_var_FVar_simp[simp]:
"the_var G s ({accC,statDeclC,stat}(Lit a)..fn) = fvar statDeclC stat fn a s"
--- a/src/HOL/Induct/Term.thy Mon Jun 28 15:32:08 2010 +0200
+++ b/src/HOL/Induct/Term.thy Mon Jun 28 15:32:13 2010 +0200
@@ -13,18 +13,12 @@
text {* \medskip Substitution function on terms *}
-consts
- subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
- subst_term_list ::
- "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
-
-primrec
+primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
+ and subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" where
"subst_term f (Var a) = f a"
- "subst_term f (App b ts) = App b (subst_term_list f ts)"
-
- "subst_term_list f [] = []"
- "subst_term_list f (t # ts) =
- subst_term f t # subst_term_list f ts"
+| "subst_term f (App b ts) = App b (subst_term_list f ts)"
+| "subst_term_list f [] = []"
+| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
text {* \medskip A simple theorem about composition of substitutions *}
@@ -41,9 +35,9 @@
lemma
assumes var: "!!v. P (Var v)"
- and app: "!!f ts. list_all P ts ==> P (App f ts)"
+ and app: "!!f ts. (\<forall>t \<in> set ts. P t) ==> P (App f ts)"
shows term_induct2: "P t"
- and "list_all P ts"
+ and "\<forall>t \<in> set ts. P t"
apply (induct t and ts)
apply (rule var)
apply (rule app)
--- a/src/HOL/Isar_Examples/Nested_Datatype.thy Mon Jun 28 15:32:08 2010 +0200
+++ b/src/HOL/Isar_Examples/Nested_Datatype.thy Mon Jun 28 15:32:13 2010 +0200
@@ -10,17 +10,14 @@
Var 'a
| App 'b "('a, 'b) term list"
-consts
- subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
- subst_term_list ::
- "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
+primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" and
+ subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" where
+ "subst_term f (Var a) = f a"
+| "subst_term f (App b ts) = App b (subst_term_list f ts)"
+| "subst_term_list f [] = []"
+| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
-primrec (subst)
- "subst_term f (Var a) = f a"
- "subst_term f (App b ts) = App b (subst_term_list f ts)"
- "subst_term_list f [] = []"
- "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
-
+lemmas subst_simps = subst_term_subst_term_list.simps
text {*
\medskip A simple lemma about composition of substitutions.
@@ -44,13 +41,13 @@
next
fix b ts assume "?Q ts"
then show "?P (App b ts)"
- by (simp only: subst.simps)
+ by (simp only: subst_simps)
next
show "?Q []" by simp
next
fix t ts
assume "?P t" "?Q ts" then show "?Q (t # ts)"
- by (simp only: subst.simps)
+ by (simp only: subst_simps)
qed
qed
@@ -59,18 +56,18 @@
theorem term_induct' [case_names Var App]:
assumes var: "!!a. P (Var a)"
- and app: "!!b ts. list_all P ts ==> P (App b ts)"
+ and app: "!!b ts. (\<forall>t \<in> set ts. P t) ==> P (App b ts)"
shows "P t"
proof (induct t)
fix a show "P (Var a)" by (rule var)
next
- fix b t ts assume "list_all P ts"
+ fix b t ts assume "\<forall>t \<in> set ts. P t"
then show "P (App b ts)" by (rule app)
next
- show "list_all P []" by simp
+ show "\<forall>t \<in> set []. P t" by simp
next
- fix t ts assume "P t" "list_all P ts"
- then show "list_all P (t # ts)" by simp
+ fix t ts assume "P t" "\<forall>t' \<in> set ts. P t'"
+ then show "\<forall>t' \<in> set (t # ts). P t'" by simp
qed
lemma