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;
```