src/CCL/Type.ML
changeset 3837 d7f033c74b38
parent 2035 e329b36d9136
child 5062 fbdb0b541314
     1.1 --- a/src/CCL/Type.ML	Fri Oct 10 16:29:41 1997 +0200
     1.2 +++ b/src/CCL/Type.ML	Fri Oct 10 17:10:12 1997 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  val simp_data_defs = [one_def,inl_def,inr_def];
     1.5  val ind_data_defs = [zero_def,succ_def,nil_def,cons_def];
     1.6  
     1.7 -goal Set.thy "A <= B <-> (ALL x.x:A --> x:B)";
     1.8 +goal Set.thy "A <= B <-> (ALL x. x:A --> x:B)";
     1.9  by (fast_tac set_cs 1);
    1.10  qed "subsetXH";
    1.11  
    1.12 @@ -25,18 +25,18 @@
    1.13  val XH_tac = mk_XH_tac Type.thy simp_type_defs [];
    1.14  
    1.15  val EmptyXH = XH_tac "a : {} <-> False";
    1.16 -val SubtypeXH = XH_tac "a : {x:A.P(x)} <-> (a:A & P(a))";
    1.17 +val SubtypeXH = XH_tac "a : {x:A. P(x)} <-> (a:A & P(a))";
    1.18  val UnitXH = XH_tac "a : Unit          <-> a=one";
    1.19  val BoolXH = XH_tac "a : Bool          <-> a=true | a=false";
    1.20 -val PlusXH = XH_tac "a : A+B           <-> (EX x:A.a=inl(x)) | (EX x:B.a=inr(x))";
    1.21 -val PiXH   = XH_tac "a : PROD x:A.B(x) <-> (EX b.a=lam x.b(x) & (ALL x:A.b(x):B(x)))";
    1.22 -val SgXH   = XH_tac "a : SUM x:A.B(x)  <-> (EX x:A.EX y:B(x).a=<x,y>)";
    1.23 +val PlusXH = XH_tac "a : A+B           <-> (EX x:A. a=inl(x)) | (EX x:B. a=inr(x))";
    1.24 +val PiXH   = XH_tac "a : PROD x:A. B(x) <-> (EX b. a=lam x. b(x) & (ALL x:A. b(x):B(x)))";
    1.25 +val SgXH   = XH_tac "a : SUM x:A. B(x)  <-> (EX x:A. EX y:B(x).a=<x,y>)";
    1.26  
    1.27  val XHs = [EmptyXH,SubtypeXH,UnitXH,BoolXH,PlusXH,PiXH,SgXH];
    1.28  
    1.29  val LiftXH = XH_tac "a : [A] <-> (a=bot | a:A)";
    1.30 -val TallXH = XH_tac "a : TALL X.B(X) <-> (ALL X. a:B(X))";
    1.31 -val TexXH  = XH_tac "a : TEX X.B(X) <-> (EX X. a:B(X))";
    1.32 +val TallXH = XH_tac "a : TALL X. B(X) <-> (ALL X. a:B(X))";
    1.33 +val TexXH  = XH_tac "a : TEX X. B(X) <-> (EX X. a:B(X))";
    1.34  
    1.35  val case_rls = XH_to_Es XHs;
    1.36  
    1.37 @@ -49,7 +49,7 @@
    1.38  val oneT   = canT_tac "one : Unit";
    1.39  val trueT  = canT_tac "true : Bool";
    1.40  val falseT = canT_tac "false : Bool";
    1.41 -val lamT   = canT_tac "[| !!x.x:A ==> b(x):B(x) |] ==> lam x.b(x) : Pi(A,B)";
    1.42 +val lamT   = canT_tac "[| !!x. x:A ==> b(x):B(x) |] ==> lam x. b(x) : Pi(A,B)";
    1.43  val pairT  = canT_tac "[| a:A; b:B(a) |] ==> <a,b>:Sigma(A,B)";
    1.44  val inlT   = canT_tac "a:A ==> inl(a) : A+B";
    1.45  val inrT   = canT_tac "b:B ==> inr(b) : A+B";
    1.46 @@ -108,16 +108,16 @@
    1.47  
    1.48  (*** Monotonicity ***)
    1.49  
    1.50 -goal Type.thy "mono (%X.X)";
    1.51 +goal Type.thy "mono (%X. X)";
    1.52  by (REPEAT (ares_tac [monoI] 1));
    1.53  qed "idM";
    1.54  
    1.55 -goal Type.thy "mono(%X.A)";
    1.56 +goal Type.thy "mono(%X. A)";
    1.57  by (REPEAT (ares_tac [monoI,subset_refl] 1));
    1.58  qed "constM";
    1.59  
    1.60  val major::prems = goal Type.thy
    1.61 -    "mono(%X.A(X)) ==> mono(%X.[A(X)])";
    1.62 +    "mono(%X. A(X)) ==> mono(%X.[A(X)])";
    1.63  by (rtac (subsetI RS monoI) 1);
    1.64  by (dtac (LiftXH RS iffD1) 1);
    1.65  by (etac disjE 1);
    1.66 @@ -128,8 +128,8 @@
    1.67  qed "LiftM";
    1.68  
    1.69  val prems = goal Type.thy
    1.70 -    "[| mono(%X.A(X)); !!x X. x:A(X) ==> mono(%X.B(X,x)) |] ==> \
    1.71 -\    mono(%X.Sigma(A(X),B(X)))";
    1.72 +    "[| mono(%X. A(X)); !!x X. x:A(X) ==> mono(%X. B(X,x)) |] ==> \
    1.73 +\    mono(%X. Sigma(A(X),B(X)))";
    1.74  by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE
    1.75              eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
    1.76              (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
    1.77 @@ -137,7 +137,7 @@
    1.78  qed "SgM";
    1.79  
    1.80  val prems = goal Type.thy
    1.81 -    "[| !!x. x:A ==> mono(%X.B(X,x)) |] ==> mono(%X.Pi(A,B(X)))";
    1.82 +    "[| !!x. x:A ==> mono(%X. B(X,x)) |] ==> mono(%X. Pi(A,B(X)))";
    1.83  by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE
    1.84              eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
    1.85              (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
    1.86 @@ -145,7 +145,7 @@
    1.87  qed "PiM";
    1.88  
    1.89  val prems = goal Type.thy
    1.90 -     "[| mono(%X.A(X));  mono(%X.B(X)) |] ==> mono(%X.A(X)+B(X))";
    1.91 +     "[| mono(%X. A(X));  mono(%X. B(X)) |] ==> mono(%X. A(X)+B(X))";
    1.92  by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE
    1.93              eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
    1.94              (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
    1.95 @@ -156,18 +156,18 @@
    1.96  
    1.97  (*** Conversion Rules for Fixed Points via monotonicity and Tarski ***)
    1.98  
    1.99 -goal Type.thy "mono(%X.Unit+X)";
   1.100 +goal Type.thy "mono(%X. Unit+X)";
   1.101  by (REPEAT (ares_tac [PlusM,constM,idM] 1));
   1.102  qed "NatM";
   1.103  bind_thm("def_NatB", result() RS (Nat_def RS def_lfp_Tarski));
   1.104  
   1.105 -goal Type.thy "mono(%X.(Unit+Sigma(A,%y.X)))";
   1.106 +goal Type.thy "mono(%X.(Unit+Sigma(A,%y. X)))";
   1.107  by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
   1.108  qed "ListM";
   1.109  bind_thm("def_ListB", result() RS (List_def RS def_lfp_Tarski));
   1.110  bind_thm("def_ListsB", result() RS (Lists_def RS def_gfp_Tarski));
   1.111  
   1.112 -goal Type.thy "mono(%X.({} + Sigma(A,%y.X)))";
   1.113 +goal Type.thy "mono(%X.({} + Sigma(A,%y. X)))";
   1.114  by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
   1.115  qed "IListsM";
   1.116  bind_thm("def_IListsB", result() RS (ILists_def RS def_gfp_Tarski));
   1.117 @@ -182,10 +182,10 @@
   1.118  
   1.119  val iXH_tac = mk_iXH_tac ind_type_eqs ind_data_defs [];
   1.120  
   1.121 -val NatXH  = iXH_tac "a : Nat <-> (a=zero | (EX x:Nat.a=succ(x)))";
   1.122 -val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A.EX xs:List(A).a=x$xs))";
   1.123 -val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A.EX xs:Lists(A).a=x$xs))";
   1.124 -val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A.EX xs:ILists(A).a=x$xs)";
   1.125 +val NatXH  = iXH_tac "a : Nat <-> (a=zero | (EX x:Nat. a=succ(x)))";
   1.126 +val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A. EX xs:List(A).a=x$xs))";
   1.127 +val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A. EX xs:Lists(A).a=x$xs))";
   1.128 +val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A. EX xs:ILists(A).a=x$xs)";
   1.129  
   1.130  val iXHs = [NatXH,ListXH];
   1.131  val icase_rls = XH_to_Es iXHs;
   1.132 @@ -283,15 +283,15 @@
   1.133  qed "lfp_subset_gfp";
   1.134  
   1.135  val prems = goal Type.thy
   1.136 -    "[| a:A;  !!x X.[| x:A;  ALL y:A.t(y):X |] ==> t(x) : B(X) |] ==> \
   1.137 +    "[| a:A;  !!x X.[| x:A;  ALL y:A. t(y):X |] ==> t(x) : B(X) |] ==> \
   1.138  \    t(a) : gfp(B)";
   1.139  by (rtac coinduct 1);
   1.140 -by (res_inst_tac [("P","%x.EX y:A.x=t(y)")] CollectI 1);
   1.141 +by (res_inst_tac [("P","%x. EX y:A. x=t(y)")] CollectI 1);
   1.142  by (ALLGOALS (fast_tac (ccl_cs addSIs prems)));
   1.143  qed "gfpI";
   1.144  
   1.145  val rew::prem::prems = goal Type.thy
   1.146 -    "[| C==gfp(B);  a:A;  !!x X.[| x:A;  ALL y:A.t(y):X |] ==> t(x) : B(X) |] ==> \
   1.147 +    "[| C==gfp(B);  a:A;  !!x X.[| x:A;  ALL y:A. t(y):X |] ==> t(x) : B(X) |] ==> \
   1.148  \    t(a) : C";
   1.149  by (rewtac rew);
   1.150  by (REPEAT (ares_tac ((prem RS gfpI)::prems) 1));