src/Tools/IsaPlanner/isand.ML
changeset 52244 cb15da7bd550
parent 52242 2d634bfa1bbf
child 52245 f76fb8858e0b
     1.1 --- a/src/Tools/IsaPlanner/isand.ML	Thu May 30 17:02:09 2013 +0200
     1.2 +++ b/src/Tools/IsaPlanner/isand.ML	Thu May 30 17:10:13 2013 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Tools/IsaPlanner/isand.ML
     1.5      Author:     Lucas Dixon, University of Edinburgh
     1.6  
     1.7 -Natural Deduction tools.
     1.8 +Natural Deduction tools (obsolete).
     1.9  
    1.10  For working with Isabelle theorems in a natural detuction style.
    1.11  ie, not having to deal with meta level quantified varaibles,
    1.12 @@ -24,17 +24,17 @@
    1.13  signature ISA_ND =
    1.14  sig
    1.15    (* inserting meta level params for frees in the conditions *)
    1.16 -  val allify_conditions : (term -> cterm) -> (string * typ) list -> thm -> thm * cterm list
    1.17 +  val allify_conditions: (term -> cterm) -> (string * typ) list -> thm -> thm * cterm list
    1.18  
    1.19 -  val variant_names : Proof.context -> term list -> string list -> string list
    1.20 +  val variant_names: Proof.context -> term list -> string list -> string list
    1.21  
    1.22    (* meta level fixed params (i.e. !! vars) *)
    1.23 -  val fix_alls_term : Proof.context -> int -> term -> term * term list
    1.24 +  val fix_alls_term: Proof.context -> int -> term -> term * term list
    1.25  
    1.26 -  val unfix_frees : cterm list -> thm -> thm
    1.27 +  val unfix_frees: cterm list -> thm -> thm
    1.28  
    1.29    (* assumptions/subgoals *)
    1.30 -  val fixed_subgoal_thms : Proof.context -> thm -> thm list * (thm list -> thm)
    1.31 +  val fixed_subgoal_thms: Proof.context -> thm -> thm list * (thm list -> thm)
    1.32  end
    1.33  
    1.34  structure IsaND : ISA_ND =
    1.35 @@ -50,40 +50,39 @@
    1.36  Results in: "B vs" [!!x. A x]
    1.37  *)
    1.38  fun allify_conditions ctermify Ts th =
    1.39 -    let
    1.40 -      val premts = Thm.prems_of th;
    1.41 +  let
    1.42 +    val premts = Thm.prems_of th;
    1.43  
    1.44 -      fun allify_prem_var (vt as (n,ty)) t =
    1.45 -          (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
    1.46 +    fun allify_prem_var (vt as (n, ty)) t =
    1.47 +      Logic.all_const ty $ Abs (n, ty, Term.abstract_over (Free vt, t))
    1.48  
    1.49 -      val allify_prem = fold_rev allify_prem_var
    1.50 +    val allify_prem = fold_rev allify_prem_var
    1.51  
    1.52 -      val cTs = map (ctermify o Free) Ts
    1.53 -      val cterm_asms = map (ctermify o allify_prem Ts) premts
    1.54 -      val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms
    1.55 -    in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end;
    1.56 +    val cTs = map (ctermify o Free) Ts
    1.57 +    val cterm_asms = map (ctermify o allify_prem Ts) premts
    1.58 +    val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms
    1.59 +  in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end;
    1.60  
    1.61  (* make free vars into schematic vars with index zero *)
    1.62  fun unfix_frees frees =
    1.63 -     fold (K (Thm.forall_elim_var 0)) frees
    1.64 -     o Drule.forall_intr_list frees;
    1.65 +   fold (K (Thm.forall_elim_var 0)) frees o Drule.forall_intr_list frees;
    1.66  
    1.67  (* datatype to capture an exported result, ie a fix or assume. *)
    1.68  datatype export =
    1.69 -         export of {fixes : Thm.cterm list, (* fixed vars *)
    1.70 -                    assumes : Thm.cterm list, (* hidden hyps/assumed prems *)
    1.71 -                    sgid : int,
    1.72 -                    gth :  Thm.thm}; (* subgoal/goalthm *)
    1.73 +  Export of
    1.74 +   {fixes : Thm.cterm list, (* fixed vars *)
    1.75 +    assumes : Thm.cterm list, (* hidden hyps/assumed prems *)
    1.76 +    sgid : int,
    1.77 +    gth :  Thm.thm}; (* subgoal/goalthm *)
    1.78  
    1.79  (* exporting function that takes a solution to the fixed/assumed goal,
    1.80  and uses this to solve the subgoal in the main theorem *)
    1.81 -fun export_solution (export {fixes = cfvs, assumes = hcprems,
    1.82 -                             sgid = i, gth = gth}) solth =
    1.83 -    let
    1.84 -      val solth' =
    1.85 -          solth |> Drule.implies_intr_list hcprems
    1.86 -                |> Drule.forall_intr_list cfvs
    1.87 -    in Drule.compose_single (solth', i, gth) end;
    1.88 +fun export_solution (Export {fixes = cfvs, assumes = hcprems, sgid = i, gth = gth}) solth =
    1.89 +  let
    1.90 +    val solth' = solth
    1.91 +      |> Drule.implies_intr_list hcprems
    1.92 +      |> Drule.forall_intr_list cfvs;
    1.93 +  in Drule.compose_single (solth', i, gth) end;
    1.94  
    1.95  fun variant_names ctxt ts xs =
    1.96    let
    1.97 @@ -114,23 +113,21 @@
    1.98       ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
    1.99  *)
   1.100  fun fix_alls_term ctxt i t =
   1.101 -    let
   1.102 -      val gt = Logic.get_goal t i;
   1.103 -      val body = Term.strip_all_body gt;
   1.104 -      val alls = rev (Term.strip_all_vars gt);
   1.105 -      val xs = variant_names ctxt [t] (map fst alls);
   1.106 -      val fvs = map Free (xs ~~ map snd alls);
   1.107 -    in ((subst_bounds (fvs,body)), fvs) end;
   1.108 +  let
   1.109 +    val gt = Logic.get_goal t i;
   1.110 +    val body = Term.strip_all_body gt;
   1.111 +    val alls = rev (Term.strip_all_vars gt);
   1.112 +    val xs = variant_names ctxt [t] (map fst alls);
   1.113 +    val fvs = map Free (xs ~~ map snd alls);
   1.114 +  in ((subst_bounds (fvs,body)), fvs) end;
   1.115  
   1.116  fun fix_alls_cterm ctxt i th =
   1.117 -    let
   1.118 -      val ctermify = Thm.cterm_of (Thm.theory_of_thm th);
   1.119 -      val (fixedbody, fvs) = fix_alls_term ctxt i (Thm.prop_of th);
   1.120 -      val cfvs = rev (map ctermify fvs);
   1.121 -      val ct_body = ctermify fixedbody
   1.122 -    in
   1.123 -      (ct_body, cfvs)
   1.124 -    end;
   1.125 +  let
   1.126 +    val cert = Thm.cterm_of (Thm.theory_of_thm th);
   1.127 +    val (fixedbody, fvs) = fix_alls_term ctxt i (Thm.prop_of th);
   1.128 +    val cfvs = rev (map cert fvs);
   1.129 +    val ct_body = cert fixedbody;
   1.130 +  in (ct_body, cfvs) end;
   1.131  
   1.132  fun fix_alls' ctxt i = apfst Thm.trivial o fix_alls_cterm ctxt i;
   1.133  
   1.134 @@ -139,14 +136,11 @@
   1.135  (* note the export goal is rotated by (i - 1) and will have to be
   1.136  unrotated to get backto the originial position(s) *)
   1.137  fun hide_other_goals th =
   1.138 -    let
   1.139 -      (* tl beacuse fst sg is the goal we are interested in *)
   1.140 -      val cprems = tl (Drule.cprems_of th)
   1.141 -      val aprems = map Thm.assume cprems
   1.142 -    in
   1.143 -      (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems,
   1.144 -       cprems)
   1.145 -    end;
   1.146 +  let
   1.147 +    (* tl beacuse fst sg is the goal we are interested in *)
   1.148 +    val cprems = tl (Drule.cprems_of th);
   1.149 +    val aprems = map Thm.assume cprems;
   1.150 +  in (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, cprems) end;
   1.151  
   1.152  (* a nicer version of the above that leaves only a single subgoal (the
   1.153  other subgoals are hidden hyps, that the exporter suffles about)
   1.154 @@ -160,14 +154,10 @@
   1.155       ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
   1.156  *)
   1.157  fun fix_alls ctxt i th =
   1.158 -    let
   1.159 -      val (fixed_gth, fixedvars) = fix_alls' ctxt i th
   1.160 -      val (sml_gth, othergoals) = hide_other_goals fixed_gth
   1.161 -    in
   1.162 -      (sml_gth, export {fixes = fixedvars,
   1.163 -                        assumes = othergoals,
   1.164 -                        sgid = i, gth = th})
   1.165 -    end;
   1.166 +  let
   1.167 +    val (fixed_gth, fixedvars) = fix_alls' ctxt i th
   1.168 +    val (sml_gth, othergoals) = hide_other_goals fixed_gth
   1.169 +  in (sml_gth, Export {fixes = fixedvars, assumes = othergoals, sgid = i, gth = th}) end;
   1.170  
   1.171  
   1.172  (* Fixme: allow different order of subgoals given to expf *)
   1.173 @@ -181,21 +171,16 @@
   1.174     "G" : thm)
   1.175  *)
   1.176  fun subgoal_thms th =
   1.177 -    let
   1.178 -      val t = (prop_of th);
   1.179 +  let
   1.180 +    val cert = Thm.cterm_of (Thm.theory_of_thm th);
   1.181  
   1.182 -      val prems = Logic.strip_imp_prems t;
   1.183 -
   1.184 -      val sgn = Thm.theory_of_thm th;
   1.185 -      val ctermify = Thm.cterm_of sgn;
   1.186 +    val t = prop_of th;
   1.187  
   1.188 -      val aprems = map (Thm.trivial o ctermify) prems;
   1.189 +    val prems = Logic.strip_imp_prems t;
   1.190 +    val aprems = map (Thm.trivial o cert) prems;
   1.191  
   1.192 -      fun explortf premths =
   1.193 -          Drule.implies_elim_list th premths
   1.194 -    in
   1.195 -      (aprems, explortf)
   1.196 -    end;
   1.197 +    fun explortf premths = Drule.implies_elim_list th premths;
   1.198 +  in (aprems, explortf) end;
   1.199  
   1.200  
   1.201  (* Fixme: allow different order of subgoals in exportf *)
   1.202 @@ -214,15 +199,15 @@
   1.203  *)
   1.204  (* requires being given solutions! *)
   1.205  fun fixed_subgoal_thms ctxt th =
   1.206 -    let
   1.207 -      val (subgoals, expf) = subgoal_thms th;
   1.208 -(*       fun export_sg (th, exp) = exp th; *)
   1.209 -      fun export_sgs expfs solthms =
   1.210 -          expf (map2 (curry (op |>)) solthms expfs);
   1.211 -(*           expf (map export_sg (ths ~~ expfs)); *)
   1.212 -    in
   1.213 -      apsnd export_sgs (Library.split_list (map (apsnd export_solution o
   1.214 -                                                 fix_alls ctxt 1) subgoals))
   1.215 -    end;
   1.216 +  let
   1.217 +    val (subgoals, expf) = subgoal_thms th;
   1.218 +(*  fun export_sg (th, exp) = exp th; *)
   1.219 +    fun export_sgs expfs solthms =
   1.220 +      expf (map2 (curry (op |>)) solthms expfs);
   1.221 +(*    expf (map export_sg (ths ~~ expfs)); *)
   1.222 +  in
   1.223 +    apsnd export_sgs
   1.224 +      (Library.split_list (map (apsnd export_solution o fix_alls ctxt 1) subgoals))
   1.225 +  end;
   1.226  
   1.227  end;