src/FOL/fologic.ML
author wenzelm
Sun, 15 Oct 2000 19:50:35 +0200
changeset 10220 2a726de6e124
parent 9850 bee6eb4b6a42
child 10384 a499b9ce2ffe
permissions -rw-r--r--
proper symbol markup with \isamath, \isatext; support sub/super scripts:
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
     1
(*  Title:      FOL/fologic.ML
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
     2
    ID:         $Id$
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
     4
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
     5
Abstract syntax operations for FOL.
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
     6
*)
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
     7
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
     8
signature FOLOGIC =
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
     9
sig
6140
af32e2c3f77a tidied; added dest_eq
paulson
parents: 4466
diff changeset
    10
  val oT		: typ
af32e2c3f77a tidied; added dest_eq
paulson
parents: 4466
diff changeset
    11
  val mk_Trueprop	: term -> term
9473
7d13a5ace928 added atomic_Trueprop;
wenzelm
parents: 7692
diff changeset
    12
  val atomic_Trueprop	: string -> term
6140
af32e2c3f77a tidied; added dest_eq
paulson
parents: 4466
diff changeset
    13
  val dest_Trueprop	: term -> term
9850
bee6eb4b6a42 added not;
wenzelm
parents: 9543
diff changeset
    14
  val not		: term
6140
af32e2c3f77a tidied; added dest_eq
paulson
parents: 4466
diff changeset
    15
  val conj		: term
af32e2c3f77a tidied; added dest_eq
paulson
parents: 4466
diff changeset
    16
  val disj		: term
af32e2c3f77a tidied; added dest_eq
paulson
parents: 4466
diff changeset
    17
  val imp		: term
9543
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    18
  val iff		: term
7692
89bbce6f5c17 added mk_conj, mk_disj, mk_imp;
wenzelm
parents: 6140
diff changeset
    19
  val mk_conj		: term * term -> term
89bbce6f5c17 added mk_conj, mk_disj, mk_imp;
wenzelm
parents: 6140
diff changeset
    20
  val mk_disj		: term * term -> term
89bbce6f5c17 added mk_conj, mk_disj, mk_imp;
wenzelm
parents: 6140
diff changeset
    21
  val mk_imp		: term * term -> term
6140
af32e2c3f77a tidied; added dest_eq
paulson
parents: 4466
diff changeset
    22
  val dest_imp	       	: term -> term*term
9543
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    23
  val mk_iff		: term * term -> term
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    24
  val dest_iff	       	: term -> term*term
6140
af32e2c3f77a tidied; added dest_eq
paulson
parents: 4466
diff changeset
    25
  val all_const		: typ -> term
af32e2c3f77a tidied; added dest_eq
paulson
parents: 4466
diff changeset
    26
  val mk_all		: term * term -> term
af32e2c3f77a tidied; added dest_eq
paulson
parents: 4466
diff changeset
    27
  val exists_const	: typ -> term
af32e2c3f77a tidied; added dest_eq
paulson
parents: 4466
diff changeset
    28
  val mk_exists		: term * term -> term
af32e2c3f77a tidied; added dest_eq
paulson
parents: 4466
diff changeset
    29
  val eq_const		: typ -> term
af32e2c3f77a tidied; added dest_eq
paulson
parents: 4466
diff changeset
    30
  val mk_eq		: term * term -> term
af32e2c3f77a tidied; added dest_eq
paulson
parents: 4466
diff changeset
    31
  val dest_eq 		: term -> term*term
9543
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    32
  val mk_binop: string -> term * term -> term
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    33
  val mk_binrel: string -> term * term -> term
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    34
  val dest_bin: string -> typ -> term -> term * term
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    35
end;
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    36
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    37
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    38
structure FOLogic: FOLOGIC =
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    39
struct
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    40
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    41
val oT = Type("o",[]);
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    42
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    43
val Trueprop = Const("Trueprop", oT-->propT);
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    44
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    45
fun mk_Trueprop P = Trueprop $ P;
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    46
9473
7d13a5ace928 added atomic_Trueprop;
wenzelm
parents: 7692
diff changeset
    47
fun atomic_Trueprop x = mk_Trueprop (Free (x, oT));
7d13a5ace928 added atomic_Trueprop;
wenzelm
parents: 7692
diff changeset
    48
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    49
fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    50
  | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    51
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    52
(** Logical constants **)
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    53
9850
bee6eb4b6a42 added not;
wenzelm
parents: 9543
diff changeset
    54
val not = Const ("Not", oT --> oT);
bee6eb4b6a42 added not;
wenzelm
parents: 9543
diff changeset
    55
val conj = Const("op &", [oT,oT]--->oT);
bee6eb4b6a42 added not;
wenzelm
parents: 9543
diff changeset
    56
val disj = Const("op |", [oT,oT]--->oT);
bee6eb4b6a42 added not;
wenzelm
parents: 9543
diff changeset
    57
val imp = Const("op -->", [oT,oT]--->oT)
bee6eb4b6a42 added not;
wenzelm
parents: 9543
diff changeset
    58
val iff = Const("op <->", [oT,oT]--->oT);
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    59
7692
89bbce6f5c17 added mk_conj, mk_disj, mk_imp;
wenzelm
parents: 6140
diff changeset
    60
fun mk_conj (t1, t2) = conj $ t1 $ t2
89bbce6f5c17 added mk_conj, mk_disj, mk_imp;
wenzelm
parents: 6140
diff changeset
    61
and mk_disj (t1, t2) = disj $ t1 $ t2
9543
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    62
and mk_imp (t1, t2) = imp $ t1 $ t2
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    63
and mk_iff (t1, t2) = iff $ t1 $ t2;
7692
89bbce6f5c17 added mk_conj, mk_disj, mk_imp;
wenzelm
parents: 6140
diff changeset
    64
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4349
diff changeset
    65
fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4349
diff changeset
    66
  | dest_imp  t = raise TERM ("dest_imp", [t]);
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4349
diff changeset
    67
9543
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    68
fun dest_iff (Const("op <->",_) $ A $ B) = (A, B)
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    69
  | dest_iff  t = raise TERM ("dest_iff", [t]);
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    70
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    71
fun eq_const T = Const ("op =", [T, T] ---> oT);
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    72
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    73
6140
af32e2c3f77a tidied; added dest_eq
paulson
parents: 4466
diff changeset
    74
fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)
af32e2c3f77a tidied; added dest_eq
paulson
parents: 4466
diff changeset
    75
  | dest_eq t = raise TERM ("dest_eq", [t])
af32e2c3f77a tidied; added dest_eq
paulson
parents: 4466
diff changeset
    76
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    77
fun all_const T = Const ("All", [T --> oT] ---> oT);
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    78
fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P));
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    79
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    80
fun exists_const T = Const ("Ex", [T --> oT] ---> oT);
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    81
fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    82
9543
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    83
(* binary oprations and relations *)
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    84
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    85
fun mk_binop c (t, u) =
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    86
  let val T = fastype_of t in
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    87
    Const (c, [T, T] ---> T) $ t $ u
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    88
  end;
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    89
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    90
fun mk_binrel c (t, u) =
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    91
  let val T = fastype_of t in
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    92
    Const (c, [T, T] ---> oT) $ t $ u
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    93
  end;
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    94
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    95
fun dest_bin c T (tm as Const (c', Type ("fun", [T', _])) $ t $ u) =
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    96
      if c = c' andalso T = T' then (t, u)
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    97
      else raise TERM ("dest_bin " ^ c, [tm])
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    98
  | dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]);
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    99
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
   100
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
   101
end;