src/Tools/IsaPlanner/isand.ML
author wenzelm
Wed Sep 12 22:00:29 2012 +0200 (2012-09-12)
changeset 49339 d1fcb4de8349
parent 46777 1ce61ee1571a
child 49340 25fc6e0da459
permissions -rw-r--r--
eliminated some old material that is unused in the visible universe;
wenzelm@23175
     1
(*  Title:      Tools/IsaPlanner/isand.ML
wenzelm@23171
     2
    Author:     Lucas Dixon, University of Edinburgh
wenzelm@23175
     3
wenzelm@23175
     4
Natural Deduction tools.
wenzelm@23171
     5
wenzelm@23175
     6
For working with Isabelle theorems in a natural detuction style.
wenzelm@23175
     7
ie, not having to deal with meta level quantified varaibles,
wenzelm@23175
     8
instead, we work with newly introduced frees, and hide the
wenzelm@23175
     9
"all"'s, exporting results from theorems proved with the frees, to
wenzelm@23175
    10
solve the all cases of the previous goal. This allows resolution
wenzelm@49339
    11
to do proof search normally.
wenzelm@23171
    12
wenzelm@23175
    13
Note: A nice idea: allow exporting to solve any subgoal, thus
wenzelm@23175
    14
allowing the interleaving of proof, or provide a structure for the
wenzelm@23175
    15
ordering of proof, thus allowing proof attempts in parrell, but
wenzelm@23175
    16
recording the order to apply things in.
wenzelm@23171
    17
wenzelm@23175
    18
THINK: are we really ok with our varify name w.r.t the prop - do
wenzelm@23175
    19
we also need to avoid names in the hidden hyps? What about
wenzelm@23175
    20
unification contraints in flex-flex pairs - might they also have
wenzelm@23175
    21
extra free vars?
wenzelm@23171
    22
*)
wenzelm@23171
    23
wenzelm@23171
    24
signature ISA_ND =
wenzelm@23171
    25
sig
wenzelm@23171
    26
  (* inserting meta level params for frees in the conditions *)
wenzelm@49339
    27
  val allify_conditions : (term -> cterm) -> (string * typ) list -> thm -> thm * cterm list
wenzelm@23171
    28
wenzelm@23171
    29
  (* meta level fixed params (i.e. !! vars) *)
wenzelm@49339
    30
  val fix_alls_term : int -> term -> term * term list
wenzelm@23171
    31
wenzelm@49339
    32
  val unfix_frees : cterm list -> thm -> thm
wenzelm@23171
    33
wenzelm@23171
    34
  (* assumptions/subgoals *)
wenzelm@49339
    35
  val fixed_subgoal_thms : thm -> thm list * (thm list -> thm)
wenzelm@23171
    36
end
wenzelm@23171
    37
wenzelm@49339
    38
structure IsaND : ISA_ND =
wenzelm@49339
    39
struct
wenzelm@23171
    40
wenzelm@23171
    41
(* Given ctertmify function, (string,type) pairs capturing the free
wenzelm@23171
    42
vars that need to be allified in the assumption, and a theorem with
wenzelm@23171
    43
assumptions possibly containing the free vars, then we give back the
wenzelm@49339
    44
assumptions allified as hidden hyps.
wenzelm@23171
    45
wenzelm@49339
    46
Given: x
wenzelm@49339
    47
th: A vs ==> B vs
wenzelm@23171
    48
Results in: "B vs" [!!x. A x]
wenzelm@23171
    49
*)
wenzelm@49339
    50
fun allify_conditions ctermify Ts th =
wenzelm@49339
    51
    let
wenzelm@23171
    52
      val premts = Thm.prems_of th;
wenzelm@49339
    53
wenzelm@49339
    54
      fun allify_prem_var (vt as (n,ty),t)  =
