modernized specifications
authorhaftmann
Mon Jun 28 15:32:13 2010 +0200 (2010-06-28)
changeset 37597a02ea93e88c6
parent 37596 248db70c9bcf
child 37598 893dcabf0c04
modernized specifications
src/HOL/Bali/Trans.thy
src/HOL/Induct/Term.thy
src/HOL/Isar_Examples/Nested_Datatype.thy
     1.1 --- a/src/HOL/Bali/Trans.thy	Mon Jun 28 15:32:08 2010 +0200
     1.2 +++ b/src/HOL/Bali/Trans.thy	Mon Jun 28 15:32:13 2010 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  theory Trans imports Evaln begin
     1.5  
     1.6  definition groundVar :: "var \<Rightarrow> bool" where
     1.7 -"groundVar v \<equiv> (case v of
     1.8 +"groundVar v \<longleftrightarrow> (case v of
     1.9                     LVar ln \<Rightarrow> True
    1.10                   | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
    1.11                   | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
    1.12 @@ -35,19 +35,15 @@
    1.13  qed
    1.14  
    1.15  definition groundExprs :: "expr list \<Rightarrow> bool" where
    1.16 -"groundExprs es \<equiv> list_all (\<lambda> e. \<exists> v. e=Lit v) es"
    1.17 +  "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)"
    1.18    
    1.19 -consts the_val:: "expr \<Rightarrow> val"
    1.20 -primrec
    1.21 -"the_val (Lit v) = v"
    1.22 +primrec the_val:: "expr \<Rightarrow> val" where
    1.23 +  "the_val (Lit v) = v"
    1.24  
    1.25 -consts the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)"
    1.26 -primrec
    1.27 -"the_var G s (LVar ln)                    =(lvar ln (store s),s)"
    1.28 -the_var_FVar_def:
    1.29 -"the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
    1.30 -the_var_AVar_def:
    1.31 -"the_var G s(a.[i])                       =avar G (the_val i) (the_val a) s"
    1.32 +primrec the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)" where
    1.33 +  "the_var G s (LVar ln)                    =(lvar ln (store s),s)"
    1.34 +| the_var_FVar_def: "the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
    1.35 +| the_var_AVar_def: "the_var G s(a.[i])                       =avar G (the_val i) (the_val a) s"
    1.36  
    1.37  lemma the_var_FVar_simp[simp]:
    1.38  "the_var G s ({accC,statDeclC,stat}(Lit a)..fn) = fvar statDeclC stat fn a s"
     2.1 --- a/src/HOL/Induct/Term.thy	Mon Jun 28 15:32:08 2010 +0200
     2.2 +++ b/src/HOL/Induct/Term.thy	Mon Jun 28 15:32:13 2010 +0200
     2.3 @@ -13,18 +13,12 @@
     2.4  
     2.5  text {* \medskip Substitution function on terms *}
     2.6  
     2.7 -consts
     2.8 -  subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
     2.9 -  subst_term_list ::
    2.10 -    "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
    2.11 -
    2.12 -primrec
    2.13 +primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
    2.14 +  and subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" where
    2.15    "subst_term f (Var a) = f a"
    2.16 -  "subst_term f (App b ts) = App b (subst_term_list f ts)"
    2.17 -
    2.18 -  "subst_term_list f [] = []"
    2.19 -  "subst_term_list f (t # ts) =
    2.20 -     subst_term f t # subst_term_list f ts"
    2.21 +| "subst_term f (App b ts) = App b (subst_term_list f ts)"
    2.22 +| "subst_term_list f [] = []"
    2.23 +| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
    2.24  
    2.25  
    2.26  text {* \medskip A simple theorem about composition of substitutions *}
    2.27 @@ -41,9 +35,9 @@
    2.28  
    2.29  lemma
    2.30    assumes var: "!!v. P (Var v)"
    2.31 -    and app: "!!f ts. list_all P ts ==> P (App f ts)"
    2.32 +    and app: "!!f ts. (\<forall>t \<in> set ts. P t) ==> P (App f ts)"
    2.33    shows term_induct2: "P t"
    2.34 -    and "list_all P ts"
    2.35 +    and "\<forall>t \<in> set ts. P t"
    2.36    apply (induct t and ts)
    2.37       apply (rule var)
    2.38      apply (rule app)
     3.1 --- a/src/HOL/Isar_Examples/Nested_Datatype.thy	Mon Jun 28 15:32:08 2010 +0200
     3.2 +++ b/src/HOL/Isar_Examples/Nested_Datatype.thy	Mon Jun 28 15:32:13 2010 +0200
     3.3 @@ -10,17 +10,14 @@
     3.4      Var 'a
     3.5    | App 'b "('a, 'b) term list"
     3.6  
     3.7 -consts
     3.8 -  subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
     3.9 -  subst_term_list ::
    3.10 -    "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
    3.11 +primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" and
    3.12 +  subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" where
    3.13 +  "subst_term f (Var a) = f a"
    3.14 +| "subst_term f (App b ts) = App b (subst_term_list f ts)"
    3.15 +| "subst_term_list f [] = []"
    3.16 +| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
    3.17  
    3.18 -primrec (subst)
    3.19 -  "subst_term f (Var a) = f a"
    3.20 -  "subst_term f (App b ts) = App b (subst_term_list f ts)"
    3.21 -  "subst_term_list f [] = []"
    3.22 -  "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
    3.23 -
    3.24 +lemmas subst_simps = subst_term_subst_term_list.simps
    3.25  
    3.26  text {*
    3.27   \medskip A simple lemma about composition of substitutions.
    3.28 @@ -44,13 +41,13 @@
    3.29    next
    3.30      fix b ts assume "?Q ts"
    3.31      then show "?P (App b ts)"
    3.32 -      by (simp only: subst.simps)
    3.33 +      by (simp only: subst_simps)
    3.34    next
    3.35      show "?Q []" by simp
    3.36    next
    3.37      fix t ts
    3.38      assume "?P t" "?Q ts" then show "?Q (t # ts)"
    3.39 -      by (simp only: subst.simps)
    3.40 +      by (simp only: subst_simps)
    3.41    qed
    3.42  qed
    3.43  
    3.44 @@ -59,18 +56,18 @@
    3.45  
    3.46  theorem term_induct' [case_names Var App]:
    3.47    assumes var: "!!a. P (Var a)"
    3.48 -    and app: "!!b ts. list_all P ts ==> P (App b ts)"
    3.49 +    and app: "!!b ts. (\<forall>t \<in> set ts. P t) ==> P (App b ts)"
    3.50    shows "P t"
    3.51  proof (induct t)
    3.52    fix a show "P (Var a)" by (rule var)
    3.53  next
    3.54 -  fix b t ts assume "list_all P ts"
    3.55 +  fix b t ts assume "\<forall>t \<in> set ts. P t"
    3.56    then show "P (App b ts)" by (rule app)
    3.57  next
    3.58 -  show "list_all P []" by simp
    3.59 +  show "\<forall>t \<in> set []. P t" by simp
    3.60  next
    3.61 -  fix t ts assume "P t" "list_all P ts"
    3.62 -  then show "list_all P (t # ts)" by simp
    3.63 +  fix t ts assume "P t" "\<forall>t' \<in> set ts. P t'"
    3.64 +  then show "\<forall>t' \<in> set (t # ts). P t'" by simp
    3.65  qed
    3.66  
    3.67  lemma