src/CCL/Type.ML
changeset 757 2ca12511676d
parent 642 0db578095e6a
child 1087 c1ccf6679a96
     1.1 --- a/src/CCL/Type.ML	Wed Nov 30 13:18:42 1994 +0100
     1.2 +++ b/src/CCL/Type.ML	Wed Nov 30 13:53:46 1994 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4  
     1.5  goal Set.thy "A <= B <-> (ALL x.x:A --> x:B)";
     1.6  by (fast_tac set_cs 1);
     1.7 -val subsetXH = result();
     1.8 +qed "subsetXH";
     1.9  
    1.10  (*** Exhaustion Rules ***)
    1.11  
    1.12 @@ -99,22 +99,22 @@
    1.13  val prems = goal Type.thy
    1.14       "[| a:A;  P(a) |] ==> a : {x:A. P(x)}";
    1.15  by (REPEAT (resolve_tac (prems@[SubtypeXH RS iffD2,conjI]) 1));
    1.16 -val SubtypeI = result();
    1.17 +qed "SubtypeI";
    1.18  
    1.19  val prems = goal Type.thy
    1.20       "[| a : {x:A. P(x)};  [| a:A;  P(a) |] ==> Q |] ==> Q";
    1.21  by (REPEAT (resolve_tac (prems@[SubtypeD1,SubtypeD2]) 1));
    1.22 -val SubtypeE = result();
    1.23 +qed "SubtypeE";
    1.24  
    1.25  (*** Monotonicity ***)
    1.26  
    1.27  goal Type.thy "mono (%X.X)";
    1.28  by (REPEAT (ares_tac [monoI] 1));
    1.29 -val idM = result();
    1.30 +qed "idM";
    1.31  
    1.32  goal Type.thy "mono(%X.A)";
    1.33  by (REPEAT (ares_tac [monoI,subset_refl] 1));
    1.34 -val constM = result();
    1.35 +qed "constM";
    1.36  
    1.37  val major::prems = goal Type.thy
    1.38      "mono(%X.A(X)) ==> mono(%X.[A(X)])";
    1.39 @@ -125,7 +125,7 @@
    1.40  by (rtac (disjI2 RS (LiftXH RS iffD2)) 1);
    1.41  by (etac (major RS monoD RS subsetD) 1);
    1.42  by (assume_tac 1);
    1.43 -val LiftM = result();
    1.44 +qed "LiftM";
    1.45  
    1.46  val prems = goal Type.thy
    1.47      "[| mono(%X.A(X)); !!x X. x:A(X) ==> mono(%X.B(X,x)) |] ==> \
    1.48 @@ -134,7 +134,7 @@
    1.49              eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
    1.50              (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
    1.51              hyp_subst_tac 1));
    1.52 -val SgM = result();
    1.53 +qed "SgM";
    1.54  
    1.55  val prems = goal Type.thy
    1.56      "[| !!x. x:A ==> mono(%X.B(X,x)) |] ==> mono(%X.Pi(A,B(X)))";
    1.57 @@ -142,7 +142,7 @@
    1.58              eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
    1.59              (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
    1.60              hyp_subst_tac 1));
    1.61 -val PiM = result();
    1.62 +qed "PiM";
    1.63  
    1.64  val prems = goal Type.thy
    1.65       "[| mono(%X.A(X));  mono(%X.B(X)) |] ==> mono(%X.A(X)+B(X))";
    1.66 @@ -150,7 +150,7 @@
    1.67              eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
    1.68              (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
    1.69              hyp_subst_tac 1));
    1.70 -val PlusM = result();
    1.71 +qed "PlusM";
    1.72  
    1.73  (**************** RECURSIVE TYPES ******************)
    1.74  
    1.75 @@ -158,19 +158,19 @@
    1.76  
    1.77  goal Type.thy "mono(%X.Unit+X)";
    1.78  by (REPEAT (ares_tac [PlusM,constM,idM] 1));
    1.79 -val NatM = result();
    1.80 -val def_NatB = result() RS (Nat_def RS def_lfp_Tarski);
    1.81 +qed "NatM";
    1.82 +val def_NatB = store_thm("def_NatB", result() RS (Nat_def RS def_lfp_Tarski));
    1.83  
    1.84  goal Type.thy "mono(%X.(Unit+Sigma(A,%y.X)))";
    1.85  by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
    1.86 -val ListM = result();
    1.87 -val def_ListB = result() RS (List_def RS def_lfp_Tarski);
    1.88 -val def_ListsB = result() RS (Lists_def RS def_gfp_Tarski);
    1.89 +qed "ListM";
    1.90 +val def_ListB = store_thm("def_ListB", result() RS (List_def RS def_lfp_Tarski));
    1.91 +val def_ListsB = store_thm("def_ListsB", result() RS (Lists_def RS def_gfp_Tarski));
    1.92  
    1.93  goal Type.thy "mono(%X.({} + Sigma(A,%y.X)))";
    1.94  by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
    1.95 -val IListsM = result();
    1.96 -val def_IListsB = result() RS (ILists_def RS def_gfp_Tarski);
    1.97 +qed "IListsM";
    1.98 +val def_IListsB = store_thm("def_IListsB", result() RS (ILists_def RS def_gfp_Tarski));
    1.99  
   1.100  val ind_type_eqs = [def_NatB,def_ListB,def_ListsB,def_IListsB];
   1.101  
   1.102 @@ -264,7 +264,7 @@
   1.103  by (rtac (major RS (XH_to_E SgXH)) 1);
   1.104  by (rtac minor 1);
   1.105  by (ALLGOALS (fast_tac term_cs));
   1.106 -val SgE2 = result();
   1.107 +qed "SgE2";
   1.108  
   1.109  (* General theorem proving ignores non-canonical term-formers,             *)
   1.110  (*         - intro rules are type rules for canonical terms                *)
   1.111 @@ -280,7 +280,7 @@
   1.112  by (rtac (lfp_lowerbound RS subset_trans) 1);
   1.113  by (rtac (mono RS gfp_lemma3) 1);
   1.114  by (rtac subset_refl 1);
   1.115 -val lfp_subset_gfp = result();
   1.116 +qed "lfp_subset_gfp";
   1.117  
   1.118  val prems = goal Type.thy
   1.119      "[| a:A;  !!x X.[| x:A;  ALL y:A.t(y):X |] ==> t(x) : B(X) |] ==> \
   1.120 @@ -288,14 +288,14 @@
   1.121  by (rtac coinduct 1);
   1.122  by (res_inst_tac [("P","%x.EX y:A.x=t(y)")] CollectI 1);
   1.123  by (ALLGOALS (fast_tac (ccl_cs addSIs prems)));
   1.124 -val gfpI = result();
   1.125 +qed "gfpI";
   1.126  
   1.127  val rew::prem::prems = goal Type.thy
   1.128      "[| C==gfp(B);  a:A;  !!x X.[| x:A;  ALL y:A.t(y):X |] ==> t(x) : B(X) |] ==> \
   1.129  \    t(a) : C";
   1.130  by (rewtac rew);
   1.131  by (REPEAT (ares_tac ((prem RS gfpI)::prems) 1));
   1.132 -val def_gfpI = result();
   1.133 +qed "def_gfpI";
   1.134  
   1.135  (* EG *)
   1.136