1.1 --- a/src/Pure/Isar/calculation.ML Tue Jan 10 19:33:35 2006 +0100
1.2 +++ b/src/Pure/Isar/calculation.ML Tue Jan 10 19:33:36 2006 +0100
1.3 @@ -7,23 +7,16 @@
1.4
1.5 signature CALCULATION =
1.6 sig
1.7 + val print_rules: Context.generic -> unit
1.8 val get_calculation: Proof.state -> thm list option
1.9 - val print_global_rules: theory -> unit
1.10 - val print_local_rules: Proof.context -> unit
1.11 - val trans_add_global: theory attribute
1.12 - val trans_del_global: theory attribute
1.13 - val trans_add_local: Proof.context attribute
1.14 - val trans_del_local: Proof.context attribute
1.15 - val sym_add_global: theory attribute
1.16 - val sym_del_global: theory attribute
1.17 - val sym_add_local: Proof.context attribute
1.18 - val sym_del_local: Proof.context attribute
1.19 - val symmetric_global: theory attribute
1.20 - val symmetric_local: Proof.context attribute
1.21 + val trans_add: Context.generic attribute
1.22 + val trans_del: Context.generic attribute
1.23 + val sym_add: Context.generic attribute
1.24 + val sym_del: Context.generic attribute
1.25 + val symmetric: Context.generic attribute
1.26 val also: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
1.27 val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
1.28 - val finally: (thmref * Attrib.src list) list option -> bool ->
1.29 - Proof.state -> Proof.state Seq.seq
1.30 + val finally: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
1.31 val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
1.32 val moreover: bool -> Proof.state -> Proof.state
1.33 val ultimately: bool -> Proof.state -> Proof.state
1.34 @@ -32,112 +25,85 @@
1.35 structure Calculation: CALCULATION =
1.36 struct
1.37
1.38 -(** global and local calculation data **)
1.39 +(** calculation data **)
1.40
1.41 -(* global calculation *)
1.42 -
1.43 -fun print_rules prt x (trans, sym) =
1.44 - [Pretty.big_list "transitivity rules:" (map (prt x) (NetRules.rules trans)),
1.45 - Pretty.big_list "symmetry rules:" (map (prt x) sym)]
1.46 - |> Pretty.chunks |> Pretty.writeln;
1.47 -
1.48 -structure GlobalCalculation = TheoryDataFun
1.49 -(struct
1.50 - val name = "Isar/calculation";
1.51 - type T = thm NetRules.T * thm list
1.52 -
1.53 - val empty = (NetRules.elim, []);
1.54 - val copy = I;
1.55 - val extend = I;
1.56 - fun merge _ ((trans1, sym1), (trans2, sym2)) =
1.57 - (NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2));
1.58 - val print = print_rules Display.pretty_thm_sg;
1.59 -end);
1.60 -
1.61 -val _ = Context.add_setup [GlobalCalculation.init];
1.62 -val print_global_rules = GlobalCalculation.print;
1.63 -
1.64 -
1.65 -(* local calculation *)
1.66 -
1.67 -structure LocalCalculation = ProofDataFun
1.68 -(struct
1.69 +structure CalculationData = GenericDataFun
1.70 +(
1.71 val name = "Isar/calculation";
1.72 type T = (thm NetRules.T * thm list) * (thm list * int) option;
1.73 + val empty = ((NetRules.elim, []), NONE);
1.74 + val extend = I;
1.75
1.76 - fun init thy = (GlobalCalculation.get thy, NONE);
1.77 - fun print ctxt (rs, _) = print_rules ProofContext.pretty_thm ctxt rs;
1.78 -end);
1.79 + fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) =
1.80 + ((NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2)), NONE);
1.81
1.82 -val _ = Context.add_setup [LocalCalculation.init];
1.83 -val get_local_rules = #1 o LocalCalculation.get o Proof.context_of;
1.84 -val print_local_rules = LocalCalculation.print;
1.85 + fun print generic ((trans, sym), _) =
1.86 + let val ctxt = Context.proof_of generic in
1.87 + [Pretty.big_list "transitivity rules:"
1.88 + (map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)),
1.89 + Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)]
1.90 + |> Pretty.chunks |> Pretty.writeln
1.91 + end;
1.92 +);
1.93 +
1.94 +val _ = Context.add_setup [CalculationData.init];
1.95 +val print_rules = CalculationData.print;
1.96
1.97
1.98 (* access calculation *)
1.99
1.100 fun get_calculation state =
1.101 - (case #2 (LocalCalculation.get (Proof.context_of state)) of
1.102 + (case #2 (CalculationData.get (Context.Proof (Proof.context_of state))) of
1.103 NONE => NONE
1.104 | SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE);
1.105
1.106 val calculationN = "calculation";
1.107
1.108 fun put_calculation calc =
1.109 - `Proof.level #-> (fn lev => Proof.map_context
1.110 - (LocalCalculation.map (apsnd (K (Option.map (rpair lev) calc)))))
1.111 + `Proof.level #-> (fn lev =>
1.112 + Proof.map_context (Context.the_proof o
1.113 + CalculationData.map (apsnd (K (Option.map (rpair lev) calc))) o Context.Proof))
1.114 #> Proof.put_thms (calculationN, calc);
1.115
1.116
1.117 +
1.118 (** attributes **)
1.119
1.120 (* add/del rules *)
1.121
1.122 -fun global_att f (x, thm) = (GlobalCalculation.map (f thm) x, thm);
1.123 -fun local_att f (x, thm) = (LocalCalculation.map (apfst (f thm)) x, thm);
1.124 +val trans_add = Attrib.declaration (CalculationData.map o apfst o apfst o NetRules.insert);
1.125 +val trans_del = Attrib.declaration (CalculationData.map o apfst o apfst o NetRules.delete);
1.126
1.127 -val trans_add_global = global_att (apfst o NetRules.insert);
1.128 -val trans_del_global = global_att (apfst o NetRules.delete);
1.129 -val trans_add_local = local_att (apfst o NetRules.insert);
1.130 -val trans_del_local = local_att (apfst o NetRules.delete);
1.131 +val sym_add =
1.132 + Attrib.declaration (CalculationData.map o apfst o apsnd o Drule.add_rule)
1.133 + #> ContextRules.elim_query NONE;
1.134 +val sym_del =
1.135 + Attrib.declaration (CalculationData.map o apfst o apsnd o Drule.del_rule)
1.136 + #> ContextRules.rule_del;
1.137
1.138 -val sym_add_global = global_att (apsnd o Drule.add_rule) o ContextRules.elim_query_global NONE;
1.139 -val sym_del_global = global_att (apsnd o Drule.del_rule) o ContextRules.rule_del_global;
1.140 -val sym_add_local = local_att (apsnd o Drule.add_rule) o ContextRules.elim_query_local NONE;
1.141 -val sym_del_local = local_att (apsnd o Drule.del_rule) o ContextRules.rule_del_local;
1.142
1.143 +(* symmetric *)
1.144
1.145 -(* symmetry *)
1.146 -
1.147 -fun gen_symmetric get_sym = Drule.rule_attribute (fn x => fn th =>
1.148 - (case Seq.chop (2, Drule.multi_resolves [th] (get_sym x)) of
1.149 +val symmetric = Attrib.rule (fn x => fn th =>
1.150 + (case Seq.chop (2, Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of
1.151 ([th'], _) => th'
1.152 | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
1.153 | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
1.154
1.155 -val symmetric_global = gen_symmetric (#2 o GlobalCalculation.get);
1.156 -val symmetric_local = gen_symmetric (#2 o #1 o LocalCalculation.get);
1.157 -
1.158
1.159 (* concrete syntax *)
1.160
1.161 -val trans_attr =
1.162 - (Attrib.add_del_args trans_add_global trans_del_global,
1.163 - Attrib.add_del_args trans_add_local trans_del_local);
1.164 -
1.165 -val sym_attr =
1.166 - (Attrib.add_del_args sym_add_global sym_del_global,
1.167 - Attrib.add_del_args sym_add_local sym_del_local);
1.168 +val trans_att = Attrib.add_del_args trans_add trans_del;
1.169 +val sym_att = Attrib.add_del_args sym_add sym_del;
1.170
1.171 val _ = Context.add_setup
1.172 [Attrib.add_attributes
1.173 - [("trans", trans_attr, "declaration of transitivity rule"),
1.174 - ("sym", sym_attr, "declaration of symmetry rule"),
1.175 - ("symmetric", (Attrib.no_args symmetric_global, Attrib.no_args symmetric_local),
1.176 - "resolution with symmetry rule")],
1.177 + [("trans", Attrib.common trans_att, "declaration of transitivity rule"),
1.178 + ("sym", Attrib.common sym_att, "declaration of symmetry rule"),
1.179 + ("symmetric", Attrib.common (Attrib.no_args symmetric), "resolution with symmetry rule")],
1.180 snd o PureThy.add_thms
1.181 - [(("", transitive_thm), [trans_add_global]),
1.182 - (("", symmetric_thm), [sym_add_global])]];
1.183 + [(("", transitive_thm), [Attrib.theory trans_add]),
1.184 + (("", symmetric_thm), [Attrib.theory sym_add])]];
1.185
1.186
1.187
1.188 @@ -158,6 +124,8 @@
1.189
1.190 (* also and finally *)
1.191
1.192 +val get_rules = #1 o CalculationData.get o Context.Proof o Proof.context_of;
1.193 +
1.194 fun calculate prep_rules final raw_rules int state =
1.195 let
1.196 val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
1.197 @@ -168,8 +136,8 @@
1.198 fun combine ths =
1.199 (case opt_rules of SOME rules => rules
1.200 | NONE =>
1.201 - (case ths of [] => NetRules.rules (#1 (get_local_rules state))
1.202 - | th :: _ => NetRules.retrieve (#1 (get_local_rules state)) (strip_assums_concl th)))
1.203 + (case ths of [] => NetRules.rules (#1 (get_rules state))
1.204 + | th :: _ => NetRules.retrieve (#1 (get_rules state)) (strip_assums_concl th)))
1.205 |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
1.206 |> Seq.filter (not o projection ths);
1.207
2.1 --- a/src/Pure/Isar/context_rules.ML Tue Jan 10 19:33:35 2006 +0100
2.2 +++ b/src/Pure/Isar/context_rules.ML Tue Jan 10 19:33:36 2006 +0100
2.3 @@ -15,40 +15,21 @@
2.4 val orderlist: ((int * int) * 'a) list -> 'a list
2.5 val find_rules_netpair: bool -> thm list -> term -> netpair -> thm list
2.6 val find_rules: bool -> thm list -> term -> ProofContext.context -> thm list list
2.7 - val print_global_rules: theory -> unit
2.8 - val print_local_rules: ProofContext.context -> unit
2.9 + val print_rules: Context.generic -> unit
2.10 val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
2.11 val addWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
2.12 val Swrap: ProofContext.context -> (int -> tactic) -> int -> tactic
2.13 val wrap: ProofContext.context -> (int -> tactic) -> int -> tactic
2.14 - val intro_bang_global: int option -> theory attribute
2.15 - val elim_bang_global: int option -> theory attribute
2.16 - val dest_bang_global: int option -> theory attribute
2.17 - val intro_global: int option -> theory attribute
2.18 - val elim_global: int option -> theory attribute
2.19 - val dest_global: int option -> theory attribute
2.20 - val intro_query_global: int option -> theory attribute
2.21 - val elim_query_global: int option -> theory attribute
2.22 - val dest_query_global: int option -> theory attribute
2.23 - val rule_del_global: theory attribute
2.24 - val intro_bang_local: int option -> ProofContext.context attribute
2.25 - val elim_bang_local: int option -> ProofContext.context attribute
2.26 - val dest_bang_local: int option -> ProofContext.context attribute
2.27 - val intro_local: int option -> ProofContext.context attribute
2.28 - val elim_local: int option -> ProofContext.context attribute
2.29 - val dest_local: int option -> ProofContext.context attribute
2.30 - val intro_query_local: int option -> ProofContext.context attribute
2.31 - val elim_query_local: int option -> ProofContext.context attribute
2.32 - val dest_query_local: int option -> ProofContext.context attribute
2.33 - val rule_del_local: ProofContext.context attribute
2.34 - val addXIs_global: theory * thm list -> theory
2.35 - val addXEs_global: theory * thm list -> theory
2.36 - val addXDs_global: theory * thm list -> theory
2.37 - val delrules_global: theory * thm list -> theory
2.38 - val addXIs_local: ProofContext.context * thm list -> ProofContext.context
2.39 - val addXEs_local: ProofContext.context * thm list -> ProofContext.context
2.40 - val addXDs_local: ProofContext.context * thm list -> ProofContext.context
2.41 - val delrules_local: ProofContext.context * thm list -> ProofContext.context
2.42 + val intro_bang: int option -> Context.generic attribute
2.43 + val elim_bang: int option -> Context.generic attribute
2.44 + val dest_bang: int option -> Context.generic attribute
2.45 + val intro: int option -> Context.generic attribute
2.46 + val elim: int option -> Context.generic attribute
2.47 + val dest: int option -> Context.generic attribute
2.48 + val intro_query: int option -> Context.generic attribute
2.49 + val elim_query: int option -> Context.generic attribute
2.50 + val dest_query: int option -> Context.generic attribute
2.51 + val rule_del: Context.generic attribute
2.52 end;
2.53
2.54 structure ContextRules: CONTEXT_RULES =
2.55 @@ -78,7 +59,7 @@
2.56 val rule_indexes = distinct (map #1 rule_kinds);
2.57
2.58
2.59 -(* raw data *)
2.60 +(* context data *)
2.61
2.62 type netpair = ((int * int) * (bool * thm)) Net.net * ((int * int) * (bool * thm)) Net.net;
2.63 val empty_netpairs: netpair list = replicate (length rule_indexes) (Net.empty, Net.empty);
2.64 @@ -108,60 +89,45 @@
2.65 else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers
2.66 end;
2.67
2.68 -fun print_rules prt x (Rules {rules, ...}) =
2.69 - let
2.70 - fun prt_kind (i, b) =
2.71 - Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
2.72 - (List.mapPartial (fn (_, (k, th)) => if k = (i, b) then SOME (prt x th) else NONE)
2.73 - (sort (int_ord o pairself fst) rules));
2.74 - in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
2.75 -
2.76 -
2.77 -(* theory and proof data *)
2.78 -
2.79 -structure GlobalRulesArgs =
2.80 -struct
2.81 +structure Rules = GenericDataFun
2.82 +(
2.83 val name = "Isar/rules";
2.84 type T = T;
2.85
2.86 val empty = make_rules ~1 [] empty_netpairs ([], []);
2.87 - val copy = I;
2.88 val extend = I;
2.89
2.90 fun merge _ (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
2.91 Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
2.92 let
2.93 - val wrappers = (gen_merge_lists' (eq_snd (op =)) ws1 ws2, gen_merge_lists' (eq_snd (op =)) ws1' ws2');
2.94 + val wrappers =
2.95 + (gen_merge_lists' (eq_snd (op =)) ws1 ws2, gen_merge_lists' (eq_snd (op =)) ws1' ws2');
2.96 val rules = gen_merge_lists' (fn ((_, (k1, th1)), (_, (k2, th2))) =>
2.97 k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) rules1 rules2;
2.98 val next = ~ (length rules);
2.99 val netpairs = Library.foldl (fn (nps, (n, (w, ((i, b), th)))) =>
2.100 nth_map i (curry insert_tagged_brl ((w, n), (b, th))) nps)
2.101 (empty_netpairs, next upto ~1 ~~ rules);
2.102 - in make_rules (next - 1) rules netpairs wrappers end;
2.103 + in make_rules (next - 1) rules netpairs wrappers end
2.104
2.105 - val print = print_rules Display.pretty_thm_sg;
2.106 -end;
2.107 + fun print generic (Rules {rules, ...}) =
2.108 + let
2.109 + val ctxt = Context.proof_of generic;
2.110 + fun prt_kind (i, b) =
2.111 + Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
2.112 + (List.mapPartial (fn (_, (k, th)) =>
2.113 + if k = (i, b) then SOME (ProofContext.pretty_thm ctxt th) else NONE)
2.114 + (sort (int_ord o pairself fst) rules));
2.115 + in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
2.116 +);
2.117
2.118 -structure GlobalRules = TheoryDataFun(GlobalRulesArgs);
2.119 -val _ = Context.add_setup [GlobalRules.init];
2.120 -val print_global_rules = GlobalRules.print;
2.121 -
2.122 -structure LocalRules = ProofDataFun
2.123 -(struct
2.124 - val name = GlobalRulesArgs.name;
2.125 - type T = GlobalRulesArgs.T;
2.126 - val init = GlobalRules.get;
2.127 - val print = print_rules ProofContext.pretty_thm;
2.128 -end);
2.129 -
2.130 -val _ = Context.add_setup [LocalRules.init];
2.131 -val print_local_rules = LocalRules.print;
2.132 +val _ = Context.add_setup [Rules.init];
2.133 +val print_rules = Rules.print;
2.134
2.135
2.136 (* access data *)
2.137
2.138 -fun netpairs ctxt = let val Rules {netpairs, ...} = LocalRules.get ctxt in netpairs end;
2.139 +fun netpairs ctxt = let val Rules {netpairs, ...} = Rules.get (Context.Proof ctxt) in netpairs end;
2.140 val netpair_bang = hd o netpairs;
2.141 val netpair = hd o tl o netpairs;
2.142
2.143 @@ -197,15 +163,16 @@
2.144
2.145 (* wrappers *)
2.146
2.147 -fun gen_add_wrapper upd w = GlobalRules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
2.148 - make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers));
2.149 +fun gen_add_wrapper upd w = Context.the_theory o
2.150 + Rules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
2.151 + make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers)) o Context.Theory;
2.152
2.153 val addSWrapper = gen_add_wrapper Library.apfst;
2.154 val addWrapper = gen_add_wrapper Library.apsnd;
2.155
2.156
2.157 fun gen_wrap which ctxt =
2.158 - let val Rules {wrappers, ...} = LocalRules.get ctxt
2.159 + let val Rules {wrappers, ...} = Rules.get (Context.Proof ctxt)
2.160 in fold_rev fst (which wrappers) end;
2.161
2.162 val Swrap = gen_wrap #1;
2.163 @@ -217,57 +184,44 @@
2.164
2.165 (* add and del rules *)
2.166
2.167 -local
2.168 +fun rule_del (x, th) =
2.169 + (Rules.map (del_rule th o del_rule (Tactic.make_elim th)) x, th);
2.170
2.171 -fun del map_data (x, th) =
2.172 - (map_data (del_rule th o del_rule (Tactic.make_elim th)) x, th);
2.173 +fun rule_add k view opt_w =
2.174 + (fn (x, th) => (Rules.map (add_rule k opt_w (view th)) x, th)) o rule_del;
2.175
2.176 -fun add k view map_data opt_w =
2.177 - (fn (x, th) => (map_data (add_rule k opt_w (view th)) x, th)) o del map_data;
2.178 +val intro_bang = rule_add intro_bangK I;
2.179 +val elim_bang = rule_add elim_bangK I;
2.180 +val dest_bang = rule_add elim_bangK Tactic.make_elim;
2.181 +val intro = rule_add introK I;
2.182 +val elim = rule_add elimK I;
2.183 +val dest = rule_add elimK Tactic.make_elim;
2.184 +val intro_query = rule_add intro_queryK I;
2.185 +val elim_query = rule_add elim_queryK I;
2.186 +val dest_query = rule_add elim_queryK Tactic.make_elim;
2.187
2.188 -in
2.189 +val _ = Context.add_setup
2.190 + [snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [Attrib.theory (intro_query NONE)])]];
2.191
2.192 -val intro_bang_global = add intro_bangK I GlobalRules.map;
2.193 -val elim_bang_global = add elim_bangK I GlobalRules.map;
2.194 -val dest_bang_global = add elim_bangK Tactic.make_elim GlobalRules.map;
2.195 -val intro_global = add introK I GlobalRules.map;
2.196 -val elim_global = add elimK I GlobalRules.map;
2.197 -val dest_global = add elimK Tactic.make_elim GlobalRules.map;
2.198 -val intro_query_global = add intro_queryK I GlobalRules.map;
2.199 -val elim_query_global = add elim_queryK I GlobalRules.map;
2.200 -val dest_query_global = add elim_queryK Tactic.make_elim GlobalRules.map;
2.201 -val rule_del_global = del GlobalRules.map;
2.202
2.203 -val intro_bang_local = add intro_bangK I LocalRules.map;
2.204 -val elim_bang_local = add elim_bangK I LocalRules.map;
2.205 -val dest_bang_local = add elim_bangK Tactic.make_elim LocalRules.map;
2.206 -val intro_local = add introK I LocalRules.map;
2.207 -val elim_local = add elimK I LocalRules.map;
2.208 -val dest_local = add elimK Tactic.make_elim LocalRules.map;
2.209 -val intro_query_local = add intro_queryK I LocalRules.map;
2.210 -val elim_query_local = add elim_queryK I LocalRules.map;
2.211 -val dest_query_local = add elim_queryK Tactic.make_elim LocalRules.map;
2.212 -val rule_del_local = del LocalRules.map;
2.213 +(* concrete syntax *)
2.214 +
2.215 +fun add_args a b c x = Attrib.syntax
2.216 + (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) -- (Scan.option Args.nat))
2.217 + >> (fn (f, n) => f n)) x;
2.218 +
2.219 +fun del_args att = Attrib.syntax (Scan.lift Args.del >> K att);
2.220 +
2.221 +val rule_atts =
2.222 + [("intro", Attrib.common (add_args intro_bang intro intro_query),
2.223 + "declaration of introduction rule"),
2.224 + ("elim", Attrib.common (add_args elim_bang elim elim_query),
2.225 + "declaration of elimination rule"),
2.226 + ("dest", Attrib.common (add_args dest_bang dest dest_query),
2.227 + "declaration of destruction rule"),
2.228 + ("rule", Attrib.common (del_args rule_del),
2.229 + "remove declaration of intro/elim/dest rule")];
2.230 +
2.231 +val _ = Context.add_setup [Attrib.add_attributes rule_atts];
2.232
2.233 end;
2.234 -
2.235 -val _ = Context.add_setup
2.236 - [snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query_global NONE])]];
2.237 -
2.238 -
2.239 -(* low-level modifiers *)
2.240 -
2.241 -fun modifier att (x, ths) =
2.242 - fst (Thm.applys_attributes [att] (x, rev ths));
2.243 -
2.244 -val addXIs_global = modifier (intro_query_global NONE);
2.245 -val addXEs_global = modifier (elim_query_global NONE);
2.246 -val addXDs_global = modifier (dest_query_global NONE);
2.247 -val delrules_global = modifier rule_del_global;
2.248 -
2.249 -val addXIs_local = modifier (intro_query_local NONE);
2.250 -val addXEs_local = modifier (elim_query_local NONE);
2.251 -val addXDs_local = modifier (dest_query_local NONE);
2.252 -val delrules_local = modifier rule_del_local;
2.253 -
2.254 -end;
3.1 --- a/src/Pure/Isar/induct_attrib.ML Tue Jan 10 19:33:35 2006 +0100
3.2 +++ b/src/Pure/Isar/induct_attrib.ML Tue Jan 10 19:33:36 2006 +0100
3.3 @@ -8,16 +8,11 @@
3.4 signature INDUCT_ATTRIB =
3.5 sig
3.6 val vars_of: term -> term list
3.7 - val dest_global_rules: theory ->
3.8 + val dest_rules: Context.generic ->
3.9 {type_cases: (string * thm) list, set_cases: (string * thm) list,
3.10 type_induct: (string * thm) list, set_induct: (string * thm) list,
3.11 type_coinduct: (string * thm) list, set_coinduct: (string * thm) list}
3.12 - val print_global_rules: theory -> unit
3.13 - val dest_local_rules: Proof.context ->
3.14 - {type_cases: (string * thm) list, set_cases: (string * thm) list,
3.15 - type_induct: (string * thm) list, set_induct: (string * thm) list,
3.16 - type_coinduct: (string * thm) list, set_coinduct: (string * thm) list}
3.17 - val print_local_rules: Proof.context -> unit
3.18 + val print_rules: Context.generic -> unit
3.19 val lookup_casesT : Proof.context -> string -> thm option
3.20 val lookup_casesS : Proof.context -> string -> thm option
3.21 val lookup_inductT : Proof.context -> string -> thm option
3.22 @@ -30,18 +25,12 @@
3.23 val find_inductS: Proof.context -> term -> thm list
3.24 val find_coinductT: Proof.context -> typ -> thm list
3.25 val find_coinductS: Proof.context -> term -> thm list
3.26 - val cases_type_global: string -> theory attribute
3.27 - val cases_set_global: string -> theory attribute
3.28 - val cases_type_local: string -> Proof.context attribute
3.29 - val cases_set_local: string -> Proof.context attribute
3.30 - val induct_type_global: string -> theory attribute
3.31 - val induct_set_global: string -> theory attribute
3.32 - val induct_type_local: string -> Proof.context attribute
3.33 - val induct_set_local: string -> Proof.context attribute
3.34 - val coinduct_type_global: string -> theory attribute
3.35 - val coinduct_set_global: string -> theory attribute
3.36 - val coinduct_type_local: string -> Proof.context attribute
3.37 - val coinduct_set_local: string -> Proof.context attribute
3.38 + val cases_type: string -> Context.generic attribute
3.39 + val cases_set: string -> Context.generic attribute
3.40 + val induct_type: string -> Context.generic attribute
3.41 + val induct_set: string -> Context.generic attribute
3.42 + val coinduct_type: string -> Context.generic attribute
3.43 + val coinduct_set: string -> Context.generic attribute
3.44 val casesN: string
3.45 val inductN: string
3.46 val coinductN: string
3.47 @@ -88,7 +77,7 @@
3.48
3.49
3.50
3.51 -(** global and local induct data **)
3.52 +(** induct data **)
3.53
3.54 (* rules *)
3.55
3.56 @@ -100,24 +89,23 @@
3.57
3.58 fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs);
3.59
3.60 -fun pretty_rules prt kind x rs =
3.61 +fun pretty_rules ctxt kind rs =
3.62 let val thms = map snd (NetRules.rules rs)
3.63 - in Pretty.big_list kind (map (prt x) thms) end;
3.64 + in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end;
3.65
3.66 -fun print_all_rules prt x ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
3.67 - [pretty_rules prt "coinduct type:" x coinductT,
3.68 - pretty_rules prt "coinduct set:" x coinductS,
3.69 - pretty_rules prt "induct type:" x inductT,
3.70 - pretty_rules prt "induct set:" x inductS,
3.71 - pretty_rules prt "cases type:" x casesT,
3.72 - pretty_rules prt "cases set:" x casesS]
3.73 - |> Pretty.chunks |> Pretty.writeln;
3.74
3.75 +(* context data *)
3.76
3.77 -(* theory data *)
3.78 +fun dest ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
3.79 + {type_cases = NetRules.rules casesT,
3.80 + set_cases = NetRules.rules casesS,
3.81 + type_induct = NetRules.rules inductT,
3.82 + set_induct = NetRules.rules inductS,
3.83 + type_coinduct = NetRules.rules coinductT,
3.84 + set_coinduct = NetRules.rules coinductS};
3.85
3.86 -structure GlobalInductArgs =
3.87 -struct
3.88 +structure Induct = GenericDataFun
3.89 +(
3.90 val name = "Isar/induct";
3.91 type T = (rules * rules) * (rules * rules) * (rules * rules);
3.92
3.93 @@ -125,59 +113,46 @@
3.94 ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
3.95 (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
3.96 (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
3.97 - val copy = I;
3.98 +
3.99 val extend = I;
3.100 +
3.101 fun merge _ (((casesT1, casesS1), (inductT1, inductS1), (coinductT1, coinductS1)),
3.102 ((casesT2, casesS2), (inductT2, inductS2), (coinductT2, coinductS2))) =
3.103 ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
3.104 (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)),
3.105 (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductS1, coinductS2)));
3.106
3.107 - fun print x = print_all_rules Display.pretty_thm_sg x;
3.108 + fun print generic ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
3.109 + let val ctxt = Context.proof_of generic in
3.110 + [pretty_rules ctxt "coinduct type:" coinductT,
3.111 + pretty_rules ctxt "coinduct set:" coinductS,
3.112 + pretty_rules ctxt "induct type:" inductT,
3.113 + pretty_rules ctxt "induct set:" inductS,
3.114 + pretty_rules ctxt "cases type:" casesT,
3.115 + pretty_rules ctxt "cases set:" casesS]
3.116 + |> Pretty.chunks |> Pretty.writeln
3.117 + end
3.118 +);
3.119
3.120 - fun dest ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
3.121 - {type_cases = NetRules.rules casesT,
3.122 - set_cases = NetRules.rules casesS,
3.123 - type_induct = NetRules.rules inductT,
3.124 - set_induct = NetRules.rules inductS,
3.125 - type_coinduct = NetRules.rules coinductT,
3.126 - set_coinduct = NetRules.rules coinductS};
3.127 -end;
3.128 +val _ = Context.add_setup [Induct.init];
3.129 +val print_rules = Induct.print;
3.130 +val dest_rules = dest o Induct.get;
3.131
3.132 -structure GlobalInduct = TheoryDataFun(GlobalInductArgs);
3.133 -val _ = Context.add_setup [GlobalInduct.init];
3.134 -val print_global_rules = GlobalInduct.print;
3.135 -val dest_global_rules = GlobalInductArgs.dest o GlobalInduct.get;
3.136 -
3.137 -
3.138 -(* proof data *)
3.139 -
3.140 -structure LocalInduct = ProofDataFun
3.141 -(struct
3.142 - val name = "Isar/induct";
3.143 - type T = GlobalInductArgs.T;
3.144 -
3.145 - fun init thy = GlobalInduct.get thy;
3.146 - fun print x = print_all_rules ProofContext.pretty_thm x;
3.147 -end);
3.148 -
3.149 -val _ = Context.add_setup [LocalInduct.init];
3.150 -val print_local_rules = LocalInduct.print;
3.151 -val dest_local_rules = GlobalInductArgs.dest o LocalInduct.get;
3.152 +val get_local = Induct.get o Context.Proof;
3.153
3.154
3.155 (* access rules *)
3.156
3.157 -val lookup_casesT = lookup_rule o #1 o #1 o LocalInduct.get;
3.158 -val lookup_casesS = lookup_rule o #2 o #1 o LocalInduct.get;
3.159 -val lookup_inductT = lookup_rule o #1 o #2 o LocalInduct.get;
3.160 -val lookup_inductS = lookup_rule o #2 o #2 o LocalInduct.get;
3.161 -val lookup_coinductT = lookup_rule o #1 o #3 o LocalInduct.get;
3.162 -val lookup_coinductS = lookup_rule o #2 o #3 o LocalInduct.get;
3.163 +val lookup_casesT = lookup_rule o #1 o #1 o get_local;
3.164 +val lookup_casesS = lookup_rule o #2 o #1 o get_local;
3.165 +val lookup_inductT = lookup_rule o #1 o #2 o get_local;
3.166 +val lookup_inductS = lookup_rule o #2 o #2 o get_local;
3.167 +val lookup_coinductT = lookup_rule o #1 o #3 o get_local;
3.168 +val lookup_coinductS = lookup_rule o #2 o #3 o get_local;
3.169
3.170
3.171 fun find_rules which how ctxt x =
3.172 - map snd (NetRules.retrieve (which (LocalInduct.get ctxt)) (how x));
3.173 + map snd (NetRules.retrieve (which (get_local ctxt)) (how x));
3.174
3.175 val find_casesT = find_rules (#1 o #1) encode_type;
3.176 val find_casesS = find_rules (#2 o #1) I;
3.177 @@ -192,8 +167,8 @@
3.178
3.179 local
3.180
3.181 -fun mk_att f g h name arg =
3.182 - let val (x, thm) = h arg in (f (g (name, thm)) x, thm) end;
3.183 +fun mk_att f g name arg =
3.184 + let val (x, thm) = g arg in (Induct.map (f (name, thm)) x, thm) end;
3.185
3.186 fun map1 f (x, y, z) = (f x, y, z);
3.187 fun map2 f (x, y, z) = (x, f y, z);
3.188 @@ -211,23 +186,17 @@
3.189
3.190 in
3.191
3.192 -val cases_type_global = mk_att GlobalInduct.map add_casesT consumes0;
3.193 -val cases_set_global = mk_att GlobalInduct.map add_casesS consumes1;
3.194 -val induct_type_global = mk_att GlobalInduct.map add_inductT consumes0;
3.195 -val induct_set_global = mk_att GlobalInduct.map add_inductS consumes1;
3.196 -val coinduct_type_global = mk_att GlobalInduct.map add_coinductT consumes0;
3.197 -val coinduct_set_global = mk_att GlobalInduct.map add_coinductS consumes1;
3.198 -
3.199 -val cases_type_local = mk_att LocalInduct.map add_casesT consumes0;
3.200 -val cases_set_local = mk_att LocalInduct.map add_casesS consumes1;
3.201 -val induct_type_local = mk_att LocalInduct.map add_inductT consumes0;
3.202 -val induct_set_local = mk_att LocalInduct.map add_inductS consumes1;
3.203 -val coinduct_type_local = mk_att LocalInduct.map add_coinductT consumes0;
3.204 -val coinduct_set_local = mk_att LocalInduct.map add_coinductS consumes1;
3.205 +val cases_type = mk_att add_casesT consumes0;
3.206 +val cases_set = mk_att add_casesS consumes1;
3.207 +val induct_type = mk_att add_inductT consumes0;
3.208 +val induct_set = mk_att add_inductS consumes1;
3.209 +val coinduct_type = mk_att add_coinductT consumes0;
3.210 +val coinduct_set = mk_att add_coinductS consumes1;
3.211
3.212 end;
3.213
3.214
3.215 +
3.216 (** concrete syntax **)
3.217
3.218 val casesN = "cases";
3.219 @@ -243,29 +212,21 @@
3.220 Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
3.221 Scan.lift (Args.$$$ k) >> K "";
3.222
3.223 -fun attrib tyname const add_type add_set =
3.224 - Attrib.syntax (spec typeN tyname >> add_type || spec setN const >> add_set);
3.225 +fun attrib add_type add_set =
3.226 + Attrib.syntax (spec typeN Args.tyname >> add_type || spec setN Args.const >> add_set);
3.227
3.228 in
3.229
3.230 -val cases_attr =
3.231 - (attrib Args.global_tyname Args.global_const cases_type_global cases_set_global,
3.232 - attrib Args.local_tyname Args.local_const cases_type_local cases_set_local);
3.233 -
3.234 -val induct_attr =
3.235 - (attrib Args.global_tyname Args.global_const induct_type_global induct_set_global,
3.236 - attrib Args.local_tyname Args.local_const induct_type_local induct_set_local);
3.237 -
3.238 -val coinduct_attr =
3.239 - (attrib Args.global_tyname Args.global_const coinduct_type_global coinduct_set_global,
3.240 - attrib Args.local_tyname Args.local_const coinduct_type_local coinduct_set_local);
3.241 +val cases_att = attrib cases_type cases_set;
3.242 +val induct_att = attrib induct_type induct_set;
3.243 +val coinduct_att = attrib coinduct_type coinduct_set;
3.244
3.245 end;
3.246
3.247 val _ = Context.add_setup
3.248 [Attrib.add_attributes
3.249 - [(casesN, cases_attr, "declaration of cases rule for type or set"),
3.250 - (inductN, induct_attr, "declaration of induction rule for type or set"),
3.251 - (coinductN, coinduct_attr, "declaration of coinduction rule for type or set")]];
3.252 + [(casesN, Attrib.common cases_att, "declaration of cases rule for type or set"),
3.253 + (inductN, Attrib.common induct_att, "declaration of induction rule for type or set"),
3.254 + (coinductN, Attrib.common coinduct_att, "declaration of coinduction rule for type or set")]];
3.255
3.256 end;