src/Pure/Isar/proof_context.ML
changeset 19310 9b2080d9ed28
parent 19274 b85e16bd70d0
child 19371 32fc9743803a
equal deleted inserted replaced
19309:8ea43e9ad83a 19310:9b2080d9ed28
   308 
   308 
   309 
   309 
   310 
   310 
   311 (** pretty printing **)
   311 (** pretty printing **)
   312 
   312 
       
   313 local
       
   314 
   313 fun pretty_term' abbrevs ctxt t =
   315 fun pretty_term' abbrevs ctxt t =
   314   let
   316   let
   315     val thy = theory_of ctxt;
   317     val thy = theory_of ctxt;
   316     val syntax = syntax_of ctxt;
   318     val syntax = syntax_of ctxt;
   317     val consts = consts_of ctxt;
   319     val consts = consts_of ctxt;
   318     val t' = t
   320     val t' = t
   319       |> K abbrevs ? Pattern.rewrite_term thy (Consts.abbrevs_of consts) []
   321       |> K abbrevs ? Pattern.rewrite_term thy (Consts.abbrevs_of consts) []
   320       |> LocalSyntax.extern_term (NameSpace.extern (Consts.space_of consts)) thy syntax;
   322       |> LocalSyntax.extern_term (NameSpace.extern (Consts.space_of consts)) thy syntax;
   321   in Sign.pretty_term' (LocalSyntax.syn_of syntax) (Context.Proof ctxt) t' end;
   323   in Sign.pretty_term' (LocalSyntax.syn_of syntax) (Context.Proof ctxt) t' end;
   322 
   324 
       
   325 in
       
   326 
   323 val pretty_term = pretty_term' true;
   327 val pretty_term = pretty_term' true;
       
   328 val pretty_term_no_abbrevs = pretty_term' false;
       
   329 
       
   330 end;
       
   331 
   324 fun pretty_typ ctxt T = Sign.pretty_typ (theory_of ctxt) T;
   332 fun pretty_typ ctxt T = Sign.pretty_typ (theory_of ctxt) T;
   325 fun pretty_sort ctxt S = Sign.pretty_sort (theory_of ctxt) S;
   333 fun pretty_sort ctxt S = Sign.pretty_sort (theory_of ctxt) S;
   326 fun pretty_classrel ctxt cs = Sign.pretty_classrel (theory_of ctxt) cs;
   334 fun pretty_classrel ctxt cs = Sign.pretty_classrel (theory_of ctxt) cs;
   327 fun pretty_arity ctxt ar = Sign.pretty_arity (theory_of ctxt) ar;
   335 fun pretty_arity ctxt ar = Sign.pretty_arity (theory_of ctxt) ar;
   328 
   336 
   340       Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, pretty_thm ctxt th]
   348       Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, pretty_thm ctxt th]
   341   | pretty_fact ctxt (a, ths) =
   349   | pretty_fact ctxt (a, ths) =
   342       Pretty.block (Pretty.fbreaks (Pretty.str (a ^ ":") :: map (pretty_thm ctxt) ths));
   350       Pretty.block (Pretty.fbreaks (Pretty.str (a ^ ":") :: map (pretty_thm ctxt) ths));
   343 
   351 
   344 fun pretty_proof ctxt prf =
   352 fun pretty_proof ctxt prf =
   345   pretty_term' true (ctxt |> transfer_syntax (ProofSyntax.proof_syntax prf (theory_of ctxt)))
   353   pretty_term_no_abbrevs (ctxt |> transfer_syntax (ProofSyntax.proof_syntax prf (theory_of ctxt)))
   346     (ProofSyntax.term_of_proof prf);
   354     (ProofSyntax.term_of_proof prf);
   347 
   355 
   348 fun pretty_proof_of ctxt full th =
   356 fun pretty_proof_of ctxt full th =
   349   pretty_proof ctxt (ProofSyntax.proof_of full th);
   357   pretty_proof ctxt (ProofSyntax.proof_of full th);
   350 
   358 
   700 
   708 
   701 (* generalize type variables *)
   709 (* generalize type variables *)
   702 
   710 
   703 fun generalize_tfrees inner outer =
   711 fun generalize_tfrees inner outer =
   704   let
   712   let
   705     val extra_fixes = fixed_names_of inner \\ fixed_names_of outer;
   713     val extra_fixes = subtract (op =) (fixed_names_of outer) (fixed_names_of inner);
   706     fun still_fixed (Free (x, _)) = not (member (op =) extra_fixes x)
   714     fun still_fixed (Free (x, _)) = not (member (op =) extra_fixes x)
   707       | still_fixed _ = false;
   715       | still_fixed _ = false;
   708     val occs_inner = type_occs_of inner;
   716     val occs_inner = type_occs_of inner;
   709     val occs_outer = type_occs_of outer;
   717     val occs_outer = type_occs_of outer;
   710     fun add a gen =
   718     fun add a gen =
   744 (** export theorems **)
   752 (** export theorems **)
   745 
   753 
   746 fun common_exports is_goal inner outer =
   754 fun common_exports is_goal inner outer =
   747   let
   755   let
   748     val gen = generalize_tfrees inner outer;
   756     val gen = generalize_tfrees inner outer;
   749     val fixes = fixed_names_of inner \\ fixed_names_of outer;
   757     val fixes = subtract (op =) (fixed_names_of outer) (fixed_names_of inner);
   750     val asms = Library.drop (length (assumptions_of outer), assumptions_of inner);
   758     val asms = Library.drop (length (assumptions_of outer), assumptions_of inner);
   751     val exp_asms = map (fn (cprops, exp) => exp is_goal cprops) asms;
   759     val exp_asms = map (fn (cprops, exp) => exp is_goal cprops) asms;
   752   in
   760   in
   753     Goal.norm_hhf_protect
   761     Goal.norm_hhf_protect
   754     #> Seq.EVERY (rev exp_asms)
   762     #> Seq.EVERY (rev exp_asms)
  1359       | local_abbrev (c, (T, SOME t)) =
  1367       | local_abbrev (c, (T, SOME t)) =
  1360           if Symtab.defined globals c then I else cons (c, Logic.mk_equals (Const (c, T), t));
  1368           if Symtab.defined globals c then I else cons (c, Logic.mk_equals (Const (c, T), t));
  1361     val abbrevs = NameSpace.extern_table (space, Symtab.make (Symtab.fold local_abbrev consts []));
  1369     val abbrevs = NameSpace.extern_table (space, Symtab.make (Symtab.fold local_abbrev consts []));
  1362   in
  1370   in
  1363     if null abbrevs andalso not (! verbose) then []
  1371     if null abbrevs andalso not (! verbose) then []
  1364     else [Pretty.big_list "abbreviations:" (map (pretty_term' false ctxt o #2) abbrevs)]
  1372     else [Pretty.big_list "abbreviations:" (map (pretty_term_no_abbrevs ctxt o #2) abbrevs)]
  1365   end;
  1373   end;
  1366 
  1374 
  1367 
  1375 
  1368 (* term bindings *)
  1376 (* term bindings *)
  1369 
  1377 
  1370 fun pretty_binds ctxt =
  1378 fun pretty_binds ctxt =
  1371   let
  1379   let
  1372     val binds = binds_of ctxt;
  1380     val binds = binds_of ctxt;
  1373     fun prt_bind (xi, (T, t)) = pretty_term' false ctxt (Logic.mk_equals (Var (xi, T), t));
  1381     fun prt_bind (xi, (T, t)) = pretty_term_no_abbrevs ctxt (Logic.mk_equals (Var (xi, T), t));
  1374   in
  1382   in
  1375     if Vartab.is_empty binds andalso not (! verbose) then []
  1383     if Vartab.is_empty binds andalso not (! verbose) then []
  1376     else [Pretty.big_list "term bindings:" (map prt_bind (Vartab.dest binds))]
  1384     else [Pretty.big_list "term bindings:" (map prt_bind (Vartab.dest binds))]
  1377   end;
  1385   end;
  1378 
  1386