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