author | wenzelm |
Wed, 03 Oct 2001 21:01:53 +0200 | |
changeset 11658 | 4200394242c5 |
parent 11656 | e499dceca569 |
child 11665 | 7324f018ea15 |
permissions | -rw-r--r-- |
11658 | 1 |
(* Title: Pure/Isar/induct_attrib.ML |
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, TU Muenchen |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
5 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
6 |
Declaration of rules for cases and induction. |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
7 |
*) |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
8 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
9 |
signature INDUCT_ATTRIB = |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
10 |
sig |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
11 |
val dest_global_rules: theory -> |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
12 |
{type_cases: (string * thm) list, set_cases: (string * thm) list, |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
13 |
type_induct: (string * thm) list, set_induct: (string * thm) list} |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
14 |
val print_global_rules: theory -> unit |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
15 |
val dest_local_rules: Proof.context -> |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
16 |
{type_cases: (string * thm) list, set_cases: (string * thm) list, |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
17 |
type_induct: (string * thm) list, set_induct: (string * thm) list} |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
18 |
val print_local_rules: Proof.context -> unit |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
19 |
val get_cases : Proof.context -> (string * thm) NetRules.T * (string * thm) NetRules.T |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
20 |
val get_induct : Proof.context -> (string * thm) NetRules.T * (string * thm) NetRules.T |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
21 |
val lookup_casesS : Proof.context -> string -> thm option |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
22 |
val lookup_casesT : Proof.context -> string -> thm option |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
23 |
val lookup_inductS : Proof.context -> string -> thm option |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
24 |
val lookup_inductT : Proof.context -> string -> thm option |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
25 |
val cases_type_global: string -> theory attribute |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
26 |
val cases_set_global: string -> theory attribute |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
27 |
val cases_type_local: string -> Proof.context attribute |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
28 |
val cases_set_local: string -> Proof.context attribute |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
29 |
val induct_type_global: string -> theory attribute |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
30 |
val induct_set_global: string -> theory attribute |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
31 |
val induct_type_local: string -> Proof.context attribute |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
32 |
val induct_set_local: string -> Proof.context attribute |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
33 |
val casesN: string |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
34 |
val inductN: string |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
35 |
val typeN: string |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
36 |
val setN: string |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
37 |
val setup: (theory -> theory) list |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
38 |
end; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
39 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
40 |
structure InductAttrib: INDUCT_ATTRIB = |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
41 |
struct |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
42 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
43 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
44 |
(** global and local induct data **) |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
45 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
46 |
(* rules *) |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
47 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
48 |
type rules = (string * thm) NetRules.T; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
49 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
50 |
fun eq_rule ((s1:string, th1), (s2, th2)) = s1 = s2 andalso Thm.eq_thm (th1, th2); |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
51 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
52 |
val type_rules = NetRules.init eq_rule (Thm.concl_of o #2); |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
53 |
val set_rules = NetRules.init eq_rule (Thm.major_prem_of o #2); |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
54 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
55 |
fun lookup_rule (rs:rules) name = Library.assoc (NetRules.rules rs, name); |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
56 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
57 |
fun print_rules kind sg rs = |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
58 |
let val thms = map snd (NetRules.rules rs) |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
59 |
in Pretty.writeln (Pretty.big_list kind (map (Display.pretty_thm_sg sg) thms)) end; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
60 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
61 |
|
11658 | 62 |
(* theory data kind 'Isar/induction' *) |
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
63 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
64 |
structure GlobalInductArgs = |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
65 |
struct |
11658 | 66 |
val name = "Isar/induction"; |
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
67 |
type T = (rules * rules) * (rules * rules); |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
68 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
69 |
val empty = ((type_rules, set_rules), (type_rules, set_rules)); |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
70 |
val copy = I; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
71 |
val prep_ext = I; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
72 |
fun merge (((casesT1, casesS1), (inductT1, inductS1)), |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
73 |
((casesT2, casesS2), (inductT2, inductS2))) = |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
74 |
((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)), |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
75 |
(NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2))); |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
76 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
77 |
fun print sg ((casesT, casesS), (inductT, inductS)) = |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
78 |
(print_rules "type cases:" sg casesT; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
79 |
print_rules "set cases:" sg casesS; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
80 |
print_rules "type induct:" sg inductT; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
81 |
print_rules "set induct:" sg inductS); |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
82 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
83 |
fun dest ((casesT, casesS), (inductT, inductS)) = |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
84 |
{type_cases = NetRules.rules casesT, |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
85 |
set_cases = NetRules.rules casesS, |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
86 |
type_induct = NetRules.rules inductT, |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
87 |
set_induct = NetRules.rules inductS}; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
88 |
end; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
89 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
90 |
structure GlobalInduct = TheoryDataFun(GlobalInductArgs); |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
91 |
val print_global_rules = GlobalInduct.print; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
92 |
val dest_global_rules = GlobalInductArgs.dest o GlobalInduct.get; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
93 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
94 |
|
11658 | 95 |
(* proof data kind 'Isar/induction' *) |
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
96 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
97 |
structure LocalInductArgs = |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
98 |
struct |
11658 | 99 |
val name = "Isar/induction"; |
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
100 |
type T = GlobalInductArgs.T; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
101 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
102 |
fun init thy = GlobalInduct.get thy; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
103 |
fun print x = GlobalInductArgs.print (ProofContext.sign_of x); |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
104 |
end; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
105 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
106 |
structure LocalInduct = ProofDataFun(LocalInductArgs); |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
107 |
val print_local_rules = LocalInduct.print; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
108 |
val dest_local_rules = GlobalInductArgs.dest o LocalInduct.get; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
109 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
110 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
111 |
(* access rules *) |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
112 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
113 |
val get_cases = #1 o LocalInduct.get; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
114 |
val get_induct = #2 o LocalInduct.get; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
115 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
116 |
val lookup_casesT = lookup_rule o #1 o get_cases; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
117 |
val lookup_casesS = lookup_rule o #2 o get_cases; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
118 |
val lookup_inductT = lookup_rule o #1 o get_induct; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
119 |
val lookup_inductS = lookup_rule o #2 o get_induct; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
120 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
121 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
122 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
123 |
(** attributes **) |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
124 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
125 |
local |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
126 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
127 |
fun mk_att f g h name arg = |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
128 |
let val (x, thm) = h arg in (f (g (name, thm)) x, thm) end; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
129 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
130 |
fun add_casesT rule x = apfst (apfst (NetRules.insert rule)) x; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
131 |
fun add_casesS rule x = apfst (apsnd (NetRules.insert rule)) x; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
132 |
fun add_inductT rule x = apsnd (apfst (NetRules.insert rule)) x; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
133 |
fun add_inductS rule x = apsnd (apsnd (NetRules.insert rule)) x; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
134 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
135 |
fun consumes0 x = RuleCases.consumes_default 0 x; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
136 |
fun consumes1 x = RuleCases.consumes_default 1 x; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
137 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
138 |
in |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
139 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
140 |
val cases_type_global = mk_att GlobalInduct.map add_casesT consumes0; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
141 |
val cases_set_global = mk_att GlobalInduct.map add_casesS consumes1; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
142 |
val induct_type_global = mk_att GlobalInduct.map add_inductT consumes0; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
143 |
val induct_set_global = mk_att GlobalInduct.map add_inductS consumes1; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
144 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
145 |
val cases_type_local = mk_att LocalInduct.map add_casesT consumes0; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
146 |
val cases_set_local = mk_att LocalInduct.map add_casesS consumes1; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
147 |
val induct_type_local = mk_att LocalInduct.map add_inductT consumes0; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
148 |
val induct_set_local = mk_att LocalInduct.map add_inductS consumes1; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
149 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
150 |
end; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
151 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
152 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
153 |
(** concrete syntax **) |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
154 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
155 |
val casesN = "cases"; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
156 |
val inductN = "induct"; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
157 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
158 |
val typeN = "type"; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
159 |
val setN = "set"; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
160 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
161 |
local |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
162 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
163 |
fun spec k = (Args.$$$ k -- Args.colon) |-- Args.!!! Args.name; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
164 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
165 |
fun attrib sign_of add_type add_set = Scan.depend (fn x => |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
166 |
let val sg = sign_of x in |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
167 |
spec typeN >> (add_type o Sign.certify_tycon sg o Sign.intern_tycon sg) || |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
168 |
spec setN >> (add_set o Sign.certify_const sg o Sign.intern_const sg) |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
169 |
end >> pair x); |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
170 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
171 |
in |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
172 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
173 |
val cases_attr = |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
174 |
(Attrib.syntax (attrib Theory.sign_of cases_type_global cases_set_global), |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
175 |
Attrib.syntax (attrib ProofContext.sign_of cases_type_local cases_set_local)); |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
176 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
177 |
val induct_attr = |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
178 |
(Attrib.syntax (attrib Theory.sign_of induct_type_global induct_set_global), |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
179 |
Attrib.syntax (attrib ProofContext.sign_of induct_type_local induct_set_local)); |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
180 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
181 |
end; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
182 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
183 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
184 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
185 |
(** theory setup **) |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
186 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
187 |
val setup = |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
188 |
[GlobalInduct.init, LocalInduct.init, |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
189 |
Attrib.add_attributes |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
190 |
[(casesN, cases_attr, "declaration of cases rule for type or set"), |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
191 |
(inductN, induct_attr, "declaration of induction rule for type or set")]]; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
192 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
193 |
end; |