src/HOL/Lambda/Type.thy

   done
 
 
 text {* Iterated function types *}
 
-lemma list_app_typeD [rulified]:
+lemma list_app_typeD [rule_format]:
     "\<forall>t T. e |- t $$ ts : T --> (\<exists>Ts. e |- t : Ts =>> T \<and> types e ts Ts)"
   apply (induct_tac ts)
    apply simp
   apply (intro strip)
   apply simp

   apply (ind_cases "e |- t $ u : T")
   apply (rule_tac x = "Ta # Ts" in exI)
   apply simp
   done
 
-lemma list_app_typeI [rulified]:
+lemma list_app_typeI [rule_format]:
     "\<forall>t T Ts. e |- t : Ts =>> T --> types e ts Ts --> e |- t $$ ts : T"
   apply (induct_tac ts)
    apply (intro strip)
    apply simp
   apply (intro strip)

    apply (erule typing.App)
    apply assumption
   apply blast
   done
 
-lemma lists_types [rulified]:
+lemma lists_types [rule_format]:
     "\<forall>Ts. types e ts Ts --> ts \<in> lists {t. \<exists>T. e |- t : T}"
   apply (induct_tac ts)
    apply (intro strip)
    apply (case_tac Ts)
      apply simp

   done
 
 
 subsection {* Lifting preserves termination and well-typedness *}
 
-lemma lift_map [rulified, simp]:
+lemma lift_map [rule_format, simp]:
     "\<forall>t. lift (t $$ ts) i = lift t i $$ map (\<lambda>t. lift t i) ts"
   apply (induct_tac ts)
    apply simp_all
   done
 
-lemma subst_map [rulified, simp]:
+lemma subst_map [rule_format, simp]:
   "\<forall>t. subst (t $$ ts) u i = subst t u i $$ map (\<lambda>t. subst t u i) ts"
   apply (induct_tac ts)
    apply simp_all
   done
 
-lemma lift_IT [rulified, intro!]:
+lemma lift_IT [rule_format, intro!]:
     "t \<in> IT ==> \<forall>i. lift t i \<in> IT"
   apply (erule IT.induct)
     apply (rule allI)
     apply (simp (no_asm))
     apply (rule conjI)

        blast,
        assumption)+
      apply auto
    done
 
-lemma lifts_IT [rulified]:
+lemma lifts_IT [rule_format]:
     "ts \<in> lists IT --> map (\<lambda>t. lift t 0) ts \<in> lists IT"
   apply (induct_tac ts)
    apply auto
   done
 

    apply simp
   apply (case_tac nat)
    apply simp_all
   done
 
-lemma lift_type' [rulified]:
+lemma lift_type' [rule_format]:
   "e |- t : T ==> \<forall>i U.
     (\<lambda>j. if j < i then e j
           else if j = i then U
           else e (j - 1)) |- lift t i : T"
   apply (erule typing.induct)

   apply (rule ext)
   apply (case_tac j)
    apply simp_all
   done
 
-lemma lift_types [rulified]:
+lemma lift_types [rule_format]:
   "\<forall>Ts. types e ts Ts -->
     types (\<lambda>j. if j < i then e j
                 else if j = i then U
                 else e (j - 1)) (map (\<lambda>t. lift t i) ts) Ts"
   apply (induct_tac ts)

   done
 
 
 subsection {* Substitution lemmas *}
 
-lemma subst_lemma [rulified]:
+lemma subst_lemma [rule_format]:
   "e |- t : T ==> \<forall>e' i U u.
     e = (\<lambda>j. if j < i then e' j
               else if j = i then U
               else e' (j-1)) -->
     e' |- u : U --> e' |- t[u/i] : T"

     apply assumption
    apply fastsimp
   apply fastsimp
   done
 
-lemma substs_lemma [rulified]:
+lemma substs_lemma [rule_format]:
   "e |- u : T ==>
     \<forall>Ts. types (\<lambda>j. if j < i then e j
                      else if j = i then T else e (j - 1)) ts Ts -->
       types e (map (\<lambda>t. t[u/i]) ts) Ts"
   apply (induct_tac ts)

   done
 
 
 subsection {* Subject reduction *}
 
-lemma subject_reduction [rulified]:
+lemma subject_reduction [rule_format]:
     "e |- t : T ==> \<forall>t'. t -> t' --> e |- t' : T"
   apply (erule typing.induct)
     apply blast
    apply blast
   apply (intro strip)

 
 lemma app_last: "(t $$ ts) $ u = t $$ (ts @ [u])"
   apply simp
   done
 
-lemma subst_Var_IT [rulified]: "r \<in> IT ==> \<forall>i j. r[Var i/j] \<in> IT"
+lemma subst_Var_IT [rule_format]: "r \<in> IT ==> \<forall>i j. r[Var i/j] \<in> IT"
   apply (erule IT.induct)
     txt {* Case @{term Var}: *}
     apply (intro strip)
     apply (simp (no_asm) add: subst_Var)
     apply

   done
 
 
 subsection {* Well-typed substitution preserves termination *}
 
-lemma subst_type_IT [rulified]:
+lemma subst_type_IT [rule_format]:
   "\<forall>t. t \<in> IT --> (\<forall>e T u i.
     (\<lambda>j. if j < i then e j
           else if j = i then U
           else e (j - 1)) |- t : T -->
     u \<in> IT --> e |- u : U --> t[u/i] \<in> IT)"