src/HOL/Library/old_recdef.ML
author Manuel Eberl <eberlm@in.tum.de>
Mon Mar 26 16:14:16 2018 +0200 (18 months ago)
changeset 67951 655aa11359dc
parent 67710 cc2db3239932
child 69593 3dda49e08b9d
permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
wenzelm@62058
     1
(*  Title:      HOL/Library/old_recdef.ML
wenzelm@60520
     2
    Author:     Konrad Slind, Cambridge University Computer Laboratory
wenzelm@60520
     3
    Author:     Lucas Dixon, University of Edinburgh
wenzelm@60520
     4
wenzelm@60520
     5
Old TFL/recdef package.
wenzelm@60520
     6
*)
wenzelm@60520
     7
wenzelm@60520
     8
signature CASE_SPLIT =
wenzelm@60520
     9
sig
wenzelm@60520
    10
  (* try to recursively split conjectured thm to given list of thms *)
wenzelm@60520
    11
  val splitto : Proof.context -> thm list -> thm -> thm
wenzelm@60520
    12
end;
wenzelm@60520
    13
wenzelm@60520
    14
signature UTILS =
wenzelm@60520
    15
sig
wenzelm@60520
    16
  exception ERR of {module: string, func: string, mesg: string}
wenzelm@60520
    17
  val end_itlist: ('a -> 'a -> 'a) -> 'a list -> 'a
wenzelm@60520
    18
  val itlist2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
wenzelm@60520
    19
  val pluck: ('a -> bool) -> 'a list -> 'a * 'a list
wenzelm@60520
    20
  val zip3: 'a list -> 'b list -> 'c list -> ('a*'b*'c) list
wenzelm@60520
    21
  val take: ('a -> 'b) -> int * 'a list -> 'b list
wenzelm@60520
    22
end;
wenzelm@60520
    23
wenzelm@60520
    24
signature USYNTAX =
wenzelm@60520
    25
sig
wenzelm@60520
    26
  datatype lambda = VAR   of {Name : string, Ty : typ}
wenzelm@60520
    27
                  | CONST of {Name : string, Ty : typ}
wenzelm@60520
    28
                  | COMB  of {Rator: term, Rand : term}
wenzelm@60520
    29
                  | LAMB  of {Bvar : term, Body : term}
wenzelm@60520
    30
wenzelm@60520
    31
  val alpha : typ
wenzelm@60520
    32
wenzelm@60520
    33
  (* Types *)
wenzelm@60520
    34
  val type_vars  : typ -> typ list
wenzelm@60520
    35
  val type_varsl : typ list -> typ list
wenzelm@60520
    36
  val mk_vartype : string -> typ
wenzelm@60520
    37
  val is_vartype : typ -> bool
wenzelm@60520
    38
  val strip_prod_type : typ -> typ list
wenzelm@60520
    39
wenzelm@60520
    40
  (* Terms *)
wenzelm@60520
    41
  val free_vars_lr : term -> term list
wenzelm@60520
    42
  val type_vars_in_term : term -> typ list
wenzelm@60520
    43
  val dest_term  : term -> lambda
wenzelm@60520
    44
wenzelm@60520
    45
  (* Prelogic *)
wenzelm@60520
    46
  val inst      : (typ*typ) list -> term -> term
wenzelm@60520
    47
wenzelm@60520
    48
  (* Construction routines *)
wenzelm@60520
    49
  val mk_abs    :{Bvar  : term, Body : term} -> term
wenzelm@60520
    50
wenzelm@60520
    51
  val mk_imp    :{ant : term, conseq :  term} -> term
wenzelm@60520
    52
  val mk_select :{Bvar : term, Body : term} -> term
wenzelm@60520
    53
  val mk_forall :{Bvar : term, Body : term} -> term
wenzelm@60520
    54
  val mk_exists :{Bvar : term, Body : term} -> term
wenzelm@60520
    55
  val mk_conj   :{conj1 : term, conj2 : term} -> term
wenzelm@60520
    56
  val mk_disj   :{disj1 : term, disj2 : term} -> term
wenzelm@60520
    57
  val mk_pabs   :{varstruct : term, body : term} -> term
wenzelm@60520
    58
wenzelm@60520
    59
  (* Destruction routines *)
wenzelm@60520
    60
  val dest_const: term -> {Name : string, Ty : typ}
wenzelm@60520
    61
  val dest_comb : term -> {Rator : term, Rand : term}
wenzelm@60520
    62
  val dest_abs  : string list -> term -> {Bvar : term, Body : term} * string list
wenzelm@60520
    63
  val dest_eq     : term -> {lhs : term, rhs : term}
wenzelm@60520
    64
  val dest_imp    : term -> {ant : term, conseq : term}
wenzelm@60520
    65
  val dest_forall : term -> {Bvar : term, Body : term}
wenzelm@60520
    66
  val dest_exists : term -> {Bvar : term, Body : term}
wenzelm@60520
    67
  val dest_neg    : term -> term
wenzelm@60520
    68
  val dest_conj   : term -> {conj1 : term, conj2 : term}
wenzelm@60520
    69
  val dest_disj   : term -> {disj1 : term, disj2 : term}
wenzelm@60520
    70
  val dest_pair   : term -> {fst : term, snd : term}
wenzelm@60520
    71
  val dest_pabs   : string list -> term -> {varstruct : term, body : term, used : string list}
wenzelm@60520
    72
wenzelm@60520
    73
  val lhs   : term -> term
wenzelm@60520
    74
  val rhs   : term -> term
wenzelm@60520
    75
  val rand  : term -> term
wenzelm@60520
    76
wenzelm@60520
    77
  (* Query routines *)
wenzelm@60520
    78
  val is_imp    : term -> bool
wenzelm@60520
    79
  val is_forall : term -> bool
wenzelm@60520
    80
  val is_exists : term -> bool
wenzelm@60520
    81
  val is_neg    : term -> bool
wenzelm@60520
    82
  val is_conj   : term -> bool
wenzelm@60520
    83
  val is_disj   : term -> bool
wenzelm@60520
    84
  val is_pair   : term -> bool
wenzelm@60520
    85
  val is_pabs   : term -> bool
wenzelm@60520
    86
wenzelm@60520
    87
  (* Construction of a term from a list of Preterms *)
wenzelm@60520
    88
  val list_mk_abs    : (term list * term) -> term
wenzelm@60520
    89
  val list_mk_imp    : (term list * term) -> term
wenzelm@60520
    90
  val list_mk_forall : (term list * term) -> term
wenzelm@60520
    91
  val list_mk_conj   : term list -> term
wenzelm@60520
    92
wenzelm@60520
    93
  (* Destructing a term to a list of Preterms *)
wenzelm@60520
    94
  val strip_comb     : term -> (term * term list)
wenzelm@60520
    95
  val strip_abs      : term -> (term list * term)
wenzelm@60520
    96
  val strip_imp      : term -> (term list * term)
wenzelm@60520
    97
  val strip_forall   : term -> (term list * term)
wenzelm@60520
    98
  val strip_exists   : term -> (term list * term)
wenzelm@60520
    99
  val strip_disj     : term -> term list
wenzelm@60520
   100
wenzelm@60520
   101
  (* Miscellaneous *)
wenzelm@60520
   102
  val mk_vstruct : typ -> term list -> term
wenzelm@60520
   103
  val gen_all    : term -> term
wenzelm@60520
   104
  val find_term  : (term -> bool) -> term -> term option
wenzelm@60520
   105
  val dest_relation : term -> term * term * term
wenzelm@60520
   106
  val is_WFR : term -> bool
wenzelm@60520
   107
  val ARB : typ -> term
wenzelm@60520
   108
end;
wenzelm@60520
   109
wenzelm@60520
   110
signature DCTERM =
wenzelm@60520
   111
sig
wenzelm@60520
   112
  val dest_comb: cterm -> cterm * cterm
wenzelm@60520
   113
  val dest_abs: string option -> cterm -> cterm * cterm
wenzelm@60520
   114
  val capply: cterm -> cterm -> cterm
wenzelm@60520
   115
  val cabs: cterm -> cterm -> cterm
wenzelm@60520
   116
  val mk_conj: cterm * cterm -> cterm
wenzelm@60520
   117
  val mk_disj: cterm * cterm -> cterm
wenzelm@60520
   118
  val mk_exists: cterm * cterm -> cterm
wenzelm@60520
   119
  val dest_conj: cterm -> cterm * cterm
wenzelm@60520
   120
  val dest_const: cterm -> {Name: string, Ty: typ}
wenzelm@60520
   121
  val dest_disj: cterm -> cterm * cterm
wenzelm@60520
   122
  val dest_eq: cterm -> cterm * cterm
wenzelm@60520
   123
  val dest_exists: cterm -> cterm * cterm
wenzelm@60520
   124
  val dest_forall: cterm -> cterm * cterm
wenzelm@60520
   125
  val dest_imp: cterm -> cterm * cterm
wenzelm@60520
   126
  val dest_neg: cterm -> cterm
wenzelm@60520
   127
  val dest_pair: cterm -> cterm * cterm
wenzelm@60520
   128
  val dest_var: cterm -> {Name:string, Ty:typ}
wenzelm@60520
   129
  val is_conj: cterm -> bool
wenzelm@60520
   130
  val is_disj: cterm -> bool
wenzelm@60520
   131
  val is_eq: cterm -> bool
wenzelm@60520
   132
  val is_exists: cterm -> bool
wenzelm@60520
   133
  val is_forall: cterm -> bool
wenzelm@60520
   134
  val is_imp: cterm -> bool
wenzelm@60520
   135
  val is_neg: cterm -> bool
wenzelm@60520
   136
  val is_pair: cterm -> bool
wenzelm@60520
   137
  val list_mk_disj: cterm list -> cterm
wenzelm@60520
   138
  val strip_abs: cterm -> cterm list * cterm
wenzelm@60520
   139
  val strip_comb: cterm -> cterm * cterm list
wenzelm@60520
   140
  val strip_disj: cterm -> cterm list
wenzelm@60520
   141
  val strip_exists: cterm -> cterm list * cterm
wenzelm@60520
   142
  val strip_forall: cterm -> cterm list * cterm
wenzelm@60520
   143
  val strip_imp: cterm -> cterm list * cterm
wenzelm@60520
   144
  val drop_prop: cterm -> cterm
wenzelm@60520
   145
  val mk_prop: cterm -> cterm
wenzelm@60520
   146
end;
wenzelm@60520
   147
wenzelm@60520
   148
signature RULES =
wenzelm@60520
   149
sig
wenzelm@60520
   150
  val dest_thm: thm -> term list * term
wenzelm@60520
   151
wenzelm@60520
   152
  (* Inference rules *)
wenzelm@60520
   153
  val REFL: cterm -> thm
wenzelm@60520
   154
  val ASSUME: cterm -> thm
wenzelm@60520
   155
  val MP: thm -> thm -> thm
wenzelm@60520
   156
  val MATCH_MP: thm -> thm -> thm
wenzelm@60520
   157
  val CONJUNCT1: thm -> thm
wenzelm@60520
   158
  val CONJUNCT2: thm -> thm
wenzelm@60520
   159
  val CONJUNCTS: thm -> thm list
wenzelm@60520
   160
  val DISCH: cterm -> thm -> thm
wenzelm@60520
   161
  val UNDISCH: thm  -> thm
wenzelm@60520
   162
  val SPEC: cterm -> thm -> thm
wenzelm@60520
   163
  val ISPEC: cterm -> thm -> thm
wenzelm@60520
   164
  val ISPECL: cterm list -> thm -> thm
wenzelm@60520
   165
  val GEN: Proof.context -> cterm -> thm -> thm
wenzelm@60520
   166
  val GENL: Proof.context -> cterm list -> thm -> thm
wenzelm@60520
   167
  val LIST_CONJ: thm list -> thm
wenzelm@60520
   168
wenzelm@60520
   169
  val SYM: thm -> thm
wenzelm@60520
   170
  val DISCH_ALL: thm -> thm
wenzelm@60520
   171
  val FILTER_DISCH_ALL: (term -> bool) -> thm -> thm
wenzelm@60520
   172
  val SPEC_ALL: thm -> thm
wenzelm@60520
   173
  val GEN_ALL: Proof.context -> thm -> thm
wenzelm@60520
   174
  val IMP_TRANS: thm -> thm -> thm
wenzelm@60520
   175
  val PROVE_HYP: thm -> thm -> thm
wenzelm@60520
   176
wenzelm@60520
   177
  val CHOOSE: Proof.context -> cterm * thm -> thm -> thm
wenzelm@60781
   178
  val EXISTS: Proof.context -> cterm * cterm -> thm -> thm
wenzelm@60520
   179
  val IT_EXISTS: Proof.context -> (cterm * cterm) list -> thm -> thm
wenzelm@60520
   180
wenzelm@60520
   181
  val EVEN_ORS: thm list -> thm list
wenzelm@60520
   182
  val DISJ_CASESL: thm -> thm list -> thm
wenzelm@60520
   183
wenzelm@60520
   184
  val list_beta_conv: cterm -> cterm list -> thm
wenzelm@60520
   185
  val SUBS: Proof.context -> thm list -> thm -> thm
wenzelm@60520
   186
  val simpl_conv: Proof.context -> thm list -> cterm -> thm
wenzelm@60520
   187
wenzelm@60520
   188
  val rbeta: thm -> thm
wenzelm@60520
   189
  val tracing: bool Unsynchronized.ref
wenzelm@60520
   190
  val CONTEXT_REWRITE_RULE: Proof.context ->
wenzelm@60520
   191
    term * term list * thm * thm list -> thm -> thm * term list
wenzelm@60520
   192
  val RIGHT_ASSOC: Proof.context -> thm -> thm
wenzelm@60520
   193
wenzelm@60520
   194
  val prove: Proof.context -> bool -> term * tactic -> thm
wenzelm@60520
   195
end;
wenzelm@60520
   196
wenzelm@60520
   197
signature THRY =
wenzelm@60520
   198
sig
wenzelm@60520
   199
  val match_term: theory -> term -> term -> (term * term) list * (typ * typ) list
wenzelm@60520
   200
  val match_type: theory -> typ -> typ -> (typ * typ) list
wenzelm@60520
   201
  val typecheck: theory -> term -> cterm
wenzelm@60520
   202
  (*datatype facts of various flavours*)
wenzelm@60520
   203
  val match_info: theory -> string -> {constructors: term list, case_const: term} option
wenzelm@60520
   204
  val induct_info: theory -> string -> {constructors: term list, nchotomy: thm} option
wenzelm@60520
   205
  val extract_info: theory -> {case_congs: thm list, case_rewrites: thm list}
wenzelm@60520
   206
end;
wenzelm@60520
   207
wenzelm@60520
   208
signature PRIM =
wenzelm@60520
   209
sig
wenzelm@60520
   210
  val trace: bool Unsynchronized.ref
wenzelm@60520
   211
  val trace_thms: Proof.context -> string -> thm list -> unit
wenzelm@60520
   212
  val trace_cterm: Proof.context -> string -> cterm -> unit
wenzelm@60520
   213
  type pattern
wenzelm@60520
   214
  val mk_functional: theory -> term list -> {functional: term, pats: pattern list}
wenzelm@60520
   215
  val wfrec_definition0: string -> term -> term -> theory -> thm * theory
wenzelm@60520
   216
  val post_definition: Proof.context -> thm list -> thm * pattern list ->
wenzelm@60520
   217
   {rules: thm,
wenzelm@60520
   218
    rows: int list,
wenzelm@60520
   219
    TCs: term list list,
wenzelm@60520
   220
    full_pats_TCs: (term * term list) list}
wenzelm@60699
   221
  val mk_induction: Proof.context ->
wenzelm@60520
   222
    {fconst: term, R: term, SV: term list, pat_TCs_list: (term * term list) list} -> thm
wenzelm@60520
   223
  val postprocess: Proof.context -> bool ->
wenzelm@60520
   224
    {wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm} ->
wenzelm@60520
   225
    {rules: thm, induction: thm, TCs: term list list} ->
wenzelm@60520
   226
    {rules: thm, induction: thm, nested_tcs: thm list}
wenzelm@60520
   227
end;
wenzelm@60520
   228
wenzelm@60520
   229
signature TFL =
wenzelm@60520
   230
sig
wenzelm@60520
   231
  val define_i: bool -> thm list -> thm list -> xstring -> term -> term list -> Proof.context ->
wenzelm@60520
   232
    {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * Proof.context
wenzelm@60520
   233
  val define: bool -> thm list -> thm list -> xstring -> string -> string list -> Proof.context ->
wenzelm@60520
   234
    {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * Proof.context
wenzelm@60520
   235
end;
wenzelm@60520
   236
wenzelm@60520
   237
signature OLD_RECDEF =
wenzelm@60520
   238
sig
wenzelm@60520
   239
  val get_recdef: theory -> string
wenzelm@60520
   240
    -> {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
wenzelm@60520
   241
  val get_hints: Proof.context -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
wenzelm@60520
   242
  val simp_add: attribute
wenzelm@60520
   243
  val simp_del: attribute
wenzelm@60520
   244
  val cong_add: attribute
wenzelm@60520
   245
  val cong_del: attribute
wenzelm@60520
   246
  val wf_add: attribute
wenzelm@60520
   247
  val wf_del: attribute
wenzelm@60520
   248
  val add_recdef: bool -> xstring -> string -> ((binding * string) * Token.src list) list ->
wenzelm@60520
   249
    Token.src option -> theory -> theory
wenzelm@60520
   250
      * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
wenzelm@60520
   251
  val add_recdef_i: bool -> xstring -> term -> ((binding * term) * attribute list) list ->
wenzelm@60520
   252
    theory -> theory * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
wenzelm@60520
   253
end;
wenzelm@60520
   254
wenzelm@60520
   255
structure Old_Recdef: OLD_RECDEF =
wenzelm@60520
   256
struct
wenzelm@60520
   257
wenzelm@60520
   258
(*** extra case splitting for TFL ***)
wenzelm@60520
   259
wenzelm@60520
   260
structure CaseSplit: CASE_SPLIT =
wenzelm@60520
   261
struct
wenzelm@60520
   262
wenzelm@60520
   263
(* make a casethm from an induction thm *)
wenzelm@60752
   264
fun cases_thm_of_induct_thm ctxt =
wenzelm@60752
   265
  Seq.hd o (ALLGOALS (fn i => REPEAT (eresolve_tac ctxt [Drule.thin_rl] i)));
wenzelm@60520
   266
wenzelm@60520
   267
(* get the case_thm (my version) from a type *)
wenzelm@60752
   268
fun case_thm_of_ty ctxt ty  =
wenzelm@60520
   269
    let
wenzelm@60752
   270
      val thy = Proof_Context.theory_of ctxt
wenzelm@60520
   271
      val ty_str = case ty of
wenzelm@60520
   272
                     Type(ty_str, _) => ty_str
wenzelm@60520
   273
                   | TFree(s,_)  => error ("Free type: " ^ s)
wenzelm@60521
   274
                   | TVar((s,_),_) => error ("Free variable: " ^ s)
wenzelm@60520
   275
      val {induct, ...} = BNF_LFP_Compat.the_info thy [BNF_LFP_Compat.Keep_Nesting] ty_str
wenzelm@60520
   276
    in
wenzelm@60752
   277
      cases_thm_of_induct_thm ctxt induct
wenzelm@60520
   278
    end;
wenzelm@60520
   279
wenzelm@60520
   280
wenzelm@60520
   281
(* for use when there are no prems to the subgoal *)
wenzelm@60520
   282
(* does a case split on the given variable *)
wenzelm@60520
   283
fun mk_casesplit_goal_thm ctxt (vstr,ty) gt =
wenzelm@60520
   284
    let
wenzelm@60520
   285
      val thy = Proof_Context.theory_of ctxt;
wenzelm@60520
   286
wenzelm@60520
   287
      val x = Free(vstr,ty);
wenzelm@60520
   288
      val abst = Abs(vstr, ty, Term.abstract_over (x, gt));
wenzelm@60520
   289
wenzelm@60752
   290
      val case_thm = case_thm_of_ty ctxt ty;
wenzelm@60520
   291
wenzelm@60520
   292
      val abs_ct = Thm.cterm_of ctxt abst;
wenzelm@60520
   293
      val free_ct = Thm.cterm_of ctxt x;
wenzelm@60520
   294
wenzelm@60520
   295
      val (Pv, Dv, type_insts) =
wenzelm@60520
   296
          case (Thm.concl_of case_thm) of
wenzelm@60521
   297
            (_ $ (Pv $ (Dv as Var(_, Dty)))) =>
wenzelm@60520
   298
            (Pv, Dv,
wenzelm@60520
   299
             Sign.typ_match thy (Dty, ty) Vartab.empty)
wenzelm@60520
   300
          | _ => error "not a valid case thm";
wenzelm@60642
   301
      val type_cinsts = map (fn (ixn, (S, T)) => ((ixn, S), Thm.ctyp_of ctxt T))
wenzelm@60520
   302
        (Vartab.dest type_insts);
wenzelm@60642
   303
      val Pv = dest_Var (Envir.subst_term_types type_insts Pv);
wenzelm@60642
   304
      val Dv = dest_Var (Envir.subst_term_types type_insts Dv);
wenzelm@60520
   305
    in
wenzelm@60520
   306
      Conv.fconv_rule Drule.beta_eta_conversion
wenzelm@60520
   307
         (case_thm
wenzelm@60520
   308
            |> Thm.instantiate (type_cinsts, [])
wenzelm@60642
   309
            |> Thm.instantiate ([], [(Pv, abs_ct), (Dv, free_ct)]))
wenzelm@60520
   310
    end;
wenzelm@60520
   311
wenzelm@60520
   312
wenzelm@60520
   313
(* the find_XXX_split functions are simply doing a lightwieght (I
wenzelm@60520
   314
think) term matching equivalent to find where to do the next split *)
wenzelm@60520
   315
wenzelm@60520
   316
(* assuming two twems are identical except for a free in one at a
wenzelm@60520
   317
subterm, or constant in another, ie assume that one term is a plit of
wenzelm@60520
   318
another, then gives back the free variable that has been split. *)
wenzelm@60520
   319
exception find_split_exp of string
wenzelm@60520
   320
fun find_term_split (Free v, _ $ _) = SOME v
wenzelm@60520
   321
  | find_term_split (Free v, Const _) = SOME v
wenzelm@60520
   322
  | find_term_split (Free v, Abs _) = SOME v (* do we really want this case? *)
wenzelm@60521
   323
  | find_term_split (Free _, Var _) = NONE (* keep searching *)
wenzelm@60520
   324
  | find_term_split (a $ b, a2 $ b2) =
wenzelm@60520
   325
    (case find_term_split (a, a2) of
wenzelm@60520
   326
       NONE => find_term_split (b,b2)
wenzelm@60520
   327
     | vopt => vopt)
wenzelm@60521
   328
  | find_term_split (Abs(_,_,t1), Abs(_,_,t2)) =
wenzelm@60520
   329
    find_term_split (t1, t2)
wenzelm@60521
   330
  | find_term_split (Const (x,_), Const(x2,_)) =
wenzelm@60520
   331
    if x = x2 then NONE else (* keep searching *)
wenzelm@60520
   332
    raise find_split_exp (* stop now *)
wenzelm@60520
   333
            "Terms are not identical upto a free varaible! (Consts)"
wenzelm@60520
   334
  | find_term_split (Bound i, Bound j) =
wenzelm@60520
   335
    if i = j then NONE else (* keep searching *)
wenzelm@60520
   336
    raise find_split_exp (* stop now *)
wenzelm@60520
   337
            "Terms are not identical upto a free varaible! (Bound)"
wenzelm@60520
   338
  | find_term_split _ =
wenzelm@60520
   339
    raise find_split_exp (* stop now *)
wenzelm@60520
   340
            "Terms are not identical upto a free varaible! (Other)";
wenzelm@60520
   341
wenzelm@60520
   342
(* assume that "splitth" is a case split form of subgoal i of "genth",
wenzelm@60520
   343
then look for a free variable to split, breaking the subgoal closer to
wenzelm@60520
   344
splitth. *)
wenzelm@60520
   345
fun find_thm_split splitth i genth =
wenzelm@60520
   346
    find_term_split (Logic.get_goal (Thm.prop_of genth) i,
wenzelm@60520
   347
                     Thm.concl_of splitth) handle find_split_exp _ => NONE;
wenzelm@60520
   348
wenzelm@60520
   349
(* as above but searches "splitths" for a theorem that suggest a case split *)
wenzelm@60520
   350
fun find_thms_split splitths i genth =
wenzelm@60520
   351
    Library.get_first (fn sth => find_thm_split sth i genth) splitths;
wenzelm@60520
   352
wenzelm@60520
   353
wenzelm@60520
   354
(* split the subgoal i of "genth" until we get to a member of
wenzelm@60520
   355
splitths. Assumes that genth will be a general form of splitths, that
wenzelm@60520
   356
can be case-split, as needed. Otherwise fails. Note: We assume that
wenzelm@60520
   357
all of "splitths" are split to the same level, and thus it doesn't
wenzelm@60520
   358
matter which one we choose to look for the next split. Simply add
wenzelm@60520
   359
search on splitthms and split variable, to change this.  *)
wenzelm@60520
   360
(* Note: possible efficiency measure: when a case theorem is no longer
wenzelm@60520
   361
useful, drop it? *)
wenzelm@60520
   362
(* Note: This should not be a separate tactic but integrated into the
wenzelm@60520
   363
case split done during recdef's case analysis, this would avoid us
wenzelm@60520
   364
having to (re)search for variables to split. *)
wenzelm@60520
   365
fun splitto ctxt splitths genth =
wenzelm@60520
   366
    let
wenzelm@60520
   367
      val _ = not (null splitths) orelse error "splitto: no given splitths";
wenzelm@60520
   368
wenzelm@60520
   369
      (* check if we are a member of splitths - FIXME: quicker and
wenzelm@60520
   370
      more flexible with discrim net. *)
wenzelm@60520
   371
      fun solve_by_splitth th split =
wenzelm@60520
   372
        Thm.biresolution (SOME ctxt) false [(false,split)] 1 th;
wenzelm@60520
   373
wenzelm@60520
   374
      fun split th =
wenzelm@60520
   375
        (case find_thms_split splitths 1 th of
wenzelm@60520
   376
          NONE =>
wenzelm@60520
   377
           (writeln (cat_lines
wenzelm@61268
   378
            (["th:", Thm.string_of_thm ctxt th, "split ths:"] @
wenzelm@61268
   379
              map (Thm.string_of_thm ctxt) splitths @ ["\n--"]));
wenzelm@60520
   380
            error "splitto: cannot find variable to split on")
wenzelm@60520
   381
        | SOME v =>
wenzelm@60520
   382
            let
wenzelm@60520
   383
              val gt = HOLogic.dest_Trueprop (#1 (Logic.dest_implies (Thm.prop_of th)));
wenzelm@60520
   384
              val split_thm = mk_casesplit_goal_thm ctxt v gt;
wenzelm@60520
   385
              val (subthms, expf) = IsaND.fixed_subgoal_thms ctxt split_thm;
wenzelm@60520
   386
            in
wenzelm@60520
   387
              expf (map recsplitf subthms)
wenzelm@60520
   388
            end)
wenzelm@60520
   389
wenzelm@60520
   390
      and recsplitf th =
wenzelm@60520
   391
        (* note: multiple unifiers! we only take the first element,
wenzelm@60520
   392
           probably fine -- there is probably only one anyway. *)
wenzelm@60520
   393
        (case get_first (Seq.pull o solve_by_splitth th) splitths of
wenzelm@60520
   394
          NONE => split th
wenzelm@60520
   395
        | SOME (solved_th, _) => solved_th);
wenzelm@60520
   396
    in
wenzelm@60520
   397
      recsplitf genth
wenzelm@60520
   398
    end;
wenzelm@60520
   399
wenzelm@60520
   400
end;
wenzelm@60520
   401
wenzelm@60520
   402
wenzelm@60521
   403
wenzelm@60520
   404
(*** basic utilities ***)
wenzelm@60520
   405
wenzelm@60520
   406
structure Utils: UTILS =
wenzelm@60520
   407
struct
wenzelm@60520
   408
wenzelm@60520
   409
(*standard exception for TFL*)
wenzelm@60520
   410
exception ERR of {module: string, func: string, mesg: string};
wenzelm@60520
   411
wenzelm@60520
   412
fun UTILS_ERR func mesg = ERR {module = "Utils", func = func, mesg = mesg};
wenzelm@60520
   413
wenzelm@60520
   414
wenzelm@60521
   415
fun end_itlist _ [] = raise (UTILS_ERR "end_itlist" "list too short")
wenzelm@60521
   416
  | end_itlist _ [x] = x
wenzelm@60520
   417
  | end_itlist f (x :: xs) = f x (end_itlist f xs);
wenzelm@60520
   418
wenzelm@60520
   419
fun itlist2 f L1 L2 base_value =
wenzelm@60520
   420
 let fun it ([],[]) = base_value
wenzelm@60520
   421
       | it ((a::rst1),(b::rst2)) = f a b (it (rst1,rst2))
wenzelm@60520
   422
       | it _ = raise UTILS_ERR "itlist2" "different length lists"
wenzelm@60520
   423
 in  it (L1,L2)
wenzelm@60520
   424
 end;
wenzelm@60520
   425
wenzelm@60520
   426
fun pluck p  =
wenzelm@60520
   427
  let fun remv ([],_) = raise UTILS_ERR "pluck" "item not found"
wenzelm@60520
   428
        | remv (h::t, A) = if p h then (h, rev A @ t) else remv (t,h::A)
wenzelm@60520
   429
  in fn L => remv(L,[])
wenzelm@60520
   430
  end;
wenzelm@60520
   431
wenzelm@60520
   432
fun take f =
wenzelm@60521
   433
  let fun grab(0, _) = []
wenzelm@60520
   434
        | grab(n, x::rst) = f x::grab(n-1,rst)
wenzelm@60520
   435
  in grab
wenzelm@60520
   436
  end;
wenzelm@60520
   437
wenzelm@60520
   438
fun zip3 [][][] = []
wenzelm@60520
   439
  | zip3 (x::l1) (y::l2) (z::l3) = (x,y,z)::zip3 l1 l2 l3
wenzelm@60520
   440
  | zip3 _ _ _ = raise UTILS_ERR "zip3" "different lengths";
wenzelm@60520
   441
wenzelm@60520
   442
wenzelm@60520
   443
end;
wenzelm@60520
   444
wenzelm@60520
   445
wenzelm@60521
   446
wenzelm@60520
   447
(*** emulation of HOL's abstract syntax functions ***)
wenzelm@60520
   448
wenzelm@60520
   449
structure USyntax: USYNTAX =
wenzelm@60520
   450
struct
wenzelm@60520
   451
wenzelm@60520
   452
infix 4 ##;
wenzelm@60520
   453
wenzelm@60520
   454
fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg};
wenzelm@60520
   455
wenzelm@60520
   456
wenzelm@60520
   457
(*---------------------------------------------------------------------------
wenzelm@60520
   458
 *
wenzelm@60520
   459
 *                            Types
wenzelm@60520
   460
 *
wenzelm@60520
   461
 *---------------------------------------------------------------------------*)
wenzelm@60520
   462
val mk_prim_vartype = TVar;
wenzelm@60520
   463
fun mk_vartype s = mk_prim_vartype ((s, 0), @{sort type});
wenzelm@60520
   464
wenzelm@60520
   465
(* But internally, it's useful *)
wenzelm@60520
   466
fun dest_vtype (TVar x) = x
wenzelm@60520
   467
  | dest_vtype _ = raise USYN_ERR "dest_vtype" "not a flexible type variable";
wenzelm@60520
   468
wenzelm@60520
   469
val is_vartype = can dest_vtype;
wenzelm@60520
   470
wenzelm@60520
   471
val type_vars  = map mk_prim_vartype o Misc_Legacy.typ_tvars
wenzelm@60520
   472
fun type_varsl L = distinct (op =) (fold (curry op @ o type_vars) L []);
wenzelm@60520
   473
wenzelm@60520
   474
val alpha  = mk_vartype "'a"
wenzelm@60520
   475
wenzelm@60520
   476
val strip_prod_type = HOLogic.flatten_tupleT;
wenzelm@60520
   477
wenzelm@60520
   478
wenzelm@60520
   479
wenzelm@60520
   480
(*---------------------------------------------------------------------------
wenzelm@60520
   481
 *
wenzelm@60520
   482
 *                              Terms
wenzelm@60520
   483
 *
wenzelm@60520
   484
 *---------------------------------------------------------------------------*)
wenzelm@60520
   485
wenzelm@60520
   486
(* Free variables, in order of occurrence, from left to right in the
wenzelm@60520
   487
 * syntax tree. *)
wenzelm@60520
   488
fun free_vars_lr tm =
wenzelm@60520
   489
  let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end
wenzelm@60520
   490
      fun add (t, frees) = case t of
wenzelm@60520
   491
            Free   _ => if (memb t frees) then frees else t::frees
wenzelm@60520
   492
          | Abs (_,_,body) => add(body,frees)
wenzelm@60520
   493
          | f$t =>  add(t, add(f, frees))
wenzelm@60520
   494
          | _ => frees
wenzelm@60520
   495
  in rev(add(tm,[]))
wenzelm@60520
   496
  end;
wenzelm@60520
   497
wenzelm@60520
   498
wenzelm@60520
   499
wenzelm@60520
   500
val type_vars_in_term = map mk_prim_vartype o Misc_Legacy.term_tvars;
wenzelm@60520
   501
wenzelm@60520
   502
wenzelm@60520
   503
wenzelm@60520
   504
(* Prelogic *)
wenzelm@60520
   505
fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty)
wenzelm@60520
   506
fun inst theta = subst_vars (map dest_tybinding theta,[])
wenzelm@60520
   507
wenzelm@60520
   508
wenzelm@60520
   509
(* Construction routines *)
wenzelm@60520
   510
wenzelm@60520
   511
fun mk_abs{Bvar as Var((s,_),ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
wenzelm@60520
   512
  | mk_abs{Bvar as Free(s,ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
wenzelm@60520
   513
  | mk_abs _ = raise USYN_ERR "mk_abs" "Bvar is not a variable";
wenzelm@60520
   514
wenzelm@60520
   515
wenzelm@60520
   516
fun mk_imp{ant,conseq} =
wenzelm@60520
   517
   let val c = Const(@{const_name HOL.implies},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
wenzelm@60520
   518
   in list_comb(c,[ant,conseq])
wenzelm@60520
   519
   end;
wenzelm@60520
   520
wenzelm@60520
   521
fun mk_select (r as {Bvar,Body}) =
wenzelm@60520
   522
  let val ty = type_of Bvar
wenzelm@60520
   523
      val c = Const(@{const_name Eps},(ty --> HOLogic.boolT) --> ty)
wenzelm@60520
   524
  in list_comb(c,[mk_abs r])
wenzelm@60520
   525
  end;
wenzelm@60520
   526
wenzelm@60520
   527
fun mk_forall (r as {Bvar,Body}) =
wenzelm@60520
   528
  let val ty = type_of Bvar
wenzelm@60520
   529
      val c = Const(@{const_name All},(ty --> HOLogic.boolT) --> HOLogic.boolT)
wenzelm@60520
   530
  in list_comb(c,[mk_abs r])
wenzelm@60520
   531
  end;
wenzelm@60520
   532
wenzelm@60520
   533
fun mk_exists (r as {Bvar,Body}) =
wenzelm@60520
   534
  let val ty = type_of Bvar
wenzelm@60520
   535
      val c = Const(@{const_name Ex},(ty --> HOLogic.boolT) --> HOLogic.boolT)
wenzelm@60520
   536
  in list_comb(c,[mk_abs r])
wenzelm@60520
   537
  end;
wenzelm@60520
   538
wenzelm@60520
   539
wenzelm@60520
   540
fun mk_conj{conj1,conj2} =
wenzelm@60520
   541
   let val c = Const(@{const_name HOL.conj},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
wenzelm@60520
   542
   in list_comb(c,[conj1,conj2])
wenzelm@60520
   543
   end;
wenzelm@60520
   544
wenzelm@60520
   545
fun mk_disj{disj1,disj2} =
wenzelm@60520
   546
   let val c = Const(@{const_name HOL.disj},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
wenzelm@60520
   547
   in list_comb(c,[disj1,disj2])
wenzelm@60520
   548
   end;
wenzelm@60520
   549
wenzelm@60520
   550
fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2);
wenzelm@60520
   551
wenzelm@60520
   552
local
wenzelm@60520
   553
fun mk_uncurry (xt, yt, zt) =
haftmann@61424
   554
    Const(@{const_name case_prod}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
wenzelm@60520
   555
fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
wenzelm@60520
   556
  | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
wenzelm@60520
   557
fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
wenzelm@60520
   558
in
wenzelm@60520
   559
fun mk_pabs{varstruct,body} =
wenzelm@60520
   560
 let fun mpa (varstruct, body) =
wenzelm@60520
   561
       if is_var varstruct
wenzelm@60520
   562
       then mk_abs {Bvar = varstruct, Body = body}
wenzelm@60520
   563
       else let val {fst, snd} = dest_pair varstruct
wenzelm@60520
   564
            in mk_uncurry (type_of fst, type_of snd, type_of body) $
wenzelm@60520
   565
               mpa (fst, mpa (snd, body))
wenzelm@60520
   566
            end
wenzelm@60520
   567
 in mpa (varstruct, body) end
wenzelm@60520
   568
 handle TYPE _ => raise USYN_ERR "mk_pabs" "";
wenzelm@60520
   569
end;
wenzelm@60520
   570
wenzelm@60520
   571
(* Destruction routines *)
wenzelm@60520
   572
wenzelm@60520
   573
datatype lambda = VAR   of {Name : string, Ty : typ}
wenzelm@60520
   574
                | CONST of {Name : string, Ty : typ}
wenzelm@60520
   575
                | COMB  of {Rator: term, Rand : term}
wenzelm@60520
   576
                | LAMB  of {Bvar : term, Body : term};
wenzelm@60520
   577
wenzelm@60520
   578
wenzelm@60521
   579
fun dest_term(Var((s,_),ty)) = VAR{Name = s, Ty = ty}
wenzelm@60520
   580
  | dest_term(Free(s,ty))    = VAR{Name = s, Ty = ty}
wenzelm@60520
   581
  | dest_term(Const(s,ty))   = CONST{Name = s, Ty = ty}
wenzelm@60520
   582
  | dest_term(M$N)           = COMB{Rator=M,Rand=N}
wenzelm@60520
   583
  | dest_term(Abs(s,ty,M))   = let  val v = Free(s,ty)
wenzelm@60520
   584
                               in LAMB{Bvar = v, Body = Term.betapply (M,v)}
wenzelm@60520
   585
                               end
wenzelm@60520
   586
  | dest_term(Bound _)       = raise USYN_ERR "dest_term" "Bound";
wenzelm@60520
   587
wenzelm@60520
   588
fun dest_const(Const(s,ty)) = {Name = s, Ty = ty}
wenzelm@60520
   589
  | dest_const _ = raise USYN_ERR "dest_const" "not a constant";
wenzelm@60520
   590
wenzelm@60520
   591
fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2}
wenzelm@60520
   592
  | dest_comb _ =  raise USYN_ERR "dest_comb" "not a comb";
wenzelm@60520
   593
wenzelm@60524
   594
fun dest_abs used (a as Abs(s, ty, _)) =
wenzelm@60520
   595
     let
wenzelm@60520
   596
       val s' = singleton (Name.variant_list used) s;
wenzelm@60520
   597
       val v = Free(s', ty);
wenzelm@60520
   598
     in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used)
wenzelm@60520
   599
     end
wenzelm@60520
   600
  | dest_abs _ _ =  raise USYN_ERR "dest_abs" "not an abstraction";
wenzelm@60520
   601
wenzelm@60520
   602
fun dest_eq(Const(@{const_name HOL.eq},_) $ M $ N) = {lhs=M, rhs=N}
wenzelm@60520
   603
  | dest_eq _ = raise USYN_ERR "dest_eq" "not an equality";
wenzelm@60520
   604
wenzelm@60520
   605
fun dest_imp(Const(@{const_name HOL.implies},_) $ M $ N) = {ant=M, conseq=N}
wenzelm@60520
   606
  | dest_imp _ = raise USYN_ERR "dest_imp" "not an implication";
wenzelm@60520
   607
wenzelm@60520
   608
fun dest_forall(Const(@{const_name All},_) $ (a as Abs _)) = fst (dest_abs [] a)
wenzelm@60520
   609
  | dest_forall _ = raise USYN_ERR "dest_forall" "not a forall";
wenzelm@60520
   610
wenzelm@60520
   611
fun dest_exists(Const(@{const_name Ex},_) $ (a as Abs _)) = fst (dest_abs [] a)
wenzelm@60520
   612
  | dest_exists _ = raise USYN_ERR "dest_exists" "not an existential";
wenzelm@60520
   613
wenzelm@60520
   614
fun dest_neg(Const(@{const_name Not},_) $ M) = M
wenzelm@60520
   615
  | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
wenzelm@60520
   616
wenzelm@60520
   617
fun dest_conj(Const(@{const_name HOL.conj},_) $ M $ N) = {conj1=M, conj2=N}
wenzelm@60520
   618
  | dest_conj _ = raise USYN_ERR "dest_conj" "not a conjunction";
wenzelm@60520
   619
wenzelm@60520
   620
fun dest_disj(Const(@{const_name HOL.disj},_) $ M $ N) = {disj1=M, disj2=N}
wenzelm@60520
   621
  | dest_disj _ = raise USYN_ERR "dest_disj" "not a disjunction";
wenzelm@60520
   622
wenzelm@60520
   623
fun mk_pair{fst,snd} =
wenzelm@60520
   624
   let val ty1 = type_of fst
wenzelm@60520
   625
       val ty2 = type_of snd
wenzelm@60520
   626
       val c = Const(@{const_name Pair},ty1 --> ty2 --> prod_ty ty1 ty2)
wenzelm@60520
   627
   in list_comb(c,[fst,snd])
wenzelm@60520
   628
   end;
wenzelm@60520
   629
wenzelm@60520
   630
fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
wenzelm@60520
   631
  | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
wenzelm@60520
   632
wenzelm@60520
   633
haftmann@61424
   634
local  fun ucheck t = (if #Name (dest_const t) = @{const_name case_prod} then t
wenzelm@60520
   635
                       else raise Match)
wenzelm@60520
   636
in
wenzelm@60520
   637
fun dest_pabs used tm =
wenzelm@60520
   638
   let val ({Bvar,Body}, used') = dest_abs used tm
wenzelm@60520
   639
   in {varstruct = Bvar, body = Body, used = used'}
wenzelm@60520
   640
   end handle Utils.ERR _ =>
wenzelm@60520
   641
          let val {Rator,Rand} = dest_comb tm
wenzelm@60520
   642
              val _ = ucheck Rator
wenzelm@60520
   643
              val {varstruct = lv, body, used = used'} = dest_pabs used Rand
wenzelm@60520
   644
              val {varstruct = rv, body, used = used''} = dest_pabs used' body
wenzelm@60520
   645
          in {varstruct = mk_pair {fst = lv, snd = rv}, body = body, used = used''}
wenzelm@60520
   646
          end
wenzelm@60520
   647
end;
wenzelm@60520
   648
wenzelm@60520
   649
wenzelm@60520
   650
val lhs   = #lhs o dest_eq
wenzelm@60520
   651
val rhs   = #rhs o dest_eq
wenzelm@60520
   652
val rand  = #Rand o dest_comb
wenzelm@60520
   653
wenzelm@60520
   654
wenzelm@60520
   655
(* Query routines *)
wenzelm@60520
   656
val is_imp    = can dest_imp
wenzelm@60520
   657
val is_forall = can dest_forall
wenzelm@60520
   658
val is_exists = can dest_exists
wenzelm@60520
   659
val is_neg    = can dest_neg
wenzelm@60520
   660
val is_conj   = can dest_conj
wenzelm@60520
   661
val is_disj   = can dest_disj
wenzelm@60520
   662
val is_pair   = can dest_pair
wenzelm@60520
   663
val is_pabs   = can (dest_pabs [])
wenzelm@60520
   664
wenzelm@60520
   665
wenzelm@60520
   666
(* Construction of a cterm from a list of Terms *)
wenzelm@60520
   667
wenzelm@60520
   668
fun list_mk_abs(L,tm) = fold_rev (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm;
wenzelm@60520
   669
wenzelm@60520
   670
(* These others are almost never used *)
wenzelm@60520
   671
fun list_mk_imp(A,c) = fold_rev (fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;
wenzelm@60520
   672
fun list_mk_forall(V,t) = fold_rev (fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
wenzelm@60520
   673
val list_mk_conj = Utils.end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm})
wenzelm@60520
   674
wenzelm@60520
   675
wenzelm@60520
   676
(* Need to reverse? *)
wenzelm@60520
   677
fun gen_all tm = list_mk_forall(Misc_Legacy.term_frees tm, tm);
wenzelm@60520
   678
wenzelm@60520
   679
(* Destructing a cterm to a list of Terms *)
wenzelm@60520
   680
fun strip_comb tm =
wenzelm@60520
   681
   let fun dest(M$N, A) = dest(M, N::A)
wenzelm@60520
   682
         | dest x = x
wenzelm@60520
   683
   in dest(tm,[])
wenzelm@60520
   684
   end;
wenzelm@60520
   685
wenzelm@60520
   686
fun strip_abs(tm as Abs _) =
wenzelm@60520
   687
       let val ({Bvar,Body}, _) = dest_abs [] tm
wenzelm@60520
   688
           val (bvs, core) = strip_abs Body
wenzelm@60520
   689
       in (Bvar::bvs, core)
wenzelm@60520
   690
       end
wenzelm@60520
   691
  | strip_abs M = ([],M);
wenzelm@60520
   692
wenzelm@60520
   693
wenzelm@60520
   694
fun strip_imp fm =
wenzelm@60520
   695
   if (is_imp fm)
wenzelm@60520
   696
   then let val {ant,conseq} = dest_imp fm
wenzelm@60520
   697
            val (was,wb) = strip_imp conseq
wenzelm@60520
   698
        in ((ant::was), wb)
wenzelm@60520
   699
        end
wenzelm@60520
   700
   else ([],fm);
wenzelm@60520
   701
wenzelm@60520
   702
fun strip_forall fm =
wenzelm@60520
   703
   if (is_forall fm)
wenzelm@60520
   704
   then let val {Bvar,Body} = dest_forall fm
wenzelm@60520
   705
            val (bvs,core) = strip_forall Body
wenzelm@60520
   706
        in ((Bvar::bvs), core)
wenzelm@60520
   707
        end
wenzelm@60520
   708
   else ([],fm);
wenzelm@60520
   709
wenzelm@60520
   710
wenzelm@60520
   711
fun strip_exists fm =
wenzelm@60520
   712
   if (is_exists fm)
wenzelm@60520
   713
   then let val {Bvar, Body} = dest_exists fm
wenzelm@60520
   714
            val (bvs,core) = strip_exists Body
wenzelm@60520
   715
        in (Bvar::bvs, core)
wenzelm@60520
   716
        end
wenzelm@60520
   717
   else ([],fm);
wenzelm@60520
   718
wenzelm@60520
   719
fun strip_disj w =
wenzelm@60520
   720
   if (is_disj w)
wenzelm@60520
   721
   then let val {disj1,disj2} = dest_disj w
wenzelm@60520
   722
        in (strip_disj disj1@strip_disj disj2)
wenzelm@60520
   723
        end
wenzelm@60520
   724
   else [w];
wenzelm@60520
   725
wenzelm@60520
   726
wenzelm@60520
   727
(* Miscellaneous *)
wenzelm@60520
   728
wenzelm@60520
   729
fun mk_vstruct ty V =
wenzelm@60520
   730
  let fun follow_prod_type (Type(@{type_name Product_Type.prod},[ty1,ty2])) vs =
wenzelm@60520
   731
              let val (ltm,vs1) = follow_prod_type ty1 vs
wenzelm@60520
   732
                  val (rtm,vs2) = follow_prod_type ty2 vs1
wenzelm@60520
   733
              in (mk_pair{fst=ltm, snd=rtm}, vs2) end
wenzelm@60520
   734
        | follow_prod_type _ (v::vs) = (v,vs)
wenzelm@60520
   735
  in #1 (follow_prod_type ty V)  end;
wenzelm@60520
   736
wenzelm@60520
   737
wenzelm@60520
   738
(* Search a term for a sub-term satisfying the predicate p. *)
wenzelm@60520
   739
fun find_term p =
wenzelm@60520
   740
   let fun find tm =
wenzelm@60520
   741
      if (p tm) then SOME tm
wenzelm@60520
   742
      else case tm of
wenzelm@60520
   743
          Abs(_,_,body) => find body
wenzelm@60520
   744
        | (t$u)         => (case find t of NONE => find u | some => some)
wenzelm@60520
   745
        | _             => NONE
wenzelm@60520
   746
   in find
wenzelm@60520
   747
   end;
wenzelm@60520
   748
wenzelm@60520
   749
fun dest_relation tm =
wenzelm@60520
   750
   if (type_of tm = HOLogic.boolT)
wenzelm@60520
   751
   then let val (Const(@{const_name Set.member},_) $ (Const(@{const_name Pair},_)$y$x) $ R) = tm
wenzelm@60520
   752
        in (R,y,x)
wenzelm@60520
   753
        end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure"
wenzelm@60520
   754
   else raise USYN_ERR "dest_relation" "not a boolean term";
wenzelm@60520
   755
wenzelm@60520
   756
fun is_WFR (Const(@{const_name Wellfounded.wf},_)$_) = true
wenzelm@60520
   757
  | is_WFR _                 = false;
wenzelm@60520
   758
wenzelm@60520
   759
fun ARB ty = mk_select{Bvar=Free("v",ty),
wenzelm@60520
   760
                       Body=Const(@{const_name True},HOLogic.boolT)};
wenzelm@60520
   761
wenzelm@60520
   762
end;
wenzelm@60520
   763
wenzelm@60520
   764
wenzelm@60521
   765
wenzelm@60520
   766
(*** derived cterm destructors ***)
wenzelm@60520
   767
wenzelm@60520
   768
structure Dcterm: DCTERM =
wenzelm@60520
   769
struct
wenzelm@60520
   770
wenzelm@60520
   771
fun ERR func mesg = Utils.ERR {module = "Dcterm", func = func, mesg = mesg};
wenzelm@60520
   772
wenzelm@60520
   773
wenzelm@60520
   774
fun dest_comb t = Thm.dest_comb t
wenzelm@60520
   775
  handle CTERM (msg, _) => raise ERR "dest_comb" msg;
wenzelm@60520
   776
wenzelm@60520
   777
fun dest_abs a t = Thm.dest_abs a t
wenzelm@60520
   778
  handle CTERM (msg, _) => raise ERR "dest_abs" msg;
wenzelm@60520
   779
wenzelm@60520
   780
fun capply t u = Thm.apply t u
wenzelm@60520
   781
  handle CTERM (msg, _) => raise ERR "capply" msg;
wenzelm@60520
   782
wenzelm@60520
   783
fun cabs a t = Thm.lambda a t
wenzelm@60520
   784
  handle CTERM (msg, _) => raise ERR "cabs" msg;
wenzelm@60520
   785
wenzelm@60520
   786
wenzelm@60520
   787
(*---------------------------------------------------------------------------
wenzelm@60520
   788
 * Some simple constructor functions.
wenzelm@60520
   789
 *---------------------------------------------------------------------------*)
wenzelm@60520
   790
wenzelm@60520
   791
val mk_hol_const = Thm.cterm_of @{theory_context HOL} o Const;
wenzelm@60520
   792
wenzelm@60520
   793
fun mk_exists (r as (Bvar, Body)) =
wenzelm@60520
   794
  let val ty = Thm.typ_of_cterm Bvar
wenzelm@60520
   795
      val c = mk_hol_const(@{const_name Ex}, (ty --> HOLogic.boolT) --> HOLogic.boolT)
wenzelm@60520
   796
  in capply c (uncurry cabs r) end;
wenzelm@60520
   797
wenzelm@60520
   798
wenzelm@60520
   799
local val c = mk_hol_const(@{const_name HOL.conj}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
wenzelm@60520
   800
in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
wenzelm@60520
   801
end;
wenzelm@60520
   802
wenzelm@60520
   803
local val c = mk_hol_const(@{const_name HOL.disj}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
wenzelm@60520
   804
in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
wenzelm@60520
   805
end;
wenzelm@60520
   806
wenzelm@60520
   807
wenzelm@60520
   808
(*---------------------------------------------------------------------------
wenzelm@60520
   809
 * The primitives.
wenzelm@60520
   810
 *---------------------------------------------------------------------------*)
wenzelm@60520
   811
fun dest_const ctm =
wenzelm@60520
   812
   (case Thm.term_of ctm
wenzelm@60520
   813
      of Const(s,ty) => {Name = s, Ty = ty}
wenzelm@60520
   814
       | _ => raise ERR "dest_const" "not a constant");
wenzelm@60520
   815
wenzelm@60520
   816
fun dest_var ctm =
wenzelm@60520
   817
   (case Thm.term_of ctm
wenzelm@60521
   818
      of Var((s,_),ty) => {Name=s, Ty=ty}
wenzelm@60520
   819
       | Free(s,ty)    => {Name=s, Ty=ty}
wenzelm@60520
   820
       |             _ => raise ERR "dest_var" "not a variable");
wenzelm@60520
   821
wenzelm@60520
   822
wenzelm@60520
   823
(*---------------------------------------------------------------------------
wenzelm@60520
   824
 * Derived destructor operations.
wenzelm@60520
   825
 *---------------------------------------------------------------------------*)
wenzelm@60520
   826
wenzelm@60520
   827
fun dest_monop expected tm =
wenzelm@60520
   828
 let
wenzelm@60520
   829
   fun err () = raise ERR "dest_monop" ("Not a(n) " ^ quote expected);
wenzelm@60520
   830
   val (c, N) = dest_comb tm handle Utils.ERR _ => err ();
wenzelm@60520
   831
   val name = #Name (dest_const c handle Utils.ERR _ => err ());
wenzelm@60520
   832
 in if name = expected then N else err () end;
wenzelm@60520
   833
wenzelm@60520
   834
fun dest_binop expected tm =
wenzelm@60520
   835
 let
wenzelm@60520
   836
   fun err () = raise ERR "dest_binop" ("Not a(n) " ^ quote expected);
wenzelm@60520
   837
   val (M, N) = dest_comb tm handle Utils.ERR _ => err ()
wenzelm@60520
   838
 in (dest_monop expected M, N) handle Utils.ERR _ => err () end;
wenzelm@60520
   839
wenzelm@60520
   840
fun dest_binder expected tm =
wenzelm@60520
   841
  dest_abs NONE (dest_monop expected tm)
wenzelm@60520
   842
  handle Utils.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected);
wenzelm@60520
   843
wenzelm@60520
   844
wenzelm@60520
   845
val dest_neg    = dest_monop @{const_name Not}
wenzelm@60520
   846
val dest_pair   = dest_binop @{const_name Pair}
wenzelm@60520
   847
val dest_eq     = dest_binop @{const_name HOL.eq}
wenzelm@60520
   848
val dest_imp    = dest_binop @{const_name HOL.implies}
wenzelm@60520
   849
val dest_conj   = dest_binop @{const_name HOL.conj}
wenzelm@60520
   850
val dest_disj   = dest_binop @{const_name HOL.disj}
wenzelm@60520
   851
val dest_exists = dest_binder @{const_name Ex}
wenzelm@60520
   852
val dest_forall = dest_binder @{const_name All}
wenzelm@60520
   853
wenzelm@60520
   854
(* Query routines *)
wenzelm@60520
   855
wenzelm@60520
   856
val is_eq     = can dest_eq
wenzelm@60520
   857
val is_imp    = can dest_imp
wenzelm@60520
   858
val is_forall = can dest_forall
wenzelm@60520
   859
val is_exists = can dest_exists
wenzelm@60520
   860
val is_neg    = can dest_neg
wenzelm@60520
   861
val is_conj   = can dest_conj
wenzelm@60520
   862
val is_disj   = can dest_disj
wenzelm@60520
   863
val is_pair   = can dest_pair
wenzelm@60520
   864
wenzelm@60520
   865
wenzelm@60520
   866
(*---------------------------------------------------------------------------
wenzelm@60520
   867
 * Iterated creation.
wenzelm@60520
   868
 *---------------------------------------------------------------------------*)
wenzelm@60520
   869
val list_mk_disj = Utils.end_itlist (fn d1 => fn tm => mk_disj (d1, tm));
wenzelm@60520
   870
wenzelm@60520
   871
(*---------------------------------------------------------------------------
wenzelm@60520
   872
 * Iterated destruction. (To the "right" in a term.)
wenzelm@60520
   873
 *---------------------------------------------------------------------------*)
wenzelm@60520
   874
fun strip break tm =
wenzelm@60520
   875
  let fun dest (p as (ctm,accum)) =
wenzelm@60520
   876
        let val (M,N) = break ctm
wenzelm@60520
   877
        in dest (N, M::accum)
wenzelm@60520
   878
        end handle Utils.ERR _ => p
wenzelm@60520
   879
  in dest (tm,[])
wenzelm@60520
   880
  end;
wenzelm@60520
   881
wenzelm@60520
   882
fun rev2swap (x,l) = (rev l, x);
wenzelm@60520
   883
wenzelm@60520
   884
val strip_comb   = strip (Library.swap o dest_comb)  (* Goes to the "left" *)
wenzelm@60520
   885
val strip_imp    = rev2swap o strip dest_imp
wenzelm@60520
   886
val strip_abs    = rev2swap o strip (dest_abs NONE)
wenzelm@60520
   887
val strip_forall = rev2swap o strip dest_forall
wenzelm@60520
   888
val strip_exists = rev2swap o strip dest_exists
wenzelm@60520
   889
wenzelm@60520
   890
val strip_disj   = rev o (op::) o strip dest_disj
wenzelm@60520
   891
wenzelm@60520
   892
wenzelm@60520
   893
(*---------------------------------------------------------------------------
wenzelm@60520
   894
 * Going into and out of prop
wenzelm@60520
   895
 *---------------------------------------------------------------------------*)
wenzelm@60520
   896
wenzelm@60520
   897
fun is_Trueprop ct =
wenzelm@60520
   898
  (case Thm.term_of ct of
wenzelm@60520
   899
    Const (@{const_name Trueprop}, _) $ _ => true
wenzelm@60520
   900
  | _ => false);
wenzelm@60520
   901
wenzelm@60520
   902
fun mk_prop ct = if is_Trueprop ct then ct else Thm.apply @{cterm Trueprop} ct;
wenzelm@60520
   903
fun drop_prop ct = if is_Trueprop ct then Thm.dest_arg ct else ct;
wenzelm@60520
   904
wenzelm@60520
   905
end;
wenzelm@60520
   906
wenzelm@60520
   907
wenzelm@60521
   908
wenzelm@60520
   909
(*** emulation of HOL inference rules for TFL ***)
wenzelm@60520
   910
wenzelm@60520
   911
structure Rules: RULES =
wenzelm@60520
   912
struct
wenzelm@60520
   913
wenzelm@60520
   914
fun RULES_ERR func mesg = Utils.ERR {module = "Rules", func = func, mesg = mesg};
wenzelm@60520
   915
wenzelm@60520
   916
wenzelm@60949
   917
fun cconcl thm = Dcterm.drop_prop (Thm.cprop_of thm);
wenzelm@60949
   918
fun chyps thm = map Dcterm.drop_prop (Thm.chyps_of thm);
wenzelm@60520
   919
wenzelm@60520
   920
fun dest_thm thm =
wenzelm@61038
   921
  (map HOLogic.dest_Trueprop (Thm.hyps_of thm), HOLogic.dest_Trueprop (Thm.prop_of thm))
wenzelm@61038
   922
    handle TERM _ => raise RULES_ERR "dest_thm" "missing Trueprop";
wenzelm@60520
   923
wenzelm@60520
   924
wenzelm@60520
   925
(* Inference rules *)
wenzelm@60520
   926
wenzelm@60520
   927
(*---------------------------------------------------------------------------
wenzelm@60520
   928
 *        Equality (one step)
wenzelm@60520
   929
 *---------------------------------------------------------------------------*)
wenzelm@60520
   930
wenzelm@67710
   931
fun REFL tm = HOLogic.mk_obj_eq (Thm.reflexive tm)
wenzelm@60520
   932
  handle THM (msg, _, _) => raise RULES_ERR "REFL" msg;
wenzelm@60520
   933
wenzelm@60520
   934
fun SYM thm = thm RS sym
wenzelm@60520
   935
  handle THM (msg, _, _) => raise RULES_ERR "SYM" msg;
wenzelm@60520
   936
wenzelm@60520
   937
fun ALPHA thm ctm1 =
wenzelm@60520
   938
  let
wenzelm@60520
   939
    val ctm2 = Thm.cprop_of thm;
wenzelm@60520
   940
    val ctm2_eq = Thm.reflexive ctm2;
wenzelm@60520
   941
    val ctm1_eq = Thm.reflexive ctm1;
wenzelm@60520
   942
  in Thm.equal_elim (Thm.transitive ctm2_eq ctm1_eq) thm end
wenzelm@60520
   943
  handle THM (msg, _, _) => raise RULES_ERR "ALPHA" msg;
wenzelm@60520
   944
wenzelm@60520
   945
fun rbeta th =
wenzelm@60520
   946
  (case Dcterm.strip_comb (cconcl th) of
wenzelm@60521
   947
    (_, [_, r]) => Thm.transitive th (Thm.beta_conversion false r)
wenzelm@60520
   948
  | _ => raise RULES_ERR "rbeta" "");
wenzelm@60520
   949
wenzelm@60520
   950
wenzelm@60520
   951
(*----------------------------------------------------------------------------
wenzelm@60520
   952
 *        Implication and the assumption list
wenzelm@60520
   953
 *
wenzelm@60520
   954
 * Assumptions get stuck on the meta-language assumption list. Implications
wenzelm@60520
   955
 * are in the object language, so discharging an assumption "A" from theorem
wenzelm@60520
   956
 * "B" results in something that looks like "A --> B".
wenzelm@60520
   957
 *---------------------------------------------------------------------------*)
wenzelm@60520
   958
wenzelm@60520
   959
fun ASSUME ctm = Thm.assume (Dcterm.mk_prop ctm);
wenzelm@60520
   960
wenzelm@60520
   961
wenzelm@60520
   962
(*---------------------------------------------------------------------------
wenzelm@60520
   963
 * Implication in TFL is -->. Meta-language implication (==>) is only used
wenzelm@60520
   964
 * in the implementation of some of the inference rules below.
wenzelm@60520
   965
 *---------------------------------------------------------------------------*)
wenzelm@60520
   966
fun MP th1 th2 = th2 RS (th1 RS mp)
wenzelm@60520
   967
  handle THM (msg, _, _) => raise RULES_ERR "MP" msg;
wenzelm@60520
   968
wenzelm@60520
   969
(*forces the first argument to be a proposition if necessary*)
wenzelm@60520
   970
fun DISCH tm thm = Thm.implies_intr (Dcterm.mk_prop tm) thm COMP impI
wenzelm@60520
   971
  handle THM (msg, _, _) => raise RULES_ERR "DISCH" msg;
wenzelm@60520
   972
wenzelm@60949
   973
fun DISCH_ALL thm = fold_rev DISCH (Thm.chyps_of thm) thm;
wenzelm@60520
   974
wenzelm@60520
   975
wenzelm@60520
   976
fun FILTER_DISCH_ALL P thm =
wenzelm@60520
   977
 let fun check tm = P (Thm.term_of tm)
wenzelm@60520
   978
 in  fold_rev (fn tm => fn th => if check tm then DISCH tm th else th) (chyps thm) thm
wenzelm@60520
   979
 end;
wenzelm@60520
   980
wenzelm@60520
   981
fun UNDISCH thm =
wenzelm@60520
   982
   let val tm = Dcterm.mk_prop (#1 (Dcterm.dest_imp (cconcl thm)))
wenzelm@60520
   983
   in Thm.implies_elim (thm RS mp) (ASSUME tm) end
wenzelm@60520
   984
   handle Utils.ERR _ => raise RULES_ERR "UNDISCH" ""
wenzelm@60520
   985
     | THM _ => raise RULES_ERR "UNDISCH" "";
wenzelm@60520
   986
wenzelm@60520
   987
fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath;
wenzelm@60520
   988
wenzelm@60522
   989
fun IMP_TRANS th1 th2 = th2 RS (th1 RS @{thm tfl_imp_trans})
wenzelm@60520
   990
  handle THM (msg, _, _) => raise RULES_ERR "IMP_TRANS" msg;
wenzelm@60520
   991
wenzelm@60520
   992
wenzelm@60520
   993
(*----------------------------------------------------------------------------
wenzelm@60520
   994
 *        Conjunction
wenzelm@60520
   995
 *---------------------------------------------------------------------------*)
wenzelm@60520
   996
wenzelm@60520
   997
fun CONJUNCT1 thm = thm RS conjunct1
wenzelm@60520
   998
  handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT1" msg;
wenzelm@60520
   999
wenzelm@60520
  1000
fun CONJUNCT2 thm = thm RS conjunct2
wenzelm@60520
  1001
  handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT2" msg;
wenzelm@60520
  1002
wenzelm@60520
  1003
fun CONJUNCTS th = CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th) handle Utils.ERR _ => [th];
wenzelm@60520
  1004
wenzelm@60520
  1005
fun LIST_CONJ [] = raise RULES_ERR "LIST_CONJ" "empty list"
wenzelm@60520
  1006
  | LIST_CONJ [th] = th
wenzelm@60520
  1007
  | LIST_CONJ (th :: rst) = MP (MP (conjI COMP (impI RS impI)) th) (LIST_CONJ rst)
wenzelm@60520
  1008
      handle THM (msg, _, _) => raise RULES_ERR "LIST_CONJ" msg;
wenzelm@60520
  1009
wenzelm@60520
  1010
wenzelm@60520
  1011
(*----------------------------------------------------------------------------
wenzelm@60520
  1012
 *        Disjunction
wenzelm@60520
  1013
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1014
local
wenzelm@60520
  1015
  val prop = Thm.prop_of disjI1
wenzelm@60524
  1016
  val [_,Q] = Misc_Legacy.term_vars prop
wenzelm@60520
  1017
  val disj1 = Thm.forall_intr (Thm.cterm_of @{context} Q) disjI1
wenzelm@60520
  1018
in
wenzelm@60520
  1019
fun DISJ1 thm tm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj1)
wenzelm@60520
  1020
  handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
wenzelm@60520
  1021
end;
wenzelm@60520
  1022
wenzelm@60520
  1023
local
wenzelm@60520
  1024
  val prop = Thm.prop_of disjI2
wenzelm@60521
  1025
  val [P,_] = Misc_Legacy.term_vars prop
wenzelm@60520
  1026
  val disj2 = Thm.forall_intr (Thm.cterm_of @{context} P) disjI2
wenzelm@60520
  1027
in
wenzelm@60520
  1028
fun DISJ2 tm thm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj2)
wenzelm@60520
  1029
  handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg;
wenzelm@60520
  1030
end;
wenzelm@60520
  1031
wenzelm@60520
  1032
wenzelm@60520
  1033
(*----------------------------------------------------------------------------
wenzelm@60520
  1034
 *
wenzelm@60520
  1035
 *                   A1 |- M1, ..., An |- Mn
wenzelm@60520
  1036
 *     ---------------------------------------------------
wenzelm@60520
  1037
 *     [A1 |- M1 \/ ... \/ Mn, ..., An |- M1 \/ ... \/ Mn]
wenzelm@60520
  1038
 *
wenzelm@60520
  1039
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1040
wenzelm@60520
  1041
wenzelm@60520
  1042
fun EVEN_ORS thms =
wenzelm@60520
  1043
  let fun blue ldisjs [] _ = []
wenzelm@60520
  1044
        | blue ldisjs (th::rst) rdisjs =
wenzelm@60520
  1045
            let val tail = tl rdisjs
wenzelm@60520
  1046
                val rdisj_tl = Dcterm.list_mk_disj tail
wenzelm@60520
  1047
            in fold_rev DISJ2 ldisjs (DISJ1 th rdisj_tl)
wenzelm@60520
  1048
               :: blue (ldisjs @ [cconcl th]) rst tail
wenzelm@60520
  1049
            end handle Utils.ERR _ => [fold_rev DISJ2 ldisjs th]
wenzelm@60520
  1050
   in blue [] thms (map cconcl thms) end;
wenzelm@60520
  1051
wenzelm@60520
  1052
wenzelm@60520
  1053
(*----------------------------------------------------------------------------
wenzelm@60520
  1054
 *
wenzelm@60520
  1055
 *         A |- P \/ Q   B,P |- R    C,Q |- R
wenzelm@60520
  1056
 *     ---------------------------------------------------
wenzelm@60520
  1057
 *                     A U B U C |- R
wenzelm@60520
  1058
 *
wenzelm@60520
  1059
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1060
wenzelm@60520
  1061
fun DISJ_CASES th1 th2 th3 =
wenzelm@60520
  1062
  let
wenzelm@60520
  1063
    val c = Dcterm.drop_prop (cconcl th1);
wenzelm@60520
  1064
    val (disj1, disj2) = Dcterm.dest_disj c;
wenzelm@60520
  1065
    val th2' = DISCH disj1 th2;
wenzelm@60520
  1066
    val th3' = DISCH disj2 th3;
wenzelm@60520
  1067
  in
wenzelm@60522
  1068
    th3' RS (th2' RS (th1 RS @{thm tfl_disjE}))
wenzelm@60520
  1069
      handle THM (msg, _, _) => raise RULES_ERR "DISJ_CASES" msg
wenzelm@60520
  1070
  end;
wenzelm@60520
  1071
wenzelm@60520
  1072
wenzelm@60520
  1073
(*-----------------------------------------------------------------------------
wenzelm@60520
  1074
 *
wenzelm@60520
  1075
 *       |- A1 \/ ... \/ An     [A1 |- M, ..., An |- M]
wenzelm@60520
  1076
 *     ---------------------------------------------------
wenzelm@60520
  1077
 *                           |- M
wenzelm@60520
  1078
 *
wenzelm@60520
  1079
 * Note. The list of theorems may be all jumbled up, so we have to
wenzelm@60520
  1080
 * first organize it to align with the first argument (the disjunctive
wenzelm@60520
  1081
 * theorem).
wenzelm@60520
  1082
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1083
wenzelm@60520
  1084
fun organize eq =    (* a bit slow - analogous to insertion sort *)
wenzelm@60520
  1085
 let fun extract a alist =
wenzelm@60520
  1086
     let fun ex (_,[]) = raise RULES_ERR "organize" "not a permutation.1"
wenzelm@60520
  1087
           | ex(left,h::t) = if (eq h a) then (h,rev left@t) else ex(h::left,t)
wenzelm@60520
  1088
     in ex ([],alist)
wenzelm@60520
  1089
     end
wenzelm@60520
  1090
     fun place [] [] = []
wenzelm@60520
  1091
       | place (a::rst) alist =
wenzelm@60520
  1092
           let val (item,next) = extract a alist
wenzelm@60520
  1093
           in item::place rst next
wenzelm@60520
  1094
           end
wenzelm@60520
  1095
       | place _ _ = raise RULES_ERR "organize" "not a permutation.2"
wenzelm@60520
  1096
 in place
wenzelm@60520
  1097
 end;
wenzelm@60520
  1098
wenzelm@60520
  1099
fun DISJ_CASESL disjth thl =
wenzelm@60520
  1100
   let val c = cconcl disjth
wenzelm@60520
  1101
       fun eq th atm =
wenzelm@60520
  1102
        exists (fn t => HOLogic.dest_Trueprop t aconv Thm.term_of atm) (Thm.hyps_of th)
wenzelm@60520
  1103
       val tml = Dcterm.strip_disj c
wenzelm@60521
  1104
       fun DL _ [] = raise RULES_ERR "DISJ_CASESL" "no cases"
wenzelm@60520
  1105
         | DL th [th1] = PROVE_HYP th th1
wenzelm@60520
  1106
         | DL th [th1,th2] = DISJ_CASES th th1 th2
wenzelm@60520
  1107
         | DL th (th1::rst) =
wenzelm@60520
  1108
            let val tm = #2 (Dcterm.dest_disj (Dcterm.drop_prop(cconcl th)))
wenzelm@60520
  1109
             in DISJ_CASES th th1 (DL (ASSUME tm) rst) end
wenzelm@60520
  1110
   in DL disjth (organize eq tml thl)
wenzelm@60520
  1111
   end;
wenzelm@60520
  1112
wenzelm@60520
  1113
wenzelm@60520
  1114
(*----------------------------------------------------------------------------
wenzelm@60520
  1115
 *        Universals
wenzelm@60520
  1116
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1117
local (* this is fragile *)
wenzelm@60520
  1118
  val prop = Thm.prop_of spec
wenzelm@60520
  1119
  val x = hd (tl (Misc_Legacy.term_vars prop))
wenzelm@60642
  1120
  val TV = dest_TVar (type_of x)
wenzelm@60520
  1121
  val gspec = Thm.forall_intr (Thm.cterm_of @{context} x) spec
wenzelm@60520
  1122
in
wenzelm@60520
  1123
fun SPEC tm thm =
wenzelm@60642
  1124
   let val gspec' = Drule.instantiate_normalize ([(TV, Thm.ctyp_of_cterm tm)], []) gspec
wenzelm@60520
  1125
   in thm RS (Thm.forall_elim tm gspec') end
wenzelm@60520
  1126
end;
wenzelm@60520
  1127
wenzelm@60520
  1128
fun SPEC_ALL thm = fold SPEC (#1 (Dcterm.strip_forall(cconcl thm))) thm;
wenzelm@60520
  1129
wenzelm@60520
  1130
val ISPEC = SPEC
wenzelm@60520
  1131
val ISPECL = fold ISPEC;
wenzelm@60520
  1132
wenzelm@60520
  1133
(* Not optimized! Too complicated. *)
wenzelm@60520
  1134
local
wenzelm@60520
  1135
  val prop = Thm.prop_of allI
wenzelm@60520
  1136
  val [P] = Misc_Legacy.add_term_vars (prop, [])
wenzelm@60642
  1137
  fun cty_theta ctxt = map (fn (i, (S, ty)) => ((i, S), Thm.ctyp_of ctxt ty))
wenzelm@60520
  1138
  fun ctm_theta ctxt =
wenzelm@60520
  1139
    map (fn (i, (_, tm2)) =>
wenzelm@60520
  1140
      let val ctm2 = Thm.cterm_of ctxt tm2
wenzelm@60642
  1141
      in ((i, Thm.typ_of_cterm ctm2), ctm2) end)
wenzelm@60520
  1142
  fun certify ctxt (ty_theta,tm_theta) =
wenzelm@60520
  1143
    (cty_theta ctxt (Vartab.dest ty_theta),
wenzelm@60520
  1144
     ctm_theta ctxt (Vartab.dest tm_theta))
wenzelm@60520
  1145
in
wenzelm@60520
  1146
fun GEN ctxt v th =
wenzelm@60520
  1147
   let val gth = Thm.forall_intr v th
wenzelm@60520
  1148
       val thy = Proof_Context.theory_of ctxt
wenzelm@60520
  1149
       val Const(@{const_name Pure.all},_)$Abs(x,ty,rst) = Thm.prop_of gth
wenzelm@60520
  1150
       val P' = Abs(x,ty, HOLogic.dest_Trueprop rst)  (* get rid of trueprop *)
wenzelm@60520
  1151
       val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty);
wenzelm@60520
  1152
       val allI2 = Drule.instantiate_normalize (certify ctxt theta) allI
wenzelm@60520
  1153
       val thm = Thm.implies_elim allI2 gth
wenzelm@60520
  1154
       val tp $ (A $ Abs(_,_,M)) = Thm.prop_of thm
wenzelm@60520
  1155
       val prop' = tp $ (A $ Abs(x,ty,M))
wenzelm@60520
  1156
   in ALPHA thm (Thm.cterm_of ctxt prop') end
wenzelm@60520
  1157
end;
wenzelm@60520
  1158
wenzelm@60520
  1159
fun GENL ctxt = fold_rev (GEN ctxt);
wenzelm@60520
  1160
wenzelm@60520
  1161
fun GEN_ALL ctxt thm =
wenzelm@60520
  1162
  let
wenzelm@60520
  1163
    val prop = Thm.prop_of thm
wenzelm@60520
  1164
    val vlist = map (Thm.cterm_of ctxt) (Misc_Legacy.add_term_vars (prop, []))
wenzelm@60520
  1165
  in GENL ctxt vlist thm end;
wenzelm@60520
  1166
wenzelm@60520
  1167
wenzelm@60520
  1168
fun MATCH_MP th1 th2 =
wenzelm@60520
  1169
   if (Dcterm.is_forall (Dcterm.drop_prop(cconcl th1)))
wenzelm@60520
  1170
   then MATCH_MP (th1 RS spec) th2
wenzelm@60520
  1171
   else MP th1 th2;
wenzelm@60520
  1172
wenzelm@60520
  1173
wenzelm@60520
  1174
(*----------------------------------------------------------------------------
wenzelm@60520
  1175
 *        Existentials
wenzelm@60520
  1176
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1177
wenzelm@60520
  1178
wenzelm@60520
  1179
wenzelm@60520
  1180
(*---------------------------------------------------------------------------
wenzelm@60520
  1181
 * Existential elimination
wenzelm@60520
  1182
 *
wenzelm@60520
  1183
 *      A1 |- ?x.t[x]   ,   A2, "t[v]" |- t'
wenzelm@60520
  1184
 *      ------------------------------------     (variable v occurs nowhere)
wenzelm@60520
  1185
 *                A1 u A2 |- t'
wenzelm@60520
  1186
 *
wenzelm@60520
  1187
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1188
wenzelm@60520
  1189
fun CHOOSE ctxt (fvar, exth) fact =
wenzelm@60520
  1190
  let
wenzelm@60520
  1191
    val lam = #2 (Dcterm.dest_comb (Dcterm.drop_prop (cconcl exth)))
wenzelm@60520
  1192
    val redex = Dcterm.capply lam fvar
wenzelm@60520
  1193
    val t$u = Thm.term_of redex
wenzelm@60520
  1194
    val residue = Thm.cterm_of ctxt (Term.betapply (t, u))
wenzelm@60520
  1195
  in
wenzelm@60522
  1196
    GEN ctxt fvar (DISCH residue fact) RS (exth RS @{thm tfl_exE})
wenzelm@60520
  1197
      handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
wenzelm@60520
  1198
  end;
wenzelm@60520
  1199
wenzelm@60781
  1200
fun EXISTS ctxt (template,witness) thm =
wenzelm@60520
  1201
  let val abstr = #2 (Dcterm.dest_comb template) in
wenzelm@60781
  1202
    thm RS (infer_instantiate ctxt [(("P", 0), abstr), (("x", 0), witness)] exI)
wenzelm@60520
  1203
      handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
wenzelm@60781
  1204
  end;
wenzelm@60520
  1205
wenzelm@60520
  1206
(*----------------------------------------------------------------------------
wenzelm@60520
  1207
 *
wenzelm@60520
  1208
 *       A |- M[x_1,...,x_n]
wenzelm@60520
  1209
 *   ----------------------------   [(x |-> y)_1,...,(x |-> y)_n]
wenzelm@60520
  1210
 *       A |- ?y_1...y_n. M
wenzelm@60520
  1211
 *
wenzelm@60520
  1212
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1213
(* Could be improved, but needs "subst_free" for certified terms *)
wenzelm@60520
  1214
wenzelm@60520
  1215
fun IT_EXISTS ctxt blist th =
wenzelm@60520
  1216
  let
wenzelm@60520
  1217
    val blist' = map (apply2 Thm.term_of) blist
wenzelm@60520
  1218
    fun ex v M = Thm.cterm_of ctxt (USyntax.mk_exists{Bvar=v,Body = M})
wenzelm@60520
  1219
  in
wenzelm@60520
  1220
    fold_rev (fn (b as (r1,r2)) => fn thm =>
wenzelm@60781
  1221
        EXISTS ctxt (ex r2 (subst_free [b]
wenzelm@60520
  1222
                   (HOLogic.dest_Trueprop(Thm.prop_of thm))), Thm.cterm_of ctxt r1)
wenzelm@60520
  1223
              thm)
wenzelm@60520
  1224
       blist' th
wenzelm@60520
  1225
  end;
wenzelm@60520
  1226
wenzelm@60520
  1227
(*----------------------------------------------------------------------------
wenzelm@60520
  1228
 *        Rewriting
wenzelm@60520
  1229
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1230
wenzelm@60520
  1231
fun SUBS ctxt thl =
wenzelm@60520
  1232
  rewrite_rule ctxt (map (fn th => th RS eq_reflection handle THM _ => th) thl);
wenzelm@60520
  1233
wenzelm@60520
  1234
val rew_conv = Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE));
wenzelm@60520
  1235
wenzelm@60520
  1236
fun simpl_conv ctxt thl ctm =
wenzelm@67710
  1237
  HOLogic.mk_obj_eq (rew_conv (ctxt addsimps thl) ctm);
wenzelm@60520
  1238
wenzelm@60520
  1239
wenzelm@60522
  1240
fun RIGHT_ASSOC ctxt = rewrite_rule ctxt @{thms tfl_disj_assoc};
wenzelm@60520
  1241
wenzelm@60520
  1242
wenzelm@60520
  1243
wenzelm@60520
  1244
(*---------------------------------------------------------------------------
wenzelm@60520
  1245
 *                  TERMINATION CONDITION EXTRACTION
wenzelm@60520
  1246
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1247
wenzelm@60520
  1248
wenzelm@60520
  1249
(* Object language quantifier, i.e., "!" *)
wenzelm@60520
  1250
fun Forall v M = USyntax.mk_forall{Bvar=v, Body=M};
wenzelm@60520
  1251
wenzelm@60520
  1252
wenzelm@60520
  1253
(* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
wenzelm@60520
  1254
fun is_cong thm =
wenzelm@60520
  1255
  case (Thm.prop_of thm) of
wenzelm@60520
  1256
    (Const(@{const_name Pure.imp},_)$(Const(@{const_name Trueprop},_)$ _) $
wenzelm@60524
  1257
      (Const(@{const_name Pure.eq},_) $ (Const (@{const_name Wfrec.cut},_) $ _ $ _ $ _ $ _) $ _)) =>
wenzelm@60520
  1258
        false
wenzelm@60520
  1259
  | _ => true;
wenzelm@60520
  1260
wenzelm@60520
  1261
wenzelm@60520
  1262
fun dest_equal(Const (@{const_name Pure.eq},_) $
wenzelm@60520
  1263
               (Const (@{const_name Trueprop},_) $ lhs)
wenzelm@60520
  1264
               $ (Const (@{const_name Trueprop},_) $ rhs)) = {lhs=lhs, rhs=rhs}
wenzelm@60520
  1265
  | dest_equal(Const (@{const_name Pure.eq},_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs}
wenzelm@60520
  1266
  | dest_equal tm = USyntax.dest_eq tm;
wenzelm@60520
  1267
wenzelm@60520
  1268
fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
wenzelm@60520
  1269
wenzelm@60520
  1270
fun dest_all used (Const(@{const_name Pure.all},_) $ (a as Abs _)) = USyntax.dest_abs used a
wenzelm@60520
  1271
  | dest_all _ _ = raise RULES_ERR "dest_all" "not a !!";
wenzelm@60520
  1272
wenzelm@60520
  1273
val is_all = can (dest_all []);
wenzelm@60520
  1274
wenzelm@60520
  1275
fun strip_all used fm =
wenzelm@60520
  1276
   if (is_all fm)
wenzelm@60520
  1277
   then let val ({Bvar, Body}, used') = dest_all used fm
wenzelm@60520
  1278
            val (bvs, core, used'') = strip_all used' Body
wenzelm@60520
  1279
        in ((Bvar::bvs), core, used'')
wenzelm@60520
  1280
        end
wenzelm@60520
  1281
   else ([], fm, used);
wenzelm@60520
  1282
wenzelm@60520
  1283
fun list_break_all(Const(@{const_name Pure.all},_) $ Abs (s,ty,body)) =
wenzelm@60520
  1284
     let val (L,core) = list_break_all body
wenzelm@60520
  1285
     in ((s,ty)::L, core)
wenzelm@60520
  1286
     end
wenzelm@60520
  1287
  | list_break_all tm = ([],tm);
wenzelm@60520
  1288
wenzelm@60520
  1289
(*---------------------------------------------------------------------------
wenzelm@60520
  1290
 * Rename a term of the form
wenzelm@60520
  1291
 *
wenzelm@60520
  1292
 *      !!x1 ...xn. x1=M1 ==> ... ==> xn=Mn
wenzelm@60520
  1293
 *                  ==> ((%v1...vn. Q) x1 ... xn = g x1 ... xn.
wenzelm@60520
  1294
 * to one of
wenzelm@60520
  1295
 *
wenzelm@60520
  1296
 *      !!v1 ... vn. v1=M1 ==> ... ==> vn=Mn
wenzelm@60520
  1297
 *      ==> ((%v1...vn. Q) v1 ... vn = g v1 ... vn.
wenzelm@60520
  1298
 *
wenzelm@60520
  1299
 * This prevents name problems in extraction, and helps the result to read
wenzelm@60520
  1300
 * better. There is a problem with varstructs, since they can introduce more
wenzelm@60520
  1301
 * than n variables, and some extra reasoning needs to be done.
wenzelm@60520
  1302
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1303
wenzelm@60520
  1304
fun get ([],_,L) = rev L
wenzelm@60520
  1305
  | get (ant::rst,n,L) =
wenzelm@60520
  1306
      case (list_break_all ant)
wenzelm@60520
  1307
        of ([],_) => get (rst, n+1,L)
wenzelm@60521
  1308
         | (_,body) =>
wenzelm@60520
  1309
            let val eq = Logic.strip_imp_concl body
wenzelm@60521
  1310
                val (f,_) = USyntax.strip_comb (get_lhs eq)
wenzelm@60520
  1311
                val (vstrl,_) = USyntax.strip_abs f
wenzelm@60520
  1312
                val names  =
wenzelm@60520
  1313
                  Name.variant_list (Misc_Legacy.add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
wenzelm@60520
  1314
            in get (rst, n+1, (names,n)::L) end
wenzelm@60520
  1315
            handle TERM _ => get (rst, n+1, L)
wenzelm@60520
  1316
              | Utils.ERR _ => get (rst, n+1, L);
wenzelm@60520
  1317
wenzelm@60520
  1318
(* Note: Thm.rename_params_rule counts from 1, not 0 *)
wenzelm@60520
  1319
fun rename thm =
wenzelm@60520
  1320
  let
wenzelm@60520
  1321
    val ants = Logic.strip_imp_prems (Thm.prop_of thm)
wenzelm@60520
  1322
    val news = get (ants,1,[])
wenzelm@60520
  1323
  in fold Thm.rename_params_rule news thm end;
wenzelm@60520
  1324
wenzelm@60520
  1325
wenzelm@60520
  1326
(*---------------------------------------------------------------------------
wenzelm@60520
  1327
 * Beta-conversion to the rhs of an equation (taken from hol90/drule.sml)
wenzelm@60520
  1328
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1329
wenzelm@60520
  1330
fun list_beta_conv tm =
wenzelm@60520
  1331
  let fun rbeta th = Thm.transitive th (Thm.beta_conversion false (#2(Dcterm.dest_eq(cconcl th))))
wenzelm@60520
  1332
      fun iter [] = Thm.reflexive tm
wenzelm@60520
  1333
        | iter (v::rst) = rbeta (Thm.combination(iter rst) (Thm.reflexive v))
wenzelm@60520
  1334
  in iter  end;
wenzelm@60520
  1335
wenzelm@60520
  1336
wenzelm@60520
  1337
(*---------------------------------------------------------------------------
wenzelm@60520
  1338
 * Trace information for the rewriter
wenzelm@60520
  1339
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1340
val tracing = Unsynchronized.ref false;
wenzelm@60520
  1341
wenzelm@60520
  1342
fun say s = if !tracing then writeln s else ();
wenzelm@60520
  1343
wenzelm@60520
  1344
fun print_thms ctxt s L =
wenzelm@61268
  1345
  say (cat_lines (s :: map (Thm.string_of_thm ctxt) L));
wenzelm@60520
  1346
wenzelm@60520
  1347
fun print_term ctxt s t =
wenzelm@60520
  1348
  say (cat_lines [s, Syntax.string_of_term ctxt t]);
wenzelm@60520
  1349
wenzelm@60520
  1350
wenzelm@60520
  1351
(*---------------------------------------------------------------------------
wenzelm@60520
  1352
 * General abstraction handlers, should probably go in USyntax.
wenzelm@60520
  1353
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1354
fun mk_aabs (vstr, body) =
wenzelm@60520
  1355
  USyntax.mk_abs {Bvar = vstr, Body = body}
wenzelm@60520
  1356
  handle Utils.ERR _ => USyntax.mk_pabs {varstruct = vstr, body = body};
wenzelm@60520
  1357
wenzelm@60520
  1358
fun list_mk_aabs (vstrl,tm) =
wenzelm@60520
  1359
    fold_rev (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;
wenzelm@60520
  1360
wenzelm@60520
  1361
fun dest_aabs used tm =
wenzelm@60520
  1362
   let val ({Bvar,Body}, used') = USyntax.dest_abs used tm
wenzelm@60520
  1363
   in (Bvar, Body, used') end
wenzelm@60520
  1364
   handle Utils.ERR _ =>
wenzelm@60520
  1365
     let val {varstruct, body, used} = USyntax.dest_pabs used tm
wenzelm@60520
  1366
     in (varstruct, body, used) end;
wenzelm@60520
  1367
wenzelm@60520
  1368
fun strip_aabs used tm =
wenzelm@60520
  1369
   let val (vstr, body, used') = dest_aabs used tm
wenzelm@60520
  1370
       val (bvs, core, used'') = strip_aabs used' body
wenzelm@60520
  1371
   in (vstr::bvs, core, used'') end
wenzelm@60520
  1372
   handle Utils.ERR _ => ([], tm, used);
wenzelm@60520
  1373
wenzelm@60520
  1374
fun dest_combn tm 0 = (tm,[])
wenzelm@60520
  1375
  | dest_combn tm n =
wenzelm@60520
  1376
     let val {Rator,Rand} = USyntax.dest_comb tm
wenzelm@60520
  1377
         val (f,rands) = dest_combn Rator (n-1)
wenzelm@60520
  1378
     in (f,Rand::rands)
wenzelm@60520
  1379
     end;
wenzelm@60520
  1380
wenzelm@60520
  1381
wenzelm@60520
  1382
wenzelm@60520
  1383
wenzelm@60520
  1384
local fun dest_pair M = let val {fst,snd} = USyntax.dest_pair M in (fst,snd) end
wenzelm@60520
  1385
      fun mk_fst tm =
wenzelm@60520
  1386
          let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm
wenzelm@60520
  1387
          in  Const (@{const_name Product_Type.fst}, ty --> fty) $ tm  end
wenzelm@60520
  1388
      fun mk_snd tm =
wenzelm@60520
  1389
          let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm
wenzelm@60520
  1390
          in  Const (@{const_name Product_Type.snd}, ty --> sty) $ tm  end
wenzelm@60520
  1391
in
wenzelm@60520
  1392
fun XFILL tych x vstruct =
wenzelm@60520
  1393
  let fun traverse p xocc L =
wenzelm@60520
  1394
        if (is_Free p)
wenzelm@60520
  1395
        then tych xocc::L
wenzelm@60520
  1396
        else let val (p1,p2) = dest_pair p
wenzelm@60520
  1397
             in traverse p1 (mk_fst xocc) (traverse p2  (mk_snd xocc) L)
wenzelm@60520
  1398
             end
wenzelm@60520
  1399
  in
wenzelm@60520
  1400
  traverse vstruct x []
wenzelm@60520
  1401
end end;
wenzelm@60520
  1402
wenzelm@60520
  1403
(*---------------------------------------------------------------------------
wenzelm@60520
  1404
 * Replace a free tuple (vstr) by a universally quantified variable (a).
wenzelm@60520
  1405
 * Note that the notion of "freeness" for a tuple is different than for a
wenzelm@60520
  1406
 * variable: if variables in the tuple also occur in any other place than
wenzelm@60520
  1407
 * an occurrences of the tuple, they aren't "free" (which is thus probably
wenzelm@60520
  1408
 *  the wrong word to use).
wenzelm@60520
  1409
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1410
wenzelm@60520
  1411
fun VSTRUCT_ELIM ctxt tych a vstr th =
wenzelm@60520
  1412
  let val L = USyntax.free_vars_lr vstr
wenzelm@60520
  1413
      val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr)))
wenzelm@60520
  1414
      val thm1 = Thm.implies_intr bind1 (SUBS ctxt [SYM(Thm.assume bind1)] th)
wenzelm@60520
  1415
      val thm2 = forall_intr_list (map tych L) thm1
wenzelm@60520
  1416
      val thm3 = forall_elim_list (XFILL tych a vstr) thm2
wenzelm@60520
  1417
  in refl RS
wenzelm@60520
  1418
     rewrite_rule ctxt [Thm.symmetric (@{thm surjective_pairing} RS eq_reflection)] thm3
wenzelm@60520
  1419
  end;
wenzelm@60520
  1420
wenzelm@60520
  1421
fun PGEN ctxt tych a vstr th =
wenzelm@60520
  1422
  let val a1 = tych a
wenzelm@60781
  1423
  in Thm.forall_intr a1 (VSTRUCT_ELIM ctxt tych a vstr th) end;
wenzelm@60520
  1424
wenzelm@60520
  1425
wenzelm@60520
  1426
(*---------------------------------------------------------------------------
wenzelm@60520
  1427
 * Takes apart a paired beta-redex, looking like "(\(x,y).N) vstr", into
wenzelm@60520
  1428
 *
wenzelm@60520
  1429
 *     (([x,y],N),vstr)
wenzelm@60520
  1430
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1431
fun dest_pbeta_redex used M n =
wenzelm@60520
  1432
  let val (f,args) = dest_combn M n
wenzelm@60521
  1433
      val _ = dest_aabs used f
wenzelm@60520
  1434
  in (strip_aabs used f,args)
wenzelm@60520
  1435
  end;
wenzelm@60520
  1436
wenzelm@60520
  1437
fun pbeta_redex M n = can (fn t => dest_pbeta_redex [] t n) M;
wenzelm@60520
  1438
wenzelm@60520
  1439
fun dest_impl tm =
wenzelm@60520
  1440
  let val ants = Logic.strip_imp_prems tm
wenzelm@60520
  1441
      val eq = Logic.strip_imp_concl tm
wenzelm@60520
  1442
  in (ants,get_lhs eq)
wenzelm@60520
  1443
  end;
wenzelm@60520
  1444
wenzelm@60520
  1445
fun restricted t = is_some (USyntax.find_term
wenzelm@60520
  1446
                            (fn (Const(@{const_name Wfrec.cut},_)) =>true | _ => false)
wenzelm@60520
  1447
                            t)
wenzelm@60520
  1448
wenzelm@60520
  1449
fun CONTEXT_REWRITE_RULE main_ctxt (func, G, cut_lemma, congs) th =
wenzelm@60520
  1450
 let val globals = func::G
wenzelm@60520
  1451
     val ctxt0 = empty_simpset main_ctxt
wenzelm@60520
  1452
     val pbeta_reduce = simpl_conv ctxt0 [@{thm split_conv} RS eq_reflection];
wenzelm@60520
  1453
     val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
wenzelm@60520
  1454
     val cut_lemma' = cut_lemma RS eq_reflection
wenzelm@60520
  1455
     fun prover used ctxt thm =
wenzelm@60520
  1456
     let fun cong_prover ctxt thm =
wenzelm@60521
  1457
         let val _ = say "cong_prover:"
wenzelm@60520
  1458
             val cntxt = Simplifier.prems_of ctxt
wenzelm@60521
  1459
             val _ = print_thms ctxt "cntxt:" cntxt
wenzelm@60521
  1460
             val _ = say "cong rule:"
wenzelm@61268
  1461
             val _ = say (Thm.string_of_thm ctxt thm)
wenzelm@60520
  1462
             (* Unquantified eliminate *)
wenzelm@60520
  1463
             fun uq_eliminate (thm,imp) =
wenzelm@60520
  1464
                 let val tych = Thm.cterm_of ctxt
wenzelm@60520
  1465
                     val _ = print_term ctxt "To eliminate:" imp
wenzelm@60520
  1466
                     val ants = map tych (Logic.strip_imp_prems imp)
wenzelm@60520
  1467
                     val eq = Logic.strip_imp_concl imp
wenzelm@60520
  1468
                     val lhs = tych(get_lhs eq)
wenzelm@60520
  1469
                     val ctxt' = Simplifier.add_prems (map ASSUME ants) ctxt
wenzelm@60520
  1470
                     val lhs_eq_lhs1 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used) ctxt' lhs
wenzelm@60520
  1471
                       handle Utils.ERR _ => Thm.reflexive lhs
wenzelm@60520
  1472
                     val _ = print_thms ctxt' "proven:" [lhs_eq_lhs1]
wenzelm@60520
  1473
                     val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
wenzelm@67710
  1474
                     val lhs_eeq_lhs2 = HOLogic.mk_obj_eq lhs_eq_lhs2
wenzelm@60520
  1475
                  in
wenzelm@60520
  1476
                  lhs_eeq_lhs2 COMP thm
wenzelm@60520
  1477
                  end
wenzelm@60520
  1478
             fun pq_eliminate (thm, vlist, imp_body, lhs_eq) =
wenzelm@60520
  1479
              let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)
wenzelm@60521
  1480
                  val _ = forall (op aconv) (ListPair.zip (vlist, args))
wenzelm@60520
  1481
                    orelse error "assertion failed in CONTEXT_REWRITE_RULE"
wenzelm@60520
  1482
                  val imp_body1 = subst_free (ListPair.zip (args, vstrl))
wenzelm@60520
  1483
                                             imp_body
wenzelm@60520
  1484
                  val tych = Thm.cterm_of ctxt
wenzelm@60520
  1485
                  val ants1 = map tych (Logic.strip_imp_prems imp_body1)
wenzelm@60520
  1486
                  val eq1 = Logic.strip_imp_concl imp_body1
wenzelm@60520
  1487
                  val Q = get_lhs eq1
wenzelm@60520
  1488
                  val QeqQ1 = pbeta_reduce (tych Q)
wenzelm@60520
  1489
                  val Q1 = #2(Dcterm.dest_eq(cconcl QeqQ1))
wenzelm@60520
  1490
                  val ctxt' = Simplifier.add_prems (map ASSUME ants1) ctxt
wenzelm@60520
  1491
                  val Q1eeqQ2 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used') ctxt' Q1
wenzelm@60520
  1492
                                handle Utils.ERR _ => Thm.reflexive Q1
wenzelm@60520
  1493
                  val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2))
wenzelm@60520
  1494
                  val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
wenzelm@60520
  1495
                  val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection)
wenzelm@60520
  1496
                  val thA = Thm.transitive(QeqQ1 RS eq_reflection) Q1eeqQ2
wenzelm@60520
  1497
                  val QeeqQ3 = Thm.transitive thA Q2eeqQ3 handle THM _ =>
wenzelm@67710
  1498
                               (HOLogic.mk_obj_eq Q2eeqQ3
wenzelm@67710
  1499
                                RS (HOLogic.mk_obj_eq thA RS trans))
wenzelm@60520
  1500
                                RS eq_reflection
wenzelm@60520
  1501
                  val impth = implies_intr_list ants1 QeeqQ3
wenzelm@67710
  1502
                  val impth1 = HOLogic.mk_obj_eq impth
wenzelm@60520
  1503
                  (* Need to abstract *)
wenzelm@60520
  1504
                  val ant_th = Utils.itlist2 (PGEN ctxt' tych) args vstrl impth1
wenzelm@60520
  1505
              in ant_th COMP thm
wenzelm@60520
  1506
              end
wenzelm@60520
  1507
             fun q_eliminate (thm, imp) =
wenzelm@60520
  1508
              let val (vlist, imp_body, used') = strip_all used imp
wenzelm@60520
  1509
                  val (ants,Q) = dest_impl imp_body
wenzelm@60520
  1510
              in if (pbeta_redex Q) (length vlist)
wenzelm@60520
  1511
                 then pq_eliminate (thm, vlist, imp_body, Q)
wenzelm@60520
  1512
                 else
wenzelm@60520
  1513
                 let val tych = Thm.cterm_of ctxt
wenzelm@60520
  1514
                     val ants1 = map tych ants
wenzelm@60520
  1515
                     val ctxt' = Simplifier.add_prems (map ASSUME ants1) ctxt
wenzelm@60520
  1516
                     val Q_eeq_Q1 = Raw_Simplifier.rewrite_cterm
wenzelm@60520
  1517
                        (false,true,false) (prover used') ctxt' (tych Q)
wenzelm@60520
  1518
                      handle Utils.ERR _ => Thm.reflexive (tych Q)
wenzelm@60520
  1519
                     val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
wenzelm@67710
  1520
                     val lhs_eq_lhs2 = HOLogic.mk_obj_eq lhs_eeq_lhs2
wenzelm@60520
  1521
                     val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2
wenzelm@60520
  1522
                 in
wenzelm@60520
  1523
                 ant_th COMP thm
wenzelm@60520
  1524
              end end
wenzelm@60520
  1525
wenzelm@60520
  1526
             fun eliminate thm =
wenzelm@60520
  1527
               case Thm.prop_of thm of
wenzelm@60520
  1528
                 Const(@{const_name Pure.imp},_) $ imp $ _ =>
wenzelm@60520
  1529
                   eliminate
wenzelm@60520
  1530
                    (if not(is_all imp)
wenzelm@60520
  1531
                     then uq_eliminate (thm, imp)
wenzelm@60520
  1532
                     else q_eliminate (thm, imp))
wenzelm@60520
  1533
                            (* Assume that the leading constant is ==,   *)
wenzelm@60520
  1534
                | _ => thm  (* if it is not a ==>                        *)
wenzelm@60520
  1535
         in SOME(eliminate (rename thm)) end
wenzelm@60520
  1536
         handle Utils.ERR _ => NONE    (* FIXME handle THM as well?? *)
wenzelm@60520
  1537
wenzelm@60520
  1538
        fun restrict_prover ctxt thm =
wenzelm@60520
  1539
          let val _ = say "restrict_prover:"
wenzelm@60520
  1540
              val cntxt = rev (Simplifier.prems_of ctxt)
wenzelm@60520
  1541
              val _ = print_thms ctxt "cntxt:" cntxt
wenzelm@60520
  1542
              val Const(@{const_name Pure.imp},_) $ (Const(@{const_name Trueprop},_) $ A) $ _ =
wenzelm@60520
  1543
                Thm.prop_of thm
wenzelm@60520
  1544
              fun genl tm = let val vlist = subtract (op aconv) globals
wenzelm@60520
  1545
                                           (Misc_Legacy.add_term_frees(tm,[]))
wenzelm@60520
  1546
                            in fold_rev Forall vlist tm
wenzelm@60520
  1547
                            end
wenzelm@60520
  1548
              (*--------------------------------------------------------------
wenzelm@60520
  1549
               * This actually isn't quite right, since it will think that
wenzelm@60520
  1550
               * not-fully applied occs. of "f" in the context mean that the
wenzelm@60520
  1551
               * current call is nested. The real solution is to pass in a
wenzelm@60520
  1552
               * term "f v1..vn" which is a pattern that any full application
wenzelm@60520
  1553
               * of "f" will match.
wenzelm@60520
  1554
               *-------------------------------------------------------------*)
wenzelm@60520
  1555
              val func_name = #1(dest_Const func)
wenzelm@60520
  1556
              fun is_func (Const (name,_)) = (name = func_name)
wenzelm@60520
  1557
                | is_func _                = false
wenzelm@60520
  1558
              val rcontext = rev cntxt
wenzelm@60520
  1559
              val cncl = HOLogic.dest_Trueprop o Thm.prop_of
wenzelm@60520
  1560
              val antl = case rcontext of [] => []
wenzelm@60520
  1561
                         | _   => [USyntax.list_mk_conj(map cncl rcontext)]
wenzelm@60520
  1562
              val TC = genl(USyntax.list_mk_imp(antl, A))
wenzelm@60520
  1563
              val _ = print_term ctxt "func:" func
wenzelm@60520
  1564
              val _ = print_term ctxt "TC:" (HOLogic.mk_Trueprop TC)
wenzelm@60520
  1565
              val _ = tc_list := (TC :: !tc_list)
wenzelm@60520
  1566
              val nestedp = is_some (USyntax.find_term is_func TC)
wenzelm@60520
  1567
              val _ = if nestedp then say "nested" else say "not_nested"
wenzelm@60520
  1568
              val th' = if nestedp then raise RULES_ERR "solver" "nested function"
wenzelm@60520
  1569
                        else let val cTC = Thm.cterm_of ctxt (HOLogic.mk_Trueprop TC)
wenzelm@60520
  1570
                             in case rcontext of
wenzelm@60520
  1571
                                [] => SPEC_ALL(ASSUME cTC)
wenzelm@60520
  1572
                               | _ => MP (SPEC_ALL (ASSUME cTC))
wenzelm@60520
  1573
                                         (LIST_CONJ rcontext)
wenzelm@60520
  1574
                             end
wenzelm@60520
  1575
              val th'' = th' RS thm
wenzelm@60520
  1576
          in SOME (th'')
wenzelm@60520
  1577
          end handle Utils.ERR _ => NONE    (* FIXME handle THM as well?? *)
wenzelm@60520
  1578
    in
wenzelm@60520
  1579
    (if (is_cong thm) then cong_prover else restrict_prover) ctxt thm
wenzelm@60520
  1580
    end
wenzelm@60520
  1581
    val ctm = Thm.cprop_of th
wenzelm@60520
  1582
    val names = Misc_Legacy.add_term_names (Thm.term_of ctm, [])
wenzelm@60520
  1583
    val th1 =
wenzelm@60520
  1584
      Raw_Simplifier.rewrite_cterm (false, true, false)
wenzelm@60520
  1585
        (prover names) (ctxt0 addsimps [cut_lemma'] |> fold Simplifier.add_eqcong congs) ctm
wenzelm@60520
  1586
    val th2 = Thm.equal_elim th1 th
wenzelm@60520
  1587
 in
wenzelm@60520
  1588
 (th2, filter_out restricted (!tc_list))
wenzelm@60520
  1589
 end;
wenzelm@60520
  1590
wenzelm@60520
  1591
wenzelm@60520
  1592
fun prove ctxt strict (t, tac) =
wenzelm@60520
  1593
  let
wenzelm@60520
  1594
    val ctxt' = Variable.auto_fixes t ctxt;
wenzelm@60520
  1595
  in
wenzelm@60520
  1596
    if strict
wenzelm@60520
  1597
    then Goal.prove ctxt' [] [] t (K tac)
wenzelm@60520
  1598
    else Goal.prove ctxt' [] [] t (K tac)
wenzelm@60520
  1599
      handle ERROR msg => (warning msg; raise RULES_ERR "prove" msg)
wenzelm@60520
  1600
  end;
wenzelm@60520
  1601
wenzelm@60520
  1602
end;
wenzelm@60520
  1603
wenzelm@60520
  1604
wenzelm@60521
  1605
wenzelm@60520
  1606
(*** theory operations ***)
wenzelm@60520
  1607
wenzelm@60520
  1608
structure Thry: THRY =
wenzelm@60520
  1609
struct
wenzelm@60520
  1610
wenzelm@60520
  1611
wenzelm@60520
  1612
fun THRY_ERR func mesg = Utils.ERR {module = "Thry", func = func, mesg = mesg};
wenzelm@60520
  1613
wenzelm@60520
  1614
wenzelm@60520
  1615
(*---------------------------------------------------------------------------
wenzelm@60520
  1616
 *    Matching
wenzelm@60520
  1617
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1618
wenzelm@60520
  1619
local
wenzelm@60520
  1620
wenzelm@60520
  1621
fun tybind (ixn, (S, T)) = (TVar (ixn, S), T);
wenzelm@60520
  1622
wenzelm@60520
  1623
in
wenzelm@60520
  1624
wenzelm@60520
  1625
fun match_term thry pat ob =
wenzelm@60520
  1626
  let
wenzelm@60520
  1627
    val (ty_theta, tm_theta) = Pattern.match thry (pat,ob) (Vartab.empty, Vartab.empty);
wenzelm@60520
  1628
    fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.subst_type ty_theta T), t)
wenzelm@60520
  1629
  in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta))
wenzelm@60520
  1630
  end;
wenzelm@60520
  1631
wenzelm@60520
  1632
fun match_type thry pat ob =
wenzelm@60520
  1633
  map tybind (Vartab.dest (Sign.typ_match thry (pat, ob) Vartab.empty));
wenzelm@60520
  1634
wenzelm@60520
  1635
end;
wenzelm@60520
  1636
wenzelm@60520
  1637
wenzelm@60520
  1638
(*---------------------------------------------------------------------------
wenzelm@60520
  1639
 * Typing
wenzelm@60520
  1640
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1641
wenzelm@60520
  1642
fun typecheck thy t =
wenzelm@60520
  1643
  Thm.global_cterm_of thy t
wenzelm@60520
  1644
    handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg
wenzelm@60520
  1645
      | TERM (msg, _) => raise THRY_ERR "typecheck" msg;
wenzelm@60520
  1646
wenzelm@60520
  1647
wenzelm@60520
  1648
(*---------------------------------------------------------------------------
wenzelm@60520
  1649
 * Get information about datatypes
wenzelm@60520
  1650
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1651
wenzelm@60520
  1652
fun match_info thy dtco =
wenzelm@60520
  1653
  case (BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] dtco,
wenzelm@60520
  1654
         BNF_LFP_Compat.get_constrs thy dtco) of
wenzelm@60520
  1655
      (SOME {case_name, ... }, SOME constructors) =>
wenzelm@60520
  1656
        SOME {case_const = Const (case_name, Sign.the_const_type thy case_name), constructors = map Const constructors}
wenzelm@60520
  1657
    | _ => NONE;
wenzelm@60520
  1658
wenzelm@60520
  1659
fun induct_info thy dtco = case BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] dtco of
wenzelm@60520
  1660
        NONE => NONE
wenzelm@60520
  1661
      | SOME {nchotomy, ...} =>
wenzelm@60520
  1662
          SOME {nchotomy = nchotomy,
wenzelm@60520
  1663
                constructors = (map Const o the o BNF_LFP_Compat.get_constrs thy) dtco};
wenzelm@60520
  1664
wenzelm@60520
  1665
fun extract_info thy =
wenzelm@60520
  1666
 let val infos = map snd (Symtab.dest (BNF_LFP_Compat.get_all thy [BNF_LFP_Compat.Keep_Nesting]))
wenzelm@60520
  1667
 in {case_congs = map (mk_meta_eq o #case_cong) infos,
wenzelm@60520
  1668
     case_rewrites = maps (map mk_meta_eq o #case_rewrites) infos}
wenzelm@60520
  1669
 end;
wenzelm@60520
  1670
wenzelm@60520
  1671
wenzelm@60520
  1672
end;
wenzelm@60520
  1673
wenzelm@60520
  1674
wenzelm@60521
  1675
wenzelm@60520
  1676
(*** first part of main module ***)
wenzelm@60520
  1677
wenzelm@60520
  1678
structure Prim: PRIM =
wenzelm@60520
  1679
struct
wenzelm@60520
  1680
wenzelm@60520
  1681
val trace = Unsynchronized.ref false;
wenzelm@60520
  1682
wenzelm@60520
  1683
wenzelm@60520
  1684
fun TFL_ERR func mesg = Utils.ERR {module = "Tfl", func = func, mesg = mesg};
wenzelm@60520
  1685
wenzelm@60520
  1686
val concl = #2 o Rules.dest_thm;
wenzelm@60520
  1687
wenzelm@60520
  1688
val list_mk_type = Utils.end_itlist (curry (op -->));
wenzelm@60520
  1689
wenzelm@60520
  1690
fun front_last [] = raise TFL_ERR "front_last" "empty list"
wenzelm@60520
  1691
  | front_last [x] = ([],x)
wenzelm@60520
  1692
  | front_last (h::t) =
wenzelm@60520
  1693
     let val (pref,x) = front_last t
wenzelm@60520
  1694
     in
wenzelm@60520
  1695
        (h::pref,x)
wenzelm@60520
  1696
     end;
wenzelm@60520
  1697
wenzelm@60520
  1698
wenzelm@60520
  1699
(*---------------------------------------------------------------------------
wenzelm@60520
  1700
 * The next function is common to pattern-match translation and
wenzelm@60520
  1701
 * proof of completeness of cases for the induction theorem.
wenzelm@60520
  1702
 *
wenzelm@60520
  1703
 * The curried function "gvvariant" returns a function to generate distinct
wenzelm@60520
  1704
 * variables that are guaranteed not to be in names.  The names of
wenzelm@60520
  1705
 * the variables go u, v, ..., z, aa, ..., az, ...  The returned
wenzelm@60520
  1706
 * function contains embedded refs!
wenzelm@60520
  1707
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1708
fun gvvariant names =
wenzelm@60520
  1709
  let val slist = Unsynchronized.ref names
wenzelm@60520
  1710
      val vname = Unsynchronized.ref "u"
wenzelm@60520
  1711
      fun new() =
wenzelm@60520
  1712
         if member (op =) (!slist) (!vname)
wenzelm@60520
  1713
         then (vname := Symbol.bump_string (!vname);  new())
wenzelm@60520
  1714
         else (slist := !vname :: !slist;  !vname)
wenzelm@60520
  1715
  in
wenzelm@60520
  1716
  fn ty => Free(new(), ty)
wenzelm@60520
  1717
  end;
wenzelm@60520
  1718
wenzelm@60520
  1719
wenzelm@60520
  1720
(*---------------------------------------------------------------------------
wenzelm@60520
  1721
 * Used in induction theorem production. This is the simple case of
wenzelm@60520
  1722
 * partitioning up pattern rows by the leading constructor.
wenzelm@60520
  1723
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1724
fun ipartition gv (constructors,rows) =
wenzelm@60520
  1725
  let fun pfail s = raise TFL_ERR "partition.part" s
wenzelm@60520
  1726
      fun part {constrs = [],   rows = [],   A} = rev A
wenzelm@60520
  1727
        | part {constrs = [],   rows = _::_, A} = pfail"extra cases in defn"
wenzelm@60520
  1728
        | part {constrs = _::_, rows = [],   A} = pfail"cases missing in defn"
wenzelm@60520
  1729
        | part {constrs = c::crst, rows,     A} =
wenzelm@60520
  1730
          let val (c, T) = dest_Const c
wenzelm@60520
  1731
              val L = binder_types T
wenzelm@60520
  1732
              val (in_group, not_in_group) =
wenzelm@60520
  1733
               fold_rev (fn (row as (p::rst, rhs)) =>
wenzelm@60520
  1734
                         fn (in_group,not_in_group) =>
wenzelm@60520
  1735
                  let val (pc,args) = USyntax.strip_comb p
wenzelm@60520
  1736
                  in if (#1(dest_Const pc) = c)
wenzelm@60520
  1737
                     then ((args@rst, rhs)::in_group, not_in_group)
wenzelm@60520
  1738
                     else (in_group, row::not_in_group)
wenzelm@60520
  1739
                  end)      rows ([],[])
wenzelm@60520
  1740
              val col_types = Utils.take type_of (length L, #1(hd in_group))
wenzelm@60520
  1741
          in
wenzelm@60520
  1742
          part{constrs = crst, rows = not_in_group,
wenzelm@60520
  1743
               A = {constructor = c,
wenzelm@60520
  1744
                    new_formals = map gv col_types,
wenzelm@60520
  1745
                    group = in_group}::A}
wenzelm@60520
  1746
          end
wenzelm@60520
  1747
  in part{constrs = constructors, rows = rows, A = []}
wenzelm@60520
  1748
  end;
wenzelm@60520
  1749
wenzelm@60520
  1750
wenzelm@60520
  1751
wenzelm@60520
  1752
(*---------------------------------------------------------------------------
wenzelm@60520
  1753
 * Each pattern carries with it a tag (i,b) where
wenzelm@60520
  1754
 * i is the clause it came from and
wenzelm@60520
  1755
 * b=true indicates that clause was given by the user
wenzelm@60520
  1756
 * (or is an instantiation of a user supplied pattern)
wenzelm@60520
  1757
 * b=false --> i = ~1
wenzelm@60520
  1758
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1759
wenzelm@60520
  1760
type pattern = term * (int * bool)
wenzelm@60520
  1761
wenzelm@60520
  1762
fun pattern_map f (tm,x) = (f tm, x);
wenzelm@60520
  1763
wenzelm@60520
  1764
fun pattern_subst theta = pattern_map (subst_free theta);
wenzelm@60520
  1765
wenzelm@60520
  1766
val pat_of = fst;
wenzelm@60520
  1767
fun row_of_pat x = fst (snd x);
wenzelm@60520
  1768
fun given x = snd (snd x);
wenzelm@60520
  1769
wenzelm@60520
  1770
(*---------------------------------------------------------------------------
wenzelm@60520
  1771
 * Produce an instance of a constructor, plus genvars for its arguments.
wenzelm@60520
  1772
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1773
fun fresh_constr ty_match colty gv c =
wenzelm@60520
  1774
  let val (_,Ty) = dest_Const c
wenzelm@60520
  1775
      val L = binder_types Ty
wenzelm@60520
  1776
      and ty = body_type Ty
wenzelm@60520
  1777
      val ty_theta = ty_match ty colty
wenzelm@60520
  1778
      val c' = USyntax.inst ty_theta c
wenzelm@60520
  1779
      val gvars = map (USyntax.inst ty_theta o gv) L
wenzelm@60520
  1780
  in (c', gvars)
wenzelm@60520
  1781
  end;
wenzelm@60520
  1782
wenzelm@60520
  1783
wenzelm@60520
  1784
(*---------------------------------------------------------------------------
wenzelm@60520
  1785
 * Goes through a list of rows and picks out the ones beginning with a
wenzelm@60520
  1786
 * pattern with constructor = name.
wenzelm@60520
  1787
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1788
fun mk_group name rows =
wenzelm@60520
  1789
  fold_rev (fn (row as ((prfx, p::rst), rhs)) =>
wenzelm@60520
  1790
            fn (in_group,not_in_group) =>
wenzelm@60520
  1791
               let val (pc,args) = USyntax.strip_comb p
wenzelm@60520
  1792
               in if ((#1 (Term.dest_Const pc) = name) handle TERM _ => false)
wenzelm@60520
  1793
                  then (((prfx,args@rst), rhs)::in_group, not_in_group)
wenzelm@60520
  1794
                  else (in_group, row::not_in_group) end)
wenzelm@60520
  1795
      rows ([],[]);
wenzelm@60520
  1796
wenzelm@60520
  1797
(*---------------------------------------------------------------------------
wenzelm@60520
  1798
 * Partition the rows. Not efficient: we should use hashing.
wenzelm@60520
  1799
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1800
fun partition _ _ (_,_,_,[]) = raise TFL_ERR "partition" "no rows"
wenzelm@60520
  1801
  | partition gv ty_match
wenzelm@60520
  1802
              (constructors, colty, res_ty, rows as (((prfx,_),_)::_)) =
wenzelm@60520
  1803
let val fresh = fresh_constr ty_match colty gv
wenzelm@60520
  1804
     fun part {constrs = [],      rows, A} = rev A
wenzelm@60520
  1805
       | part {constrs = c::crst, rows, A} =
wenzelm@60520
  1806
         let val (c',gvars) = fresh c
wenzelm@60520
  1807
             val (in_group, not_in_group) = mk_group (#1 (dest_Const c')) rows
wenzelm@60520
  1808
             val in_group' =
wenzelm@60520
  1809
                 if (null in_group)  (* Constructor not given *)
wenzelm@60520
  1810
                 then [((prfx, #2(fresh c)), (USyntax.ARB res_ty, (~1,false)))]
wenzelm@60520
  1811
                 else in_group
wenzelm@60520
  1812
         in
wenzelm@60520
  1813
         part{constrs = crst,
wenzelm@60520
  1814
              rows = not_in_group,
wenzelm@60520
  1815
              A = {constructor = c',
wenzelm@60520
  1816
                   new_formals = gvars,
wenzelm@60520
  1817
                   group = in_group'}::A}
wenzelm@60520
  1818
         end
wenzelm@60520
  1819
in part{constrs=constructors, rows=rows, A=[]}
wenzelm@60520
  1820
end;
wenzelm@60520
  1821
wenzelm@60520
  1822
(*---------------------------------------------------------------------------
wenzelm@60520
  1823
 * Misc. routines used in mk_case
wenzelm@60520
  1824
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1825
wenzelm@60520
  1826
fun mk_pat (c,l) =
wenzelm@60520
  1827
  let val L = length (binder_types (type_of c))
wenzelm@60520
  1828
      fun build (prfx,tag,plist) =
wenzelm@60520
  1829
          let val (args, plist') = chop L plist
wenzelm@60520
  1830
          in (prfx,tag,list_comb(c,args)::plist') end
wenzelm@60520
  1831
  in map build l end;
wenzelm@60520
  1832
wenzelm@60520
  1833
fun v_to_prfx (prfx, v::pats) = (v::prfx,pats)
wenzelm@60520
  1834
  | v_to_prfx _ = raise TFL_ERR "mk_case" "v_to_prfx";
wenzelm@60520
  1835
wenzelm@60520
  1836
fun v_to_pats (v::prfx,tag, pats) = (prfx, tag, v::pats)
wenzelm@60520
  1837
  | v_to_pats _ = raise TFL_ERR "mk_case" "v_to_pats";
wenzelm@60520
  1838
wenzelm@60520
  1839
wenzelm@60520
  1840
(*----------------------------------------------------------------------------
wenzelm@60520
  1841
 * Translation of pattern terms into nested case expressions.
wenzelm@60520
  1842
 *
wenzelm@60520
  1843
 * This performs the translation and also builds the full set of patterns.
wenzelm@60520
  1844
 * Thus it supports the construction of induction theorems even when an
wenzelm@60520
  1845
 * incomplete set of patterns is given.
wenzelm@60520
  1846
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1847
wenzelm@60520
  1848
fun mk_case ty_info ty_match usednames range_ty =
wenzelm@60520
  1849
 let
wenzelm@60520
  1850
 fun mk_case_fail s = raise TFL_ERR "mk_case" s
wenzelm@60520
  1851
 val fresh_var = gvvariant usednames
wenzelm@60520
  1852
 val divide = partition fresh_var ty_match
wenzelm@60521
  1853
 fun expand _ ty ((_,[]), _) = mk_case_fail"expand_var_row"
wenzelm@60520
  1854
   | expand constructors ty (row as ((prfx, p::rst), rhs)) =
wenzelm@60520
  1855
       if (is_Free p)
wenzelm@60520
  1856
       then let val fresh = fresh_constr ty_match ty fresh_var
wenzelm@60520
  1857
                fun expnd (c,gvs) =
wenzelm@60520
  1858
                  let val capp = list_comb(c,gvs)
wenzelm@60520
  1859
                  in ((prfx, capp::rst), pattern_subst[(p,capp)] rhs)
wenzelm@60520
  1860
                  end
wenzelm@60520
  1861
            in map expnd (map fresh constructors)  end
wenzelm@60520
  1862
       else [row]
wenzelm@60520
  1863
 fun mk{rows=[],...} = mk_case_fail"no rows"
wenzelm@60520
  1864
   | mk{path=[], rows = ((prfx, []), (tm,tag))::_} =  (* Done *)
wenzelm@60520
  1865
        ([(prfx,tag,[])], tm)
wenzelm@60520
  1866
   | mk{path=[], rows = _::_} = mk_case_fail"blunder"
wenzelm@60520
  1867
   | mk{path as u::rstp, rows as ((prfx, []), rhs)::rst} =
wenzelm@60520
  1868
        mk{path = path,
wenzelm@60520
  1869
           rows = ((prfx, [fresh_var(type_of u)]), rhs)::rst}
wenzelm@60520
  1870
   | mk{path = u::rstp, rows as ((_, p::_), _)::_} =
wenzelm@60520
  1871
     let val (pat_rectangle,rights) = ListPair.unzip rows
wenzelm@60520
  1872
         val col0 = map(hd o #2) pat_rectangle
wenzelm@60520
  1873
     in
wenzelm@60520
  1874
     if (forall is_Free col0)
wenzelm@60520
  1875
     then let val rights' = map (fn(v,e) => pattern_subst[(v,u)] e)
wenzelm@60520
  1876
                                (ListPair.zip (col0, rights))
wenzelm@60520
  1877
              val pat_rectangle' = map v_to_prfx pat_rectangle
wenzelm@60520
  1878
              val (pref_patl,tm) = mk{path = rstp,
wenzelm@60520
  1879
                                      rows = ListPair.zip (pat_rectangle',
wenzelm@60520
  1880
                                                           rights')}
wenzelm@60520
  1881
          in (map v_to_pats pref_patl, tm)
wenzelm@60520
  1882
          end
wenzelm@60520
  1883
     else
wenzelm@60520
  1884
     let val pty as Type (ty_name,_) = type_of p
wenzelm@60520
  1885
     in
wenzelm@60520
  1886
     case (ty_info ty_name)
wenzelm@60520
  1887
     of NONE => mk_case_fail("Not a known datatype: "^ty_name)
wenzelm@60520
  1888
      | SOME{case_const,constructors} =>
wenzelm@60520
  1889
        let
wenzelm@60520
  1890
            val case_const_name = #1(dest_Const case_const)
wenzelm@60520
  1891
            val nrows = maps (expand constructors pty) rows
wenzelm@60520
  1892
            val subproblems = divide(constructors, pty, range_ty, nrows)
wenzelm@60520
  1893
            val groups      = map #group subproblems
wenzelm@60520
  1894
            and new_formals = map #new_formals subproblems
wenzelm@60520
  1895
            and constructors' = map #constructor subproblems
wenzelm@60520
  1896
            val news = map (fn (nf,rows) => {path = nf@rstp, rows=rows})
wenzelm@60520
  1897
                           (ListPair.zip (new_formals, groups))
wenzelm@60520
  1898
            val rec_calls = map mk news
wenzelm@60520
  1899
            val (pat_rect,dtrees) = ListPair.unzip rec_calls
wenzelm@60520
  1900
            val case_functions = map USyntax.list_mk_abs
wenzelm@60520
  1901
                                  (ListPair.zip (new_formals, dtrees))
wenzelm@60520
  1902
            val types = map type_of (case_functions@[u]) @ [range_ty]
wenzelm@60520
  1903
            val case_const' = Const(case_const_name, list_mk_type types)
wenzelm@60520
  1904
            val tree = list_comb(case_const', case_functions@[u])
wenzelm@60520
  1905
            val pat_rect1 = flat (ListPair.map mk_pat (constructors', pat_rect))
wenzelm@60520
  1906
        in (pat_rect1,tree)
wenzelm@60520
  1907
        end
wenzelm@60520
  1908
     end end
wenzelm@60520
  1909
 in mk
wenzelm@60520
  1910
 end;
wenzelm@60520
  1911
wenzelm@60520
  1912
wenzelm@60520
  1913
(* Repeated variable occurrences in a pattern are not allowed. *)
wenzelm@60520
  1914
fun FV_multiset tm =
wenzelm@60520
  1915
   case (USyntax.dest_term tm)
wenzelm@60520
  1916
     of USyntax.VAR{Name = c, Ty = T} => [Free(c, T)]
wenzelm@60520
  1917
      | USyntax.CONST _ => []
wenzelm@60520
  1918
      | USyntax.COMB{Rator, Rand} => FV_multiset Rator @ FV_multiset Rand
wenzelm@60520
  1919
      | USyntax.LAMB _ => raise TFL_ERR "FV_multiset" "lambda";
wenzelm@60520
  1920
wenzelm@60520
  1921
fun no_repeat_vars thy pat =
wenzelm@60520
  1922
 let fun check [] = true
wenzelm@60520
  1923
       | check (v::rst) =
wenzelm@60520
  1924
         if member (op aconv) rst v then
wenzelm@60520
  1925
            raise TFL_ERR "no_repeat_vars"
wenzelm@60520
  1926
                          (quote (#1 (dest_Free v)) ^
wenzelm@60520
  1927
                          " occurs repeatedly in the pattern " ^
wenzelm@60520
  1928
                          quote (Syntax.string_of_term_global thy pat))
wenzelm@60520
  1929
         else check rst
wenzelm@60520
  1930
 in check (FV_multiset pat)
wenzelm@60520
  1931
 end;
wenzelm@60520
  1932
wenzelm@60520
  1933
fun dest_atom (Free p) = p
wenzelm@60520
  1934
  | dest_atom (Const p) = p
wenzelm@60520
  1935
  | dest_atom  _ = raise TFL_ERR "dest_atom" "function name not an identifier";
wenzelm@60520
  1936
wenzelm@60520
  1937
fun same_name (p,q) = #1(dest_atom p) = #1(dest_atom q);
wenzelm@60520
  1938
wenzelm@60520
  1939
local fun mk_functional_err s = raise TFL_ERR "mk_functional" s
wenzelm@60520
  1940
      fun single [_$_] =
wenzelm@60520
  1941
              mk_functional_err "recdef does not allow currying"
wenzelm@60520
  1942
        | single [f] = f
wenzelm@60520
  1943
        | single fs  =
wenzelm@60520
  1944
              (*multiple function names?*)
wenzelm@60520
  1945
              if length (distinct same_name fs) < length fs
wenzelm@60520
  1946
              then mk_functional_err
wenzelm@60520
  1947
                   "The function being declared appears with multiple types"
wenzelm@60520
  1948
              else mk_functional_err
wenzelm@60520
  1949
                   (string_of_int (length fs) ^
wenzelm@60520
  1950
                    " distinct function names being declared")
wenzelm@60520
  1951
in
wenzelm@60520
  1952
fun mk_functional thy clauses =
wenzelm@60520
  1953
 let val (L,R) = ListPair.unzip (map HOLogic.dest_eq clauses
wenzelm@60520
  1954
                   handle TERM _ => raise TFL_ERR "mk_functional"
wenzelm@60520
  1955
                        "recursion equations must use the = relation")
wenzelm@60520
  1956
     val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L)
wenzelm@60520
  1957
     val atom = single (distinct (op aconv) funcs)
wenzelm@60520
  1958
     val (fname,ftype) = dest_atom atom
wenzelm@60521
  1959
     val _ = map (no_repeat_vars thy) pats
wenzelm@60520
  1960
     val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
wenzelm@60520
  1961
                              map_index (fn (i, t) => (t,(i,true))) R)
wenzelm@60520
  1962
     val names = List.foldr Misc_Legacy.add_term_names [] R
wenzelm@60520
  1963
     val atype = type_of(hd pats)
wenzelm@60520
  1964
     and aname = singleton (Name.variant_list names) "a"
wenzelm@60520
  1965
     val a = Free(aname,atype)
wenzelm@60520
  1966
     val ty_info = Thry.match_info thy
wenzelm@60520
  1967
     val ty_match = Thry.match_type thy
wenzelm@60520
  1968
     val range_ty = type_of (hd R)
wenzelm@60520
  1969
     val (patts, case_tm) = mk_case ty_info ty_match (aname::names) range_ty
wenzelm@60520
  1970
                                    {path=[a], rows=rows}
wenzelm@60520
  1971
     val patts1 = map (fn (_,tag,[pat]) => (pat,tag)) patts
wenzelm@60520
  1972
          handle Match => mk_functional_err "error in pattern-match translation"
wenzelm@60520
  1973
     val patts2 = Library.sort (Library.int_ord o apply2 row_of_pat) patts1
wenzelm@60520
  1974
     val finals = map row_of_pat patts2
wenzelm@60520
  1975
     val originals = map (row_of_pat o #2) rows
wenzelm@60521
  1976
     val _ = case (subtract (op =) finals originals)
wenzelm@60520
  1977
             of [] => ()
wenzelm@60520
  1978
          | L => mk_functional_err
wenzelm@60520
  1979
 ("The following clauses are redundant (covered by preceding clauses): " ^
wenzelm@60520
  1980
                   commas (map (fn i => string_of_int (i + 1)) L))
wenzelm@60520
  1981
 in {functional = Abs(Long_Name.base_name fname, ftype,
wenzelm@60520
  1982
                      abstract_over (atom, absfree (aname,atype) case_tm)),
wenzelm@60520
  1983
     pats = patts2}
wenzelm@60520
  1984
end end;
wenzelm@60520
  1985
wenzelm@60520
  1986
wenzelm@60520
  1987
(*----------------------------------------------------------------------------
wenzelm@60520
  1988
 *
wenzelm@60520
  1989
 *                    PRINCIPLES OF DEFINITION
wenzelm@60520
  1990
 *
wenzelm@60520
  1991
 *---------------------------------------------------------------------------*)
wenzelm@60520
  1992
wenzelm@60520
  1993
wenzelm@60520
  1994
(*For Isabelle, the lhs of a definition must be a constant.*)
wenzelm@60520
  1995
fun const_def sign (c, Ty, rhs) =
wenzelm@60520
  1996
  singleton (Syntax.check_terms (Proof_Context.init_global sign))
wenzelm@60520
  1997
    (Const(@{const_name Pure.eq},dummyT) $ Const(c,Ty) $ rhs);
wenzelm@60520
  1998
wenzelm@60520
  1999
(*Make all TVars available for instantiation by adding a ? to the front*)
wenzelm@60520
  2000
fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts)
wenzelm@60520
  2001
  | poly_tvars (TFree (a,sort)) = TVar (("?" ^ a, 0), sort)
wenzelm@60520
  2002
  | poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort);
wenzelm@60520
  2003
wenzelm@60520
  2004
local
wenzelm@60520
  2005
  val f_eq_wfrec_R_M =
wenzelm@60522
  2006
    #ant(USyntax.dest_imp(#2(USyntax.strip_forall (concl @{thm tfl_wfrec}))))
wenzelm@60520
  2007
  val {lhs=f, rhs} = USyntax.dest_eq f_eq_wfrec_R_M
wenzelm@60521
  2008
  val _ = dest_Free f
wenzelm@60520
  2009
  val (wfrec,_) = USyntax.strip_comb rhs
wenzelm@60520
  2010
in
wenzelm@60520
  2011
wenzelm@60520
  2012
fun wfrec_definition0 fid R (functional as Abs(x, Ty, _)) thy =
wenzelm@60520
  2013
  let
wenzelm@60520
  2014
    val def_name = Thm.def_name (Long_Name.base_name fid)
wenzelm@60520
  2015
    val wfrec_R_M = map_types poly_tvars (wfrec $ map_types poly_tvars R) $ functional
wenzelm@60520
  2016
    val def_term = const_def thy (fid, Ty, wfrec_R_M)
wenzelm@60520
  2017
    val ([def], thy') =
wenzelm@60520
  2018
      Global_Theory.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy
wenzelm@60520
  2019
  in (def, thy') end;
wenzelm@60520
  2020
wenzelm@60520
  2021
end;
wenzelm@60520
  2022
wenzelm@60520
  2023
wenzelm@60520
  2024
wenzelm@60520
  2025
(*---------------------------------------------------------------------------
wenzelm@60520
  2026
 * This structure keeps track of congruence rules that aren't derived
wenzelm@60520
  2027
 * from a datatype definition.
wenzelm@60520
  2028
 *---------------------------------------------------------------------------*)
wenzelm@60520
  2029
fun extraction_thms thy =
wenzelm@60520
  2030
 let val {case_rewrites,case_congs} = Thry.extract_info thy
wenzelm@60520
  2031
 in (case_rewrites, case_congs)
wenzelm@60520
  2032
 end;
wenzelm@60520
  2033
wenzelm@60520
  2034
wenzelm@60520
  2035
(*---------------------------------------------------------------------------
wenzelm@60520
  2036
 * Pair patterns with termination conditions. The full list of patterns for
wenzelm@60520
  2037
 * a definition is merged with the TCs arising from the user-given clauses.
wenzelm@60520
  2038
 * There can be fewer clauses than the full list, if the user omitted some
wenzelm@60520
  2039
 * cases. This routine is used to prepare input for mk_induction.
wenzelm@60520
  2040
 *---------------------------------------------------------------------------*)
wenzelm@60520
  2041
fun merge full_pats TCs =
wenzelm@60520
  2042
let fun insert (p,TCs) =
wenzelm@60520
  2043
      let fun insrt ((x as (h,[]))::rst) =
wenzelm@60520
  2044
                 if (p aconv h) then (p,TCs)::rst else x::insrt rst
wenzelm@60520
  2045
            | insrt (x::rst) = x::insrt rst
wenzelm@60520
  2046
            | insrt[] = raise TFL_ERR "merge.insert" "pattern not found"
wenzelm@60520
  2047
      in insrt end
wenzelm@60520
  2048
    fun pass ([],ptcl_final) = ptcl_final
wenzelm@60520
  2049
      | pass (ptcs::tcl, ptcl) = pass(tcl, insert ptcs ptcl)
wenzelm@60520
  2050
in
wenzelm@60520
  2051
  pass (TCs, map (fn p => (p,[])) full_pats)
wenzelm@60520
  2052
end;
wenzelm@60520
  2053
wenzelm@60520
  2054
wenzelm@60520
  2055
fun givens pats = map pat_of (filter given pats);
wenzelm@60520
  2056
wenzelm@60520
  2057
fun post_definition ctxt meta_tflCongs (def, pats) =
wenzelm@60520
  2058
 let val thy = Proof_Context.theory_of ctxt
wenzelm@60520
  2059
     val tych = Thry.typecheck thy
wenzelm@60520
  2060
     val f = #lhs(USyntax.dest_eq(concl def))
wenzelm@60522
  2061
     val corollary = Rules.MATCH_MP @{thm tfl_wfrec} def
wenzelm@60520
  2062
     val pats' = filter given pats
wenzelm@60520
  2063
     val given_pats = map pat_of pats'
wenzelm@60520
  2064
     val rows = map row_of_pat pats'
wenzelm@60520
  2065
     val WFR = #ant(USyntax.dest_imp(concl corollary))
wenzelm@60520
  2066
     val R = #Rand(USyntax.dest_comb WFR)
wenzelm@60520
  2067
     val corollary' = Rules.UNDISCH corollary  (* put WF R on assums *)
wenzelm@60520
  2068
     val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary') given_pats
wenzelm@60520
  2069
     val (case_rewrites,context_congs) = extraction_thms thy
wenzelm@60520
  2070
     (*case_ss causes minimal simplification: bodies of case expressions are
wenzelm@60520
  2071
       not simplified. Otherwise large examples (Red-Black trees) are too
wenzelm@60520
  2072
       slow.*)
wenzelm@60520
  2073
     val case_simpset =
wenzelm@60520
  2074
       put_simpset HOL_basic_ss ctxt
wenzelm@60520
  2075
          addsimps case_rewrites
wenzelm@60520
  2076
          |> fold (Simplifier.add_cong o #case_cong_weak o snd)
wenzelm@60520
  2077
              (Symtab.dest (BNF_LFP_Compat.get_all thy [BNF_LFP_Compat.Keep_Nesting]))
wenzelm@60520
  2078
     val corollaries' = map (Simplifier.simplify case_simpset) corollaries
wenzelm@60520
  2079
     val extract =
wenzelm@60520
  2080
      Rules.CONTEXT_REWRITE_RULE ctxt (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)
wenzelm@60520
  2081
     val (rules, TCs) = ListPair.unzip (map extract corollaries')
wenzelm@60522
  2082
     val rules0 = map (rewrite_rule ctxt @{thms tfl_cut_def}) rules
wenzelm@60520
  2083
     val mk_cond_rule = Rules.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
wenzelm@60520
  2084
     val rules1 = Rules.LIST_CONJ(map mk_cond_rule rules0)
wenzelm@60520
  2085
 in
wenzelm@60520
  2086
 {rules = rules1,
wenzelm@60520
  2087
  rows = rows,
wenzelm@60520
  2088
  full_pats_TCs = merge (map pat_of pats) (ListPair.zip (given_pats, TCs)),
wenzelm@60520
  2089
  TCs = TCs}
wenzelm@60520
  2090
 end;
wenzelm@60520
  2091
wenzelm@60520
  2092
wenzelm@60520
  2093
(*----------------------------------------------------------------------------
wenzelm@60520
  2094
 *
wenzelm@60520
  2095
 *                           INDUCTION THEOREM
wenzelm@60520
  2096
 *
wenzelm@60520
  2097
 *---------------------------------------------------------------------------*)
wenzelm@60520
  2098
wenzelm@60520
  2099
wenzelm@60520
  2100
(*------------------------  Miscellaneous function  --------------------------
wenzelm@60520
  2101
 *
wenzelm@60520
  2102
 *           [x_1,...,x_n]     ?v_1...v_n. M[v_1,...,v_n]
wenzelm@60520
  2103
 *     -----------------------------------------------------------
wenzelm@60520
  2104
 *     ( M[x_1,...,x_n], [(x_i,?v_1...v_n. M[v_1,...,v_n]),
wenzelm@60520
  2105
 *                        ...
wenzelm@60520
  2106
 *                        (x_j,?v_n. M[x_1,...,x_(n-1),v_n])] )
wenzelm@60520
  2107
 *
wenzelm@60520
  2108
 * This function is totally ad hoc. Used in the production of the induction
wenzelm@60520
  2109
 * theorem. The nchotomy theorem can have clauses that look like
wenzelm@60520
  2110
 *
wenzelm@60520
  2111
 *     ?v1..vn. z = C vn..v1
wenzelm@60520
  2112
 *
wenzelm@60520
  2113
 * in which the order of quantification is not the order of occurrence of the
wenzelm@60520
  2114
 * quantified variables as arguments to C. Since we have no control over this
wenzelm@60520
  2115
 * aspect of the nchotomy theorem, we make the correspondence explicit by
wenzelm@60520
  2116
 * pairing the incoming new variable with the term it gets beta-reduced into.
wenzelm@60520
  2117
 *---------------------------------------------------------------------------*)
wenzelm@60520
  2118
wenzelm@60520
  2119
fun alpha_ex_unroll (xlist, tm) =
wenzelm@60520
  2120
  let val (qvars,body) = USyntax.strip_exists tm
wenzelm@60520
  2121
      val vlist = #2 (USyntax.strip_comb (USyntax.rhs body))
wenzelm@60520
  2122
      val plist = ListPair.zip (vlist, xlist)
wenzelm@60520
  2123
      val args = map (the o AList.lookup (op aconv) plist) qvars
wenzelm@60520
  2124
                   handle Option.Option => raise Fail "TFL.alpha_ex_unroll: no correspondence"
wenzelm@60520
  2125
      fun build ex      []   = []
wenzelm@60520
  2126
        | build (_$rex) (v::rst) =
wenzelm@60520
  2127
           let val ex1 = Term.betapply(rex, v)
wenzelm@60520
  2128
           in  ex1 :: build ex1 rst
wenzelm@60520
  2129
           end
wenzelm@60520
  2130
     val (nex::exl) = rev (tm::build tm args)
wenzelm@60520
  2131
  in
wenzelm@60520
  2132
  (nex, ListPair.zip (args, rev exl))
wenzelm@60520
  2133
  end;
wenzelm@60520
  2134
wenzelm@60520
  2135
wenzelm@60520
  2136
wenzelm@60520
  2137
(*----------------------------------------------------------------------------
wenzelm@60520
  2138
 *
wenzelm@60520
  2139
 *             PROVING COMPLETENESS OF PATTERNS
wenzelm@60520
  2140
 *
wenzelm@60520
  2141
 *---------------------------------------------------------------------------*)
wenzelm@60520
  2142
wenzelm@60699
  2143
fun mk_case ctxt ty_info usednames =
wenzelm@60520
  2144
 let
wenzelm@60699
  2145
 val thy = Proof_Context.theory_of ctxt
wenzelm@60520
  2146
 val divide = ipartition (gvvariant usednames)
wenzelm@60520
  2147
 val tych = Thry.typecheck thy
wenzelm@60520
  2148
 fun tych_binding(x,y) = (tych x, tych y)
wenzelm@60520
  2149
 fun fail s = raise TFL_ERR "mk_case" s
wenzelm@60520
  2150
 fun mk{rows=[],...} = fail"no rows"
wenzelm@60520
  2151
   | mk{path=[], rows = [([], (thm, bindings))]} =
wenzelm@60520
  2152
                         Rules.IT_EXISTS ctxt (map tych_binding bindings) thm
wenzelm@60520
  2153
   | mk{path = u::rstp, rows as (p::_, _)::_} =
wenzelm@60520
  2154
     let val (pat_rectangle,rights) = ListPair.unzip rows
wenzelm@60520
  2155
         val col0 = map hd pat_rectangle
wenzelm@60520
  2156
         val pat_rectangle' = map tl pat_rectangle
wenzelm@60520
  2157
     in
wenzelm@60520
  2158
     if (forall is_Free col0) (* column 0 is all variables *)
wenzelm@60520
  2159
     then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[(u,v)]))
wenzelm@60520
  2160
                                (ListPair.zip (rights, col0))
wenzelm@60520
  2161
          in mk{path = rstp, rows = ListPair.zip (pat_rectangle', rights')}
wenzelm@60520
  2162
          end
wenzelm@60520
  2163
     else                     (* column 0 is all constructors *)
wenzelm@60520
  2164
     let val Type (ty_name,_) = type_of p
wenzelm@60520
  2165
     in
wenzelm@60520
  2166
     case (ty_info ty_name)
wenzelm@60520
  2167
     of NONE => fail("Not a known datatype: "^ty_name)
wenzelm@60520
  2168
      | SOME{constructors,nchotomy} =>
wenzelm@60520
  2169
        let val thm' = Rules.ISPEC (tych u) nchotomy
wenzelm@60520
  2170
            val disjuncts = USyntax.strip_disj (concl thm')
wenzelm@60520
  2171
            val subproblems = divide(constructors, rows)
wenzelm@60520
  2172
            val groups      = map #group subproblems
wenzelm@60520
  2173
            and new_formals = map #new_formals subproblems
wenzelm@60520
  2174
            val existentials = ListPair.map alpha_ex_unroll
wenzelm@60520
  2175
                                   (new_formals, disjuncts)
wenzelm@60520
  2176
            val constraints = map #1 existentials
wenzelm@60520
  2177
            val vexl = map #2 existentials
wenzelm@60520
  2178
            fun expnd tm (pats,(th,b)) = (pats, (Rules.SUBS ctxt [Rules.ASSUME (tych tm)] th, b))
wenzelm@60520
  2179
            val news = map (fn (nf,rows,c) => {path = nf@rstp,
wenzelm@60520
  2180
                                               rows = map (expnd c) rows})
wenzelm@60520
  2181
                           (Utils.zip3 new_formals groups constraints)
wenzelm@60520
  2182
            val recursive_thms = map mk news
wenzelm@60520
  2183
            val build_exists = Library.foldr
wenzelm@60520
  2184
                                (fn((x,t), th) =>
wenzelm@60520
  2185
                                 Rules.CHOOSE ctxt (tych x, Rules.ASSUME (tych t)) th)
wenzelm@60520
  2186
            val thms' = ListPair.map build_exists (vexl, recursive_thms)
wenzelm@60520
  2187
            val same_concls = Rules.EVEN_ORS thms'
wenzelm@60520
  2188
        in Rules.DISJ_CASESL thm' same_concls
wenzelm@60520
  2189
        end
wenzelm@60520
  2190
     end end
wenzelm@60520
  2191
 in mk
wenzelm@60520
  2192
 end;
wenzelm@60520
  2193
wenzelm@60520
  2194
wenzelm@60699
  2195
fun complete_cases ctxt =
wenzelm@60699
  2196
 let val thy = Proof_Context.theory_of ctxt
wenzelm@60520
  2197
     val tych = Thry.typecheck thy
wenzelm@60520
  2198
     val ty_info = Thry.induct_info thy
wenzelm@60520
  2199
 in fn pats =>
wenzelm@60520
  2200
 let val names = List.foldr Misc_Legacy.add_term_names [] pats
wenzelm@60520
  2201
     val T = type_of (hd pats)
wenzelm@60520
  2202
     val aname = singleton (Name.variant_list names) "a"
wenzelm@60520
  2203
     val vname = singleton (Name.variant_list (aname::names)) "v"
wenzelm@60520
  2204
     val a = Free (aname, T)
wenzelm@60520
  2205
     val v = Free (vname, T)
wenzelm@60520
  2206
     val a_eq_v = HOLogic.mk_eq(a,v)
wenzelm@60781
  2207
     val ex_th0 = Rules.EXISTS ctxt (tych (USyntax.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
wenzelm@60520
  2208
                           (Rules.REFL (tych a))
wenzelm@60520
  2209
     val th0 = Rules.ASSUME (tych a_eq_v)
wenzelm@60520
  2210
     val rows = map (fn x => ([x], (th0,[]))) pats
wenzelm@60520
  2211
 in
wenzelm@60520
  2212
 Rules.GEN ctxt (tych a)
wenzelm@60520
  2213
       (Rules.RIGHT_ASSOC ctxt
wenzelm@60520
  2214
          (Rules.CHOOSE ctxt (tych v, ex_th0)
wenzelm@60699
  2215
                (mk_case ctxt ty_info (vname::aname::names)
wenzelm@60699
  2216
                 {path=[v], rows=rows})))
wenzelm@60520
  2217
 end end;
wenzelm@60520
  2218
wenzelm@60520
  2219
wenzelm@60520
  2220
(*---------------------------------------------------------------------------
wenzelm@60520
  2221
 * Constructing induction hypotheses: one for each recursive call.
wenzelm@60520
  2222
 *
wenzelm@60520
  2223
 * Note. R will never occur as a variable in the ind_clause, because
wenzelm@60520
  2224
 * to do so, it would have to be from a nested definition, and we don't
wenzelm@60520
  2225
 * allow nested defns to have R variable.
wenzelm@60520
  2226
 *
wenzelm@60520
  2227
 * Note. When the context is empty, there can be no local variables.
wenzelm@60520
  2228
 *---------------------------------------------------------------------------*)
wenzelm@60520
  2229
wenzelm@60520
  2230
local infix 5 ==>
wenzelm@60520
  2231
      fun (tm1 ==> tm2) = USyntax.mk_imp{ant = tm1, conseq = tm2}
wenzelm@60520
  2232
in
wenzelm@60520
  2233
fun build_ih f (P,SV) (pat,TCs) =
wenzelm@60520
  2234
 let val pat_vars = USyntax.free_vars_lr pat
wenzelm@60520
  2235
     val globals = pat_vars@SV
wenzelm@60520
  2236
     fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm)
wenzelm@60520
  2237
     fun dest_TC tm =
wenzelm@60520
  2238
         let val (cntxt,R_y_pat) = USyntax.strip_imp(#2(USyntax.strip_forall tm))
wenzelm@60520
  2239
             val (R,y,_) = USyntax.dest_relation R_y_pat
wenzelm@60520
  2240
             val P_y = if (nested tm) then R_y_pat ==> P$y else P$y
wenzelm@60520
  2241
         in case cntxt
wenzelm@60520
  2242
              of [] => (P_y, (tm,[]))
wenzelm@60520
  2243
               | _  => let
wenzelm@60520
  2244
                    val imp = USyntax.list_mk_conj cntxt ==> P_y
wenzelm@60520
  2245
                    val lvs = subtract (op aconv) globals (USyntax.free_vars_lr imp)
wenzelm@60520
  2246
                    val locals = #2(Utils.pluck (curry (op aconv) P) lvs) handle Utils.ERR _ => lvs
wenzelm@60520
  2247
                    in (USyntax.list_mk_forall(locals,imp), (tm,locals)) end
wenzelm@60520
  2248
         end
wenzelm@60520
  2249
 in case TCs
wenzelm@60520
  2250
    of [] => (USyntax.list_mk_forall(pat_vars, P$pat), [])
wenzelm@60520
  2251
     |  _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)
wenzelm@60520
  2252
                 val ind_clause = USyntax.list_mk_conj ihs ==> P$pat
wenzelm@60520
  2253
             in (USyntax.list_mk_forall(pat_vars,ind_clause), TCs_locals)
wenzelm@60520
  2254
             end
wenzelm@60520
  2255
 end
wenzelm@60520
  2256
end;
wenzelm@60520
  2257
wenzelm@60520
  2258
(*---------------------------------------------------------------------------
wenzelm@60520
  2259
 * This function makes good on the promise made in "build_ih".
wenzelm@60520
  2260
 *
wenzelm@60520
  2261
 * Input  is tm = "(!y. R y pat ==> P y) ==> P pat",
wenzelm@60520
  2262
 *           TCs = TC_1[pat] ... TC_n[pat]
wenzelm@60520
  2263
 *           thm = ih1 /\ ... /\ ih_n |- ih[pat]
wenzelm@60520
  2264
 *---------------------------------------------------------------------------*)
wenzelm@60520
  2265
fun prove_case ctxt f (tm,TCs_locals,thm) =
wenzelm@60520
  2266
 let val tych = Thry.typecheck (Proof_Context.theory_of ctxt)
wenzelm@60520
  2267
     val antc = tych(#ant(USyntax.dest_imp tm))
wenzelm@60520
  2268
     val thm' = Rules.SPEC_ALL thm
wenzelm@60520
  2269
     fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm)
wenzelm@60520
  2270
     fun get_cntxt TC = tych(#ant(USyntax.dest_imp(#2(USyntax.strip_forall(concl TC)))))
wenzelm@60520
  2271
     fun mk_ih ((TC,locals),th2,nested) =
wenzelm@60520
  2272
         Rules.GENL ctxt (map tych locals)
wenzelm@60520
  2273
            (if nested then Rules.DISCH (get_cntxt TC) th2 handle Utils.ERR _ => th2
wenzelm@60520
  2274
             else if USyntax.is_imp (concl TC) then Rules.IMP_TRANS TC th2
wenzelm@60520
  2275
             else Rules.MP th2 TC)
wenzelm@60520
  2276
 in
wenzelm@60520
  2277
 Rules.DISCH antc
wenzelm@60520
  2278
 (if USyntax.is_imp(concl thm') (* recursive calls in this clause *)
wenzelm@60520
  2279
  then let val th1 = Rules.ASSUME antc
wenzelm@60520
  2280
           val TCs = map #1 TCs_locals
wenzelm@60520
  2281
           val ylist = map (#2 o USyntax.dest_relation o #2 o USyntax.strip_imp o
wenzelm@60520
  2282
                            #2 o USyntax.strip_forall) TCs
wenzelm@60520
  2283
           val TClist = map (fn(TC,lvs) => (Rules.SPEC_ALL(Rules.ASSUME(tych TC)),lvs))
wenzelm@60520
  2284
                            TCs_locals
wenzelm@60520
  2285
           val th2list = map (fn t => Rules.SPEC (tych t) th1) ylist
wenzelm@60520
  2286
           val nlist = map nested TCs
wenzelm@60520
  2287
           val triples = Utils.zip3 TClist th2list nlist
wenzelm@60520
  2288
           val Pylist = map mk_ih triples
wenzelm@60520
  2289
       in Rules.MP thm' (Rules.LIST_CONJ Pylist) end
wenzelm@60520
  2290
  else thm')
wenzelm@60520
  2291
 end;
wenzelm@60520
  2292
wenzelm@60520
  2293
wenzelm@60520
  2294
(*---------------------------------------------------------------------------
wenzelm@60520
  2295
 *
wenzelm@60520
  2296
 *         x = (v1,...,vn)  |- M[x]
wenzelm@60520
  2297
 *    ---------------------------------------------
wenzelm@60520
  2298
 *      ?v1 ... vn. x = (v1,...,vn) |- M[x]
wenzelm@60520
  2299
 *
wenzelm@60520
  2300
 *---------------------------------------------------------------------------*)
wenzelm@60520
  2301
fun LEFT_ABS_VSTRUCT ctxt tych thm =
wenzelm@60520
  2302
  let fun CHOOSER v (tm,thm) =
wenzelm@60520
  2303
        let val ex_tm = USyntax.mk_exists{Bvar=v,Body=tm}
wenzelm@60520
  2304
        in (ex_tm, Rules.CHOOSE ctxt (tych v, Rules.ASSUME (tych ex_tm)) thm)
wenzelm@60520
  2305
        end
wenzelm@60520
  2306
      val [veq] = filter (can USyntax.dest_eq) (#1 (Rules.dest_thm thm))
wenzelm@60520
  2307
      val {lhs,rhs} = USyntax.dest_eq veq
wenzelm@60520
  2308
      val L = USyntax.free_vars_lr rhs
wenzelm@60520
  2309
  in  #2 (fold_rev CHOOSER L (veq,thm))  end;
wenzelm@60520
  2310
wenzelm@60520
  2311
wenzelm@60520
  2312
(*----------------------------------------------------------------------------
wenzelm@60520
  2313
 * Input : f, R,  and  [(pat1,TCs1),..., (patn,TCsn)]
wenzelm@60520
  2314
 *
wenzelm@60522
  2315
 * Instantiates tfl_wf_induct, getting Sinduct and then tries to prove
wenzelm@60520
  2316
 * recursion induction (Rinduct) by proving the antecedent of Sinduct from
wenzelm@60520
  2317
 * the antecedent of Rinduct.
wenzelm@60520
  2318
 *---------------------------------------------------------------------------*)
wenzelm@60699
  2319
fun mk_induction ctxt {fconst, R, SV, pat_TCs_list} =
wenzelm@60699
  2320
let
wenzelm@60699
  2321
    val thy = Proof_Context.theory_of ctxt
wenzelm@60520
  2322
    val tych = Thry.typecheck thy
wenzelm@60522
  2323
    val Sinduction = Rules.UNDISCH (Rules.ISPEC (tych R) @{thm tfl_wf_induct})
wenzelm@60520
  2324
    val (pats,TCsl) = ListPair.unzip pat_TCs_list
wenzelm@60699
  2325
    val case_thm = complete_cases ctxt pats
wenzelm@60520
  2326
    val domain = (type_of o hd) pats
wenzelm@60520
  2327
    val Pname = singleton (Name.variant_list (List.foldr (Library.foldr Misc_Legacy.add_term_names)
wenzelm@60520
  2328
                              [] (pats::TCsl))) "P"
wenzelm@60520
  2329
    val P = Free(Pname, domain --> HOLogic.boolT)
wenzelm@60520
  2330
    val Sinduct = Rules.SPEC (tych P) Sinduction
wenzelm@60520
  2331
    val Sinduct_assumf = USyntax.rand ((#ant o USyntax.dest_imp o concl) Sinduct)
wenzelm@60520
  2332
    val Rassums_TCl' = map (build_ih fconst (P,SV)) pat_TCs_list
wenzelm@60520
  2333
    val (Rassums,TCl') = ListPair.unzip Rassums_TCl'
wenzelm@60520
  2334
    val Rinduct_assum = Rules.ASSUME (tych (USyntax.list_mk_conj Rassums))
wenzelm@60520
  2335
    val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
wenzelm@60520
  2336
    val tasks = Utils.zip3 cases TCl' (Rules.CONJUNCTS Rinduct_assum)
wenzelm@60520
  2337
    val proved_cases = map (prove_case ctxt fconst) tasks
wenzelm@60520
  2338
    val v =
wenzelm@60520
  2339
      Free (singleton
wenzelm@60520
  2340
        (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] (map concl proved_cases))) "v",
wenzelm@60520
  2341
          domain)
wenzelm@60520
  2342
    val vtyped = tych v
wenzelm@60520
  2343
    val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
wenzelm@60520
  2344
    val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS ctxt [th]th')
wenzelm@60520
  2345
                          (substs, proved_cases)
wenzelm@60520
  2346
    val abs_cases = map (LEFT_ABS_VSTRUCT ctxt tych) proved_cases1
wenzelm@60520
  2347
    val dant = Rules.GEN ctxt vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases)
wenzelm@60520
  2348
    val dc = Rules.MP Sinduct dant
wenzelm@60520
  2349
    val Parg_ty = type_of(#Bvar(USyntax.dest_forall(concl dc)))
wenzelm@60520
  2350
    val vars = map (gvvariant[Pname]) (USyntax.strip_prod_type Parg_ty)
wenzelm@60520
  2351
    val dc' = fold_rev (Rules.GEN ctxt o tych) vars
wenzelm@60520
  2352
                       (Rules.SPEC (tych(USyntax.mk_vstruct Parg_ty vars)) dc)
wenzelm@60520
  2353
in
wenzelm@60520
  2354
   Rules.GEN ctxt (tych P) (Rules.DISCH (tych(concl Rinduct_assum)) dc')
wenzelm@60520
  2355
end
wenzelm@60520
  2356
handle Utils.ERR _ => raise TFL_ERR "mk_induction" "failed derivation";
wenzelm@60520
  2357
wenzelm@60520
  2358
wenzelm@60520
  2359
wenzelm@60520
  2360
(*---------------------------------------------------------------------------
wenzelm@60520
  2361
 *
wenzelm@60520
  2362
 *                        POST PROCESSING
wenzelm@60520
  2363
 *
wenzelm@60520
  2364
 *---------------------------------------------------------------------------*)
wenzelm@60520
  2365
wenzelm@60520
  2366
wenzelm@60520
  2367
fun simplify_induction thy hth ind =
wenzelm@60520
  2368
  let val tych = Thry.typecheck thy
wenzelm@60520
  2369
      val (asl,_) = Rules.dest_thm ind
wenzelm@60520
  2370
      val (_,tc_eq_tc') = Rules.dest_thm hth
wenzelm@60520
  2371
      val tc = USyntax.lhs tc_eq_tc'
wenzelm@60520
  2372
      fun loop [] = ind
wenzelm@60520
  2373
        | loop (asm::rst) =
wenzelm@60520
  2374
          if (can (Thry.match_term thy asm) tc)
wenzelm@60520
  2375
          then Rules.UNDISCH
wenzelm@60520
  2376
                 (Rules.MATCH_MP
wenzelm@60522
  2377
                     (Rules.MATCH_MP @{thm tfl_simp_thm} (Rules.DISCH (tych asm) ind))
wenzelm@60520
  2378
                     hth)
wenzelm@60520
  2379
         else loop rst
wenzelm@60520
  2380
  in loop asl
wenzelm@60520
  2381
end;
wenzelm@60520
  2382
wenzelm@60520
  2383
wenzelm@60520
  2384
(*---------------------------------------------------------------------------
wenzelm@60520
  2385
 * The termination condition is an antecedent to the rule, and an
wenzelm@60520
  2386
 * assumption to the theorem.
wenzelm@60520
  2387
 *---------------------------------------------------------------------------*)
wenzelm@60520
  2388
fun elim_tc tcthm (rule,induction) =
wenzelm@60520
  2389
   (Rules.MP rule tcthm, Rules.PROVE_HYP tcthm induction)
wenzelm@60520
  2390
wenzelm@60520
  2391
wenzelm@60520
  2392
fun trace_thms ctxt s L =
wenzelm@61268
  2393
  if !trace then writeln (cat_lines (s :: map (Thm.string_of_thm ctxt) L))
wenzelm@60520
  2394
  else ();
wenzelm@60520
  2395
wenzelm@60520
  2396
fun trace_cterm ctxt s ct =
wenzelm@60520
  2397
  if !trace then
wenzelm@60520
  2398
    writeln (cat_lines [s, Syntax.string_of_term ctxt (Thm.term_of ct)])
wenzelm@60520
  2399
  else ();
wenzelm@60520
  2400
wenzelm@60520
  2401
wenzelm@60520
  2402
fun postprocess ctxt strict {wf_tac, terminator, simplifier} {rules,induction,TCs} =
wenzelm@60520
  2403
  let
wenzelm@60520
  2404
    val thy = Proof_Context.theory_of ctxt;
wenzelm@60520
  2405
    val tych = Thry.typecheck thy;
wenzelm@60520
  2406
wenzelm@60520
  2407
   (*---------------------------------------------------------------------
wenzelm@60520
  2408
    * Attempt to eliminate WF condition. It's the only assumption of rules
wenzelm@60520
  2409
    *---------------------------------------------------------------------*)
wenzelm@60520
  2410
    val (rules1,induction1)  =
wenzelm@60520
  2411
       let val thm =
wenzelm@60520
  2412
        Rules.prove ctxt strict (HOLogic.mk_Trueprop (hd(#1(Rules.dest_thm rules))), wf_tac)
wenzelm@60520
  2413
       in (Rules.PROVE_HYP thm rules, Rules.PROVE_HYP thm induction)
wenzelm@60520
  2414
       end handle Utils.ERR _ => (rules,induction);
wenzelm@60520
  2415
wenzelm@60520
  2416
   (*----------------------------------------------------------------------
wenzelm@60520
  2417
    * The termination condition (tc) is simplified to |- tc = tc' (there
wenzelm@60520
  2418
    * might not be a change!) and then 3 attempts are made:
wenzelm@60520
  2419
    *
wenzelm@60522
  2420
    *   1. if |- tc = T, then eliminate it with tfl_eq_True; otherwise,
wenzelm@60520
  2421
    *   2. apply the terminator to tc'. If |- tc' = T then eliminate; else
wenzelm@60520
  2422
    *   3. replace tc by tc' in both the rules and the induction theorem.
wenzelm@60520
  2423
    *---------------------------------------------------------------------*)
wenzelm@60520
  2424
wenzelm@60520
  2425
   fun simplify_tc tc (r,ind) =
wenzelm@60520
  2426
       let val tc1 = tych tc
wenzelm@60520
  2427
           val _ = trace_cterm ctxt "TC before simplification: " tc1
wenzelm@60520
  2428
           val tc_eq = simplifier tc1
wenzelm@60520
  2429
           val _ = trace_thms ctxt "result: " [tc_eq]
wenzelm@60520
  2430
       in
wenzelm@60522
  2431
       elim_tc (Rules.MATCH_MP @{thm tfl_eq_True} tc_eq) (r,ind)
wenzelm@60520
  2432
       handle Utils.ERR _ =>
wenzelm@60522
  2433
        (elim_tc (Rules.MATCH_MP(Rules.MATCH_MP @{thm tfl_rev_eq_mp} tc_eq)
wenzelm@60520
  2434
                  (Rules.prove ctxt strict (HOLogic.mk_Trueprop(USyntax.rhs(concl tc_eq)),
wenzelm@60520
  2435
                           terminator)))
wenzelm@60520
  2436
                 (r,ind)
wenzelm@60520
  2437
         handle Utils.ERR _ =>
wenzelm@60522
  2438
          (Rules.UNDISCH(Rules.MATCH_MP (Rules.MATCH_MP @{thm tfl_simp_thm} r) tc_eq),
wenzelm@60520
  2439
           simplify_induction thy tc_eq ind))
wenzelm@60520
  2440
       end
wenzelm@60520
  2441
wenzelm@60520
  2442
   (*----------------------------------------------------------------------
wenzelm@60520
  2443
    * Nested termination conditions are harder to get at, since they are
wenzelm@60520
  2444
    * left embedded in the body of the function (and in induction
wenzelm@60520
  2445
    * theorem hypotheses). Our "solution" is to simplify them, and try to
wenzelm@60520
  2446
    * prove termination, but leave the application of the resulting theorem
wenzelm@60520
  2447
    * to a higher level. So things go much as in "simplify_tc": the
wenzelm@60520
  2448
    * termination condition (tc) is simplified to |- tc = tc' (there might
wenzelm@60520
  2449
    * not be a change) and then 2 attempts are made:
wenzelm@60520
  2450
    *
wenzelm@60520
  2451
    *   1. if |- tc = T, then return |- tc; otherwise,
wenzelm@60520
  2452
    *   2. apply the terminator to tc'. If |- tc' = T then return |- tc; else
wenzelm@60520
  2453
    *   3. return |- tc = tc'
wenzelm@60520
  2454
    *---------------------------------------------------------------------*)
wenzelm@60520
  2455
   fun simplify_nested_tc tc =
wenzelm@60520
  2456
      let val tc_eq = simplifier (tych (#2 (USyntax.strip_forall tc)))
wenzelm@60520
  2457
      in
wenzelm@60520
  2458
      Rules.GEN_ALL ctxt
wenzelm@60522
  2459
       (Rules.MATCH_MP @{thm tfl_eq_True} tc_eq
wenzelm@60520
  2460
        handle Utils.ERR _ =>
wenzelm@60522
  2461
          (Rules.MATCH_MP(Rules.MATCH_MP @{thm tfl_rev_eq_mp} tc_eq)
wenzelm@60520
  2462
                      (Rules.prove ctxt strict (HOLogic.mk_Trueprop (USyntax.rhs(concl tc_eq)),
wenzelm@60520
  2463
                               terminator))
wenzelm@60520
  2464
            handle Utils.ERR _ => tc_eq))
wenzelm@60520
  2465
      end
wenzelm@60520
  2466
wenzelm@60520
  2467
   (*-------------------------------------------------------------------
wenzelm@60520
  2468
    * Attempt to simplify the termination conditions in each rule and
wenzelm@60520
  2469
    * in the induction theorem.
wenzelm@60520
  2470
    *-------------------------------------------------------------------*)
wenzelm@60520
  2471
   fun strip_imp tm = if USyntax.is_neg tm then ([],tm) else USyntax.strip_imp tm
wenzelm@60520
  2472
   fun loop ([],extras,R,ind) = (rev R, ind, extras)
wenzelm@60520
  2473
     | loop ((r,ftcs)::rst, nthms, R, ind) =
wenzelm@60520
  2474
        let val tcs = #1(strip_imp (concl r))
wenzelm@60520
  2475
            val extra_tcs = subtract (op aconv) tcs ftcs
wenzelm@60520
  2476
            val extra_tc_thms = map simplify_nested_tc extra_tcs
wenzelm@60520
  2477
            val (r1,ind1) = fold simplify_tc tcs (r,ind)
wenzelm@60520
  2478
            val r2 = Rules.FILTER_DISCH_ALL(not o USyntax.is_WFR) r1
wenzelm@60520
  2479
        in loop(rst, nthms@extra_tc_thms, r2::R, ind1)
wenzelm@60520
  2480
        end
wenzelm@60520
  2481
   val rules_tcs = ListPair.zip (Rules.CONJUNCTS rules1, TCs)
wenzelm@60520
  2482
   val (rules2,ind2,extras) = loop(rules_tcs,[],[],induction1)
wenzelm@60520
  2483
in
wenzelm@60520
  2484
  {induction = ind2, rules = Rules.LIST_CONJ rules2, nested_tcs = extras}
wenzelm@60520
  2485
end;
wenzelm@60520
  2486
wenzelm@60520
  2487
end;
wenzelm@60520
  2488
wenzelm@60520
  2489
wenzelm@60521
  2490
wenzelm@60520
  2491
(*** second part of main module (postprocessing of TFL definitions) ***)
wenzelm@60520
  2492
wenzelm@60520
  2493
structure Tfl: TFL =
wenzelm@60520
  2494
struct
wenzelm@60520
  2495
wenzelm@60520
  2496
(* misc *)
wenzelm@60520
  2497
wenzelm@60520
  2498
(*---------------------------------------------------------------------------
wenzelm@60520
  2499
 * Extract termination goals so that they can be put it into a goalstack, or
wenzelm@60520
  2500
 * have a tactic directly applied to them.
wenzelm@60520
  2501
 *--------------------------------------------------------------------------*)
wenzelm@60520
  2502
fun termination_goals rules =
wenzelm@60520
  2503
    map (Type.legacy_freeze o HOLogic.dest_Trueprop)
wenzelm@60520
  2504
      (fold_rev (union (op aconv) o Thm.prems_of) rules []);
wenzelm@60520
  2505
wenzelm@60520
  2506
(*---------------------------------------------------------------------------
wenzelm@60520
  2507
 * Three postprocessors are applied to the definition.  It
wenzelm@60520
  2508
 * attempts to prove wellfoundedness of the given relation, simplifies the
wenzelm@60520
  2509
 * non-proved termination conditions, and finally attempts to prove the
wenzelm@60520
  2510
 * simplified termination conditions.
wenzelm@60520
  2511
 *--------------------------------------------------------------------------*)
wenzelm@60520
  2512
fun std_postprocessor ctxt strict wfs =
wenzelm@60520
  2513
  Prim.postprocess ctxt strict
wenzelm@60774
  2514
   {wf_tac = REPEAT (ares_tac ctxt wfs 1),
wenzelm@60520
  2515
    terminator =
wenzelm@60520
  2516
      asm_simp_tac ctxt 1
wenzelm@60520
  2517
      THEN TRY (Arith_Data.arith_tac ctxt 1 ORELSE
wenzelm@60520
  2518
        fast_force_tac (ctxt addSDs @{thms not0_implies_Suc}) 1),
wenzelm@60520
  2519
    simplifier = Rules.simpl_conv ctxt []};
wenzelm@60520
  2520
wenzelm@60520
  2521
wenzelm@60520
  2522
wenzelm@60520
  2523
val concl = #2 o Rules.dest_thm;
wenzelm@60520
  2524
wenzelm@60520
  2525
(*---------------------------------------------------------------------------
wenzelm@60520
  2526
 * Postprocess a definition made by "define". This is a separate stage of
wenzelm@60520
  2527
 * processing from the definition stage.
wenzelm@60520
  2528
 *---------------------------------------------------------------------------*)
wenzelm@60520
  2529
local
wenzelm@60520
  2530
wenzelm@60520
  2531
(* The rest of these local definitions are for the tricky nested case *)
wenzelm@60520
  2532
val solved = not o can USyntax.dest_eq o #2 o USyntax.strip_forall o concl
wenzelm@60520
  2533
wenzelm@60520
  2534
fun id_thm th =
wenzelm@60520
  2535
   let val {lhs,rhs} = USyntax.dest_eq (#2 (USyntax.strip_forall (#2 (Rules.dest_thm th))));
wenzelm@60520
  2536
   in lhs aconv rhs end
wenzelm@60520
  2537
   handle Utils.ERR _ => false;
wenzelm@60520
  2538
wenzelm@60520
  2539
val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection;
wenzelm@60520
  2540
fun mk_meta_eq r =
wenzelm@60520
  2541
  (case Thm.concl_of r of
wenzelm@60520
  2542
     Const(@{const_name Pure.eq},_)$_$_ => r
wenzelm@60520
  2543
  |   _ $(Const(@{const_name HOL.eq},_)$_$_) => r RS eq_reflection
wenzelm@60520
  2544
  |   _ => r RS P_imp_P_eq_True)
wenzelm@60520
  2545
wenzelm@60520
  2546
(*Is this the best way to invoke the simplifier??*)
wenzelm@60520
  2547
fun rewrite ctxt L = rewrite_rule ctxt (map mk_meta_eq (filter_out id_thm L))
wenzelm@60520
  2548
wenzelm@60520
  2549
fun join_assums ctxt th =
wenzelm@60520
  2550
  let val tych = Thm.cterm_of ctxt
wenzelm@60520
  2551
      val {lhs,rhs} = USyntax.dest_eq(#2 (USyntax.strip_forall (concl th)))
wenzelm@60520
  2552
      val cntxtl = (#1 o USyntax.strip_imp) lhs  (* cntxtl should = cntxtr *)
wenzelm@60520
  2553
      val cntxtr = (#1 o USyntax.strip_imp) rhs  (* but union is solider *)
wenzelm@60520
  2554
      val cntxt = union (op aconv) cntxtl cntxtr
wenzelm@60520
  2555
  in
wenzelm@60520
  2556
    Rules.GEN_ALL ctxt
wenzelm@60520
  2557
      (Rules.DISCH_ALL
wenzelm@60520
  2558
         (rewrite ctxt (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th)))
wenzelm@60520
  2559
  end
wenzelm@60520
  2560
  val gen_all = USyntax.gen_all
wenzelm@60520
  2561
in
wenzelm@60520
  2562
fun proof_stage ctxt strict wfs {f, R, rules, full_pats_TCs, TCs} =
wenzelm@60520
  2563
  let
wenzelm@60520
  2564
    val _ = writeln "Proving induction theorem ..."
wenzelm@60520
  2565
    val ind =
wenzelm@60699
  2566
      Prim.mk_induction ctxt
wenzelm@60520
  2567
        {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs}
wenzelm@60520
  2568
    val _ = writeln "Postprocessing ...";
wenzelm@60520
  2569
    val {rules, induction, nested_tcs} =
wenzelm@60520
  2570
      std_postprocessor ctxt strict wfs {rules=rules, induction=ind, TCs=TCs}
wenzelm@60520
  2571
  in
wenzelm@60520
  2572
  case nested_tcs
wenzelm@60520
  2573
  of [] => {induction=induction, rules=rules,tcs=[]}
wenzelm@60521
  2574
  | L  => let val _ = writeln "Simplifying nested TCs ..."
wenzelm@60520
  2575
              val (solved,simplified,stubborn) =
wenzelm@60520
  2576
               fold_rev (fn th => fn (So,Si,St) =>
wenzelm@60520
  2577
                     if (id_thm th) then (So, Si, th::St) else
wenzelm@60520
  2578
                     if (solved th) then (th::So, Si, St)
wenzelm@60520
  2579
                     else (So, th::Si, St)) nested_tcs ([],[],[])
wenzelm@60520
  2580
              val simplified' = map (join_assums ctxt) simplified
wenzelm@60520
  2581
              val dummy = (Prim.trace_thms ctxt "solved =" solved;
wenzelm@60520
  2582
                           Prim.trace_thms ctxt "simplified' =" simplified')
wenzelm@60520
  2583
              val rewr = full_simplify (ctxt addsimps (solved @ simplified'));
wenzelm@60520
  2584
              val dummy = Prim.trace_thms ctxt "Simplifying the induction rule..." [induction]
wenzelm@60520
  2585
              val induction' = rewr induction
wenzelm@60520
  2586
              val dummy = Prim.trace_thms ctxt "Simplifying the recursion rules..." [rules]
wenzelm@60520
  2587
              val rules'     = rewr rules
wenzelm@60520
  2588
              val _ = writeln "... Postprocessing finished";
wenzelm@60520
  2589
          in
wenzelm@60520
  2590
          {induction = induction',
wenzelm@60520
  2591
               rules = rules',
wenzelm@60520
  2592
                 tcs = map (gen_all o USyntax.rhs o #2 o USyntax.strip_forall o concl)
wenzelm@60520
  2593
                           (simplified@stubborn)}
wenzelm@60520
  2594
          end
wenzelm@60520
  2595
  end;
wenzelm@60520
  2596
wenzelm@60520
  2597
wenzelm@60520
  2598
(*lcp: curry the predicate of the induction rule*)
wenzelm@60520
  2599
fun curry_rule ctxt rl =
wenzelm@60520
  2600
  Split_Rule.split_rule_var ctxt (Term.head_of (HOLogic.dest_Trueprop (Thm.concl_of rl))) rl;
wenzelm@60520
  2601
wenzelm@60520
  2602
(*lcp: put a theorem into Isabelle form, using meta-level connectives*)
wenzelm@60520
  2603
fun meta_outer ctxt =
wenzelm@60520
  2604
  curry_rule ctxt o Drule.export_without_context o
wenzelm@60752
  2605
  rule_by_tactic ctxt
wenzelm@60752
  2606
    (REPEAT (FIRSTGOAL (resolve_tac ctxt [allI, impI, conjI] ORELSE' eresolve_tac ctxt [conjE])));
wenzelm@60520
  2607
wenzelm@60520
  2608
(*Strip off the outer !P*)
wenzelm@60520
  2609
val spec'=
wenzelm@60520
  2610
  Rule_Insts.read_instantiate @{context} [((("x", 0), Position.none), "P::'b=>bool")] [] spec;
wenzelm@60520
  2611
wenzelm@60524
  2612
fun simplify_defn ctxt strict congs wfs pats def0 =
wenzelm@60520
  2613
  let
wenzelm@60825
  2614
    val thy = Proof_Context.theory_of ctxt;
wenzelm@67710
  2615
    val def = HOLogic.mk_obj_eq (Thm.unvarify_global thy def0)
wenzelm@60520
  2616
    val {rules, rows, TCs, full_pats_TCs} = Prim.post_definition ctxt congs (def, pats)
wenzelm@60520
  2617
    val {lhs=f,rhs} = USyntax.dest_eq (concl def)
wenzelm@60520
  2618
    val (_,[R,_]) = USyntax.strip_comb rhs
wenzelm@60521
  2619
    val _ = Prim.trace_thms ctxt "congs =" congs
wenzelm@60520
  2620
    (*the next step has caused simplifier looping in some cases*)
wenzelm@60520
  2621
    val {induction, rules, tcs} =
wenzelm@60520
  2622
      proof_stage ctxt strict wfs
wenzelm@60520
  2623
       {f = f, R = R, rules = rules,
wenzelm@60520
  2624
        full_pats_TCs = full_pats_TCs,
wenzelm@60520
  2625
        TCs = TCs}
wenzelm@60520
  2626
    val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
wenzelm@60520
  2627
                      (Rules.CONJUNCTS rules)
wenzelm@60520
  2628
  in
wenzelm@60520
  2629
    {induct = meta_outer ctxt (Object_Logic.rulify_no_asm ctxt (induction RS spec')),
wenzelm@60520
  2630
     rules = ListPair.zip(rules', rows),
wenzelm@60520
  2631
     tcs = (termination_goals rules') @ tcs}
wenzelm@60520
  2632
  end
wenzelm@60520
  2633
  handle Utils.ERR {mesg,func,module} =>
wenzelm@60520
  2634
    error (mesg ^ "\n    (In TFL function " ^ module ^ "." ^ func ^ ")");
wenzelm@60520
  2635
wenzelm@60520
  2636
wenzelm@60520
  2637
(* Derive the initial equations from the case-split rules to meet the
wenzelm@60520
  2638
users specification of the recursive function. *)
wenzelm@60520
  2639
local
wenzelm@60520
  2640
  fun get_related_thms i =
wenzelm@60520
  2641
      map_filter ((fn (r,x) => if x = i then SOME r else NONE));
wenzelm@60520
  2642
wenzelm@60521
  2643
  fun solve_eq _ (_, [], _) =  error "derive_init_eqs: missing rules"
wenzelm@60521
  2644
    | solve_eq _ (_, [a], i) = [(a, i)]
wenzelm@60520
  2645
    | solve_eq ctxt (th, splitths, i) =
wenzelm@60520
  2646
      (writeln "Proving unsplit equation...";
wenzelm@60520
  2647
      [((Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
wenzelm@60520
  2648
          (CaseSplit.splitto ctxt splitths th), i)])
wenzelm@60520
  2649
      handle ERROR s =>
wenzelm@60520
  2650
             (warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);
wenzelm@60520
  2651
in
wenzelm@60520
  2652
fun derive_init_eqs ctxt rules eqs =
wenzelm@60520
  2653
  map (Thm.trivial o Thm.cterm_of ctxt o HOLogic.mk_Trueprop) eqs
wenzelm@60520
  2654
  |> map_index (fn (i, e) => solve_eq ctxt (e, (get_related_thms i rules), i))
wenzelm@60520
  2655
  |> flat;
wenzelm@60520
  2656
end;
wenzelm@60520
  2657
wenzelm@60520
  2658
wenzelm@60520
  2659
(*---------------------------------------------------------------------------
wenzelm@60520
  2660
 * Defining a function with an associated termination relation.
wenzelm@60520
  2661
 *---------------------------------------------------------------------------*)
wenzelm@60520
  2662
fun define_i strict congs wfs fid R eqs ctxt =
wenzelm@60520
  2663
  let
wenzelm@60520
  2664
    val thy = Proof_Context.theory_of ctxt
wenzelm@60520
  2665
    val {functional, pats} = Prim.mk_functional thy eqs
wenzelm@60520
  2666
    val (def, thy') = Prim.wfrec_definition0 fid R functional thy
wenzelm@60520
  2667
    val ctxt' = Proof_Context.transfer thy' ctxt
wenzelm@60520
  2668
    val (lhs, _) = Logic.dest_equals (Thm.prop_of def)
wenzelm@60524
  2669
    val {induct, rules, tcs} = simplify_defn ctxt' strict congs wfs pats def
wenzelm@60520
  2670
    val rules' = if strict then derive_init_eqs ctxt' rules eqs else rules
wenzelm@60520
  2671
  in ({lhs = lhs, rules = rules', induct = induct, tcs = tcs}, ctxt') end;
wenzelm@60520
  2672
wenzelm@60520
  2673
fun define strict congs wfs fid R seqs ctxt =
wenzelm@60520
  2674
  define_i strict congs wfs fid
wenzelm@60520
  2675
    (Syntax.read_term ctxt R) (map (Syntax.read_term ctxt) seqs) ctxt
wenzelm@60520
  2676
      handle Utils.ERR {mesg,...} => error mesg;
wenzelm@60520
  2677
wenzelm@60520
  2678
end;
wenzelm@60520
  2679
wenzelm@60520
  2680
end;
wenzelm@60520
  2681
wenzelm@60520
  2682
wenzelm@60521
  2683
wenzelm@60520
  2684
(*** wrappers for Isar ***)
wenzelm@60520
  2685
wenzelm@60520
  2686
(** recdef hints **)
wenzelm@60520
  2687
wenzelm@60520
  2688
(* type hints *)
wenzelm@60520
  2689
wenzelm@60520
  2690
type hints = {simps: thm list, congs: (string * thm) list, wfs: thm list};
wenzelm@60520
  2691
wenzelm@60520
  2692
fun mk_hints (simps, congs, wfs) = {simps = simps, congs = congs, wfs = wfs}: hints;
wenzelm@60520
  2693
fun map_hints f ({simps, congs, wfs}: hints) = mk_hints (f (simps, congs, wfs));
wenzelm@60520
  2694
wenzelm@60520
  2695
fun map_simps f = map_hints (fn (simps, congs, wfs) => (f simps, congs, wfs));
wenzelm@60520
  2696
fun map_congs f = map_hints (fn (simps, congs, wfs) => (simps, f congs, wfs));
wenzelm@60520
  2697
fun map_wfs f = map_hints (fn (simps, congs, wfs) => (simps, congs, f wfs));
wenzelm@60520
  2698
wenzelm@60520
  2699
wenzelm@60520
  2700
(* congruence rules *)
wenzelm@60520
  2701
wenzelm@60520
  2702
local
wenzelm@60520
  2703
wenzelm@60520
  2704
val cong_head =
wenzelm@60520
  2705
  fst o Term.dest_Const o Term.head_of o fst o Logic.dest_equals o Thm.concl_of;
wenzelm@60520
  2706
wenzelm@60520
  2707
fun prep_cong raw_thm =
wenzelm@60520
  2708
  let val thm = safe_mk_meta_eq raw_thm in (cong_head thm, thm) end;
wenzelm@60520
  2709
wenzelm@60520
  2710
in
wenzelm@60520
  2711
wenzelm@60520
  2712
fun add_cong raw_thm congs =
wenzelm@60520
  2713
  let
wenzelm@60520
  2714
    val (c, thm) = prep_cong raw_thm;
wenzelm@60520
  2715
    val _ = if AList.defined (op =) congs c
wenzelm@60520
  2716
      then warning ("Overwriting recdef congruence rule for " ^ quote c)
wenzelm@60520
  2717
      else ();
wenzelm@60520
  2718
  in AList.update (op =) (c, thm) congs end;
wenzelm@60520
  2719
wenzelm@60520
  2720
fun del_cong raw_thm congs =
wenzelm@60520
  2721
  let
wenzelm@60524
  2722
    val (c, _) = prep_cong raw_thm;
wenzelm@60520
  2723
    val _ = if AList.defined (op =) congs c
wenzelm@60520
  2724
      then ()
wenzelm@60520
  2725
      else warning ("No recdef congruence rule for " ^ quote c);
wenzelm@60520
  2726
  in AList.delete (op =) c congs end;
wenzelm@60520