# HG changeset patch # User wenzelm # Date 1132406467 -3600 # Node ID ad4b8567f6ebd5155ade49b985cdaf78d29cccff # Parent 6bcd9b2ca49b662d5a9839a0819911d2766d89a2 added coinduct attribute; tuned; diff -r 6bcd9b2ca49b -r ad4b8567f6eb src/Pure/Isar/induct_attrib.ML --- 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;