--- a/src/Tools/IsaPlanner/isand.ML Thu May 30 17:02:09 2013 +0200
+++ b/src/Tools/IsaPlanner/isand.ML Thu May 30 17:10:13 2013 +0200
@@ -1,7 +1,7 @@
(* Title: Tools/IsaPlanner/isand.ML
Author: Lucas Dixon, University of Edinburgh
-Natural Deduction tools.
+Natural Deduction tools (obsolete).
For working with Isabelle theorems in a natural detuction style.
ie, not having to deal with meta level quantified varaibles,
@@ -24,17 +24,17 @@
signature ISA_ND =
sig
(* inserting meta level params for frees in the conditions *)
- val allify_conditions : (term -> cterm) -> (string * typ) list -> thm -> thm * cterm list
+ val allify_conditions: (term -> cterm) -> (string * typ) list -> thm -> thm * cterm list
- val variant_names : Proof.context -> term list -> string list -> string list
+ val variant_names: Proof.context -> term list -> string list -> string list
(* meta level fixed params (i.e. !! vars) *)
- val fix_alls_term : Proof.context -> int -> term -> term * term list
+ val fix_alls_term: Proof.context -> int -> term -> term * term list
- val unfix_frees : cterm list -> thm -> thm
+ val unfix_frees: cterm list -> thm -> thm
(* assumptions/subgoals *)
- val fixed_subgoal_thms : Proof.context -> thm -> thm list * (thm list -> thm)
+ val fixed_subgoal_thms: Proof.context -> thm -> thm list * (thm list -> thm)
end
structure IsaND : ISA_ND =
@@ -50,40 +50,39 @@
Results in: "B vs" [!!x. A x]
*)
fun allify_conditions ctermify Ts th =
- let
- val premts = Thm.prems_of th;
+ let
+ val premts = Thm.prems_of th;
- fun allify_prem_var (vt as (n,ty)) t =
- (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
+ fun allify_prem_var (vt as (n, ty)) t =
+ Logic.all_const ty $ Abs (n, ty, Term.abstract_over (Free vt, t))
- val allify_prem = fold_rev allify_prem_var
+ val allify_prem = fold_rev allify_prem_var
- val cTs = map (ctermify o Free) Ts
- val cterm_asms = map (ctermify o allify_prem Ts) premts
- val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms
- in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end;
+ val cTs = map (ctermify o Free) Ts
+ val cterm_asms = map (ctermify o allify_prem Ts) premts
+ val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms
+ in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end;
(* make free vars into schematic vars with index zero *)
fun unfix_frees frees =
- fold (K (Thm.forall_elim_var 0)) frees
- o Drule.forall_intr_list frees;
+ fold (K (Thm.forall_elim_var 0)) frees o Drule.forall_intr_list frees;
(* datatype to capture an exported result, ie a fix or assume. *)
datatype export =
- export of {fixes : Thm.cterm list, (* fixed vars *)
- assumes : Thm.cterm list, (* hidden hyps/assumed prems *)
- sgid : int,
- gth : Thm.thm}; (* subgoal/goalthm *)
+ Export of
+ {fixes : Thm.cterm list, (* fixed vars *)
+ assumes : Thm.cterm list, (* hidden hyps/assumed prems *)
+ sgid : int,
+ gth : Thm.thm}; (* subgoal/goalthm *)
(* exporting function that takes a solution to the fixed/assumed goal,
and uses this to solve the subgoal in the main theorem *)
-fun export_solution (export {fixes = cfvs, assumes = hcprems,
- sgid = i, gth = gth}) solth =
- let
- val solth' =
- solth |> Drule.implies_intr_list hcprems
- |> Drule.forall_intr_list cfvs
- in Drule.compose_single (solth', i, gth) end;
+fun export_solution (Export {fixes = cfvs, assumes = hcprems, sgid = i, gth = gth}) solth =
+ let
+ val solth' = solth
+ |> Drule.implies_intr_list hcprems
+ |> Drule.forall_intr_list cfvs;
+ in Drule.compose_single (solth', i, gth) end;
fun variant_names ctxt ts xs =
let
@@ -114,23 +113,21 @@
("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
*)
fun fix_alls_term ctxt i t =
- let
- val gt = Logic.get_goal t i;
- val body = Term.strip_all_body gt;
- val alls = rev (Term.strip_all_vars gt);
- val xs = variant_names ctxt [t] (map fst alls);
- val fvs = map Free (xs ~~ map snd alls);
- in ((subst_bounds (fvs,body)), fvs) end;
+ let
+ val gt = Logic.get_goal t i;
+ val body = Term.strip_all_body gt;
+ val alls = rev (Term.strip_all_vars gt);
+ val xs = variant_names ctxt [t] (map fst alls);
+ val fvs = map Free (xs ~~ map snd alls);
+ in ((subst_bounds (fvs,body)), fvs) end;
fun fix_alls_cterm ctxt i th =
- let
- val ctermify = Thm.cterm_of (Thm.theory_of_thm th);
- val (fixedbody, fvs) = fix_alls_term ctxt i (Thm.prop_of th);
- val cfvs = rev (map ctermify fvs);
- val ct_body = ctermify fixedbody
- in
- (ct_body, cfvs)
- end;
+ let
+ val cert = Thm.cterm_of (Thm.theory_of_thm th);
+ val (fixedbody, fvs) = fix_alls_term ctxt i (Thm.prop_of th);
+ val cfvs = rev (map cert fvs);
+ val ct_body = cert fixedbody;
+ in (ct_body, cfvs) end;
fun fix_alls' ctxt i = apfst Thm.trivial o fix_alls_cterm ctxt i;
@@ -139,14 +136,11 @@
(* note the export goal is rotated by (i - 1) and will have to be
unrotated to get backto the originial position(s) *)
fun hide_other_goals th =
- let
- (* tl beacuse fst sg is the goal we are interested in *)
- val cprems = tl (Drule.cprems_of th)
- val aprems = map Thm.assume cprems
- in
- (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems,
- cprems)
- end;
+ let
+ (* tl beacuse fst sg is the goal we are interested in *)
+ val cprems = tl (Drule.cprems_of th);
+ val aprems = map Thm.assume cprems;
+ in (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, cprems) end;
(* a nicer version of the above that leaves only a single subgoal (the
other subgoals are hidden hyps, that the exporter suffles about)
@@ -160,14 +154,10 @@
("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
*)
fun fix_alls ctxt i th =
- let
- val (fixed_gth, fixedvars) = fix_alls' ctxt i th
- val (sml_gth, othergoals) = hide_other_goals fixed_gth
- in
- (sml_gth, export {fixes = fixedvars,
- assumes = othergoals,
- sgid = i, gth = th})
- end;
+ let
+ val (fixed_gth, fixedvars) = fix_alls' ctxt i th
+ val (sml_gth, othergoals) = hide_other_goals fixed_gth
+ in (sml_gth, Export {fixes = fixedvars, assumes = othergoals, sgid = i, gth = th}) end;
(* Fixme: allow different order of subgoals given to expf *)
@@ -181,21 +171,16 @@
"G" : thm)
*)
fun subgoal_thms th =
- let
- val t = (prop_of th);
+ let
+ val cert = Thm.cterm_of (Thm.theory_of_thm th);
- val prems = Logic.strip_imp_prems t;
-
- val sgn = Thm.theory_of_thm th;
- val ctermify = Thm.cterm_of sgn;
+ val t = prop_of th;
- val aprems = map (Thm.trivial o ctermify) prems;
+ val prems = Logic.strip_imp_prems t;
+ val aprems = map (Thm.trivial o cert) prems;
- fun explortf premths =
- Drule.implies_elim_list th premths
- in
- (aprems, explortf)
- end;
+ fun explortf premths = Drule.implies_elim_list th premths;
+ in (aprems, explortf) end;
(* Fixme: allow different order of subgoals in exportf *)
@@ -214,15 +199,15 @@
*)
(* requires being given solutions! *)
fun fixed_subgoal_thms ctxt th =
- let
- val (subgoals, expf) = subgoal_thms th;
-(* fun export_sg (th, exp) = exp th; *)
- fun export_sgs expfs solthms =
- expf (map2 (curry (op |>)) solthms expfs);
-(* expf (map export_sg (ths ~~ expfs)); *)
- in
- apsnd export_sgs (Library.split_list (map (apsnd export_solution o
- fix_alls ctxt 1) subgoals))
- end;
+ let
+ val (subgoals, expf) = subgoal_thms th;
+(* fun export_sg (th, exp) = exp th; *)
+ fun export_sgs expfs solthms =
+ expf (map2 (curry (op |>)) solthms expfs);
+(* expf (map export_sg (ths ~~ expfs)); *)
+ in
+ apsnd export_sgs
+ (Library.split_list (map (apsnd export_solution o fix_alls ctxt 1) subgoals))
+ end;
end;