src/Tools/IsaPlanner/isand.ML
author wenzelm
Thu, 07 Apr 2016 20:51:52 +0200
changeset 62908 d7009a515733
parent 60358 aebfbcab1eb8
permissions -rw-r--r--
clarified mode of ROOT.ML files;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23175
267ba70e7a9d tuned headers -- adapted to usual conventions;
wenzelm
parents: 23171
diff changeset
     1
(*  Title:      Tools/IsaPlanner/isand.ML
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
     2
    Author:     Lucas Dixon, University of Edinburgh
23175
267ba70e7a9d tuned headers -- adapted to usual conventions;
wenzelm
parents: 23171
diff changeset
     3
52244
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
     4
Natural Deduction tools (obsolete).
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
     5
23175
267ba70e7a9d tuned headers -- adapted to usual conventions;
wenzelm
parents: 23171
diff changeset
     6
For working with Isabelle theorems in a natural detuction style.
267ba70e7a9d tuned headers -- adapted to usual conventions;
wenzelm
parents: 23171
diff changeset
     7
ie, not having to deal with meta level quantified varaibles,
267ba70e7a9d tuned headers -- adapted to usual conventions;
wenzelm
parents: 23171
diff changeset
     8
instead, we work with newly introduced frees, and hide the
267ba70e7a9d tuned headers -- adapted to usual conventions;
wenzelm
parents: 23171
diff changeset
     9
"all"'s, exporting results from theorems proved with the frees, to
267ba70e7a9d tuned headers -- adapted to usual conventions;
wenzelm
parents: 23171
diff changeset
    10
solve the all cases of the previous goal. This allows resolution
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 46777
diff changeset
    11
to do proof search normally.
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    12
23175
267ba70e7a9d tuned headers -- adapted to usual conventions;
wenzelm
parents: 23171
diff changeset
    13
Note: A nice idea: allow exporting to solve any subgoal, thus
267ba70e7a9d tuned headers -- adapted to usual conventions;
wenzelm
parents: 23171
diff changeset
    14
allowing the interleaving of proof, or provide a structure for the
267ba70e7a9d tuned headers -- adapted to usual conventions;
wenzelm
parents: 23171
diff changeset
    15
ordering of proof, thus allowing proof attempts in parrell, but
267ba70e7a9d tuned headers -- adapted to usual conventions;
wenzelm
parents: 23171
diff changeset
    16
recording the order to apply things in.
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    17
23175
267ba70e7a9d tuned headers -- adapted to usual conventions;
wenzelm
parents: 23171
diff changeset
    18
THINK: are we really ok with our varify name w.r.t the prop - do
267ba70e7a9d tuned headers -- adapted to usual conventions;
wenzelm
parents: 23171
diff changeset
    19
we also need to avoid names in the hidden hyps? What about
267ba70e7a9d tuned headers -- adapted to usual conventions;
wenzelm
parents: 23171
diff changeset
    20
unification contraints in flex-flex pairs - might they also have
267ba70e7a9d tuned headers -- adapted to usual conventions;
wenzelm
parents: 23171
diff changeset
    21
extra free vars?
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    22
*)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    23
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    24
signature ISA_ND =
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    25
sig
52244
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
    26
  val variant_names: Proof.context -> term list -> string list -> string list
49340
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
    27
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    28
  (* meta level fixed params (i.e. !! vars) *)
52244
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
    29
  val fix_alls_term: Proof.context -> int -> term -> term * term list
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    30
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    31
  (* assumptions/subgoals *)
52244
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
    32
  val fixed_subgoal_thms: Proof.context -> thm -> thm list * (thm list -> thm)
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    33
end
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    34
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 46777
diff changeset
    35
structure IsaND : ISA_ND =
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 46777
diff changeset
    36
struct
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    37
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    38
(* datatype to capture an exported result, ie a fix or assume. *)
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 46777
diff changeset
    39
datatype export =
52244
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
    40
  Export of
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
    41
   {fixes : Thm.cterm list, (* fixed vars *)
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
    42
    assumes : Thm.cterm list, (* hidden hyps/assumed prems *)
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
    43
    sgid : int,
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
    44
    gth :  Thm.thm}; (* subgoal/goalthm *)
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    45
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    46
(* exporting function that takes a solution to the fixed/assumed goal,
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    47
and uses this to solve the subgoal in the main theorem *)
52244
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
    48
fun export_solution (Export {fixes = cfvs, assumes = hcprems, sgid = i, gth = gth}) solth =
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
    49
  let
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
    50
    val solth' = solth
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
    51
      |> Drule.implies_intr_list hcprems
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
    52
      |> Drule.forall_intr_list cfvs;