wenzelm@46217
    55
          (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
wenzelm@23171
    56
wenzelm@30190
    57
      fun allify_prem Ts p = List.foldr allify_prem_var p Ts
wenzelm@23171
    58
wenzelm@23171
    59
      val cTs = map (ctermify o Free) Ts
wenzelm@23171
    60
      val cterm_asms = map (ctermify o allify_prem Ts) premts
wenzelm@23171
    61
      val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms
wenzelm@49339
    62
    in
wenzelm@23171
    63
      (Library.foldl (fn (x,y) => y COMP x) (th, allifyied_asm_thms), cterm_asms)
wenzelm@23171
    64
    end;
wenzelm@23171
    65
wenzelm@23171
    66
(* make free vars into schematic vars with index zero *)
wenzelm@49339
    67
fun unfix_frees frees =
wenzelm@46777
    68
     fold (K (Thm.forall_elim_var 0)) frees
wenzelm@23171
    69
     o Drule.forall_intr_list frees;
wenzelm@23171
    70
wenzelm@23171
    71
(* datatype to capture an exported result, ie a fix or assume. *)
wenzelm@49339
    72
datatype export =
wenzelm@23171
    73
         export of {fixes : Thm.cterm list, (* fixed vars *)
wenzelm@23171
    74
                    assumes : Thm.cterm list, (* hidden hyps/assumed prems *)
wenzelm@23171
    75
                    sgid : int,
wenzelm@23171
    76
                    gth :  Thm.thm}; (* subgoal/goalthm *)
wenzelm@23171
    77
wenzelm@23171
    78
(* exporting function that takes a solution to the fixed/assumed goal,
wenzelm@23171
    79
and uses this to solve the subgoal in the main theorem *)
wenzelm@23171
    80
fun export_solution (export {fixes = cfvs, assumes = hcprems,
wenzelm@49339
    81
                             sgid = i, gth = gth}) solth =
wenzelm@49339
    82
    let
wenzelm@49339
    83
      val solth' =
wenzelm@23171
    84
          solth |> Drule.implies_intr_list hcprems
wenzelm@23171
    85
                |> Drule.forall_intr_list cfvs
wenzelm@23171
    86
    in Drule.compose_single (solth', i, gth) end;
wenzelm@23171
    87
wenzelm@23171
    88
wenzelm@23171
    89
(* fix parameters of a subgoal "i", as free variables, and create an
wenzelm@23171
    90
exporting function that will use the result of this proved goal to
wenzelm@49339
    91
show the goal in the original theorem.
wenzelm@23171
    92
wenzelm@23171
    93
Note, an advantage of this over Isar is that it supports instantiation
wenzelm@23171
    94
of unkowns in the earlier theorem, ie we can do instantiation of meta
wenzelm@49339
    95
vars!
wenzelm@23171
    96
wenzelm@49339
    97
avoids constant, free and vars names.
wenzelm@23171
    98
wenzelm@23171
    99
loosely corresponds to:
wenzelm@23171
   100
Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
wenzelm@49339
   101
Result:
wenzelm@49339
   102
  ("(As ==> SGi x') ==> (As ==> SGi x')" : thm,
wenzelm@49339
   103
   expf :
wenzelm@49339
   104
     ("As ==> SGi x'" : thm) ->
wenzelm@23171
   105
     ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
wenzelm@23171
   106
*)
wenzelm@49339
   107
fun fix_alls_term i t =
wenzelm@23171
   108
    let
wenzelm@44121
   109
      val varnames = map (fst o fst o Term.dest_Var) (Misc_Legacy.term_vars t)
wenzelm@44121
   110
      val names = Misc_Legacy.add_term_names (t,varnames);
wenzelm@23171
   111
      val gt = Logic.get_goal t i;
wenzelm@23171
   112
      val body = Term.strip_all_body gt;
wenzelm@23171
   113
      val alls = rev (Term.strip_all_vars gt);
wenzelm@49339
   114
      val fvs = map Free
wenzelm@23171
   115
                    (Name.variant_list names (map fst alls)
wenzelm@23171
   116
                       ~~ (map snd alls));
wenzelm@23171
   117
    in ((subst_bounds (fvs,body)), fvs) end;
wenzelm@23171
   118
wenzelm@49339
   119
fun fix_alls_cterm i th =
wenzelm@23171
   120
    let
wenzelm@23171
   121
      val ctermify = Thm.cterm_of (Thm.theory_of_thm th);
wenzelm@23171
   122
      val (fixedbody, fvs) = fix_alls_term i (Thm.prop_of th);
wenzelm@23171
   123
      val cfvs = rev (map ctermify fvs);
wenzelm@23171
   124
      val ct_body = ctermify fixedbody
wenzelm@23171
   125
    in
wenzelm@23171
   126
      (ct_body, cfvs)
wenzelm@23171
   127
    end;
wenzelm@23171
   128
wenzelm@49339
   129
fun fix_alls' i =
wenzelm@23171
   130
     (apfst Thm.trivial) o (fix_alls_cterm i);
wenzelm@23171
   131
wenzelm@23171
   132
wenzelm@49339
   133
(* hide other goals *)
wenzelm@23171
   134
(* note the export goal is rotated by (i - 1) and will have to be
wenzelm@23171
   135
unrotated to get backto the originial position(s) *)
wenzelm@49339
   136
fun hide_other_goals th =
wenzelm@23171
   137
    let
wenzelm@23171
   138
      (* tl beacuse fst sg is the goal we are interested in *)
wenzelm@23171
   139
      val cprems = tl (Drule.cprems_of th)
wenzelm@23171
   140
      val aprems = map Thm.assume cprems
wenzelm@23171
   141
    in
wenzelm@49339
   142
      (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems,
wenzelm@23171
   143
       cprems)
wenzelm@23171
   144
    end;
wenzelm@23171
   145
wenzelm@23171
   146
(* a nicer version of the above that leaves only a single subgoal (the
wenzelm@23171
   147
other subgoals are hidden hyps, that the exporter suffles about)
wenzelm@23171
   148
namely the subgoal that we were trying to solve. *)
wenzelm@23171
   149
(* loosely corresponds to:
wenzelm@23171
   150
Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
wenzelm@49339
   151
Result:
wenzelm@49339
   152
  ("(As ==> SGi x') ==> SGi x'" : thm,
wenzelm@49339
   153
   expf :
wenzelm@49339
   154
     ("SGi x'" : thm) ->
wenzelm@23171
   155
     ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
wenzelm@23171
   156
*)
wenzelm@49339
   157
fun fix_alls i th =
wenzelm@49339
   158
    let
wenzelm@23171
   159
      val (fixed_gth, fixedvars) = fix_alls' i th
wenzelm@23171
   160
      val (sml_gth, othergoals) = hide_other_goals fixed_gth
wenzelm@23171
   161
    in
wenzelm@49339
   162
      (sml_gth, export {fixes = fixedvars,
wenzelm@49339
   163
                        assumes = othergoals,
wenzelm@23171
   164
                        sgid = i, gth = th})
wenzelm@23171
   165
    end;
wenzelm@23171
   166
wenzelm@23171
   167
wenzelm@23171
   168
(* Fixme: allow different order of subgoals given to expf *)
wenzelm@23171
   169
(* make each subgoal into a separate thm that needs to be proved *)
wenzelm@23171
   170
(* loosely corresponds to:
wenzelm@49339
   171
Given
wenzelm@23171
   172
  "[| SG0; ... SGm |] ==> G" : thm
wenzelm@49339
   173
Result:
wenzelm@23171
   174
(["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals
wenzelm@23171
   175
 ["SG0", ..., "SGm"] : thm list ->   -- export function
wenzelm@23171
   176
   "G" : thm)
wenzelm@23171
   177
*)
wenzelm@49339
   178
fun subgoal_thms th =
wenzelm@49339
   179
    let
wenzelm@49339
   180
      val t = (prop_of th);
wenzelm@23171
   181
wenzelm@23171
   182
      val prems = Logic.strip_imp_prems t;
wenzelm@23171
   183
wenzelm@23171
   184
      val sgn = Thm.theory_of_thm th;
wenzelm@23171
   185
      val ctermify = Thm.cterm_of sgn;
wenzelm@23171
   186
wenzelm@23171
   187
      val aprems = map (Thm.trivial o ctermify) prems;
wenzelm@23171
   188
wenzelm@49339
   189
      fun explortf premths =
wenzelm@23171
   190
          Drule.implies_elim_list th premths
wenzelm@23171
   191
    in
wenzelm@23171
   192
      (aprems, explortf)
wenzelm@23171
   193
    end;
wenzelm@23171
   194
wenzelm@23171
   195
wenzelm@23171
   196
(* Fixme: allow different order of subgoals in exportf *)
wenzelm@23171
   197
(* as above, but also fix all parameters in all subgoals, and uses
wenzelm@23171
   198
fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent
wenzelm@23171
   199
subgoals. *)
wenzelm@23171
   200
(* loosely corresponds to:
wenzelm@49339
   201
Given
wenzelm@49339
   202
  "[| !! x0s. A0s x0s ==> SG0 x0s;
wenzelm@23171
   203
      ...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm
wenzelm@49339
   204
Result:
wenzelm@49339
   205
(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'",
wenzelm@23171
   206
  ... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals
wenzelm@23171
   207
 ["SG0 x0s'", ..., "SGm xms'"] : thm list ->   -- export function
wenzelm@23171
   208
   "G" : thm)
wenzelm@23171
   209
*)
wenzelm@23171
   210
(* requires being given solutions! *)
wenzelm@49339
   211
fun fixed_subgoal_thms th =
wenzelm@49339
   212
    let
wenzelm@23171
   213
      val (subgoals, expf) = subgoal_thms th;
wenzelm@23171
   214
(*       fun export_sg (th, exp) = exp th; *)
wenzelm@49339
   215
      fun export_sgs expfs solthms =
wenzelm@23171
   216
          expf (map2 (curry (op |>)) solthms expfs);
wenzelm@23171
   217
(*           expf (map export_sg (ths ~~ expfs)); *)
wenzelm@49339
   218
    in
wenzelm@49339
   219
      apsnd export_sgs (Library.split_list (map (apsnd export_solution o
wenzelm@23171
   220
                                                 fix_alls 1) subgoals))
wenzelm@23171
   221
    end;
wenzelm@23171
   222
wenzelm@23171
   223
end;