inductive: no collective atts;
authorwenzelm
Fri Sep 28 21:45:11 2001 +0200 (2001-09-28)
changeset 116382c3dee321b4b
parent 11637 647e6c84323c
child 11639 4213422388c4
inductive: no collective atts;
src/HOL/Lambda/Eta.thy
src/HOL/Lambda/Lambda.thy
src/HOL/Lambda/ParRed.thy
src/HOL/Lambda/Type.thy
     1.1 --- a/src/HOL/Lambda/Eta.thy	Fri Sep 28 20:09:10 2001 +0200
     1.2 +++ b/src/HOL/Lambda/Eta.thy	Fri Sep 28 21:45:11 2001 +0200
     1.3 @@ -31,11 +31,11 @@
     1.4    "s -e>= t" == "(s, t) \<in> eta^="
     1.5  
     1.6  inductive eta
     1.7 -  intros [simp, intro]
     1.8 -    eta: "\<not> free s 0 ==> Abs (s $ Var 0) -e> s[dummy/0]"
     1.9 -    appL: "s -e> t ==> s $ u -e> t $ u"
    1.10 -    appR: "s -e> t ==> u $ s -e> u $ t"
    1.11 -    abs: "s -e> t ==> Abs s -e> Abs t"
    1.12 +  intros
    1.13 +    eta [simp, intro]: "\<not> free s 0 ==> Abs (s $ Var 0) -e> s[dummy/0]"
    1.14 +    appL [simp, intro]: "s -e> t ==> s $ u -e> t $ u"
    1.15 +    appR [simp, intro]: "s -e> t ==> u $ s -e> u $ t"
    1.16 +    abs [simp, intro]: "s -e> t ==> Abs s -e> Abs t"
    1.17  
    1.18  inductive_cases eta_cases [elim!]:
    1.19    "Abs s -e> z"
    1.20 @@ -249,4 +249,4 @@
    1.21    apply (auto simp add: not_free_iff_lifted)
    1.22    done
    1.23  
    1.24 -end
    1.25 \ No newline at end of file
    1.26 +end
     2.1 --- a/src/HOL/Lambda/Lambda.thy	Fri Sep 28 20:09:10 2001 +0200
     2.2 +++ b/src/HOL/Lambda/Lambda.thy	Fri Sep 28 21:45:11 2001 +0200
     2.3 @@ -64,11 +64,11 @@
     2.4    "s ->> t" == "(s, t) \<in> beta^*"
     2.5  
     2.6  inductive beta
     2.7 -  intros [simp, intro!]
     2.8 -    beta: "Abs s $ t -> s[t/0]"
     2.9 -    appL: "s -> t ==> s $ u -> t $ u"
    2.10 -    appR: "s -> t ==> u $ s -> u $ t"
    2.11 -    abs: "s -> t ==> Abs s -> Abs t"
    2.12 +  intros
    2.13 +    beta [simp, intro!]: "Abs s $ t -> s[t/0]"
    2.14 +    appL [simp, intro!]: "s -> t ==> s $ u -> t $ u"
    2.15 +    appR [simp, intro!]: "s -> t ==> u $ s -> u $ t"
    2.16 +    abs [simp, intro!]: "s -> t ==> Abs s -> Abs t"
    2.17  
    2.18  inductive_cases beta_cases [elim!]:
    2.19    "Var i -> t"
    2.20 @@ -203,4 +203,4 @@
    2.21    apply (simp add: rtrancl_beta_Abs)
    2.22    done
    2.23  
    2.24 -end
    2.25 \ No newline at end of file
    2.26 +end
     3.1 --- a/src/HOL/Lambda/ParRed.thy	Fri Sep 28 20:09:10 2001 +0200
     3.2 +++ b/src/HOL/Lambda/ParRed.thy	Fri Sep 28 21:45:11 2001 +0200
     3.3 @@ -23,11 +23,11 @@
     3.4    "s => t" == "(s, t) \<in> par_beta"
     3.5  
     3.6  inductive par_beta
     3.7 -  intros [simp, intro!]
     3.8 -    var: "Var n => Var n"
     3.9 -    abs: "s => t ==> Abs s => Abs t"
    3.10 -    app: "[| s => s'; t => t' |] ==> s $ t => s' $ t'"
    3.11 -    beta: "[| s => s'; t => t' |] ==> (Abs s) $ t => s'[t'/0]"
    3.12 +  intros
    3.13 +    var [simp, intro!]: "Var n => Var n"
    3.14 +    abs [simp, intro!]: "s => t ==> Abs s => Abs t"
    3.15 +    app [simp, intro!]: "[| s => s'; t => t' |] ==> s $ t => s' $ t'"
    3.16 +    beta [simp, intro!]: "[| s => s'; t => t' |] ==> (Abs s) $ t => s'[t'/0]"
    3.17  
    3.18  inductive_cases par_beta_cases [elim!]:
    3.19    "Var n => t"
    3.20 @@ -130,4 +130,4 @@
    3.21      par_beta_subset_beta beta_subset_par_beta)+
    3.22    done
    3.23  
    3.24 -end
    3.25 \ No newline at end of file
    3.26 +end
     4.1 --- a/src/HOL/Lambda/Type.thy	Fri Sep 28 20:09:10 2001 +0200
     4.2 +++ b/src/HOL/Lambda/Type.thy	Fri Sep 28 21:45:11 2001 +0200
     4.3 @@ -32,10 +32,10 @@
     4.4    "Ts =>> T" == "foldr Fun Ts T"
     4.5  
     4.6  inductive typing
     4.7 -  intros [intro!]
     4.8 -    Var: "env x = T ==> env |- Var x : T"
     4.9 -    Abs: "(nat_case T env) |- t : U ==> env |- Abs t : (T => U)"
    4.10 -    App: "env |- s : T => U ==> env |- t : T ==> env |- (s $ t) : U"
    4.11 +  intros
    4.12 +    Var [intro!]: "env x = T ==> env |- Var x : T"
    4.13 +    Abs [intro!]: "(nat_case T env) |- t : U ==> env |- Abs t : (T => U)"
    4.14 +    App [intro!]: "env |- s : T => U ==> env |- t : T ==> env |- (s $ t) : U"
    4.15  
    4.16  inductive_cases [elim!]:
    4.17    "e |- Var i : T"
    4.18 @@ -466,4 +466,4 @@
    4.19    apply (erule type_implies_IT)
    4.20    done
    4.21  
    4.22 -end
    4.23 \ No newline at end of file
    4.24 +end