src/Pure/drule.ML
author wenzelm
Tue, 01 Aug 1995 17:20:42 +0200
changeset 1218 59ed8ef1a3a1
parent 1194 563ecd14c1d8
child 1237 45ac644b0052
permissions -rw-r--r--
modified pretty_thm, standard, eq_thm to handle shyps;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
     1
(*  Title:      Pure/drule.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Derived rules and other operations on theorems and theories
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
11
d0e17c42dbb4 Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents: 0
diff changeset
     9
infix 0 RS RSN RL RLN MRS MRL COMP;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
signature DRULE =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
  sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
  structure Thm : THM
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
  local open Thm  in
668
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    15
  val add_defs		: (string * string) list -> theory -> theory
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    16
  val add_defs_i	: (string * term) list -> theory -> theory
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    17
  val asm_rl		: thm
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    18
  val assume_ax		: theory -> string -> thm
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    19
  val COMP		: thm * thm -> thm
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    20
  val compose		: thm * int * thm -> thm list
708
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
    21
  val cprems_of		: thm -> cterm list
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
    22
  val cskip_flexpairs	: cterm -> cterm
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
    23
  val cstrip_imp_prems	: cterm -> cterm list
668
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    24
  val cterm_instantiate	: (cterm*cterm)list -> thm -> thm
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    25
  val cut_rl		: thm
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    26
  val equal_abs_elim	: cterm  -> thm -> thm
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
    27
  val equal_abs_elim_list: cterm list -> thm -> thm
668
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    28
  val eq_thm		: thm * thm -> bool
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    29
  val eq_thm_sg		: thm * thm -> bool
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
    30
  val flexpair_abs_elim_list: cterm list -> thm -> thm
668
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    31
  val forall_intr_list	: cterm list -> thm -> thm
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    32
  val forall_intr_frees	: thm -> thm
1194
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
    33
  val forall_intr_vars	: thm -> thm
668
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    34
  val forall_elim_list	: cterm list -> thm -> thm
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    35
  val forall_elim_var	: int -> thm -> thm
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    36
  val forall_elim_vars	: int -> thm -> thm
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    37
  val implies_elim_list	: thm -> thm list -> thm
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    38
  val implies_intr_list	: cterm list -> thm -> thm
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    39
  val MRL		: thm list list * thm list -> thm list
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    40
  val MRS		: thm list * thm -> thm
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    41
  val pprint_cterm	: cterm -> pprint_args -> unit
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    42
  val pprint_ctyp	: ctyp -> pprint_args -> unit
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    43
  val pprint_theory	: theory -> pprint_args -> unit
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    44
  val pprint_thm	: thm -> pprint_args -> unit
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    45
  val pretty_thm	: thm -> Sign.Syntax.Pretty.T
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    46
  val print_cterm	: cterm -> unit
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    47
  val print_ctyp	: ctyp -> unit
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    48
  val print_goals	: int -> thm -> unit
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    49
  val print_goals_ref	: (int -> thm -> unit) ref
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    50
  val print_syntax	: theory -> unit
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    51
  val print_theory	: theory -> unit
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    52
  val print_thm		: thm -> unit
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    53
  val prth		: thm -> thm
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    54
  val prthq		: thm Sequence.seq -> thm Sequence.seq
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    55
  val prths		: thm list -> thm list
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    56
  val read_instantiate	: (string*string)list -> thm -> thm
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
  val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
668
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    58
  val read_insts	:
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
    59
          Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
    60
                  -> (indexname -> typ option) * (indexname -> sort option)
949
83c588d6fee9 Changed treatment of during type inference internally generated type
nipkow
parents: 922
diff changeset
    61
                  -> string list -> (string*string)list
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
    62
                  -> (indexname*ctyp)list * (cterm*cterm)list
668
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    63
  val reflexive_thm	: thm
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    64
  val revcut_rl		: thm
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    65
  val rewrite_goal_rule	: bool*bool -> (meta_simpset -> thm -> thm option)
214
ed6a3e2b1a33 added new parameter to the simplification tactics which indicates if
nipkow
parents: 211
diff changeset
    66
        -> meta_simpset -> int -> thm -> thm
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
  val rewrite_goals_rule: thm list -> thm -> thm
668
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    68
  val rewrite_rule	: thm list -> thm -> thm
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    69
  val RS		: thm * thm -> thm
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    70
  val RSN		: thm * (int * thm) -> thm
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    71
  val RL		: thm list * thm list -> thm list
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    72
  val RLN		: thm list * (int * thm list) -> thm list
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    73
  val show_hyps		: bool ref
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    74
  val size_of_thm	: thm -> int
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    75
  val standard		: thm -> thm
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    76
  val string_of_cterm	: cterm -> string
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    77
  val string_of_ctyp	: ctyp -> string
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    78
  val string_of_thm	: thm -> string
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    79
  val symmetric_thm	: thm
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    80
  val thin_rl		: thm
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    81
  val transitive_thm	: thm
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
  val triv_forall_equality: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
  val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
668
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    84
  val zero_var_indexes	: thm -> thm
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
  end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
668
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    88
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
    89
functor DruleFun (structure Logic: LOGIC and Thm: THM): DRULE =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
structure Thm = Thm;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
structure Sign = Thm.Sign;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
structure Type = Sign.Type;
575
74f0e5fce609 added print_syntax: theory -> unit;
wenzelm
parents: 561
diff changeset
    94
structure Syntax = Sign.Syntax;
74f0e5fce609 added print_syntax: theory -> unit;
wenzelm
parents: 561
diff changeset
    95
structure Pretty = Syntax.Pretty
400
3c2c40c87112 replaced ext_axtab by new_axioms;
wenzelm
parents: 385
diff changeset
    96
structure Symtab = Sign.Symtab;
3c2c40c87112 replaced ext_axtab by new_axioms;
wenzelm
parents: 385
diff changeset
    97
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
local open Thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
561
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   101
(**** Extend Theories ****)
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   102
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   103
(** add constant definitions **)
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   104
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   105
(* all_axioms_of *)
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   106
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   107
(*results may contain duplicates!*)
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   108
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   109
fun ancestry_of thy =
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   110
  thy :: flat (map ancestry_of (parents_of thy));
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   111
776
df8f91c0e57c improved axioms_of: returns thms as the manual says;
wenzelm
parents: 708
diff changeset
   112
val all_axioms_of = 
df8f91c0e57c improved axioms_of: returns thms as the manual says;
wenzelm
parents: 708
diff changeset
   113
  flat o map (Symtab.dest o #new_axioms o rep_theory) o ancestry_of;
561
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   114
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   115
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   116
(* clash_types, clash_consts *)
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   117
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   118
(*check if types have common instance (ignoring sorts)*)
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   119
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   120
fun clash_types ty1 ty2 =
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   121
  let
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   122
    val ty1' = Type.varifyT ty1;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   123
    val ty2' = incr_tvar (maxidx_of_typ ty1' + 1) (Type.varifyT ty2);
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   124
  in
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   125
    Type.raw_unify (ty1', ty2')
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   126
  end;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   127
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   128
fun clash_consts (c1, ty1) (c2, ty2) =
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   129
  c1 = c2 andalso clash_types ty1 ty2;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   130
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   131
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   132
(* clash_defns *)
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   133
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   134
fun clash_defn c_ty (name, tm) =
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   135
  let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals tm))) in
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   136
    if clash_consts c_ty (c, ty') then Some (name, ty') else None
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   137
  end handle TERM _ => None;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   138
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   139
fun clash_defns c_ty axms =
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   140
  distinct (mapfilter (clash_defn c_ty) axms);
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   141
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   142
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   143
(* dest_defn *)
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   144
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   145
fun dest_defn tm =
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   146
  let
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   147
    fun err msg = raise_term msg [tm];
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   148
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   149
    val (lhs, rhs) = Logic.dest_equals tm
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   150
      handle TERM _ => err "Not a meta-equality (==)";
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   151
    val (head, args) = strip_comb lhs;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   152
    val (c, ty) = dest_Const head
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   153
      handle TERM _ => err "Head of lhs not a constant";
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   154
655
9748dbcd4157 minor change of occs_const in dest_defn;
wenzelm
parents: 641
diff changeset
   155
    fun occs_const (Const c_ty') = (c_ty' = (c, ty))
