src/Tools/IsaPlanner/isand.ML
 author wenzelm Thu May 30 17:21:11 2013 +0200 (2013-05-30) changeset 52245 f76fb8858e0b parent 52244 cb15da7bd550 child 52246 54c0d4128b30 permissions -rw-r--r--
tuned signature;
tuned;
 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@52244 ` 26` ``` val variant_names: Proof.context -> term list -> string list -> string list ``` wenzelm@49340 ` 27` wenzelm@23171 ` 28` ``` (* meta level fixed params (i.e. !! vars) *) ``` wenzelm@52244 ` 29` ``` val fix_alls_term: Proof.context -> int -> term -> term * term list ``` wenzelm@23171 ` 30` wenzelm@52244 ` 31` ``` val unfix_frees: cterm list -> thm -> thm ``` wenzelm@23171 ` 32` wenzelm@23171 ` 33` ``` (* assumptions/subgoals *) ``` wenzelm@52244 ` 34` ``` val fixed_subgoal_thms: Proof.context -> thm -> thm list * (thm list -> thm) ``` wenzelm@23171 ` 35` ```end ``` wenzelm@23171 ` 36` wenzelm@49339 ` 37` ```structure IsaND : ISA_ND = ``` wenzelm@49339 ` 38` ```struct ``` wenzelm@23171 ` 39` wenzelm@23171 ` 40` ```(* make free vars into schematic vars with index zero *) ``` wenzelm@49339 ` 41` ```fun unfix_frees frees = ``` wenzelm@52244 ` 42` ``` fold (K (Thm.forall_elim_var 0)) frees o Drule.forall_intr_list frees; ``` wenzelm@23171 ` 43` wenzelm@23171 ` 44` ```(* datatype to capture an exported result, ie a fix or assume. *) ``` wenzelm@49339 ` 45` ```datatype export = ``` wenzelm@52244 ` 46` ``` Export of ``` wenzelm@52244 ` 47` ``` {fixes : Thm.cterm list, (* fixed vars *) ``` wenzelm@52244 ` 48` ``` assumes : Thm.cterm list, (* hidden hyps/assumed prems *) ``` wenzelm@52244 ` 49` ``` sgid : int, ``` wenzelm@52244 ` 50` ``` gth : Thm.thm}; (* subgoal/goalthm *) ``` wenzelm@23171 ` 51` wenzelm@23171 ` 52` ```(* exporting function that takes a solution to the fixed/assumed goal, ``` wenzelm@23171 ` 53` ```and uses this to solve the subgoal in the main theorem *) ``` wenzelm@52244 ` 54` ```fun export_solution (Export {fixes = cfvs, assumes = hcprems, sgid = i, gth = gth}) solth = ``` wenzelm@52244 ` 55` ``` let ``` wenzelm@52244 ` 56` ``` val solth' = solth ``` wenzelm@52244 ` 57` ``` |> Drule.implies_intr_list hcprems ``` wenzelm@52244 ` 58` ``` |> Drule.forall_intr_list cfvs; ``` wenzelm@52244 ` 59` ``` in Drule.compose_single (solth', i, gth) end; ``` wenzelm@23171 ` 60` wenzelm@49340 ` 61` ```fun variant_names ctxt ts xs = ``` wenzelm@49340 ` 62` ``` let ``` wenzelm@49340 ` 63` ``` val names = ``` wenzelm@49340 ` 64` ``` Variable.names_of ctxt ``` wenzelm@49340 ` 65` ``` |> (fold o fold_aterms) ``` wenzelm@49340 ` 66` ``` (fn Var ((a, _), _) => Name.declare a ``` wenzelm@49340 ` 67` ``` | Free (a, _) => Name.declare a ``` wenzelm@49340 ` 68` ``` | _ => I) ts; ``` wenzelm@49340 ` 69` ``` in fst (fold_map Name.variant xs names) end; ``` wenzelm@23171 ` 70` wenzelm@23171 ` 71` ```(* fix parameters of a subgoal "i", as free variables, and create an ``` wenzelm@23171 ` 72` ```exporting function that will use the result of this proved goal to ``` wenzelm@49339 ` 73` ```show the goal in the original theorem. ``` wenzelm@23171 ` 74` wenzelm@23171 ` 75` ```Note, an advantage of this over Isar is that it supports instantiation ``` wenzelm@23171 ` 76` ```of unkowns in the earlier theorem, ie we can do instantiation of meta ``` wenzelm@49339 ` 77` ```vars! ``` wenzelm@23171 ` 78` wenzelm@49339 ` 79` ```avoids constant, free and vars names. ``` wenzelm@23171 ` 80` wenzelm@23171 ` 81` ```loosely corresponds to: ``` wenzelm@23171 ` 82` ```Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm ``` wenzelm@49339 ` 83` ```Result: ``` wenzelm@49339 ` 84` ``` ("(As ==> SGi x') ==> (As ==> SGi x')" : thm, ``` wenzelm@49339 ` 85` ``` expf : ``` wenzelm@49339 ` 86` ``` ("As ==> SGi x'" : thm) -> ``` wenzelm@23171 ` 87` ``` ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm) ``` wenzelm@23171 ` 88` ```*) ``` wenzelm@49340 ` 89` ```fun fix_alls_term ctxt i t = ``` wenzelm@52244 ` 90` ``` let ``` wenzelm@52244 ` 91` ``` val gt = Logic.get_goal t i; ``` wenzelm@52244 ` 92` ``` val body = Term.strip_all_body gt; ``` wenzelm@52244 ` 93` ``` val alls = rev (Term.strip_all_vars gt); ``` wenzelm@52244 ` 94` ``` val xs = variant_names ctxt [t] (map fst alls); ``` wenzelm@52244 ` 95` ``` val fvs = map Free (xs ~~ map snd alls); ``` wenzelm@52244 ` 96` ``` in ((subst_bounds (fvs,body)), fvs) end; ``` wenzelm@23171 ` 97` wenzelm@49340 ` 98` ```fun fix_alls_cterm ctxt i th = ``` wenzelm@52244 ` 99` ``` let ``` wenzelm@52244 ` 100` ``` val cert = Thm.cterm_of (Thm.theory_of_thm th); ``` wenzelm@52244 ` 101` ``` val (fixedbody, fvs) = fix_alls_term ctxt i (Thm.prop_of th); ``` wenzelm@52244 ` 102` ``` val cfvs = rev (map cert fvs); ``` wenzelm@52244 ` 103` ``` val ct_body = cert fixedbody; ``` wenzelm@52244 ` 104` ``` in (ct_body, cfvs) end; ``` wenzelm@23171 ` 105` wenzelm@49340 ` 106` ```fun fix_alls' ctxt i = apfst Thm.trivial o fix_alls_cterm ctxt i; ``` wenzelm@23171 ` 107` wenzelm@23171 ` 108` wenzelm@49339 ` 109` ```(* hide other goals *) ``` wenzelm@23171 ` 110` ```(* note the export goal is rotated by (i - 1) and will have to be ``` wenzelm@23171 ` 111` ```unrotated to get backto the originial position(s) *) ``` wenzelm@49339 ` 112` ```fun hide_other_goals th = ``` wenzelm@52244 ` 113` ``` let ``` wenzelm@52244 ` 114` ``` (* tl beacuse fst sg is the goal we are interested in *) ``` wenzelm@52244 ` 115` ``` val cprems = tl (Drule.cprems_of th); ``` wenzelm@52244 ` 116` ``` val aprems = map Thm.assume cprems; ``` wenzelm@52244 ` 117` ``` in (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, cprems) end; ``` wenzelm@23171 ` 118` wenzelm@23171 ` 119` ```(* a nicer version of the above that leaves only a single subgoal (the ``` wenzelm@23171 ` 120` ```other subgoals are hidden hyps, that the exporter suffles about) ``` wenzelm@23171 ` 121` ```namely the subgoal that we were trying to solve. *) ``` wenzelm@23171 ` 122` ```(* loosely corresponds to: ``` wenzelm@23171 ` 123` ```Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm ``` wenzelm@49339 ` 124` ```Result: ``` wenzelm@49339 ` 125` ``` ("(As ==> SGi x') ==> SGi x'" : thm, ``` wenzelm@49339 ` 126` ``` expf : ``` wenzelm@49339 ` 127` ``` ("SGi x'" : thm) -> ``` wenzelm@23171 ` 128` ``` ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm) ``` wenzelm@23171 ` 129` ```*) ``` wenzelm@49340 ` 130` ```fun fix_alls ctxt i th = ``` wenzelm@52244 ` 131` ``` let ``` wenzelm@52244 ` 132` ``` val (fixed_gth, fixedvars) = fix_alls' ctxt i th ``` wenzelm@52244 ` 133` ``` val (sml_gth, othergoals) = hide_other_goals fixed_gth ``` wenzelm@52244 ` 134` ``` in (sml_gth, Export {fixes = fixedvars, assumes = othergoals, sgid = i, gth = th}) end; ``` wenzelm@23171 ` 135` wenzelm@23171 ` 136` wenzelm@23171 ` 137` ```(* Fixme: allow different order of subgoals given to expf *) ``` wenzelm@23171 ` 138` ```(* make each subgoal into a separate thm that needs to be proved *) ``` wenzelm@23171 ` 139` ```(* loosely corresponds to: ``` wenzelm@49339 ` 140` ```Given ``` wenzelm@23171 ` 141` ``` "[| SG0; ... SGm |] ==> G" : thm ``` wenzelm@49339 ` 142` ```Result: ``` wenzelm@23171 ` 143` ```(["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals ``` wenzelm@23171 ` 144` ``` ["SG0", ..., "SGm"] : thm list -> -- export function ``` wenzelm@23171 ` 145` ``` "G" : thm) ``` wenzelm@23171 ` 146` ```*) ``` wenzelm@49339 ` 147` ```fun subgoal_thms th = ``` wenzelm@52244 ` 148` ``` let ``` wenzelm@52244 ` 149` ``` val cert = Thm.cterm_of (Thm.theory_of_thm th); ``` wenzelm@23171 ` 150` wenzelm@52244 ` 151` ``` val t = prop_of th; ``` wenzelm@23171 ` 152` wenzelm@52244 ` 153` ``` val prems = Logic.strip_imp_prems t; ``` wenzelm@52244 ` 154` ``` val aprems = map (Thm.trivial o cert) prems; ``` wenzelm@23171 ` 155` wenzelm@52244 ` 156` ``` fun explortf premths = Drule.implies_elim_list th premths; ``` wenzelm@52244 ` 157` ``` in (aprems, explortf) end; ``` wenzelm@23171 ` 158` wenzelm@23171 ` 159` wenzelm@23171 ` 160` ```(* Fixme: allow different order of subgoals in exportf *) ``` wenzelm@23171 ` 161` ```(* as above, but also fix all parameters in all subgoals, and uses ``` wenzelm@23171 ` 162` ```fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent ``` wenzelm@23171 ` 163` ```subgoals. *) ``` wenzelm@23171 ` 164` ```(* loosely corresponds to: ``` wenzelm@49339 ` 165` ```Given ``` wenzelm@49339 ` 166` ``` "[| !! x0s. A0s x0s ==> SG0 x0s; ``` wenzelm@23171 ` 167` ``` ...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm ``` wenzelm@49339 ` 168` ```Result: ``` wenzelm@49339 ` 169` ```(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'", ``` wenzelm@23171 ` 170` ``` ... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals ``` wenzelm@23171 ` 171` ``` ["SG0 x0s'", ..., "SGm xms'"] : thm list -> -- export function ``` wenzelm@23171 ` 172` ``` "G" : thm) ``` wenzelm@23171 ` 173` ```*) ``` wenzelm@23171 ` 174` ```(* requires being given solutions! *) ``` wenzelm@49340 ` 175` ```fun fixed_subgoal_thms ctxt th = ``` wenzelm@52244 ` 176` ``` let ``` wenzelm@52244 ` 177` ``` val (subgoals, expf) = subgoal_thms th; ``` wenzelm@52244 ` 178` ```(* fun export_sg (th, exp) = exp th; *) ``` wenzelm@52244 ` 179` ``` fun export_sgs expfs solthms = ``` wenzelm@52244 ` 180` ``` expf (map2 (curry (op |>)) solthms expfs); ``` wenzelm@52244 ` 181` ```(* expf (map export_sg (ths ~~ expfs)); *) ``` wenzelm@52244 ` 182` ``` in ``` wenzelm@52244 ` 183` ``` apsnd export_sgs ``` wenzelm@52244 ` 184` ``` (Library.split_list (map (apsnd export_solution o fix_alls ctxt 1) subgoals)) ``` wenzelm@52244 ` 185` ``` end; ``` wenzelm@23171 ` 186` wenzelm@23171 ` 187` ```end; ```