src/Tools/IsaPlanner/isand.ML
author wenzelm
Thu May 31 20:55:29 2007 +0200 (2007-05-31)
changeset 23171 861f63a35d31
child 23175 267ba70e7a9d
permissions -rw-r--r--
moved IsaPlanner from Provers to Tools;
wenzelm@23171
     1
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
wenzelm@23171
     2
(*  Title:      Pure/IsaPlanner/isand.ML
wenzelm@23171
     3
    ID:		$Id$
wenzelm@23171
     4
    Author:     Lucas Dixon, University of Edinburgh
wenzelm@23171
     5
                lucas.dixon@ed.ac.uk
wenzelm@23171
     6
    Updated:    26 Apr 2005
wenzelm@23171
     7
    Date:       6 Aug 2004
wenzelm@23171
     8
*)
wenzelm@23171
     9
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
wenzelm@23171
    10
(*  DESCRIPTION:
wenzelm@23171
    11
wenzelm@23171
    12
    Natural Deduction tools
wenzelm@23171
    13
wenzelm@23171
    14
    For working with Isabelle theorems in a natural detuction style.
wenzelm@23171
    15
    ie, not having to deal with meta level quantified varaibles,
wenzelm@23171
    16
    instead, we work with newly introduced frees, and hide the
wenzelm@23171
    17
    "all"'s, exporting results from theorems proved with the frees, to
wenzelm@23171
    18
    solve the all cases of the previous goal. This allows resolution
wenzelm@23171
    19
    to do proof search normally. 
wenzelm@23171
    20
wenzelm@23171
    21
    Note: A nice idea: allow exporting to solve any subgoal, thus
wenzelm@23171
    22
    allowing the interleaving of proof, or provide a structure for the
wenzelm@23171
    23
    ordering of proof, thus allowing proof attempts in parrell, but
wenzelm@23171
    24
    recording the order to apply things in.
wenzelm@23171
    25
wenzelm@23171
    26
    THINK: are we really ok with our varify name w.r.t the prop - do
wenzelm@23171
    27
    we also need to avoid names in the hidden hyps? What about
wenzelm@23171
    28
    unification contraints in flex-flex pairs - might they also have
wenzelm@23171
    29
    extra free vars?
wenzelm@23171
    30
*)
wenzelm@23171
    31
wenzelm@23171
    32
signature ISA_ND =
wenzelm@23171
    33
sig
wenzelm@23171
    34
wenzelm@23171
    35
  (* export data *)
wenzelm@23171
    36
  datatype export = export of
wenzelm@23171
    37
           {gth: Thm.thm, (* initial goal theorem *)
wenzelm@23171
    38
            sgid: int, (* subgoal id which has been fixed etc *)
wenzelm@23171
    39
            fixes: Thm.cterm list, (* frees *)
wenzelm@23171
    40
            assumes: Thm.cterm list} (* assumptions *)
wenzelm@23171
    41
  val fixes_of_exp : export -> Thm.cterm list
wenzelm@23171
    42
  val export_back : export -> Thm.thm -> Thm.thm Seq.seq
wenzelm@23171
    43
  val export_solution : export -> Thm.thm -> Thm.thm
wenzelm@23171
    44
  val export_solutions : export list * Thm.thm -> Thm.thm
wenzelm@23171
    45
wenzelm@23171
    46
  (* inserting meta level params for frees in the conditions *)
wenzelm@23171
    47
  val allify_conditions :
wenzelm@23171
    48
      (Term.term -> Thm.cterm) ->