561
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   156
      | occs_const (Abs (_, _, t)) = occs_const t
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   157
      | occs_const (t $ u) = occs_const t orelse occs_const u
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   158
      | occs_const _ = false;
641
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   159
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   160
    val show_frees = commas_quote o map (fst o dest_Free);
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   161
    val show_tfrees = commas_quote o map fst;
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   162
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   163
    val lhs_dups = duplicates args;
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   164
    val rhs_extras = gen_rems (op =) (term_frees rhs, args);
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   165
    val rhs_extrasT = gen_rems (op =) (term_tfrees rhs, typ_tfrees ty);
561
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   166
  in
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   167
    if not (forall is_Free args) then
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   168
      err "Arguments of lhs have to be variables"
641
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   169
    else if not (null lhs_dups) then
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   170
      err ("Duplicate variables on lhs: " ^ show_frees lhs_dups)
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   171
    else if not (null rhs_extras) then
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   172
      err ("Extra variables on rhs: " ^ show_frees rhs_extras)
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   173
    else if not (null rhs_extrasT) then
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   174
      err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT)
561
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   175
    else if occs_const rhs then
655
9748dbcd4157 minor change of occs_const in dest_defn;
wenzelm
parents: 641
diff changeset
   176
      err ("Constant to be defined occurs on rhs")
561
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   177
    else (c, ty)
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   178
  end;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   179
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   180
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   181
(* check_defn *)
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   182
641
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   183
fun err_in_defn name msg =
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   184
  (writeln msg; error ("The error(s) above occurred in definition " ^ quote name));
561
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   185
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   186
fun check_defn sign (axms, (name, tm)) =
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   187
  let
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   188
    fun show_const (c, ty) = quote (Pretty.string_of (Pretty.block
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   189
      [Pretty.str (c ^ " ::"), Pretty.brk 1, Sign.pretty_typ sign ty]));
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   190
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   191
    fun show_defn c (dfn, ty') = show_const (c, ty') ^ " in " ^ dfn;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   192
    fun show_defns c = commas o map (show_defn c);
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   193
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   194
    val (c, ty) = dest_defn tm
641
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   195
      handle TERM (msg, _) => err_in_defn name msg;
561
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   196
    val defns = clash_defns (c, ty) axms;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   197
  in
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   198
    if not (null defns) then
