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