# HG changeset patch # User wenzelm # Date 1369926613 -7200 # Node ID cb15da7bd550dd0bf2857cd48f9558ebd91b657e # Parent 92bafa4235fa15e527a2ce7b01937c3fd8dd8fa7 misc tuning; diff -r 92bafa4235fa -r cb15da7bd550 src/Tools/IsaPlanner/isand.ML --- 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;