src/HOL/W0/W.ML

 
 Addsimps [Suc_le_lessD];
 Delsimps (ex_simps @ all_simps);
 
 (* correctness of W with respect to has_type *)
-goal W.thy
+Goal
         "!a s t m n . Ok (s,t,m) = W e a n --> $s a |- e :: t";
 by (expr.induct_tac "e" 1);
 (* case Var n *)
 by (Asm_simp_tac 1);
 (* case Abs e *)

 val has_type_casesE = map(has_type.mk_cases expr.simps)
         [" s |- Var n :: t"," s |- Abs e :: t","s |- App e1 e2 ::t"];
 
 
 (* the resulting type variable is always greater or equal than the given one *)
-goal thy
+Goal
         "!a n s t m. W e a n  = Ok (s,t,m) --> n<=m";
 by (expr.induct_tac "e" 1);
 (* case Var(n) *)
 by (fast_tac (HOL_cs addss simpset()) 1);
 (* case Abs e *)

 by (Asm_simp_tac 1);
 qed_spec_mp "W_var_ge";
 
 Addsimps [W_var_ge];
 
-goal thy
+Goal
         "!! s. Ok (s,t,m) = W e a n ==> n<=m";
 by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
 qed "W_var_geD";
 
 

 by ( simp_tac (simpset() addsimps [eq_sym_conv]) 1);
 qed "rotate_Ok";
 
 
 (* resulting type variable is new *)
-goal thy
+Goal
      "!n a s t m. new_tv n a --> W e a n = Ok (s,t,m) -->    \
 \                 new_tv m s & new_tv m t";
 by (expr.induct_tac "e" 1);
 (* case Var n *)
 by (fast_tac (HOL_cs addDs [list_all_nth] addss (simpset() 

                      addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le]
                      addss (simpset())) 1);
 qed_spec_mp "new_tv_W";
 
 
-goal thy
+Goal
      "!n a s t m v. W e a n = Ok (s,t,m) -->            \
 \         (v:free_tv s | v:free_tv t) --> v<n --> v:free_tv a";
 by (expr.induct_tac "e" 1);
 (* case Var n *)
 by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list] 

                      addSEs [UnE]
                      addss simpset()) 1); 
 qed_spec_mp "free_tv_W"; 
 
 (* Completeness of W w.r.t. has_type *)
-goal thy
+Goal
  "!s' a t' n. $s' a |- e :: t' --> new_tv n a -->     \
 \             (? s t. (? m. W e a n = Ok (s,t,m)) &  \
 \                     (? r. $s' a = $r ($s a) & t' = $r t))";
 by (expr.induct_tac "e" 1);
 (* case Var n *)

        addss ((simpset() addsimps [free_tv_subst,dom_def]))) 1);
 (** LEVEL 106 **)
 by (Fast_tac 1);
 qed_spec_mp "W_complete_lemma";
 
-goal W.thy
+Goal
  "!!e. [] |- e :: t' ==>  (? s t. (? m. W e [] n = Ok(s,t,m)) &  \
 \                                 (? r. t' = $r t))";
 by (cut_inst_tac [("a","[]"),("s'","id_subst"),("e","e"),("t'","t'")]
                 W_complete_lemma 1);
 by (ALLGOALS Asm_full_simp_tac);