src/Pure/axclass.ML
changeset 11969 c850db2e2e98
parent 11828 ef3e51b1b4ec
child 12004 1703de633aaf
     1.1 --- a/src/Pure/axclass.ML	Sat Oct 27 23:17:46 2001 +0200
     1.2 +++ b/src/Pure/axclass.ML	Sat Oct 27 23:18:40 2001 +0200
     1.3 @@ -26,12 +26,6 @@
     1.4    val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory
     1.5    val default_intro_classes_tac: thm list -> int -> tactic
     1.6    val axclass_tac: thm list -> tactic
     1.7 -  val prove_subclass: theory -> class * class -> thm list
     1.8 -    -> tactic option -> thm
     1.9 -  val prove_arity: theory -> string * sort list * class -> thm list
    1.10 -    -> tactic option -> thm
    1.11 -  val goal_subclass: theory -> xclass * xclass -> thm list
    1.12 -  val goal_arity: theory -> xstring * string list * xclass -> thm list
    1.13    val instance_subclass_proof: (xclass * xclass) * Comment.text -> bool -> theory -> ProofHistory.T
    1.14    val instance_subclass_proof_i: (class * class) * Comment.text -> bool -> theory -> ProofHistory.T
    1.15    val instance_arity_proof: (xstring * string list * xclass) * Comment.text
    1.16 @@ -349,24 +343,16 @@
    1.17  
    1.18  (* provers *)
    1.19  
    1.20 -fun prove mk_prop str_of thy sig_prop thms usr_tac =
    1.21 -  let
    1.22 -    val sign = Theory.sign_of thy;
    1.23 -    val goal = Thm.cterm_of sign (mk_prop sig_prop)
    1.24 -      handle TERM (msg, _) => error msg
    1.25 -        | TYPE (msg, _, _) => error msg;
    1.26 -    val tac = axclass_tac thms THEN (if_none usr_tac all_tac);
    1.27 -  in
    1.28 -    prove_goalw_cterm [] goal (K [tac])
    1.29 -  end
    1.30 -  handle ERROR => error ("The error(s) above occurred while trying to prove "
    1.31 -    ^ quote (str_of (Theory.sign_of thy, sig_prop)));
    1.32 +fun prove mk_prop str_of sign prop thms usr_tac =
    1.33 +  (Tactic.prove sign [] [] (mk_prop prop) (K (axclass_tac thms THEN (if_none usr_tac all_tac)))
    1.34 +    handle ERROR => error ("The error(s) above occurred while trying to prove " ^
    1.35 +     quote (str_of sign prop))) |> Drule.standard;
    1.36  
    1.37  val prove_subclass =
    1.38 -  prove mk_classrel (fn (sg, c1_c2) => Sign.str_of_classrel sg c1_c2);
    1.39 +  prove mk_classrel (fn sg => fn c1_c2 => Sign.str_of_classrel sg c1_c2);
    1.40  
    1.41  val prove_arity =
    1.42 -  prove mk_arity (fn (sg, (t, Ss, c)) => Sign.str_of_arity sg (t, Ss, [c]));
    1.43 +  prove mk_arity (fn sg => fn (t, Ss, c) => Sign.str_of_arity sg (t, Ss, [c]));
    1.44  
    1.45  
    1.46  
    1.47 @@ -400,10 +386,12 @@
    1.48  (* old-style instance declarations *)
    1.49  
    1.50  fun ext_inst_subclass prep_classrel raw_c1_c2 names thms usr_tac thy =
    1.51 -  let val c1_c2 = prep_classrel (Theory.sign_of thy) raw_c1_c2 in
    1.52 -    message ("Proving class inclusion " ^
    1.53 -      quote (Sign.str_of_classrel (Theory.sign_of thy) c1_c2) ^ " ...");
    1.54 -    thy |> add_classrel_thms [prove_subclass thy c1_c2 (witnesses thy names thms) usr_tac]
    1.55 +  let
    1.56 +    val sign = Theory.sign_of thy;
    1.57 +    val c1_c2 = prep_classrel sign raw_c1_c2;
    1.58 +  in
    1.59 +    message ("Proving class inclusion " ^ quote (Sign.str_of_classrel sign c1_c2) ^ " ...");
    1.60 +    thy |> add_classrel_thms [prove_subclass sign c1_c2 (witnesses thy names thms) usr_tac]
    1.61    end;
    1.62  
    1.63  fun ext_inst_arity prep_arity (raw_t, raw_Ss, raw_cs) names thms usr_tac thy =
    1.64 @@ -414,7 +402,7 @@
    1.65      fun prove c =
    1.66       (message ("Proving type arity " ^
    1.67          quote (Sign.str_of_arity sign (t, Ss, [c])) ^ " ...");
    1.68 -        prove_arity thy (t, Ss, c) wthms usr_tac);
    1.69 +        prove_arity sign (t, Ss, c) wthms usr_tac);
    1.70    in add_arity_thms (map prove cs) thy end;
    1.71  
    1.72  fun sane_inst_subclass prep sub tac = ext_inst_subclass prep sub [] [] (Some tac);
    1.73 @@ -428,15 +416,6 @@
    1.74  val add_inst_arity_i = sane_inst_arity cert_arity;
    1.75  
    1.76  
    1.77 -(* make old-style interactive goals *)
    1.78 -
    1.79 -fun mk_goal mk_prop thy sig_prop =
    1.80 -  Goals.goalw_cterm [] (Thm.cterm_of (Theory.sign_of thy) (mk_prop (Theory.sign_of thy) sig_prop));
    1.81 -
    1.82 -val goal_subclass = mk_goal (mk_classrel oo read_classrel);
    1.83 -val goal_arity = mk_goal (mk_arity oo read_simple_arity);
    1.84 -
    1.85 -
    1.86  
    1.87  (** instance proof interfaces **)
    1.88  
    1.89 @@ -486,5 +465,4 @@
    1.90  
    1.91  end;
    1.92  
    1.93 -
    1.94  end;