641
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   199
      err_in_defn name ("Definition of " ^ show_const (c, ty) ^
561
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   200
        " clashes with " ^ show_defns c defns)
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   201
    else (name, tm) :: axms
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   202
  end;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   203
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   204
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   205
(* add_defs *)
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   206
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   207
fun ext_defns prep_axm raw_axms thy =
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   208
  let
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   209
    val axms = map (prep_axm (sign_of thy)) raw_axms;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   210
    val all_axms = all_axioms_of thy;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   211
  in
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   212
    foldl (check_defn (sign_of thy)) (all_axms, axms);
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   213
    add_axioms_i axms thy
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   214
  end;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   215
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   216
val add_defs_i = ext_defns cert_axm;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   217
val add_defs = ext_defns read_axm;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   218
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   219
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   220
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
(**** More derived rules and operations on theorems ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
708
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   223
(** some cterm->cterm operations: much faster than calling cterm_of! **)
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   224
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   225
(*Discard flexflex pairs; return a cterm*)
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   226
fun cskip_flexpairs ct =
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   227
    case term_of ct of
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   228
	(Const("==>", _) $ (Const("=?=",_)$_$_) $ _) =>
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   229
	    cskip_flexpairs (#2 (dest_cimplies ct))
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   230
      | _ => ct;
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   231
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   232
(* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   233
fun cstrip_imp_prems ct =
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   234
    let val (cA,cB) = dest_cimplies ct
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   235
    in  cA :: cstrip_imp_prems cB  end
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   236
    handle TERM _ => [];
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   237
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   238
(*The premises of a theorem, as a cterm list*)
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   239
val cprems_of = cstrip_imp_prems o cskip_flexpairs o cprop_of;
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   240
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   241
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   242
(** reading of instantiations **)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   243
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   244
fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   245
        | _ => error("Lexical error in variable name " ^ quote (implode cs));
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   246
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   247
fun absent ixn =
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   248
  error("No such variable in term: " ^ Syntax.string_of_vname ixn);
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   249
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   250
fun inst_failure ixn =
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   251
  error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   252
952
9e10962866b0 Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents: 949
diff changeset
   253
(* this code is a bit of a mess. add_cterm could be simplified greatly if
9e10962866b0 Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents: 949
diff changeset
   254
   simultaneous instantiations were read or at least type checked
9e10962866b0 Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents: 949
diff changeset
   255
   simultaneously rather than one after the other. This would make the tricky
9e10962866b0 Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents: 949
diff changeset
   256
   composition of implicit type instantiations (parameter tye) superfluous.
9e10962866b0 Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents: 949
diff changeset
   257
*)
949
83c588d6fee9 Changed treatment of during type inference internally generated type
nipkow
parents: 922
diff changeset
   258
fun read_insts sign (rtypes,rsorts) (types,sorts) used insts =
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   259
let val {tsig,...} = Sign.rep_sg sign
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   260
    fun split([],tvs,vs) = (tvs,vs)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   261
      | split((sv,st)::l,tvs,vs) = (case explode sv of
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   262
                  "'"::cs => split(l,(indexname cs,st)::tvs,vs)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   263
                | cs => split(l,tvs,(indexname cs,st)::vs));
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   264
    val (tvs,vs) = split(insts,[],[]);
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   265
    fun readT((a,i),st) =
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   266
        let val ixn = ("'" ^ a,i);
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   267
            val S = case rsorts ixn of Some S => S | None => absent ixn;
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   268
            val T = Sign.read_typ (sign,sorts) st;
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   269
        in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   270
           else inst_failure ixn
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   271
        end
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   272
    val tye = map readT tvs;
949
83c588d6fee9 Changed treatment of during type inference internally generated type
nipkow
parents: 922
diff changeset
   273
    fun add_cterm ((cts,tye,used), (ixn,st)) =
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   274
        let val T = case rtypes ixn of
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   275
                      Some T => typ_subst_TVars tye T
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   276
                    | None => absent ixn;
949
83c588d6fee9 Changed treatment of during type inference internally generated type
nipkow
parents: 922
diff changeset
   277
            val (ct,tye2) = read_def_cterm(sign,types,sorts) used false (st,T);
952
9e10962866b0 Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents: 949
diff changeset
   278
            val cts' = (ixn,T,ct)::cts
9e10962866b0 Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents: 949
diff changeset
   279
            fun inst(ixn,T,ct) = (ixn,typ_subst_TVars tye2 T,ct)
949
83c588d6fee9 Changed treatment of during type inference internally generated type
nipkow
parents: 922
diff changeset
   280
            val used' = add_term_tvarnames(term_of ct,used);
952
9e10962866b0 Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents: 949
diff changeset
   281
        in (map inst cts',tye2 @ tye,used') end
949
83c588d6fee9 Changed treatment of during type inference internally generated type
nipkow
parents: 922
diff changeset
   282
    val (cterms,tye',_) = foldl add_cterm (([],tye,used), vs);
952
9e10962866b0 Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents: 949
diff changeset
   283
in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye',
9e10962866b0 Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents: 949
diff changeset
   284
    map (fn (ixn,T,ct) => (cterm_of sign (Var(ixn,T)), ct)) cterms)
9e10962866b0 Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents: 949
diff changeset
   285
end;
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   286
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   287
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   288
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   289
(*** Printing of theories, theorems, etc. ***)
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   290
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   291
(*If false, hypotheses are printed as dots*)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   292
val show_hyps = ref true;
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   293
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   294
fun pretty_thm th =
1218
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   295
  let
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   296
    val {sign, shyps, hyps, prop, ...} = rep_thm th;
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   297
    val hlen = length shyps + length hyps;
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   298
    val hsymbs =
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   299
      if hlen = 0 then []
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   300
      else if ! show_hyps then
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   301
        [Pretty.brk 2, Pretty.list "[" "]"
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   302
          (map (Sign.pretty_term sign) hyps @ map Sign.pretty_sort shyps)]
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   303
      else
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   304
        [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ "]")];
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   305
  in
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   306
    Pretty.block (Sign.pretty_term sign prop :: hsymbs)
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   307
  end;
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   308
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   309
val string_of_thm = Pretty.string_of o pretty_thm;
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   310
val pprint_thm = Pretty.pprint o Pretty.quote o pretty_thm;
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   311
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   312
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   313
(** Top-level commands for printing theorems **)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   314
val print_thm = writeln o string_of_thm;
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   315
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   316
fun prth th = (print_thm th; th);
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   317
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   318
(*Print and return a sequence of theorems, separated by blank lines. *)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   319
fun prthq thseq =
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   320
  (Sequence.prints (fn _ => print_thm) 100000 thseq; thseq);
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   321
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   322
(*Print and return a list of theorems, separated by blank lines. *)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   323
fun prths ths = (print_list_ln print_thm ths; ths);
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   324
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   325
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   326
(* other printing commands *)
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   327
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   328
fun pprint_ctyp cT =
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   329
  let val {sign, T} = rep_ctyp cT in Sign.pprint_typ sign T end;
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   330
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   331
fun string_of_ctyp cT =
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   332
  let val {sign, T} = rep_ctyp cT in Sign.string_of_typ sign T end;
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   333
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   334
val print_ctyp = writeln o string_of_ctyp;
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   335
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   336
fun pprint_cterm ct =
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   337
  let val {sign, t, ...} = rep_cterm ct in Sign.pprint_term sign t end;
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   338
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   339
fun string_of_cterm ct =
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   340
  let val {sign, t, ...} = rep_cterm ct in Sign.string_of_term sign t end;
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   341
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   342
val print_cterm = writeln o string_of_cterm;
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   343
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   344
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   345
(* print theory *)
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   346
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   347
val pprint_theory = Sign.pprint_sg o sign_of;
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   348
575
74f0e5fce609 added print_syntax: theory -> unit;
wenzelm
parents: 561
diff changeset
   349
val print_syntax = Syntax.print_syntax o syn_of;
74f0e5fce609 added print_syntax: theory -> unit;
wenzelm
parents: 561
diff changeset
   350
385
921f87897a76 added print_sign, print_axioms: theory -> unit;
wenzelm
parents: 252
diff changeset
   351
fun print_axioms thy =
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   352
  let
400
3c2c40c87112 replaced ext_axtab by new_axioms;
wenzelm
parents: 385
diff changeset
   353
    val {sign, new_axioms, ...} = rep_theory thy;
3c2c40c87112 replaced ext_axtab by new_axioms;
wenzelm
parents: 385
diff changeset
   354
    val axioms = Symtab.dest new_axioms;
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   355
385
921f87897a76 added print_sign, print_axioms: theory -> unit;
wenzelm
parents: 252
diff changeset
   356
    fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1,
921f87897a76 added print_sign, print_axioms: theory -> unit;
wenzelm
parents: 252
diff changeset
   357
      Pretty.quote (Sign.pretty_term sign t)];
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   358
  in
385
921f87897a76 added print_sign, print_axioms: theory -> unit;
wenzelm
parents: 252
diff changeset
   359
    Pretty.writeln (Pretty.big_list "additional axioms:" (map prt_axm axioms))
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   360
  end;
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   361
843
c1a4a4206102 removed print_sign, print_axioms;
wenzelm
parents: 776
diff changeset
   362
fun print_theory thy = (Sign.print_sg (sign_of thy); print_axioms thy);
385
921f87897a76 added print_sign, print_axioms: theory -> unit;
wenzelm
parents: 252
diff changeset
   363
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   364
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   365
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   366
(** Print thm A1,...,An/B in "goal style" -- premises as numbered subgoals **)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   367
641
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   368
(* get type_env, sort_env of term *)
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   369
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   370
local
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   371
  open Syntax;
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   372
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   373
  fun ins_entry (x, y) [] = [(x, [y])]
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   374
    | ins_entry (x, y) ((pair as (x', ys')) :: pairs) =
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   375
        if x = x' then (x', y ins ys') :: pairs
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   376
        else pair :: ins_entry (x, y) pairs;
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   377
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   378
  fun add_type_env (Free (x, T), env) = ins_entry (T, x) env
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   379
    | add_type_env (Var (xi, T), env) = ins_entry (T, string_of_vname xi) env
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   380
    | add_type_env (Abs (_, _, t), env) = add_type_env (t, env)
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   381
    | add_type_env (t $ u, env) = add_type_env (u, add_type_env (t, env))
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   382
    | add_type_env (_, env) = env;
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   383
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   384
  fun add_sort_env (Type (_, Ts), env) = foldr add_sort_env (Ts, env)
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   385
    | add_sort_env (TFree (x, S), env) = ins_entry (S, x) env
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   386
    | add_sort_env (TVar (xi, S), env) = ins_entry (S, string_of_vname xi) env;
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   387
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   388
  val sort = map (apsnd sort_strings);
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   389
in
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   390
  fun type_env t = sort (add_type_env (t, []));
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   391
  fun sort_env t = rev (sort (it_term_types add_sort_env (t, [])));
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   392
end;
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   393
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   394
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   395
(* print_goals *)
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   396
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   397
fun print_goals maxgoals state =
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   398
  let
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   399
    open Syntax;
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   400
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   401
    val {sign, prop, ...} = rep_thm state;
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   402
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   403
    val pretty_term = Sign.pretty_term sign;
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   404
    val pretty_typ = Sign.pretty_typ sign;
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   405
    val pretty_sort = Sign.pretty_sort;
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   406
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   407
    fun pretty_vars prtf (X, vs) = Pretty.block
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   408
      [Pretty.block (Pretty.commas (map Pretty.str vs)),
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   409
        Pretty.str " ::", Pretty.brk 1, prtf X];
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   410
641
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   411
    fun print_list _ _ [] = ()
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   412
      | print_list name prtf lst =
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   413
          (writeln ""; Pretty.writeln (Pretty.big_list name (map prtf lst)));
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   414
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   415
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   416
    fun print_goals (_, []) = ()
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   417
      | print_goals (n, A :: As) = (Pretty.writeln (Pretty.blk (0,
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   418
          [Pretty.str (" " ^ string_of_int n ^ ". "), pretty_term A]));
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   419
            print_goals (n + 1, As));
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   420
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   421
    val print_ffpairs =
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   422
      print_list "Flex-flex pairs:" (pretty_term o Logic.mk_flexpair);
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   423
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   424
    val print_types = print_list "Types:" (pretty_vars pretty_typ) o type_env;
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   425
    val print_sorts = print_list "Sorts:" (pretty_vars pretty_sort) o sort_env;
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   426
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   427
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   428
    val (tpairs, As, B) = Logic.strip_horn prop;
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   429
    val ngoals = length As;
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   430
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   431
    val orig_no_freeTs = ! show_no_free_types;
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   432
    val orig_sorts = ! show_sorts;
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   433
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   434
    fun restore () =
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   435
      (show_no_free_types := orig_no_freeTs; show_sorts := orig_sorts);
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   436
  in
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   437
    (show_no_free_types := true; show_sorts := false;
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   438
      Pretty.writeln (pretty_term B);
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   439
      if ngoals = 0 then writeln "No subgoals!"
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   440
      else if ngoals > maxgoals then
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   441
        (print_goals (1, take (maxgoals, As));
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   442
          writeln ("A total of " ^ string_of_int ngoals ^ " subgoals..."))
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   443
      else print_goals (1, As);
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   444
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   445
      print_ffpairs tpairs;
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   446
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   447
      if orig_sorts then
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   448
        (print_types prop; print_sorts prop)
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   449
      else if ! show_types then
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   450
        print_types prop
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   451
      else ())
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   452
    handle exn => (restore (); raise exn);
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   453
    restore ()
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   454
  end;
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   455
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   456
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   457
(*"hook" for user interfaces: allows print_goals to be replaced*)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   458
val print_goals_ref = ref print_goals;
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   459
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   460
(*** Find the type (sort) associated with a (T)Var or (T)Free in a term
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   461
     Used for establishing default types (of variables) and sorts (of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   462
     type variables) when reading another term.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   463
     Index -1 indicates that a (T)Free rather than a (T)Var is wanted.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   464
***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   465
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   466
fun types_sorts thm =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   467
    let val {prop,hyps,...} = rep_thm thm;
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   468
        val big = list_comb(prop,hyps); (* bogus term! *)
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   469
        val vars = map dest_Var (term_vars big);
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   470
        val frees = map dest_Free (term_frees big);
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   471
        val tvars = term_tvars big;
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   472
        val tfrees = term_tfrees big;
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   473
        fun typ(a,i) = if i<0 then assoc(frees,a) else assoc(vars,(a,i));
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   474
        fun sort(a,i) = if i<0 then assoc(tfrees,a) else assoc(tvars,(a,i));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   475
    in (typ,sort) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   476
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   477
(** Standardization of rules **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   478
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   479
(*Generalization over a list of variables, IGNORING bad ones*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   480
fun forall_intr_list [] th = th
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   481
  | forall_intr_list (y::ys) th =
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   482
        let val gth = forall_intr_list ys th
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   483
        in  forall_intr y gth   handle THM _ =>  gth  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   484
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   485
(*Generalization over all suitable Free variables*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   486
fun forall_intr_frees th =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   487
    let val {prop,sign,...} = rep_thm th
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   488
    in  forall_intr_list
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   489
         (map (cterm_of sign) (sort atless (term_frees prop)))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   490
         th
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   491
    end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   492
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   493
(*Replace outermost quantified variable by Var of given index.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   494
    Could clash with Vars already present.*)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   495
fun forall_elim_var i th =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   496
    let val {prop,sign,...} = rep_thm th
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   497
    in case prop of
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   498
          Const("all",_) $ Abs(a,T,_) =>
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   499
              forall_elim (cterm_of sign (Var((a,i), T)))  th
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   500
        | _ => raise THM("forall_elim_var", i, [th])
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   501
    end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   502
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   503
(*Repeat forall_elim_var until all outer quantifiers are removed*)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   504
fun forall_elim_vars i th =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   505
    forall_elim_vars i (forall_elim_var i th)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   506
        handle THM _ => th;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   507
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   508
(*Specialization over a list of cterms*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   509
fun forall_elim_list cts th = foldr (uncurry forall_elim) (rev cts, th);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   510
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   511
(* maps [A1,...,An], B   to   [| A1;...;An |] ==> B  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   512
fun implies_intr_list cAs th = foldr (uncurry implies_intr) (cAs,th);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   513
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   514
(* maps [| A1;...;An |] ==> B and [A1,...,An]   to   B *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   515
fun implies_elim_list impth ths = foldl (uncurry implies_elim) (impth,ths);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   516
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   517
(*Reset Var indexes to zero, renaming to preserve distinctness*)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   518
fun zero_var_indexes th =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   519
    let val {prop,sign,...} = rep_thm th;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   520
        val vars = term_vars prop
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   521
        val bs = foldl add_new_id ([], map (fn Var((a,_),_)=>a) vars)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   522
        val inrs = add_term_tvars(prop,[]);
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   523
        val nms' = rev(foldl add_new_id ([], map (#1 o #1) inrs));
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   524
        val tye = map (fn ((v,rs),a) => (v, TVar((a,0),rs))) (inrs ~~ nms')
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   525
        val ctye = map (fn (v,T) => (v,ctyp_of sign T)) tye;
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   526
        fun varpairs([],[]) = []
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   527
          | varpairs((var as Var(v,T)) :: vars, b::bs) =
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   528
                let val T' = typ_subst_TVars tye T
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   529
                in (cterm_of sign (Var(v,T')),
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   530
                    cterm_of sign (Var((b,0),T'))) :: varpairs(vars,bs)
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   531
                end
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   532
          | varpairs _ = raise TERM("varpairs", []);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   533
    in instantiate (ctye, varpairs(vars,rev bs)) th end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   534
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   535
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   536
(*Standard form of object-rule: no hypotheses, Frees, or outer quantifiers;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   537
    all generality expressed by Vars having index 0.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   538
fun standard th =
1218
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   539
  let val {maxidx,...} = rep_thm th
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   540
  in  
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   541
    th |> implies_intr_hyps
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   542
    |> strip_shyps |> implies_intr_shyps
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   543
    |> forall_intr_frees |> forall_elim_vars (maxidx + 1)
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   544
    |> zero_var_indexes |> varifyT
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   545
  end;
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   546
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   547
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   548
(*Assume a new formula, read following the same conventions as axioms.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   549
  Generalizes over Free variables,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   550
  creates the assumption, and then strips quantifiers.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   551
  Example is [| ALL x:?A. ?P(x) |] ==> [| ?P(?a) |]
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   552
             [ !(A,P,a)[| ALL x:A. P(x) |] ==> [| P(a) |] ]    *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   553
fun assume_ax thy sP =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   554
    let val sign = sign_of thy
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   555
        val prop = Logic.close_form (term_of (read_cterm sign
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   556
                         (sP, propT)))
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   557
    in forall_elim_vars 0 (assume (cterm_of sign prop))  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   558
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   559
(*Resolution: exactly one resolvent must be produced.*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   560
fun tha RSN (i,thb) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   561
  case Sequence.chop (2, biresolution false [(false,tha)] i thb) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   562
      ([th],_) => th
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   563
    | ([],_)   => raise THM("RSN: no unifiers", i, [tha,thb])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   564
    |      _   => raise THM("RSN: multiple unifiers", i, [tha,thb]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   565
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   566
(*resolution: P==>Q, Q==>R gives P==>R. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   567
fun tha RS thb = tha RSN (1,thb);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   568
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   569
(*For joining lists of rules*)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   570
fun thas RLN (i,thbs) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   571
  let val resolve = biresolution false (map (pair false) thas) i
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   572
      fun resb thb = Sequence.list_of_s (resolve thb) handle THM _ => []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   573
  in  flat (map resb thbs)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   574
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   575
fun thas RL thbs = thas RLN (1,thbs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   576
11
d0e17c42dbb4 Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents: 0
diff changeset
   577
(*Resolve a list of rules against bottom_rl from right to left;
d0e17c42dbb4 Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents: 0
diff changeset
   578
  makes proof trees*)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   579
fun rls MRS bottom_rl =
11
d0e17c42dbb4 Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents: 0
diff changeset
   580
  let fun rs_aux i [] = bottom_rl
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   581
        | rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls)
11
d0e17c42dbb4 Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents: 0
diff changeset
   582
  in  rs_aux 1 rls  end;
d0e17c42dbb4 Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents: 0
diff changeset
   583
d0e17c42dbb4 Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents: 0
diff changeset
   584
(*As above, but for rule lists*)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   585
fun rlss MRL bottom_rls =
11
d0e17c42dbb4 Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents: 0
diff changeset
   586
  let fun rs_aux i [] = bottom_rls
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   587
        | rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss)
11
d0e17c42dbb4 Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents: 0
diff changeset
   588
  in  rs_aux 1 rlss  end;
d0e17c42dbb4 Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents: 0
diff changeset
   589
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   590
(*compose Q and [...,Qi,Q(i+1),...]==>R to [...,Q(i+1),...]==>R
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   591
  with no lifting or renaming!  Q may contain ==> or meta-quants
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   592
  ALWAYS deletes premise i *)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   593
fun compose(tha,i,thb) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   594
    Sequence.list_of_s (bicompose false (false,tha,0) i thb);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   595
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   596
(*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   597
fun tha COMP thb =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   598
    case compose(tha,1,thb) of
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   599
        [th] => th
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   600
      | _ =>   raise THM("COMP", 1, [tha,thb]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   601
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   602
(*Instantiate theorem th, reading instantiations under signature sg*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   603
fun read_instantiate_sg sg sinsts th =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   604
    let val ts = types_sorts th;
952
9e10962866b0 Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents: 949
diff changeset
   605
        val used = add_term_tvarnames(#prop(rep_thm th),[]);
9e10962866b0 Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents: 949
diff changeset
   606
    in  instantiate (read_insts sg ts ts used sinsts) th  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   607
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   608
(*Instantiate theorem th, reading instantiations under theory of th*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   609
fun read_instantiate sinsts th =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   610
    read_instantiate_sg (#sign (rep_thm th)) sinsts th;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   611
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   612
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   613
(*Left-to-right replacements: tpairs = [...,(vi,ti),...].
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   614
  Instantiates distinct Vars by terms, inferring type instantiations. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   615
local
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   616
  fun add_types ((ct,cu), (sign,tye)) =
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   617
    let val {sign=signt, t=t, T= T, ...} = rep_cterm ct
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   618
        and {sign=signu, t=u, T= U, ...} = rep_cterm cu
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   619
        val sign' = Sign.merge(sign, Sign.merge(signt, signu))
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   620
        val tye' = Type.unify (#tsig(Sign.rep_sg sign')) ((T,U), tye)
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   621
          handle Type.TUNIFY => raise TYPE("add_types", [T,U], [t,u])
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   622
    in  (sign', tye')  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   623
in
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   624
fun cterm_instantiate ctpairs0 th =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   625
  let val (sign,tye) = foldr add_types (ctpairs0, (#sign(rep_thm th),[]))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   626
      val tsig = #tsig(Sign.rep_sg sign);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   627
      fun instT(ct,cu) = let val inst = subst_TVars tye
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   628
                         in (cterm_fun inst ct, cterm_fun inst cu) end
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   629
      fun ctyp2 (ix,T) = (ix, ctyp_of sign T)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   630
  in  instantiate (map ctyp2 tye, map instT ctpairs0) th  end
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   631
  handle TERM _ =>
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   632
           raise THM("cterm_instantiate: incompatible signatures",0,[th])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   633
       | TYPE _ => raise THM("cterm_instantiate: types", 0, [th])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   634
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   635
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   636
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   637
(** theorem equality test is exported and used by BEST_FIRST **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   638
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   639
(*equality of theorems uses equality of signatures and
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   640
  the a-convertible test for terms*)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   641
fun eq_thm (th1,th2) =
1218
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   642
    let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   643
        and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   644
    in  Sign.eq_sg (sg1,sg2) andalso
1218
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   645
        eq_set (shyps1, shyps2) andalso
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   646
        aconvs(hyps1,hyps2) andalso
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   647
        prop1 aconv prop2
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   648
    end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   649
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   650
(*Do the two theorems have the same signature?*)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   651
fun eq_thm_sg (th1,th2) = Sign.eq_sg(#sign(rep_thm th1), #sign(rep_thm th2));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   652
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   653
(*Useful "distance" function for BEST_FIRST*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   654
val size_of_thm = size_of_term o #prop o rep_thm;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   655
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   656
1194
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   657
(** Mark Staples's weaker version of eq_thm: ignores variable renaming and
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   658
    (some) type variable renaming **)
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   659
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   660
 (* Can't use term_vars, because it sorts the resulting list of variable names.
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   661
    We instead need the unique list noramlised by the order of appearance
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   662
    in the term. *)
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   663
fun term_vars' (t as Var(v,T)) = [t]
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   664
  | term_vars' (Abs(_,_,b)) = term_vars' b
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   665
  | term_vars' (f$a) = (term_vars' f) @ (term_vars' a)
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   666
  | term_vars' _ = [];
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   667
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   668
fun forall_intr_vars th =
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   669
  let val {prop,sign,...} = rep_thm th;
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   670
      val vars = distinct (term_vars' prop);
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   671
  in forall_intr_list (map (cterm_of sign) vars) th end;
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   672
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   673
fun weak_eq_thm (tha,thb) = 
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   674
    eq_thm(forall_intr_vars (freezeT tha), forall_intr_vars (freezeT thb));
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   675
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   676
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   677
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   678
(*** Meta-Rewriting Rules ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   679
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   680
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   681
val reflexive_thm =
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 843
diff changeset
   682
  let val cx = cterm_of Sign.proto_pure (Var(("x",0),TVar(("'a",0),logicS)))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   683
  in Thm.reflexive cx end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   684
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   685
val symmetric_thm =
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 843
diff changeset
   686
  let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   687
  in standard(Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   688
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   689
val transitive_thm =
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 843
diff changeset
   690
  let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT)
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 843
diff changeset
   691
      val yz = read_cterm Sign.proto_pure ("y::'a::logic == z",propT)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   692
      val xythm = Thm.assume xy and yzthm = Thm.assume yz
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   693
  in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   694
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   695
(** Below, a "conversion" has type cterm -> thm **)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   696
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 843
diff changeset
   697
val refl_cimplies = reflexive (cterm_of Sign.proto_pure implies);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   698
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   699
(*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
214
ed6a3e2b1a33 added new parameter to the simplification tactics which indicates if
nipkow
parents: 211
diff changeset
   700
(*Do not rewrite flex-flex pairs*)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   701
fun goals_conv pred cv =
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   702
  let fun gconv i ct =
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   703
        let val (A,B) = Thm.dest_cimplies ct
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   704
            val (thA,j) = case term_of A of
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   705
                  Const("=?=",_)$_$_ => (reflexive A, i)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   706
                | _ => (if pred i then cv A else reflexive A, i+1)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   707
        in  combination (combination refl_cimplies thA) (gconv j B) end
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   708
        handle TERM _ => reflexive ct
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   709
  in gconv 1 end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   710
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   711
(*Use a conversion to transform a theorem*)
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   712
fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   713
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   714
(*rewriting conversion*)
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   715
fun rew_conv mode prover mss = rewrite_cterm mode mss prover;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   716
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   717
(*Rewrite a theorem*)
214
ed6a3e2b1a33 added new parameter to the simplification tactics which indicates if
nipkow
parents: 211
diff changeset
   718
fun rewrite_rule thms =
ed6a3e2b1a33 added new parameter to the simplification tactics which indicates if
nipkow
parents: 211
diff changeset
   719
  fconv_rule (rew_conv (true,false) (K(K None)) (Thm.mss_of thms));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   720
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   721
(*Rewrite the subgoals of a proof state (represented by a theorem) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   722
fun rewrite_goals_rule thms =
214
ed6a3e2b1a33 added new parameter to the simplification tactics which indicates if
nipkow
parents: 211
diff changeset
   723
  fconv_rule (goals_conv (K true) (rew_conv (true,false) (K(K None))
ed6a3e2b1a33 added new parameter to the simplification tactics which indicates if
nipkow
parents: 211
diff changeset
   724
             (Thm.mss_of thms)));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   725
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   726
(*Rewrite the subgoal of a proof state (represented by a theorem) *)
214
ed6a3e2b1a33 added new parameter to the simplification tactics which indicates if
nipkow
parents: 211
diff changeset
   727
fun rewrite_goal_rule mode prover mss i thm =
ed6a3e2b1a33 added new parameter to the simplification tactics which indicates if
nipkow
parents: 211
diff changeset
   728
  if 0 < i  andalso  i <= nprems_of thm
ed6a3e2b1a33 added new parameter to the simplification tactics which indicates if
nipkow
parents: 211
diff changeset
   729
  then fconv_rule (goals_conv (fn j => j=i) (rew_conv mode prover mss)) thm
ed6a3e2b1a33 added new parameter to the simplification tactics which indicates if
nipkow
parents: 211
diff changeset
   730
  else raise THM("rewrite_goal_rule",i,[thm]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   731
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   732
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   733
(** Derived rules mainly for METAHYPS **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   734
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   735
(*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   736
fun equal_abs_elim ca eqth =
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   737
  let val {sign=signa, t=a, ...} = rep_cterm ca
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   738
      and combth = combination eqth (reflexive ca)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   739
      val {sign,prop,...} = rep_thm eqth
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   740
      val (abst,absu) = Logic.dest_equals prop
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   741
      val cterm = cterm_of (Sign.merge (sign,signa))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   742
  in  transitive (symmetric (beta_conversion (cterm (abst$a))))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   743
           (transitive combth (beta_conversion (cterm (absu$a))))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   744
  end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   745
  handle THM _ => raise THM("equal_abs_elim", 0, [eqth]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   746
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   747
(*Calling equal_abs_elim with multiple terms*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   748
fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   749
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   750
local
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   751
  open Logic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   752
  val alpha = TVar(("'a",0), [])     (*  type ?'a::{}  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   753
  fun err th = raise THM("flexpair_inst: ", 0, [th])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   754
  fun flexpair_inst def th =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   755
    let val {prop = Const _ $ t $ u,  sign,...} = rep_thm th
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   756
        val cterm = cterm_of sign
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   757
        fun cvar a = cterm(Var((a,0),alpha))
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   758
        val def' = cterm_instantiate [(cvar"t", cterm t), (cvar"u", cterm u)]
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   759
                   def
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   760
    in  equal_elim def' th
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   761
    end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   762
    handle THM _ => err th | bind => err th
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   763
in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   764
val flexpair_intr = flexpair_inst (symmetric flexpair_def)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   765
and flexpair_elim = flexpair_inst flexpair_def
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   766
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   767
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   768
(*Version for flexflex pairs -- this supports lifting.*)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   769
fun flexpair_abs_elim_list cts =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   770
    flexpair_intr o equal_abs_elim_list cts o flexpair_elim;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   771
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   772
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   773
(*** Some useful meta-theorems ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   774
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   775
(*The rule V/V, obtains assumption solving for eresolve_tac*)
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 843
diff changeset
   776
val asm_rl = trivial(read_cterm Sign.proto_pure ("PROP ?psi",propT));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   777
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   778
(*Meta-level cut rule: [| V==>W; V |] ==> W *)
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 843
diff changeset
   779
val cut_rl = trivial(read_cterm Sign.proto_pure
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   780
        ("PROP ?psi ==> PROP ?theta", propT));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   781
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   782
(*Generalized elim rule for one conclusion; cut_rl with reversed premises:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   783
     [| PROP V;  PROP V ==> PROP W |] ==> PROP W *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   784
val revcut_rl =
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 843
diff changeset
   785
  let val V = read_cterm Sign.proto_pure ("PROP V", propT)
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 843
diff changeset
   786
      and VW = read_cterm Sign.proto_pure ("PROP V ==> PROP W", propT);
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   787
  in  standard (implies_intr V
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   788
                (implies_intr VW
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   789
                 (implies_elim (assume VW) (assume V))))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   790
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   791
668
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
   792
(*for deleting an unwanted assumption*)
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
   793
val thin_rl =
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 843
diff changeset
   794
  let val V = read_cterm Sign.proto_pure ("PROP V", propT)
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 843
diff changeset
   795
      and W = read_cterm Sign.proto_pure ("PROP W", propT);
668
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
   796
  in  standard (implies_intr V (implies_intr W (assume W)))
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
   797
  end;
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
   798
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   799
(* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   800
val triv_forall_equality =
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 843
diff changeset
   801
  let val V  = read_cterm Sign.proto_pure ("PROP V", propT)
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 843
diff changeset
   802
      and QV = read_cterm Sign.proto_pure ("!!x::'a. PROP V", propT)
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 843
diff changeset
   803
      and x  = read_cterm Sign.proto_pure ("x", TFree("'a",logicS));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   804
  in  standard (equal_intr (implies_intr QV (forall_elim x (assume QV)))
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   805
                           (implies_intr V  (forall_intr x (assume V))))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   806
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   807
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   808
end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   809
end;
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   810