52467
24c6ddb48cb8 tuned signature;
wenzelm
parents: 52246
diff changeset
    53
  in Drule.compose (solth', i, gth) end;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    54
49340
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
    55
fun variant_names ctxt ts xs =
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
    56
  let
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
    57
    val names =
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
    58
      Variable.names_of ctxt
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
    59
      |> (fold o fold_aterms)
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
    60
          (fn Var ((a, _), _) => Name.declare a
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
    61
            | Free (a, _) => Name.declare a
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
    62
            | _ => I) ts;
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
    63
  in fst (fold_map Name.variant xs names) end;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    64
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    65
(* fix parameters of a subgoal "i", as free variables, and create an
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    66
exporting function that will use the result of this proved goal to
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 46777
diff changeset
    67
show the goal in the original theorem.
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    68
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    69
Note, an advantage of this over Isar is that it supports instantiation
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    70
of unkowns in the earlier theorem, ie we can do instantiation of meta
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 46777
diff changeset
    71
vars!
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    72
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 46777
diff changeset
    73
avoids constant, free and vars names.
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    74
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    75
loosely corresponds to:
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    76
Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 46777
diff changeset
    77
Result:
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 46777
diff changeset
    78
  ("(As ==> SGi x') ==> (As ==> SGi x')" : thm,
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 46777
diff changeset
    79
   expf :
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 46777
diff changeset
    80
     ("As ==> SGi x'" : thm) ->
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    81
     ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    82
*)
49340
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
    83
fun fix_alls_term ctxt i t =
52244
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
    84
  let
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
    85
    val gt = Logic.get_goal t i;
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
    86
    val body = Term.strip_all_body gt;
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
    87
    val alls = rev (Term.strip_all_vars gt);
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
    88
    val xs = variant_names ctxt [t] (map fst alls);
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
    89
    val fvs = map Free (xs ~~ map snd alls);
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
    90
  in ((subst_bounds (fvs,body)), fvs) end;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    91
49340
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
    92
fun fix_alls_cterm ctxt i th =
52244
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
    93
  let
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
    94
    val (fixedbody, fvs) = fix_alls_term ctxt i (Thm.prop_of th);
59641
a2d056424d3c clarified context;
wenzelm
parents: 59621
diff changeset
    95
    val cfvs = rev (map (Thm.cterm_of ctxt) fvs);
a2d056424d3c clarified context;
wenzelm
parents: 59621
diff changeset
    96
    val ct_body = Thm.cterm_of ctxt fixedbody;
52244
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
    97
  in (ct_body, cfvs) end;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    98
49340
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
    99
fun fix_alls' ctxt i = apfst Thm.trivial o fix_alls_cterm ctxt i;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   100
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   101
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 46777
diff changeset
   102
(* hide other goals *)
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   103
(* note the export goal is rotated by (i - 1) and will have to be
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   104
unrotated to get backto the originial position(s) *)
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 46777
diff changeset
   105
fun hide_other_goals th =
52244
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
   106
  let
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
   107
    (* tl beacuse fst sg is the goal we are interested in *)
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
   108
    val cprems = tl (Drule.cprems_of th);
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
   109
    val aprems = map Thm.assume cprems;
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
   110
  in (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, cprems) end;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   111
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   112
(* a nicer version of the above that leaves only a single subgoal (the
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   113
other subgoals are hidden hyps, that the exporter suffles about)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   114
namely the subgoal that we were trying to solve. *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   115
(* loosely corresponds to:
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   116
Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 46777
diff changeset
   117
Result:
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 46777
diff changeset
   118
  ("(As ==> SGi x') ==> SGi x'" : thm,
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 46777
diff changeset
   119
   expf :
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 46777
diff changeset
   120
     ("SGi x'" : thm) ->
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   121
     ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   122
*)
49340
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
   123
fun fix_alls ctxt i th =
52244
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
   124
  let
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
   125
    val (fixed_gth, fixedvars) = fix_alls' ctxt i th
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
   126
    val (sml_gth, othergoals) = hide_other_goals fixed_gth
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
   127
  in (sml_gth, Export {fixes = fixedvars, assumes = othergoals, sgid = i, gth = th}) end;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   128
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   129
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   130
(* Fixme: allow different order of subgoals given to expf *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   131
(* make each subgoal into a separate thm that needs to be proved *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   132
(* loosely corresponds to:
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 46777
diff changeset
   133
Given
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   134
  "[| SG0; ... SGm |] ==> G" : thm
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 46777
diff changeset
   135
Result:
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   136
(["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   137
 ["SG0", ..., "SGm"] : thm list ->   -- export function
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   138
   "G" : thm)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   139
*)
60358
aebfbcab1eb8 clarified context;
wenzelm
parents: 59641
diff changeset
   140
fun subgoal_thms ctxt th =
52244
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
   141
  let
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 52467
diff changeset
   142
    val t = Thm.prop_of th;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   143
52244
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
   144
    val prems = Logic.strip_imp_prems t;
60358
aebfbcab1eb8 clarified context;
wenzelm
parents: 59641
diff changeset
   145
    val aprems = map (Thm.trivial o Thm.cterm_of ctxt) prems;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   146
52244
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
   147
    fun explortf premths = Drule.implies_elim_list th premths;
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
   148
  in (aprems, explortf) end;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   149
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   150
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   151
(* Fixme: allow different order of subgoals in exportf *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   152
(* as above, but also fix all parameters in all subgoals, and uses
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   153
fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   154
subgoals. *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   155
(* loosely corresponds to:
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 46777
diff changeset
   156
Given
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 46777
diff changeset
   157
  "[| !! x0s. A0s x0s ==> SG0 x0s;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   158
      ...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 46777
diff changeset
   159
Result:
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 46777
diff changeset
   160
(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'",
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   161
  ... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   162
 ["SG0 x0s'", ..., "SGm xms'"] : thm list ->   -- export function
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   163
   "G" : thm)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   164
*)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   165
(* requires being given solutions! *)
49340
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
   166
fun fixed_subgoal_thms ctxt th =
52244
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
   167
  let
60358
aebfbcab1eb8 clarified context;
wenzelm
parents: 59641
diff changeset
   168
    val (subgoals, expf) = subgoal_thms ctxt th;
52244
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
   169
(*  fun export_sg (th, exp) = exp th; *)
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
   170
    fun export_sgs expfs solthms =
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
   171
      expf (map2 (curry (op |>)) solthms expfs);
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
   172
(*    expf (map export_sg (ths ~~ expfs)); *)
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
   173
  in
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
   174
    apsnd export_sgs
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
   175
      (Library.split_list (map (apsnd export_solution o fix_alls ctxt 1) subgoals))
cb15da7bd550 misc tuning;
wenzelm
parents: 52242
diff changeset
   176
  end;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   177
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   178
end;