author  haftmann 
Wed, 21 Jan 2009 16:47:32 +0100  
changeset 29581  b3b33e0298eb 
parent 29276  94b1ffec9201 
child 30211  556d1810cdad 
permissions  rwrr 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

1 
(* Title: Tools/induct.ML 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

2 
Author: Markus Wenzel, TU Muenchen 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

3 

26924  4 
Proof by cases, induction, and coinduction. 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

5 
*) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

6 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

7 
signature INDUCT_DATA = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

8 
sig 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

9 
val cases_default: thm 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

10 
val atomize: thm list 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

11 
val rulify: thm list 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

12 
val rulify_fallback: thm list 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

13 
end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

14 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

15 
signature INDUCT = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

16 
sig 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

17 
(*rule declarations*) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

18 
val vars_of: term > term list 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

19 
val dest_rules: Proof.context > 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

20 
{type_cases: (string * thm) list, pred_cases: (string * thm) list, 
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

21 
type_induct: (string * thm) list, pred_induct: (string * thm) list, 
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

22 
type_coinduct: (string * thm) list, pred_coinduct: (string * thm) list} 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

23 
val print_rules: Proof.context > unit 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

24 
val lookup_casesT: Proof.context > string > thm option 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

25 
val lookup_casesP: Proof.context > string > thm option 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

26 
val lookup_inductT: Proof.context > string > thm option 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

27 
val lookup_inductP: Proof.context > string > thm option 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

28 
val lookup_coinductT: Proof.context > string > thm option 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

29 
val lookup_coinductP: Proof.context > string > thm option 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

30 
val find_casesT: Proof.context > typ > thm list 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

31 
val find_casesP: Proof.context > term > thm list 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

32 
val find_inductT: Proof.context > typ > thm list 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

33 
val find_inductP: Proof.context > term > thm list 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

34 
val find_coinductT: Proof.context > typ > thm list 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

35 
val find_coinductP: Proof.context > term > thm list 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

36 
val cases_type: string > attribute 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

37 
val cases_pred: string > attribute 
27140  38 
val cases_del: attribute 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

39 
val induct_type: string > attribute 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

40 
val induct_pred: string > attribute 
27140  41 
val induct_del: attribute 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

42 
val coinduct_type: string > attribute 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

43 
val coinduct_pred: string > attribute 
27140  44 
val coinduct_del: attribute 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

45 
val casesN: string 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

46 
val inductN: string 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

47 
val coinductN: string 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

48 
val typeN: string 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

49 
val predN: string 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

50 
val setN: string 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

51 
(*proof methods*) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

52 
val fix_tac: Proof.context > int > (string * typ) list > int > tactic 
29581  53 
val add_defs: (binding option * term) option list > Proof.context > 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

54 
(term option list * thm list) * Proof.context 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

55 
val atomize_term: theory > term > term 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

56 
val atomize_tac: int > tactic 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

57 
val inner_atomize_tac: int > tactic 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

58 
val rulified_term: thm > theory * term 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

59 
val rulify_tac: int > tactic 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

60 
val internalize: int > thm > thm 
26940  61 
val guess_instance: Proof.context > thm > int > thm > thm Seq.seq 
26924  62 
val cases_tac: Proof.context > term option list list > thm option > 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

63 
thm list > int > cases_tactic 
27323
385c0ce33173
tuned get_inductT: *all* rules for missing instantiation;
wenzelm
parents:
27140
diff
changeset

64 
val get_inductT: Proof.context > term option list list > thm list list 
29581  65 
val induct_tac: Proof.context > (binding option * term) option list list > 
26924  66 
(string * typ) list list > term option list > thm list option > 
67 
thm list > int > cases_tactic 

68 
val coinduct_tac: Proof.context > term option list > term option list > thm option > 

69 
thm list > int > cases_tactic 

24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

70 
val setup: theory > theory 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

71 
end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

72 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

73 
functor InductFun(Data: INDUCT_DATA): INDUCT = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

74 
struct 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

75 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

76 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

77 
(** misc utils **) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

78 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

79 
(* encode_type  for indexing purposes *) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

80 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

81 
fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

82 
 encode_type (TFree (a, _)) = Free (a, dummyT) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

83 
 encode_type (TVar (a, _)) = Var (a, dummyT); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

84 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

85 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

86 
(* variables  ordered lefttoright, preferring right *) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

87 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

88 
fun vars_of tm = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

89 
rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t  _ => I) tm [])); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

90 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

91 
local 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

92 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