wenzelm@23171
    49
      (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list
wenzelm@23171
    50
  val allify_conditions' :
wenzelm@23171
    51
      (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list
wenzelm@23171
    52
  val assume_allified :
wenzelm@23171
    53
      theory -> (string * Term.sort) list * (string * Term.typ) list
wenzelm@23171
    54
      -> Term.term -> (Thm.cterm * Thm.thm)
wenzelm@23171
    55
wenzelm@23171
    56
  (* meta level fixed params (i.e. !! vars) *)
wenzelm@23171
    57
  val fix_alls_in_term : Term.term -> Term.term * Term.term list
wenzelm@23171
    58
  val fix_alls_term : int -> Term.term -> Term.term * Term.term list
wenzelm@23171
    59
  val fix_alls_cterm : int -> Thm.thm -> Thm.cterm * Thm.cterm list
wenzelm@23171
    60
  val fix_alls' : int -> Thm.thm -> Thm.thm * Thm.cterm list
wenzelm@23171
    61
  val fix_alls : int -> Thm.thm -> Thm.thm * export
wenzelm@23171
    62
wenzelm@23171
    63
  (* meta variables in types and terms *)
wenzelm@23171
    64
  val fix_tvars_to_tfrees_in_terms 
wenzelm@23171
    65
      : string list (* avoid these names *)
wenzelm@23171
    66
        -> Term.term list -> 
wenzelm@23171
    67
        (((string * int) * Term.sort) * (string * Term.sort)) list (* renamings *)
wenzelm@23171
    68
  val fix_vars_to_frees_in_terms
wenzelm@23171
    69
      : string list (* avoid these names *)
wenzelm@23171
    70
        -> Term.term list ->
wenzelm@23171
    71
        (((string * int) * Term.typ) * (string * Term.typ)) list (* renamings *)
wenzelm@23171
    72
  val fix_tvars_to_tfrees : Thm.thm -> Thm.ctyp list * Thm.thm
wenzelm@23171
    73
  val fix_vars_to_frees : Thm.thm -> Thm.cterm list * Thm.thm
wenzelm@23171
    74
  val fix_vars_and_tvars : 
wenzelm@23171
    75
      Thm.thm -> (Thm.cterm list * Thm.ctyp list) * Thm.thm
wenzelm@23171
    76
  val fix_vars_upto_idx : int -> Thm.thm -> Thm.thm
wenzelm@23171
    77
  val fix_tvars_upto_idx : int -> Thm.thm -> Thm.thm
wenzelm@23171
    78
  val unfix_frees : Thm.cterm list -> Thm.thm -> Thm.thm
wenzelm@23171
    79
  val unfix_tfrees : Thm.ctyp list -> Thm.thm -> Thm.thm
wenzelm@23171
    80
  val unfix_frees_and_tfrees :
wenzelm@23171
    81
      (Thm.cterm list * Thm.ctyp list) -> Thm.thm -> Thm.thm
wenzelm@23171
    82
wenzelm@23171
    83
  (* assumptions/subgoals *)
wenzelm@23171
    84
  val assume_prems :
wenzelm@23171
    85
      int -> Thm.thm -> Thm.thm list * Thm.thm * Thm.cterm list
wenzelm@23171
    86
  val fixed_subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm)
wenzelm@23171
    87
  val fixes_and_assumes : int -> Thm.thm -> Thm.thm list * Thm.thm * export
wenzelm@23171
    88
  val hide_other_goals : Thm.thm -> Thm.thm * Thm.cterm list
wenzelm@23171
    89
  val hide_prems : Thm.thm -> Thm.thm * Thm.cterm list
wenzelm@23171
    90
wenzelm@23171
    91
  (* abstracts cterms (vars) to locally meta-all bounds *)
wenzelm@23171
    92
  val prepare_goal_export : string list * Thm.cterm list -> Thm.thm 
wenzelm@23171
    93
                            -> int * Thm.thm
wenzelm@23171
    94
  val solve_with : Thm.thm -> Thm.thm -> Thm.thm Seq.seq
wenzelm@23171
    95
  val subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm)
wenzelm@23171
    96
end
wenzelm@23171
    97
wenzelm@23171
    98
wenzelm@23171
    99
structure IsaND 
wenzelm@23171
   100
: ISA_ND
wenzelm@23171
   101
= struct
wenzelm@23171
   102
wenzelm@23171
   103
(* Solve *some* subgoal of "th" directly by "sol" *)
wenzelm@23171
   104
(* Note: this is probably what Markus ment to do upon export of a
wenzelm@23171
   105
"show" but maybe he used RS/rtac instead, which would wrongly lead to
wenzelm@23171
   106
failing if there are premices to the shown goal. 
wenzelm@23171
   107
wenzelm@23171
   108
given: 
wenzelm@23171
   109
sol : Thm.thm = [| Ai... |] ==> Ci
wenzelm@23171
   110
th : Thm.thm = 
wenzelm@23171
   111
  [| ... [| Ai... |] ==> Ci ... |] ==> G
wenzelm@23171
   112
results in: 
wenzelm@23171
   113
  [| ... [| Ai-1... |] ==> Ci-1
wenzelm@23171
   114
    [| Ai+1... |] ==> Ci+1 ...
wenzelm@23171
   115
  |] ==> G
wenzelm@23171
   116
i.e. solves some subgoal of th that is identical to sol. 
wenzelm@23171
   117
*)
wenzelm@23171
   118
fun solve_with sol th = 
wenzelm@23171
   119
    let fun solvei 0 = Seq.empty
wenzelm@23171
   120
          | solvei i = 
wenzelm@23171
   121
            Seq.append (bicompose false (false,sol,0) i th) (solvei (i - 1))
wenzelm@23171
   122
    in
wenzelm@23171
   123
      solvei (Thm.nprems_of th)
wenzelm@23171
   124
    end;
wenzelm@23171
   125
wenzelm@23171
   126
wenzelm@23171
   127
(* Given ctertmify function, (string,type) pairs capturing the free
wenzelm@23171
   128
vars that need to be allified in the assumption, and a theorem with
wenzelm@23171
   129
assumptions possibly containing the free vars, then we give back the
wenzelm@23171
   130
assumptions allified as hidden hyps. 
wenzelm@23171
   131
wenzelm@23171
   132
Given: x 
wenzelm@23171
   133
th: A vs ==> B vs 
wenzelm@23171
   134
Results in: "B vs" [!!x. A x]
wenzelm@23171
   135
*)
wenzelm@23171
   136
fun allify_conditions ctermify Ts th = 
wenzelm@23171
   137
    let 
wenzelm@23171
   138
      val premts = Thm.prems_of th;
wenzelm@23171
   139
    
wenzelm@23171
   140
      fun allify_prem_var (vt as (n,ty),t)  = 
