src/Pure/drule.ML
author nipkow
Tue, 02 Sep 1997 16:10:26 +0200
changeset 3653 6d5b3d5ff132
parent 3575 4e9beacb5339
child 3766 8e1794c4e81b
permissions -rw-r--r--
Added Larry's equal_intr_rule
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
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    13
  val add_defs		: (string * string) list -> theory -> theory
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    14
  val add_defs_i	: (string * term) list -> theory -> theory
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    15
  val asm_rl		: thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    16
  val assume_ax		: theory -> string -> thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    17
  val COMP		: thm * thm -> thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    18
  val compose		: thm * int * thm -> thm list
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    19
  val cprems_of		: thm -> cterm list
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    20
  val cterm_instantiate	: (cterm*cterm)list -> thm -> thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    21
  val cut_rl		: thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    22
  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
    23
  val equal_abs_elim_list: cterm list -> thm -> thm
3653
6d5b3d5ff132 Added Larry's equal_intr_rule
nipkow
parents: 3575
diff changeset
    24
  val equal_intr_rule   : thm
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    25
  val eq_thm		: thm * thm -> bool
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    26
  val same_thm		: thm * thm -> bool
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    27
  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
    28
  val flexpair_abs_elim_list: cterm list -> thm -> thm
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    29
  val forall_intr_list	: cterm list -> thm -> thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    30
  val forall_intr_frees	: thm -> thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    31
  val forall_intr_vars	: thm -> thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    32
  val forall_elim_list	: cterm list -> thm -> thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    33
  val forall_elim_var	: int -> thm -> thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    34
  val forall_elim_vars	: int -> thm -> thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    35
  val implies_elim_list	: thm -> thm list -> thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    36
  val implies_intr_list	: cterm list -> thm -> thm
2004
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
    37
  val dest_implies      : cterm -> cterm * cterm
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    38
  val MRL		: thm list list * thm list -> thm list
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    39
  val MRS		: thm list * thm -> thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    40
  val read_instantiate	: (string*string)list -> thm -> thm
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
  val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    42
  val read_insts	:
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
    43
          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
    44
                  -> (indexname -> typ option) * (indexname -> sort option)
949
83c588d6fee9 Changed treatment of during type inference internally generated type
nipkow
parents: 922
diff changeset
    45
                  -> string list -> (string*string)list
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
    46
                  -> (indexname*ctyp)list * (cterm*cterm)list
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    47
  val reflexive_thm	: thm
2004
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
    48
  val refl_implies      : thm
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    49
  val revcut_rl		: thm
3555
5a720f6b9f38 added rewrite_thm;
wenzelm
parents: 3530
diff changeset
    50
  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
    51
        -> meta_simpset -> int -> thm -> thm
3575
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3555
diff changeset
    52
  val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3555
diff changeset
    53
  val rewrite_rule_aux	: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
3555
5a720f6b9f38 added rewrite_thm;
wenzelm
parents: 3530
diff changeset
    54
  val rewrite_thm	: bool * bool -> (meta_simpset -> thm -> thm option)
5a720f6b9f38 added rewrite_thm;
wenzelm
parents: 3530
diff changeset
    55
	-> meta_simpset -> thm -> thm
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    56
  val RS		: thm * thm -> thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    57
  val RSN		: thm * (int * thm) -> thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    58
  val RL		: thm list * thm list -> thm list
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    59
  val RLN		: thm list * (int * thm list) -> thm list
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    60
  val size_of_thm	: thm -> int
2004
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
    61
  val skip_flexpairs	: cterm -> cterm
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    62
  val standard		: thm -> thm
2004
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
    63
  val strip_imp_prems	: cterm -> cterm list
1756
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
    64
  val swap_prems_rl     : thm
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    65
  val symmetric_thm	: thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    66
  val thin_rl		: thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    67
  val transitive_thm	: thm
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
  val triv_forall_equality: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
  val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    70
  val zero_var_indexes	: thm -> thm
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
668
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
    73
1499
01fdd1ea6324 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
    74
structure Drule : DRULE =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
561
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
    77
(**** Extend Theories ****)
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
    78
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
    79
(** add constant definitions **)
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
    80
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
    81
(* all_axioms_of *)
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
    82
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
    83
(*results may contain duplicates!*)
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
    84
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
    85
