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