# HG changeset patch # User wenzelm # Date 1320871446 -3600 # Node ID 924c2f6dcd05c2e8a2f2568881405739104e9ed8 # Parent b8eb7a791dacd270c6b4fcd00ab537403ac8dae0 misc tuning and simplification; diff -r b8eb7a791dac -r 924c2f6dcd05 src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Wed Nov 09 21:36:18 2011 +0100 +++ b/src/Pure/Isar/class_declaration.ML Wed Nov 09 21:44:06 2011 +0100 @@ -41,7 +41,8 @@ val (([raw_props], [(_, raw_inst_morph)], export_morph), _) = empty_ctxt |> Expression.cert_goal_expression ([(class, (("", false), Expression.Named param_map_const))], []); - val (props, inst_morph) = if null param_map + val (props, inst_morph) = + if null param_map then (raw_props |> map (Morphism.term typ_morph), raw_inst_morph $> typ_morph) else (raw_props, raw_inst_morph); (*FIXME proper handling in @@ -49,13 +50,15 @@ (* witness for canonical interpretation *) val prop = try the_single props; - val wit = Option.map (fn prop => let + val wit = Option.map (fn prop => + let val sup_axioms = map_filter (fst o Class.rules thy) sups; - val loc_intro_tac = case Locale.intros_of thy class - of (_, NONE) => all_tac - | (_, SOME intro) => ALLGOALS (Tactic.rtac intro); + val loc_intro_tac = + (case Locale.intros_of thy class of + (_, NONE) => all_tac + | (_, SOME intro) => ALLGOALS (Tactic.rtac intro)); val tac = loc_intro_tac - THEN ALLGOALS (Proof_Context.fact_tac (sup_axioms @ the_list assm_axiom)) + THEN ALLGOALS (Proof_Context.fact_tac (sup_axioms @ the_list assm_axiom)); in Element.prove_witness empty_ctxt prop tac end) prop; val axiom = Option.map Element.conclude_witness wit; @@ -69,9 +72,10 @@ fun prove_assm_intro thm = let val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt; - val const_eq_morph = case eq_morph - of SOME eq_morph => const_morph $> eq_morph - | NONE => const_morph + val const_eq_morph = + (case eq_morph of + SOME eq_morph => const_morph $> eq_morph + | NONE => const_morph); val thm'' = Morphism.thm const_eq_morph thm'; val tac = ALLGOALS (Proof_Context.fact_tac [thm'']); in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end; @@ -80,17 +84,19 @@ (* of_class *) val of_class_prop_concl = Logic.mk_of_class (aT, class); - val of_class_prop = case prop of NONE => of_class_prop_concl + val of_class_prop = + (case prop of + NONE => of_class_prop_concl | SOME prop => Logic.mk_implies (Morphism.term const_morph - ((map_types o map_atyps) (K aT) prop), of_class_prop_concl); + ((map_types o map_atyps) (K aT) prop), of_class_prop_concl)); val sup_of_classes = map (snd o Class.rules thy) sups; val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class); val axclass_intro = #intro (AxClass.get_info thy class); val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort); - val tac = REPEAT (SOMEGOAL - (Tactic.match_tac (axclass_intro :: sup_of_classes - @ loc_axiom_intros @ base_sort_trivs) - ORELSE' Tactic.assume_tac)); + val tac = + REPEAT (SOMEGOAL + (Tactic.match_tac (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs) + ORELSE' Tactic.assume_tac)); val of_class = Skip_Proof.prove_global thy [] [] of_class_prop (K tac); in (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) end; @@ -110,8 +116,8 @@ val base_constraints = (map o apsnd) (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd) (Class.these_operations thy sups); - val reject_bcd_etc = (map o map_atyps) (fn T as TFree (v, sort) => - if v = Name.aT then T + val reject_bcd_etc = (map o map_atyps) (fn T as TFree (a, _) => + if a = Name.aT then T else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification") | T => T); fun singleton_fixate Ts = @@ -123,22 +129,26 @@ if null tfrees then inferred_sort else (case tfrees of - [(_, a_sort)] => if Sorts.sort_le algebra (a_sort, inferred_sort) - then inter_sort a_sort inferred_sort - else error ("Type inference imposes additional sort constraint " - ^ Syntax.string_of_sort_global thy inferred_sort - ^ " of type parameter " ^ Name.aT ^ " of sort " - ^ Syntax.string_of_sort_global thy a_sort) + [(_, a_sort)] => + if Sorts.sort_le algebra (a_sort, inferred_sort) then + inter_sort a_sort inferred_sort + else + error ("Type inference imposes additional sort constraint " ^ + Syntax.string_of_sort_global thy inferred_sort ^ + " of type parameter " ^ Name.aT ^ " of sort " ^ + Syntax.string_of_sort_global thy a_sort) | _ => error "Multiple type variables in class specification"); in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end; fun after_infer_fixate Ts = let - val sort' = (fold o fold_atyps) (fn T as TFree _ => I | T as TVar (vi, sort) => - if Type_Infer.is_param vi then inter_sort sort else I) Ts []; + val S' = + (fold o fold_atyps) + (fn TVar (xi, S) => if Type_Infer.is_param xi then inter_sort S else I | _ => I) Ts []; in (map o map_atyps) - (fn T as TFree _ => T | T as TVar (vi, _) => - if Type_Infer.is_param vi then Type_Infer.param 0 (Name.aT, sort') else T) Ts + (fn T as TVar (xi, _) => + if Type_Infer.is_param xi then Type_Infer.param 0 (Name.aT, S') else T + | T => T) Ts end; (* preprocessing elements, retrieving base sort from type-checked elements *) @@ -193,38 +203,39 @@ (* prepare import *) val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy)); - val sups = map (prep_class thy) raw_supclasses - |> Sign.minimize_sort thy; - val _ = case filter_out (Class.is_class thy) sups - of [] => () - | no_classes => error ("No (proper) classes: " ^ commas (map quote no_classes)); + val sups = Sign.minimize_sort thy (map (prep_class thy) raw_supclasses); + val _ = + (case filter_out (Class.is_class thy) sups of + [] => () + | no_classes => error ("No (proper) classes: " ^ commas_quote no_classes)); val raw_supparams = (map o apsnd) (snd o snd) (Class.these_params thy sups); val raw_supparam_names = map fst raw_supparams; - val _ = if has_duplicates (op =) raw_supparam_names - then error ("Duplicate parameter(s) in superclasses: " - ^ (commas o map quote o duplicates (op =)) raw_supparam_names) + val _ = + if has_duplicates (op =) raw_supparam_names then + error ("Duplicate parameter(s) in superclasses: " ^ + (commas_quote (duplicates (op =) raw_supparam_names))) else (); (* infer types and base sort *) - val (base_sort, supparam_names, supexpr, inferred_elems) = - prep_class_elems thy sups raw_elems; + val (base_sort, supparam_names, supexpr, inferred_elems) = prep_class_elems thy sups raw_elems; val sup_sort = inter_sort base_sort sups; (* process elements as class specification *) val class_ctxt = Class.begin sups base_sort (Proof_Context.init_global thy); val ((_, _, syntax_elems), _) = class_ctxt |> Expression.cert_declaration supexpr I inferred_elems; - fun check_vars e vs = if null vs - then error ("No type variable in part of specification element " - ^ (Pretty.string_of o Pretty.chunks) (Element.pretty_ctxt class_ctxt e)) + fun check_vars e vs = + if null vs then + error ("No type variable in part of specification element " ^ + Pretty.string_of (Pretty.chunks (Element.pretty_ctxt class_ctxt e))) else (); fun check_element (e as Element.Fixes fxs) = - map (fn (_, SOME T, _) => check_vars e (Term.add_tfreesT T [])) fxs + List.app (fn (_, SOME T, _) => check_vars e (Term.add_tfreesT T [])) fxs | check_element (e as Element.Assumes assms) = - maps (fn (_, ts_pss) => map - (fn (t, _) => check_vars e (Term.add_tfrees t [])) ts_pss) assms - | check_element e = [()]; - val _ = map check_element syntax_elems; + List.app (fn (_, ts_pss) => + List.app (fn (t, _) => check_vars e (Term.add_tfrees t [])) ts_pss) assms + | check_element _ = (); + val _ = List.app check_element syntax_elems; fun fork_syn (Element.Fixes xs) = fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs #>> Element.Fixes @@ -278,9 +289,10 @@ val raw_pred = Locale.intros_of thy class |> fst |> Option.map (Logic.unvarify_global o Logic.strip_imp_concl o Thm.prop_of); - fun get_axiom thy = case (#axioms o AxClass.get_info thy) class - of [] => NONE - | [thm] => SOME thm; + fun get_axiom thy = + (case #axioms (AxClass.get_info thy class) of + [] => NONE + | [thm] => SOME thm); in thy |> add_consts class base_sort sups supparam_names global_syntax @@ -331,9 +343,10 @@ let val thy = Proof_Context.theory_of lthy; val proto_sup = prep_class thy raw_sup; - val proto_sub = case Named_Target.peek lthy - of SOME {target, is_class = true, ...} => target - | _ => error "Not in a class target"; + val proto_sub = + (case Named_Target.peek lthy of + SOME {target, is_class = true, ...} => target + | _ => error "Not in a class target"); val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup); val expr = ([(sup, (("", false), Expression.Positional []))], []);