--- a/src/Pure/Isar/induct_attrib.ML Sat Nov 19 14:21:06 2005 +0100
+++ b/src/Pure/Isar/induct_attrib.ML Sat Nov 19 14:21:07 2005 +0100
@@ -10,20 +10,26 @@
val vars_of: term -> term list
val dest_global_rules: theory ->
{type_cases: (string * thm) list, set_cases: (string * thm) list,
- type_induct: (string * thm) list, set_induct: (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_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 lookup_casesT : Proof.context -> string -> thm option
val lookup_casesS : Proof.context -> string -> thm option
val lookup_inductT : Proof.context -> string -> thm option
val lookup_inductS : Proof.context -> string -> thm option
+ val lookup_coinductT : Proof.context -> string -> thm option
+ val lookup_coinductS : Proof.context -> string -> thm option
val find_casesT: Proof.context -> typ -> thm list
val find_casesS: Proof.context -> thm -> thm list
val find_inductT: Proof.context -> typ -> thm list
val find_inductS: Proof.context -> thm -> thm list
+ val find_coinductT: Proof.context -> typ -> thm list
+ val find_coinductS: Proof.context -> thm -> thm list
val cases_type_global: string -> theory attribute
val cases_set_global: string -> theory attribute
val cases_type_local: string -> Proof.context attribute
@@ -32,8 +38,13 @@
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 casesN: string
val inductN: string
+ val coinductN: string
val typeN: string
val setN: string
end;
@@ -53,23 +64,25 @@
(* variables -- ordered left-to-right, preferring right *)
-local
+fun vars_of tm =
+ Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []
+ |> Library.distinct
+ |> rev;
-fun rev_vars_of tm =
- Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []
- |> Library.distinct;
+local
val mk_var = encode_type o #2 o Term.dest_Var;
+fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty =>
+ raise THM ("No variables in conclusion of rule", 0, [thm]);
+
in
-val vars_of = rev o rev_vars_of;
+fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty =>
+ raise THM ("No variables in major premise of rule", 0, [thm]);
-fun first_var thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty =>
- raise THM ("No variables in first premise of rule", 0, [thm]);
-
-fun last_var thm = mk_var (hd (rev_vars_of (Thm.concl_of thm))) handle Empty =>
- raise THM ("No variables in conclusion of rule", 0, [thm]);
+val left_var_concl = concl_var hd;
+val right_var_concl = concl_var List.last;
end;
@@ -87,41 +100,48 @@
fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs);
-fun print_rules prt kind x rs =
+fun pretty_rules prt kind x rs =
let val thms = map snd (NetRules.rules rs)
- in Pretty.writeln (Pretty.big_list kind (map (prt x) thms)) end;
+ in Pretty.big_list kind (map (prt x) thms) end;
-fun print_all_rules prt x ((casesT, casesS), (inductT, inductS)) =
- (print_rules prt "induct type:" x inductT;
- print_rules prt "induct set:" x inductS;
- print_rules prt "cases type:" x casesT;
- print_rules prt "cases set:" x casesS);
+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;
-(* theory data kind 'Isar/induction' *)
+(* theory data *)
structure GlobalInductArgs =
struct
- val name = "Isar/induction";
- type T = (rules * rules) * (rules * rules);
+ val name = "Isar/induct";
+ type T = (rules * rules) * (rules * rules) * (rules * rules);
val empty =
- ((init_rules (first_var o #2), init_rules (Thm.major_prem_of o #2)),
- (init_rules (last_var o #2), init_rules (Thm.major_prem_of o #2)));
+ ((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)),
- ((casesT2, casesS2), (inductT2, inductS2))) =
+ 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 (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)) =
+ 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};
+ set_induct = NetRules.rules inductS,
+ type_coinduct = NetRules.rules coinductT,
+ set_coinduct = NetRules.rules coinductS};
end;
structure GlobalInduct = TheoryDataFun(GlobalInductArgs);
@@ -130,11 +150,11 @@
val dest_global_rules = GlobalInductArgs.dest o GlobalInduct.get;
-(* proof data kind 'Isar/induction' *)
+(* proof data *)
structure LocalInduct = ProofDataFun
(struct
- val name = "Isar/induction";
+ val name = "Isar/induct";
type T = GlobalInductArgs.T;
fun init thy = GlobalInduct.get thy;
@@ -152,6 +172,8 @@
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;
fun find_rules which how ctxt x =
@@ -161,6 +183,8 @@
val find_casesS = find_rules (#2 o #1) Thm.concl_of;
val find_inductT = find_rules (#1 o #2) encode_type;
val find_inductS = find_rules (#2 o #2) Thm.concl_of;
+val find_coinductT = find_rules (#1 o #3) encode_type;
+val find_coinductS = find_rules (#2 o #3) Thm.concl_of;
@@ -171,10 +195,16 @@
fun mk_att f g h name arg =
let val (x, thm) = h arg in (f (g (name, thm)) x, thm) end;
-fun add_casesT rule x = apfst (apfst (NetRules.insert rule)) x;
-fun add_casesS rule x = apfst (apsnd (NetRules.insert rule)) x;
-fun add_inductT rule x = apsnd (apfst (NetRules.insert rule)) x;
-fun add_inductS rule x = apsnd (apsnd (NetRules.insert rule)) x;
+fun map1 f (x, y, z) = (f x, y, z);
+fun map2 f (x, y, z) = (x, f y, z);
+fun map3 f (x, y, z) = (x, y, f z);
+
+fun add_casesT rule x = map1 (apfst (NetRules.insert rule)) x;
+fun add_casesS rule x = map1 (apsnd (NetRules.insert rule)) x;
+fun add_inductT rule x = map2 (apfst (NetRules.insert rule)) x;
+fun add_inductS rule x = map2 (apsnd (NetRules.insert rule)) x;
+fun add_coinductT rule x = map3 (apfst (NetRules.insert rule)) x;
+fun add_coinductS rule x = map3 (apsnd (NetRules.insert rule)) x;
fun consumes0 x = RuleCases.consumes_default 0 x;
fun consumes1 x = RuleCases.consumes_default 1 x;
@@ -185,11 +215,15 @@
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;
end;
@@ -198,6 +232,7 @@
val casesN = "cases";
val inductN = "induct";
+val coinductN = "coinduct";
val typeN = "type";
val setN = "set";
@@ -221,11 +256,16 @@
(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);
+
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")]];
+ (inductN, induct_attr, "declaration of induction rule for type or set"),
+ (coinductN, coinduct_attr, "declaration of coinduction rule for type or set")]];
end;