src/Pure/drule.ML
author wenzelm
Thu, 27 Nov 1997 19:36:08 +0100
changeset 4313 03353197410c
parent 4285 05af145a61d4
child 4440 9ed4098074bc
permissions -rw-r--r--
removed same_thm;
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
3766
8e1794c4e81b moved theory stuff (add_defs etc.) to theory.ML;
wenzelm
parents: 3653
diff changeset
     6
Derived rules and other operations on theorems.
0
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 =
3766
8e1794c4e81b moved theory stuff (add_defs etc.) to theory.ML;
wenzelm
parents: 3653
diff changeset
    12
sig
4285
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    13
  val dest_implies      : cterm -> cterm * cterm
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    14
  val skip_flexpairs	: cterm -> cterm
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    15
  val strip_imp_prems	: cterm -> cterm list
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    16
  val cprems_of		: thm -> cterm list
4285
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    17
  val read_insts	:
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    18
          Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    19
                  -> (indexname -> typ option) * (indexname -> sort option)
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    20
                  -> string list -> (string*string)list
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    21
                  -> (indexname*ctyp)list * (cterm*cterm)list
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    22
  val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    23
  val forall_intr_list	: cterm list -> thm -> thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    24
  val forall_intr_frees	: thm -> thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    25
  val forall_intr_vars	: thm -> thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    26
  val forall_elim_list	: cterm list -> thm -> thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    27
  val forall_elim_var	: int -> thm -> thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    28
  val forall_elim_vars	: int -> thm -> thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    29
  val implies_elim_list	: thm -> thm list -> thm
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    30
  val implies_intr_list	: cterm list -> thm -> thm
4285
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    31
  val zero_var_indexes	: thm -> thm
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    32
  val standard		: thm -> thm
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    33
  val assume_ax		: theory -> string -> thm
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    34
  val RSN		: thm * (int * thm) -> thm
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    35
  val RS		: thm * thm -> thm
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    36
  val RLN		: thm list * (int * thm list) -> thm list
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    37
  val RL		: thm list * thm list -> thm list
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    38
  val MRS		: thm list * thm -> thm
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    39
  val MRL		: thm list list * thm list -> thm list
4285
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    40
  val compose		: thm * int * thm -> thm list
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    41
  val COMP		: thm * thm -> thm
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
  val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
4285
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    43
  val read_instantiate	: (string*string)list -> thm -> thm
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    44
  val cterm_instantiate	: (cterm*cterm)list -> thm -> thm
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    45
  val weak_eq_thm	: thm * thm -> bool
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    46
  val eq_thm_sg		: thm * thm -> bool
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    47
  val size_of_thm	: thm -> int
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    48
  val reflexive_thm	: thm
4285
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    49
  val symmetric_thm	: thm
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    50
  val transitive_thm	: thm
2004
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
    51
  val refl_implies      : thm
3575
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3555
diff changeset
    52
  val rewrite_rule_aux	: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
3555
5a720f6b9f38 added rewrite_thm;
wenzelm
parents: 3530
diff changeset
    53
  val rewrite_thm	: bool * bool -> (meta_simpset -> thm -> thm option)
5a720f6b9f38 added rewrite_thm;
wenzelm
parents: 3530
diff changeset
    54
	-> meta_simpset -> thm -> thm
4285
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    55
  val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    56
  val rewrite_goal_rule	: bool * bool -> (meta_simpset -> thm -> thm option)
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    57
        -> meta_simpset -> int -> thm -> thm
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    58
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    59
  val equal_abs_elim	: cterm  -> thm -> thm
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    60
  val equal_abs_elim_list: cterm list -> thm -> thm
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    61
  val flexpair_abs_elim_list: cterm list -> thm -> thm
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    62
  val asm_rl		: thm
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    63
  val cut_rl		: thm
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    64
  val revcut_rl		: thm
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    65
  val thin_rl		: thm
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    66
  val triv_forall_equality: thm
1756
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
    67
  val swap_prems_rl     : thm
4285
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    68
  val equal_intr_rule   : thm
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
    69
  val instantiate': ctyp option list -> cterm option list -> thm -> thm
3766
8e1794c4e81b moved theory stuff (add_defs etc.) to theory.ML;
wenzelm
parents: 3653
diff changeset
    70
end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
1499
01fdd1ea6324 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
    72