fun ancestry_of thy =
2672
85d7e800d754 Replaced "flat" by the Basis Library function List.concat
paulson
parents: 2266
diff changeset
    86
  thy :: List.concat (map ancestry_of (parents_of thy));
561
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
    87
1237
45ac644b0052 adapted to new version of shyps-stuff;
wenzelm
parents: 1218
diff changeset
    88
val all_axioms_of =
2672
85d7e800d754 Replaced "flat" by the Basis Library function List.concat
paulson
parents: 2266
diff changeset
    89
  List.concat 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
    90
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
    91
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
    92
(* clash_types, clash_consts *)
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
    93
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
    94
(*check if types have common instance (ignoring sorts)*)
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
    95
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
    96
fun clash_types ty1 ty2 =
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
    97
  let
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
    98
    val ty1' = Type.varifyT ty1;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
    99
    val ty2' = incr_tvar (maxidx_of_typ ty1' + 1) (Type.varifyT ty2);
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   100
  in
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   101
    Type.raw_unify (ty1', ty2')
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   102
  end;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   103
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   104
fun clash_consts (c1, ty1) (c2, ty2) =
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   105
  c1 = c2 andalso clash_types ty1 ty2;
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
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   108
(* clash_defns *)
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   109
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   110
fun clash_defn c_ty (name, tm) =
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   111
  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
   112
    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
   113
  end handle TERM _ => None;
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
fun clash_defns c_ty axms =
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   116
  distinct (mapfilter (clash_defn c_ty) axms);
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
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   119
(* dest_defn *)
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   120
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   121
fun dest_defn tm =
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   122
  let
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   123
    fun err msg = raise_term msg [tm];
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   124
3530
d9ca80f0759c defs: allow conditions;
wenzelm
parents: 2672
diff changeset
   125
    val (lhs, rhs) = Logic.dest_equals (Logic.strip_imp_concl tm)
561
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   126
      handle TERM _ => err "Not a meta-equality (==)";
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   127
    val (head, args) = strip_comb lhs;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   128
    val (c, ty) = dest_Const head
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   129
      handle TERM _ => err "Head of lhs not a constant";
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   130
655
9748dbcd4157 minor change of occs_const in dest_defn;
wenzelm
parents: 641
diff changeset
   131
    fun occs_const (Const c_ty') = (c_ty' = (c, ty))
561
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   132
      | occs_const (Abs (_, _, t)) = occs_const t
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   133
      | occs_const (t $ u) = occs_const t orelse occs_const u
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   134
      | occs_const _ = false;
641
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   135
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   136
    val show_frees = commas_quote o map (fst o dest_Free);
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   137
    val show_tfrees = commas_quote o map fst;
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   138
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   139
    val lhs_dups = duplicates args;
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   140
    val rhs_extras = gen_rems (op =) (term_frees rhs, args);
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   141
    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
   142
  in
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   143
    if not (forall is_Free args) then
1906
4699a9058a4f Improved (?) wording of error message
paulson
parents: 1756
diff changeset
   144
      err "Arguments (on lhs) must be variables"
641
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   145
    else if not (null lhs_dups) then
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   146
      err ("Duplicate variables on lhs: " ^ show_frees lhs_dups)
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   147
    else if not (null rhs_extras) then
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   148
      err ("Extra variables on rhs: " ^ show_frees rhs_extras)
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   149
    else if not (null rhs_extrasT) then
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   150
      err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT)
561
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   151
    else if occs_const rhs then
655
9748dbcd4157 minor change of occs_const in dest_defn;
wenzelm
parents: 641
diff changeset
   152
      err ("Constant to be defined occurs on rhs")