93 
val mk_var = encode_type o #2 o Term.dest_Var; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

94 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

95 
fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty => 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

96 
raise THM ("No variables in conclusion of rule", 0, [thm]); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

97 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

98 
in 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

99 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

100 
fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty => 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

101 
raise THM ("No variables in major premise of rule", 0, [thm]); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

102 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

103 
val left_var_concl = concl_var hd; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

104 
val right_var_concl = concl_var List.last; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

105 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

106 
end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

107 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

108 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

109 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

110 
(** induct data **) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

111 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

112 
(* rules *) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

113 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

114 
type rules = (string * thm) NetRules.T; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

115 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

116 
val init_rules = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

117 
NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

118 
Thm.eq_thm_prop (th1, th2)); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

119 

27140  120 
fun filter_rules (rs: rules) th = 
121 
filter (fn (_, th') => Thm.eq_thm_prop (th, th')) (NetRules.rules rs); 

122 

24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

123 
fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

124 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

125 
fun pretty_rules ctxt kind rs = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

126 
let val thms = map snd (NetRules.rules rs) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

127 
in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

128 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

129 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

130 
(* context data *) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

131 

27140  132 
structure InductData = GenericDataFun 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

133 
( 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

134 
type T = (rules * rules) * (rules * rules) * (rules * rules); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

135 
val empty = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

136 
((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)), 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

137 
(init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)), 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

138 
(init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2))); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

139 
val extend = I; 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

140 
fun merge _ (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1)), 
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

141 
((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2))) = 
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

142 
((NetRules.merge (casesT1, casesT2), NetRules.merge (casesP1, casesP2)), 
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

143 
(NetRules.merge (inductT1, inductT2), NetRules.merge (inductP1, inductP2)), 
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

144 
(NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductP1, coinductP2))); 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

145 
); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

146 

27140  147 
val get_local = InductData.get o Context.Proof; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

148 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

149 
fun dest_rules ctxt = 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

150 
let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP)) = get_local ctxt in 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

151 
{type_cases = NetRules.rules casesT, 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

152 
pred_cases = NetRules.rules casesP, 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

153 
type_induct = NetRules.rules inductT, 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

154 
pred_induct = NetRules.rules inductP, 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

155 
type_coinduct = NetRules.rules coinductT, 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

156 
pred_coinduct = NetRules.rules coinductP} 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

157 
end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

158 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

159 
fun print_rules ctxt = 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

160 
let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP)) = get_local ctxt in 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

161 
[pretty_rules ctxt "coinduct type:" coinductT, 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

162 
pretty_rules ctxt "coinduct pred:" coinductP, 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

163 
pretty_rules ctxt "induct type:" inductT, 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

164 
pretty_rules ctxt "induct pred:" inductP, 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

165 
pretty_rules ctxt "cases type:" casesT, 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

166 
pretty_rules ctxt "cases pred:" casesP] 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

167 
> Pretty.chunks > Pretty.writeln 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

168 
end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

169 

24867  170 
val _ = 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

171 
OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules" 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

172 
OuterKeyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o 
24867  173 
Toplevel.keep (print_rules o Toplevel.context_of))); 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

174 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

175 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

176 
(* access rules *) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

177 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

178 
val lookup_casesT = lookup_rule o #1 o #1 o get_local; 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

179 
val lookup_casesP = lookup_rule o #2 o #1 o get_local; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

180 
val lookup_inductT = lookup_rule o #1 o #2 o get_local; 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

181 
val lookup_inductP = lookup_rule o #2 o #2 o get_local; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

182 
val lookup_coinductT = lookup_rule o #1 o #3 o get_local; 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

183 
val lookup_coinductP = lookup_rule o #2 o #3 o get_local; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

184 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

185 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

186 
fun find_rules which how ctxt x = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

187 
map snd (NetRules.retrieve (which (get_local ctxt)) (how x)); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

188 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