wenzelm@23171
   141
          (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
wenzelm@23171
   142
wenzelm@23171
   143
      fun allify_prem Ts p = foldr allify_prem_var p Ts
wenzelm@23171
   144
wenzelm@23171
   145
      val cTs = map (ctermify o Free) Ts
wenzelm@23171
   146
      val cterm_asms = map (ctermify o allify_prem Ts) premts
wenzelm@23171
   147
      val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms
wenzelm@23171
   148
    in 
wenzelm@23171
   149
      (Library.foldl (fn (x,y) => y COMP x) (th, allifyied_asm_thms), cterm_asms)
wenzelm@23171
   150
    end;
wenzelm@23171
   151
wenzelm@23171
   152
fun allify_conditions' Ts th = 
wenzelm@23171
   153
    allify_conditions (Thm.cterm_of (Thm.theory_of_thm th)) Ts th;
wenzelm@23171
   154
wenzelm@23171
   155
(* allify types *)
wenzelm@23171
   156
fun allify_typ ts ty = 
wenzelm@23171
   157
    let 
wenzelm@23171
   158
      fun trec (x as (TFree (s,srt))) = 
wenzelm@23171
   159
          (case Library.find_first (fn (s2,srt2) => s = s2) ts
wenzelm@23171
   160
            of NONE => x
wenzelm@23171
   161
             | SOME (s2,_) => TVar ((s,0),srt))
wenzelm@23171
   162
            (*  Maybe add in check here for bad sorts? 
wenzelm@23171
   163
             if srt = srt2 then TVar ((s,0),srt) 
wenzelm@23171
   164
               else raise  ("thaw_typ", ts, ty) *)
wenzelm@23171
   165
          | trec (Type (s,typs)) = Type (s, map trec typs)
wenzelm@23171
   166
          | trec (v as TVar _) = v;
wenzelm@23171
   167
    in trec ty end;
wenzelm@23171
   168
wenzelm@23171
   169
(* implicit types and term *)
wenzelm@23171
   170
fun allify_term_typs ty = Term.map_types (allify_typ ty);
wenzelm@23171
   171
wenzelm@23171
   172
(* allified version of term, given frees to allify over. Note that we
wenzelm@23171
   173
only allify over the types on the given allified cterm, we can't do
wenzelm@23171
   174
this for the theorem as we are not allowed type-vars in the hyp. *)
wenzelm@23171
   175
(* FIXME: make the allified term keep the same conclusion as it
wenzelm@23171
   176
started with, rather than a strictly more general version (ie use
wenzelm@23171
   177
instantiate with initial params we abstracted from, rather than
wenzelm@23171
   178
forall_elim_vars. *)
wenzelm@23171
   179
fun assume_allified sgn (tyvs,vs) t = 
wenzelm@23171
   180
    let
wenzelm@23171
   181
      fun allify_var (vt as (n,ty),t)  = 
wenzelm@23171
   182
          (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
wenzelm@23171
   183
      fun allify Ts p = List.foldr allify_var p Ts
wenzelm@23171
   184
wenzelm@23171
   185
      val ctermify = Thm.cterm_of sgn;
wenzelm@23171
   186
      val cvars = map (fn (n,ty) => ctermify (Var ((n,0),ty))) vs
wenzelm@23171
   187
      val allified_term = t |> allify vs;
wenzelm@23171
   188
      val ct = ctermify allified_term;
wenzelm@23171
   189
      val typ_allified_ct = ctermify (allify_term_typs tyvs allified_term);
wenzelm@23171
   190
    in (typ_allified_ct, 
wenzelm@23171
   191
        Drule.forall_elim_vars 0 (Thm.assume ct)) end;
wenzelm@23171
   192
wenzelm@23171
   193
wenzelm@23171
   194
(* change type-vars to fresh type frees *)
wenzelm@23171
   195
fun fix_tvars_to_tfrees_in_terms names ts = 
wenzelm@23171
   196
    let 
wenzelm@23171
   197
      val tfree_names = map fst (List.foldr Term.add_term_tfrees [] ts);
wenzelm@23171
   198
      val tvars = List.foldr Term.add_term_tvars [] ts;
wenzelm@23171
   199
      val (names',renamings) = 
wenzelm@23171
   200
          List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) => 
wenzelm@23171
   201
                         let val n2 = Name.variant Ns n in 
wenzelm@23171
   202
                           (n2::Ns, (tv, (n2,s))::Rs)
wenzelm@23171
   203
                         end) (tfree_names @ names,[]) tvars;
wenzelm@23171
   204
    in renamings end;
wenzelm@23171
   205
fun fix_tvars_to_tfrees th = 
wenzelm@23171
   206
    let 
wenzelm@23171
   207
      val sign = Thm.theory_of_thm th;
wenzelm@23171
   208
      val ctypify = Thm.ctyp_of sign;
wenzelm@23171
   209
      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
wenzelm@23171
   210
      val renamings = fix_tvars_to_tfrees_in_terms 
wenzelm@23171
   211
                        [] ((Thm.prop_of th) :: tpairs);
wenzelm@23171
   212
      val crenamings = 
wenzelm@23171
   213
          map (fn (v,f) => (ctypify (TVar v), ctypify (TFree f)))
wenzelm@23171
   214
              renamings;
wenzelm@23171
   215
      val fixedfrees = map snd crenamings;
wenzelm@23171
   216
    in (fixedfrees, Thm.instantiate (crenamings, []) th) end;
wenzelm@23171
   217
wenzelm@23171
   218
wenzelm@23171
   219
(* change type-free's to type-vars in th, skipping the ones in "ns" *)
wenzelm@23171
   220
fun unfix_tfrees ns th = 
wenzelm@23171
   221
    let 
wenzelm@23171
   222
      val varfiytfrees = map (Term.dest_TFree o Thm.typ_of) ns
wenzelm@23171
   223
      val skiptfrees = subtract (op =) varfiytfrees (Term.add_term_tfrees (Thm.prop_of th,[]));
wenzelm@23171
   224
    in #2 (Thm.varifyT' skiptfrees th) end;
wenzelm@23171
   225
wenzelm@23171
   226
(* change schematic/meta vars to fresh free vars, avoiding name clashes 
wenzelm@23171
   227
   with "names" *)
wenzelm@23171
   228
fun fix_vars_to_frees_in_terms names ts = 
wenzelm@23171
   229
    let 
wenzelm@23171
   230
      val vars = map Term.dest_Var (List.foldr Term.add_term_vars [] ts);
wenzelm@23171
   231
      val Ns = List.foldr Term.add_term_names names ts;
wenzelm@23171
   232
      val (_,renamings) = 
wenzelm@23171
   233
          Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => 
wenzelm@23171
   234
                    let val n2 = Name.variant Ns n in
wenzelm@23171
   235
                      (n2 :: Ns, (v, (n2,ty)) :: Rs)
wenzelm@23171
   236
                    end) ((Ns,[]), vars);
wenzelm@23171
   237
    in renamings end;
wenzelm@23171
   238
fun fix_vars_to_frees th = 
wenzelm@23171
   239
    let 
wenzelm@23171
   240
      val ctermify = Thm.cterm_of (Thm.theory_of_thm th)
wenzelm@23171
   241
      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
wenzelm@23171
   242
      val renamings = fix_vars_to_frees_in_terms 
wenzelm@23171
   243
                        [] ([Thm.prop_of th] @ tpairs);
wenzelm@23171
   244
      val crenamings = 
wenzelm@23171
   245
          map (fn (v,f) => (ctermify (Var v), ctermify (Free f)))
wenzelm@23171
   246
              renamings;
wenzelm@23171
   247
      val fixedfrees = map snd crenamings;
wenzelm@23171
   248
    in (fixedfrees, Thm.instantiate ([], crenamings) th) end;
wenzelm@23171
   249
wenzelm@23171
   250
fun fix_tvars_upto_idx ix th = 
wenzelm@23171
   251
    let 
wenzelm@23171
   252
      val sgn = Thm.theory_of_thm th;
wenzelm@23171
   253
      val ctypify = Thm.ctyp_of sgn
wenzelm@23171
   254
      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
wenzelm@23171
   255
      val prop = (Thm.prop_of th);
wenzelm@23171
   256
      val tvars = List.foldr Term.add_term_tvars [] (prop :: tpairs);
wenzelm@23171
   257
      val ctyfixes = 
wenzelm@23171
   258
          map_filter 
wenzelm@23171
   259
            (fn (v as ((s,i),ty)) => 
wenzelm@23171
   260
                if i <= ix then SOME (ctypify (TVar v), ctypify (TFree (s,ty)))
wenzelm@23171
   261
                else NONE) tvars;
wenzelm@23171
   262
    in Thm.instantiate (ctyfixes, []) th end;
wenzelm@23171
   263
fun fix_vars_upto_idx ix th = 
wenzelm@23171
   264
    let 
wenzelm@23171
   265
      val sgn = Thm.theory_of_thm th;
wenzelm@23171
   266
      val ctermify = Thm.cterm_of sgn
wenzelm@23171
   267
      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
wenzelm@23171
   268
      val prop = (Thm.prop_of th);
wenzelm@23171
   269
      val vars = map Term.dest_Var (List.foldr Term.add_term_vars 
wenzelm@23171
   270
                                               [] (prop :: tpairs));
wenzelm@23171
   271
      val cfixes = 
wenzelm@23171
   272
          map_filter 
wenzelm@23171
   273
            (fn (v as ((s,i),ty)) => 
wenzelm@23171
   274
                if i <= ix then SOME (ctermify (Var v), ctermify (Free (s,ty)))
wenzelm@23171
   275
                else NONE) vars;
wenzelm@23171
   276
    in Thm.instantiate ([], cfixes) th end;
wenzelm@23171
   277
wenzelm@23171
   278
wenzelm@23171
   279
(* make free vars into schematic vars with index zero *)
wenzelm@23171
   280
 fun unfix_frees frees = 
wenzelm@23171
   281
     apply (map (K (Drule.forall_elim_var 0)) frees) 
wenzelm@23171
   282
     o Drule.forall_intr_list frees;
wenzelm@23171
   283
wenzelm@23171
   284
(* fix term and type variables *)
wenzelm@23171
   285
fun fix_vars_and_tvars th = 
wenzelm@23171
   286
    let val (tvars, th') = fix_tvars_to_tfrees th
wenzelm@23171
   287
      val (vars, th'') = fix_vars_to_frees th' 
wenzelm@23171
   288
    in ((vars, tvars), th'') end;
wenzelm@23171
   289
wenzelm@23171
   290
(* implicit Thm.thm argument *)
wenzelm@23171
   291
(* assumes: vars may contain fixed versions of the frees *)
wenzelm@23171
   292
(* THINK: what if vs already has types varified? *)
wenzelm@23171
   293
fun unfix_frees_and_tfrees (vs,tvs) = 
wenzelm@23171
   294
    (unfix_tfrees tvs o unfix_frees vs);
wenzelm@23171
   295
wenzelm@23171
   296
(* datatype to capture an exported result, ie a fix or assume. *)
wenzelm@23171
   297
datatype export = 
wenzelm@23171
   298
         export of {fixes : Thm.cterm list, (* fixed vars *)
wenzelm@23171
   299
                    assumes : Thm.cterm list, (* hidden hyps/assumed prems *)
wenzelm@23171
   300
                    sgid : int,
wenzelm@23171
   301
                    gth :  Thm.thm}; (* subgoal/goalthm *)
wenzelm@23171
   302
wenzelm@23171
   303
fun fixes_of_exp (export rep) = #fixes rep;
wenzelm@23171
   304
wenzelm@23171
   305
(* export the result of the new goal thm, ie if we reduced teh
wenzelm@23171
   306
subgoal, then we get a new reduced subtgoal with the old
wenzelm@23171
   307
all-quantified variables *)
wenzelm@23171
   308
local 
wenzelm@23171
   309
wenzelm@23171
   310
(* allify puts in a meta level univ quantifier for a free variavble *)
wenzelm@23171
   311
fun allify_term (v, t) = 
wenzelm@23171
   312
    let val vt = #t (Thm.rep_cterm v)
wenzelm@23171
   313
      val (n,ty) = Term.dest_Free vt
wenzelm@23171
   314
    in (Term.all ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end;
wenzelm@23171
   315
wenzelm@23171
   316
fun allify_for_sg_term ctermify vs t =
wenzelm@23171
   317
    let val t_alls = foldr allify_term t vs;
wenzelm@23171
   318
        val ct_alls = ctermify t_alls; 
wenzelm@23171
   319
    in 
wenzelm@23171
   320
      (ct_alls, Drule.forall_elim_list vs (Thm.assume ct_alls))
wenzelm@23171
   321
    end;
wenzelm@23171
   322
(* lookup type of a free var name from a list *)
wenzelm@23171
   323
fun lookupfree vs vn  = 
wenzelm@23171
   324
    case Library.find_first (fn (n,ty) => n = vn) vs of 
wenzelm@23171
   325
      NONE => error ("prepare_goal_export:lookupfree: " ^ vn ^ " does not occur in the term")
wenzelm@23171
   326
    | SOME x => x;
wenzelm@23171
   327
in
wenzelm@23171
   328
fun export_back (export {fixes = vs, assumes = hprems, 
wenzelm@23171
   329
                         sgid = i, gth = gth}) newth = 
wenzelm@23171
   330
    let 
wenzelm@23171
   331
      val sgn = Thm.theory_of_thm newth;
wenzelm@23171
   332
      val ctermify = Thm.cterm_of sgn;
wenzelm@23171
   333
wenzelm@23171
   334
      val sgs = prems_of newth;
wenzelm@23171
   335
      val (sgallcts, sgthms) = 
wenzelm@23171
   336
          Library.split_list (map (allify_for_sg_term ctermify vs) sgs);
wenzelm@23171
   337
      val minimal_newth = 
wenzelm@23171
   338
          (Library.foldl (fn ( newth', sgthm) => 
wenzelm@23171
   339
                          Drule.compose_single (sgthm, 1, newth'))
wenzelm@23171
   340
                      (newth, sgthms));
wenzelm@23171
   341
      val allified_newth = 
wenzelm@23171
   342
          minimal_newth 
wenzelm@23171
   343
            |> Drule.implies_intr_list hprems
wenzelm@23171
   344
            |> Drule.forall_intr_list vs 
wenzelm@23171
   345
wenzelm@23171
   346
      val newth' = Drule.implies_intr_list sgallcts allified_newth
wenzelm@23171
   347
    in
wenzelm@23171
   348
      bicompose false (false, newth', (length sgallcts)) i gth
wenzelm@23171
   349
    end;
wenzelm@23171
   350
wenzelm@23171
   351
(* 
wenzelm@23171
   352
Given "vs" : names of free variables to abstract over,
wenzelm@23171
   353
Given cterms : premices to abstract over (P1... Pn) in terms of vs,
wenzelm@23171
   354
Given a thm of the form: 
wenzelm@23171
   355
P1 vs; ...; Pn vs ==> Goal(C vs)
wenzelm@23171
   356
wenzelm@23171
   357
Gives back: 
wenzelm@23171
   358
(n, length of given cterms which have been allified
wenzelm@23171
   359
 [| !! vs. P1 vs; !! vs. Pn vs |] ==> !! C vs) the allified thm
wenzelm@23171
   360
*)
wenzelm@23171
   361
(* note: C may contain further premices etc 
wenzelm@23171
   362
Note that cterms is the assumed facts, ie prems of "P1" that are
wenzelm@23171
   363
reintroduced in allified form.
wenzelm@23171
   364
*)
wenzelm@23171
   365
fun prepare_goal_export (vs, cterms) th = 
wenzelm@23171
   366
    let 
wenzelm@23171
   367
      val sgn = Thm.theory_of_thm th;
wenzelm@23171
   368
      val ctermify = Thm.cterm_of sgn;
wenzelm@23171
   369
wenzelm@23171
   370
      val allfrees = map Term.dest_Free (Term.term_frees (Thm.prop_of th))
wenzelm@23171
   371
      val cfrees = map (ctermify o Free o lookupfree allfrees) vs
wenzelm@23171
   372
wenzelm@23171
   373
      val sgs = prems_of th;
wenzelm@23171
   374
      val (sgallcts, sgthms) = 
wenzelm@23171
   375
          Library.split_list (map (allify_for_sg_term ctermify cfrees) sgs);
wenzelm@23171
   376
wenzelm@23171
   377
      val minimal_th = 
wenzelm@23171
   378
          Goal.conclude (Library.foldl (fn ( th', sgthm) => 
wenzelm@23171
   379
                          Drule.compose_single (sgthm, 1, th'))
wenzelm@23171
   380
                      (th, sgthms));
wenzelm@23171
   381
wenzelm@23171
   382
      val allified_th = 
wenzelm@23171
   383
          minimal_th 
wenzelm@23171
   384
            |> Drule.implies_intr_list cterms
wenzelm@23171
   385
            |> Drule.forall_intr_list cfrees 
wenzelm@23171
   386
wenzelm@23171
   387
      val th' = Drule.implies_intr_list sgallcts allified_th
wenzelm@23171
   388
    in
wenzelm@23171
   389
      ((length sgallcts), th')
wenzelm@23171
   390
    end;
wenzelm@23171
   391
wenzelm@23171
   392
end;
wenzelm@23171
   393
wenzelm@23171
   394
wenzelm@23171
   395
(* exporting function that takes a solution to the fixed/assumed goal,
wenzelm@23171
   396
and uses this to solve the subgoal in the main theorem *)
wenzelm@23171
   397
fun export_solution (export {fixes = cfvs, assumes = hcprems,
wenzelm@23171
   398
                             sgid = i, gth = gth}) solth = 
wenzelm@23171
   399
    let 
wenzelm@23171
   400
      val solth' = 
wenzelm@23171
   401
          solth |> Drule.implies_intr_list hcprems
wenzelm@23171
   402
                |> Drule.forall_intr_list cfvs
wenzelm@23171
   403
    in Drule.compose_single (solth', i, gth) end;
wenzelm@23171
   404
wenzelm@23171
   405
fun export_solutions (xs,th) = foldr (uncurry export_solution) th xs;
wenzelm@23171
   406
wenzelm@23171
   407
wenzelm@23171
   408
(* fix parameters of a subgoal "i", as free variables, and create an
wenzelm@23171
   409
exporting function that will use the result of this proved goal to
wenzelm@23171
   410
show the goal in the original theorem. 
wenzelm@23171
   411
wenzelm@23171
   412
Note, an advantage of this over Isar is that it supports instantiation
wenzelm@23171
   413
of unkowns in the earlier theorem, ie we can do instantiation of meta
wenzelm@23171
   414
vars! 
wenzelm@23171
   415
wenzelm@23171
   416
avoids constant, free and vars names. 
wenzelm@23171
   417
wenzelm@23171
   418
loosely corresponds to:
wenzelm@23171
   419
Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
wenzelm@23171
   420
Result: 
wenzelm@23171
   421
  ("(As ==> SGi x') ==> (As ==> SGi x')" : thm, 
wenzelm@23171
   422
   expf : 
wenzelm@23171
   423
     ("As ==> SGi x'" : thm) -> 
wenzelm@23171
   424
     ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
wenzelm@23171
   425
*)
wenzelm@23171
   426
fun fix_alls_in_term alledt = 
wenzelm@23171
   427
    let
wenzelm@23171
   428
      val t = Term.strip_all_body alledt;
wenzelm@23171
   429
      val alls = rev (Term.strip_all_vars alledt);
wenzelm@23171
   430
      val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t)
wenzelm@23171
   431
      val names = Term.add_term_names (t,varnames);
wenzelm@23171
   432
      val fvs = map Free 
wenzelm@23171
   433
                    (Name.variant_list names (map fst alls)
wenzelm@23171
   434
                       ~~ (map snd alls));
wenzelm@23171
   435
    in ((subst_bounds (fvs,t)), fvs) end;
wenzelm@23171
   436
wenzelm@23171
   437
fun fix_alls_term i t = 
wenzelm@23171
   438
    let 
wenzelm@23171
   439
      val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t)
wenzelm@23171
   440
      val names = Term.add_term_names (t,varnames);
wenzelm@23171
   441
      val gt = Logic.get_goal t i;
wenzelm@23171
   442
      val body = Term.strip_all_body gt;
wenzelm@23171
   443
      val alls = rev (Term.strip_all_vars gt);
wenzelm@23171
   444
      val fvs = map Free 
wenzelm@23171
   445
                    (Name.variant_list names (map fst alls)
wenzelm@23171
   446
                       ~~ (map snd alls));
wenzelm@23171
   447
    in ((subst_bounds (fvs,body)), fvs) end;
wenzelm@23171
   448
wenzelm@23171
   449
fun fix_alls_cterm i th = 
wenzelm@23171
   450
    let
wenzelm@23171
   451
      val ctermify = Thm.cterm_of (Thm.theory_of_thm th);
wenzelm@23171
   452
      val (fixedbody, fvs) = fix_alls_term i (Thm.prop_of th);
wenzelm@23171
   453
      val cfvs = rev (map ctermify fvs);
wenzelm@23171
   454
      val ct_body = ctermify fixedbody
wenzelm@23171
   455
    in
wenzelm@23171
   456
      (ct_body, cfvs)
wenzelm@23171
   457
    end;
wenzelm@23171
   458
wenzelm@23171
   459
fun fix_alls' i = 
wenzelm@23171
   460
     (apfst Thm.trivial) o (fix_alls_cterm i);
wenzelm@23171
   461
wenzelm@23171
   462
wenzelm@23171
   463
(* hide other goals *) 
wenzelm@23171
   464
(* note the export goal is rotated by (i - 1) and will have to be
wenzelm@23171
   465
unrotated to get backto the originial position(s) *)
wenzelm@23171
   466
fun hide_other_goals th = 
wenzelm@23171
   467
    let
wenzelm@23171
   468
      (* tl beacuse fst sg is the goal we are interested in *)
wenzelm@23171
   469
      val cprems = tl (Drule.cprems_of th)
wenzelm@23171
   470
      val aprems = map Thm.assume cprems
wenzelm@23171
   471
    in
wenzelm@23171
   472
      (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, 
wenzelm@23171
   473
       cprems)
wenzelm@23171
   474
    end;
wenzelm@23171
   475
wenzelm@23171
   476
(* a nicer version of the above that leaves only a single subgoal (the
wenzelm@23171
   477
other subgoals are hidden hyps, that the exporter suffles about)
wenzelm@23171
   478
namely the subgoal that we were trying to solve. *)
wenzelm@23171
   479
(* loosely corresponds to:
wenzelm@23171
   480
Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
wenzelm@23171
   481
Result: 
wenzelm@23171
   482
  ("(As ==> SGi x') ==> SGi x'" : thm, 
wenzelm@23171
   483
   expf : 
wenzelm@23171
   484
     ("SGi x'" : thm) -> 
wenzelm@23171
   485
     ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
wenzelm@23171
   486
*)
wenzelm@23171
   487
fun fix_alls i th = 
wenzelm@23171
   488
    let 
wenzelm@23171
   489
      val (fixed_gth, fixedvars) = fix_alls' i th
wenzelm@23171
   490
      val (sml_gth, othergoals) = hide_other_goals fixed_gth
wenzelm@23171
   491
    in
wenzelm@23171
   492
      (sml_gth, export {fixes = fixedvars, 
wenzelm@23171
   493
                        assumes = othergoals, 
wenzelm@23171
   494
                        sgid = i, gth = th})
wenzelm@23171
   495
    end;
wenzelm@23171
   496
wenzelm@23171
   497
wenzelm@23171
   498
(* assume the premises of subgoal "i", this gives back a list of
wenzelm@23171
   499
assumed theorems that are the premices of subgoal i, it also gives
wenzelm@23171
   500
back a new goal thm and an exporter, the new goalthm is as the old
wenzelm@23171
   501
one, but without the premices, and the exporter will use a proof of
wenzelm@23171
   502
the new goalthm, possibly using the assumed premices, to shoe the
wenzelm@23171
   503
orginial goal.
wenzelm@23171
   504
wenzelm@23171
   505
Note: Dealing with meta vars, need to meta-level-all them in the
wenzelm@23171
   506
shyps, which we can later instantiate with a specific value.... ? 
wenzelm@23171
   507
think about this... maybe need to introduce some new fixed vars and
wenzelm@23171
   508
then remove them again at the end... like I do with rw_inst. 
wenzelm@23171
   509
wenzelm@23171
   510
loosely corresponds to:
wenzelm@23171
   511
Given "[| SG0; ... [| A0; ... An |] ==> SGi; ... SGm |] ==> G" : thm
wenzelm@23171
   512
Result: 
wenzelm@23171
   513
(["A0" [A0], ... ,"An" [An]] : thm list, -- assumptions
wenzelm@23171
   514
 "SGi ==> SGi" : thm, -- new goal 
wenzelm@23171
   515
 "SGi" ["A0" ... "An"] : thm ->   -- export function
wenzelm@23171
   516
    ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list)
wenzelm@23171
   517
*)
wenzelm@23171
   518
fun assume_prems i th =
wenzelm@23171
   519
    let 
wenzelm@23171
   520
      val t = (prop_of th); 
wenzelm@23171
   521
      val gt = Logic.get_goal t i;
wenzelm@23171
   522
      val _ = case Term.strip_all_vars gt of [] => () 
wenzelm@23171
   523
              | _ => error "assume_prems: goal has params"
wenzelm@23171
   524
      val body = gt;
wenzelm@23171
   525
      val prems = Logic.strip_imp_prems body;
wenzelm@23171
   526
      val concl = Logic.strip_imp_concl body;
wenzelm@23171
   527
wenzelm@23171
   528
      val sgn = Thm.theory_of_thm th;
wenzelm@23171
   529
      val ctermify = Thm.cterm_of sgn;
wenzelm@23171
   530
      val cprems = map ctermify prems;
wenzelm@23171
   531
      val aprems = map Thm.assume cprems;
wenzelm@23171
   532
      val gthi = Thm.trivial (ctermify concl);
wenzelm@23171
   533
wenzelm@23171
   534
      (* fun explortf thi = 
wenzelm@23171
   535
          Drule.compose (Drule.implies_intr_list cprems thi, 
wenzelm@23171
   536
                         i, th) *)
wenzelm@23171
   537
    in
wenzelm@23171
   538
      (aprems, gthi, cprems)
wenzelm@23171
   539
    end;
wenzelm@23171
   540
wenzelm@23171
   541
wenzelm@23171
   542
(* first fix the variables, then assume the assumptions *)
wenzelm@23171
   543
(* loosely corresponds to:
wenzelm@23171
   544
Given 
wenzelm@23171
   545
  "[| SG0; ... 
wenzelm@23171
   546
      !! xs. [| A0 xs; ... An xs |] ==> SGi xs; 
wenzelm@23171
   547
      ... SGm |] ==> G" : thm
wenzelm@23171
   548
Result: 
wenzelm@23171
   549
(["A0 xs'" [A0 xs'], ... ,"An xs'" [An xs']] : thm list, -- assumptions
wenzelm@23171
   550
 "SGi xs' ==> SGi xs'" : thm,  -- new goal 
wenzelm@23171
   551
 "SGi xs'" ["A0 xs'" ... "An xs'"] : thm ->   -- export function
wenzelm@23171
   552
    ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list)
wenzelm@23171
   553
*)
wenzelm@23171
   554
wenzelm@23171
   555
(* Note: the fix_alls actually pulls through all the assumptions which
wenzelm@23171
   556
means that the second export is not needed. *)
wenzelm@23171
   557
fun fixes_and_assumes i th = 
wenzelm@23171
   558
    let 
wenzelm@23171
   559
      val (fixgth, exp1) = fix_alls i th
wenzelm@23171
   560
      val (assumps, goalth, _) = assume_prems 1 fixgth
wenzelm@23171
   561
    in 
wenzelm@23171
   562
      (assumps, goalth, exp1)
wenzelm@23171
   563
    end;
wenzelm@23171
   564
wenzelm@23171
   565
wenzelm@23171
   566
(* Fixme: allow different order of subgoals given to expf *)
wenzelm@23171
   567
(* make each subgoal into a separate thm that needs to be proved *)
wenzelm@23171
   568
(* loosely corresponds to:
wenzelm@23171
   569
Given 
wenzelm@23171
   570
  "[| SG0; ... SGm |] ==> G" : thm
wenzelm@23171
   571
Result: 
wenzelm@23171
   572
(["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals
wenzelm@23171
   573
 ["SG0", ..., "SGm"] : thm list ->   -- export function
wenzelm@23171
   574
   "G" : thm)
wenzelm@23171
   575
*)
wenzelm@23171
   576
fun subgoal_thms th = 
wenzelm@23171
   577
    let 
wenzelm@23171
   578
      val t = (prop_of th); 
wenzelm@23171
   579
wenzelm@23171
   580
      val prems = Logic.strip_imp_prems t;
wenzelm@23171
   581
wenzelm@23171
   582
      val sgn = Thm.theory_of_thm th;
wenzelm@23171
   583
      val ctermify = Thm.cterm_of sgn;
wenzelm@23171
   584
wenzelm@23171
   585
      val aprems = map (Thm.trivial o ctermify) prems;
wenzelm@23171
   586
wenzelm@23171
   587
      fun explortf premths = 
wenzelm@23171
   588
          Drule.implies_elim_list th premths
wenzelm@23171
   589
    in
wenzelm@23171
   590
      (aprems, explortf)
wenzelm@23171
   591
    end;
wenzelm@23171
   592
wenzelm@23171
   593
wenzelm@23171
   594
(* make all the premices of a theorem hidden, and provide an unhide
wenzelm@23171
   595
function, that will bring them back out at a later point. This is
wenzelm@23171
   596
useful if you want to get back these premices, after having used the
wenzelm@23171
   597
theorem with the premices hidden *)
wenzelm@23171
   598
(* loosely corresponds to:
wenzelm@23171
   599
Given "As ==> G" : thm
wenzelm@23171
   600
Result: ("G [As]" : thm, 
wenzelm@23171
   601
         "G [As]" : thm -> "As ==> G" : thm
wenzelm@23171
   602
*)
wenzelm@23171
   603
fun hide_prems th = 
wenzelm@23171
   604
    let 
wenzelm@23171
   605
      val cprems = Drule.cprems_of th;
wenzelm@23171
   606
      val aprems = map Thm.assume cprems;
wenzelm@23171
   607
    (*   val unhidef = Drule.implies_intr_list cprems; *)
wenzelm@23171
   608
    in
wenzelm@23171
   609
      (Drule.implies_elim_list th aprems, cprems)
wenzelm@23171
   610
    end;
wenzelm@23171
   611
wenzelm@23171
   612
wenzelm@23171
   613
wenzelm@23171
   614
wenzelm@23171
   615
(* Fixme: allow different order of subgoals in exportf *)
wenzelm@23171
   616
(* as above, but also fix all parameters in all subgoals, and uses
wenzelm@23171
   617
fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent
wenzelm@23171
   618
subgoals. *)
wenzelm@23171
   619
(* loosely corresponds to:
wenzelm@23171
   620
Given 
wenzelm@23171
   621
  "[| !! x0s. A0s x0s ==> SG0 x0s; 
wenzelm@23171
   622
      ...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm
wenzelm@23171
   623
Result: 
wenzelm@23171
   624
(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'", 
wenzelm@23171
   625
  ... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals
wenzelm@23171
   626
 ["SG0 x0s'", ..., "SGm xms'"] : thm list ->   -- export function
wenzelm@23171
   627
   "G" : thm)
wenzelm@23171
   628
*)
wenzelm@23171
   629
(* requires being given solutions! *)
wenzelm@23171
   630
fun fixed_subgoal_thms th = 
wenzelm@23171
   631
    let 
wenzelm@23171
   632
      val (subgoals, expf) = subgoal_thms th;
wenzelm@23171
   633
(*       fun export_sg (th, exp) = exp th; *)
wenzelm@23171
   634
      fun export_sgs expfs solthms = 
wenzelm@23171
   635
          expf (map2 (curry (op |>)) solthms expfs);
wenzelm@23171
   636
(*           expf (map export_sg (ths ~~ expfs)); *)
wenzelm@23171
   637
    in 
wenzelm@23171
   638
      apsnd export_sgs (Library.split_list (map (apsnd export_solution o 
wenzelm@23171
   639
                                                 fix_alls 1) subgoals))
wenzelm@23171
   640
    end;
wenzelm@23171
   641
wenzelm@23171
   642
end;