src/Tools/IsaPlanner/isand.ML
 author wenzelm Thu Jun 09 16:34:49 2011 +0200 (2011-06-09) changeset 43324 2b47822868e4 parent 35845 e5980f0ad025 child 44121 44adaa6db327 permissions -rw-r--r--
discontinued Name.variant to emphasize that this is old-style / indirect;
 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@23175 ` 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` wenzelm@23171 ` 27` ``` (* export data *) ``` wenzelm@23171 ` 28` ``` datatype export = export of ``` wenzelm@23171 ` 29` ``` {gth: Thm.thm, (* initial goal theorem *) ``` wenzelm@23171 ` 30` ``` sgid: int, (* subgoal id which has been fixed etc *) ``` wenzelm@23171 ` 31` ``` fixes: Thm.cterm list, (* frees *) ``` wenzelm@23171 ` 32` ``` assumes: Thm.cterm list} (* assumptions *) ``` wenzelm@23171 ` 33` ``` val fixes_of_exp : export -> Thm.cterm list ``` wenzelm@23171 ` 34` ``` val export_back : export -> Thm.thm -> Thm.thm Seq.seq ``` wenzelm@23171 ` 35` ``` val export_solution : export -> Thm.thm -> Thm.thm ``` wenzelm@23171 ` 36` ``` val export_solutions : export list * Thm.thm -> Thm.thm ``` wenzelm@23171 ` 37` wenzelm@23171 ` 38` ``` (* inserting meta level params for frees in the conditions *) ``` wenzelm@23171 ` 39` ``` val allify_conditions : ``` wenzelm@23171 ` 40` ``` (Term.term -> Thm.cterm) -> ``` wenzelm@23171 ` 41` ``` (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list ``` wenzelm@23171 ` 42` ``` val allify_conditions' : ``` wenzelm@23171 ` 43` ``` (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list ``` wenzelm@23171 ` 44` ``` val assume_allified : ``` wenzelm@23171 ` 45` ``` theory -> (string * Term.sort) list * (string * Term.typ) list ``` wenzelm@23171 ` 46` ``` -> Term.term -> (Thm.cterm * Thm.thm) ``` wenzelm@23171 ` 47` wenzelm@23171 ` 48` ``` (* meta level fixed params (i.e. !! vars) *) ``` wenzelm@23171 ` 49` ``` val fix_alls_in_term : Term.term -> Term.term * Term.term list ``` wenzelm@23171 ` 50` ``` val fix_alls_term : int -> Term.term -> Term.term * Term.term list ``` wenzelm@23171 ` 51` ``` val fix_alls_cterm : int -> Thm.thm -> Thm.cterm * Thm.cterm list ``` wenzelm@23171 ` 52` ``` val fix_alls' : int -> Thm.thm -> Thm.thm * Thm.cterm list ``` wenzelm@23171 ` 53` ``` val fix_alls : int -> Thm.thm -> Thm.thm * export ``` wenzelm@23171 ` 54` wenzelm@23171 ` 55` ``` (* meta variables in types and terms *) ``` wenzelm@23171 ` 56` ``` val fix_tvars_to_tfrees_in_terms ``` wenzelm@23171 ` 57` ``` : string list (* avoid these names *) ``` wenzelm@23171 ` 58` ``` -> Term.term list -> ``` wenzelm@23171 ` 59` ``` (((string * int) * Term.sort) * (string * Term.sort)) list (* renamings *) ``` wenzelm@23171 ` 60` ``` val fix_vars_to_frees_in_terms ``` wenzelm@23171 ` 61` ``` : string list (* avoid these names *) ``` wenzelm@23171 ` 62` ``` -> Term.term list -> ``` wenzelm@23171 ` 63` ``` (((string * int) * Term.typ) * (string * Term.typ)) list (* renamings *) ``` wenzelm@23171 ` 64` ``` val fix_tvars_to_tfrees : Thm.thm -> Thm.ctyp list * Thm.thm ``` wenzelm@23171 ` 65` ``` val fix_vars_to_frees : Thm.thm -> Thm.cterm list * Thm.thm ``` wenzelm@23171 ` 66` ``` val fix_vars_and_tvars : ``` wenzelm@23171 ` 67` ``` Thm.thm -> (Thm.cterm list * Thm.ctyp list) * Thm.thm ``` wenzelm@23171 ` 68` ``` val fix_vars_upto_idx : int -> Thm.thm -> Thm.thm ``` wenzelm@23171 ` 69` ``` val fix_tvars_upto_idx : int -> Thm.thm -> Thm.thm ``` wenzelm@23171 ` 70` ``` val unfix_frees : Thm.cterm list -> Thm.thm -> Thm.thm ``` wenzelm@23171 ` 71` ``` val unfix_tfrees : Thm.ctyp list -> Thm.thm -> Thm.thm ``` wenzelm@23171 ` 72` ``` val unfix_frees_and_tfrees : ``` wenzelm@23171 ` 73` ``` (Thm.cterm list * Thm.ctyp list) -> Thm.thm -> Thm.thm ``` wenzelm@23171 ` 74` wenzelm@23171 ` 75` ``` (* assumptions/subgoals *) ``` wenzelm@23171 ` 76` ``` val assume_prems : ``` wenzelm@23171 ` 77` ``` int -> Thm.thm -> Thm.thm list * Thm.thm * Thm.cterm list ``` wenzelm@23171 ` 78` ``` val fixed_subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm) ``` wenzelm@23171 ` 79` ``` val fixes_and_assumes : int -> Thm.thm -> Thm.thm list * Thm.thm * export ``` wenzelm@23171 ` 80` ``` val hide_other_goals : Thm.thm -> Thm.thm * Thm.cterm list ``` wenzelm@23171 ` 81` ``` val hide_prems : Thm.thm -> Thm.thm * Thm.cterm list ``` wenzelm@23171 ` 82` wenzelm@23171 ` 83` ``` (* abstracts cterms (vars) to locally meta-all bounds *) ``` wenzelm@23171 ` 84` ``` val prepare_goal_export : string list * Thm.cterm list -> Thm.thm ``` wenzelm@23171 ` 85` ``` -> int * Thm.thm ``` wenzelm@23171 ` 86` ``` val solve_with : Thm.thm -> Thm.thm -> Thm.thm Seq.seq ``` wenzelm@23171 ` 87` ``` val subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm) ``` wenzelm@23171 ` 88` ```end ``` wenzelm@23171 ` 89` wenzelm@23171 ` 90` wenzelm@23171 ` 91` ```structure IsaND ``` wenzelm@23171 ` 92` ```: ISA_ND ``` wenzelm@23171 ` 93` ```= struct ``` wenzelm@23171 ` 94` wenzelm@23171 ` 95` ```(* Solve *some* subgoal of "th" directly by "sol" *) ``` wenzelm@23171 ` 96` ```(* Note: this is probably what Markus ment to do upon export of a ``` wenzelm@23171 ` 97` ```"show" but maybe he used RS/rtac instead, which would wrongly lead to ``` wenzelm@23171 ` 98` ```failing if there are premices to the shown goal. ``` wenzelm@23171 ` 99` wenzelm@23171 ` 100` ```given: ``` wenzelm@23171 ` 101` ```sol : Thm.thm = [| Ai... |] ==> Ci ``` wenzelm@23171 ` 102` ```th : Thm.thm = ``` wenzelm@23171 ` 103` ``` [| ... [| Ai... |] ==> Ci ... |] ==> G ``` wenzelm@23171 ` 104` ```results in: ``` wenzelm@23171 ` 105` ``` [| ... [| Ai-1... |] ==> Ci-1 ``` wenzelm@23171 ` 106` ``` [| Ai+1... |] ==> Ci+1 ... ``` wenzelm@23171 ` 107` ``` |] ==> G ``` wenzelm@23171 ` 108` ```i.e. solves some subgoal of th that is identical to sol. ``` wenzelm@23171 ` 109` ```*) ``` wenzelm@23171 ` 110` ```fun solve_with sol th = ``` wenzelm@23171 ` 111` ``` let fun solvei 0 = Seq.empty ``` wenzelm@23171 ` 112` ``` | solvei i = ``` wenzelm@31945 ` 113` ``` Seq.append (Thm.bicompose false (false,sol,0) i th) (solvei (i - 1)) ``` wenzelm@23171 ` 114` ``` in ``` wenzelm@23171 ` 115` ``` solvei (Thm.nprems_of th) ``` wenzelm@23171 ` 116` ``` end; ``` wenzelm@23171 ` 117` wenzelm@23171 ` 118` wenzelm@23171 ` 119` ```(* Given ctertmify function, (string,type) pairs capturing the free ``` wenzelm@23171 ` 120` ```vars that need to be allified in the assumption, and a theorem with ``` wenzelm@23171 ` 121` ```assumptions possibly containing the free vars, then we give back the ``` wenzelm@23171 ` 122` ```assumptions allified as hidden hyps. ``` wenzelm@23171 ` 123` wenzelm@23171 ` 124` ```Given: x ``` wenzelm@23171 ` 125` ```th: A vs ==> B vs ``` wenzelm@23171 ` 126` ```Results in: "B vs" [!!x. A x] ``` wenzelm@23171 ` 127` ```*) ``` wenzelm@23171 ` 128` ```fun allify_conditions ctermify Ts th = ``` wenzelm@23171 ` 129` ``` let ``` wenzelm@23171 ` 130` ``` val premts = Thm.prems_of th; ``` wenzelm@23171 ` 131` ``` ``` wenzelm@23171 ` 132` ``` fun allify_prem_var (vt as (n,ty),t) = ``` wenzelm@23171 ` 133` ``` (Term.all ty) \$ (Abs(n,ty,Term.abstract_over (Free vt, t))) ``` wenzelm@23171 ` 134` wenzelm@30190 ` 135` ``` fun allify_prem Ts p = List.foldr allify_prem_var p Ts ``` wenzelm@23171 ` 136` wenzelm@23171 ` 137` ``` val cTs = map (ctermify o Free) Ts ``` wenzelm@23171 ` 138` ``` val cterm_asms = map (ctermify o allify_prem Ts) premts ``` wenzelm@23171 ` 139` ``` val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms ``` wenzelm@23171 ` 140` ``` in ``` wenzelm@23171 ` 141` ``` (Library.foldl (fn (x,y) => y COMP x) (th, allifyied_asm_thms), cterm_asms) ``` wenzelm@23171 ` 142` ``` end; ``` wenzelm@23171 ` 143` wenzelm@23171 ` 144` ```fun allify_conditions' Ts th = ``` wenzelm@23171 ` 145` ``` allify_conditions (Thm.cterm_of (Thm.theory_of_thm th)) Ts th; ``` wenzelm@23171 ` 146` wenzelm@23171 ` 147` ```(* allify types *) ``` wenzelm@23171 ` 148` ```fun allify_typ ts ty = ``` wenzelm@23171 ` 149` ``` let ``` wenzelm@23171 ` 150` ``` fun trec (x as (TFree (s,srt))) = ``` wenzelm@23171 ` 151` ``` (case Library.find_first (fn (s2,srt2) => s = s2) ts ``` wenzelm@23171 ` 152` ``` of NONE => x ``` wenzelm@23171 ` 153` ``` | SOME (s2,_) => TVar ((s,0),srt)) ``` wenzelm@23171 ` 154` ``` (* Maybe add in check here for bad sorts? ``` wenzelm@23171 ` 155` ``` if srt = srt2 then TVar ((s,0),srt) ``` wenzelm@23171 ` 156` ``` else raise ("thaw_typ", ts, ty) *) ``` wenzelm@23171 ` 157` ``` | trec (Type (s,typs)) = Type (s, map trec typs) ``` wenzelm@23171 ` 158` ``` | trec (v as TVar _) = v; ``` wenzelm@23171 ` 159` ``` in trec ty end; ``` wenzelm@23171 ` 160` wenzelm@23171 ` 161` ```(* implicit types and term *) ``` wenzelm@23171 ` 162` ```fun allify_term_typs ty = Term.map_types (allify_typ ty); ``` wenzelm@23171 ` 163` wenzelm@23171 ` 164` ```(* allified version of term, given frees to allify over. Note that we ``` wenzelm@23171 ` 165` ```only allify over the types on the given allified cterm, we can't do ``` wenzelm@23171 ` 166` ```this for the theorem as we are not allowed type-vars in the hyp. *) ``` wenzelm@23171 ` 167` ```(* FIXME: make the allified term keep the same conclusion as it ``` wenzelm@23171 ` 168` ```started with, rather than a strictly more general version (ie use ``` wenzelm@23171 ` 169` ```instantiate with initial params we abstracted from, rather than ``` wenzelm@23171 ` 170` ```forall_elim_vars. *) ``` wenzelm@23171 ` 171` ```fun assume_allified sgn (tyvs,vs) t = ``` wenzelm@23171 ` 172` ``` let ``` wenzelm@23171 ` 173` ``` fun allify_var (vt as (n,ty),t) = ``` wenzelm@23171 ` 174` ``` (Term.all ty) \$ (Abs(n,ty,Term.abstract_over (Free vt, t))) ``` wenzelm@23171 ` 175` ``` fun allify Ts p = List.foldr allify_var p Ts ``` wenzelm@23171 ` 176` wenzelm@23171 ` 177` ``` val ctermify = Thm.cterm_of sgn; ``` wenzelm@23171 ` 178` ``` val cvars = map (fn (n,ty) => ctermify (Var ((n,0),ty))) vs ``` wenzelm@23171 ` 179` ``` val allified_term = t |> allify vs; ``` wenzelm@23171 ` 180` ``` val ct = ctermify allified_term; ``` wenzelm@23171 ` 181` ``` val typ_allified_ct = ctermify (allify_term_typs tyvs allified_term); ``` wenzelm@23171 ` 182` ``` in (typ_allified_ct, ``` wenzelm@26653 ` 183` ``` Thm.forall_elim_vars 0 (Thm.assume ct)) end; ``` wenzelm@23171 ` 184` wenzelm@23171 ` 185` wenzelm@23171 ` 186` ```(* change type-vars to fresh type frees *) ``` wenzelm@23171 ` 187` ```fun fix_tvars_to_tfrees_in_terms names ts = ``` wenzelm@23171 ` 188` ``` let ``` wenzelm@29270 ` 189` ``` val tfree_names = map fst (List.foldr OldTerm.add_term_tfrees [] ts); ``` wenzelm@29270 ` 190` ``` val tvars = List.foldr OldTerm.add_term_tvars [] ts; ``` wenzelm@23171 ` 191` ``` val (names',renamings) = ``` wenzelm@23171 ` 192` ``` List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) => ``` wenzelm@43324 ` 193` ``` let val n2 = singleton (Name.variant_list Ns) n in ``` wenzelm@23171 ` 194` ``` (n2::Ns, (tv, (n2,s))::Rs) ``` wenzelm@23171 ` 195` ``` end) (tfree_names @ names,[]) tvars; ``` wenzelm@23171 ` 196` ``` in renamings end; ``` wenzelm@23171 ` 197` ```fun fix_tvars_to_tfrees th = ``` wenzelm@23171 ` 198` ``` let ``` wenzelm@23171 ` 199` ``` val sign = Thm.theory_of_thm th; ``` wenzelm@23171 ` 200` ``` val ctypify = Thm.ctyp_of sign; ``` wenzelm@23171 ` 201` ``` val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); ``` wenzelm@23171 ` 202` ``` val renamings = fix_tvars_to_tfrees_in_terms ``` wenzelm@23171 ` 203` ``` [] ((Thm.prop_of th) :: tpairs); ``` wenzelm@23171 ` 204` ``` val crenamings = ``` wenzelm@23171 ` 205` ``` map (fn (v,f) => (ctypify (TVar v), ctypify (TFree f))) ``` wenzelm@23171 ` 206` ``` renamings; ``` wenzelm@23171 ` 207` ``` val fixedfrees = map snd crenamings; ``` wenzelm@23171 ` 208` ``` in (fixedfrees, Thm.instantiate (crenamings, []) th) end; ``` wenzelm@23171 ` 209` wenzelm@23171 ` 210` wenzelm@23171 ` 211` ```(* change type-free's to type-vars in th, skipping the ones in "ns" *) ``` wenzelm@23171 ` 212` ```fun unfix_tfrees ns th = ``` wenzelm@23171 ` 213` ``` let ``` wenzelm@23171 ` 214` ``` val varfiytfrees = map (Term.dest_TFree o Thm.typ_of) ns ``` wenzelm@29270 ` 215` ``` val skiptfrees = subtract (op =) varfiytfrees (OldTerm.add_term_tfrees (Thm.prop_of th,[])); ``` wenzelm@35845 ` 216` ``` in #2 (Thm.varifyT_global' skiptfrees th) end; ``` wenzelm@23171 ` 217` wenzelm@23171 ` 218` ```(* change schematic/meta vars to fresh free vars, avoiding name clashes ``` wenzelm@23171 ` 219` ``` with "names" *) ``` wenzelm@23171 ` 220` ```fun fix_vars_to_frees_in_terms names ts = ``` wenzelm@23171 ` 221` ``` let ``` wenzelm@29265 ` 222` ``` val vars = map Term.dest_Var (List.foldr OldTerm.add_term_vars [] ts); ``` wenzelm@29270 ` 223` ``` val Ns = List.foldr OldTerm.add_term_names names ts; ``` wenzelm@23171 ` 224` ``` val (_,renamings) = ``` wenzelm@23171 ` 225` ``` Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => ``` wenzelm@43324 ` 226` ``` let val n2 = singleton (Name.variant_list Ns) n in ``` wenzelm@23171 ` 227` ``` (n2 :: Ns, (v, (n2,ty)) :: Rs) ``` wenzelm@23171 ` 228` ``` end) ((Ns,[]), vars); ``` wenzelm@23171 ` 229` ``` in renamings end; ``` wenzelm@23171 ` 230` ```fun fix_vars_to_frees th = ``` wenzelm@23171 ` 231` ``` let ``` wenzelm@23171 ` 232` ``` val ctermify = Thm.cterm_of (Thm.theory_of_thm th) ``` wenzelm@23171 ` 233` ``` val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); ``` wenzelm@23171 ` 234` ``` val renamings = fix_vars_to_frees_in_terms ``` wenzelm@23171 ` 235` ``` [] ([Thm.prop_of th] @ tpairs); ``` wenzelm@23171 ` 236` ``` val crenamings = ``` wenzelm@23171 ` 237` ``` map (fn (v,f) => (ctermify (Var v), ctermify (Free f))) ``` wenzelm@23171 ` 238` ``` renamings; ``` wenzelm@23171 ` 239` ``` val fixedfrees = map snd crenamings; ``` wenzelm@23171 ` 240` ``` in (fixedfrees, Thm.instantiate ([], crenamings) th) end; ``` wenzelm@23171 ` 241` wenzelm@23171 ` 242` ```fun fix_tvars_upto_idx ix th = ``` wenzelm@23171 ` 243` ``` let ``` wenzelm@23171 ` 244` ``` val sgn = Thm.theory_of_thm th; ``` wenzelm@23171 ` 245` ``` val ctypify = Thm.ctyp_of sgn ``` wenzelm@23171 ` 246` ``` val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); ``` wenzelm@23171 ` 247` ``` val prop = (Thm.prop_of th); ``` wenzelm@29270 ` 248` ``` val tvars = List.foldr OldTerm.add_term_tvars [] (prop :: tpairs); ``` wenzelm@23171 ` 249` ``` val ctyfixes = ``` wenzelm@23171 ` 250` ``` map_filter ``` wenzelm@23171 ` 251` ``` (fn (v as ((s,i),ty)) => ``` wenzelm@23171 ` 252` ``` if i <= ix then SOME (ctypify (TVar v), ctypify (TFree (s,ty))) ``` wenzelm@23171 ` 253` ``` else NONE) tvars; ``` wenzelm@23171 ` 254` ``` in Thm.instantiate (ctyfixes, []) th end; ``` wenzelm@23171 ` 255` ```fun fix_vars_upto_idx ix th = ``` wenzelm@23171 ` 256` ``` let ``` wenzelm@23171 ` 257` ``` val sgn = Thm.theory_of_thm th; ``` wenzelm@23171 ` 258` ``` val ctermify = Thm.cterm_of sgn ``` wenzelm@23171 ` 259` ``` val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); ``` wenzelm@23171 ` 260` ``` val prop = (Thm.prop_of th); ``` wenzelm@29265 ` 261` ``` val vars = map Term.dest_Var (List.foldr OldTerm.add_term_vars ``` wenzelm@23171 ` 262` ``` [] (prop :: tpairs)); ``` wenzelm@23171 ` 263` ``` val cfixes = ``` wenzelm@23171 ` 264` ``` map_filter ``` wenzelm@23171 ` 265` ``` (fn (v as ((s,i),ty)) => ``` wenzelm@23171 ` 266` ``` if i <= ix then SOME (ctermify (Var v), ctermify (Free (s,ty))) ``` wenzelm@23171 ` 267` ``` else NONE) vars; ``` wenzelm@23171 ` 268` ``` in Thm.instantiate ([], cfixes) th end; ``` wenzelm@23171 ` 269` wenzelm@23171 ` 270` wenzelm@23171 ` 271` ```(* make free vars into schematic vars with index zero *) ``` wenzelm@23171 ` 272` ``` fun unfix_frees frees = ``` wenzelm@26653 ` 273` ``` apply (map (K (Thm.forall_elim_var 0)) frees) ``` wenzelm@23171 ` 274` ``` o Drule.forall_intr_list frees; ``` wenzelm@23171 ` 275` wenzelm@23171 ` 276` ```(* fix term and type variables *) ``` wenzelm@23171 ` 277` ```fun fix_vars_and_tvars th = ``` wenzelm@23171 ` 278` ``` let val (tvars, th') = fix_tvars_to_tfrees th ``` wenzelm@23171 ` 279` ``` val (vars, th'') = fix_vars_to_frees th' ``` wenzelm@23171 ` 280` ``` in ((vars, tvars), th'') end; ``` wenzelm@23171 ` 281` wenzelm@23171 ` 282` ```(* implicit Thm.thm argument *) ``` wenzelm@23171 ` 283` ```(* assumes: vars may contain fixed versions of the frees *) ``` wenzelm@23171 ` 284` ```(* THINK: what if vs already has types varified? *) ``` wenzelm@23171 ` 285` ```fun unfix_frees_and_tfrees (vs,tvs) = ``` wenzelm@23171 ` 286` ``` (unfix_tfrees tvs o unfix_frees vs); ``` wenzelm@23171 ` 287` wenzelm@23171 ` 288` ```(* datatype to capture an exported result, ie a fix or assume. *) ``` wenzelm@23171 ` 289` ```datatype export = ``` wenzelm@23171 ` 290` ``` export of {fixes : Thm.cterm list, (* fixed vars *) ``` wenzelm@23171 ` 291` ``` assumes : Thm.cterm list, (* hidden hyps/assumed prems *) ``` wenzelm@23171 ` 292` ``` sgid : int, ``` wenzelm@23171 ` 293` ``` gth : Thm.thm}; (* subgoal/goalthm *) ``` wenzelm@23171 ` 294` wenzelm@23171 ` 295` ```fun fixes_of_exp (export rep) = #fixes rep; ``` wenzelm@23171 ` 296` wenzelm@23171 ` 297` ```(* export the result of the new goal thm, ie if we reduced teh ``` wenzelm@23171 ` 298` ```subgoal, then we get a new reduced subtgoal with the old ``` wenzelm@23171 ` 299` ```all-quantified variables *) ``` wenzelm@23171 ` 300` ```local ``` wenzelm@23171 ` 301` wenzelm@23171 ` 302` ```(* allify puts in a meta level univ quantifier for a free variavble *) ``` wenzelm@23171 ` 303` ```fun allify_term (v, t) = ``` wenzelm@23171 ` 304` ``` let val vt = #t (Thm.rep_cterm v) ``` wenzelm@23171 ` 305` ``` val (n,ty) = Term.dest_Free vt ``` wenzelm@23171 ` 306` ``` in (Term.all ty) \$ (Abs(n,ty,Term.abstract_over (vt, t))) end; ``` wenzelm@23171 ` 307` wenzelm@23171 ` 308` ```fun allify_for_sg_term ctermify vs t = ``` wenzelm@30190 ` 309` ``` let val t_alls = List.foldr allify_term t vs; ``` wenzelm@23171 ` 310` ``` val ct_alls = ctermify t_alls; ``` wenzelm@23171 ` 311` ``` in ``` wenzelm@23171 ` 312` ``` (ct_alls, Drule.forall_elim_list vs (Thm.assume ct_alls)) ``` wenzelm@23171 ` 313` ``` end; ``` wenzelm@23171 ` 314` ```(* lookup type of a free var name from a list *) ``` wenzelm@23171 ` 315` ```fun lookupfree vs vn = ``` wenzelm@23171 ` 316` ``` case Library.find_first (fn (n,ty) => n = vn) vs of ``` wenzelm@23171 ` 317` ``` NONE => error ("prepare_goal_export:lookupfree: " ^ vn ^ " does not occur in the term") ``` wenzelm@23171 ` 318` ``` | SOME x => x; ``` wenzelm@23171 ` 319` ```in ``` wenzelm@23171 ` 320` ```fun export_back (export {fixes = vs, assumes = hprems, ``` wenzelm@23171 ` 321` ``` sgid = i, gth = gth}) newth = ``` wenzelm@23171 ` 322` ``` let ``` wenzelm@23171 ` 323` ``` val sgn = Thm.theory_of_thm newth; ``` wenzelm@23171 ` 324` ``` val ctermify = Thm.cterm_of sgn; ``` wenzelm@23171 ` 325` wenzelm@23171 ` 326` ``` val sgs = prems_of newth; ``` wenzelm@23171 ` 327` ``` val (sgallcts, sgthms) = ``` wenzelm@23171 ` 328` ``` Library.split_list (map (allify_for_sg_term ctermify vs) sgs); ``` wenzelm@23171 ` 329` ``` val minimal_newth = ``` wenzelm@23171 ` 330` ``` (Library.foldl (fn ( newth', sgthm) => ``` wenzelm@23171 ` 331` ``` Drule.compose_single (sgthm, 1, newth')) ``` wenzelm@23171 ` 332` ``` (newth, sgthms)); ``` wenzelm@23171 ` 333` ``` val allified_newth = ``` wenzelm@23171 ` 334` ``` minimal_newth ``` wenzelm@23171 ` 335` ``` |> Drule.implies_intr_list hprems ``` wenzelm@23171 ` 336` ``` |> Drule.forall_intr_list vs ``` wenzelm@23171 ` 337` wenzelm@23171 ` 338` ``` val newth' = Drule.implies_intr_list sgallcts allified_newth ``` wenzelm@23171 ` 339` ``` in ``` wenzelm@31945 ` 340` ``` Thm.bicompose false (false, newth', (length sgallcts)) i gth ``` wenzelm@23171 ` 341` ``` end; ``` wenzelm@23171 ` 342` wenzelm@23171 ` 343` ```(* ``` wenzelm@23171 ` 344` ```Given "vs" : names of free variables to abstract over, ``` wenzelm@23171 ` 345` ```Given cterms : premices to abstract over (P1... Pn) in terms of vs, ``` wenzelm@23171 ` 346` ```Given a thm of the form: ``` wenzelm@23171 ` 347` ```P1 vs; ...; Pn vs ==> Goal(C vs) ``` wenzelm@23171 ` 348` wenzelm@23171 ` 349` ```Gives back: ``` wenzelm@23171 ` 350` ```(n, length of given cterms which have been allified ``` wenzelm@23171 ` 351` ``` [| !! vs. P1 vs; !! vs. Pn vs |] ==> !! C vs) the allified thm ``` wenzelm@23171 ` 352` ```*) ``` wenzelm@23171 ` 353` ```(* note: C may contain further premices etc ``` wenzelm@23171 ` 354` ```Note that cterms is the assumed facts, ie prems of "P1" that are ``` wenzelm@23171 ` 355` ```reintroduced in allified form. ``` wenzelm@23171 ` 356` ```*) ``` wenzelm@23171 ` 357` ```fun prepare_goal_export (vs, cterms) th = ``` wenzelm@23171 ` 358` ``` let ``` wenzelm@23171 ` 359` ``` val sgn = Thm.theory_of_thm th; ``` wenzelm@23171 ` 360` ``` val ctermify = Thm.cterm_of sgn; ``` wenzelm@23171 ` 361` wenzelm@29265 ` 362` ``` val allfrees = map Term.dest_Free (OldTerm.term_frees (Thm.prop_of th)) ``` wenzelm@23171 ` 363` ``` val cfrees = map (ctermify o Free o lookupfree allfrees) vs ``` wenzelm@23171 ` 364` wenzelm@23171 ` 365` ``` val sgs = prems_of th; ``` wenzelm@23171 ` 366` ``` val (sgallcts, sgthms) = ``` wenzelm@23171 ` 367` ``` Library.split_list (map (allify_for_sg_term ctermify cfrees) sgs); ``` wenzelm@23171 ` 368` wenzelm@23171 ` 369` ``` val minimal_th = ``` wenzelm@23171 ` 370` ``` Goal.conclude (Library.foldl (fn ( th', sgthm) => ``` wenzelm@23171 ` 371` ``` Drule.compose_single (sgthm, 1, th')) ``` wenzelm@23171 ` 372` ``` (th, sgthms)); ``` wenzelm@23171 ` 373` wenzelm@23171 ` 374` ``` val allified_th = ``` wenzelm@23171 ` 375` ``` minimal_th ``` wenzelm@23171 ` 376` ``` |> Drule.implies_intr_list cterms ``` wenzelm@23171 ` 377` ``` |> Drule.forall_intr_list cfrees ``` wenzelm@23171 ` 378` wenzelm@23171 ` 379` ``` val th' = Drule.implies_intr_list sgallcts allified_th ``` wenzelm@23171 ` 380` ``` in ``` wenzelm@23171 ` 381` ``` ((length sgallcts), th') ``` wenzelm@23171 ` 382` ``` end; ``` wenzelm@23171 ` 383` wenzelm@23171 ` 384` ```end; ``` wenzelm@23171 ` 385` wenzelm@23171 ` 386` wenzelm@23171 ` 387` ```(* exporting function that takes a solution to the fixed/assumed goal, ``` wenzelm@23171 ` 388` ```and uses this to solve the subgoal in the main theorem *) ``` wenzelm@23171 ` 389` ```fun export_solution (export {fixes = cfvs, assumes = hcprems, ``` wenzelm@23171 ` 390` ``` sgid = i, gth = gth}) solth = ``` wenzelm@23171 ` 391` ``` let ``` wenzelm@23171 ` 392` ``` val solth' = ``` wenzelm@23171 ` 393` ``` solth |> Drule.implies_intr_list hcprems ``` wenzelm@23171 ` 394` ``` |> Drule.forall_intr_list cfvs ``` wenzelm@23171 ` 395` ``` in Drule.compose_single (solth', i, gth) end; ``` wenzelm@23171 ` 396` wenzelm@30190 ` 397` ```fun export_solutions (xs,th) = List.foldr (uncurry export_solution) th xs; ``` wenzelm@23171 ` 398` wenzelm@23171 ` 399` wenzelm@23171 ` 400` ```(* fix parameters of a subgoal "i", as free variables, and create an ``` wenzelm@23171 ` 401` ```exporting function that will use the result of this proved goal to ``` wenzelm@23171 ` 402` ```show the goal in the original theorem. ``` wenzelm@23171 ` 403` wenzelm@23171 ` 404` ```Note, an advantage of this over Isar is that it supports instantiation ``` wenzelm@23171 ` 405` ```of unkowns in the earlier theorem, ie we can do instantiation of meta ``` wenzelm@23171 ` 406` ```vars! ``` wenzelm@23171 ` 407` wenzelm@23171 ` 408` ```avoids constant, free and vars names. ``` wenzelm@23171 ` 409` wenzelm@23171 ` 410` ```loosely corresponds to: ``` wenzelm@23171 ` 411` ```Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm ``` wenzelm@23171 ` 412` ```Result: ``` wenzelm@23171 ` 413` ``` ("(As ==> SGi x') ==> (As ==> SGi x')" : thm, ``` wenzelm@23171 ` 414` ``` expf : ``` wenzelm@23171 ` 415` ``` ("As ==> SGi x'" : thm) -> ``` wenzelm@23171 ` 416` ``` ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm) ``` wenzelm@23171 ` 417` ```*) ``` wenzelm@23171 ` 418` ```fun fix_alls_in_term alledt = ``` wenzelm@23171 ` 419` ``` let ``` wenzelm@23171 ` 420` ``` val t = Term.strip_all_body alledt; ``` wenzelm@23171 ` 421` ``` val alls = rev (Term.strip_all_vars alledt); ``` wenzelm@29265 ` 422` ``` val varnames = map (fst o fst o Term.dest_Var) (OldTerm.term_vars t) ``` wenzelm@29270 ` 423` ``` val names = OldTerm.add_term_names (t,varnames); ``` wenzelm@23171 ` 424` ``` val fvs = map Free ``` wenzelm@23171 ` 425` ``` (Name.variant_list names (map fst alls) ``` wenzelm@23171 ` 426` ``` ~~ (map snd alls)); ``` wenzelm@23171 ` 427` ``` in ((subst_bounds (fvs,t)), fvs) end; ``` wenzelm@23171 ` 428` wenzelm@23171 ` 429` ```fun fix_alls_term i t = ``` wenzelm@23171 ` 430` ``` let ``` wenzelm@29265 ` 431` ``` val varnames = map (fst o fst o Term.dest_Var) (OldTerm.term_vars t) ``` wenzelm@29270 ` 432` ``` val names = OldTerm.add_term_names (t,varnames); ``` wenzelm@23171 ` 433` ``` val gt = Logic.get_goal t i; ``` wenzelm@23171 ` 434` ``` val body = Term.strip_all_body gt; ``` wenzelm@23171 ` 435` ``` val alls = rev (Term.strip_all_vars gt); ``` wenzelm@23171 ` 436` ``` val fvs = map Free ``` wenzelm@23171 ` 437` ``` (Name.variant_list names (map fst alls) ``` wenzelm@23171 ` 438` ``` ~~ (map snd alls)); ``` wenzelm@23171 ` 439` ``` in ((subst_bounds (fvs,body)), fvs) end; ``` wenzelm@23171 ` 440` wenzelm@23171 ` 441` ```fun fix_alls_cterm i th = ``` wenzelm@23171 ` 442` ``` let ``` wenzelm@23171 ` 443` ``` val ctermify = Thm.cterm_of (Thm.theory_of_thm th); ``` wenzelm@23171 ` 444` ``` val (fixedbody, fvs) = fix_alls_term i (Thm.prop_of th); ``` wenzelm@23171 ` 445` ``` val cfvs = rev (map ctermify fvs); ``` wenzelm@23171 ` 446` ``` val ct_body = ctermify fixedbody ``` wenzelm@23171 ` 447` ``` in ``` wenzelm@23171 ` 448` ``` (ct_body, cfvs) ``` wenzelm@23171 ` 449` ``` end; ``` wenzelm@23171 ` 450` wenzelm@23171 ` 451` ```fun fix_alls' i = ``` wenzelm@23171 ` 452` ``` (apfst Thm.trivial) o (fix_alls_cterm i); ``` wenzelm@23171 ` 453` wenzelm@23171 ` 454` wenzelm@23171 ` 455` ```(* hide other goals *) ``` wenzelm@23171 ` 456` ```(* note the export goal is rotated by (i - 1) and will have to be ``` wenzelm@23171 ` 457` ```unrotated to get backto the originial position(s) *) ``` wenzelm@23171 ` 458` ```fun hide_other_goals th = ``` wenzelm@23171 ` 459` ``` let ``` wenzelm@23171 ` 460` ``` (* tl beacuse fst sg is the goal we are interested in *) ``` wenzelm@23171 ` 461` ``` val cprems = tl (Drule.cprems_of th) ``` wenzelm@23171 ` 462` ``` val aprems = map Thm.assume cprems ``` wenzelm@23171 ` 463` ``` in ``` wenzelm@23171 ` 464` ``` (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, ``` wenzelm@23171 ` 465` ``` cprems) ``` wenzelm@23171 ` 466` ``` end; ``` wenzelm@23171 ` 467` wenzelm@23171 ` 468` ```(* a nicer version of the above that leaves only a single subgoal (the ``` wenzelm@23171 ` 469` ```other subgoals are hidden hyps, that the exporter suffles about) ``` wenzelm@23171 ` 470` ```namely the subgoal that we were trying to solve. *) ``` wenzelm@23171 ` 471` ```(* loosely corresponds to: ``` wenzelm@23171 ` 472` ```Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm ``` wenzelm@23171 ` 473` ```Result: ``` wenzelm@23171 ` 474` ``` ("(As ==> SGi x') ==> SGi x'" : thm, ``` wenzelm@23171 ` 475` ``` expf : ``` wenzelm@23171 ` 476` ``` ("SGi x'" : thm) -> ``` wenzelm@23171 ` 477` ``` ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm) ``` wenzelm@23171 ` 478` ```*) ``` wenzelm@23171 ` 479` ```fun fix_alls i th = ``` wenzelm@23171 ` 480` ``` let ``` wenzelm@23171 ` 481` ``` val (fixed_gth, fixedvars) = fix_alls' i th ``` wenzelm@23171 ` 482` ``` val (sml_gth, othergoals) = hide_other_goals fixed_gth ``` wenzelm@23171 ` 483` ``` in ``` wenzelm@23171 ` 484` ``` (sml_gth, export {fixes = fixedvars, ``` wenzelm@23171 ` 485` ``` assumes = othergoals, ``` wenzelm@23171 ` 486` ``` sgid = i, gth = th}) ``` wenzelm@23171 ` 487` ``` end; ``` wenzelm@23171 ` 488` wenzelm@23171 ` 489` wenzelm@23171 ` 490` ```(* assume the premises of subgoal "i", this gives back a list of ``` wenzelm@23171 ` 491` ```assumed theorems that are the premices of subgoal i, it also gives ``` wenzelm@23171 ` 492` ```back a new goal thm and an exporter, the new goalthm is as the old ``` wenzelm@23171 ` 493` ```one, but without the premices, and the exporter will use a proof of ``` wenzelm@23171 ` 494` ```the new goalthm, possibly using the assumed premices, to shoe the ``` wenzelm@23171 ` 495` ```orginial goal. ``` wenzelm@23171 ` 496` wenzelm@23171 ` 497` ```Note: Dealing with meta vars, need to meta-level-all them in the ``` wenzelm@23171 ` 498` ```shyps, which we can later instantiate with a specific value.... ? ``` wenzelm@23171 ` 499` ```think about this... maybe need to introduce some new fixed vars and ``` wenzelm@23171 ` 500` ```then remove them again at the end... like I do with rw_inst. ``` wenzelm@23171 ` 501` wenzelm@23171 ` 502` ```loosely corresponds to: ``` wenzelm@23171 ` 503` ```Given "[| SG0; ... [| A0; ... An |] ==> SGi; ... SGm |] ==> G" : thm ``` wenzelm@23171 ` 504` ```Result: ``` wenzelm@23171 ` 505` ```(["A0" [A0], ... ,"An" [An]] : thm list, -- assumptions ``` wenzelm@23171 ` 506` ``` "SGi ==> SGi" : thm, -- new goal ``` wenzelm@23171 ` 507` ``` "SGi" ["A0" ... "An"] : thm -> -- export function ``` wenzelm@23171 ` 508` ``` ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list) ``` wenzelm@23171 ` 509` ```*) ``` wenzelm@23171 ` 510` ```fun assume_prems i th = ``` wenzelm@23171 ` 511` ``` let ``` wenzelm@23171 ` 512` ``` val t = (prop_of th); ``` wenzelm@23171 ` 513` ``` val gt = Logic.get_goal t i; ``` wenzelm@23171 ` 514` ``` val _ = case Term.strip_all_vars gt of [] => () ``` wenzelm@23171 ` 515` ``` | _ => error "assume_prems: goal has params" ``` wenzelm@23171 ` 516` ``` val body = gt; ``` wenzelm@23171 ` 517` ``` val prems = Logic.strip_imp_prems body; ``` wenzelm@23171 ` 518` ``` val concl = Logic.strip_imp_concl body; ``` wenzelm@23171 ` 519` wenzelm@23171 ` 520` ``` val sgn = Thm.theory_of_thm th; ``` wenzelm@23171 ` 521` ``` val ctermify = Thm.cterm_of sgn; ``` wenzelm@23171 ` 522` ``` val cprems = map ctermify prems; ``` wenzelm@23171 ` 523` ``` val aprems = map Thm.assume cprems; ``` wenzelm@23171 ` 524` ``` val gthi = Thm.trivial (ctermify concl); ``` wenzelm@23171 ` 525` wenzelm@23171 ` 526` ``` (* fun explortf thi = ``` wenzelm@23171 ` 527` ``` Drule.compose (Drule.implies_intr_list cprems thi, ``` wenzelm@23171 ` 528` ``` i, th) *) ``` wenzelm@23171 ` 529` ``` in ``` wenzelm@23171 ` 530` ``` (aprems, gthi, cprems) ``` wenzelm@23171 ` 531` ``` end; ``` wenzelm@23171 ` 532` wenzelm@23171 ` 533` wenzelm@23171 ` 534` ```(* first fix the variables, then assume the assumptions *) ``` wenzelm@23171 ` 535` ```(* loosely corresponds to: ``` wenzelm@23171 ` 536` ```Given ``` wenzelm@23171 ` 537` ``` "[| SG0; ... ``` wenzelm@23171 ` 538` ``` !! xs. [| A0 xs; ... An xs |] ==> SGi xs; ``` wenzelm@23171 ` 539` ``` ... SGm |] ==> G" : thm ``` wenzelm@23171 ` 540` ```Result: ``` wenzelm@23171 ` 541` ```(["A0 xs'" [A0 xs'], ... ,"An xs'" [An xs']] : thm list, -- assumptions ``` wenzelm@23171 ` 542` ``` "SGi xs' ==> SGi xs'" : thm, -- new goal ``` wenzelm@23171 ` 543` ``` "SGi xs'" ["A0 xs'" ... "An xs'"] : thm -> -- export function ``` wenzelm@23171 ` 544` ``` ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list) ``` wenzelm@23171 ` 545` ```*) ``` wenzelm@23171 ` 546` wenzelm@23171 ` 547` ```(* Note: the fix_alls actually pulls through all the assumptions which ``` wenzelm@23171 ` 548` ```means that the second export is not needed. *) ``` wenzelm@23171 ` 549` ```fun fixes_and_assumes i th = ``` wenzelm@23171 ` 550` ``` let ``` wenzelm@23171 ` 551` ``` val (fixgth, exp1) = fix_alls i th ``` wenzelm@23171 ` 552` ``` val (assumps, goalth, _) = assume_prems 1 fixgth ``` wenzelm@23171 ` 553` ``` in ``` wenzelm@23171 ` 554` ``` (assumps, goalth, exp1) ``` wenzelm@23171 ` 555` ``` end; ``` wenzelm@23171 ` 556` wenzelm@23171 ` 557` wenzelm@23171 ` 558` ```(* Fixme: allow different order of subgoals given to expf *) ``` wenzelm@23171 ` 559` ```(* make each subgoal into a separate thm that needs to be proved *) ``` wenzelm@23171 ` 560` ```(* loosely corresponds to: ``` wenzelm@23171 ` 561` ```Given ``` wenzelm@23171 ` 562` ``` "[| SG0; ... SGm |] ==> G" : thm ``` wenzelm@23171 ` 563` ```Result: ``` wenzelm@23171 ` 564` ```(["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals ``` wenzelm@23171 ` 565` ``` ["SG0", ..., "SGm"] : thm list -> -- export function ``` wenzelm@23171 ` 566` ``` "G" : thm) ``` wenzelm@23171 ` 567` ```*) ``` wenzelm@23171 ` 568` ```fun subgoal_thms th = ``` wenzelm@23171 ` 569` ``` let ``` wenzelm@23171 ` 570` ``` val t = (prop_of th); ``` wenzelm@23171 ` 571` wenzelm@23171 ` 572` ``` val prems = Logic.strip_imp_prems t; ``` wenzelm@23171 ` 573` wenzelm@23171 ` 574` ``` val sgn = Thm.theory_of_thm th; ``` wenzelm@23171 ` 575` ``` val ctermify = Thm.cterm_of sgn; ``` wenzelm@23171 ` 576` wenzelm@23171 ` 577` ``` val aprems = map (Thm.trivial o ctermify) prems; ``` wenzelm@23171 ` 578` wenzelm@23171 ` 579` ``` fun explortf premths = ``` wenzelm@23171 ` 580` ``` Drule.implies_elim_list th premths ``` wenzelm@23171 ` 581` ``` in ``` wenzelm@23171 ` 582` ``` (aprems, explortf) ``` wenzelm@23171 ` 583` ``` end; ``` wenzelm@23171 ` 584` wenzelm@23171 ` 585` wenzelm@23171 ` 586` ```(* make all the premices of a theorem hidden, and provide an unhide ``` wenzelm@23171 ` 587` ```function, that will bring them back out at a later point. This is ``` wenzelm@23171 ` 588` ```useful if you want to get back these premices, after having used the ``` wenzelm@23171 ` 589` ```theorem with the premices hidden *) ``` wenzelm@23171 ` 590` ```(* loosely corresponds to: ``` wenzelm@23171 ` 591` ```Given "As ==> G" : thm ``` wenzelm@23171 ` 592` ```Result: ("G [As]" : thm, ``` wenzelm@23171 ` 593` ``` "G [As]" : thm -> "As ==> G" : thm ``` wenzelm@23171 ` 594` ```*) ``` wenzelm@23171 ` 595` ```fun hide_prems th = ``` wenzelm@23171 ` 596` ``` let ``` wenzelm@23171 ` 597` ``` val cprems = Drule.cprems_of th; ``` wenzelm@23171 ` 598` ``` val aprems = map Thm.assume cprems; ``` wenzelm@23171 ` 599` ``` (* val unhidef = Drule.implies_intr_list cprems; *) ``` wenzelm@23171 ` 600` ``` in ``` wenzelm@23171 ` 601` ``` (Drule.implies_elim_list th aprems, cprems) ``` wenzelm@23171 ` 602` ``` end; ``` wenzelm@23171 ` 603` wenzelm@23171 ` 604` wenzelm@23171 ` 605` wenzelm@23171 ` 606` wenzelm@23171 ` 607` ```(* Fixme: allow different order of subgoals in exportf *) ``` wenzelm@23171 ` 608` ```(* as above, but also fix all parameters in all subgoals, and uses ``` wenzelm@23171 ` 609` ```fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent ``` wenzelm@23171 ` 610` ```subgoals. *) ``` wenzelm@23171 ` 611` ```(* loosely corresponds to: ``` wenzelm@23171 ` 612` ```Given ``` wenzelm@23171 ` 613` ``` "[| !! x0s. A0s x0s ==> SG0 x0s; ``` wenzelm@23171 ` 614` ``` ...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm ``` wenzelm@23171 ` 615` ```Result: ``` wenzelm@23171 ` 616` ```(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'", ``` wenzelm@23171 ` 617` ``` ... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals ``` wenzelm@23171 ` 618` ``` ["SG0 x0s'", ..., "SGm xms'"] : thm list -> -- export function ``` wenzelm@23171 ` 619` ``` "G" : thm) ``` wenzelm@23171 ` 620` ```*) ``` wenzelm@23171 ` 621` ```(* requires being given solutions! *) ``` wenzelm@23171 ` 622` ```fun fixed_subgoal_thms th = ``` wenzelm@23171 ` 623` ``` let ``` wenzelm@23171 ` 624` ``` val (subgoals, expf) = subgoal_thms th; ``` wenzelm@23171 ` 625` ```(* fun export_sg (th, exp) = exp th; *) ``` wenzelm@23171 ` 626` ``` fun export_sgs expfs solthms = ``` wenzelm@23171 ` 627` ``` expf (map2 (curry (op |>)) solthms expfs); ``` wenzelm@23171 ` 628` ```(* expf (map export_sg (ths ~~ expfs)); *) ``` wenzelm@23171 ` 629` ``` in ``` wenzelm@23171 ` 630` ``` apsnd export_sgs (Library.split_list (map (apsnd export_solution o ``` wenzelm@23171 ` 631` ``` fix_alls 1) subgoals)) ``` wenzelm@23171 ` 632` ``` end; ``` wenzelm@23171 ` 633` wenzelm@23171 ` 634` ```end; ```