structure Drule : DRULE =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
3991
4cb2f2422695 ProtoPure.thy;
wenzelm
parents: 3766
diff changeset
    75
708
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
    76
(** 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
    77
2004
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
    78
(** 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
    79
1703
e22ad43bab5f moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents: 1596
diff changeset
    80
(*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
    81
fun dest_implies ct =
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
    82
    case term_of ct of 
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
    83
	(Const("==>", _) $ _ $ _) => 
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
    84
	    let val (ct1,ct2) = dest_comb ct
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
    85
	    in  (#2 (dest_comb ct1), ct2)  end	     
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
    86
      | _ => raise TERM ("dest_implies", [term_of ct]) ;
1703
e22ad43bab5f moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents: 1596
diff changeset
    87
e22ad43bab5f moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents: 1596
diff changeset
    88
708
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
    89
(*Discard flexflex pairs; return a cterm*)
2004
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
    90
fun skip_flexpairs ct =
708
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
    91
    case term_of ct of
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    92
	(Const("==>", _) $ (Const("=?=",_)$_$_) $ _) =>
2004
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
    93
	    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
    94
      | _ => ct;
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
    95
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
    96
(* 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
    97
fun strip_imp_prems ct =
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
    98
    let val (cA,cB) = dest_implies ct
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
    99
    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
   100
    handle TERM _ => [];
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   101
2004
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   102
(* 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
   103
fun strip_imp_concl ct =
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   104
    case term_of ct of (Const("==>", _) $ _ $ _) => 
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   105
	strip_imp_concl (#2 (dest_comb ct))
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   106
  | _ => ct;
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   107
708
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   108
(*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
   109
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
   110
8422e50adce0 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents: 668
diff changeset
   111
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   112
(** reading of instantiations **)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   113
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   114
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
   115
        | _ => 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
   116
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   117
fun absent ixn =
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   118
  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
   119
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   120
fun inst_failure ixn =
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   121
  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
   122
952
9e10962866b0 Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents: 949
diff changeset
   123
(* 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
   124
   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
   125
   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
   126
   composition of implicit type instantiations (parameter tye) superfluous.
4281
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   127
949
83c588d6fee9 Changed treatment of during type inference internally generated type
nipkow
parents: 922
diff changeset
   128
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
   129
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
   130
    fun split([],tvs,vs) = (tvs,vs)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   131
      | 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
   132
                  "'"::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
   133
                | 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
   134
    val (tvs,vs) = split(insts,[],[]);
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   135
    fun readT((a,i),st) =
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   136
        let val ixn = ("'" ^ a,i);
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   137
            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
   138
            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
   139
        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
   140
           else inst_failure ixn
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   141
        end
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   142
    val tye = map readT tvs;
949
83c588d6fee9 Changed treatment of during type inference internally generated type
nipkow
parents: 922
diff changeset
   143
    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
   144
        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
   145
                      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
   146
                    | None => absent ixn;
949
83c588d6fee9 Changed treatment of during type inference internally generated type
nipkow
parents: 922
diff changeset
   147
            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
   148
            val cts' = (ixn,T,ct)::cts
9e10962866b0 Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents: 949
diff changeset
   149
            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
   150
            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
   151
        in (map inst cts',tye2 @ tye,used') end
949
83c588d6fee9 Changed treatment of during type inference internally generated type
nipkow
parents: 922
diff changeset
   152
    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
   153
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
   154
    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
   155
end;
4281
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   156
*)
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   157
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   158
fun read_insts sign (rtypes,rsorts) (types,sorts) used insts =
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   159
let val {tsig,...} = Sign.rep_sg sign
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   160
    fun split([],tvs,vs) = (tvs,vs)
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   161
      | split((sv,st)::l,tvs,vs) = (case explode sv of
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   162
                  "'"::cs => split(l,(indexname cs,st)::tvs,vs)
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   163
                | cs => split(l,tvs,(indexname cs,st)::vs));
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   164
    val (tvs,vs) = split(insts,[],[]);
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   165
    fun readT((a,i),st) =
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   166
        let val ixn = ("'" ^ a,i);
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   167
            val S = case rsorts ixn of Some S => S | None => absent ixn;
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   168
            val T = Sign.read_typ (sign,sorts) st;
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   169
        in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   170
           else inst_failure ixn
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   171
        end
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   172
    val tye = map readT tvs;
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   173
    fun mkty(ixn,st) = (case rtypes ixn of
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   174
                          Some T => (ixn,(st,typ_subst_TVars tye T))
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   175
                        | None => absent ixn);
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   176
    val ixnsTs = map mkty vs;
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   177
    val ixns = map fst ixnsTs
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   178
    and sTs  = map snd ixnsTs
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   179
    val (cts,tye2) = read_def_cterms(sign,types,sorts) used false sTs;
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   180
    fun mkcVar(ixn,T) =
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   181
        let val U = typ_subst_TVars tye2 T
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   182
        in cterm_of sign (Var(ixn,U)) end
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   183
    val ixnTs = ListPair.zip(ixns, map snd sTs)
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   184
in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) (tye2 @ tye),
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   185
    ListPair.zip(map mkcVar ixnTs,cts))
6c6073b13600 Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents: 4270
diff changeset
   186
end;
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   187
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   188
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   189
(*** Find the type (sort) associated with a (T)Var or (T)Free in a term
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
     Used for establishing default types (of variables) and sorts (of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
     type variables) when reading another term.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
     Index -1 indicates that a (T)Free rather than a (T)Var is wanted.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
fun types_sorts thm =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
    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
   197
        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
   198
        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
   199
        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
   200
        val tvars = term_tvars big;
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   201
        val tfrees = term_tfrees big;
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   202
        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
   203
        fun sort(a,i) = if i<0 then assoc(tfrees,a) else assoc(tvars,(a,i));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
    in (typ,sort) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
(** Standardization of rules **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
(*Generalization over a list of variables, IGNORING bad ones*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
fun forall_intr_list [] th = th
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
  | forall_intr_list (y::ys) th =
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   211
        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
   212
        in  forall_intr y gth   handle THM _ =>  gth  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
(*Generalization over all suitable Free variables*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
fun forall_intr_frees th =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
    let val {prop,sign,...} = rep_thm th
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
    in  forall_intr_list
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   218
         (map (cterm_of sign) (sort atless (term_frees prop)))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
         th
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
    end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
(*Replace outermost quantified variable by Var of given index.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
    Could clash with Vars already present.*)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   224
fun forall_elim_var i th =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
    let val {prop,sign,...} = rep_thm th
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
    in case prop of
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   227
          Const("all",_) $ Abs(a,T,_) =>
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   228
              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
   229
        | _ => raise THM("forall_elim_var", i, [th])
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
    end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
(*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
   233
fun forall_elim_vars i th =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
    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
   235
        handle THM _ => th;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
(*Specialization over a list of cterms*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
fun forall_elim_list cts th = foldr (uncurry forall_elim) (rev cts, th);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
(* maps [A1,...,An], B   to   [| A1;...;An |] ==> B  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
fun implies_intr_list cAs th = foldr (uncurry implies_intr) (cAs,th);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
(* maps [| A1;...;An |] ==> B and [A1,...,An]   to   B *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
fun implies_elim_list impth ths = foldl (uncurry implies_elim) (impth,ths);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
(*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
   247
fun zero_var_indexes th =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
    let val {prop,sign,...} = rep_thm th;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
        val vars = term_vars prop
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
        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
   251
        val inrs = add_term_tvars(prop,[]);
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   252
        val nms' = rev(foldl add_new_id ([], map (#1 o #1) inrs));
2266
82aef6857c5b Replaced map...~~ by ListPair.map
paulson
parents: 2180
diff changeset
   253
        val tye = ListPair.map (fn ((v,rs),a) => (v, TVar((a,0),rs)))
82aef6857c5b Replaced map...~~ by ListPair.map
paulson
parents: 2180
diff changeset
   254
	             (inrs, nms')
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   255
        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
   256
        fun varpairs([],[]) = []
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   257
          | 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
   258
                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
   259
                in (cterm_of sign (Var(v,T')),
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   260
                    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
   261
                end
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   262
          | varpairs _ = raise TERM("varpairs", []);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
    in instantiate (ctye, varpairs(vars,rev bs)) th end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
(*Standard form of object-rule: no hypotheses, Frees, or outer quantifiers;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
    all generality expressed by Vars having index 0.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
fun standard th =
1218
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   269
  let val {maxidx,...} = rep_thm th
1237
45ac644b0052 adapted to new version of shyps-stuff;
wenzelm
parents: 1218
diff changeset
   270
  in
1218
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   271
    th |> implies_intr_hyps
1412
2ab32768c996 Now "standard" compresses theorems (for sharing).
paulson
parents: 1241
diff changeset
   272
       |> forall_intr_frees |> forall_elim_vars (maxidx + 1)
1439
1f5949a43e82 improved printing of errors in 'defs';
wenzelm
parents: 1435
diff changeset
   273
       |> Thm.strip_shyps |> Thm.implies_intr_shyps
1412
2ab32768c996 Now "standard" compresses theorems (for sharing).
paulson
parents: 1241
diff changeset
   274
       |> zero_var_indexes |> Thm.varifyT |> Thm.compress
1218
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   275
  end;
59ed8ef1a3a1 modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents: 1194
diff changeset
   276
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   278
(*Assume a new formula, read following the same conventions as axioms.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
  Generalizes over Free variables,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
  creates the assumption, and then strips quantifiers.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
  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
   282
             [ !(A,P,a)[| ALL x:A. P(x) |] ==> [| P(a) |] ]    *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
fun assume_ax thy sP =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
    let val sign = sign_of thy
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   285
        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
   286
                         (sP, propT)))
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   287
    in forall_elim_vars 0 (assume (cterm_of sign prop))  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   289
(*Resolution: exactly one resolvent must be produced.*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
fun tha RSN (i,thb) =
4270
957c887b89b5 changed Sequence interface (now Seq, in seq.ML);
wenzelm
parents: 4057
diff changeset
   291
  case Seq.chop (2, biresolution false [(false,tha)] i thb) of
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
      ([th],_) => th
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
    | ([],_)   => raise THM("RSN: no unifiers", i, [tha,thb])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
    |      _   => raise THM("RSN: multiple unifiers", i, [tha,thb]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
(*resolution: P==>Q, Q==>R gives P==>R. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
fun tha RS thb = tha RSN (1,thb);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
(*For joining lists of rules*)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   300
fun thas RLN (i,thbs) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
  let val resolve = biresolution false (map (pair false) thas) i
4270
957c887b89b5 changed Sequence interface (now Seq, in seq.ML);
wenzelm
parents: 4057
diff changeset
   302
      fun resb thb = Seq.list_of (resolve thb) handle THM _ => []
2672
85d7e800d754 Replaced "flat" by the Basis Library function List.concat
paulson
parents: 2266
diff changeset
   303
  in  List.concat (map resb thbs)  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
fun thas RL thbs = thas RLN (1,thbs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306
11
d0e17c42dbb4 Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents: 0
diff changeset
   307
(*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
   308
  makes proof trees*)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   309
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
   310
  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
   311
        | 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
   312
  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
   313
d0e17c42dbb4 Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents: 0
diff changeset
   314
(*As above, but for rule lists*)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   315
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
   316
  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
   317
        | 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
   318
  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
   319
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   320
(*compose Q and [...,Qi,Q(i+1),...]==>R to [...,Q(i+1),...]==>R
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
  with no lifting or renaming!  Q may contain ==> or meta-quants
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   322
  ALWAYS deletes premise i *)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   323
fun compose(tha,i,thb) =
4270
957c887b89b5 changed Sequence interface (now Seq, in seq.ML);
wenzelm
parents: 4057
diff changeset
   324
    Seq.list_of (bicompose false (false,tha,0) i thb);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   325
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   326
(*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   327
fun tha COMP thb =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
    case compose(tha,1,thb) of
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   329
        [th] => th
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   330
      | _ =>   raise THM("COMP", 1, [tha,thb]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   331
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
(*Instantiate theorem th, reading instantiations under signature sg*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   333
fun read_instantiate_sg sg sinsts th =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   334
    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
   335
        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
   336
    in  instantiate (read_insts sg ts ts used sinsts) th  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   337
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   338
(*Instantiate theorem th, reading instantiations under theory of th*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   339
fun read_instantiate sinsts th =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   340
    read_instantiate_sg (#sign (rep_thm th)) sinsts th;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   341
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   342
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   343
(*Left-to-right replacements: tpairs = [...,(vi,ti),...].
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   344
  Instantiates distinct Vars by terms, inferring type instantiations. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   345
local
1435
aefcd255ed4a Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents: 1412
diff changeset
   346
  fun add_types ((ct,cu), (sign,tye,maxidx)) =
2152
76d5ed939545 Now uses Int.max instead of max
paulson
parents: 2004
diff changeset
   347
    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
   348
        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
   349
        val maxi = Int.max(maxidx, Int.max(maxt, maxu));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   350
        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
   351
        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
   352
          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
   353
    in  (sign', tye', maxi')  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   354
in
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   355
fun cterm_instantiate ctpairs0 th =
1435
aefcd255ed4a Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents: 1412
diff changeset
   356
  let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th),[],0))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   357
      val tsig = #tsig(Sign.rep_sg sign);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   358
      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
   359
                         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
   360
      fun ctyp2 (ix,T) = (ix, ctyp_of sign T)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   361
  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
   362
  handle TERM _ =>
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   363
           raise THM("cterm_instantiate: incompatible signatures",0,[th])
4057
edd8cb346109 propagate exn msg;
wenzelm
parents: 4016
diff changeset
   364
       | TYPE (msg, _, _) => raise THM("cterm_instantiate: " ^ msg, 0, [th])
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   365
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   366
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   367
4016
90aebb69c04e eq_thm moved to thm.ML;
wenzelm
parents: 3991
diff changeset
   368
(** theorem equality **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   369
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   370
(*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
   371
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
   372
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   373
(*Useful "distance" function for BEST_FIRST*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   374
val size_of_thm = size_of_term o #prop o rep_thm;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   375
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   376
1194
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   377
(** 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
   378
    (some) type variable renaming **)
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   379
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   380
 (* 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
   381
    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
   382
    in the term. *)
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   383
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
   384
  | 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
   385
  | 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
   386
  | term_vars' _ = [];
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   387
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   388
fun forall_intr_vars th =
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   389
  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
   390
      val vars = distinct (term_vars' prop);
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   391
  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
   392
1237
45ac644b0052 adapted to new version of shyps-stuff;
wenzelm
parents: 1218
diff changeset
   393
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
   394
    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
   395
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   396
563ecd14c1d8 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents: 952
diff changeset
   397
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   398
(*** Meta-Rewriting Rules ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   399
4016
90aebb69c04e eq_thm moved to thm.ML;
wenzelm
parents: 3991
diff changeset
   400
fun store_thm name thm = PureThy.smart_store_thm (name, standard thm);
90aebb69c04e eq_thm moved to thm.ML;
wenzelm
parents: 3991
diff changeset
   401
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   402
val reflexive_thm =
3991
4cb2f2422695 ProtoPure.thy;
wenzelm
parents: 3766
diff changeset
   403
  let val cx = cterm_of (sign_of ProtoPure.thy) (Var(("x",0),TVar(("'a",0),logicS)))
4016
90aebb69c04e eq_thm moved to thm.ML;
wenzelm
parents: 3991
diff changeset
   404
  in store_thm "reflexive" (Thm.reflexive cx) end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   405
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   406
val symmetric_thm =
3991
4cb2f2422695 ProtoPure.thy;
wenzelm
parents: 3766
diff changeset
   407
  let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT)
4016
90aebb69c04e eq_thm moved to thm.ML;
wenzelm
parents: 3991
diff changeset
   408
  in store_thm "symmetric" (Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   409
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   410
val transitive_thm =
3991
4cb2f2422695 ProtoPure.thy;
wenzelm
parents: 3766
diff changeset
   411
  let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT)
4cb2f2422695 ProtoPure.thy;
wenzelm
parents: 3766
diff changeset
   412
      val yz = read_cterm (sign_of ProtoPure.thy) ("y::'a::logic == z",propT)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   413
      val xythm = Thm.assume xy and yzthm = Thm.assume yz
4016
90aebb69c04e eq_thm moved to thm.ML;
wenzelm
parents: 3991
diff changeset
   414
  in store_thm "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   415
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   416
(** 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
   417
3991
4cb2f2422695 ProtoPure.thy;
wenzelm
parents: 3766
diff changeset
   418
val refl_implies = reflexive (cterm_of (sign_of ProtoPure.thy) implies);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   419
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   420
(*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
   421
(*Do not rewrite flex-flex pairs*)
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   422
fun goals_conv pred cv =
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   423
  let fun gconv i ct =
2004
3411fe560611 New operations on cterms. Now same names as in Logic
paulson
parents: 1906
diff changeset
   424
        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
   425
            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
   426
                  Const("=?=",_)$_$_ => (reflexive A, i)
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   427
                | _ => (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
   428
        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
   429
        handle TERM _ => reflexive ct
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   430
  in gconv 1 end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   431
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   432
(*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
   433
fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   434
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   435
(*rewriting conversion*)
229
4002c4cd450c Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents: 214
diff changeset
   436
fun rew_conv mode prover mss = rewrite_cterm mode mss prover;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   437
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   438
(*Rewrite a theorem*)
3575
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3555
diff changeset
   439
fun rewrite_rule_aux _ []   th = th
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3555
diff changeset
   440
  | rewrite_rule_aux prover thms th =
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3555
diff changeset
   441
      fconv_rule (rew_conv (true,false) prover (Thm.mss_of thms)) th;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   442
3555
5a720f6b9f38 added rewrite_thm;
wenzelm
parents: 3530
diff changeset
   443
fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss);
5a720f6b9f38 added rewrite_thm;
wenzelm
parents: 3530
diff changeset
   444
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   445
(*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
   446
fun rewrite_goals_rule_aux _ []   th = th
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3555
diff changeset
   447
  | rewrite_goals_rule_aux prover thms th =
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3555
diff changeset
   448
      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
   449
        (Thm.mss_of thms))) th;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   450
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   451
(*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
   452
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
   453
  if 0 < i  andalso  i <= nprems_of thm
ed6a3e2b1a33 added new parameter to the simplification tactics which indicates if
nipkow
parents: 211
diff changeset
   454
  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
   455
  else raise THM("rewrite_goal_rule",i,[thm]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   456
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   457
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   458
(** Derived rules mainly for METAHYPS **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   459
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   460
(*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   461
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
   462
  let val {sign=signa, t=a, ...} = rep_cterm ca
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   463
      and combth = combination eqth (reflexive ca)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   464
      val {sign,prop,...} = rep_thm eqth
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   465
      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
   466
      val cterm = cterm_of (Sign.merge (sign,signa))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   467
  in  transitive (symmetric (beta_conversion (cterm (abst$a))))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   468
           (transitive combth (beta_conversion (cterm (absu$a))))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   469
  end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   470
  handle THM _ => raise THM("equal_abs_elim", 0, [eqth]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   471
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   472
(*Calling equal_abs_elim with multiple terms*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   473
fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   474
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   475
local
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   476
  val alpha = TVar(("'a",0), [])     (*  type ?'a::{}  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   477
  fun err th = raise THM("flexpair_inst: ", 0, [th])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   478
  fun flexpair_inst def th =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   479
    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
   480
        val cterm = cterm_of sign
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   481
        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
   482
        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
   483
                   def
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   484
    in  equal_elim def' th
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   485
    end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   486
    handle THM _ => err th | bind => err th
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   487
in
3991
4cb2f2422695 ProtoPure.thy;
wenzelm
parents: 3766
diff changeset
   488
val flexpair_intr = flexpair_inst (symmetric ProtoPure.flexpair_def)
4cb2f2422695 ProtoPure.thy;
wenzelm
parents: 3766
diff changeset
   489
and flexpair_elim = flexpair_inst ProtoPure.flexpair_def
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   490
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   491
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   492
(*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
   493
fun flexpair_abs_elim_list cts =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   494
    flexpair_intr o equal_abs_elim_list cts o flexpair_elim;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   495
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   496
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   497
(*** Some useful meta-theorems ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   498
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   499
(*The rule V/V, obtains assumption solving for eresolve_tac*)
4016
90aebb69c04e eq_thm moved to thm.ML;
wenzelm
parents: 3991
diff changeset
   500
val asm_rl =
90aebb69c04e eq_thm moved to thm.ML;
wenzelm
parents: 3991
diff changeset
   501
  store_thm "asm_rl" (trivial(read_cterm (sign_of ProtoPure.thy) ("PROP ?psi",propT)));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   502
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   503
(*Meta-level cut rule: [| V==>W; V |] ==> W *)
4016
90aebb69c04e eq_thm moved to thm.ML;
wenzelm
parents: 3991
diff changeset
   504
val cut_rl =
90aebb69c04e eq_thm moved to thm.ML;
wenzelm
parents: 3991
diff changeset
   505
  store_thm "cut_rl"
90aebb69c04e eq_thm moved to thm.ML;
wenzelm
parents: 3991
diff changeset
   506
    (trivial(read_cterm (sign_of ProtoPure.thy) ("PROP ?psi ==> PROP ?theta", propT)));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   507
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   508
(*Generalized elim rule for one conclusion; cut_rl with reversed premises:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   509
     [| PROP V;  PROP V ==> PROP W |] ==> PROP W *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   510
val revcut_rl =
3991
4cb2f2422695 ProtoPure.thy;
wenzelm
parents: 3766
diff changeset
   511
  let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
4cb2f2422695 ProtoPure.thy;
wenzelm
parents: 3766
diff changeset
   512
      and VW = read_cterm (sign_of ProtoPure.thy) ("PROP V ==> PROP W", propT);
4016
90aebb69c04e eq_thm moved to thm.ML;
wenzelm
parents: 3991
diff changeset
   513
  in
90aebb69c04e eq_thm moved to thm.ML;
wenzelm
parents: 3991
diff changeset
   514
    store_thm "revcut_rl"
90aebb69c04e eq_thm moved to thm.ML;
wenzelm
parents: 3991
diff changeset
   515
      (implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V))))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   516
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   517
668
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
   518
(*for deleting an unwanted assumption*)
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
   519
val thin_rl =
3991
4cb2f2422695 ProtoPure.thy;
wenzelm
parents: 3766
diff changeset
   520
  let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
4cb2f2422695 ProtoPure.thy;
wenzelm
parents: 3766
diff changeset
   521
      and W = read_cterm (sign_of ProtoPure.thy) ("PROP W", propT);
4016
90aebb69c04e eq_thm moved to thm.ML;
wenzelm
parents: 3991
diff changeset
   522
  in  store_thm "thin_rl" (implies_intr V (implies_intr W (assume W)))
668
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
   523
  end;
0d0923eb0f0d Pure/drule/thin_rl: new
lcp
parents: 655
diff changeset
   524
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   525
(* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   526
val triv_forall_equality =
3991
4cb2f2422695 ProtoPure.thy;
wenzelm
parents: 3766
diff changeset
   527
  let val V  = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
4cb2f2422695 ProtoPure.thy;
wenzelm
parents: 3766
diff changeset
   528
      and QV = read_cterm (sign_of ProtoPure.thy) ("!!x::'a. PROP V", propT)
4cb2f2422695 ProtoPure.thy;
wenzelm
parents: 3766
diff changeset
   529
      and x  = read_cterm (sign_of ProtoPure.thy) ("x", TFree("'a",logicS));
4016
90aebb69c04e eq_thm moved to thm.ML;
wenzelm
parents: 3991
diff changeset
   530
  in
90aebb69c04e eq_thm moved to thm.ML;
wenzelm
parents: 3991
diff changeset
   531
    store_thm "triv_forall_equality"
90aebb69c04e eq_thm moved to thm.ML;
wenzelm
parents: 3991
diff changeset
   532
      (equal_intr (implies_intr QV (forall_elim x (assume QV)))
90aebb69c04e eq_thm moved to thm.ML;
wenzelm
parents: 3991
diff changeset
   533
        (implies_intr V  (forall_intr x (assume V))))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   534
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   535
1756
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   536
(* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==>
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   537
   (PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi)
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   538
   `thm COMP swap_prems_rl' swaps the first two premises of `thm'
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   539
*)
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   540
val swap_prems_rl =
3991
4cb2f2422695 ProtoPure.thy;
wenzelm
parents: 3766
diff changeset
   541
  let val cmajor = read_cterm (sign_of ProtoPure.thy)
1756
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   542
            ("PROP PhiA ==> PROP PhiB ==> PROP Psi", propT);
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   543
      val major = assume cmajor;
3991
4cb2f2422695 ProtoPure.thy;
wenzelm
parents: 3766
diff changeset
   544
      val cminor1 = read_cterm (sign_of ProtoPure.thy)  ("PROP PhiA", propT);
1756
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   545
      val minor1 = assume cminor1;
3991
4cb2f2422695 ProtoPure.thy;
wenzelm
parents: 3766
diff changeset
   546
      val cminor2 = read_cterm (sign_of ProtoPure.thy)  ("PROP PhiB", propT);
1756
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   547
      val minor2 = assume cminor2;
4016
90aebb69c04e eq_thm moved to thm.ML;
wenzelm
parents: 3991
diff changeset
   548
  in store_thm "swap_prems_rl"
1756
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   549
       (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   550
         (implies_elim (implies_elim major minor1) minor2))))
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   551
  end;
978ee7ededdd Added swap_prems_rl
nipkow
parents: 1703
diff changeset
   552
3653
6d5b3d5ff132 Added Larry's equal_intr_rule
nipkow
parents: 3575
diff changeset
   553
(* [| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |]
6d5b3d5ff132 Added Larry's equal_intr_rule
nipkow
parents: 3575
diff changeset
   554
   ==> PROP ?phi == PROP ?psi
6d5b3d5ff132 Added Larry's equal_intr_rule
nipkow
parents: 3575
diff changeset
   555
   Introduction rule for == using ==> not meta-hyps.
6d5b3d5ff132 Added Larry's equal_intr_rule
nipkow
parents: 3575
diff changeset
   556
*)
6d5b3d5ff132 Added Larry's equal_intr_rule
nipkow
parents: 3575
diff changeset
   557
val equal_intr_rule =
3991
4cb2f2422695 ProtoPure.thy;
wenzelm
parents: 3766
diff changeset
   558
  let val PQ = read_cterm (sign_of ProtoPure.thy) ("PROP phi ==> PROP psi", propT)
4cb2f2422695 ProtoPure.thy;
wenzelm
parents: 3766
diff changeset
   559
      and QP = read_cterm (sign_of ProtoPure.thy) ("PROP psi ==> PROP phi", propT)
4016
90aebb69c04e eq_thm moved to thm.ML;
wenzelm
parents: 3991
diff changeset
   560
  in
90aebb69c04e eq_thm moved to thm.ML;
wenzelm
parents: 3991
diff changeset
   561
    store_thm "equal_intr_rule"
90aebb69c04e eq_thm moved to thm.ML;
wenzelm
parents: 3991
diff changeset
   562
      (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP))))
3653
6d5b3d5ff132 Added Larry's equal_intr_rule
nipkow
parents: 3575
diff changeset
   563
  end;
6d5b3d5ff132 Added Larry's equal_intr_rule
nipkow
parents: 3575
diff changeset
   564
4285
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   565
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   566
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   567
(** instantiate' rule **)
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   568
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   569
(* collect vars *)
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   570
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   571
val add_tvarsT = foldl_atyps (fn (vs, TVar v) => v ins vs | (vs, _) => vs);
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   572
val add_tvars = foldl_types add_tvarsT;
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   573
val add_vars = foldl_aterms (fn (vs, Var v) => v ins vs | (vs, _) => vs);
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   574
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   575
fun tvars_of thm = rev (add_tvars ([], #prop (Thm.rep_thm thm)));
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   576
fun vars_of thm = rev (add_vars ([], #prop (Thm.rep_thm thm)));
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   577
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   578
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   579
(* instantiate by left-to-right occurrence of variables *)
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   580
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   581
fun instantiate' cTs cts thm =
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   582
  let
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   583
    fun err msg =
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   584
      raise TYPE ("instantiate': " ^ msg,
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   585
        mapfilter (apsome Thm.typ_of) cTs,
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   586
        mapfilter (apsome Thm.term_of) cts);
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   587
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   588
    fun inst_of (v, ct) =
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   589
      (Thm.cterm_of (#sign (Thm.rep_cterm ct)) (Var v), ct)
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   590
        handle TYPE (msg, _, _) => err msg;
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   591
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   592
    fun zip_vars _ [] = []
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   593
      | zip_vars (_ :: vs) (None :: opt_ts) = zip_vars vs opt_ts
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   594
      | zip_vars (v :: vs) (Some t :: opt_ts) = (v, t) :: zip_vars vs opt_ts
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   595
      | zip_vars [] _ = err "more instantiations than variables in thm";
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   596
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   597
    (*instantiate types first!*)
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   598
    val thm' =
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   599
      if forall is_none cTs then thm
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   600
      else Thm.instantiate (zip_vars (map fst (tvars_of thm)) cTs, []) thm;
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   601
    in
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   602
      if forall is_none cts then thm'
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   603
      else Thm.instantiate ([], map inst_of (zip_vars (vars_of thm') cts)) thm'
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   604
    end;
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   605
05af145a61d4 cleaned signature;
wenzelm
parents: 4281
diff changeset
   606
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   607
end;
252
7532f95d7f44 removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents: 229
diff changeset
   608
1499
01fdd1ea6324 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   609
open Drule;