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