src/Tools/IsaPlanner/isand.ML
author wenzelm
Thu May 30 17:26:01 2013 +0200 (2013-05-30)
changeset 52246 54c0d4128b30
parent 52245 f76fb8858e0b
child 52467 24c6ddb48cb8
permissions -rw-r--r--
tuned signature;
wenzelm@23175
     1
(*  Title:      Tools/IsaPlanner/isand.ML
wenzelm@23171
     2
    Author:     Lucas Dixon, University of Edinburgh
wenzelm@23175
     3
wenzelm@52244
     4
Natural Deduction tools (obsolete).
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@52244
    26
  val variant_names: Proof.context -> term list -> string list -> string list
wenzelm@49340
    27
wenzelm@23171
    28
  (* meta level fixed params (i.e. !! vars) *)
wenzelm@52244
    29
  val fix_alls_term: Proof.context -> int -> term -> term * term list
wenzelm@23171
    30
wenzelm@23171
    31
  (* assumptions/subgoals *)
wenzelm@52244
    32
  val fixed_subgoal_thms: Proof.context -> thm -> thm list * (thm list -> thm)
wenzelm@23171
    33
end
wenzelm@23171
    34
wenzelm@49339
    35
structure IsaND : ISA_ND =
wenzelm@49339
    36
struct
wenzelm@23171
    37
wenzelm@23171
    38
(* datatype to capture an exported result, ie a fix or assume. *)
wenzelm@49339
    39
datatype export =
wenzelm@52244
    40
  Export of
wenzelm@52244
    41
   {fixes : Thm.cterm list, (* fixed vars *)
wenzelm@52244
    42
    assumes : Thm.cterm list, (* hidden hyps/assumed prems *)
wenzelm@52244
    43
    sgid : int,
wenzelm@52244
    44
    gth :  Thm.thm}; (* subgoal/goalthm *)
wenzelm@23171
    45
wenzelm@23171
    46
(* exporting function that takes a solution to the fixed/assumed goal,
wenzelm@23171
    47
and uses this to solve the subgoal in the main theorem *)
wenzelm@52244
    48
fun export_solution (Export {fixes = cfvs, assumes = hcprems, sgid = i, gth = gth}) solth =
wenzelm@52244
    49
  let
wenzelm@52244
    50
    val solth' = solth
wenzelm@52244
    51
      |> Drule.implies_intr_list hcprems
wenzelm@52244
    52
      |> Drule.forall_intr_list cfvs;
wenzelm@52244
    53
  in Drule.compose_single (solth', i, gth) end;
wenzelm@23171
    54
wenzelm@49340
    55
fun variant_names ctxt ts xs =
wenzelm@49340
    56
  let
wenzelm@49340
    57
    val names =
wenzelm@49340
    58
      Variable.names_of ctxt
wenzelm@49340
    59
      |> (fold o fold_aterms)
wenzelm@49340
    60
          (fn Var ((a, _), _) => Name.declare a
wenzelm@49340
    61
            | Free (a, _) => Name.declare a
wenzelm@49340
    62
            | _ => I) ts;
wenzelm@49340
    63
  in fst (fold_map Name.variant xs names) end;
wenzelm@23171
    64
wenzelm@23171
    65
(* fix parameters of a subgoal "i", as free variables, and create an
wenzelm@23171
    66
exporting function that will use the result of this proved goal to
wenzelm@49339
    67
show the goal in the original theorem.
wenzelm@23171
    68
wenzelm@23171
    69
Note, an advantage of this over Isar is that it supports instantiation
wenzelm@23171
    70
of unkowns in the earlier theorem, ie we can do instantiation of meta
wenzelm@49339
    71
vars!
wenzelm@23171
    72
wenzelm@49339
    73
avoids constant, free and vars names.
wenzelm@23171
    74
wenzelm@23171
    75
loosely corresponds to:
wenzelm@23171
    76
Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
wenzelm@49339
    77
Result:
wenzelm@49339
    78
  ("(As ==> SGi x') ==> (As ==> SGi x')" : thm,
wenzelm@49339
    79
   expf :
wenzelm@49339
    80
     ("As ==> SGi x'" : thm) ->
wenzelm@23171
    81
     ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
wenzelm@23171
    82
*)
wenzelm@49340
    83
fun fix_alls_term ctxt i t =
wenzelm@52244
    84
  let
wenzelm@52244
    85
    val gt = Logic.get_goal t i;
wenzelm@52244
    86
    val body = Term.strip_all_body gt;
wenzelm@52244
    87
    val alls = rev (Term.strip_all_vars gt);
wenzelm@52244
    88
    val xs = variant_names ctxt [t] (map fst alls);
wenzelm@52244
    89
    val fvs = map Free (xs ~~ map snd alls);
wenzelm@52244
    90
  in ((subst_bounds (fvs,body)), fvs) end;
wenzelm@23171
    91
wenzelm@49340
    92
fun fix_alls_cterm ctxt i th =
wenzelm@52244
    93
  let
wenzelm@52244
    94
    val cert = Thm.cterm_of (Thm.theory_of_thm th);
wenzelm@52244
    95
    val (fixedbody, fvs) = fix_alls_term ctxt i (Thm.prop_of th);
wenzelm@52244
    96
    val cfvs = rev (map cert fvs);
wenzelm@52244
    97
    val ct_body = cert fixedbody;
wenzelm@52244
    98
  in (ct_body, cfvs) end;
wenzelm@23171
    99
wenzelm@49340
   100
fun fix_alls' ctxt i = apfst Thm.trivial o fix_alls_cterm ctxt i;
wenzelm@23171
   101
wenzelm@23171
   102
wenzelm@49339
   103
(* hide other goals *)
wenzelm@23171
   104
(* note the export goal is rotated by (i - 1) and will have to be
wenzelm@23171
   105
unrotated to get backto the originial position(s) *)
wenzelm@49339
   106
fun hide_other_goals th =
wenzelm@52244
   107
  let
wenzelm@52244
   108
    (* tl beacuse fst sg is the goal we are interested in *)
wenzelm@52244
   109
    val cprems = tl (Drule.cprems_of th);
wenzelm@52244
   110
    val aprems = map Thm.assume cprems;
wenzelm@52244
   111
  in (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, cprems) end;
wenzelm@23171
   112
wenzelm@23171
   113
(* a nicer version of the above that leaves only a single subgoal (the
wenzelm@23171
   114
other subgoals are hidden hyps, that the exporter suffles about)
wenzelm@23171
   115
namely the subgoal that we were trying to solve. *)
wenzelm@23171
   116
(* loosely corresponds to:
wenzelm@23171
   117
Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
wenzelm@49339
   118
Result:
wenzelm@49339
   119
  ("(As ==> SGi x') ==> SGi x'" : thm,
wenzelm@49339
   120
   expf :
wenzelm@49339
   121
     ("SGi x'" : thm) ->
wenzelm@23171
   122
     ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
wenzelm@23171
   123
*)
wenzelm@49340
   124
fun fix_alls ctxt i th =
wenzelm@52244
   125
  let
wenzelm@52244
   126
    val (fixed_gth, fixedvars) = fix_alls' ctxt i th
wenzelm@52244
   127
    val (sml_gth, othergoals) = hide_other_goals fixed_gth
wenzelm@52244
   128
  in (sml_gth, Export {fixes = fixedvars, assumes = othergoals, sgid = i, gth = th}) end;
wenzelm@23171
   129
wenzelm@23171
   130
wenzelm@23171
   131
(* Fixme: allow different order of subgoals given to expf *)
wenzelm@23171
   132
(* make each subgoal into a separate thm that needs to be proved *)
wenzelm@23171
   133
(* loosely corresponds to:
wenzelm@49339
   134
Given
wenzelm@23171
   135
  "[| SG0; ... SGm |] ==> G" : thm
wenzelm@49339
   136
Result:
wenzelm@23171
   137
(["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals
wenzelm@23171
   138
 ["SG0", ..., "SGm"] : thm list ->   -- export function
wenzelm@23171
   139
   "G" : thm)
wenzelm@23171
   140
*)
wenzelm@49339
   141
fun subgoal_thms th =
wenzelm@52244
   142
  let
wenzelm@52244
   143
    val cert = Thm.cterm_of (Thm.theory_of_thm th);
wenzelm@23171
   144
wenzelm@52244
   145
    val t = prop_of th;
wenzelm@23171
   146
wenzelm@52244
   147
    val prems = Logic.strip_imp_prems t;
wenzelm@52244
   148
    val aprems = map (Thm.trivial o cert) prems;
wenzelm@23171
   149
wenzelm@52244
   150
    fun explortf premths = Drule.implies_elim_list th premths;
wenzelm@52244
   151
  in (aprems, explortf) end;
wenzelm@23171
   152
wenzelm@23171
   153
wenzelm@23171
   154
(* Fixme: allow different order of subgoals in exportf *)
wenzelm@23171
   155
(* as above, but also fix all parameters in all subgoals, and uses
wenzelm@23171
   156
fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent
wenzelm@23171
   157
subgoals. *)
wenzelm@23171
   158
(* loosely corresponds to:
wenzelm@49339
   159
Given
wenzelm@49339
   160
  "[| !! x0s. A0s x0s ==> SG0 x0s;
wenzelm@23171
   161
      ...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm
wenzelm@49339
   162
Result:
wenzelm@49339
   163
(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'",
wenzelm@23171
   164
  ... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals
wenzelm@23171
   165
 ["SG0 x0s'", ..., "SGm xms'"] : thm list ->   -- export function
wenzelm@23171
   166
   "G" : thm)
wenzelm@23171
   167
*)
wenzelm@23171
   168
(* requires being given solutions! *)
wenzelm@49340
   169
fun fixed_subgoal_thms ctxt th =
wenzelm@52244
   170
  let
wenzelm@52244
   171
    val (subgoals, expf) = subgoal_thms th;
wenzelm@52244
   172
(*  fun export_sg (th, exp) = exp th; *)
wenzelm@52244
   173
    fun export_sgs expfs solthms =
wenzelm@52244
   174
      expf (map2 (curry (op |>)) solthms expfs);
wenzelm@52244
   175
(*    expf (map export_sg (ths ~~ expfs)); *)
wenzelm@52244
   176
  in
wenzelm@52244
   177
    apsnd export_sgs
wenzelm@52244
   178
      (Library.split_list (map (apsnd export_solution o fix_alls ctxt 1) subgoals))
wenzelm@52244
   179
  end;
wenzelm@23171
   180
wenzelm@23171
   181
end;