src/Tools/IsaPlanner/isand.ML
author wenzelm
Wed Sep 12 23:18:26 2012 +0200 (2012-09-12)
changeset 49340 25fc6e0da459
parent 49339 d1fcb4de8349
child 52242 2d634bfa1bbf
permissions -rw-r--r--
observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
     1 (*  Title:      Tools/IsaPlanner/isand.ML
     2     Author:     Lucas Dixon, University of Edinburgh
     3 
     4 Natural Deduction tools.
     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   (* inserting meta level params for frees in the conditions *)
    27   val allify_conditions : (term -> cterm) -> (string * typ) list -> thm -> thm * cterm list
    28 
    29   val variant_names : Proof.context -> term list -> string list -> string list
    30 
    31   (* meta level fixed params (i.e. !! vars) *)
    32   val fix_alls_term : Proof.context -> int -> term -> term * term list
    33 
    34   val unfix_frees : cterm list -> thm -> thm
    35 
    36   (* assumptions/subgoals *)
    37   val fixed_subgoal_thms : Proof.context -> thm -> thm list * (thm list -> thm)
    38 end
    39 
    40 structure IsaND : ISA_ND =
    41 struct
    42 
    43 (* Given ctertmify function, (string,type) pairs capturing the free
    44 vars that need to be allified in the assumption, and a theorem with
    45 assumptions possibly containing the free vars, then we give back the
    46 assumptions allified as hidden hyps.
    47 
    48 Given: x
    49 th: A vs ==> B vs
    50 Results in: "B vs" [!!x. A x]
    51 *)
    52 fun allify_conditions ctermify Ts th =
    53     let
    54       val premts = Thm.prems_of th;
    55 
    56       fun allify_prem_var (vt as (n,ty),t)  =
    57           (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
    58 
    59       fun allify_prem Ts p = List.foldr allify_prem_var p Ts
    60 
    61       val cTs = map (ctermify o Free) Ts
    62       val cterm_asms = map (ctermify o allify_prem Ts) premts
    63       val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms
    64     in
    65       (Library.foldl (fn (x,y) => y COMP x) (th, allifyied_asm_thms), cterm_asms)
    66     end;
    67 
    68 (* make free vars into schematic vars with index zero *)
    69 fun unfix_frees frees =
    70      fold (K (Thm.forall_elim_var 0)) frees
    71      o Drule.forall_intr_list frees;
    72 
    73 (* datatype to capture an exported result, ie a fix or assume. *)
    74 datatype export =
    75          export of {fixes : Thm.cterm list, (* fixed vars *)
    76                     assumes : Thm.cterm list, (* hidden hyps/assumed prems *)
    77                     sgid : int,
    78                     gth :  Thm.thm}; (* subgoal/goalthm *)
    79 
    80 (* exporting function that takes a solution to the fixed/assumed goal,
    81 and uses this to solve the subgoal in the main theorem *)
    82 fun export_solution (export {fixes = cfvs, assumes = hcprems,
    83                              sgid = i, gth = gth}) solth =
    84     let
    85       val solth' =
    86           solth |> Drule.implies_intr_list hcprems
    87                 |> Drule.forall_intr_list cfvs
    88     in Drule.compose_single (solth', i, gth) end;
    89 
    90 fun variant_names ctxt ts xs =
    91   let
    92     val names =
    93       Variable.names_of ctxt
    94       |> (fold o fold_aterms)
    95           (fn Var ((a, _), _) => Name.declare a
    96             | Free (a, _) => Name.declare a
    97             | _ => I) ts;
    98   in fst (fold_map Name.variant xs names) end;
    99 
   100 (* fix parameters of a subgoal "i", as free variables, and create an
   101 exporting function that will use the result of this proved goal to
   102 show the goal in the original theorem.
   103 
   104 Note, an advantage of this over Isar is that it supports instantiation
   105 of unkowns in the earlier theorem, ie we can do instantiation of meta
   106 vars!
   107 
   108 avoids constant, free and vars names.
   109 
   110 loosely corresponds to:
   111 Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
   112 Result:
   113   ("(As ==> SGi x') ==> (As ==> SGi x')" : thm,
   114    expf :
   115      ("As ==> SGi x'" : thm) ->
   116      ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
   117 *)
   118 fun fix_alls_term ctxt i t =
   119     let
   120       val gt = Logic.get_goal t i;
   121       val body = Term.strip_all_body gt;
   122       val alls = rev (Term.strip_all_vars gt);
   123       val xs = variant_names ctxt [t] (map fst alls);
   124       val fvs = map Free (xs ~~ map snd alls);
   125     in ((subst_bounds (fvs,body)), fvs) end;
   126 
   127 fun fix_alls_cterm ctxt i th =
   128     let
   129       val ctermify = Thm.cterm_of (Thm.theory_of_thm th);
   130       val (fixedbody, fvs) = fix_alls_term ctxt i (Thm.prop_of th);
   131       val cfvs = rev (map ctermify fvs);
   132       val ct_body = ctermify fixedbody
   133     in
   134       (ct_body, cfvs)
   135     end;
   136 
   137 fun fix_alls' ctxt i = apfst Thm.trivial o fix_alls_cterm ctxt i;
   138 
   139 
   140 (* hide other goals *)
   141 (* note the export goal is rotated by (i - 1) and will have to be
   142 unrotated to get backto the originial position(s) *)
   143 fun hide_other_goals th =
   144     let
   145       (* tl beacuse fst sg is the goal we are interested in *)
   146       val cprems = tl (Drule.cprems_of th)
   147       val aprems = map Thm.assume cprems
   148     in
   149       (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems,
   150        cprems)
   151     end;
   152 
   153 (* a nicer version of the above that leaves only a single subgoal (the
   154 other subgoals are hidden hyps, that the exporter suffles about)
   155 namely the subgoal that we were trying to solve. *)
   156 (* loosely corresponds to:
   157 Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
   158 Result:
   159   ("(As ==> SGi x') ==> SGi x'" : thm,
   160    expf :
   161      ("SGi x'" : thm) ->
   162      ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
   163 *)
   164 fun fix_alls ctxt i th =
   165     let
   166       val (fixed_gth, fixedvars) = fix_alls' ctxt i th
   167       val (sml_gth, othergoals) = hide_other_goals fixed_gth
   168     in
   169       (sml_gth, export {fixes = fixedvars,
   170                         assumes = othergoals,
   171                         sgid = i, gth = th})
   172     end;
   173 
   174 
   175 (* Fixme: allow different order of subgoals given to expf *)
   176 (* make each subgoal into a separate thm that needs to be proved *)
   177 (* loosely corresponds to:
   178 Given
   179   "[| SG0; ... SGm |] ==> G" : thm
   180 Result:
   181 (["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals
   182  ["SG0", ..., "SGm"] : thm list ->   -- export function
   183    "G" : thm)
   184 *)
   185 fun subgoal_thms th =
   186     let
   187       val t = (prop_of th);
   188 
   189       val prems = Logic.strip_imp_prems t;
   190 
   191       val sgn = Thm.theory_of_thm th;
   192       val ctermify = Thm.cterm_of sgn;
   193 
   194       val aprems = map (Thm.trivial o ctermify) prems;
   195 
   196       fun explortf premths =
   197           Drule.implies_elim_list th premths
   198     in
   199       (aprems, explortf)
   200     end;
   201 
   202 
   203 (* Fixme: allow different order of subgoals in exportf *)
   204 (* as above, but also fix all parameters in all subgoals, and uses
   205 fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent
   206 subgoals. *)
   207 (* loosely corresponds to:
   208 Given
   209   "[| !! x0s. A0s x0s ==> SG0 x0s;
   210       ...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm
   211 Result:
   212 (["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'",
   213   ... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals
   214  ["SG0 x0s'", ..., "SGm xms'"] : thm list ->   -- export function
   215    "G" : thm)
   216 *)
   217 (* requires being given solutions! *)
   218 fun fixed_subgoal_thms ctxt th =
   219     let
   220       val (subgoals, expf) = subgoal_thms th;
   221 (*       fun export_sg (th, exp) = exp th; *)
   222       fun export_sgs expfs solthms =
   223           expf (map2 (curry (op |>)) solthms expfs);
   224 (*           expf (map export_sg (ths ~~ expfs)); *)
   225     in
   226       apsnd export_sgs (Library.split_list (map (apsnd export_solution o
   227                                                  fix_alls ctxt 1) subgoals))
   228     end;
   229 
   230 end;