ind_syntax.ML
changeset 128 89669c58e506
child 134 4b7da5a895e7
equal deleted inserted replaced
127:d9527f97246e 128:89669c58e506
       
     1 (*  Title: 	HOL/ind_syntax.ML
       
     2     ID:         $Id$
       
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
       
     4     Copyright   1994  University of Cambridge
       
     5 
       
     6 Abstract Syntax functions for Inductive Definitions
       
     7 See also ../Pure/section-utils.ML
       
     8 *)
       
     9 
       
    10 (*The structure protects these items from redeclaration (somewhat!).  The 
       
    11   datatype definitions in theory files refer to these items by name!
       
    12 *)
       
    13 structure Ind_Syntax =
       
    14 struct
       
    15 
       
    16 (** Abstract syntax definitions for HOL **)
       
    17 
       
    18 val termC: class = "term";
       
    19 val termS: sort = [termC];
       
    20 
       
    21 val termTVar = TVar(("'a",0),termS);
       
    22 
       
    23 val boolT = Type("bool",[]);
       
    24 val unitT = Type("unit",[]);
       
    25 
       
    26 val conj = Const("op &", [boolT,boolT]--->boolT)
       
    27 and disj = Const("op |", [boolT,boolT]--->boolT)
       
    28 and imp = Const("op -->", [boolT,boolT]--->boolT);
       
    29 
       
    30 fun eq_const T = Const("op =", [T,T]--->boolT);
       
    31 
       
    32 fun mk_set T = Type("set",[T]);
       
    33 
       
    34 fun dest_set (Type("set",[T])) = T
       
    35   | dest_set _                 = error "dest_set: set type expected"
       
    36 
       
    37 fun mk_mem (x,A) = 
       
    38   let val setT = fastype_of A
       
    39   in  Const("op :", [dest_set setT, setT]--->boolT) $ x $ A
       
    40   end;
       
    41 
       
    42 fun Int_const T = 
       
    43   let val sT = mk_set T
       
    44   in  Const("op Int", [sT,sT]--->sT)  end;
       
    45 
       
    46 fun exists_const T = Const("Ex", [T-->boolT]--->boolT);
       
    47 fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));
       
    48 
       
    49 fun all_const T = Const("All", [T-->boolT]--->boolT);
       
    50 fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P));
       
    51 
       
    52 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
       
    53 fun mk_all_imp (A,P) = 
       
    54   let val T = dest_set (fastype_of A)
       
    55   in  all_const T $ Abs("v", T, imp $ (mk_mem (Bound 0, A)) $ (P $ Bound 0))
       
    56   end;
       
    57 
       
    58 (** Cartesian product type **)
       
    59 
       
    60 fun mk_prod (T1,T2) = Type("*", [T1,T2]);
       
    61 
       
    62 fun factors (Type("*", [T1,T2])) = factors T1 @ factors T2
       
    63   | factors T                    = [T];
       
    64 
       
    65 (*Make a correctly typed ordered pair*)
       
    66 fun mk_Pair (t1,t2) = 
       
    67   let val T1 = fastype_of t1
       
    68       and T2 = fastype_of t2
       
    69   in  Const("Pair", [T1, T2] ---> mk_prod(T1,T2)) $ t1 $ t2  end;
       
    70    
       
    71 fun split_const(Ta,Tb,Tc) = 
       
    72     Const("split", [[Ta,Tb]--->Tc, mk_prod(Ta,Tb)] ---> Tc);
       
    73 
       
    74 (*Given u expecting arguments of types [T1,...,Tn], create term of 
       
    75   type T1*...*Tn => Tc using split.  Here * associates to the LEFT*)
       
    76 fun ap_split_l Tc u [ ]   = Abs("null", unitT, u)
       
    77   | ap_split_l Tc u [_]   = u
       
    78   | ap_split_l Tc u (Ta::Tb::Ts) = ap_split_l Tc (split_const(Ta,Tb,Tc) $ u) 
       
    79                                               (mk_prod(Ta,Tb) :: Ts);
       
    80 
       
    81 (*Given u expecting arguments of types [T1,...,Tn], create term of 
       
    82   type T1*...*Tn => i using split.  Here * associates to the RIGHT*)
       
    83 fun ap_split Tc u [ ]   = Abs("null", unitT, u)
       
    84   | ap_split Tc u [_]   = u
       
    85   | ap_split Tc u [Ta,Tb] = split_const(Ta,Tb,Tc) $ u
       
    86   | ap_split Tc u (Ta::Ts) = 
       
    87       split_const(Ta, foldr1 mk_prod Ts, Tc) $ 
       
    88       (Abs("v", Ta, ap_split Tc (u $ Bound(length Ts - 2)) Ts));
       
    89 
       
    90 (** Disjoint sum type **)
       
    91 
       
    92 fun mk_sum (T1,T2) = Type("+", [T1,T2]);
       
    93 val Inl	= Const("Inl", dummyT)
       
    94 and Inr	= Const("Inr", dummyT);		(*correct types added later!*)
       
    95 (*val elim	= Const("case", [iT-->iT, iT-->iT, iT]--->iT)*)
       
    96 
       
    97 fun summands (Type("+", [T1,T2])) = summands T1 @ summands T2
       
    98   | summands T                    = [T];
       
    99 
       
   100 (*Given the destination type, fills in correct types of an Inl/Inr nest*)
       
   101 fun mend_sum_types (h,T) =
       
   102     (case (h,T) of
       
   103 	 (Const("Inl",_) $ h1, Type("+", [T1,T2])) =>
       
   104 	     Const("Inl", T1 --> T) $ (mend_sum_types (h1, T1))
       
   105        | (Const("Inr",_) $ h2, Type("+", [T1,T2])) =>
       
   106 	     Const("Inr", T2 --> T) $ (mend_sum_types (h2, T2))
       
   107        | _ => h);
       
   108 
       
   109 fun Collect_const T = Const("Collect", [T-->boolT] ---> mk_set T);
       
   110 fun mk_Collect (a,T,t) = Collect_const T $ absfree(a, T, t);
       
   111 
       
   112 val Trueprop = Const("Trueprop",boolT-->propT);
       
   113 fun mk_tprop P = Trueprop $ P;
       
   114 
       
   115 
       
   116 (*simple error-checking in the premises of an inductive definition*)
       
   117 fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
       
   118 	error"Premises may not be conjuctive"
       
   119   | chk_prem rec_hd (Const("op :",_) $ t $ X) = 
       
   120 	deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol"
       
   121   | chk_prem rec_hd t = 
       
   122 	deny (Logic.occs(rec_hd,t)) "Recursion term in side formula";
       
   123 
       
   124 (*Return the conclusion of a rule, of the form t:X*)
       
   125 fun rule_concl rl = 
       
   126     let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = 
       
   127 		Logic.strip_imp_concl rl
       
   128     in  (t,X)  end;
       
   129 
       
   130 (*As above, but return error message if bad*)
       
   131 fun rule_concl_msg sign rl = rule_concl rl
       
   132     handle Bind => error ("Ill-formed conclusion of introduction rule: " ^ 
       
   133 			  Sign.string_of_term sign rl);
       
   134 
       
   135 (*For simplifying the elimination rule*)
       
   136 val sumprod_free_SEs = 
       
   137     Pair_inject ::
       
   138     map make_elim [Inl_neq_Inr, Inr_neq_Inl, Inl_inject, Inr_inject];
       
   139 
       
   140 (*For deriving cases rules.  
       
   141   read_instantiate replaces a propositional variable by a formula variable*)
       
   142 val equals_CollectD = 
       
   143     read_instantiate [("W","?Q")]
       
   144         (make_elim (equalityD1 RS subsetD RS CollectD));
       
   145 
       
   146 (*Delete needless equality assumptions*)
       
   147 val refl_thin = prove_goal HOL.thy "!!P. [| a=a;  P |] ==> P"
       
   148      (fn _ => [assume_tac 1]);
       
   149 
       
   150 end;
       
   151