src/Tools/IsaPlanner/isand.ML
 author wenzelm Thu May 30 16:53:32 2013 +0200 (2013-05-30) changeset 52242 2d634bfa1bbf parent 49340 25fc6e0da459 child 52244 cb15da7bd550 permissions -rw-r--r--
more standard fold/fold_rev;
 wenzelm@23175 ` 1` ```(* Title: Tools/IsaPlanner/isand.ML ``` wenzelm@23171 ` 2` ``` Author: Lucas Dixon, University of Edinburgh ``` wenzelm@23175 ` 3` wenzelm@23175 ` 4` ```Natural Deduction tools. ``` wenzelm@23171 ` 5` wenzelm@23175 ` 6` ```For working with Isabelle theorems in a natural detuction style. ``` wenzelm@23175 ` 7` ```ie, not having to deal with meta level quantified varaibles, ``` wenzelm@23175 ` 8` ```instead, we work with newly introduced frees, and hide the ``` wenzelm@23175 ` 9` ```"all"'s, exporting results from theorems proved with the frees, to ``` wenzelm@23175 ` 10` ```solve the all cases of the previous goal. This allows resolution ``` wenzelm@49339 ` 11` ```to do proof search normally. ``` wenzelm@23171 ` 12` wenzelm@23175 ` 13` ```Note: A nice idea: allow exporting to solve any subgoal, thus ``` wenzelm@23175 ` 14` ```allowing the interleaving of proof, or provide a structure for the ``` wenzelm@23175 ` 15` ```ordering of proof, thus allowing proof attempts in parrell, but ``` wenzelm@23175 ` 16` ```recording the order to apply things in. ``` wenzelm@23171 ` 17` wenzelm@23175 ` 18` ```THINK: are we really ok with our varify name w.r.t the prop - do ``` wenzelm@23175 ` 19` ```we also need to avoid names in the hidden hyps? What about ``` wenzelm@23175 ` 20` ```unification contraints in flex-flex pairs - might they also have ``` wenzelm@23175 ` 21` ```extra free vars? ``` wenzelm@23171 ` 22` ```*) ``` wenzelm@23171 ` 23` wenzelm@23171 ` 24` ```signature ISA_ND = ``` wenzelm@23171 ` 25` ```sig ``` wenzelm@23171 ` 26` ``` (* inserting meta level params for frees in the conditions *) ``` wenzelm@49339 ` 27` ``` val allify_conditions : (term -> cterm) -> (string * typ) list -> thm -> thm * cterm list ``` wenzelm@23171 ` 28` wenzelm@49340 ` 29` ``` val variant_names : Proof.context -> term list -> string list -> string list ``` wenzelm@49340 ` 30` wenzelm@23171 ` 31` ``` (* meta level fixed params (i.e. !! vars) *) ``` wenzelm@49340 ` 32` ``` val fix_alls_term : Proof.context -> int -> term -> term * term list ``` wenzelm@23171 ` 33` wenzelm@49339 ` 34` ``` val unfix_frees : cterm list -> thm -> thm ``` wenzelm@23171 ` 35` wenzelm@23171 ` 36` ``` (* assumptions/subgoals *) ``` wenzelm@49340 ` 37` ``` val fixed_subgoal_thms : Proof.context -> thm -> thm list * (thm list -> thm) ``` wenzelm@23171 ` 38` ```end ``` wenzelm@23171 ` 39` wenzelm@49339 ` 40` ```structure IsaND : ISA_ND = ``` wenzelm@49339 ` 41` ```struct ``` wenzelm@23171 ` 42` wenzelm@23171 ` 43` ```(* Given ctertmify function, (string,type) pairs capturing the free ``` wenzelm@23171 ` 44` ```vars that need to be allified in the assumption, and a theorem with ``` wenzelm@23171 ` 45` ```assumptions possibly containing the free vars, then we give back the ``` wenzelm@49339 ` 46` ```assumptions allified as hidden hyps. ``` wenzelm@23171 ` 47` wenzelm@49339 ` 48` ```Given: x ``` wenzelm@49339 ` 49` ```th: A vs ==> B vs ``` wenzelm@23171 ` 50` ```Results in: "B vs" [!!x. A x] ``` wenzelm@23171 ` 51` ```*) ``` wenzelm@49339 ` 52` ```fun allify_conditions ctermify Ts th = ``` wenzelm@49339 ` 53` ``` let ``` wenzelm@23171 ` 54` ``` val premts = Thm.prems_of th; ``` wenzelm@49339 ` 55` wenzelm@52242 ` 56` ``` fun allify_prem_var (vt as (n,ty)) t = ``` wenzelm@46217 ` 57` ``` (Logic.all_const ty) \$ (Abs(n,ty,Term.abstract_over (Free vt, t))) ``` wenzelm@23171 ` 58` wenzelm@52242 ` 59` ``` val allify_prem = fold_rev allify_prem_var ``` wenzelm@23171 ` 60` wenzelm@23171 ` 61` ``` val cTs = map (ctermify o Free) Ts ``` wenzelm@23171 ` 62` ``` val cterm_asms = map (ctermify o allify_prem Ts) premts ``` wenzelm@23171 ` 63` ``` val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms ``` wenzelm@52242 ` 64` ``` in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end; ``` wenzelm@23171 ` 65` wenzelm@23171 ` 66` ```(* make free vars into schematic vars with index zero *) ``` wenzelm@49339 ` 67` ```fun unfix_frees frees = ``` wenzelm@46777 ` 68` ``` fold (K (Thm.forall_elim_var 0)) frees ``` wenzelm@23171 ` 69` ``` o Drule.forall_intr_list frees; ``` wenzelm@23171 ` 70` wenzelm@23171 ` 71` ```(* datatype to capture an exported result, ie a fix or assume. *) ``` wenzelm@49339 ` 72` ```datatype export = ``` wenzelm@23171 ` 73` ``` export of {fixes : Thm.cterm list, (* fixed vars *) ``` wenzelm@23171 ` 74` ``` assumes : Thm.cterm list, (* hidden hyps/assumed prems *) ``` wenzelm@23171 ` 75` ``` sgid : int, ``` wenzelm@23171 ` 76` ``` gth : Thm.thm}; (* subgoal/goalthm *) ``` wenzelm@23171 ` 77` wenzelm@23171 ` 78` ```(* exporting function that takes a solution to the fixed/assumed goal, ``` wenzelm@23171 ` 79` ```and uses this to solve the subgoal in the main theorem *) ``` wenzelm@23171 ` 80` ```fun export_solution (export {fixes = cfvs, assumes = hcprems, ``` wenzelm@49339 ` 81` ``` sgid = i, gth = gth}) solth = ``` wenzelm@49339 ` 82` ``` let ``` wenzelm@49339 ` 83` ``` val solth' = ``` wenzelm@23171 ` 84` ``` solth |> Drule.implies_intr_list hcprems ``` wenzelm@23171 ` 85` ``` |> Drule.forall_intr_list cfvs ``` wenzelm@23171 ` 86` ``` in Drule.compose_single (solth', i, gth) end; ``` wenzelm@23171 ` 87` wenzelm@49340 ` 88` ```fun variant_names ctxt ts xs = ``` wenzelm@49340 ` 89` ``` let ``` wenzelm@49340 ` 90` ``` val names = ``` wenzelm@49340 ` 91` ``` Variable.names_of ctxt ``` wenzelm@49340 ` 92` ``` |> (fold o fold_aterms) ``` wenzelm@49340 ` 93` ``` (fn Var ((a, _), _) => Name.declare a ``` wenzelm@49340 ` 94` ``` | Free (a, _) => Name.declare a ``` wenzelm@49340 ` 95` ``` | _ => I) ts; ``` wenzelm@49340 ` 96` ``` in fst (fold_map Name.variant xs names) end; ``` wenzelm@23171 ` 97` wenzelm@23171 ` 98` ```(* fix parameters of a subgoal "i", as free variables, and create an ``` wenzelm@23171 ` 99` ```exporting function that will use the result of this proved goal to ``` wenzelm@49339 ` 100` ```show the goal in the original theorem. ``` wenzelm@23171 ` 101` wenzelm@23171 ` 102` ```Note, an advantage of this over Isar is that it supports instantiation ``` wenzelm@23171 ` 103` ```of unkowns in the earlier theorem, ie we can do instantiation of meta ``` wenzelm@49339 ` 104` ```vars! ``` wenzelm@23171 ` 105` wenzelm@49339 ` 106` ```avoids constant, free and vars names. ``` wenzelm@23171 ` 107` wenzelm@23171 ` 108` ```loosely corresponds to: ``` wenzelm@23171 ` 109` ```Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm ``` wenzelm@49339 ` 110` ```Result: ``` wenzelm@49339 ` 111` ``` ("(As ==> SGi x') ==> (As ==> SGi x')" : thm, ``` wenzelm@49339 ` 112` ``` expf : ``` wenzelm@49339 ` 113` ``` ("As ==> SGi x'" : thm) -> ``` wenzelm@23171 ` 114` ``` ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm) ``` wenzelm@23171 ` 115` ```*) ``` wenzelm@49340 ` 116` ```fun fix_alls_term ctxt i t = ``` wenzelm@23171 ` 117` ``` let ``` wenzelm@23171 ` 118` ``` val gt = Logic.get_goal t i; ``` wenzelm@23171 ` 119` ``` val body = Term.strip_all_body gt; ``` wenzelm@23171 ` 120` ``` val alls = rev (Term.strip_all_vars gt); ``` wenzelm@49340 ` 121` ``` val xs = variant_names ctxt [t] (map fst alls); ``` wenzelm@49340 ` 122` ``` val fvs = map Free (xs ~~ map snd alls); ``` wenzelm@23171 ` 123` ``` in ((subst_bounds (fvs,body)), fvs) end; ``` wenzelm@23171 ` 124` wenzelm@49340 ` 125` ```fun fix_alls_cterm ctxt i th = ``` wenzelm@23171 ` 126` ``` let ``` wenzelm@23171 ` 127` ``` val ctermify = Thm.cterm_of (Thm.theory_of_thm th); ``` wenzelm@49340 ` 128` ``` val (fixedbody, fvs) = fix_alls_term ctxt i (Thm.prop_of th); ``` wenzelm@23171 ` 129` ``` val cfvs = rev (map ctermify fvs); ``` wenzelm@23171 ` 130` ``` val ct_body = ctermify fixedbody ``` wenzelm@23171 ` 131` ``` in ``` wenzelm@23171 ` 132` ``` (ct_body, cfvs) ``` wenzelm@23171 ` 133` ``` end; ``` wenzelm@23171 ` 134` wenzelm@49340 ` 135` ```fun fix_alls' ctxt i = apfst Thm.trivial o fix_alls_cterm ctxt i; ``` wenzelm@23171 ` 136` wenzelm@23171 ` 137` wenzelm@49339 ` 138` ```(* hide other goals *) ``` wenzelm@23171 ` 139` ```(* note the export goal is rotated by (i - 1) and will have to be ``` wenzelm@23171 ` 140` ```unrotated to get backto the originial position(s) *) ``` wenzelm@49339 ` 141` ```fun hide_other_goals th = ``` wenzelm@23171 ` 142` ``` let ``` wenzelm@23171 ` 143` ``` (* tl beacuse fst sg is the goal we are interested in *) ``` wenzelm@23171 ` 144` ``` val cprems = tl (Drule.cprems_of th) ``` wenzelm@23171 ` 145` ``` val aprems = map Thm.assume cprems ``` wenzelm@23171 ` 146` ``` in ``` wenzelm@49339 ` 147` ``` (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, ``` wenzelm@23171 ` 148` ``` cprems) ``` wenzelm@23171 ` 149` ``` end; ``` wenzelm@23171 ` 150` wenzelm@23171 ` 151` ```(* a nicer version of the above that leaves only a single subgoal (the ``` wenzelm@23171 ` 152` ```other subgoals are hidden hyps, that the exporter suffles about) ``` wenzelm@23171 ` 153` ```namely the subgoal that we were trying to solve. *) ``` wenzelm@23171 ` 154` ```(* loosely corresponds to: ``` wenzelm@23171 ` 155` ```Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm ``` wenzelm@49339 ` 156` ```Result: ``` wenzelm@49339 ` 157` ``` ("(As ==> SGi x') ==> SGi x'" : thm, ``` wenzelm@49339 ` 158` ``` expf : ``` wenzelm@49339 ` 159` ``` ("SGi x'" : thm) -> ``` wenzelm@23171 ` 160` ``` ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm) ``` wenzelm@23171 ` 161` ```*) ``` wenzelm@49340 ` 162` ```fun fix_alls ctxt i th = ``` wenzelm@49339 ` 163` ``` let ``` wenzelm@49340 ` 164` ``` val (fixed_gth, fixedvars) = fix_alls' ctxt i th ``` wenzelm@23171 ` 165` ``` val (sml_gth, othergoals) = hide_other_goals fixed_gth ``` wenzelm@23171 ` 166` ``` in ``` wenzelm@49339 ` 167` ``` (sml_gth, export {fixes = fixedvars, ``` wenzelm@49339 ` 168` ``` assumes = othergoals, ``` wenzelm@23171 ` 169` ``` sgid = i, gth = th}) ``` wenzelm@23171 ` 170` ``` end; ``` wenzelm@23171 ` 171` wenzelm@23171 ` 172` wenzelm@23171 ` 173` ```(* Fixme: allow different order of subgoals given to expf *) ``` wenzelm@23171 ` 174` ```(* make each subgoal into a separate thm that needs to be proved *) ``` wenzelm@23171 ` 175` ```(* loosely corresponds to: ``` wenzelm@49339 ` 176` ```Given ``` wenzelm@23171 ` 177` ``` "[| SG0; ... SGm |] ==> G" : thm ``` wenzelm@49339 ` 178` ```Result: ``` wenzelm@23171 ` 179` ```(["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals ``` wenzelm@23171 ` 180` ``` ["SG0", ..., "SGm"] : thm list -> -- export function ``` wenzelm@23171 ` 181` ``` "G" : thm) ``` wenzelm@23171 ` 182` ```*) ``` wenzelm@49339 ` 183` ```fun subgoal_thms th = ``` wenzelm@49339 ` 184` ``` let ``` wenzelm@49339 ` 185` ``` val t = (prop_of th); ``` wenzelm@23171 ` 186` wenzelm@23171 ` 187` ``` val prems = Logic.strip_imp_prems t; ``` wenzelm@23171 ` 188` wenzelm@23171 ` 189` ``` val sgn = Thm.theory_of_thm th; ``` wenzelm@23171 ` 190` ``` val ctermify = Thm.cterm_of sgn; ``` wenzelm@23171 ` 191` wenzelm@23171 ` 192` ``` val aprems = map (Thm.trivial o ctermify) prems; ``` wenzelm@23171 ` 193` wenzelm@49339 ` 194` ``` fun explortf premths = ``` wenzelm@23171 ` 195` ``` Drule.implies_elim_list th premths ``` wenzelm@23171 ` 196` ``` in ``` wenzelm@23171 ` 197` ``` (aprems, explortf) ``` wenzelm@23171 ` 198` ``` end; ``` wenzelm@23171 ` 199` wenzelm@23171 ` 200` wenzelm@23171 ` 201` ```(* Fixme: allow different order of subgoals in exportf *) ``` wenzelm@23171 ` 202` ```(* as above, but also fix all parameters in all subgoals, and uses ``` wenzelm@23171 ` 203` ```fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent ``` wenzelm@23171 ` 204` ```subgoals. *) ``` wenzelm@23171 ` 205` ```(* loosely corresponds to: ``` wenzelm@49339 ` 206` ```Given ``` wenzelm@49339 ` 207` ``` "[| !! x0s. A0s x0s ==> SG0 x0s; ``` wenzelm@23171 ` 208` ``` ...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm ``` wenzelm@49339 ` 209` ```Result: ``` wenzelm@49339 ` 210` ```(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'", ``` wenzelm@23171 ` 211` ``` ... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals ``` wenzelm@23171 ` 212` ``` ["SG0 x0s'", ..., "SGm xms'"] : thm list -> -- export function ``` wenzelm@23171 ` 213` ``` "G" : thm) ``` wenzelm@23171 ` 214` ```*) ``` wenzelm@23171 ` 215` ```(* requires being given solutions! *) ``` wenzelm@49340 ` 216` ```fun fixed_subgoal_thms ctxt th = ``` wenzelm@49339 ` 217` ``` let ``` wenzelm@23171 ` 218` ``` val (subgoals, expf) = subgoal_thms th; ``` wenzelm@23171 ` 219` ```(* fun export_sg (th, exp) = exp th; *) ``` wenzelm@49339 ` 220` ``` fun export_sgs expfs solthms = ``` wenzelm@23171 ` 221` ``` expf (map2 (curry (op |>)) solthms expfs); ``` wenzelm@23171 ` 222` ```(* expf (map export_sg (ths ~~ expfs)); *) ``` wenzelm@49339 ` 223` ``` in ``` wenzelm@49339 ` 224` ``` apsnd export_sgs (Library.split_list (map (apsnd export_solution o ``` wenzelm@49340 ` 225` ``` fix_alls ctxt 1) subgoals)) ``` wenzelm@23171 ` 226` ``` end; ``` wenzelm@23171 ` 227` wenzelm@23171 ` 228` ```end; ```