189 
val find_casesT = find_rules (#1 o #1) encode_type; 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

190 
val find_casesP = find_rules (#2 o #1) I; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

191 
val find_inductT = find_rules (#1 o #2) encode_type; 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

192 
val find_inductP = find_rules (#2 o #2) I; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

193 
val find_coinductT = find_rules (#1 o #3) encode_type; 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

194 
val find_coinductP = find_rules (#2 o #3) I; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

195 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

196 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

197 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

198 
(** attributes **) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

199 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

200 
local 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

201 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

202 
fun mk_att f g name arg = 
27140  203 
let val (x, thm) = g arg in (InductData.map (f (name, thm)) x, thm) end; 
204 

205 
fun del_att which = Thm.declaration_attribute (fn th => InductData.map (which (pairself (fn rs => 

206 
fold NetRules.delete (filter_rules rs th) rs)))); 

24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

207 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

208 
fun map1 f (x, y, z) = (f x, y, z); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

209 
fun map2 f (x, y, z) = (x, f y, z); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

210 
fun map3 f (x, y, z) = (x, y, f z); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

211 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

212 
fun add_casesT rule x = map1 (apfst (NetRules.insert rule)) x; 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

213 
fun add_casesP rule x = map1 (apsnd (NetRules.insert rule)) x; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

214 
fun add_inductT rule x = map2 (apfst (NetRules.insert rule)) x; 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

215 
fun add_inductP rule x = map2 (apsnd (NetRules.insert rule)) x; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

216 
fun add_coinductT rule x = map3 (apfst (NetRules.insert rule)) x; 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

217 
fun add_coinductP rule x = map3 (apsnd (NetRules.insert rule)) x; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

218 

27140  219 
val consumes0 = RuleCases.consumes_default 0; 
220 
val consumes1 = RuleCases.consumes_default 1; 

24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

221 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

222 
in 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

223 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

224 
val cases_type = mk_att add_casesT consumes0; 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

225 
val cases_pred = mk_att add_casesP consumes1; 
27140  226 
val cases_del = del_att map1; 
227 

24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

228 
val induct_type = mk_att add_inductT consumes0; 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

229 
val induct_pred = mk_att add_inductP consumes1; 
27140  230 
val induct_del = del_att map2; 
231 

24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

232 
val coinduct_type = mk_att add_coinductT consumes0; 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

233 
val coinduct_pred = mk_att add_coinductP consumes1; 
27140  234 
val coinduct_del = del_att map3; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

235 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

236 
end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

237 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

238 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

239 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

240 
(** attribute syntax **) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

241 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

242 
val casesN = "cases"; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

243 
val inductN = "induct"; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

244 
val coinductN = "coinduct"; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

245 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

246 
val typeN = "type"; 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

247 
val predN = "pred"; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

248 
val setN = "set"; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

249 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

250 
local 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

251 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

252 
fun spec k arg = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

253 
Scan.lift (Args.$$$ k  Args.colon)  arg  
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

254 
Scan.lift (Args.$$$ k) >> K ""; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

255 

27140  256 
fun attrib add_type add_pred del = Attrib.syntax 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

257 
(spec typeN Args.tyname >> add_type  
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

258 
spec predN Args.const >> add_pred  
27140  259 
spec setN Args.const >> add_pred  
260 
Scan.lift Args.del >> K del); 

24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

261 

27140  262 
val cases_att = attrib cases_type cases_pred cases_del; 
263 
val induct_att = attrib induct_type induct_pred induct_del; 

264 
val coinduct_att = attrib coinduct_type coinduct_pred coinduct_del; 

24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

265 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

266 
in 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

267 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

268 
val attrib_setup = Attrib.add_attributes 
27140  269 
[(casesN, cases_att, "declaration of cases rule"), 
270 
(inductN, induct_att, "declaration of induction rule"), 

271 
(coinductN, coinduct_att, "declaration of coinduction rule")]; 

24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

272 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

273 
end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

274 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

275 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

276 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

277 
(** method utils **) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

278 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

279 
(* alignment *) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

280 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

281 
fun align_left msg xs ys = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

282 
let val m = length xs and n = length ys 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

283 
in if m < n then error msg else (Library.take (n, xs) ~~ ys) end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

284 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

285 
fun align_right msg xs ys = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

286 
let val m = length xs and n = length ys 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

287 
in if m < n then error msg else (Library.drop (m  n, xs) ~~ ys) end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

288 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

289 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

290 
(* prep_inst *) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

291 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

292 
fun prep_inst thy align tune (tm, ts) = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

293 
let 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

294 
val cert = Thm.cterm_of thy; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

295 
fun prep_var (x, SOME t) = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

296 
let 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

297 
val cx = cert x; 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26568
diff
changeset

298 
val xT = #T (Thm.rep_cterm cx); 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

299 
val ct = cert (tune t); 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26568
diff
changeset

300 
val tT = Thm.ctyp_of_term ct; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

301 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26568
diff
changeset

302 
if Type.could_unify (Thm.typ_of tT, xT) then SOME (cx, ct) 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

303 
else error (Pretty.string_of (Pretty.block 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

304 
[Pretty.str "Illtyped instantiation:", Pretty.fbrk, 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

305 
Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1, 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

306 
Display.pretty_ctyp (#T (Thm.crep_cterm ct))])) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

307 
end 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

308 
 prep_var (_, NONE) = NONE; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

309 
val xs = vars_of tm; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

310 
in 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

311 
align "Rule has fewer variables than instantiations given" xs ts 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

312 
> map_filter prep_var 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

313 
end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

314 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

315 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

316 
(* trace_rules *) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

317 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

318 
fun trace_rules _ kind [] = error ("Unable to figure out " ^ kind ^ " rule") 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

319 
 trace_rules ctxt _ rules = Method.trace ctxt rules; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

320 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

321 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

322 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

323 
(** cases method **) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

324 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

325 
(* 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

326 
rule selection scheme: 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

327 
cases  default case split 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

328 
`A t` cases ...  predicate/set cases 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

329 
cases t  type cases 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

330 
... cases ... r  explicit rule 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

331 
*) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

332 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

333 
local 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

334 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

335 
fun get_casesT ctxt ((SOME t :: _) :: _) = find_casesT ctxt (Term.fastype_of t) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

336 
 get_casesT _ _ = []; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

337 

24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

338 
fun get_casesP ctxt (fact :: _) = find_casesP ctxt (Thm.concl_of fact) 
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

339 
 get_casesP _ _ = []; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

340 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

341 
in 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

342 

26924  343 
fun cases_tac ctxt insts opt_rule facts = 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

344 
let 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

345 
val thy = ProofContext.theory_of ctxt; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

346 
val cert = Thm.cterm_of thy; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

347 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

348 
fun inst_rule r = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

349 
if null insts then `RuleCases.get r 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

350 
else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

351 
> maps (prep_inst thy align_left I) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

352 
> Drule.cterm_instantiate) r > pair (RuleCases.get r); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

353 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

354 
val ruleq = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

355 
(case opt_rule of 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

356 
SOME r => Seq.single (inst_rule r) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

357 
 NONE => 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

358 
(get_casesP ctxt facts @ get_casesT ctxt insts @ [Data.cases_default]) 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

359 
> tap (trace_rules ctxt casesN) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

360 
> Seq.of_list > Seq.maps (Seq.try inst_rule)); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

361 
in 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

362 
fn i => fn st => 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

363 
ruleq 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

364 
> Seq.maps (RuleCases.consume [] facts) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

365 
> Seq.maps (fn ((cases, (_, more_facts)), rule) => 
26924  366 
CASES (RuleCases.make_common false (thy, Thm.prop_of rule) cases) 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

367 
(Method.insert_tac more_facts i THEN Tactic.rtac rule i) st) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

368 
end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

369 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

370 
end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

371 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

372 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

373 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

374 
(** induct method **) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

375 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

376 
val conjunction_congs = [@{thm Pure.all_conjunction}, @{thm imp_conjunction}]; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

377 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

378 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

379 
(* atomize *) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

380 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

381 
fun atomize_term thy = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

382 
MetaSimplifier.rewrite_term thy Data.atomize [] 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

383 
#> ObjectLogic.drop_judgment thy; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

384 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

385 
val atomize_cterm = MetaSimplifier.rewrite true Data.atomize; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

386 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

387 
val atomize_tac = Simplifier.rewrite_goal_tac Data.atomize; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

388 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

389 
val inner_atomize_tac = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

390 
Simplifier.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

391 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

392 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

393 
(* rulify *) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

394 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

395 
fun rulify_term thy = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

396 
MetaSimplifier.rewrite_term thy (Data.rulify @ conjunction_congs) [] #> 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

397 
MetaSimplifier.rewrite_term thy Data.rulify_fallback []; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

398 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

399 
fun rulified_term thm = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

400 
let 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

401 
val thy = Thm.theory_of_thm thm; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

402 
val rulify = rulify_term thy; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

403 
val (As, B) = Logic.strip_horn (Thm.prop_of thm); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

404 
in (thy, Logic.list_implies (map rulify As, rulify B)) end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

405 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

406 
val rulify_tac = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

407 
Simplifier.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN' 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

408 
Simplifier.rewrite_goal_tac Data.rulify_fallback THEN' 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

409 
Goal.conjunction_tac THEN_ALL_NEW 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

410 
(Simplifier.rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

411 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

412 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

413 
(* prepare rule *) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

414 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

415 
fun rule_instance thy inst rule = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

416 
Drule.cterm_instantiate (prep_inst thy align_left I (Thm.prop_of rule, inst)) rule; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

417 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

418 
fun internalize k th = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

419 
th > Thm.permute_prems 0 k 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

420 
> Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of th  k) atomize_cterm); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

421 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

422 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

423 
(* guess rule instantiation  cannot handle pending goal parameters *) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

424 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

425 
local 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

426 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

427 
fun dest_env thy (env as Envir.Envir {iTs, ...}) = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

428 
let 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

429 
val cert = Thm.cterm_of thy; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

430 
val certT = Thm.ctyp_of thy; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

431 
val pairs = Envir.alist_of env; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

432 
val ts = map (cert o Envir.norm_term env o #2 o #2) pairs; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

433 
val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

434 
in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) (Vartab.dest iTs), xs ~~ ts) end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

435 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

436 
in 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

437 

26940  438 
fun guess_instance ctxt rule i st = 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

439 
let 
26940  440 
val thy = ProofContext.theory_of ctxt; 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26568
diff
changeset

441 
val maxidx = Thm.maxidx_of st; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

442 
val goal = Thm.term_of (Thm.cprem_of st i); (*exception Subscript*) 
29276  443 
val params = rev (Term.rename_wrt_term goal (Logic.strip_params goal)); 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

444 
in 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

445 
if not (null params) then 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

446 
(warning ("Cannot determine rule instantiation due to pending parameter(s): " ^ 
26940  447 
commas_quote (map (Syntax.string_of_term ctxt o Syntax.mark_boundT) params)); 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

448 
Seq.single rule) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

449 
else 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

450 
let 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

451 
val rule' = Thm.incr_indexes (maxidx + 1) rule; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

452 
val concl = Logic.strip_assums_concl goal; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

453 
in 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

454 
Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

455 
(Envir.empty (#maxidx (Thm.rep_thm rule'))) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

456 
> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule') 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

457 
end 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

458 
end handle Subscript => Seq.empty; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

459 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

460 
end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

461 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

462 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

463 
(* special renaming of rule parameters *) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

464 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

465 
fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

466 
let 
26712
e2dcda7b0401
adapted to ProofContext.revert_skolem: extra Name.clean required;
wenzelm
parents:
26626
diff
changeset

467 
val x = Name.clean (ProofContext.revert_skolem ctxt z); 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

468 
fun index i [] = [] 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

469 
 index i (y :: ys) = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

470 
if x = y then x ^ string_of_int i :: index (i + 1) ys 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

471 
else y :: index i ys; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

472 
fun rename_params [] = [] 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

473 
 rename_params ((y, Type (U, _)) :: ys) = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

474 
(if U = T then x else y) :: rename_params ys 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

475 
 rename_params ((y, _) :: ys) = y :: rename_params ys; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

476 
fun rename_asm A = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

477 
let 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

478 
val xs = rename_params (Logic.strip_params A); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

479 
val xs' = 
28375  480 
(case filter (fn x' => x' = x) xs of 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

481 
[] => xs  [_] => xs  _ => index 1 xs); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

482 
in Logic.list_rename_params (xs', A) end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

483 
fun rename_prop p = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

484 
let val (As, C) = Logic.strip_horn p 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

485 
in Logic.list_implies (map rename_asm As, C) end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

486 
val cp' = cterm_fun rename_prop (Thm.cprop_of thm); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

487 
val thm' = Thm.equal_elim (Thm.reflexive cp') thm; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

488 
in [RuleCases.save thm thm'] end 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

489 
 special_rename_params _ _ ths = ths; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

490 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

491 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

492 
(* fix_tac *) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

493 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

494 
local 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

495 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

496 
fun goal_prefix k ((c as Const ("all", _)) $ Abs (a, T, B)) = c $ Abs (a, T, goal_prefix k B) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

497 
 goal_prefix 0 _ = Term.dummy_pattern propT 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

498 
 goal_prefix k ((c as Const ("==>", _)) $ A $ B) = c $ A $ goal_prefix (k  1) B 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

499 
 goal_prefix _ _ = Term.dummy_pattern propT; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

500 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

501 
fun goal_params k (Const ("all", _) $ Abs (_, _, B)) = goal_params k B + 1 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

502 
 goal_params 0 _ = 0 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

503 
 goal_params k (Const ("==>", _) $ _ $ B) = goal_params (k  1) B 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

504 
 goal_params _ _ = 0; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

505 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

506 
fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) => 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

507 
let 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

508 
val thy = ProofContext.theory_of ctxt; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

509 
val cert = Thm.cterm_of thy; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

510 
val certT = Thm.ctyp_of thy; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

511 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

512 
val v = Free (x, T); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

513 
fun spec_rule prfx (xs, body) = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

514 
@{thm Pure.meta_spec} 
26712
e2dcda7b0401
adapted to ProofContext.revert_skolem: extra Name.clean required;
wenzelm
parents:
26626
diff
changeset

515 
> Thm.rename_params_rule ([Name.clean (ProofContext.revert_skolem ctxt x)], 1) 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

516 
> Thm.lift_rule (cert prfx) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

517 
> `(Thm.prop_of #> Logic.strip_assums_concl) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

518 
> (fn pred $ arg => 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

519 
Drule.cterm_instantiate 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

520 
[(cert (Term.head_of pred), cert (Logic.rlist_abs (xs, body))), 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

521 
(cert (Term.head_of arg), cert (Logic.rlist_abs (xs, v)))]); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

522 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

523 
fun goal_concl k xs (Const ("all", _) $ Abs (a, T, B)) = goal_concl k ((a, T) :: xs) B 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

524 
 goal_concl 0 xs B = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

525 
if not (Term.exists_subterm (fn t => t aconv v) B) then NONE 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

526 
else SOME (xs, Term.absfree (x, T, Term.incr_boundvars 1 B)) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

527 
 goal_concl k xs (Const ("==>", _) $ _ $ B) = goal_concl (k  1) xs B 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

528 
 goal_concl _ _ _ = NONE; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

529 
in 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

530 
(case goal_concl n [] goal of 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

531 
SOME concl => 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

532 
(compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN' rtac asm_rl) i 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

533 
 NONE => all_tac) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

534 
end); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

535 

24832  536 
fun miniscope_tac p = CONVERSION o 
26568  537 
Conv.params_conv p (K (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq])); 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

538 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

539 
in 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

540 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

541 
fun fix_tac _ _ [] = K all_tac 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

542 
 fix_tac ctxt n xs = SUBGOAL (fn (goal, i) => 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

543 
(EVERY' (map (meta_spec_tac ctxt n) xs) THEN' 
24832  544 
(miniscope_tac (goal_params n goal) ctxt)) i); 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

545 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

546 
end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

547 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

548 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

549 
(* add_defs *) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

550 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

551 
fun add_defs def_insts = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

552 
let 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

553 
fun add (SOME (SOME x, t)) ctxt = 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

554 
let val ([(lhs, (_, th))], ctxt') = 
28965  555 
LocalDefs.add_defs [((x, NoSyn), ((Binding.empty, []), t))] ctxt 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

556 
in ((SOME lhs, [th]), ctxt') end 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

557 
 add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

558 
 add NONE ctxt = ((NONE, []), ctxt); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

559 
in fold_map add def_insts #> apfst (split_list #> apsnd flat) end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

560 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

561 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

562 
(* induct_tac *) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

563 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

564 
(* 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

565 
rule selection scheme: 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

566 
`A x` induct ...  predicate/set induction 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

567 
induct x  type induction 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

568 
... induct ... r  explicit rule 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

569 
*) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

570 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

571 
fun get_inductT ctxt insts = 
27323
385c0ce33173
tuned get_inductT: *all* rules for missing instantiation;
wenzelm
parents:
27140
diff
changeset

572 
fold_rev multiply (insts > map 
385c0ce33173
tuned get_inductT: *all* rules for missing instantiation;
wenzelm
parents:
27140
diff
changeset

573 
((fn [] => NONE  ts => List.last ts) #> 
385c0ce33173
tuned get_inductT: *all* rules for missing instantiation;
wenzelm
parents:
27140
diff
changeset

574 
(fn NONE => TVar (("'a", 0), [])  SOME t => Term.fastype_of t) #> 
385c0ce33173
tuned get_inductT: *all* rules for missing instantiation;
wenzelm
parents:
27140
diff
changeset

575 
find_inductT ctxt)) [[]] 
27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
27809
diff
changeset

576 
> filter_out (forall Thm.is_internal); 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

577 

24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

578 
fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact)) 
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

579 
 get_inductP _ _ = []; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

580 

26924  581 
fun induct_tac ctxt def_insts arbitrary taking opt_rule facts = 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

582 
let 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

583 
val thy = ProofContext.theory_of ctxt; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

584 
val cert = Thm.cterm_of thy; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

585 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

586 
val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt >> split_list; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

587 
val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

588 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

589 
fun inst_rule (concls, r) = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

590 
(if null insts then `RuleCases.get r 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

591 
else (align_left "Rule has fewer conclusions than arguments given" 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

592 
(map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

593 
> maps (prep_inst thy align_right (atomize_term thy)) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

594 
> Drule.cterm_instantiate) r > pair (RuleCases.get r)) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

595 
> (fn ((cases, consumes), th) => (((cases, concls), consumes), th)); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

596 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

597 
val ruleq = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

598 
(case opt_rule of 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

599 
SOME rs => Seq.single (inst_rule (RuleCases.strict_mutual_rule ctxt rs)) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

600 
 NONE => 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

601 
(get_inductP ctxt facts @ 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

602 
map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts)) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

603 
> map_filter (RuleCases.mutual_rule ctxt) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

604 
> tap (trace_rules ctxt inductN o map #2) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

605 
> Seq.of_list > Seq.maps (Seq.try inst_rule)); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

606 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

607 
fun rule_cases rule = 
26924  608 
RuleCases.make_nested false (Thm.prop_of rule) (rulified_term rule); 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

609 
in 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

610 
(fn i => fn st => 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

611 
ruleq 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

612 
> Seq.maps (RuleCases.consume (flat defs) facts) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

613 
> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) => 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

614 
(PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j => 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

615 
(CONJUNCTS (ALLGOALS 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

616 
(Method.insert_tac (more_facts @ nth_list atomized_defs (j  1)) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

617 
THEN' fix_tac defs_ctxt 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

618 
(nth concls (j  1) + more_consumes) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

619 
(nth_list arbitrary (j  1)))) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

620 
THEN' inner_atomize_tac) j)) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

621 
THEN' atomize_tac) i st > Seq.maps (fn st' => 
26940  622 
guess_instance ctxt (internalize more_consumes rule) i st' 
24865  623 
> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking)) 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

624 
> Seq.maps (fn rule' => 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

625 
CASES (rule_cases rule' cases) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

626 
(Tactic.rtac rule' i THEN 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

627 
PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st')))) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

628 
THEN_ALL_NEW_CASES rulify_tac 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

629 
end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

630 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

631 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

632 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

633 
(** coinduct method **) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

634 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

635 
(* 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

636 
rule selection scheme: 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

637 
goal "A x" coinduct ...  predicate/set coinduction 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

638 
coinduct x  type coinduction 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

639 
coinduct ... r  explicit rule 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

640 
*) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

641 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

642 
local 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

643 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

644 
fun get_coinductT ctxt (SOME t :: _) = find_coinductT ctxt (Term.fastype_of t) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

645 
 get_coinductT _ _ = []; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

646 

24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

647 
fun get_coinductP ctxt goal = find_coinductP ctxt (Logic.strip_assums_concl goal); 
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

648 

cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

649 
fun main_prop_of th = 
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

650 
if RuleCases.get_consumes th > 0 then Thm.major_prem_of th else Thm.concl_of th; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

651 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

652 
in 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

653 

26924  654 
fun coinduct_tac ctxt inst taking opt_rule facts = 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

655 
let 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

656 
val thy = ProofContext.theory_of ctxt; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

657 
val cert = Thm.cterm_of thy; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

658 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

659 
fun inst_rule r = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

660 
if null inst then `RuleCases.get r 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

661 
else Drule.cterm_instantiate (prep_inst thy align_right I (main_prop_of r, inst)) r 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

662 
> pair (RuleCases.get r); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

663 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

664 
fun ruleq goal = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

665 
(case opt_rule of 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

666 
SOME r => Seq.single (inst_rule r) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

667 
 NONE => 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

668 
(get_coinductP ctxt goal @ get_coinductT ctxt inst) 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

669 
> tap (trace_rules ctxt coinductN) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

670 
> Seq.of_list > Seq.maps (Seq.try inst_rule)); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

671 
in 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

672 
SUBGOAL_CASES (fn (goal, i) => fn st => 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

673 
ruleq goal 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

674 
> Seq.maps (RuleCases.consume [] facts) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

675 
> Seq.maps (fn ((cases, (_, more_facts)), rule) => 
26940  676 
guess_instance ctxt rule i st 
24865  677 
> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking)) 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

678 
> Seq.maps (fn rule' => 
26924  679 
CASES (RuleCases.make_common false (thy, Thm.prop_of rule') cases) 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

680 
(Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st))) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

681 
end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

682 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

683 
end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

684 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

685 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

686 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

687 
(** concrete syntax **) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

688 

27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27370
diff
changeset

689 
structure P = OuterParse; 
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27370
diff
changeset

690 

24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

691 
val arbitraryN = "arbitrary"; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

692 
val takingN = "taking"; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

693 
val ruleN = "rule"; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

694 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

695 
local 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

696 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

697 
fun single_rule [rule] = rule 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

698 
 single_rule _ = error "Single rule expected"; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

699 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

700 
fun named_rule k arg get = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

701 
Scan.lift (Args.$$$ k  Args.colon)  Scan.repeat arg : 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

702 
(fn names => Scan.peek (fn context => Scan.succeed (names > map (fn name => 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

703 
(case get (Context.proof_of context) name of SOME x => x 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

704 
 NONE => error ("No rule for " ^ k ^ " " ^ quote name)))))); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

705 

24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

706 
fun rule get_type get_pred = 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

707 
named_rule typeN Args.tyname get_type  
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

708 
named_rule predN Args.const get_pred  
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

709 
named_rule setN Args.const get_pred  
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

710 
Scan.lift (Args.$$$ ruleN  Args.colon)  Attrib.thms; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

711 

24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

712 
val cases_rule = rule lookup_casesT lookup_casesP >> single_rule; 
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

713 
val induct_rule = rule lookup_inductT lookup_inductP; 
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

714 
val coinduct_rule = rule lookup_coinductT lookup_coinductP >> single_rule; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

715 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

716 
val inst = Scan.lift (Args.$$$ "_") >> K NONE  Args.term >> SOME; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

717 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

718 
val def_inst = 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

719 
((Scan.lift (Args.binding  (Args.$$$ "\<equiv>"  Args.$$$ "==")) >> SOME) 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

720 
 Args.term) >> SOME  
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

721 
inst >> Option.map (pair NONE); 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

722 

27370  723 
val free = Args.context  Args.term >> (fn (_, Free v) => v  (ctxt, t) => 
724 
error ("Bad free variable: " ^ Syntax.string_of_term ctxt t)); 

24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

725 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

726 
fun unless_more_args scan = Scan.unless (Scan.lift 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

727 
((Args.$$$ arbitraryN  Args.$$$ takingN  Args.$$$ typeN  
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

728 
Args.$$$ predN  Args.$$$ setN  Args.$$$ ruleN)  Args.colon)) scan; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

729 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

730 
val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN  Args.colon)  
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27370
diff
changeset

731 
P.and_list1' (Scan.repeat (unless_more_args free))) []; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

732 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

733 
val taking = Scan.optional (Scan.lift (Args.$$$ takingN  Args.colon)  
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

734 
Scan.repeat1 (unless_more_args inst)) []; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

735 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

736 
in 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

737 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

738 
fun cases_meth src = 
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27370
diff
changeset

739 
Method.syntax (P.and_list' (Scan.repeat (unless_more_args inst))  Scan.option cases_rule) src 
26924  740 
#> (fn ((insts, opt_rule), ctxt) => 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

741 
Method.METHOD_CASES (fn facts => 
26924  742 
Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts)))); 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

743 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

744 
fun induct_meth src = 
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27370
diff
changeset

745 
Method.syntax (P.and_list' (Scan.repeat (unless_more_args def_inst))  
26924  746 
(arbitrary  taking  Scan.option induct_rule)) src 
747 
#> (fn ((insts, ((arbitrary, taking), opt_rule)), ctxt) => 

24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

748 
Method.RAW_METHOD_CASES (fn facts => 
26924  749 
Seq.DETERM (HEADGOAL (induct_tac ctxt insts arbitrary taking opt_rule facts)))); 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

750 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

751 
fun coinduct_meth src = 
26924  752 
Method.syntax (Scan.repeat (unless_more_args inst)  taking  Scan.option coinduct_rule) src 
753 
#> (fn (((insts, taking), opt_rule), ctxt) => 

24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

754 
Method.RAW_METHOD_CASES (fn facts => 
26924  755 
Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts)))); 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

756 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

757 
end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

758 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

759 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

760 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

761 
(** theory setup **) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

762 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

763 
val setup = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

764 
attrib_setup #> 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

765 
Method.add_methods 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

766 
[(casesN, cases_meth, "case analysis on types or predicates/sets"), 
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

767 
(inductN, induct_meth, "induction on types or predicates/sets"), 
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

768 
(coinductN, coinduct_meth, "coinduction on types or predicates/sets")]; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

769 

a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

770 
end; 