# HG changeset patch # User haftmann # Date 1193333273 -7200 # Node ID 62638dcafe385e3840b2b93632475704456c1fd7 # Parent 37a1743f0fc3f5b3f22ba32cf2df4b228b9d5c8e fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc. diff -r 37a1743f0fc3 -r 62638dcafe38 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Thu Oct 25 19:27:52 2007 +0200 +++ b/src/Pure/Isar/class.ML Thu Oct 25 19:27:53 2007 +0200 @@ -26,6 +26,8 @@ val refresh_syntax: class -> Proof.context -> Proof.context val intro_classes_tac: thm list -> tactic val default_intro_classes_tac: thm list -> tactic + val prove_subclass: class * class -> thm list -> Proof.context + -> theory -> theory val print_classes: theory -> unit val uncheck: bool ref @@ -61,6 +63,13 @@ (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE) #> ProofContext.theory_of; +fun prove_interpretation_in tac after_qed (name, expr) = + Locale.interpretation_in_locale + (ProofContext.theory after_qed) (name, expr) + #> Proof.global_terminal_proof + (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE) + #> ProofContext.theory_of; + fun OF_LAST thm1 thm2 = thm1 RSN (Thm.nprems_of thm2, thm2); fun strip_all_ofclass thy sort = @@ -315,29 +324,31 @@ (*partial morphism of canonical interpretation*) intro: thm, defs: thm list, - operations: (string * ((term * (typ * int)) * (term * typ))) list - (*constant name ~> ((locale term, - (constant constraint, instantiaton index of class typ)), locale term & typ for uncheck)*) + operations: (string * (term * (typ * int))) list, + (*constant name ~> (locale term, + (constant constraint, instantiaton index of class typ))*) + unchecks: (term * term) list }; fun rep_class_data (ClassData d) = d; fun mk_class_data ((consts, base_sort, inst, morphism, intro), - (defs, operations)) = + (defs, (operations, unchecks))) = ClassData { consts = consts, base_sort = base_sort, inst = inst, morphism = morphism, intro = intro, defs = defs, - operations = operations }; + operations = operations, unchecks = unchecks }; fun map_class_data f (ClassData { consts, base_sort, inst, morphism, intro, - defs, operations }) = + defs, operations, unchecks }) = mk_class_data (f ((consts, base_sort, inst, morphism, intro), - (defs, operations))); + (defs, (operations, unchecks)))); fun merge_class_data _ (ClassData { consts = consts, base_sort = base_sort, inst = inst, morphism = morphism, intro = intro, - defs = defs1, operations = operations1 }, + defs = defs1, operations = operations1, unchecks = unchecks1 }, ClassData { consts = _, base_sort = _, inst = _, morphism = _, intro = _, - defs = defs2, operations = operations2 }) = + defs = defs2, operations = operations2, unchecks = unchecks2 }) = mk_class_data ((consts, base_sort, inst, morphism, intro), (Thm.merge_thms (defs1, defs2), - AList.merge (op =) (K true) (operations1, operations2))); + (AList.merge (op =) (K true) (operations1, operations2), + Library.merge (op aconv o pairself snd) (unchecks1, unchecks2)))); structure ClassData = TheoryDataFun ( @@ -383,7 +394,8 @@ fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy; -fun local_operation thy = AList.lookup (op =) o these_operations thy; +fun these_unchecks thy = + maps (#unchecks o the_class_data thy) o ancestry thy; fun sups_base_sort thy sort = let @@ -435,30 +447,35 @@ fun add_class_data ((class, superclasses), (cs, base_sort, inst, phi, intro)) thy = let - val operations = map (fn (v_ty as (_, ty'), (c, ty)) => - (c, ((Free v_ty, (Logic.varifyT ty, 0)), (Free v_ty, ty')))) cs; + val operations = map (fn (v_ty, (c, ty)) => + (c, ((Free v_ty, (Logic.varifyT ty, 0))))) cs; + val unchecks = map (fn ((v, ty'), (c, _)) => + (Free (v, Type.strip_sorts ty'), Const (c, Type.strip_sorts ty'))) cs; val cs = (map o pairself) fst cs; val add_class = Graph.new_node (class, - mk_class_data ((cs, base_sort, map (SOME o Const) inst, phi, intro), ([], operations))) + mk_class_data ((cs, base_sort, map (SOME o Const) inst, phi, intro), ([], (operations, unchecks)))) #> fold (curry Graph.add_edge class) superclasses; in ClassData.map add_class thy end; -fun register_operation class ((c, (t, t_rev)), some_def) thy = +fun register_operation class (c, ((t, some_t_rev), some_def)) thy = let val ty = Sign.the_const_constraint thy c; val typargs = Sign.const_typargs thy (c, ty); val typidx = find_index (fn TVar ((v, _), _) => Name.aT = v | _ => false) typargs; - val t_rev' = (map_types o map_atyps) - (fn ty as TFree (v, _) => if Name.aT = v then TFree (v, []) else ty | ty => ty) t_rev; - val ty' = Term.fastype_of t_rev'; + fun mk_uncheck t_rev = + let + val t_rev' = map_types Type.strip_sorts t_rev; + val ty' = Term.fastype_of t_rev'; + in (t_rev', Const (c, ty')) end; + val some_t_rev' = Option.map mk_uncheck some_t_rev; in thy |> (ClassData.map o Graph.map_node class o map_class_data o apsnd) - (fn (defs, operations) => + (fn (defs, (operations, unchecks)) => (fold cons (the_list some_def) defs, - (c, ((t, (ty, typidx)), (t_rev', ty'))) :: operations)) + ((c, (t, (ty, typidx))) :: operations, fold cons (the_list some_t_rev') unchecks))) end; @@ -550,6 +567,56 @@ ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule")]); +fun subclass_rule thy (sub, sup) = + let + val ctxt = Locale.init sub thy; + val ctxt_thy = ProofContext.init thy; + val props = + Locale.global_asms_of thy sup + |> maps snd + |> map (ObjectLogic.ensure_propT thy); + fun tac { prems, context } = + Locale.intro_locales_tac true context prems + ORELSE ALLGOALS assume_tac; + in + Goal.prove_multi ctxt [] [] props tac + |> map (Assumption.export false ctxt ctxt_thy) + |> Variable.export ctxt ctxt_thy + end; + +fun prove_single_subclass (sub, sup) thms ctxt thy = + let + val ctxt_thy = ProofContext.init thy; + val subclass_rule = Conjunction.intr_balanced thms + |> Assumption.export false ctxt ctxt_thy + |> singleton (Variable.export ctxt ctxt_thy); + val sub_inst = Thm.ctyp_of thy (TVar ((Name.aT, 0), [sub])); + val sub_ax = #axioms (AxClass.get_info thy sub); + val classrel = + #intro (AxClass.get_info thy sup) + |> Drule.instantiate' [SOME sub_inst] [] + |> OF_LAST (subclass_rule OF sub_ax) + |> strip_all_ofclass thy (Sign.super_classes thy sup) + |> Thm.strip_shyps + in + thy + |> AxClass.add_classrel classrel + |> prove_interpretation_in (ALLGOALS (ProofContext.fact_tac thms)) + I (sub, Locale.Locale sup) + |> ClassData.map (Graph.add_edge (sub, sup)) + end; + +fun prove_subclass (sub, sup) thms ctxt thy = + let + val supclasses = Sign.complete_sort thy [sup] + |> filter_out (fn class => Sign.subsort thy ([sub], [class])); + fun transform sup' = subclass_rule thy (sup, sup') |> map (fn thm => thm OF thms); + in + thy + |> fold_rev (fn sup' => prove_single_subclass (sub, sup') + (transform sup') ctxt) supclasses + end; + (** classes and class target **) @@ -560,7 +627,7 @@ constraints: (string * typ) list, base_sort: sort, local_operation: string * typ -> (typ * term) option, - rews: (term * term) list, + unchecks: (term * term) list, passed: bool } option; fun init _ = NONE; @@ -568,27 +635,30 @@ fun synchronize_syntax thy sups base_sort ctxt = let + (* constraints *) val operations = these_operations thy sups; - - (* constraints *) - fun local_constraint (c, ((_, (ty, _)),_ )) = + fun local_constraint (c, (_, (ty, _))) = let val ty' = ty |> map_atyps (fn ty as TVar ((v, 0), _) => if v = Name.aT then TVar ((v, 0), base_sort) else ty) |> SOME; in (c, ty') end - val constraints = (map o apsnd) (fst o snd o fst) operations; + val constraints = (map o apsnd) (fst o snd) operations; (* check phase *) val typargs = Consts.typargs (ProofContext.consts_of ctxt); - fun check_const (c, ty) ((t, (_, idx)), _) = + fun check_const (c, ty) (t, (_, idx)) = ((nth (typargs (c, ty)) idx), t); fun local_operation (c_ty as (c, _)) = AList.lookup (op =) operations c |> Option.map (check_const c_ty); (* uncheck phase *) - val rews = map (fn (c, (_, (t, ty))) => (t, Const (c, ty))) operations; + val basify = + map_atyps (fn ty as TFree (v, _) => if Name.aT = v then TFree (v, base_sort) + else ty | ty => ty); + val unchecks = these_unchecks thy sups + |> (map o pairself o map_types) basify; in ctxt |> fold (ProofContext.add_const_constraint o local_constraint) operations @@ -596,7 +666,7 @@ constraints = constraints, base_sort = base_sort, local_operation = local_operation, - rews = rews, + unchecks = unchecks, passed = false })) end; @@ -608,9 +678,9 @@ in synchronize_syntax thy [class] base_sort ctxt end; val mark_passed = (ClassSyntax.map o Option.map) - (fn { constraints, base_sort, local_operation, rews, passed } => + (fn { constraints, base_sort, local_operation, unchecks, passed } => { constraints = constraints, base_sort = base_sort, - local_operation = local_operation, rews = rews, passed = true }); + local_operation = local_operation, unchecks = unchecks, passed = true }); fun sort_term_check ts ctxt = let @@ -647,9 +717,9 @@ let (*FIXME abbreviations*) val thy = ProofContext.theory_of ctxt; - val rews = (#rews o the o ClassSyntax.get) ctxt; + val unchecks = (#unchecks o the o ClassSyntax.get) ctxt; val ts' = if ! uncheck - then map (Pattern.rewrite_term thy rews []) ts else ts; + then map (Pattern.rewrite_term thy unchecks []) ts else ts; in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end; fun init_ctxt thy sups base_sort ctxt = @@ -802,6 +872,7 @@ val prfx = class_prefix class; val thy' = thy |> Sign.add_path prfx; val phi = morphism thy' class; + val base_sort = (#base_sort o the_class_data thy) class; val c' = Sign.full_name thy' c; val dict' = (map_types Logic.unvarifyT o Morphism.term phi) dict; @@ -817,7 +888,7 @@ |> Thm.add_def false (c, def_eq) |>> Thm.symmetric |-> (fn def => class_interpretation class [def] [Thm.prop_of def] - #> register_operation class ((c', (dict, dict')), SOME (Thm.varifyT def))) + #> register_operation class (c', ((dict, SOME dict'), SOME (Thm.varifyT def)))) |> Sign.restore_naming thy |> Sign.add_const_constraint (c', SOME ty') end; @@ -834,8 +905,7 @@ val c' = Sign.full_name thy' c; val rews = map (Logic.dest_equals o Thm.prop_of) (these_defs thy' [class]) val rhs' = (Pattern.rewrite_term thy rews [] o Morphism.term phi) rhs; - val rhs'' = map_types Logic.unvarifyT rhs'; - val ty' = Term.fastype_of rhs''; + val ty' = (Logic.unvarifyT o Term.fastype_of) rhs'; val c'' = NameSpace.full (Sign.naming_of thy' |> NameSpace.add_path prfx) c; val ty'' = (Type.strip_sorts o Logic.unvarifyT) (Sign.the_const_constraint thy' c''); @@ -846,7 +916,7 @@ |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs') |> snd |> Sign.add_const_constraint (c', SOME ty') |> Sign.notation true prmode [(Const (c', ty'), mx)] - |> register_operation class ((c', (rhs, rhs'')), NONE) + |> register_operation class (c', ((rhs, NONE), NONE)) |> Sign.restore_naming thy end;