src/Tools/IsaPlanner/isand.ML
 author wenzelm Thu May 30 17:10:13 2013 +0200 (2013-05-30) changeset 52244 cb15da7bd550 parent 52242 2d634bfa1bbf child 52245 f76fb8858e0b permissions -rw-r--r--
misc tuning;
 wenzelm@23175 ` 1` ```(* Title: Tools/IsaPlanner/isand.ML ``` wenzelm@23171 ` 2` ``` Author: Lucas Dixon, University of Edinburgh ``` wenzelm@23175 ` 3` wenzelm@52244 ` 4` ```Natural Deduction tools (obsolete). ``` 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@52244 ` 27` ``` val allify_conditions: (term -> cterm) -> (string * typ) list -> thm -> thm * cterm list ``` wenzelm@23171 ` 28` wenzelm@52244 ` 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@52244 ` 32` ``` val fix_alls_term: Proof.context -> int -> term -> term * term list ``` wenzelm@23171 ` 33` wenzelm@52244 ` 34` ``` val unfix_frees: cterm list -> thm -> thm ``` wenzelm@23171 ` 35` wenzelm@23171 ` 36` ``` (* assumptions/subgoals *) ``` wenzelm@52244 ` 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@52244 ` 53` ``` let ``` wenzelm@52244 ` 54` ``` val premts = Thm.prems_of th; ``` wenzelm@49339 ` 55` wenzelm@52244 ` 56` ``` fun allify_prem_var (vt as (n, ty)) t = ``` wenzelm@52244 ` 57` ``` Logic.all_const ty \$ Abs (n, ty, Term.abstract_over (Free vt, t)) ``` wenzelm@23171 ` 58` wenzelm@52244 ` 59` ``` val allify_prem = fold_rev allify_prem_var ``` wenzelm@23171 ` 60` wenzelm@52244 ` 61` ``` val cTs = map (ctermify o Free) Ts ``` wenzelm@52244 ` 62` ``` val cterm_asms = map (ctermify o allify_prem Ts) premts ``` wenzelm@52244 ` 63` ``` val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms ``` wenzelm@52244 ` 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@52244 ` 68` ``` fold (K (Thm.forall_elim_var 0)) frees o Drule.forall_intr_list frees; ``` wenzelm@23171 ` 69` wenzelm@23171 ` 70` ```(* datatype to capture an exported result, ie a fix or assume. *) ``` wenzelm@49339 ` 71` ```datatype export = ``` wenzelm@52244 ` 72` ``` Export of ``` wenzelm@52244 ` 73` ``` {fixes : Thm.cterm list, (* fixed vars *) ``` wenzelm@52244 ` 74` ``` assumes : Thm.cterm list, (* hidden hyps/assumed prems *) ``` wenzelm@52244 ` 75` ``` sgid : int, ``` wenzelm@52244 ` 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@52244 ` 80` ```fun export_solution (Export {fixes = cfvs, assumes = hcprems, sgid = i, gth = gth}) solth = ``` wenzelm@52244 ` 81` ``` let ``` wenzelm@52244 ` 82` ``` val solth' = solth ``` wenzelm@52244 ` 83` ``` |> Drule.implies_intr_list hcprems ``` wenzelm@52244 ` 84` ``` |> Drule.forall_intr_list cfvs; ``` wenzelm@52244 ` 85` ``` in Drule.compose_single (solth', i, gth) end; ``` wenzelm@23171 ` 86` wenzelm@49340 ` 87` ```fun variant_names ctxt ts xs = ``` wenzelm@49340 ` 88` ``` let ``` wenzelm@49340 ` 89` ``` val names = ``` wenzelm@49340 ` 90` ``` Variable.names_of ctxt ``` wenzelm@49340 ` 91` ``` |> (fold o fold_aterms) ``` wenzelm@49340 ` 92` ``` (fn Var ((a, _), _) => Name.declare a ``` wenzelm@49340 ` 93` ``` | Free (a, _) => Name.declare a ``` wenzelm@49340 ` 94` ``` | _ => I) ts; ``` wenzelm@49340 ` 95` ``` in fst (fold_map Name.variant xs names) end; ``` wenzelm@23171 ` 96` wenzelm@23171 ` 97` ```(* fix parameters of a subgoal "i", as free variables, and create an ``` wenzelm@23171 ` 98` ```exporting function that will use the result of this proved goal to ``` wenzelm@49339 ` 99` ```show the goal in the original theorem. ``` wenzelm@23171 ` 100` wenzelm@23171 ` 101` ```Note, an advantage of this over Isar is that it supports instantiation ``` wenzelm@23171 ` 102` ```of unkowns in the earlier theorem, ie we can do instantiation of meta ``` wenzelm@49339 ` 103` ```vars! ``` wenzelm@23171 ` 104` wenzelm@49339 ` 105` ```avoids constant, free and vars names. ``` wenzelm@23171 ` 106` wenzelm@23171 ` 107` ```loosely corresponds to: ``` wenzelm@23171 ` 108` ```Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm ``` wenzelm@49339 ` 109` ```Result: ``` wenzelm@49339 ` 110` ``` ("(As ==> SGi x') ==> (As ==> SGi x')" : thm, ``` wenzelm@49339 ` 111` ``` expf : ``` wenzelm@49339 ` 112` ``` ("As ==> SGi x'" : thm) -> ``` wenzelm@23171 ` 113` ``` ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm) ``` wenzelm@23171 ` 114` ```*) ``` wenzelm@49340 ` 115` ```fun fix_alls_term ctxt i t = ``` wenzelm@52244 ` 116` ``` let ``` wenzelm@52244 ` 117` ``` val gt = Logic.get_goal t i; ``` wenzelm@52244 ` 118` ``` val body = Term.strip_all_body gt; ``` wenzelm@52244 ` 119` ``` val alls = rev (Term.strip_all_vars gt); ``` wenzelm@52244 ` 120` ``` val xs = variant_names ctxt [t] (map fst alls); ``` wenzelm@52244 ` 121` ``` val fvs = map Free (xs ~~ map snd alls); ``` wenzelm@52244 ` 122` ``` in ((subst_bounds (fvs,body)), fvs) end; ``` wenzelm@23171 ` 123` wenzelm@49340 ` 124` ```fun fix_alls_cterm ctxt i th = ``` wenzelm@52244 ` 125` ``` let ``` wenzelm@52244 ` 126` ``` val cert = Thm.cterm_of (Thm.theory_of_thm th); ``` wenzelm@52244 ` 127` ``` val (fixedbody, fvs) = fix_alls_term ctxt i (Thm.prop_of th); ``` wenzelm@52244 ` 128` ``` val cfvs = rev (map cert fvs); ``` wenzelm@52244 ` 129` ``` val ct_body = cert fixedbody; ``` wenzelm@52244 ` 130` ``` in (ct_body, cfvs) end; ``` wenzelm@23171 ` 131` wenzelm@49340 ` 132` ```fun fix_alls' ctxt i = apfst Thm.trivial o fix_alls_cterm ctxt i; ``` wenzelm@23171 ` 133` wenzelm@23171 ` 134` wenzelm@49339 ` 135` ```(* hide other goals *) ``` wenzelm@23171 ` 136` ```(* note the export goal is rotated by (i - 1) and will have to be ``` wenzelm@23171 ` 137` ```unrotated to get backto the originial position(s) *) ``` wenzelm@49339 ` 138` ```fun hide_other_goals th = ``` wenzelm@52244 ` 139` ``` let ``` wenzelm@52244 ` 140` ``` (* tl beacuse fst sg is the goal we are interested in *) ``` wenzelm@52244 ` 141` ``` val cprems = tl (Drule.cprems_of th); ``` wenzelm@52244 ` 142` ``` val aprems = map Thm.assume cprems; ``` wenzelm@52244 ` 143` ``` in (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, cprems) end; ``` wenzelm@23171 ` 144` wenzelm@23171 ` 145` ```(* a nicer version of the above that leaves only a single subgoal (the ``` wenzelm@23171 ` 146` ```other subgoals are hidden hyps, that the exporter suffles about) ``` wenzelm@23171 ` 147` ```namely the subgoal that we were trying to solve. *) ``` wenzelm@23171 ` 148` ```(* loosely corresponds to: ``` wenzelm@23171 ` 149` ```Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm ``` wenzelm@49339 ` 150` ```Result: ``` wenzelm@49339 ` 151` ``` ("(As ==> SGi x') ==> SGi x'" : thm, ``` wenzelm@49339 ` 152` ``` expf : ``` wenzelm@49339 ` 153` ``` ("SGi x'" : thm) -> ``` wenzelm@23171 ` 154` ``` ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm) ``` wenzelm@23171 ` 155` ```*) ``` wenzelm@49340 ` 156` ```fun fix_alls ctxt i th = ``` wenzelm@52244 ` 157` ``` let ``` wenzelm@52244 ` 158` ``` val (fixed_gth, fixedvars) = fix_alls' ctxt i th ``` wenzelm@52244 ` 159` ``` val (sml_gth, othergoals) = hide_other_goals fixed_gth ``` wenzelm@52244 ` 160` ``` in (sml_gth, Export {fixes = fixedvars, assumes = othergoals, sgid = i, gth = th}) end; ``` wenzelm@23171 ` 161` wenzelm@23171 ` 162` wenzelm@23171 ` 163` ```(* Fixme: allow different order of subgoals given to expf *) ``` wenzelm@23171 ` 164` ```(* make each subgoal into a separate thm that needs to be proved *) ``` wenzelm@23171 ` 165` ```(* loosely corresponds to: ``` wenzelm@49339 ` 166` ```Given ``` wenzelm@23171 ` 167` ``` "[| SG0; ... SGm |] ==> G" : thm ``` wenzelm@49339 ` 168` ```Result: ``` wenzelm@23171 ` 169` ```(["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals ``` wenzelm@23171 ` 170` ``` ["SG0", ..., "SGm"] : thm list -> -- export function ``` wenzelm@23171 ` 171` ``` "G" : thm) ``` wenzelm@23171 ` 172` ```*) ``` wenzelm@49339 ` 173` ```fun subgoal_thms th = ``` wenzelm@52244 ` 174` ``` let ``` wenzelm@52244 ` 175` ``` val cert = Thm.cterm_of (Thm.theory_of_thm th); ``` wenzelm@23171 ` 176` wenzelm@52244 ` 177` ``` val t = prop_of th; ``` wenzelm@23171 ` 178` wenzelm@52244 ` 179` ``` val prems = Logic.strip_imp_prems t; ``` wenzelm@52244 ` 180` ``` val aprems = map (Thm.trivial o cert) prems; ``` wenzelm@23171 ` 181` wenzelm@52244 ` 182` ``` fun explortf premths = Drule.implies_elim_list th premths; ``` wenzelm@52244 ` 183` ``` in (aprems, explortf) end; ``` wenzelm@23171 ` 184` wenzelm@23171 ` 185` wenzelm@23171 ` 186` ```(* Fixme: allow different order of subgoals in exportf *) ``` wenzelm@23171 ` 187` ```(* as above, but also fix all parameters in all subgoals, and uses ``` wenzelm@23171 ` 188` ```fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent ``` wenzelm@23171 ` 189` ```subgoals. *) ``` wenzelm@23171 ` 190` ```(* loosely corresponds to: ``` wenzelm@49339 ` 191` ```Given ``` wenzelm@49339 ` 192` ``` "[| !! x0s. A0s x0s ==> SG0 x0s; ``` wenzelm@23171 ` 193` ``` ...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm ``` wenzelm@49339 ` 194` ```Result: ``` wenzelm@49339 ` 195` ```(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'", ``` wenzelm@23171 ` 196` ``` ... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals ``` wenzelm@23171 ` 197` ``` ["SG0 x0s'", ..., "SGm xms'"] : thm list -> -- export function ``` wenzelm@23171 ` 198` ``` "G" : thm) ``` wenzelm@23171 ` 199` ```*) ``` wenzelm@23171 ` 200` ```(* requires being given solutions! *) ``` wenzelm@49340 ` 201` ```fun fixed_subgoal_thms ctxt th = ``` wenzelm@52244 ` 202` ``` let ``` wenzelm@52244 ` 203` ``` val (subgoals, expf) = subgoal_thms th; ``` wenzelm@52244 ` 204` ```(* fun export_sg (th, exp) = exp th; *) ``` wenzelm@52244 ` 205` ``` fun export_sgs expfs solthms = ``` wenzelm@52244 ` 206` ``` expf (map2 (curry (op |>)) solthms expfs); ``` wenzelm@52244 ` 207` ```(* expf (map export_sg (ths ~~ expfs)); *) ``` wenzelm@52244 ` 208` ``` in ``` wenzelm@52244 ` 209` ``` apsnd export_sgs ``` wenzelm@52244 ` 210` ``` (Library.split_list (map (apsnd export_solution o fix_alls ctxt 1) subgoals)) ``` wenzelm@52244 ` 211` ``` end; ``` wenzelm@23171 ` 212` wenzelm@23171 ` 213` ```end; ```