src/Tools/IsaPlanner/isand.ML
author wenzelm
Thu May 30 17:10:13 2013 +0200 (2013-05-30)
changeset 52244 cb15da7bd550
parent 52242 2d634bfa1bbf
child 52245 f76fb8858e0b
permissions -rw-r--r--
misc tuning;
     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   (* 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     val allify_prem = fold_rev allify_prem_var
    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 (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) 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 o Drule.forall_intr_list frees;
    69 
    70 (* datatype to capture an exported result, ie a fix or assume. *)
    71 datatype export =
    72   Export of
    73    {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, sgid = i, gth = gth}) solth =
    81   let
    82     val solth' = solth
    83       |> Drule.implies_intr_list hcprems
    84       |> Drule.forall_intr_list cfvs;
    85   in Drule.compose_single (solth', i, gth) end;
    86 
    87 fun variant_names ctxt ts xs =
    88   let
    89     val names =
    90       Variable.names_of ctxt
    91       |> (fold o fold_aterms)
    92           (fn Var ((a, _), _) => Name.declare a
    93             | Free (a, _) => Name.declare a
    94             | _ => I) ts;
    95   in fst (fold_map Name.variant xs names) end;
    96 
    97 (* fix parameters of a subgoal "i", as free variables, and create an
    98 exporting function that will use the result of this proved goal to
    99 show the goal in the original theorem.
   100 
   101 Note, an advantage of this over Isar is that it supports instantiation
   102 of unkowns in the earlier theorem, ie we can do instantiation of meta
   103 vars!
   104 
   105 avoids constant, free and vars names.
   106 
   107 loosely corresponds to:
   108 Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
   109 Result:
   110   ("(As ==> SGi x') ==> (As ==> SGi x')" : thm,
   111    expf :
   112      ("As ==> SGi x'" : thm) ->
   113      ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
   114 *)
   115 fun fix_alls_term ctxt i t =
   116   let
   117     val gt = Logic.get_goal t i;
   118     val body = Term.strip_all_body gt;
   119     val alls = rev (Term.strip_all_vars gt);
   120     val xs = variant_names ctxt [t] (map fst alls);
   121     val fvs = map Free (xs ~~ map snd alls);
   122   in ((subst_bounds (fvs,body)), fvs) end;
   123 
   124 fun fix_alls_cterm ctxt i th =
   125   let
   126     val cert = Thm.cterm_of (Thm.theory_of_thm th);
   127     val (fixedbody, fvs) = fix_alls_term ctxt i (Thm.prop_of th);
   128     val cfvs = rev (map cert fvs);
   129     val ct_body = cert fixedbody;
   130   in (ct_body, cfvs) end;
   131 
   132 fun fix_alls' ctxt i = apfst Thm.trivial o fix_alls_cterm ctxt i;
   133 
   134 
   135 (* hide other goals *)
   136 (* note the export goal is rotated by (i - 1) and will have to be
   137 unrotated to get backto the originial position(s) *)
   138 fun hide_other_goals th =
   139   let
   140     (* tl beacuse fst sg is the goal we are interested in *)
   141     val cprems = tl (Drule.cprems_of th);
   142     val aprems = map Thm.assume cprems;
   143   in (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, cprems) end;
   144 
   145 (* a nicer version of the above that leaves only a single subgoal (the
   146 other subgoals are hidden hyps, that the exporter suffles about)
   147 namely the subgoal that we were trying to solve. *)
   148 (* loosely corresponds to:
   149 Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
   150 Result:
   151   ("(As ==> SGi x') ==> SGi x'" : thm,
   152    expf :
   153      ("SGi x'" : thm) ->
   154      ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
   155 *)
   156 fun fix_alls ctxt i th =
   157   let
   158     val (fixed_gth, fixedvars) = fix_alls' ctxt i th
   159     val (sml_gth, othergoals) = hide_other_goals fixed_gth
   160   in (sml_gth, Export {fixes = fixedvars, assumes = othergoals, sgid = i, gth = th}) end;
   161 
   162 
   163 (* Fixme: allow different order of subgoals given to expf *)
   164 (* make each subgoal into a separate thm that needs to be proved *)
   165 (* loosely corresponds to:
   166 Given
   167   "[| SG0; ... SGm |] ==> G" : thm
   168 Result:
   169 (["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals
   170  ["SG0", ..., "SGm"] : thm list ->   -- export function
   171    "G" : thm)
   172 *)
   173 fun subgoal_thms th =
   174   let
   175     val cert = Thm.cterm_of (Thm.theory_of_thm th);
   176 
   177     val t = prop_of th;
   178 
   179     val prems = Logic.strip_imp_prems t;
   180     val aprems = map (Thm.trivial o cert) prems;
   181 
   182     fun explortf premths = Drule.implies_elim_list th premths;
   183   in (aprems, explortf) end;
   184 
   185 
   186 (* Fixme: allow different order of subgoals in exportf *)
   187 (* as above, but also fix all parameters in all subgoals, and uses
   188 fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent
   189 subgoals. *)
   190 (* loosely corresponds to:
   191 Given
   192   "[| !! x0s. A0s x0s ==> SG0 x0s;
   193       ...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm
   194 Result:
   195 (["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'",
   196   ... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals
   197  ["SG0 x0s'", ..., "SGm xms'"] : thm list ->   -- export function
   198    "G" : thm)
   199 *)
   200 (* requires being given solutions! *)
   201 fun fixed_subgoal_thms ctxt th =
   202   let
   203     val (subgoals, expf) = subgoal_thms th;
   204 (*  fun export_sg (th, exp) = exp th; *)
   205     fun export_sgs expfs solthms =
   206       expf (map2 (curry (op |>)) solthms expfs);
   207 (*    expf (map export_sg (ths ~~ expfs)); *)
   208   in
   209     apsnd export_sgs
   210       (Library.split_list (map (apsnd export_solution o fix_alls ctxt 1) subgoals))
   211   end;
   212 
   213 end;