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