src/FOL/fologic.ML
author blanchet
Wed, 11 Jun 2014 19:32:12 +0200
changeset 57221 d82c22eb9bea
parent 44241 7943b69f0188
child 69593 3dda49e08b9d
permissions -rw-r--r--
moved generic code further up
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
    Author:     Lawrence C Paulson
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
     3
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
     4
Abstract syntax operations for FOL.
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
     5
*)
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
signature FOLOGIC =
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
     8
sig
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
     9
  val oT: typ
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    10
  val mk_Trueprop: term -> term
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    11
  val dest_Trueprop: term -> term
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    12
  val not: term
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    13
  val conj: term
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    14
  val disj: term
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    15
  val imp: term
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    16
  val iff: term
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    17
  val mk_conj: term * term -> term
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    18
  val mk_disj: term * term -> term
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    19
  val mk_imp: term * term -> term
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    20
  val dest_imp: term -> term * term
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    21
  val dest_conj: term -> term list
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    22
  val mk_iff: term * term -> term
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    23
  val dest_iff: term -> term * term
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    24
  val all_const: typ -> term
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    25
  val mk_all: term * term -> term
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    26
  val exists_const: typ -> term
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    27
  val mk_exists: term * term -> term
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    28
  val eq_const: typ -> term
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    29
  val mk_eq: term * term -> term
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    30
  val dest_eq: term -> term * term
9543
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    31
  val mk_binop: string -> term * term -> term
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    32
  val mk_binrel: string -> term * term -> term
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    33
  val dest_bin: string -> typ -> term -> term * term
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    34
end;
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    35
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
structure FOLogic: FOLOGIC =
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    38
struct
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    39
38500
d5477ee35820 more antiquotations
haftmann
parents: 32449
diff changeset
    40
val oT = Type(@{type_name o},[]);
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    41
38500
d5477ee35820 more antiquotations
haftmann
parents: 32449
diff changeset
    42
val Trueprop = Const(@{const_name Trueprop}, oT-->propT);
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    43
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    44
fun mk_Trueprop P = Trueprop $ P;
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    45
38500
d5477ee35820 more antiquotations
haftmann
parents: 32449
diff changeset
    46
fun dest_Trueprop (Const (@{const_name Trueprop}, _) $ P) = P
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    47
  | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    48
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    49
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    50
(* Logical constants *)
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    51
38500
d5477ee35820 more antiquotations
haftmann
parents: 32449
diff changeset
    52
val not = Const (@{const_name Not}, oT --> oT);
41310
65631ca437c9 proper identifiers for consts and types;
wenzelm
parents: 38500
diff changeset
    53
val conj = Const(@{const_name conj}, [oT,oT]--->oT);
65631ca437c9 proper identifiers for consts and types;
wenzelm
parents: 38500
diff changeset
    54
val disj = Const(@{const_name disj}, [oT,oT]--->oT);
65631ca437c9 proper identifiers for consts and types;
wenzelm
parents: 38500
diff changeset
    55
val imp = Const(@{const_name imp}, [oT,oT]--->oT)
65631ca437c9 proper identifiers for consts and types;
wenzelm
parents: 38500
diff changeset
    56
val iff = Const(@{const_name iff}, [oT,oT]--->oT);
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    57
7692
89bbce6f5c17 added mk_conj, mk_disj, mk_imp;
wenzelm
parents: 6140
diff changeset
    58
fun mk_conj (t1, t2) = conj $ t1 $ t2
89bbce6f5c17 added mk_conj, mk_disj, mk_imp;
wenzelm
parents: 6140
diff changeset
    59
and mk_disj (t1, t2) = disj $ t1 $ t2
9543
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    60
and mk_imp (t1, t2) = imp $ t1 $ t2
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    61
and mk_iff (t1, t2) = iff $ t1 $ t2;
7692
89bbce6f5c17 added mk_conj, mk_disj, mk_imp;
wenzelm
parents: 6140
diff changeset
    62
41310
65631ca437c9 proper identifiers for consts and types;
wenzelm
parents: 38500
diff changeset
    63
fun dest_imp (Const(@{const_name imp},_) $ A $ B) = (A, B)
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4349
diff changeset
    64
  | 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
    65
41310
65631ca437c9 proper identifiers for consts and types;
wenzelm
parents: 38500
diff changeset
    66
fun dest_conj (Const (@{const_name conj}, _) $ t $ t') = t :: dest_conj t'
11668
548ba68385a3 added dest_conj, dest_concls;
wenzelm
parents: 10384
diff changeset
    67
  | dest_conj t = [t];
548ba68385a3 added dest_conj, dest_concls;
wenzelm
parents: 10384
diff changeset
    68
41310
65631ca437c9 proper identifiers for consts and types;
wenzelm
parents: 38500
diff changeset
    69
fun dest_iff (Const(@{const_name iff},_) $ A $ B) = (A, B)
9543
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    70
  | dest_iff  t = raise TERM ("dest_iff", [t]);
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    71
41310
65631ca437c9 proper identifiers for consts and types;
wenzelm
parents: 38500
diff changeset
    72
fun eq_const T = Const (@{const_name eq}, [T, T] ---> oT);
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    73
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
    74
41310
65631ca437c9 proper identifiers for consts and types;
wenzelm
parents: 38500
diff changeset
    75
fun dest_eq (Const (@{const_name eq}, _) $ lhs $ rhs) = (lhs, rhs)
6140
af32e2c3f77a tidied; added dest_eq
paulson
parents: 4466
diff changeset
    76
  | dest_eq t = raise TERM ("dest_eq", [t])
af32e2c3f77a tidied; added dest_eq
paulson
parents: 4466
diff changeset
    77
38500
d5477ee35820 more antiquotations
haftmann
parents: 32449
diff changeset
    78
fun all_const T = Const (@{const_name All}, [T --> oT] ---> oT);
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 41310
diff changeset
    79
fun mk_all (Free (x, T), P) = all_const T $ absfree (x, T) P;
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    80
38500
d5477ee35820 more antiquotations
haftmann
parents: 32449
diff changeset
    81
fun exists_const T = Const (@{const_name Ex}, [T --> oT] ---> oT);
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 41310
diff changeset
    82
fun mk_exists (Free (x, T), P) = exists_const T $ absfree (x, T) P;
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
    83
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31974
diff changeset
    84
9543
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    85
(* binary oprations and relations *)
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    86
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    87
fun mk_binop c (t, u) =
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    88
  let val T = fastype_of t in
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    89
    Const (c, [T, T] ---> T) $ t $ u
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    90
  end;
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    91
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    92
fun mk_binrel c (t, u) =
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    93
  let val T = fastype_of t in
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    94
    Const (c, [T, T] ---> oT) $ t $ u
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    95
  end;
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    96
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    97
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
    98
      if c = c' andalso T = T' then (t, u)
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
    99
      else raise TERM ("dest_bin " ^ c, [tm])
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
   100
  | dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]);
ce61d1c1a509 new abstract syntax operations, used in ZF
paulson
parents: 9473
diff changeset
   101
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff changeset
   102
end;