src/HOL/Tools/TFL/rules.ML
author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 37678 0040bafffdef
child 38549 d0385f2764d8
permissions -rw-r--r--
tuned titles
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Tools/TFL/rules.ML
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     2
    Author:     Konrad Slind, Cambridge University Computer Laboratory
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     3
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 26928
diff changeset
     4
Emulation of HOL inference rules for TFL.
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     5
*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     6
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     7
signature RULES =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     8
sig
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     9
  val dest_thm: thm -> term list * term
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    10
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    11
  (* Inference rules *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    12
  val REFL: cterm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    13
  val ASSUME: cterm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    14
  val MP: thm -> thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    15
  val MATCH_MP: thm -> thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    16
  val CONJUNCT1: thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    17
  val CONJUNCT2: thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    18
  val CONJUNCTS: thm -> thm list
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    19
  val DISCH: cterm -> thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    20
  val UNDISCH: thm  -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    21
  val SPEC: cterm -> thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    22
  val ISPEC: cterm -> thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    23
  val ISPECL: cterm list -> thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    24
  val GEN: cterm -> thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    25
  val GENL: cterm list -> thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    26
  val LIST_CONJ: thm list -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    27
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    28
  val SYM: thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    29
  val DISCH_ALL: thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    30
  val FILTER_DISCH_ALL: (term -> bool) -> thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    31
  val SPEC_ALL: thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    32
  val GEN_ALL: thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    33
  val IMP_TRANS: thm -> thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    34
  val PROVE_HYP: thm -> thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    35
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    36
  val CHOOSE: cterm * thm -> thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    37
  val EXISTS: cterm * cterm -> thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    38
  val EXISTL: cterm list -> thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    39
  val IT_EXISTS: (cterm*cterm) list -> thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    40
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    41
  val EVEN_ORS: thm list -> thm list
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    42
  val DISJ_CASESL: thm -> thm list -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    43
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    44
  val list_beta_conv: cterm -> cterm list -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    45
  val SUBS: thm list -> thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    46
  val simpl_conv: simpset -> thm list -> cterm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    47
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    48
  val rbeta: thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    49
(* For debugging my isabelle solver in the conditional rewriter *)
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32603
diff changeset
    50
  val term_ref: term list Unsynchronized.ref
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32603
diff changeset
    51
  val thm_ref: thm list Unsynchronized.ref
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32603
diff changeset
    52
  val ss_ref: simpset list Unsynchronized.ref
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32603
diff changeset
    53
  val tracing: bool Unsynchronized.ref
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    54
  val CONTEXT_REWRITE_RULE: term * term list * thm * thm list
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    55
                             -> thm -> thm * term list
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    56
  val RIGHT_ASSOC: thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    57
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    58
  val prove: bool -> cterm * tactic -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    59
end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    60
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    61
structure Rules: RULES =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    62
struct
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    63
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    64
structure S = USyntax;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    65
structure U = Utils;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    66
structure D = Dcterm;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    67
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    68
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    69
fun RULES_ERR func mesg = U.ERR {module = "Rules", func = func, mesg = mesg};
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    70
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    71
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    72
fun cconcl thm = D.drop_prop (#prop (Thm.crep_thm thm));
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    73
fun chyps thm = map D.drop_prop (#hyps (Thm.crep_thm thm));
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    74
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    75
fun dest_thm thm =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    76
  let val {prop,hyps,...} = Thm.rep_thm thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    77
  in (map HOLogic.dest_Trueprop hyps, HOLogic.dest_Trueprop prop) end
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    78
  handle TERM _ => raise RULES_ERR "dest_thm" "missing Trueprop";
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    79
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    80
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    81
(* Inference rules *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    82
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    83
(*---------------------------------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    84
 *        Equality (one step)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    85
 *---------------------------------------------------------------------------*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    86
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    87
fun REFL tm = Thm.reflexive tm RS meta_eq_to_obj_eq
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    88
  handle THM (msg, _, _) => raise RULES_ERR "REFL" msg;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    89
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    90
fun SYM thm = thm RS sym
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    91
  handle THM (msg, _, _) => raise RULES_ERR "SYM" msg;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    92
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    93
fun ALPHA thm ctm1 =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    94
  let
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    95
    val ctm2 = Thm.cprop_of thm;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    96
    val ctm2_eq = Thm.reflexive ctm2;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    97
    val ctm1_eq = Thm.reflexive ctm1;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    98
  in Thm.equal_elim (Thm.transitive ctm2_eq ctm1_eq) thm end
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    99
  handle THM (msg, _, _) => raise RULES_ERR "ALPHA" msg;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   100
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   101
fun rbeta th =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   102
  (case D.strip_comb (cconcl th) of
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   103
    (_, [l, r]) => Thm.transitive th (Thm.beta_conversion false r)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   104
  | _ => raise RULES_ERR "rbeta" "");
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   105
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   106
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   107
(*----------------------------------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   108
 *        Implication and the assumption list
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   109
 *
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   110
 * Assumptions get stuck on the meta-language assumption list. Implications
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   111
 * are in the object language, so discharging an assumption "A" from theorem
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   112
 * "B" results in something that looks like "A --> B".
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   113
 *---------------------------------------------------------------------------*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   114
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   115
fun ASSUME ctm = Thm.assume (D.mk_prop ctm);
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   116
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   117
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   118
(*---------------------------------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   119
 * Implication in TFL is -->. Meta-language implication (==>) is only used
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   120
 * in the implementation of some of the inference rules below.
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   121
 *---------------------------------------------------------------------------*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   122
fun MP th1 th2 = th2 RS (th1 RS mp)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   123
  handle THM (msg, _, _) => raise RULES_ERR "MP" msg;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   124
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   125
(*forces the first argument to be a proposition if necessary*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   126
fun DISCH tm thm = Thm.implies_intr (D.mk_prop tm) thm COMP impI
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   127
  handle THM (msg, _, _) => raise RULES_ERR "DISCH" msg;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   128
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   129
fun DISCH_ALL thm = fold_rev DISCH (#hyps (Thm.crep_thm thm)) thm;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   130
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   131
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   132
fun FILTER_DISCH_ALL P thm =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   133
 let fun check tm = P (#t (Thm.rep_cterm tm))
33339
d41f77196338 eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   134
 in  fold_rev (fn tm => fn th => if check tm then DISCH tm th else th) (chyps thm) thm
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   135
 end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   136
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   137
fun UNDISCH thm =
36617
ed8083930203 UNDISCH/DISJ_CASESL: eliminated slightly odd Thm.legacy_freezeT -- these rules appear to be applied to thms with fixed types only;
wenzelm
parents: 36615
diff changeset
   138
   let val tm = D.mk_prop (#1 (D.dest_imp (cconcl thm)))
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   139
   in Thm.implies_elim (thm RS mp) (ASSUME tm) end
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   140
   handle U.ERR _ => raise RULES_ERR "UNDISCH" ""
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   141
     | THM _ => raise RULES_ERR "UNDISCH" "";
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   142
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   143
fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   144
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   145
fun IMP_TRANS th1 th2 = th2 RS (th1 RS Thms.imp_trans)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   146
  handle THM (msg, _, _) => raise RULES_ERR "IMP_TRANS" msg;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   147
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   148
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   149
(*----------------------------------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   150
 *        Conjunction
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   151
 *---------------------------------------------------------------------------*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   152
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   153
fun CONJUNCT1 thm = thm RS conjunct1
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   154
  handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT1" msg;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   155
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   156
fun CONJUNCT2 thm = thm RS conjunct2
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   157
  handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT2" msg;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   158
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   159
fun CONJUNCTS th = CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th) handle U.ERR _ => [th];
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   160
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   161
fun LIST_CONJ [] = raise RULES_ERR "LIST_CONJ" "empty list"
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   162
  | LIST_CONJ [th] = th
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   163
  | LIST_CONJ (th :: rst) = MP (MP (conjI COMP (impI RS impI)) th) (LIST_CONJ rst)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   164
      handle THM (msg, _, _) => raise RULES_ERR "LIST_CONJ" msg;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   165
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   166
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   167
(*----------------------------------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   168
 *        Disjunction
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   169
 *---------------------------------------------------------------------------*)
26626
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   170
local val thy = Thm.theory_of_thm disjI1
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   171
      val prop = Thm.prop_of disjI1
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 26928
diff changeset
   172
      val [P,Q] = OldTerm.term_vars prop
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   173
      val disj1 = Thm.forall_intr (Thm.cterm_of thy Q) disjI1
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   174
in
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36617
diff changeset
   175
fun DISJ1 thm tm = thm RS (Thm.forall_elim (D.drop_prop tm) disj1)
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   176
  handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   177
end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   178
26626
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   179
local val thy = Thm.theory_of_thm disjI2
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   180
      val prop = Thm.prop_of disjI2
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 26928
diff changeset
   181
      val [P,Q] = OldTerm.term_vars prop
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   182
      val disj2 = Thm.forall_intr (Thm.cterm_of thy P) disjI2
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   183
in
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36617
diff changeset
   184
fun DISJ2 tm thm = thm RS (Thm.forall_elim (D.drop_prop tm) disj2)
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   185
  handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   186
end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   187
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   188
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   189
(*----------------------------------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   190
 *
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   191
 *                   A1 |- M1, ..., An |- Mn
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   192
 *     ---------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   193
 *     [A1 |- M1 \/ ... \/ Mn, ..., An |- M1 \/ ... \/ Mn]
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   194
 *
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   195
 *---------------------------------------------------------------------------*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   196
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   197
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   198
fun EVEN_ORS thms =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   199
  let fun blue ldisjs [] _ = []
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   200
        | blue ldisjs (th::rst) rdisjs =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   201
            let val tail = tl rdisjs
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   202
                val rdisj_tl = D.list_mk_disj tail
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   203
            in fold_rev DISJ2 ldisjs (DISJ1 th rdisj_tl)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   204
               :: blue (ldisjs @ [cconcl th]) rst tail
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   205
            end handle U.ERR _ => [fold_rev DISJ2 ldisjs th]
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   206
   in blue [] thms (map cconcl thms) end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   207
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   208
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   209
(*----------------------------------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   210
 *
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   211
 *         A |- P \/ Q   B,P |- R    C,Q |- R
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   212
 *     ---------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   213
 *                     A U B U C |- R
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   214
 *
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   215
 *---------------------------------------------------------------------------*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   216
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   217
fun DISJ_CASES th1 th2 th3 =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   218
  let
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   219
    val c = D.drop_prop (cconcl th1);
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   220
    val (disj1, disj2) = D.dest_disj c;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   221
    val th2' = DISCH disj1 th2;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   222
    val th3' = DISCH disj2 th3;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   223
  in
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   224
    th3' RS (th2' RS (th1 RS Thms.tfl_disjE))
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   225
      handle THM (msg, _, _) => raise RULES_ERR "DISJ_CASES" msg
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   226
  end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   227
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   228
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   229
(*-----------------------------------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   230
 *
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   231
 *       |- A1 \/ ... \/ An     [A1 |- M, ..., An |- M]
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   232
 *     ---------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   233
 *                           |- M
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   234
 *
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   235
 * Note. The list of theorems may be all jumbled up, so we have to
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   236
 * first organize it to align with the first argument (the disjunctive
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   237
 * theorem).
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   238
 *---------------------------------------------------------------------------*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   239
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   240
fun organize eq =    (* a bit slow - analogous to insertion sort *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   241
 let fun extract a alist =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   242
     let fun ex (_,[]) = raise RULES_ERR "organize" "not a permutation.1"
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   243
           | ex(left,h::t) = if (eq h a) then (h,rev left@t) else ex(h::left,t)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   244
     in ex ([],alist)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   245
     end
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   246
     fun place [] [] = []
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   247
       | place (a::rst) alist =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   248
           let val (item,next) = extract a alist
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   249
           in item::place rst next
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   250
           end
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   251
       | place _ _ = raise RULES_ERR "organize" "not a permutation.2"
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   252
 in place
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   253
 end;
36617
ed8083930203 UNDISCH/DISJ_CASESL: eliminated slightly odd Thm.legacy_freezeT -- these rules appear to be applied to thms with fixed types only;
wenzelm
parents: 36615
diff changeset
   254
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   255
fun DISJ_CASESL disjth thl =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   256
   let val c = cconcl disjth
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   257
       fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   258
                                       aconv term_of atm)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   259
                              (#hyps(rep_thm th))
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   260
       val tml = D.strip_disj c
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   261
       fun DL th [] = raise RULES_ERR "DISJ_CASESL" "no cases"
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   262
         | DL th [th1] = PROVE_HYP th th1
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   263
         | DL th [th1,th2] = DISJ_CASES th th1 th2
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   264
         | DL th (th1::rst) =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   265
            let val tm = #2(D.dest_disj(D.drop_prop(cconcl th)))
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   266
             in DISJ_CASES th th1 (DL (ASSUME tm) rst) end
36617
ed8083930203 UNDISCH/DISJ_CASESL: eliminated slightly odd Thm.legacy_freezeT -- these rules appear to be applied to thms with fixed types only;
wenzelm
parents: 36615
diff changeset
   267
   in DL disjth (organize eq tml thl)
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   268
   end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   269
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   270
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   271
(*----------------------------------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   272
 *        Universals
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   273
 *---------------------------------------------------------------------------*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   274
local (* this is fragile *)
26626
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   275
      val thy = Thm.theory_of_thm spec
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   276
      val prop = Thm.prop_of spec
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 26928
diff changeset
   277
      val x = hd (tl (OldTerm.term_vars prop))
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   278
      val cTV = ctyp_of thy (type_of x)
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36617
diff changeset
   279
      val gspec = Thm.forall_intr (cterm_of thy x) spec
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   280
in
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   281
fun SPEC tm thm =
26626
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   282
   let val gspec' = instantiate ([(cTV, Thm.ctyp_of_term tm)], []) gspec
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36617
diff changeset
   283
   in thm RS (Thm.forall_elim tm gspec') end
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   284
end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   285
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   286
fun SPEC_ALL thm = fold SPEC (#1(D.strip_forall(cconcl thm))) thm;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   287
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   288
val ISPEC = SPEC
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   289
val ISPECL = fold ISPEC;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   290
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   291
(* Not optimized! Too complicated. *)
26626
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   292
local val thy = Thm.theory_of_thm allI
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   293
      val prop = Thm.prop_of allI
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 26928
diff changeset
   294
      val [P] = OldTerm.add_term_vars (prop, [])
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   295
      fun cty_theta s = map (fn (i, (S, ty)) => (ctyp_of s (TVar (i, S)), ctyp_of s ty))
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   296
      fun ctm_theta s = map (fn (i, (_, tm2)) =>
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   297
                             let val ctm2 = cterm_of s tm2
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   298
                             in (cterm_of s (Var(i,#T(rep_cterm ctm2))), ctm2)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   299
                             end)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   300
      fun certify s (ty_theta,tm_theta) =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   301
        (cty_theta s (Vartab.dest ty_theta),
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   302
         ctm_theta s (Vartab.dest tm_theta))
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   303
in
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   304
fun GEN v th =
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36617
diff changeset
   305
   let val gth = Thm.forall_intr v th
26626
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   306
       val thy = Thm.theory_of_thm gth
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   307
       val Const("all",_)$Abs(x,ty,rst) = Thm.prop_of gth
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   308
       val P' = Abs(x,ty, HOLogic.dest_Trueprop rst)  (* get rid of trueprop *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   309
       val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty);
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   310
       val allI2 = instantiate (certify thy theta) allI
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   311
       val thm = Thm.implies_elim allI2 gth
26626
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   312
       val tp $ (A $ Abs(_,_,M)) = Thm.prop_of thm
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   313
       val prop' = tp $ (A $ Abs(x,ty,M))
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   314
   in ALPHA thm (cterm_of thy prop')
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   315
   end
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   316
end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   317
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   318
val GENL = fold_rev GEN;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   319
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   320
fun GEN_ALL thm =
26626
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   321
   let val thy = Thm.theory_of_thm thm
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   322
       val prop = Thm.prop_of thm
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   323
       val tycheck = cterm_of thy
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 26928
diff changeset
   324
       val vlist = map tycheck (OldTerm.add_term_vars (prop, []))
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   325
  in GENL vlist thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   326
  end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   327
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   328
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   329
fun MATCH_MP th1 th2 =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   330
   if (D.is_forall (D.drop_prop(cconcl th1)))
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   331
   then MATCH_MP (th1 RS spec) th2
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   332
   else MP th1 th2;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   333
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   334
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   335
(*----------------------------------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   336
 *        Existentials
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   337
 *---------------------------------------------------------------------------*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   338
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   339
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   340
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   341
(*---------------------------------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   342
 * Existential elimination
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   343
 *
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   344
 *      A1 |- ?x.t[x]   ,   A2, "t[v]" |- t'
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   345
 *      ------------------------------------     (variable v occurs nowhere)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   346
 *                A1 u A2 |- t'
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   347
 *
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   348
 *---------------------------------------------------------------------------*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   349
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   350
fun CHOOSE (fvar, exth) fact =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   351
  let
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   352
    val lam = #2 (D.dest_comb (D.drop_prop (cconcl exth)))
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   353
    val redex = D.capply lam fvar
26626
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   354
    val thy = Thm.theory_of_cterm redex
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   355
    val t$u = Thm.term_of redex
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   356
    val residue = Thm.cterm_of thy (Term.betapply (t, u))
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   357
  in
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   358
    GEN fvar (DISCH residue fact) RS (exth RS Thms.choose_thm)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   359
      handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   360
  end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   361
26626
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   362
local val thy = Thm.theory_of_thm exI
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   363
      val prop = Thm.prop_of exI
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 26928
diff changeset
   364
      val [P,x] = OldTerm.term_vars prop
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   365
in
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   366
fun EXISTS (template,witness) thm =
26626
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   367
   let val thy = Thm.theory_of_thm thm
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   368
       val prop = Thm.prop_of thm
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   369
       val P' = cterm_of thy P
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   370
       val x' = cterm_of thy x
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   371
       val abstr = #2 (D.dest_comb template)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   372
   in
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   373
   thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   374
     handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   375
   end
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   376
end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   377
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   378
(*----------------------------------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   379
 *
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   380
 *         A |- M
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   381
 *   -------------------   [v_1,...,v_n]
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   382
 *    A |- ?v1...v_n. M
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   383
 *
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   384
 *---------------------------------------------------------------------------*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   385
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   386
fun EXISTL vlist th =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   387
  fold_rev (fn v => fn thm => EXISTS(D.mk_exists(v,cconcl thm), v) thm)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   388
           vlist th;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   389
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   390
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   391
(*----------------------------------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   392
 *
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   393
 *       A |- M[x_1,...,x_n]
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   394
 *   ----------------------------   [(x |-> y)_1,...,(x |-> y)_n]
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   395
 *       A |- ?y_1...y_n. M
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   396
 *
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   397
 *---------------------------------------------------------------------------*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   398
(* Could be improved, but needs "subst_free" for certified terms *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   399
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   400
fun IT_EXISTS blist th =
26626
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   401
   let val thy = Thm.theory_of_thm th
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   402
       val tych = cterm_of thy
26626
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   403
       val blist' = map (pairself Thm.term_of) blist
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   404
       fun ex v M  = cterm_of thy (S.mk_exists{Bvar=v,Body = M})
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   405
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   406
  in
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   407
  fold_rev (fn (b as (r1,r2)) => fn thm =>
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   408
        EXISTS(ex r2 (subst_free [b]
26626
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   409
                   (HOLogic.dest_Trueprop(Thm.prop_of thm))), tych r1)
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   410
              thm)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   411
       blist' th
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   412
  end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   413
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   414
(*---------------------------------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   415
 *  Faster version, that fails for some as yet unknown reason
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   416
 * fun IT_EXISTS blist th =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   417
 *    let val {thy,...} = rep_thm th
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   418
 *        val tych = cterm_of thy
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   419
 *        fun detype (x,y) = ((#t o rep_cterm) x, (#t o rep_cterm) y)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   420
 *   in
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   421
 *  fold (fn (b as (r1,r2), thm) =>
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   422
 *  EXISTS(D.mk_exists(r2, tych(subst_free[detype b](#t(rep_cterm(cconcl thm))))),
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   423
 *           r1) thm)  blist th
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   424
 *   end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   425
 *---------------------------------------------------------------------------*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   426
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   427
(*----------------------------------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   428
 *        Rewriting
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   429
 *---------------------------------------------------------------------------*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   430
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   431
fun SUBS thl =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   432
  rewrite_rule (map (fn th => th RS eq_reflection handle THM _ => th) thl);
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   433
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   434
val rew_conv = MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE));
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   435
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   436
fun simpl_conv ss thl ctm =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   437
 rew_conv (ss addsimps thl) ctm RS meta_eq_to_obj_eq;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   438
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   439
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   440
val RIGHT_ASSOC = rewrite_rule [Thms.disj_assoc];
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   441
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   442
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   443
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   444
(*---------------------------------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   445
 *                  TERMINATION CONDITION EXTRACTION
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   446
 *---------------------------------------------------------------------------*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   447
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   448
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   449
(* Object language quantifier, i.e., "!" *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   450
fun Forall v M = S.mk_forall{Bvar=v, Body=M};
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   451
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   452
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   453
(* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   454
fun is_cong thm =
26626
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   455
  case (Thm.prop_of thm)
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   456
     of (Const("==>",_)$(Const("Trueprop",_)$ _) $
32603
e08fdd615333 tuned const_name antiquotations
haftmann
parents: 32462
diff changeset
   457
         (Const("==",_) $ (Const (@{const_name Recdef.cut},_) $ f $ R $ a $ x) $ _)) => false
26626
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   458
      | _ => true;
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   459
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   460
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   461
fun dest_equal(Const ("==",_) $
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   462
               (Const ("Trueprop",_) $ lhs)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   463
               $ (Const ("Trueprop",_) $ rhs)) = {lhs=lhs, rhs=rhs}
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   464
  | dest_equal(Const ("==",_) $ lhs $ rhs)  = {lhs=lhs, rhs=rhs}
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   465
  | dest_equal tm = S.dest_eq tm;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   466
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   467
fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   468
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   469
fun dest_all used (Const("all",_) $ (a as Abs _)) = S.dest_abs used a
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   470
  | dest_all _ _ = raise RULES_ERR "dest_all" "not a !!";
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   471
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   472
val is_all = can (dest_all []);
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   473
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   474
fun strip_all used fm =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   475
   if (is_all fm)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   476
   then let val ({Bvar, Body}, used') = dest_all used fm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   477
            val (bvs, core, used'') = strip_all used' Body
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   478
        in ((Bvar::bvs), core, used'')
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   479
        end
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   480
   else ([], fm, used);
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   481
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   482
fun break_all(Const("all",_) $ Abs (_,_,body)) = body
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   483
  | break_all _ = raise RULES_ERR "break_all" "not a !!";
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   484
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   485
fun list_break_all(Const("all",_) $ Abs (s,ty,body)) =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   486
     let val (L,core) = list_break_all body
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   487
     in ((s,ty)::L, core)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   488
     end
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   489
  | list_break_all tm = ([],tm);
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   490
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   491
(*---------------------------------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   492
 * Rename a term of the form
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   493
 *
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   494
 *      !!x1 ...xn. x1=M1 ==> ... ==> xn=Mn
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   495
 *                  ==> ((%v1...vn. Q) x1 ... xn = g x1 ... xn.
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   496
 * to one of
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   497
 *
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   498
 *      !!v1 ... vn. v1=M1 ==> ... ==> vn=Mn
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   499
 *      ==> ((%v1...vn. Q) v1 ... vn = g v1 ... vn.
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   500
 *
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   501
 * This prevents name problems in extraction, and helps the result to read
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   502
 * better. There is a problem with varstructs, since they can introduce more
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   503
 * than n variables, and some extra reasoning needs to be done.
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   504
 *---------------------------------------------------------------------------*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   505
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   506
fun get ([],_,L) = rev L
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   507
  | get (ant::rst,n,L) =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   508
      case (list_break_all ant)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   509
        of ([],_) => get (rst, n+1,L)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   510
         | (vlist,body) =>
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   511
            let val eq = Logic.strip_imp_concl body
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   512
                val (f,args) = S.strip_comb (get_lhs eq)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   513
                val (vstrl,_) = S.strip_abs f
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   514
                val names  =
29270
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29265
diff changeset
   515
                  Name.variant_list (OldTerm.add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   516
            in get (rst, n+1, (names,n)::L) end
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   517
            handle TERM _ => get (rst, n+1, L)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   518
              | U.ERR _ => get (rst, n+1, L);
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   519
31945
d5f186aa0bed structure Thm: less pervasive names;
wenzelm
parents: 30190
diff changeset
   520
(* Note: Thm.rename_params_rule counts from 1, not 0 *)
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   521
fun rename thm =
26626
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   522
  let val thy = Thm.theory_of_thm thm
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   523
      val tych = cterm_of thy
26626
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   524
      val ants = Logic.strip_imp_prems (Thm.prop_of thm)
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   525
      val news = get (ants,1,[])
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   526
  in
31945
d5f186aa0bed structure Thm: less pervasive names;
wenzelm
parents: 30190
diff changeset
   527
  fold Thm.rename_params_rule news thm
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   528
  end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   529
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   530
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   531
(*---------------------------------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   532
 * Beta-conversion to the rhs of an equation (taken from hol90/drule.sml)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   533
 *---------------------------------------------------------------------------*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   534
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   535
fun list_beta_conv tm =
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36617
diff changeset
   536
  let fun rbeta th = Thm.transitive th (Thm.beta_conversion false (#2(D.dest_eq(cconcl th))))
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   537
      fun iter [] = Thm.reflexive tm
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36617
diff changeset
   538
        | iter (v::rst) = rbeta (Thm.combination(iter rst) (Thm.reflexive v))
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   539
  in iter  end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   540
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   541
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   542
(*---------------------------------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   543
 * Trace information for the rewriter
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   544
 *---------------------------------------------------------------------------*)
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32603
diff changeset
   545
val term_ref = Unsynchronized.ref [] : term list Unsynchronized.ref
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32603
diff changeset
   546
val ss_ref = Unsynchronized.ref [] : simpset list Unsynchronized.ref;
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32603
diff changeset
   547
val thm_ref = Unsynchronized.ref [] : thm list Unsynchronized.ref;
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32603
diff changeset
   548
val tracing = Unsynchronized.ref false;
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   549
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   550
fun say s = if !tracing then writeln s else ();
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   551
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   552
fun print_thms s L =
32091
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 31945
diff changeset
   553
  say (cat_lines (s :: map Display.string_of_thm_without_context L));
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   554
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32091
diff changeset
   555
fun print_cterm s ct =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32091
diff changeset
   556
  say (cat_lines [s, Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct)]);
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   557
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   558
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   559
(*---------------------------------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   560
 * General abstraction handlers, should probably go in USyntax.
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   561
 *---------------------------------------------------------------------------*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   562
fun mk_aabs (vstr, body) =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   563
  S.mk_abs {Bvar = vstr, Body = body}
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   564
  handle U.ERR _ => S.mk_pabs {varstruct = vstr, body = body};
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   565
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   566
fun list_mk_aabs (vstrl,tm) =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   567
    fold_rev (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   568
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   569
fun dest_aabs used tm =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   570
   let val ({Bvar,Body}, used') = S.dest_abs used tm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   571
   in (Bvar, Body, used') end
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   572
   handle U.ERR _ =>
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   573
     let val {varstruct, body, used} = S.dest_pabs used tm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   574
     in (varstruct, body, used) end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   575
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   576
fun strip_aabs used tm =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   577
   let val (vstr, body, used') = dest_aabs used tm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   578
       val (bvs, core, used'') = strip_aabs used' body
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   579
   in (vstr::bvs, core, used'') end
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   580
   handle U.ERR _ => ([], tm, used);
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   581
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   582
fun dest_combn tm 0 = (tm,[])
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   583
  | dest_combn tm n =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   584
     let val {Rator,Rand} = S.dest_comb tm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   585
         val (f,rands) = dest_combn Rator (n-1)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   586
     in (f,Rand::rands)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   587
     end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   588
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   589
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   590
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   591
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   592
local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   593
      fun mk_fst tm =
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37391
diff changeset
   594
          let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm
37391
476270a6c2dc tuned quotes, antiquotations and whitespace
haftmann
parents: 37136
diff changeset
   595
          in  Const ("Product_Type.fst", ty --> fty) $ tm  end
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   596
      fun mk_snd tm =
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37391
diff changeset
   597
          let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm
37391
476270a6c2dc tuned quotes, antiquotations and whitespace
haftmann
parents: 37136
diff changeset
   598
          in  Const ("Product_Type.snd", ty --> sty) $ tm  end
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   599
in
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   600
fun XFILL tych x vstruct =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   601
  let fun traverse p xocc L =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   602
        if (is_Free p)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   603
        then tych xocc::L
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   604
        else let val (p1,p2) = dest_pair p
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   605
             in traverse p1 (mk_fst xocc) (traverse p2  (mk_snd xocc) L)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   606
             end
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   607
  in
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   608
  traverse vstruct x []
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   609
end end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   610
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   611
(*---------------------------------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   612
 * Replace a free tuple (vstr) by a universally quantified variable (a).
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   613
 * Note that the notion of "freeness" for a tuple is different than for a
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   614
 * variable: if variables in the tuple also occur in any other place than
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   615
 * an occurrences of the tuple, they aren't "free" (which is thus probably
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   616
 *  the wrong word to use).
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   617
 *---------------------------------------------------------------------------*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   618
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   619
fun VSTRUCT_ELIM tych a vstr th =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   620
  let val L = S.free_vars_lr vstr
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   621
      val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr)))
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36617
diff changeset
   622
      val thm1 = Thm.implies_intr bind1 (SUBS [SYM(Thm.assume bind1)] th)
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   623
      val thm2 = forall_intr_list (map tych L) thm1
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   624
      val thm3 = forall_elim_list (XFILL tych a vstr) thm2
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   625
  in refl RS
37136
e0c9d3e49e15 dropped legacy theorem bindings
haftmann
parents: 36945
diff changeset
   626
     rewrite_rule [Thm.symmetric (@{thm surjective_pairing} RS eq_reflection)] thm3
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   627
  end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   628
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   629
fun PGEN tych a vstr th =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   630
  let val a1 = tych a
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   631
      val vstr1 = tych vstr
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   632
  in
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36617
diff changeset
   633
  Thm.forall_intr a1
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   634
     (if (is_Free vstr)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   635
      then cterm_instantiate [(vstr1,a1)] th
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   636
      else VSTRUCT_ELIM tych a vstr th)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   637
  end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   638
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   639
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   640
(*---------------------------------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   641
 * Takes apart a paired beta-redex, looking like "(\(x,y).N) vstr", into
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   642
 *
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   643
 *     (([x,y],N),vstr)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   644
 *---------------------------------------------------------------------------*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   645
fun dest_pbeta_redex used M n =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   646
  let val (f,args) = dest_combn M n
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   647
      val dummy = dest_aabs used f
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   648
  in (strip_aabs used f,args)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   649
  end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   650
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   651
fun pbeta_redex M n = can (U.C (dest_pbeta_redex []) n) M;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   652
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   653
fun dest_impl tm =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   654
  let val ants = Logic.strip_imp_prems tm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   655
      val eq = Logic.strip_imp_concl tm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   656
  in (ants,get_lhs eq)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   657
  end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   658
33035
15eab423e573 standardized basic operations on type option;
wenzelm
parents: 32740
diff changeset
   659
fun restricted t = is_some (S.find_term
32603
e08fdd615333 tuned const_name antiquotations
haftmann
parents: 32462
diff changeset
   660
                            (fn (Const(@{const_name Recdef.cut},_)) =>true | _ => false)
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   661
                            t)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   662
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   663
fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   664
 let val globals = func::G
35232
f588e1169c8b renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
wenzelm
parents: 33339
diff changeset
   665
     val ss0 = Simplifier.global_context (Thm.theory_of_thm th) empty_ss
37136
e0c9d3e49e15 dropped legacy theorem bindings
haftmann
parents: 36945
diff changeset
   666
     val pbeta_reduce = simpl_conv ss0 [@{thm split_conv} RS eq_reflection];
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32603
diff changeset
   667
     val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   668
     val dummy = term_ref := []
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   669
     val dummy = thm_ref  := []
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   670
     val dummy = ss_ref  := []
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   671
     val cut_lemma' = cut_lemma RS eq_reflection
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   672
     fun prover used ss thm =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   673
     let fun cong_prover ss thm =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   674
         let val dummy = say "cong_prover:"
29302
eb782d1dc07c normalized some ML type/val aliases;
wenzelm
parents: 29270
diff changeset
   675
             val cntxt = Simplifier.prems_of_ss ss
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   676
             val dummy = print_thms "cntxt:" cntxt
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   677
             val dummy = say "cong rule:"
32091
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 31945
diff changeset
   678
             val dummy = say (Display.string_of_thm_without_context thm)
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   679
             val dummy = thm_ref := (thm :: !thm_ref)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   680
             val dummy = ss_ref := (ss :: !ss_ref)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   681
             (* Unquantified eliminate *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   682
             fun uq_eliminate (thm,imp,thy) =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   683
                 let val tych = cterm_of thy
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32091
diff changeset
   684
                     val dummy = print_cterm "To eliminate:" (tych imp)
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   685
                     val ants = map tych (Logic.strip_imp_prems imp)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   686
                     val eq = Logic.strip_imp_concl imp
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   687
                     val lhs = tych(get_lhs eq)
29302
eb782d1dc07c normalized some ML type/val aliases;
wenzelm
parents: 29270
diff changeset
   688
                     val ss' = Simplifier.add_prems (map ASSUME ants) ss
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   689
                     val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) ss' lhs
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   690
                       handle U.ERR _ => Thm.reflexive lhs
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   691
                     val dummy = print_thms "proven:" [lhs_eq_lhs1]
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   692
                     val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   693
                     val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   694
                  in
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   695
                  lhs_eeq_lhs2 COMP thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   696
                  end
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   697
             fun pq_eliminate (thm,thy,vlist,imp_body,lhs_eq) =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   698
              let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   699
                  val dummy = forall (op aconv) (ListPair.zip (vlist, args))
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   700
                    orelse error "assertion failed in CONTEXT_REWRITE_RULE"
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   701
                  val imp_body1 = subst_free (ListPair.zip (args, vstrl))
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   702
                                             imp_body
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   703
                  val tych = cterm_of thy
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   704
                  val ants1 = map tych (Logic.strip_imp_prems imp_body1)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   705
                  val eq1 = Logic.strip_imp_concl imp_body1
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   706
                  val Q = get_lhs eq1
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   707
                  val QeqQ1 = pbeta_reduce (tych Q)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   708
                  val Q1 = #2(D.dest_eq(cconcl QeqQ1))
29302
eb782d1dc07c normalized some ML type/val aliases;
wenzelm
parents: 29270
diff changeset
   709
                  val ss' = Simplifier.add_prems (map ASSUME ants1) ss
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   710
                  val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') ss' Q1
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   711
                                handle U.ERR _ => Thm.reflexive Q1
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   712
                  val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2))
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   713
                  val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   714
                  val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   715
                  val thA = Thm.transitive(QeqQ1 RS eq_reflection) Q1eeqQ2
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   716
                  val QeeqQ3 = Thm.transitive thA Q2eeqQ3 handle THM _ =>
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   717
                               ((Q2eeqQ3 RS meta_eq_to_obj_eq)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   718
                                RS ((thA RS meta_eq_to_obj_eq) RS trans))
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   719
                                RS eq_reflection
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   720
                  val impth = implies_intr_list ants1 QeeqQ3
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   721
                  val impth1 = impth RS meta_eq_to_obj_eq
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   722
                  (* Need to abstract *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   723
                  val ant_th = U.itlist2 (PGEN tych) args vstrl impth1
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   724
              in ant_th COMP thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   725
              end
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   726
             fun q_eliminate (thm,imp,thy) =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   727
              let val (vlist, imp_body, used') = strip_all used imp
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   728
                  val (ants,Q) = dest_impl imp_body
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   729
              in if (pbeta_redex Q) (length vlist)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   730
                 then pq_eliminate (thm,thy,vlist,imp_body,Q)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   731
                 else
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   732
                 let val tych = cterm_of thy
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   733
                     val ants1 = map tych ants
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   734
                     val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   735
                     val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   736
                        (false,true,false) (prover used') ss' (tych Q)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   737
                      handle U.ERR _ => Thm.reflexive (tych Q)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   738
                     val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   739
                     val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   740
                     val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   741
                 in
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   742
                 ant_th COMP thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   743
              end end
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   744
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   745
             fun eliminate thm =
26626
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   746
               case Thm.prop_of thm
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   747
               of Const("==>",_) $ imp $ _ =>
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   748
                   eliminate
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   749
                    (if not(is_all imp)
26626
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   750
                     then uq_eliminate (thm, imp, Thm.theory_of_thm thm)
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   751
                     else q_eliminate (thm, imp, Thm.theory_of_thm thm))
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   752
                            (* Assume that the leading constant is ==,   *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   753
                | _ => thm  (* if it is not a ==>                        *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   754
         in SOME(eliminate (rename thm)) end
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   755
         handle U.ERR _ => NONE    (* FIXME handle THM as well?? *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   756
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   757
        fun restrict_prover ss thm =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   758
          let val dummy = say "restrict_prover:"
29302
eb782d1dc07c normalized some ML type/val aliases;
wenzelm
parents: 29270
diff changeset
   759
              val cntxt = rev(Simplifier.prems_of_ss ss)
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   760
              val dummy = print_thms "cntxt:" cntxt
26626
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   761
              val thy = Thm.theory_of_thm thm
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   762
              val Const("==>",_) $ (Const("Trueprop",_) $ A) $ _ = Thm.prop_of thm
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   763
              fun genl tm = let val vlist = subtract (op aconv) globals
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 26928
diff changeset
   764
                                           (OldTerm.add_term_frees(tm,[]))
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   765
                            in fold_rev Forall vlist tm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   766
                            end
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   767
              (*--------------------------------------------------------------
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   768
               * This actually isn't quite right, since it will think that
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   769
               * not-fully applied occs. of "f" in the context mean that the
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   770
               * current call is nested. The real solution is to pass in a
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   771
               * term "f v1..vn" which is a pattern that any full application
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   772
               * of "f" will match.
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   773
               *-------------------------------------------------------------*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   774
              val func_name = #1(dest_Const func)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   775
              fun is_func (Const (name,_)) = (name = func_name)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   776
                | is_func _                = false
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   777
              val rcontext = rev cntxt
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   778
              val cncl = HOLogic.dest_Trueprop o Thm.prop_of
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   779
              val antl = case rcontext of [] => []
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   780
                         | _   => [S.list_mk_conj(map cncl rcontext)]
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   781
              val TC = genl(S.list_mk_imp(antl, A))
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32091
diff changeset
   782
              val dummy = print_cterm "func:" (cterm_of thy func)
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32091
diff changeset
   783
              val dummy = print_cterm "TC:" (cterm_of thy (HOLogic.mk_Trueprop TC))
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   784
              val dummy = tc_list := (TC :: !tc_list)
33035
15eab423e573 standardized basic operations on type option;
wenzelm
parents: 32740
diff changeset
   785
              val nestedp = is_some (S.find_term is_func TC)
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   786
              val dummy = if nestedp then say "nested" else say "not_nested"
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   787
              val dummy = term_ref := ([func,TC]@(!term_ref))
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   788
              val th' = if nestedp then raise RULES_ERR "solver" "nested function"
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   789
                        else let val cTC = cterm_of thy
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   790
                                              (HOLogic.mk_Trueprop TC)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   791
                             in case rcontext of
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   792
                                [] => SPEC_ALL(ASSUME cTC)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   793
                               | _ => MP (SPEC_ALL (ASSUME cTC))
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   794
                                         (LIST_CONJ rcontext)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   795
                             end
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   796
              val th'' = th' RS thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   797
          in SOME (th'')
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   798
          end handle U.ERR _ => NONE    (* FIXME handle THM as well?? *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   799
    in
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   800
    (if (is_cong thm) then cong_prover else restrict_prover) ss thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   801
    end
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   802
    val ctm = cprop_of th
29270
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29265
diff changeset
   803
    val names = OldTerm.add_term_names (term_of ctm, [])
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   804
    val th1 = MetaSimplifier.rewrite_cterm(false,true,false)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   805
      (prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36617
diff changeset
   806
    val th2 = Thm.equal_elim th1 th
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   807
 in
33317
b4534348b8fd standardized filter/filter_out;
wenzelm
parents: 33035
diff changeset
   808
 (th2, filter_out restricted (!tc_list))
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   809
 end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   810
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   811
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   812
fun prove strict (ptm, tac) =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   813
  let
26626
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   814
    val thy = Thm.theory_of_cterm ptm;
c6231d64d264 rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 23150
diff changeset
   815
    val t = Thm.term_of ptm;
36610
bafd82950e24 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents: 35232
diff changeset
   816
    val ctxt = ProofContext.init_global thy |> Variable.auto_fixes t;
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   817
  in
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   818
    if strict then Goal.prove ctxt [] [] t (K tac)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   819
    else Goal.prove ctxt [] [] t (K tac)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   820
      handle ERROR msg => (warning msg; raise RULES_ERR "prove" msg)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   821
  end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   822
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   823
end;