src/Tools/IsaPlanner/isand.ML
 author wenzelm Wed Sep 12 22:00:29 2012 +0200 (2012-09-12) changeset 49339 d1fcb4de8349 parent 46777 1ce61ee1571a child 49340 25fc6e0da459 permissions -rw-r--r--
eliminated some old material that is unused in the visible universe;
 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@23171 ` 29` ``` (* meta level fixed params (i.e. !! vars) *) ``` wenzelm@49339 ` 30` ``` val fix_alls_term : int -> term -> term * term list ``` wenzelm@23171 ` 31` wenzelm@49339 ` 32` ``` val unfix_frees : cterm list -> thm -> thm ``` wenzelm@23171 ` 33` wenzelm@23171 ` 34` ``` (* assumptions/subgoals *) ``` wenzelm@49339 ` 35` ``` val fixed_subgoal_thms : thm -> thm list * (thm list -> thm) ``` wenzelm@23171 ` 36` ```end ``` wenzelm@23171 ` 37` wenzelm@49339 ` 38` ```structure IsaND : ISA_ND = ``` wenzelm@49339 ` 39` ```struct ``` wenzelm@23171 ` 40` wenzelm@23171 ` 41` ```(* Given ctertmify function, (string,type) pairs capturing the free ``` wenzelm@23171 ` 42` ```vars that need to be allified in the assumption, and a theorem with ``` wenzelm@23171 ` 43` ```assumptions possibly containing the free vars, then we give back the ``` wenzelm@49339 ` 44` ```assumptions allified as hidden hyps. ``` wenzelm@23171 ` 45` wenzelm@49339 ` 46` ```Given: x ``` wenzelm@49339 ` 47` ```th: A vs ==> B vs ``` wenzelm@23171 ` 48` ```Results in: "B vs" [!!x. A x] ``` wenzelm@23171 ` 49` ```*) ``` wenzelm@49339 ` 50` ```fun allify_conditions ctermify Ts th = ``` wenzelm@49339 ` 51` ``` let ``` wenzelm@23171 ` 52` ``` val premts = Thm.prems_of th; ``` wenzelm@49339 ` 53` wenzelm@49339 ` 54` ``` fun allify_prem_var (vt as (n,ty),t) = ``` wenzelm@46217 ` 55` ``` (Logic.all_const ty) \$ (Abs(n,ty,Term.abstract_over (Free vt, t))) ``` wenzelm@23171 ` 56` wenzelm@30190 ` 57` ``` fun allify_prem Ts p = List.foldr allify_prem_var p Ts ``` wenzelm@23171 ` 58` wenzelm@23171 ` 59` ``` val cTs = map (ctermify o Free) Ts ``` wenzelm@23171 ` 60` ``` val cterm_asms = map (ctermify o allify_prem Ts) premts ``` wenzelm@23171 ` 61` ``` val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms ``` wenzelm@49339 ` 62` ``` in ``` wenzelm@23171 ` 63` ``` (Library.foldl (fn (x,y) => y COMP x) (th, allifyied_asm_thms), cterm_asms) ``` wenzelm@23171 ` 64` ``` 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@23171 ` 88` wenzelm@23171 ` 89` ```(* fix parameters of a subgoal "i", as free variables, and create an ``` wenzelm@23171 ` 90` ```exporting function that will use the result of this proved goal to ``` wenzelm@49339 ` 91` ```show the goal in the original theorem. ``` wenzelm@23171 ` 92` wenzelm@23171 ` 93` ```Note, an advantage of this over Isar is that it supports instantiation ``` wenzelm@23171 ` 94` ```of unkowns in the earlier theorem, ie we can do instantiation of meta ``` wenzelm@49339 ` 95` ```vars! ``` wenzelm@23171 ` 96` wenzelm@49339 ` 97` ```avoids constant, free and vars names. ``` wenzelm@23171 ` 98` wenzelm@23171 ` 99` ```loosely corresponds to: ``` wenzelm@23171 ` 100` ```Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm ``` wenzelm@49339 ` 101` ```Result: ``` wenzelm@49339 ` 102` ``` ("(As ==> SGi x') ==> (As ==> SGi x')" : thm, ``` wenzelm@49339 ` 103` ``` expf : ``` wenzelm@49339 ` 104` ``` ("As ==> SGi x'" : thm) -> ``` wenzelm@23171 ` 105` ``` ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm) ``` wenzelm@23171 ` 106` ```*) ``` wenzelm@49339 ` 107` ```fun fix_alls_term i t = ``` wenzelm@23171 ` 108` ``` let ``` wenzelm@44121 ` 109` ``` val varnames = map (fst o fst o Term.dest_Var) (Misc_Legacy.term_vars t) ``` wenzelm@44121 ` 110` ``` val names = Misc_Legacy.add_term_names (t,varnames); ``` wenzelm@23171 ` 111` ``` val gt = Logic.get_goal t i; ``` wenzelm@23171 ` 112` ``` val body = Term.strip_all_body gt; ``` wenzelm@23171 ` 113` ``` val alls = rev (Term.strip_all_vars gt); ``` wenzelm@49339 ` 114` ``` val fvs = map Free ``` wenzelm@23171 ` 115` ``` (Name.variant_list names (map fst alls) ``` wenzelm@23171 ` 116` ``` ~~ (map snd alls)); ``` wenzelm@23171 ` 117` ``` in ((subst_bounds (fvs,body)), fvs) end; ``` wenzelm@23171 ` 118` wenzelm@49339 ` 119` ```fun fix_alls_cterm i th = ``` wenzelm@23171 ` 120` ``` let ``` wenzelm@23171 ` 121` ``` val ctermify = Thm.cterm_of (Thm.theory_of_thm th); ``` wenzelm@23171 ` 122` ``` val (fixedbody, fvs) = fix_alls_term i (Thm.prop_of th); ``` wenzelm@23171 ` 123` ``` val cfvs = rev (map ctermify fvs); ``` wenzelm@23171 ` 124` ``` val ct_body = ctermify fixedbody ``` wenzelm@23171 ` 125` ``` in ``` wenzelm@23171 ` 126` ``` (ct_body, cfvs) ``` wenzelm@23171 ` 127` ``` end; ``` wenzelm@23171 ` 128` wenzelm@49339 ` 129` ```fun fix_alls' i = ``` wenzelm@23171 ` 130` ``` (apfst Thm.trivial) o (fix_alls_cterm i); ``` wenzelm@23171 ` 131` wenzelm@23171 ` 132` wenzelm@49339 ` 133` ```(* hide other goals *) ``` wenzelm@23171 ` 134` ```(* note the export goal is rotated by (i - 1) and will have to be ``` wenzelm@23171 ` 135` ```unrotated to get backto the originial position(s) *) ``` wenzelm@49339 ` 136` ```fun hide_other_goals th = ``` wenzelm@23171 ` 137` ``` let ``` wenzelm@23171 ` 138` ``` (* tl beacuse fst sg is the goal we are interested in *) ``` wenzelm@23171 ` 139` ``` val cprems = tl (Drule.cprems_of th) ``` wenzelm@23171 ` 140` ``` val aprems = map Thm.assume cprems ``` wenzelm@23171 ` 141` ``` in ``` wenzelm@49339 ` 142` ``` (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, ``` wenzelm@23171 ` 143` ``` cprems) ``` wenzelm@23171 ` 144` ``` end; ``` wenzelm@23171 ` 145` wenzelm@23171 ` 146` ```(* a nicer version of the above that leaves only a single subgoal (the ``` wenzelm@23171 ` 147` ```other subgoals are hidden hyps, that the exporter suffles about) ``` wenzelm@23171 ` 148` ```namely the subgoal that we were trying to solve. *) ``` wenzelm@23171 ` 149` ```(* loosely corresponds to: ``` wenzelm@23171 ` 150` ```Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm ``` wenzelm@49339 ` 151` ```Result: ``` wenzelm@49339 ` 152` ``` ("(As ==> SGi x') ==> SGi x'" : thm, ``` wenzelm@49339 ` 153` ``` expf : ``` wenzelm@49339 ` 154` ``` ("SGi x'" : thm) -> ``` wenzelm@23171 ` 155` ``` ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm) ``` wenzelm@23171 ` 156` ```*) ``` wenzelm@49339 ` 157` ```fun fix_alls i th = ``` wenzelm@49339 ` 158` ``` let ``` wenzelm@23171 ` 159` ``` val (fixed_gth, fixedvars) = fix_alls' i th ``` wenzelm@23171 ` 160` ``` val (sml_gth, othergoals) = hide_other_goals fixed_gth ``` wenzelm@23171 ` 161` ``` in ``` wenzelm@49339 ` 162` ``` (sml_gth, export {fixes = fixedvars, ``` wenzelm@49339 ` 163` ``` assumes = othergoals, ``` wenzelm@23171 ` 164` ``` sgid = i, gth = th}) ``` wenzelm@23171 ` 165` ``` end; ``` wenzelm@23171 ` 166` wenzelm@23171 ` 167` wenzelm@23171 ` 168` ```(* Fixme: allow different order of subgoals given to expf *) ``` wenzelm@23171 ` 169` ```(* make each subgoal into a separate thm that needs to be proved *) ``` wenzelm@23171 ` 170` ```(* loosely corresponds to: ``` wenzelm@49339 ` 171` ```Given ``` wenzelm@23171 ` 172` ``` "[| SG0; ... SGm |] ==> G" : thm ``` wenzelm@49339 ` 173` ```Result: ``` wenzelm@23171 ` 174` ```(["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals ``` wenzelm@23171 ` 175` ``` ["SG0", ..., "SGm"] : thm list -> -- export function ``` wenzelm@23171 ` 176` ``` "G" : thm) ``` wenzelm@23171 ` 177` ```*) ``` wenzelm@49339 ` 178` ```fun subgoal_thms th = ``` wenzelm@49339 ` 179` ``` let ``` wenzelm@49339 ` 180` ``` val t = (prop_of th); ``` wenzelm@23171 ` 181` wenzelm@23171 ` 182` ``` val prems = Logic.strip_imp_prems t; ``` wenzelm@23171 ` 183` wenzelm@23171 ` 184` ``` val sgn = Thm.theory_of_thm th; ``` wenzelm@23171 ` 185` ``` val ctermify = Thm.cterm_of sgn; ``` wenzelm@23171 ` 186` wenzelm@23171 ` 187` ``` val aprems = map (Thm.trivial o ctermify) prems; ``` wenzelm@23171 ` 188` wenzelm@49339 ` 189` ``` fun explortf premths = ``` wenzelm@23171 ` 190` ``` Drule.implies_elim_list th premths ``` wenzelm@23171 ` 191` ``` in ``` wenzelm@23171 ` 192` ``` (aprems, explortf) ``` wenzelm@23171 ` 193` ``` end; ``` wenzelm@23171 ` 194` wenzelm@23171 ` 195` wenzelm@23171 ` 196` ```(* Fixme: allow different order of subgoals in exportf *) ``` wenzelm@23171 ` 197` ```(* as above, but also fix all parameters in all subgoals, and uses ``` wenzelm@23171 ` 198` ```fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent ``` wenzelm@23171 ` 199` ```subgoals. *) ``` wenzelm@23171 ` 200` ```(* loosely corresponds to: ``` wenzelm@49339 ` 201` ```Given ``` wenzelm@49339 ` 202` ``` "[| !! x0s. A0s x0s ==> SG0 x0s; ``` wenzelm@23171 ` 203` ``` ...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm ``` wenzelm@49339 ` 204` ```Result: ``` wenzelm@49339 ` 205` ```(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'", ``` wenzelm@23171 ` 206` ``` ... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals ``` wenzelm@23171 ` 207` ``` ["SG0 x0s'", ..., "SGm xms'"] : thm list -> -- export function ``` wenzelm@23171 ` 208` ``` "G" : thm) ``` wenzelm@23171 ` 209` ```*) ``` wenzelm@23171 ` 210` ```(* requires being given solutions! *) ``` wenzelm@49339 ` 211` ```fun fixed_subgoal_thms th = ``` wenzelm@49339 ` 212` ``` let ``` wenzelm@23171 ` 213` ``` val (subgoals, expf) = subgoal_thms th; ``` wenzelm@23171 ` 214` ```(* fun export_sg (th, exp) = exp th; *) ``` wenzelm@49339 ` 215` ``` fun export_sgs expfs solthms = ``` wenzelm@23171 ` 216` ``` expf (map2 (curry (op |>)) solthms expfs); ``` wenzelm@23171 ` 217` ```(* expf (map export_sg (ths ~~ expfs)); *) ``` wenzelm@49339 ` 218` ``` in ``` wenzelm@49339 ` 219` ``` apsnd export_sgs (Library.split_list (map (apsnd export_solution o ``` wenzelm@23171 ` 220` ``` fix_alls 1) subgoals)) ``` wenzelm@23171 ` 221` ``` end; ``` wenzelm@23171 ` 222` wenzelm@23171 ` 223` ```end; ```