561
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   153
    else (c, ty)
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   154
  end;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   155
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   156
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   157
(* check_defn *)
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   158
641
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   159
fun err_in_defn name msg =
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   160
  (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
   161
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   162
fun check_defn sign (axms, (name, tm)) =
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   163
  let
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   164
    fun show_const (c, ty) = quote (Pretty.string_of (Pretty.block
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   165
      [Pretty.str (c ^ " ::"), Pretty.brk 1, Sign.pretty_typ sign ty]));
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   166
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   167
    fun show_defn c (dfn, ty') = show_const (c, ty') ^ " in " ^ dfn;
1439
1f5949a43e82 improved printing of errors in 'defs';
wenzelm
parents: 1435
diff changeset
   168
    fun show_defns c = cat_lines o map (show_defn c);
561
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   169
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   170
    val (c, ty) = dest_defn tm
641
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   171
      handle TERM (msg, _) => err_in_defn name msg;
561
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   172
    val defns = clash_defns (c, ty) axms;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   173
  in
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   174
    if not (null defns) then
641
49fc43cd6a35 add_defs: improved error messages;
wenzelm
parents: 575
diff changeset
   175
      err_in_defn name ("Definition of " ^ show_const (c, ty) ^
1439
1f5949a43e82 improved printing of errors in 'defs';
wenzelm
parents: 1435
diff changeset
   176
        "\nclashes with " ^ show_defns c defns)
561
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   177
    else (name, tm) :: axms
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
(* add_defs *)
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   182
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   183
fun ext_defns prep_axm raw_axms thy =
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   184
  let
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   185
    val axms = map (prep_axm (sign_of thy)) raw_axms;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   186
    val all_axms = all_axioms_of thy;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   187
  in
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   188
    foldl (check_defn (sign_of thy)) (all_axms, axms);
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   189
    add_axioms_i axms thy
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   190
  end;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   191
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   192
val add_defs_i = ext_defns cert_axm;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   193
val add_defs = ext_defns read_axm;
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   194
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   195
95225e63ef02 added add_defs, add_defs_i;
wenzelm
parents: 400
diff changeset
   196
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
(**** More derived rules and operations on theorems ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
708
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   199
(** 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
   200
2004
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   201
(** SAME NAMES as in structure Logic: use compound identifiers! **)
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   202
1703
e22ad43bab5f moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents: 1596
diff changeset
   203
(*dest_implies for cterms. Note T=prop below*)
2004
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   204
fun dest_implies ct =
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   205
    case term_of ct of 
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   206
	(Const("==>", _) $ _ $ _) => 
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   207
	    let val (ct1,ct2) = dest_comb ct
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   208
	    in  (#2 (dest_comb ct1), ct2)  end	     
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   209
      | _ => raise TERM ("dest_implies", [term_of ct]) ;
1703
e22ad43bab5f moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents: 1596
diff changeset
   210
e22ad43bab5f moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents: 1596
diff changeset
   211
708
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   212
(*Discard flexflex pairs; return a cterm*)
2004
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   213
fun skip_flexpairs ct =
708
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   214
    case term_of ct of
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   215
	(Const("==>", _) $ (Const("=?=",_)$_$_) $ _) =>
2004
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   216
	    skip_flexpairs (#2 (dest_implies ct))
708
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   217
      | _ => ct;
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   218
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   219
(* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
2004
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   220
fun strip_imp_prems ct =
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   221
    let val (cA,cB) = dest_implies ct
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   222
    in  cA :: strip_imp_prems cB  end
708
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   223
    handle TERM _ => [];
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   224
2004
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   225
(* A1==>...An==>B  goes to B, where B is not an implication *)
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   226
fun strip_imp_concl ct =
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   227
    case term_of ct of (Const("==>", _) $ _ $ _) => 
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   228
	strip_imp_concl (#2 (dest_comb ct))
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   229
  | _ => ct;
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   230
708
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   231
(*The premises of a theorem, as a cterm list*)
2004
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   232
val cprems_of = strip_imp_prems o skip_flexpairs o cprop_of;
708
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   233
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   234
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   235
(** reading of instantiations **)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   236
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   237
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
   238
        | _ => 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
   239
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   240
fun absent ixn =
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   241
  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
   242
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   243
fun inst_failure ixn =
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   244
  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
   245
952
9e10962866b0 Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents: 949
diff changeset
   246
(* 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
   247
   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
   248
   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
   249
   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
   250
*)
949
83c588d6fee9 Changed treatment of during type inference internally generated type
nipkow
parents: 922
diff changeset
   251
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
   252
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
   253
    fun split([],tvs,vs) = (tvs,vs)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   254
      | 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
   255
                  "'"::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
   256
                | 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
   257
    val (tvs,vs) = split(insts,[],[]);
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   258
    fun readT((a,i),st) =
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   259
        let val ixn = ("'" ^ a,i);
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   260
            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
   261
            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
   262
        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
   263
           else inst_failure ixn
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   264
        end
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   265
    val tye = map readT tvs;
949
83c588d6fee9 Changed treatment of during type inference internally generated type
nipkow
parents: 922
diff changeset
   266
    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
   267
        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
   268
                      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
   269
                    | None => absent ixn;
949
83c588d6fee9 Changed treatment of during type inference internally generated type
nipkow
parents: 922
diff changeset
   270
            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
   271
            val cts' = (ixn,T,ct)::cts
9e10962866b0 Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents: 949
diff changeset
   272
            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
   273
            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
   274
        in (map inst cts',tye2 @ tye,used') end
949
83c588d6fee9 Changed treatment of during type inference internally generated type
nipkow
parents: 922
diff changeset
   275
    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
   276
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
   277
    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
   278
end;
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   279
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   280
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   281
(*** Find the type (sort) associated with a (T)Var or (T)Free in a term
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
     Used for establishing default types (of variables) and sorts (of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
     type variables) when reading another term.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
     Index -1 indicates that a (T)Free rather than a (T)Var is wanted.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
fun types_sorts thm =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
    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
   289
        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
   290
        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
   291
        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
   292
        val tvars = term_tvars big;
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   293
        val tfrees = term_tfrees big;
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   294
        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
   295
        fun sort(a,i) = if i<0 then assoc(tfrees,a) else assoc(tvars,(a,i));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
    in (typ,sort) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
(** Standardization of rules **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
(*Generalization over a list of variables, IGNORING bad ones*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
fun forall_intr_list [] th = th
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
  | forall_intr_list (y::ys) th =
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   303
        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
   304
        in  forall_intr y gth   handle THM _ =>  gth  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306
(*Generalization over all suitable Free variables*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   307
fun forall_intr_frees th =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   308
    let val {prop,sign,...} = rep_thm th
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   309
    in  forall_intr_list
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   310
         (map (cterm_of sign) (sort atless (term_frees prop)))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   311
         th
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   312
    end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   313
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   314
(*Replace outermost quantified variable by Var of given index.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   315
    Could clash with Vars already present.*)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   316
fun forall_elim_var i th =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   317
    let val {prop,sign,...} = rep_thm th
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   318
    in case prop of
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   319
          Const("all",_) $ Abs(a,T,_) =>
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   320
              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
   321
        | _ => raise THM("forall_elim_var", i, [th])
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   322
    end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
(*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
   325
fun forall_elim_vars i th =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   326
    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
   327
        handle THM _ => th;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   329
(*Specialization over a list of cterms*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   330
fun forall_elim_list cts th = foldr (uncurry forall_elim) (rev cts, th);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   331
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
(* maps [A1,...,An], B   to   [| A1;...;An |] ==> B  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   333
fun implies_intr_list cAs th = foldr (uncurry implies_intr) (cAs,th);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   334
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   335
(* maps [| A1;...;An |] ==> B and [A1,...,An]   to   B *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   336
fun implies_elim_list impth ths = foldl (uncurry implies_elim) (impth,ths);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   337
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   338
(*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
   339
fun zero_var_indexes th =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   340
    let val {prop,sign,...} = rep_thm th;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   341
        val vars = term_vars prop
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   342
        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
   343
        val inrs = add_term_tvars(prop,[]);
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   344
        val nms' = rev(foldl add_new_id ([], map (#1 o #1) inrs));
2266
82aef6857c5b Replaced map...~~ by ListPair.map
paulson
parents: 2180
diff changeset
   345
        val tye = ListPair.map (fn ((v,rs),a) => (v, TVar((a,0),rs)))
82aef6857c5b Replaced map...~~ by ListPair.map
paulson
parents: 2180
diff changeset
   346
	             (inrs, nms')
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   347
        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
   348
        fun varpairs([],[]) = []
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   349
          | 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
   350
                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
   351
                in (cterm_of sign (Var(v,T')),
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   352
                    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
   353
                end
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   354
          | varpairs _ = raise TERM("varpairs", []);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   355
    in instantiate (ctye, varpairs(vars,rev bs)) th end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   356
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   357
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   358
(*Standard form of object-rule: no hypotheses, Frees, or outer quantifiers;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   359
    all generality expressed by Vars having index 0.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   360
fun standard th =
1218
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   361
  let val {maxidx,...} = rep_thm th
1237
45ac644b0052 adapted to new version of shyps-stuff;
wenzelm
parents: 1218
diff changeset
   362
  in
1218
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   363
    th |> implies_intr_hyps
1412
2ab32768c996 Now "standard" compresses theorems (for sharing).
paulson
parents: 1241
diff changeset
   364
       |> forall_intr_frees |> forall_elim_vars (maxidx + 1)
1439
1f5949a43e82 improved printing of errors in 'defs';
wenzelm
parents: 1435
diff changeset
   365
       |> Thm.strip_shyps |> Thm.implies_intr_shyps
1412
2ab32768c996 Now "standard" compresses theorems (for sharing).
paulson
parents: 1241
diff changeset
   366
       |> zero_var_indexes |> Thm.varifyT |> Thm.compress
1218
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   367
  end;
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   368
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   369
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   370
(*Assume a new formula, read following the same conventions as axioms.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   371
  Generalizes over Free variables,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   372
  creates the assumption, and then strips quantifiers.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   373
  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
   374
             [ !(A,P,a)[| ALL x:A. P(x) |] ==> [| P(a) |] ]    *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   375
fun assume_ax thy sP =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   376
    let val sign = sign_of thy
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   377
        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
   378
                         (sP, propT)))
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   379
    in forall_elim_vars 0 (assume (cterm_of sign prop))  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   380
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   381
(*Resolution: exactly one resolvent must be produced.*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   382
fun tha RSN (i,thb) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   383
  case Sequence.chop (2, biresolution false [(false,tha)] i thb) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   384
      ([th],_) => th
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   385
    | ([],_)   => raise THM("RSN: no unifiers", i, [tha,thb])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   386
    |      _   => raise THM("RSN: multiple unifiers", i, [tha,thb]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   387
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   388
(*resolution: P==>Q, Q==>R gives P==>R. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   389
fun tha RS thb = tha RSN (1,thb);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   390
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   391
(*For joining lists of rules*)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   392
fun thas RLN (i,thbs) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   393
  let val resolve = biresolution false (map (pair false) thas) i
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   394
      fun resb thb = Sequence.list_of_s (resolve thb) handle THM _ => []
2672
85d7e800d754 Replaced "flat" by the Basis Library function List.concat
paulson
parents: 2266
diff changeset
   395
  in  List.concat (map resb thbs)  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   396
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   397
fun thas RL thbs = thas RLN (1,thbs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   398
11
d0e17c42dbb4 Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents: 0
diff changeset
   399
(*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
   400
  makes proof trees*)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   401
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
   402
  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
   403
        | 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
   404
  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
   405
d0e17c42dbb4 Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents: 0
diff changeset
   406
(*As above, but for rule lists*)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   407
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
   408
  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
   409
        | 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
   410
  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
   411
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   412
(*compose Q and [...,Qi,Q(i+1),...]==>R to [...,Q(i+1),...]==>R
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   413
  with no lifting or renaming!  Q may contain ==> or meta-quants
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   414
  ALWAYS deletes premise i *)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   415
fun compose(tha,i,thb) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   416
    Sequence.list_of_s (bicompose false (false,tha,0) i thb);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   417
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   418
(*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   419
fun tha COMP thb =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   420
    case compose(tha,1,thb) of
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   421
        [th] => th
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   422
      | _ =>   raise THM("COMP", 1, [tha,thb]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   423
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   424
(*Instantiate theorem th, reading instantiations under signature sg*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   425
fun read_instantiate_sg sg sinsts th =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   426
    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
   427
        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
   428
    in  instantiate (read_insts sg ts ts used sinsts) th  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   429
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   430
(*Instantiate theorem th, reading instantiations under theory of th*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   431
fun read_instantiate sinsts th =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   432
    read_instantiate_sg (#sign (rep_thm th)) sinsts th;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   433
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   434
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   435
(*Left-to-right replacements: tpairs = [...,(vi,ti),...].
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   436
  Instantiates distinct Vars by terms, inferring type instantiations. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   437
local
1435
aefcd255ed4a Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents: 1412
diff changeset
   438
  fun add_types ((ct,cu), (sign,tye,maxidx)) =
2152
76d5ed939545 Now uses Int.max instead of max
paulson
parents: 2004
diff changeset
   439
    let val {sign=signt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct
76d5ed939545 Now uses Int.max instead of max
paulson
parents: 2004
diff changeset
   440
        and {sign=signu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu;
76d5ed939545 Now uses Int.max instead of max
paulson
parents: 2004
diff changeset
   441
        val maxi = Int.max(maxidx, Int.max(maxt, maxu));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   442
        val sign' = Sign.merge(sign, Sign.merge(signt, signu))
1435
aefcd255ed4a Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents: 1412
diff changeset
   443
        val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) maxi tye (T,U)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   444
          handle Type.TUNIFY => raise TYPE("add_types", [T,U], [t,u])
1435
aefcd255ed4a Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents: 1412
diff changeset
   445
    in  (sign', tye', maxi')  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   446
in
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   447
fun cterm_instantiate ctpairs0 th =
1435
aefcd255ed4a Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents: 1412
diff changeset
   448
  let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th),[],0))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   449
      val tsig = #tsig(Sign.rep_sg sign);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   450
      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
   451
                         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
   452
      fun ctyp2 (ix,T) = (ix, ctyp_of sign T)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   453
  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
   454
  handle TERM _ =>
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   455
           raise THM("cterm_instantiate: incompatible signatures",0,[th])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   456
       | TYPE _ => raise THM("cterm_instantiate: types", 0, [th])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   457
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   458
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   459
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   460
(** theorem equality test is exported and used by BEST_FIRST **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   461
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   462
(*equality of theorems uses equality of signatures and
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   463
  the a-convertible test for terms*)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   464
fun eq_thm (th1,th2) =
1218
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   465
    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
   466
        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
   467
    in  Sign.eq_sg (sg1,sg2) andalso
2180
934572a94139 Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents: 2152
diff changeset
   468
        eq_set_sort (shyps1, shyps2) andalso
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   469
        aconvs(hyps1,hyps2) andalso
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   470
        prop1 aconv prop2
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   471
    end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   472
1241
bfc93c86f0a1 added same_sg and same_thm
clasohm
parents: 1237
diff changeset
   473
(*equality of theorems using similarity of signatures,
bfc93c86f0a1 added same_sg and same_thm
clasohm
parents: 1237
diff changeset
   474
  i.e. the theorems belong to the same theory but not necessarily to the same
bfc93c86f0a1 added same_sg and same_thm
clasohm
parents: 1237
diff changeset
   475
  version of this theory*)
bfc93c86f0a1 added same_sg and same_thm
clasohm
parents: 1237
diff changeset
   476
fun same_thm (th1,th2) =
bfc93c86f0a1 added same_sg and same_thm
clasohm
parents: 1237
diff changeset
   477
    let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1
bfc93c86f0a1 added same_sg and same_thm
clasohm
parents: 1237
diff changeset
   478
        and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2
bfc93c86f0a1 added same_sg and same_thm
clasohm
parents: 1237
diff changeset
   479
    in  Sign.same_sg (sg1,sg2) andalso
2180
934572a94139 Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents: 2152
diff changeset
   480
        eq_set_sort (shyps1, shyps2) andalso
1241
bfc93c86f0a1 added same_sg and same_thm
clasohm
parents: 1237
diff changeset
   481
        aconvs(hyps1,hyps2) andalso
bfc93c86f0a1 added same_sg and same_thm
clasohm
parents: 1237
diff changeset
   482
        prop1 aconv prop2
bfc93c86f0a1 added same_sg and same_thm
clasohm
parents: 1237
diff changeset
   483
    end;
bfc93c86f0a1 added same_sg and same_thm
clasohm
parents: 1237
diff changeset
   484
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   485
(*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
   486
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
   487
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   488
(*Useful "distance" function for BEST_FIRST*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   489
val size_of_thm = size_of_term o #prop o rep_thm;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   490
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   491
1194
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   492
(** 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
   493
    (some) type variable renaming **)
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   494
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   495
 (* 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
   496
    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
   497
    in the term. *)
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   498
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
   499
  | 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
   500
  | 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
   501
  | term_vars' _ = [];
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   502
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   503
fun forall_intr_vars th =
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   504
  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
   505
      val vars = distinct (term_vars' prop);
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   506
  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
   507
1237
45ac644b0052 adapted to new version of shyps-stuff;
wenzelm
parents: 1218
diff changeset
   508
fun weak_eq_thm (tha,thb) =
1194
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   509
    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
   510
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   511
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   512
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   513
(*** Meta-Rewriting Rules ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   514
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   515
val reflexive_thm =
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 843
diff changeset
   516
  let val cx = cterm_of Sign.proto_pure (Var(("x",0),TVar(("'a",0),logicS)))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   517
  in Thm.reflexive cx end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   518
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   519
val symmetric_thm =
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 843
diff changeset
   520
  let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   521
  in standard(Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   522
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   523
val transitive_thm =
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 843
diff changeset
   524
  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
   525
      val yz = read_cterm Sign.proto_pure ("y::'a::logic == z",propT)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   526
      val xythm = Thm.assume xy and yzthm = Thm.assume yz
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   527
  in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   528
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   529
(** 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
   530
2004
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   531
val refl_implies = reflexive (cterm_of Sign.proto_pure implies);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   532
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   533
(*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
   534
(*Do not rewrite flex-flex pairs*)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   535
fun goals_conv pred cv =
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   536
  let fun gconv i ct =
2004
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   537
        let val (A,B) = dest_implies ct
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   538
            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
   539
                  Const("=?=",_)$_$_ => (reflexive A, i)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   540
                | _ => (if pred i then cv A else reflexive A, i+1)
2004
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   541
        in  combination (combination refl_implies thA) (gconv j B) end
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   542
        handle TERM _ => reflexive ct
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   543
  in gconv 1 end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   544
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   545
(*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
   546
fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   547
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   548
(*rewriting conversion*)
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   549
fun rew_conv mode prover mss = rewrite_cterm mode mss prover;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   550
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   551
(*Rewrite a theorem*)
3575
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3555
diff changeset
   552
fun rewrite_rule_aux _ []   th = th
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3555
diff changeset
   553
  | rewrite_rule_aux prover thms th =
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3555
diff changeset
   554
      fconv_rule (rew_conv (true,false) prover (Thm.mss_of thms)) th;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   555
3555
5a720f6b9f38 added rewrite_thm;
wenzelm
parents: 3530
diff changeset
   556
fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss);
5a720f6b9f38 added rewrite_thm;
wenzelm
parents: 3530
diff changeset
   557
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   558
(*Rewrite the subgoals of a proof state (represented by a theorem) *)
3575
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3555
diff changeset
   559
fun rewrite_goals_rule_aux _ []   th = th
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3555
diff changeset
   560
  | rewrite_goals_rule_aux prover thms th =
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3555
diff changeset
   561
      fconv_rule (goals_conv (K true) (rew_conv (true, true) prover
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3555
diff changeset
   562
        (Thm.mss_of thms))) th;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   563
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   564
(*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
   565
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
   566
  if 0 < i  andalso  i <= nprems_of thm
ed6a3e2b1a33 added new parameter to the simplification tactics which indicates if
nipkow
parents: 211
diff changeset
   567
  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
   568
  else raise THM("rewrite_goal_rule",i,[thm]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   569
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   570
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   571
(** Derived rules mainly for METAHYPS **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   572
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   573
(*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   574
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
   575
  let val {sign=signa, t=a, ...} = rep_cterm ca
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   576
      and combth = combination eqth (reflexive ca)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   577
      val {sign,prop,...} = rep_thm eqth
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   578
      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
   579
      val cterm = cterm_of (Sign.merge (sign,signa))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   580
  in  transitive (symmetric (beta_conversion (cterm (abst$a))))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   581
           (transitive combth (beta_conversion (cterm (absu$a))))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   582
  end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   583
  handle THM _ => raise THM("equal_abs_elim", 0, [eqth]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   584
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   585
(*Calling equal_abs_elim with multiple terms*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   586
fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   587
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   588
local
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   589
  val alpha = TVar(("'a",0), [])     (*  type ?'a::{}  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   590
  fun err th = raise THM("flexpair_inst: ", 0, [th])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   591
  fun flexpair_inst def th =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   592
    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
   593
        val cterm = cterm_of sign
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   594
        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
   595
        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
   596
                   def
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   597
    in  equal_elim def' th
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   598
    end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   599
    handle THM _ => err th | bind => err th
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   600
in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   601
val flexpair_intr = flexpair_inst (symmetric flexpair_def)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   602
and flexpair_elim = flexpair_inst flexpair_def
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   603
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   604
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   605
(*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
   606
fun flexpair_abs_elim_list cts =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   607
    flexpair_intr o equal_abs_elim_list cts o flexpair_elim;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   608
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   609
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   610
(*** Some useful meta-theorems ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   611
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   612
(*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
   613
val asm_rl = trivial(read_cterm Sign.proto_pure ("PROP ?psi",propT));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   614
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   615
(*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
   616
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
   617
        ("PROP ?psi ==> PROP ?theta", propT));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   618
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   619
(*Generalized elim rule for one conclusion; cut_rl with reversed premises:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   620
     [| PROP V;  PROP V ==> PROP W |] ==> PROP W *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   621
val revcut_rl =
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 843
diff changeset
   622
  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
   623
      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
   624
  in  standard (implies_intr V
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   625
                (implies_intr VW
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   626
                 (implies_elim (assume VW) (assume V))))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   627
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   628
668
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
   629
(*for deleting an unwanted assumption*)
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
   630
val thin_rl =
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 843
diff changeset
   631
  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
   632
      and W = read_cterm Sign.proto_pure ("PROP W", propT);
668
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
   633
  in  standard (implies_intr V (implies_intr W (assume W)))
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
   634
  end;
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
   635
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   636
(* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   637
val triv_forall_equality =
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 843
diff changeset
   638
  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
   639
      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
   640
      and x  = read_cterm Sign.proto_pure ("x", TFree("'a",logicS));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   641
  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
   642
                           (implies_intr V  (forall_intr x (assume V))))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   643
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   644
1756
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   645
(* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==>
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   646
   (PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi)
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   647
   `thm COMP swap_prems_rl' swaps the first two premises of `thm'
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   648
*)
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   649
val swap_prems_rl =
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   650
  let val cmajor = read_cterm Sign.proto_pure
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   651
            ("PROP PhiA ==> PROP PhiB ==> PROP Psi", propT);
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   652
      val major = assume cmajor;
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   653
      val cminor1 = read_cterm Sign.proto_pure  ("PROP PhiA", propT);
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   654
      val minor1 = assume cminor1;
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   655
      val cminor2 = read_cterm Sign.proto_pure  ("PROP PhiB", propT);
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   656
      val minor2 = assume cminor2;
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   657
  in standard
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   658
       (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   659
         (implies_elim (implies_elim major minor1) minor2))))
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   660
  end;
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   661
3653
6d5b3d5ff132 Added Larry's equal_intr_rule
nipkow
parents: 3575
diff changeset
   662
(* [| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |]
6d5b3d5ff132 Added Larry's equal_intr_rule
nipkow
parents: 3575
diff changeset
   663
   ==> PROP ?phi == PROP ?psi
6d5b3d5ff132 Added Larry's equal_intr_rule
nipkow
parents: 3575
diff changeset
   664
   Introduction rule for == using ==> not meta-hyps.
6d5b3d5ff132 Added Larry's equal_intr_rule
nipkow
parents: 3575
diff changeset
   665
*)
6d5b3d5ff132 Added Larry's equal_intr_rule
nipkow
parents: 3575
diff changeset
   666
val equal_intr_rule =
6d5b3d5ff132 Added Larry's equal_intr_rule
nipkow
parents: 3575
diff changeset
   667
  let val PQ = read_cterm Sign.proto_pure ("PROP phi ==> PROP psi", propT)
6d5b3d5ff132 Added Larry's equal_intr_rule
nipkow
parents: 3575
diff changeset
   668
      and QP = read_cterm Sign.proto_pure ("PROP psi ==> PROP phi", propT)
6d5b3d5ff132 Added Larry's equal_intr_rule
nipkow
parents: 3575
diff changeset
   669
  in  equal_intr (assume PQ) (assume QP)
6d5b3d5ff132 Added Larry's equal_intr_rule
nipkow
parents: 3575
diff changeset
   670
      |> implies_intr QP
6d5b3d5ff132 Added Larry's equal_intr_rule
nipkow
parents: 3575
diff changeset
   671
      |> implies_intr PQ
6d5b3d5ff132 Added Larry's equal_intr_rule
nipkow
parents: 3575
diff changeset
   672
      |> standard
6d5b3d5ff132 Added Larry's equal_intr_rule
nipkow
parents: 3575
diff changeset
   673
  end;
6d5b3d5ff132 Added Larry's equal_intr_rule
nipkow
parents: 3575
diff changeset
   674
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   675
end;
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   676
1499
01fdd1ea6324 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   677
open Drule;