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