src/Pure/drule.ML
changeset 1218 59ed8ef1a3a1
parent 1194 563ecd14c1d8
child 1237 45ac644b0052
equal deleted inserted replaced
1217:f96a04c6b352 1218:59ed8ef1a3a1
   290 
   290 
   291 (*If false, hypotheses are printed as dots*)
   291 (*If false, hypotheses are printed as dots*)
   292 val show_hyps = ref true;
   292 val show_hyps = ref true;
   293 
   293 
   294 fun pretty_thm th =
   294 fun pretty_thm th =
   295 let val {sign, hyps, prop,...} = rep_thm th
   295   let
   296     val hsymbs = if null hyps then []
   296     val {sign, shyps, hyps, prop, ...} = rep_thm th;
   297                  else if !show_hyps then
   297     val hlen = length shyps + length hyps;
   298                       [Pretty.brk 2,
   298     val hsymbs =
   299                        Pretty.lst("[","]") (map (Sign.pretty_term sign) hyps)]
   299       if hlen = 0 then []
   300                  else Pretty.str" [" :: map (fn _ => Pretty.str".") hyps @
   300       else if ! show_hyps then
   301                       [Pretty.str"]"];
   301         [Pretty.brk 2, Pretty.list "[" "]"
   302 in Pretty.blk(0, Sign.pretty_term sign prop :: hsymbs) end;
   302           (map (Sign.pretty_term sign) hyps @ map Sign.pretty_sort shyps)]
       
   303       else
       
   304         [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ "]")];
       
   305   in
       
   306     Pretty.block (Sign.pretty_term sign prop :: hsymbs)
       
   307   end;
   303 
   308 
   304 val string_of_thm = Pretty.string_of o pretty_thm;
   309 val string_of_thm = Pretty.string_of o pretty_thm;
   305 
       
   306 val pprint_thm = Pretty.pprint o Pretty.quote o pretty_thm;
   310 val pprint_thm = Pretty.pprint o Pretty.quote o pretty_thm;
   307 
   311 
   308 
   312 
   309 (** Top-level commands for printing theorems **)
   313 (** Top-level commands for printing theorems **)
   310 val print_thm = writeln o string_of_thm;
   314 val print_thm = writeln o string_of_thm;
   530 
   534 
   531 
   535 
   532 (*Standard form of object-rule: no hypotheses, Frees, or outer quantifiers;
   536 (*Standard form of object-rule: no hypotheses, Frees, or outer quantifiers;
   533     all generality expressed by Vars having index 0.*)
   537     all generality expressed by Vars having index 0.*)
   534 fun standard th =
   538 fun standard th =
   535     let val {maxidx,...} = rep_thm th
   539   let val {maxidx,...} = rep_thm th
   536     in  varifyT (zero_var_indexes (forall_elim_vars(maxidx+1)
   540   in  
   537                          (forall_intr_frees(implies_intr_hyps th))))
   541     th |> implies_intr_hyps
   538     end;
   542     |> strip_shyps |> implies_intr_shyps
       
   543     |> forall_intr_frees |> forall_elim_vars (maxidx + 1)
       
   544     |> zero_var_indexes |> varifyT
       
   545   end;
       
   546 
   539 
   547 
   540 (*Assume a new formula, read following the same conventions as axioms.
   548 (*Assume a new formula, read following the same conventions as axioms.
   541   Generalizes over Free variables,
   549   Generalizes over Free variables,
   542   creates the assumption, and then strips quantifiers.
   550   creates the assumption, and then strips quantifiers.
   543   Example is [| ALL x:?A. ?P(x) |] ==> [| ?P(?a) |]
   551   Example is [| ALL x:?A. ?P(x) |] ==> [| ?P(?a) |]
   629 (** theorem equality test is exported and used by BEST_FIRST **)
   637 (** theorem equality test is exported and used by BEST_FIRST **)
   630 
   638 
   631 (*equality of theorems uses equality of signatures and
   639 (*equality of theorems uses equality of signatures and
   632   the a-convertible test for terms*)
   640   the a-convertible test for terms*)
   633 fun eq_thm (th1,th2) =
   641 fun eq_thm (th1,th2) =
   634     let val {sign=sg1, hyps=hyps1, prop=prop1, ...} = rep_thm th1
   642     let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1
   635         and {sign=sg2, hyps=hyps2, prop=prop2, ...} = rep_thm th2
   643         and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2
   636     in  Sign.eq_sg (sg1,sg2) andalso
   644     in  Sign.eq_sg (sg1,sg2) andalso
       
   645         eq_set (shyps1, shyps2) andalso
   637         aconvs(hyps1,hyps2) andalso
   646         aconvs(hyps1,hyps2) andalso
   638         prop1 aconv prop2
   647         prop1 aconv prop2
   639     end;
   648     end;
   640 
   649 
   641 (*Do the two theorems have the same signature?*)
   650 (*Do the two theorems have the same signature?*)