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