src/Pure/axclass.ML
changeset 37249 8365cbc31349
parent 37246 b3ff14122645
child 38383 1ad96229b455
equal deleted inserted replaced
37246:b3ff14122645 37249:8365cbc31349
   410   end;
   410   end;
   411 
   411 
   412 
   412 
   413 (* primitive rules *)
   413 (* primitive rules *)
   414 
   414 
   415 fun gen_add_classrel store raw_th thy =
   415 fun add_classrel raw_th thy =
   416   let
   416   let
   417     val th = Thm.strip_shyps (Thm.transfer thy raw_th);
   417     val th = Thm.strip_shyps (Thm.transfer thy raw_th);
   418     val prop = Thm.plain_prop_of th;
   418     val prop = Thm.plain_prop_of th;
   419     fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
   419     fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
   420     val rel = Logic.dest_classrel prop handle TERM _ => err ();
   420     val rel = Logic.dest_classrel prop handle TERM _ => err ();
   421     val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
   421     val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
   422     val (th', thy') =
   422     val (th', thy') = PureThy.store_thm
   423       if store then PureThy.store_thm
   423       (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy;
   424         (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy
       
   425       else (th, thy);
       
   426     val th'' = th'
   424     val th'' = th'
   427       |> Thm.unconstrainT
   425       |> Thm.unconstrainT
   428       |> Drule.instantiate' [SOME (ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
   426       |> Drule.instantiate' [SOME (ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
   429   in
   427   in
   430     thy'
   428     thy'
   431     |> Sign.primitive_classrel (c1, c2)
   429     |> Sign.primitive_classrel (c1, c2)
   432     |> (#2 oo put_trancl_classrel) ((c1, c2), th'')
   430     |> (#2 oo put_trancl_classrel) ((c1, c2), th'')
   433     |> perhaps complete_arities
   431     |> perhaps complete_arities
   434   end;
   432   end;
   435 
   433 
   436 fun gen_add_arity store raw_th thy =
   434 fun add_arity raw_th thy =
   437   let
   435   let
   438     val th = Thm.strip_shyps (Thm.transfer thy raw_th);
   436     val th = Thm.strip_shyps (Thm.transfer thy raw_th);
   439     val prop = Thm.plain_prop_of th;
   437     val prop = Thm.plain_prop_of th;
   440     fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
   438     fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
   441     val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
   439     val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
   442 
   440 
   443     val (th', thy') =
   441     val (th', thy') = PureThy.store_thm
   444       if store then PureThy.store_thm
   442       (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy;
   445         (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy
       
   446       else (th, thy);
       
   447 
   443 
   448     val args = Name.names Name.context Name.aT Ss;
   444     val args = Name.names Name.context Name.aT Ss;
   449     val T = Type (t, map TFree args);
   445     val T = Type (t, map TFree args);
   450     val std_vars = map (fn (a, S) => SOME (ctyp_of thy' (TVar ((a, 0), [])))) args;
   446     val std_vars = map (fn (a, S) => SOME (ctyp_of thy' (TVar ((a, 0), [])))) args;
   451 
   447 
   461     |> fold (#2 oo declare_overloaded) missing_params
   457     |> fold (#2 oo declare_overloaded) missing_params
   462     |> Sign.primitive_arity (t, Ss, [c])
   458     |> Sign.primitive_arity (t, Ss, [c])
   463     |> put_arity ((t, Ss, c), th'')
   459     |> put_arity ((t, Ss, c), th'')
   464   end;
   460   end;
   465 
   461 
   466 val add_classrel = gen_add_classrel true;
       
   467 val add_arity = gen_add_arity true;
       
   468 
       
   469 
   462 
   470 (* tactical proofs *)
   463 (* tactical proofs *)
   471 
   464 
   472 fun prove_classrel raw_rel tac thy =
   465 fun prove_classrel raw_rel tac thy =
   473   let
   466   let
   475     val (c1, c2) = cert_classrel thy raw_rel;
   468     val (c1, c2) = cert_classrel thy raw_rel;
   476     val th = Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (K tac) handle ERROR msg =>
   469     val th = Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (K tac) handle ERROR msg =>
   477       cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
   470       cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
   478         quote (Syntax.string_of_classrel ctxt [c1, c2]));
   471         quote (Syntax.string_of_classrel ctxt [c1, c2]));
   479   in
   472   in
   480     thy
   473     thy |> add_classrel th
   481     |> PureThy.add_thms [((Binding.name
       
   482         (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])]
       
   483     |-> (fn [th'] => gen_add_classrel false th')
       
   484   end;
   474   end;
   485 
   475 
   486 fun prove_arity raw_arity tac thy =
   476 fun prove_arity raw_arity tac thy =
   487   let
   477   let
   488     val ctxt = ProofContext.init_global thy;
   478     val ctxt = ProofContext.init_global thy;
   492     val ths = Goal.prove_multi ctxt [] [] props
   482     val ths = Goal.prove_multi ctxt [] [] props
   493       (fn _ => Goal.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg =>
   483       (fn _ => Goal.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg =>
   494         cat_error msg ("The error(s) above occurred while trying to prove type arity " ^
   484         cat_error msg ("The error(s) above occurred while trying to prove type arity " ^
   495           quote (Syntax.string_of_arity ctxt arity));
   485           quote (Syntax.string_of_arity ctxt arity));
   496   in
   486   in
   497     thy
   487     thy |> fold add_arity ths
   498     |> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths))
       
   499     |-> fold (gen_add_arity false)
       
   500   end;
   488   end;
   501 
   489 
   502 
   490 
   503 
   491 
   504 (** class definitions **)
   492 (** class definitions **)
   611 (** axiomatizations **)
   599 (** axiomatizations **)
   612 
   600 
   613 local
   601 local
   614 
   602 
   615 (*old-style axioms*)
   603 (*old-style axioms*)
   616 fun add_axiom (b, prop) =
       
   617   Thm.add_axiom (b, prop) #->
       
   618   (fn (_, thm) => PureThy.add_thm ((b, Drule.export_without_context thm), []));
       
   619 
       
   620 fun axiomatize prep mk name add raw_args thy =
   604 fun axiomatize prep mk name add raw_args thy =
   621   let
   605   let
   622     val args = prep thy raw_args;
   606     val args = prep thy raw_args;
   623     val specs = mk args;
   607     val specs = mk args;
   624     val names = name args;
   608     val names = name args;
   625   in
   609   in
   626     thy
   610     thy
   627     |> fold_map add_axiom (map Binding.name names ~~ specs)
   611     |> fold_map Thm.add_axiom (map Binding.name names ~~ specs)
   628     |-> fold add
   612     |-> fold (add o Drule.export_without_context o snd)
   629   end;
   613   end;
   630 
   614 
   631 fun ax_classrel prep =
   615 fun ax_classrel prep =
   632   axiomatize (map o prep) (map Logic.mk_classrel)
   616   axiomatize (map o prep) (map Logic.mk_classrel)
   633     (map (prefix classrel_prefix o Logic.name_classrel)) (gen_add_classrel false);
   617     (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
   634 
   618 
   635 fun ax_arity prep =
   619 fun ax_arity prep =
   636   axiomatize (prep o ProofContext.init_global) Logic.mk_arities
   620   axiomatize (prep o ProofContext.init_global) Logic.mk_arities
   637     (map (prefix arity_prefix) o Logic.name_arities) (gen_add_arity false);
   621     (map (prefix arity_prefix) o Logic.name_arities) add_arity;
   638 
   622 
   639 fun class_const c =
   623 fun class_const c =
   640   (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);
   624   (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);
   641 
   625 
   642 fun ax_class prep_class prep_classrel (bclass, raw_super) thy =
   626 fun ax_class prep_class prep_classrel (bclass, raw_super) thy =