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