# HG changeset patch
# User haftmann
# Date 1277731933 -7200
# Node ID a02ea93e88c6a3944beb49b3384cd031782e9897
# Parent  248db70c9bcff1ffb777e24ba018d35a4b7e6424
modernized specifications

diff -r 248db70c9bcf -r a02ea93e88c6 src/HOL/Bali/Trans.thy
--- 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"
diff -r 248db70c9bcf -r a02ea93e88c6 src/HOL/Induct/Term.thy
--- 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)
diff -r 248db70c9bcf -r a02ea93e88c6 src/HOL/Isar_Examples/Nested_Datatype.thy
--- 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