--- a/src/Pure/Isar/calculation.ML Tue Jan 10 19:33:35 2006 +0100
+++ b/src/Pure/Isar/calculation.ML Tue Jan 10 19:33:36 2006 +0100
@@ -7,23 +7,16 @@
signature CALCULATION =
sig
+ val print_rules: Context.generic -> unit
val get_calculation: Proof.state -> thm list option
- val print_global_rules: theory -> unit
- val print_local_rules: Proof.context -> unit
- val trans_add_global: theory attribute
- val trans_del_global: theory attribute
- val trans_add_local: Proof.context attribute
- val trans_del_local: Proof.context attribute
- val sym_add_global: theory attribute
- val sym_del_global: theory attribute
- val sym_add_local: Proof.context attribute
- val sym_del_local: Proof.context attribute
- val symmetric_global: theory attribute
- val symmetric_local: Proof.context attribute
+ val trans_add: Context.generic attribute
+ val trans_del: Context.generic attribute
+ val sym_add: Context.generic attribute
+ val sym_del: Context.generic attribute
+ val symmetric: Context.generic attribute
val also: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
- val finally: (thmref * Attrib.src list) list option -> bool ->
- Proof.state -> Proof.state Seq.seq
+ val finally: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
val moreover: bool -> Proof.state -> Proof.state
val ultimately: bool -> Proof.state -> Proof.state
@@ -32,112 +25,85 @@
structure Calculation: CALCULATION =
struct
-(** global and local calculation data **)
-
-(* global calculation *)
-
-fun print_rules prt x (trans, sym) =
- [Pretty.big_list "transitivity rules:" (map (prt x) (NetRules.rules trans)),
- Pretty.big_list "symmetry rules:" (map (prt x) sym)]
- |> Pretty.chunks |> Pretty.writeln;
-
-structure GlobalCalculation = TheoryDataFun
-(struct
- val name = "Isar/calculation";
- type T = thm NetRules.T * thm list
+(** calculation data **)
- val empty = (NetRules.elim, []);
- val copy = I;
- val extend = I;
- fun merge _ ((trans1, sym1), (trans2, sym2)) =
- (NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2));
- val print = print_rules Display.pretty_thm_sg;
-end);
-
-val _ = Context.add_setup [GlobalCalculation.init];
-val print_global_rules = GlobalCalculation.print;
-
-
-(* local calculation *)
-
-structure LocalCalculation = ProofDataFun
-(struct
+structure CalculationData = GenericDataFun
+(
val name = "Isar/calculation";
type T = (thm NetRules.T * thm list) * (thm list * int) option;
+ val empty = ((NetRules.elim, []), NONE);
+ val extend = I;
- fun init thy = (GlobalCalculation.get thy, NONE);
- fun print ctxt (rs, _) = print_rules ProofContext.pretty_thm ctxt rs;
-end);
+ fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) =
+ ((NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2)), NONE);
-val _ = Context.add_setup [LocalCalculation.init];
-val get_local_rules = #1 o LocalCalculation.get o Proof.context_of;
-val print_local_rules = LocalCalculation.print;
+ fun print generic ((trans, sym), _) =
+ let val ctxt = Context.proof_of generic in
+ [Pretty.big_list "transitivity rules:"
+ (map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)),
+ Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)]
+ |> Pretty.chunks |> Pretty.writeln
+ end;
+);
+
+val _ = Context.add_setup [CalculationData.init];
+val print_rules = CalculationData.print;
(* access calculation *)
fun get_calculation state =
- (case #2 (LocalCalculation.get (Proof.context_of state)) of
+ (case #2 (CalculationData.get (Context.Proof (Proof.context_of state))) of
NONE => NONE
| SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE);
val calculationN = "calculation";
fun put_calculation calc =
- `Proof.level #-> (fn lev => Proof.map_context
- (LocalCalculation.map (apsnd (K (Option.map (rpair lev) calc)))))
+ `Proof.level #-> (fn lev =>
+ Proof.map_context (Context.the_proof o
+ CalculationData.map (apsnd (K (Option.map (rpair lev) calc))) o Context.Proof))
#> Proof.put_thms (calculationN, calc);
+
(** attributes **)
(* add/del rules *)
-fun global_att f (x, thm) = (GlobalCalculation.map (f thm) x, thm);
-fun local_att f (x, thm) = (LocalCalculation.map (apfst (f thm)) x, thm);
+val trans_add = Attrib.declaration (CalculationData.map o apfst o apfst o NetRules.insert);
+val trans_del = Attrib.declaration (CalculationData.map o apfst o apfst o NetRules.delete);
-val trans_add_global = global_att (apfst o NetRules.insert);
-val trans_del_global = global_att (apfst o NetRules.delete);
-val trans_add_local = local_att (apfst o NetRules.insert);
-val trans_del_local = local_att (apfst o NetRules.delete);
-
-val sym_add_global = global_att (apsnd o Drule.add_rule) o ContextRules.elim_query_global NONE;
-val sym_del_global = global_att (apsnd o Drule.del_rule) o ContextRules.rule_del_global;
-val sym_add_local = local_att (apsnd o Drule.add_rule) o ContextRules.elim_query_local NONE;
-val sym_del_local = local_att (apsnd o Drule.del_rule) o ContextRules.rule_del_local;
+val sym_add =
+ Attrib.declaration (CalculationData.map o apfst o apsnd o Drule.add_rule)
+ #> ContextRules.elim_query NONE;
+val sym_del =
+ Attrib.declaration (CalculationData.map o apfst o apsnd o Drule.del_rule)
+ #> ContextRules.rule_del;
-(* symmetry *)
+(* symmetric *)
-fun gen_symmetric get_sym = Drule.rule_attribute (fn x => fn th =>
- (case Seq.chop (2, Drule.multi_resolves [th] (get_sym x)) of
+val symmetric = Attrib.rule (fn x => fn th =>
+ (case Seq.chop (2, Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of
([th'], _) => th'
| ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
| _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
-val symmetric_global = gen_symmetric (#2 o GlobalCalculation.get);
-val symmetric_local = gen_symmetric (#2 o #1 o LocalCalculation.get);
-
(* concrete syntax *)
-val trans_attr =
- (Attrib.add_del_args trans_add_global trans_del_global,
- Attrib.add_del_args trans_add_local trans_del_local);
-
-val sym_attr =
- (Attrib.add_del_args sym_add_global sym_del_global,
- Attrib.add_del_args sym_add_local sym_del_local);
+val trans_att = Attrib.add_del_args trans_add trans_del;
+val sym_att = Attrib.add_del_args sym_add sym_del;
val _ = Context.add_setup
[Attrib.add_attributes
- [("trans", trans_attr, "declaration of transitivity rule"),
- ("sym", sym_attr, "declaration of symmetry rule"),
- ("symmetric", (Attrib.no_args symmetric_global, Attrib.no_args symmetric_local),
- "resolution with symmetry rule")],
+ [("trans", Attrib.common trans_att, "declaration of transitivity rule"),
+ ("sym", Attrib.common sym_att, "declaration of symmetry rule"),
+ ("symmetric", Attrib.common (Attrib.no_args symmetric), "resolution with symmetry rule")],
snd o PureThy.add_thms
- [(("", transitive_thm), [trans_add_global]),
- (("", symmetric_thm), [sym_add_global])]];
+ [(("", transitive_thm), [Attrib.theory trans_add]),
+ (("", symmetric_thm), [Attrib.theory sym_add])]];
@@ -158,6 +124,8 @@
(* also and finally *)
+val get_rules = #1 o CalculationData.get o Context.Proof o Proof.context_of;
+
fun calculate prep_rules final raw_rules int state =
let
val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
@@ -168,8 +136,8 @@
fun combine ths =
(case opt_rules of SOME rules => rules
| NONE =>
- (case ths of [] => NetRules.rules (#1 (get_local_rules state))
- | th :: _ => NetRules.retrieve (#1 (get_local_rules state)) (strip_assums_concl th)))
+ (case ths of [] => NetRules.rules (#1 (get_rules state))
+ | th :: _ => NetRules.retrieve (#1 (get_rules state)) (strip_assums_concl th)))
|> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
|> Seq.filter (not o projection ths);
--- a/src/Pure/Isar/context_rules.ML Tue Jan 10 19:33:35 2006 +0100
+++ b/src/Pure/Isar/context_rules.ML Tue Jan 10 19:33:36 2006 +0100
@@ -15,40 +15,21 @@
val orderlist: ((int * int) * 'a) list -> 'a list
val find_rules_netpair: bool -> thm list -> term -> netpair -> thm list
val find_rules: bool -> thm list -> term -> ProofContext.context -> thm list list
- val print_global_rules: theory -> unit
- val print_local_rules: ProofContext.context -> unit
+ val print_rules: Context.generic -> unit
val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
val addWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
val Swrap: ProofContext.context -> (int -> tactic) -> int -> tactic
val wrap: ProofContext.context -> (int -> tactic) -> int -> tactic
- val intro_bang_global: int option -> theory attribute
- val elim_bang_global: int option -> theory attribute
- val dest_bang_global: int option -> theory attribute
- val intro_global: int option -> theory attribute
- val elim_global: int option -> theory attribute
- val dest_global: int option -> theory attribute
- val intro_query_global: int option -> theory attribute
- val elim_query_global: int option -> theory attribute
- val dest_query_global: int option -> theory attribute
- val rule_del_global: theory attribute
- val intro_bang_local: int option -> ProofContext.context attribute
- val elim_bang_local: int option -> ProofContext.context attribute
- val dest_bang_local: int option -> ProofContext.context attribute
- val intro_local: int option -> ProofContext.context attribute
- val elim_local: int option -> ProofContext.context attribute
- val dest_local: int option -> ProofContext.context attribute
- val intro_query_local: int option -> ProofContext.context attribute
- val elim_query_local: int option -> ProofContext.context attribute
- val dest_query_local: int option -> ProofContext.context attribute
- val rule_del_local: ProofContext.context attribute
- val addXIs_global: theory * thm list -> theory
- val addXEs_global: theory * thm list -> theory
- val addXDs_global: theory * thm list -> theory
- val delrules_global: theory * thm list -> theory
- val addXIs_local: ProofContext.context * thm list -> ProofContext.context
- val addXEs_local: ProofContext.context * thm list -> ProofContext.context
- val addXDs_local: ProofContext.context * thm list -> ProofContext.context
- val delrules_local: ProofContext.context * thm list -> ProofContext.context
+ val intro_bang: int option -> Context.generic attribute
+ val elim_bang: int option -> Context.generic attribute
+ val dest_bang: int option -> Context.generic attribute
+ val intro: int option -> Context.generic attribute
+ val elim: int option -> Context.generic attribute
+ val dest: int option -> Context.generic attribute
+ val intro_query: int option -> Context.generic attribute
+ val elim_query: int option -> Context.generic attribute
+ val dest_query: int option -> Context.generic attribute
+ val rule_del: Context.generic attribute
end;
structure ContextRules: CONTEXT_RULES =
@@ -78,7 +59,7 @@
val rule_indexes = distinct (map #1 rule_kinds);
-(* raw data *)
+(* context data *)
type netpair = ((int * int) * (bool * thm)) Net.net * ((int * int) * (bool * thm)) Net.net;
val empty_netpairs: netpair list = replicate (length rule_indexes) (Net.empty, Net.empty);
@@ -108,60 +89,45 @@
else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers
end;
-fun print_rules prt x (Rules {rules, ...}) =
- let
- fun prt_kind (i, b) =
- Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
- (List.mapPartial (fn (_, (k, th)) => if k = (i, b) then SOME (prt x th) else NONE)
- (sort (int_ord o pairself fst) rules));
- in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
-
-
-(* theory and proof data *)
-
-structure GlobalRulesArgs =
-struct
+structure Rules = GenericDataFun
+(
val name = "Isar/rules";
type T = T;
val empty = make_rules ~1 [] empty_netpairs ([], []);
- val copy = I;
val extend = I;
fun merge _ (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
let
- val wrappers = (gen_merge_lists' (eq_snd (op =)) ws1 ws2, gen_merge_lists' (eq_snd (op =)) ws1' ws2');
+ val wrappers =
+ (gen_merge_lists' (eq_snd (op =)) ws1 ws2, gen_merge_lists' (eq_snd (op =)) ws1' ws2');
val rules = gen_merge_lists' (fn ((_, (k1, th1)), (_, (k2, th2))) =>
k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) rules1 rules2;
val next = ~ (length rules);
val netpairs = Library.foldl (fn (nps, (n, (w, ((i, b), th)))) =>
nth_map i (curry insert_tagged_brl ((w, n), (b, th))) nps)
(empty_netpairs, next upto ~1 ~~ rules);
- in make_rules (next - 1) rules netpairs wrappers end;
-
- val print = print_rules Display.pretty_thm_sg;
-end;
-
-structure GlobalRules = TheoryDataFun(GlobalRulesArgs);
-val _ = Context.add_setup [GlobalRules.init];
-val print_global_rules = GlobalRules.print;
+ in make_rules (next - 1) rules netpairs wrappers end
-structure LocalRules = ProofDataFun
-(struct
- val name = GlobalRulesArgs.name;
- type T = GlobalRulesArgs.T;
- val init = GlobalRules.get;
- val print = print_rules ProofContext.pretty_thm;
-end);
+ fun print generic (Rules {rules, ...}) =
+ let
+ val ctxt = Context.proof_of generic;
+ fun prt_kind (i, b) =
+ Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
+ (List.mapPartial (fn (_, (k, th)) =>
+ if k = (i, b) then SOME (ProofContext.pretty_thm ctxt th) else NONE)
+ (sort (int_ord o pairself fst) rules));
+ in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
+);
-val _ = Context.add_setup [LocalRules.init];
-val print_local_rules = LocalRules.print;
+val _ = Context.add_setup [Rules.init];
+val print_rules = Rules.print;
(* access data *)
-fun netpairs ctxt = let val Rules {netpairs, ...} = LocalRules.get ctxt in netpairs end;
+fun netpairs ctxt = let val Rules {netpairs, ...} = Rules.get (Context.Proof ctxt) in netpairs end;
val netpair_bang = hd o netpairs;
val netpair = hd o tl o netpairs;
@@ -197,15 +163,16 @@
(* wrappers *)
-fun gen_add_wrapper upd w = GlobalRules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
- make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers));
+fun gen_add_wrapper upd w = Context.the_theory o
+ Rules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
+ make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers)) o Context.Theory;
val addSWrapper = gen_add_wrapper Library.apfst;
val addWrapper = gen_add_wrapper Library.apsnd;
fun gen_wrap which ctxt =
- let val Rules {wrappers, ...} = LocalRules.get ctxt
+ let val Rules {wrappers, ...} = Rules.get (Context.Proof ctxt)
in fold_rev fst (which wrappers) end;
val Swrap = gen_wrap #1;
@@ -217,57 +184,44 @@
(* add and del rules *)
-local
+fun rule_del (x, th) =
+ (Rules.map (del_rule th o del_rule (Tactic.make_elim th)) x, th);
-fun del map_data (x, th) =
- (map_data (del_rule th o del_rule (Tactic.make_elim th)) x, th);
+fun rule_add k view opt_w =
+ (fn (x, th) => (Rules.map (add_rule k opt_w (view th)) x, th)) o rule_del;
-fun add k view map_data opt_w =
- (fn (x, th) => (map_data (add_rule k opt_w (view th)) x, th)) o del map_data;
+val intro_bang = rule_add intro_bangK I;
+val elim_bang = rule_add elim_bangK I;
+val dest_bang = rule_add elim_bangK Tactic.make_elim;
+val intro = rule_add introK I;
+val elim = rule_add elimK I;
+val dest = rule_add elimK Tactic.make_elim;
+val intro_query = rule_add intro_queryK I;
+val elim_query = rule_add elim_queryK I;
+val dest_query = rule_add elim_queryK Tactic.make_elim;
-in
+val _ = Context.add_setup
+ [snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [Attrib.theory (intro_query NONE)])]];
+
-val intro_bang_global = add intro_bangK I GlobalRules.map;
-val elim_bang_global = add elim_bangK I GlobalRules.map;
-val dest_bang_global = add elim_bangK Tactic.make_elim GlobalRules.map;
-val intro_global = add introK I GlobalRules.map;
-val elim_global = add elimK I GlobalRules.map;
-val dest_global = add elimK Tactic.make_elim GlobalRules.map;
-val intro_query_global = add intro_queryK I GlobalRules.map;
-val elim_query_global = add elim_queryK I GlobalRules.map;
-val dest_query_global = add elim_queryK Tactic.make_elim GlobalRules.map;
-val rule_del_global = del GlobalRules.map;
+(* concrete syntax *)
+
+fun add_args a b c x = Attrib.syntax
+ (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) -- (Scan.option Args.nat))
+ >> (fn (f, n) => f n)) x;
+
+fun del_args att = Attrib.syntax (Scan.lift Args.del >> K att);
-val intro_bang_local = add intro_bangK I LocalRules.map;
-val elim_bang_local = add elim_bangK I LocalRules.map;
-val dest_bang_local = add elim_bangK Tactic.make_elim LocalRules.map;
-val intro_local = add introK I LocalRules.map;
-val elim_local = add elimK I LocalRules.map;
-val dest_local = add elimK Tactic.make_elim LocalRules.map;
-val intro_query_local = add intro_queryK I LocalRules.map;
-val elim_query_local = add elim_queryK I LocalRules.map;
-val dest_query_local = add elim_queryK Tactic.make_elim LocalRules.map;
-val rule_del_local = del LocalRules.map;
+val rule_atts =
+ [("intro", Attrib.common (add_args intro_bang intro intro_query),
+ "declaration of introduction rule"),
+ ("elim", Attrib.common (add_args elim_bang elim elim_query),
+ "declaration of elimination rule"),
+ ("dest", Attrib.common (add_args dest_bang dest dest_query),
+ "declaration of destruction rule"),
+ ("rule", Attrib.common (del_args rule_del),
+ "remove declaration of intro/elim/dest rule")];
+
+val _ = Context.add_setup [Attrib.add_attributes rule_atts];
end;
-
-val _ = Context.add_setup
- [snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query_global NONE])]];
-
-
-(* low-level modifiers *)
-
-fun modifier att (x, ths) =
- fst (Thm.applys_attributes [att] (x, rev ths));
-
-val addXIs_global = modifier (intro_query_global NONE);
-val addXEs_global = modifier (elim_query_global NONE);
-val addXDs_global = modifier (dest_query_global NONE);
-val delrules_global = modifier rule_del_global;
-
-val addXIs_local = modifier (intro_query_local NONE);
-val addXEs_local = modifier (elim_query_local NONE);
-val addXDs_local = modifier (dest_query_local NONE);
-val delrules_local = modifier rule_del_local;
-
-end;
--- a/src/Pure/Isar/induct_attrib.ML Tue Jan 10 19:33:35 2006 +0100
+++ b/src/Pure/Isar/induct_attrib.ML Tue Jan 10 19:33:36 2006 +0100
@@ -8,16 +8,11 @@
signature INDUCT_ATTRIB =
sig
val vars_of: term -> term list
- val dest_global_rules: theory ->
+ val dest_rules: Context.generic ->
{type_cases: (string * thm) list, set_cases: (string * thm) list,
type_induct: (string * thm) list, set_induct: (string * thm) list,
type_coinduct: (string * thm) list, set_coinduct: (string * thm) list}
- val print_global_rules: theory -> unit
- val dest_local_rules: Proof.context ->
- {type_cases: (string * thm) list, set_cases: (string * thm) list,
- type_induct: (string * thm) list, set_induct: (string * thm) list,
- type_coinduct: (string * thm) list, set_coinduct: (string * thm) list}
- val print_local_rules: Proof.context -> unit
+ val print_rules: Context.generic -> unit
val lookup_casesT : Proof.context -> string -> thm option
val lookup_casesS : Proof.context -> string -> thm option
val lookup_inductT : Proof.context -> string -> thm option
@@ -30,18 +25,12 @@
val find_inductS: Proof.context -> term -> thm list
val find_coinductT: Proof.context -> typ -> thm list
val find_coinductS: Proof.context -> term -> thm list
- val cases_type_global: string -> theory attribute
- val cases_set_global: string -> theory attribute
- val cases_type_local: string -> Proof.context attribute
- val cases_set_local: string -> Proof.context attribute
- val induct_type_global: string -> theory attribute
- val induct_set_global: string -> theory attribute
- val induct_type_local: string -> Proof.context attribute
- val induct_set_local: string -> Proof.context attribute
- val coinduct_type_global: string -> theory attribute
- val coinduct_set_global: string -> theory attribute
- val coinduct_type_local: string -> Proof.context attribute
- val coinduct_set_local: string -> Proof.context attribute
+ val cases_type: string -> Context.generic attribute
+ val cases_set: string -> Context.generic attribute
+ val induct_type: string -> Context.generic attribute
+ val induct_set: string -> Context.generic attribute
+ val coinduct_type: string -> Context.generic attribute
+ val coinduct_set: string -> Context.generic attribute
val casesN: string
val inductN: string
val coinductN: string
@@ -88,7 +77,7 @@
-(** global and local induct data **)
+(** induct data **)
(* rules *)
@@ -100,24 +89,23 @@
fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs);
-fun pretty_rules prt kind x rs =
+fun pretty_rules ctxt kind rs =
let val thms = map snd (NetRules.rules rs)
- in Pretty.big_list kind (map (prt x) thms) end;
-
-fun print_all_rules prt x ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
- [pretty_rules prt "coinduct type:" x coinductT,
- pretty_rules prt "coinduct set:" x coinductS,
- pretty_rules prt "induct type:" x inductT,
- pretty_rules prt "induct set:" x inductS,
- pretty_rules prt "cases type:" x casesT,
- pretty_rules prt "cases set:" x casesS]
- |> Pretty.chunks |> Pretty.writeln;
+ in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end;
-(* theory data *)
+(* context data *)
-structure GlobalInductArgs =
-struct
+fun dest ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
+ {type_cases = NetRules.rules casesT,
+ set_cases = NetRules.rules casesS,
+ type_induct = NetRules.rules inductT,
+ set_induct = NetRules.rules inductS,
+ type_coinduct = NetRules.rules coinductT,
+ set_coinduct = NetRules.rules coinductS};
+
+structure Induct = GenericDataFun
+(
val name = "Isar/induct";
type T = (rules * rules) * (rules * rules) * (rules * rules);
@@ -125,59 +113,46 @@
((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
(init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
(init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
- val copy = I;
+
val extend = I;
+
fun merge _ (((casesT1, casesS1), (inductT1, inductS1), (coinductT1, coinductS1)),
((casesT2, casesS2), (inductT2, inductS2), (coinductT2, coinductS2))) =
((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
(NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)),
(NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductS1, coinductS2)));
- fun print x = print_all_rules Display.pretty_thm_sg x;
-
- fun dest ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
- {type_cases = NetRules.rules casesT,
- set_cases = NetRules.rules casesS,
- type_induct = NetRules.rules inductT,
- set_induct = NetRules.rules inductS,
- type_coinduct = NetRules.rules coinductT,
- set_coinduct = NetRules.rules coinductS};
-end;
-
-structure GlobalInduct = TheoryDataFun(GlobalInductArgs);
-val _ = Context.add_setup [GlobalInduct.init];
-val print_global_rules = GlobalInduct.print;
-val dest_global_rules = GlobalInductArgs.dest o GlobalInduct.get;
+ fun print generic ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
+ let val ctxt = Context.proof_of generic in
+ [pretty_rules ctxt "coinduct type:" coinductT,
+ pretty_rules ctxt "coinduct set:" coinductS,
+ pretty_rules ctxt "induct type:" inductT,
+ pretty_rules ctxt "induct set:" inductS,
+ pretty_rules ctxt "cases type:" casesT,
+ pretty_rules ctxt "cases set:" casesS]
+ |> Pretty.chunks |> Pretty.writeln
+ end
+);
-
-(* proof data *)
-
-structure LocalInduct = ProofDataFun
-(struct
- val name = "Isar/induct";
- type T = GlobalInductArgs.T;
+val _ = Context.add_setup [Induct.init];
+val print_rules = Induct.print;
+val dest_rules = dest o Induct.get;
- fun init thy = GlobalInduct.get thy;
- fun print x = print_all_rules ProofContext.pretty_thm x;
-end);
-
-val _ = Context.add_setup [LocalInduct.init];
-val print_local_rules = LocalInduct.print;
-val dest_local_rules = GlobalInductArgs.dest o LocalInduct.get;
+val get_local = Induct.get o Context.Proof;
(* access rules *)
-val lookup_casesT = lookup_rule o #1 o #1 o LocalInduct.get;
-val lookup_casesS = lookup_rule o #2 o #1 o LocalInduct.get;
-val lookup_inductT = lookup_rule o #1 o #2 o LocalInduct.get;
-val lookup_inductS = lookup_rule o #2 o #2 o LocalInduct.get;
-val lookup_coinductT = lookup_rule o #1 o #3 o LocalInduct.get;
-val lookup_coinductS = lookup_rule o #2 o #3 o LocalInduct.get;
+val lookup_casesT = lookup_rule o #1 o #1 o get_local;
+val lookup_casesS = lookup_rule o #2 o #1 o get_local;
+val lookup_inductT = lookup_rule o #1 o #2 o get_local;
+val lookup_inductS = lookup_rule o #2 o #2 o get_local;
+val lookup_coinductT = lookup_rule o #1 o #3 o get_local;
+val lookup_coinductS = lookup_rule o #2 o #3 o get_local;
fun find_rules which how ctxt x =
- map snd (NetRules.retrieve (which (LocalInduct.get ctxt)) (how x));
+ map snd (NetRules.retrieve (which (get_local ctxt)) (how x));
val find_casesT = find_rules (#1 o #1) encode_type;
val find_casesS = find_rules (#2 o #1) I;
@@ -192,8 +167,8 @@
local
-fun mk_att f g h name arg =
- let val (x, thm) = h arg in (f (g (name, thm)) x, thm) end;
+fun mk_att f g name arg =
+ let val (x, thm) = g arg in (Induct.map (f (name, thm)) x, thm) end;
fun map1 f (x, y, z) = (f x, y, z);
fun map2 f (x, y, z) = (x, f y, z);
@@ -211,23 +186,17 @@
in
-val cases_type_global = mk_att GlobalInduct.map add_casesT consumes0;
-val cases_set_global = mk_att GlobalInduct.map add_casesS consumes1;
-val induct_type_global = mk_att GlobalInduct.map add_inductT consumes0;
-val induct_set_global = mk_att GlobalInduct.map add_inductS consumes1;
-val coinduct_type_global = mk_att GlobalInduct.map add_coinductT consumes0;
-val coinduct_set_global = mk_att GlobalInduct.map add_coinductS consumes1;
-
-val cases_type_local = mk_att LocalInduct.map add_casesT consumes0;
-val cases_set_local = mk_att LocalInduct.map add_casesS consumes1;
-val induct_type_local = mk_att LocalInduct.map add_inductT consumes0;
-val induct_set_local = mk_att LocalInduct.map add_inductS consumes1;
-val coinduct_type_local = mk_att LocalInduct.map add_coinductT consumes0;
-val coinduct_set_local = mk_att LocalInduct.map add_coinductS consumes1;
+val cases_type = mk_att add_casesT consumes0;
+val cases_set = mk_att add_casesS consumes1;
+val induct_type = mk_att add_inductT consumes0;
+val induct_set = mk_att add_inductS consumes1;
+val coinduct_type = mk_att add_coinductT consumes0;
+val coinduct_set = mk_att add_coinductS consumes1;
end;
+
(** concrete syntax **)
val casesN = "cases";
@@ -243,29 +212,21 @@
Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
Scan.lift (Args.$$$ k) >> K "";
-fun attrib tyname const add_type add_set =
- Attrib.syntax (spec typeN tyname >> add_type || spec setN const >> add_set);
+fun attrib add_type add_set =
+ Attrib.syntax (spec typeN Args.tyname >> add_type || spec setN Args.const >> add_set);
in
-val cases_attr =
- (attrib Args.global_tyname Args.global_const cases_type_global cases_set_global,
- attrib Args.local_tyname Args.local_const cases_type_local cases_set_local);
-
-val induct_attr =
- (attrib Args.global_tyname Args.global_const induct_type_global induct_set_global,
- attrib Args.local_tyname Args.local_const induct_type_local induct_set_local);
-
-val coinduct_attr =
- (attrib Args.global_tyname Args.global_const coinduct_type_global coinduct_set_global,
- attrib Args.local_tyname Args.local_const coinduct_type_local coinduct_set_local);
+val cases_att = attrib cases_type cases_set;
+val induct_att = attrib induct_type induct_set;
+val coinduct_att = attrib coinduct_type coinduct_set;
end;
val _ = Context.add_setup
[Attrib.add_attributes
- [(casesN, cases_attr, "declaration of cases rule for type or set"),
- (inductN, induct_attr, "declaration of induction rule for type or set"),
- (coinductN, coinduct_attr, "declaration of coinduction rule for type or set")]];
+ [(casesN, Attrib.common cases_att, "declaration of cases rule for type or set"),
+ (inductN, Attrib.common induct_att, "declaration of induction rule for type or set"),
+ (coinductN, Attrib.common coinduct_att, "declaration of coinduction rule for type or set")]];
end;