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