author  blanchet 
Mon, 15 Sep 2014 10:49:07 +0200  
changeset 58335  a5a3b576fcfb 
parent 58002  0ed1e999a0fb 
child 58826  2ed2eaabe3df 
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 

37524  7 
signature INDUCT_ARGS = 
24830
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 
34987
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

13 
val equal_def: thm 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

14 
val dest_def: term > (term * term) option 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

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

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

17 

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

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

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

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

21 
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

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

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

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

25 
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

26 
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

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

28 
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

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

30 
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

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

32 
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

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

34 
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

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

36 
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

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

38 
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

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

40 
val cases_pred: string > attribute 
27140  41 
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

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

43 
val induct_pred: string > attribute 
27140  44 
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

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

46 
val coinduct_pred: string > attribute 
27140  47 
val coinduct_del: attribute 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset

48 
val map_simpset: (Proof.context > Proof.context) > Context.generic > Context.generic 
36602
0cbcdfd9e527
slightly more standard induct_simp_add/del attributes;
wenzelm
parents:
35625
diff
changeset

49 
val induct_simp_add: attribute 
0cbcdfd9e527
slightly more standard induct_simp_add/del attributes;
wenzelm
parents:
35625
diff
changeset

50 
val induct_simp_del: attribute 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

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

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

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

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

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

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

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

58 
(*proof methods*) 
45132  59 
val arbitrary_tac: Proof.context > int > (string * typ) list > int > tactic 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

60 
val add_defs: (binding option * (term * bool)) 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

61 
(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

62 
val atomize_term: theory > term > term 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

63 
val atomize_cterm: Proof.context > conv 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

64 
val atomize_tac: Proof.context > int > tactic 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

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

66 
val rulified_term: thm > theory * term 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

67 
val rulify_tac: Proof.context > int > tactic 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

68 
val simplified_rule: Proof.context > thm > thm 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

69 
val simplify_tac: Proof.context > int > tactic 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

70 
val trivial_tac: int > tactic 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

71 
val rotate_tac: int > int > int > tactic 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

72 
val internalize: Proof.context > int > thm > thm 
26940  73 
val guess_instance: Proof.context > thm > int > thm > thm Seq.seq 
34987
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

74 
val cases_tac: Proof.context > bool > 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

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

76 
val get_inductT: Proof.context > term option list list > thm list list 
45014
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
44942
diff
changeset

77 
type case_data = (((string * string list) * string list) list * int) (* FIXME > rule_cases.ML *) 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
44942
diff
changeset

78 
val gen_induct_tac: (theory > case_data * thm > case_data * thm) > 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
44942
diff
changeset

79 
Proof.context > bool > (binding option * (term * bool)) option list list > 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
44942
diff
changeset

80 
(string * typ) list list > term option list > thm list option > 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
44942
diff
changeset

81 
thm list > int > cases_tactic 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

82 
val induct_tac: Proof.context > bool > (binding option * (term * bool)) option list list > 
26924  83 
(string * typ) list list > term option list > thm list option > 
84 
thm list > int > cases_tactic 

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

86 
thm list > int > cases_tactic 

45014
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
44942
diff
changeset

87 
val gen_induct_setup: binding > 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
44942
diff
changeset

88 
(Proof.context > bool > (binding option * (term * bool)) option list list > 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
44942
diff
changeset

89 
(string * typ) list list > term option list > thm list option > 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
44942
diff
changeset

90 
thm list > int > cases_tactic) > 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
44942
diff
changeset

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

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

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

94 

37524  95 
functor Induct(Induct_Args: INDUCT_ARGS): INDUCT = 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

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

97 

37523  98 
(** variables  ordered lefttoright, preferring right **) 
24830
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 vars_of tm = 
45131  101 
rev (distinct (op =) (Term.fold_aterms (fn t as Var _ => cons t  _ => I) tm [])); 
24830
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 
local 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

104 

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

106 

47060
e2741ec9ae36
prefer explicitly qualified exception List.Empty;
wenzelm
parents:
46961
diff
changeset

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

108 
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

109 

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

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

111 

47060
e2741ec9ae36
prefer explicitly qualified exception List.Empty;
wenzelm
parents:
46961
diff
changeset

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

113 
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

114 

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

115 
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

116 
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

117 

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

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

119 

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

120 

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

121 

34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

122 
(** constraint simplification **) 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

123 

b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

124 
(* rearrange parameters and premises to allow application of onepointrules *) 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

125 

b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

126 
fun swap_params_conv ctxt i j cv = 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

127 
let 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

128 
fun conv1 0 ctxt = Conv.forall_conv (cv o snd) ctxt 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

129 
 conv1 k ctxt = 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

130 
Conv.rewr_conv @{thm swap_params} then_conv 
37525  131 
Conv.forall_conv (conv1 (k  1) o snd) ctxt 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

132 
fun conv2 0 ctxt = conv1 j ctxt 
37525  133 
 conv2 k ctxt = Conv.forall_conv (conv2 (k  1) o snd) ctxt 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

134 
in conv2 i ctxt end; 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

135 

b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

136 
fun swap_prems_conv 0 = Conv.all_conv 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

137 
 swap_prems_conv i = 
37525  138 
Conv.implies_concl_conv (swap_prems_conv (i  1)) then_conv 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

139 
Conv.rewr_conv Drule.swap_prems_eq 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

140 

42361  141 
fun drop_judgment ctxt = Object_Logic.drop_judgment (Proof_Context.theory_of ctxt); 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

142 

b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

143 
fun find_eq ctxt t = 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

144 
let 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

145 
val l = length (Logic.strip_params t); 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

146 
val Hs = Logic.strip_assums_hyp t; 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

147 
fun find (i, t) = 
37525  148 
(case Induct_Args.dest_def (drop_judgment ctxt t) of 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

149 
SOME (Bound j, _) => SOME (i, j) 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

150 
 SOME (_, Bound j) => SOME (i, j) 
37525  151 
 _ => NONE); 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

152 
in 
37525  153 
(case get_first find (map_index I Hs) of 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

154 
NONE => NONE 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

155 
 SOME (0, 0) => NONE 
37525  156 
 SOME (i, j) => SOME (i, l  j  1, j)) 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

157 
end; 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

158 

37525  159 
fun mk_swap_rrule ctxt ct = 
160 
(case find_eq ctxt (term_of ct) of 

34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

161 
NONE => NONE 
37525  162 
 SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct)); 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

163 

37525  164 
val rearrange_eqs_simproc = 
56245  165 
Simplifier.simproc_global Pure.thy "rearrange_eqs" ["Pure.all t"] 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset

166 
(fn ctxt => fn t => mk_swap_rrule ctxt (cterm_of (Proof_Context.theory_of ctxt) t)); 
37525  167 

34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

168 

b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

169 
(* rotate k premises to the left by j, skipping over first j premises *) 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

170 

b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

171 
fun rotate_conv 0 j 0 = Conv.all_conv 
37525  172 
 rotate_conv 0 j k = swap_prems_conv j then_conv rotate_conv 1 j (k  1) 
173 
 rotate_conv i j k = Conv.implies_concl_conv (rotate_conv (i  1) j k); 

34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

174 

b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

175 
fun rotate_tac j 0 = K all_tac 
37525  176 
 rotate_tac j k = SUBGOAL (fn (goal, i) => 
177 
CONVERSION (rotate_conv 

178 
j (length (Logic.strip_assums_hyp goal)  j  k) k) i); 

179 

34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

180 

b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

181 
(* rulify operators around definition *) 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

182 

b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

183 
fun rulify_defs_conv ctxt ct = 
37524  184 
if exists_subterm (is_some o Induct_Args.dest_def) (term_of ct) andalso 
185 
not (is_some (Induct_Args.dest_def (drop_judgment ctxt (term_of ct)))) 

34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

186 
then 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

187 
(Conv.forall_conv (rulify_defs_conv o snd) ctxt else_conv 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

188 
Conv.implies_conv (Conv.try_conv (rulify_defs_conv ctxt)) 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

189 
(Conv.try_conv (rulify_defs_conv ctxt)) else_conv 
37524  190 
Conv.first_conv (map Conv.rewr_conv Induct_Args.rulify) then_conv 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

191 
Conv.try_conv (rulify_defs_conv ctxt)) ct 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

192 
else Conv.no_conv ct; 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

193 

b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

194 

b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

195 

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

196 
(** induct data **) 
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 
(* rules *) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

199 

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

201 

33373  202 
fun init_rules index : rules = 
203 
Item_Net.init 

204 
(fn ((s1, th1), (s2, th2)) => s1 = s2 andalso Thm.eq_thm_prop (th1, th2)) 

205 
(single o index); 

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

206 

27140  207 
fun filter_rules (rs: rules) th = 
30560  208 
filter (fn (_, th') => Thm.eq_thm_prop (th, th')) (Item_Net.content rs); 
27140  209 

30560  210 
fun lookup_rule (rs: rules) = AList.lookup (op =) (Item_Net.content rs); 
24830
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 pretty_rules ctxt kind rs = 
30560  213 
let val thms = map snd (Item_Net.content rs) 
51584  214 
in Pretty.big_list kind (map (Display.pretty_thm_item ctxt) thms) end; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

215 

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

216 

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

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

218 

37524  219 
structure Data = Generic_Data 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

220 
( 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

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

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

223 
((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

224 
(init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)), 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

225 
(init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)), 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset

226 
simpset_of (empty_simpset @{context} 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset

227 
addsimprocs [rearrange_eqs_simproc] addsimps [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

228 
val extend = I; 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

229 
fun merge (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1), simpset1), 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

230 
((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2), simpset2)) = 
30560  231 
((Item_Net.merge (casesT1, casesT2), Item_Net.merge (casesP1, casesP2)), 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

232 
(Item_Net.merge (inductT1, inductT2), Item_Net.merge (inductP1, inductP2)), 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

233 
(Item_Net.merge (coinductT1, coinductT2), Item_Net.merge (coinductP1, coinductP2)), 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

234 
merge_ss (simpset1, simpset2)); 
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 

37524  237 
val get_local = Data.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

238 

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

239 
fun dest_rules ctxt = 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

240 
let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP), _) = get_local ctxt in 
30560  241 
{type_cases = Item_Net.content casesT, 
242 
pred_cases = Item_Net.content casesP, 

243 
type_induct = Item_Net.content inductT, 

244 
pred_induct = Item_Net.content inductP, 

245 
type_coinduct = Item_Net.content coinductT, 

246 
pred_coinduct = Item_Net.content coinductP} 

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

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

248 

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

249 
fun print_rules ctxt = 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

250 
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

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

252 
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

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

254 
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

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

256 
pretty_rules ctxt "cases pred:" casesP] 
56334
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
56245
diff
changeset

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

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

259 

24867  260 
val _ = 
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
45375
diff
changeset

261 
Outer_Syntax.improper_command @{command_spec "print_induct_rules"} 
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
45375
diff
changeset

262 
"print induction and cases rules" 
51658
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51584
diff
changeset

263 
(Scan.succeed (Toplevel.unknown_context o 
24867  264 
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

265 

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

266 

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

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

268 

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

269 
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

270 
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

271 
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

272 
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

273 
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

274 
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

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 
fun find_rules which how ctxt x = 
30560  278 
map snd (Item_Net.retrieve (which (get_local ctxt)) (how x)); 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

279 

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

281 
val find_casesP = find_rules (#2 o #1) I; 
37523  282 
val find_inductT = find_rules (#1 o #2) Net.encode_type; 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

283 
val find_inductP = find_rules (#2 o #2) I; 
37523  284 
val find_coinductT = find_rules (#1 o #3) Net.encode_type; 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

285 
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

286 

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

287 

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 
(** attributes **) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

290 

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

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

292 

45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
45328
diff
changeset

293 
fun mk_att f g name = 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
45328
diff
changeset

294 
Thm.mixed_attribute (fn (context, thm) => 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
45328
diff
changeset

295 
let 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
45328
diff
changeset

296 
val thm' = g thm; 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
45328
diff
changeset

297 
val context' = Data.map (f (name, thm')) context; 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
45328
diff
changeset

298 
in (context', thm') end); 
27140  299 

37525  300 
fun del_att which = 
301 
Thm.declaration_attribute (fn th => Data.map (which (pairself (fn rs => 

302 
fold Item_Net.remove (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

303 

34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

304 
fun map1 f (x, y, z, s) = (f x, y, z, s); 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

305 
fun map2 f (x, y, z, s) = (x, f y, z, s); 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

306 
fun map3 f (x, y, z, s) = (x, y, f z, s); 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

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

308 

33373  309 
fun add_casesT rule x = map1 (apfst (Item_Net.update rule)) x; 
310 
fun add_casesP rule x = map1 (apsnd (Item_Net.update rule)) x; 

311 
fun add_inductT rule x = map2 (apfst (Item_Net.update rule)) x; 

312 
fun add_inductP rule x = map2 (apsnd (Item_Net.update rule)) x; 

313 
fun add_coinductT rule x = map3 (apfst (Item_Net.update rule)) x; 

314 
fun add_coinductP rule x = map3 (apsnd (Item_Net.update rule)) x; 

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

315 

45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
45328
diff
changeset

316 
val consumes0 = Rule_Cases.default_consumes 0; 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
45328
diff
changeset

317 
val consumes1 = Rule_Cases.default_consumes 1; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

318 

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

319 
in 
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 
val cases_type = mk_att add_casesT consumes0; 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

322 
val cases_pred = mk_att add_casesP consumes1; 
27140  323 
val cases_del = del_att map1; 
324 

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

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

326 
val induct_pred = mk_att add_inductP consumes1; 
27140  327 
val induct_del = del_att map2; 
328 

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

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

330 
val coinduct_pred = mk_att add_coinductP consumes1; 
27140  331 
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

332 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset

333 
fun map_simpset f context = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset

334 
context > (Data.map o map4 o Simplifier.simpset_map (Context.proof_of context)) f; 
36602
0cbcdfd9e527
slightly more standard induct_simp_add/del attributes;
wenzelm
parents:
35625
diff
changeset

335 

0cbcdfd9e527
slightly more standard induct_simp_add/del attributes;
wenzelm
parents:
35625
diff
changeset

336 
fun induct_simp f = 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset

337 
Thm.declaration_attribute (fn thm => map_simpset (fn ctxt => f (ctxt, [thm]))); 
36602
0cbcdfd9e527
slightly more standard induct_simp_add/del attributes;
wenzelm
parents:
35625
diff
changeset

338 

0cbcdfd9e527
slightly more standard induct_simp_add/del attributes;
wenzelm
parents:
35625
diff
changeset

339 
val induct_simp_add = induct_simp (op addsimps); 
0cbcdfd9e527
slightly more standard induct_simp_add/del attributes;
wenzelm
parents:
35625
diff
changeset

340 
val induct_simp_del = induct_simp (op delsimps); 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

341 

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

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

343 

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

344 

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

345 

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

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

347 

34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

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

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

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

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

352 

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

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

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

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

356 

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

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

358 

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

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

360 
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

361 
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

362 

30528  363 
fun attrib add_type add_pred del = 
55951
c07d184aebe9
tuned signature  more uniform check_type_name/read_type_name;
wenzelm
parents:
54742
diff
changeset

364 
spec typeN (Args.type_name {proper = false, strict = false}) >> add_type  
55954  365 
spec predN (Args.const {proper = false, strict = false}) >> add_pred  
366 
spec setN (Args.const {proper = false, strict = false}) >> add_pred  

30528  367 
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

368 

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

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

370 

30528  371 
val attrib_setup = 
30722
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30560
diff
changeset

372 
Attrib.setup @{binding cases} (attrib cases_type cases_pred cases_del) 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30560
diff
changeset

373 
"declaration of cases rule" #> 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30560
diff
changeset

374 
Attrib.setup @{binding induct} (attrib induct_type induct_pred induct_del) 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30560
diff
changeset

375 
"declaration of induction rule" #> 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30560
diff
changeset

376 
Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del) 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

377 
"declaration of coinduction rule" #> 
36602
0cbcdfd9e527
slightly more standard induct_simp_add/del attributes;
wenzelm
parents:
35625
diff
changeset

378 
Attrib.setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del) 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

379 
"declaration of rules for simplifying induction or cases rules"; 
24830
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 
end; 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

382 

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

383 

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 
(** method utils **) 
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 
(* alignment *) 
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 
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

390 
let val m = length xs and n = length ys 
33957  391 
in if m < n then error msg else (take n xs ~~ ys) end; 
24830
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 
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

394 
let val m = length xs and n = length ys 
33957  395 
in if m < n then error msg else (drop (m  n) xs ~~ ys) end; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

396 

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

397 

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

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

399 

32432
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32188
diff
changeset

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

401 
let 
42361  402 
val cert = Thm.cterm_of (Proof_Context.theory_of ctxt); 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

403 
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

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

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

406 
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

407 
val ct = cert (tune t); 
32432
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32188
diff
changeset

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

409 
in 
32432
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32188
diff
changeset

410 
if Type.could_unify (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

411 
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

412 
[Pretty.str "Illtyped instantiation:", Pretty.fbrk, 
32432
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32188
diff
changeset

413 
Syntax.pretty_term ctxt (Thm.term_of ct), Pretty.str " ::", Pretty.brk 1, 
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32188
diff
changeset

414 
Syntax.pretty_typ ctxt tT])) 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

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

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

417 
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

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

419 
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

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

421 
end; 
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 

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

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

425 

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

426 
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

427 
 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

428 

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

429 

34987
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

430 
(* mark equality constraints in cases rule *) 
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

431 

37524  432 
val equal_def' = Thm.symmetric Induct_Args.equal_def; 
34987
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

433 

c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

434 
fun mark_constraints n ctxt = Conv.fconv_rule 
45130  435 
(Conv.prems_conv ~1 (Conv.params_conv ~1 (K (Conv.prems_conv n 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

436 
(Raw_Simplifier.rewrite ctxt false [equal_def']))) ctxt)); 
34987
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

437 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

438 
fun unmark_constraints ctxt = 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

439 
Conv.fconv_rule (Raw_Simplifier.rewrite ctxt true [Induct_Args.equal_def]); 
34987
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

440 

37525  441 

34987
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

442 
(* simplify *) 
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

443 

c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

444 
fun simplify_conv' ctxt = 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset

445 
Simplifier.full_rewrite (put_simpset (#4 (get_local ctxt)) ctxt); 
34987
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

446 

c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

447 
fun simplify_conv ctxt ct = 
37524  448 
if exists_subterm (is_some o Induct_Args.dest_def) (term_of ct) then 
34987
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

449 
(Conv.try_conv (rulify_defs_conv ctxt) then_conv simplify_conv' ctxt) ct 
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

450 
else Conv.all_conv ct; 
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

451 

c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

452 
fun gen_simplified_rule cv ctxt = 
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

453 
Conv.fconv_rule (Conv.prems_conv ~1 (cv ctxt)); 
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

454 

c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

455 
val simplified_rule' = gen_simplified_rule simplify_conv'; 
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

456 
val simplified_rule = gen_simplified_rule simplify_conv; 
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

457 

c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

458 
fun simplify_tac ctxt = CONVERSION (simplify_conv ctxt); 
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

459 

37524  460 
val trivial_tac = Induct_Args.trivial_tac; 
34987
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

461 

c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

462 

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

463 

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

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

465 

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

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

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

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

469 
`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

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

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

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

473 

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

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

475 

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

476 
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

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

478 

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

479 
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

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

481 

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

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

483 

34987
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

484 
fun cases_tac ctxt simp 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

485 
let 
42361  486 
val thy = Proof_Context.theory_of ctxt; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

487 

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

488 
fun inst_rule r = 
34987
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

489 
(if null insts then r 
45131  490 
else 
491 
(align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts 

492 
> maps (prep_inst ctxt align_left I) 

493 
> Drule.cterm_instantiate) r) 

494 
> simp ? mark_constraints (Rule_Cases.get_constraints r) ctxt 

495 
> pair (Rule_Cases.get r); 

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

496 

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

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

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

499 
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

500 
 NONE => 
37524  501 
(get_casesP ctxt facts @ get_casesT ctxt insts @ [Induct_Args.cases_default]) 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

502 
> 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

503 
> 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

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

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

506 
ruleq 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

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

508 
> Seq.maps (fn ((cases, (_, more_facts)), rule) => 
45131  509 
let 
510 
val rule' = rule 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

511 
> simp ? (simplified_rule' ctxt #> unmark_constraints ctxt); 
34987
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

512 
in 
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

513 
CASES (Rule_Cases.make_common (thy, 
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

514 
Thm.prop_of (Rule_Cases.internalize_params rule')) cases) 
45130  515 
((Method.insert_tac more_facts THEN' rtac rule' THEN_ALL_NEW 
34987
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

516 
(if simp then TRY o trivial_tac else K all_tac)) i) st 
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

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

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

519 

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

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

521 

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 

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

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

525 

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

526 
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

527 

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

528 

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

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

530 

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

531 
fun atomize_term thy = 
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
38715
diff
changeset

532 
Raw_Simplifier.rewrite_term thy Induct_Args.atomize [] 
35625  533 
#> Object_Logic.drop_judgment thy; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

534 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

535 
fun atomize_cterm ctxt = Raw_Simplifier.rewrite ctxt true Induct_Args.atomize; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

536 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

537 
fun atomize_tac ctxt = rewrite_goal_tac ctxt Induct_Args.atomize; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

538 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

539 
fun inner_atomize_tac ctxt = 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

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

541 

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

542 

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

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

544 

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

545 
fun rulify_term thy = 
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
38715
diff
changeset

546 
Raw_Simplifier.rewrite_term thy (Induct_Args.rulify @ conjunction_congs) [] #> 
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
38715
diff
changeset

547 
Raw_Simplifier.rewrite_term thy Induct_Args.rulify_fallback []; 
24830
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 
fun rulified_term thm = 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

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

551 
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

552 
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

553 
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

554 
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

555 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

556 
fun rulify_tac ctxt = 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

557 
rewrite_goal_tac ctxt (Induct_Args.rulify @ conjunction_congs) THEN' 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

558 
rewrite_goal_tac ctxt Induct_Args.rulify_fallback THEN' 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

559 
Goal.conjunction_tac THEN_ALL_NEW 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

560 
(rewrite_goal_tac ctxt [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac ctxt); 
24830
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 

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

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

564 

32432
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32188
diff
changeset

565 
fun rule_instance ctxt inst rule = 
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32188
diff
changeset

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

567 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

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

569 
th > Thm.permute_prems 0 k 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

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

571 

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

572 

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

573 
(* 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

574 

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

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

576 

32032  577 
fun dest_env thy env = 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

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

579 
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

580 
val certT = Thm.ctyp_of thy; 
32032  581 
val pairs = Vartab.dest (Envir.term_env env); 
582 
val types = Vartab.dest (Envir.type_env env); 

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

583 
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

584 
val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts); 
32032  585 
in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) types, xs ~~ ts) end; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

586 

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

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

588 

26940  589 
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

590 
let 
42361  591 
val thy = Proof_Context.theory_of ctxt; 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26568
diff
changeset

592 
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

593 
val goal = Thm.term_of (Thm.cprem_of st i); (*exception Subscript*) 
29276  594 
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

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

596 
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

597 
(warning ("Cannot determine rule instantiation due to pending parameter(s): " ^ 
49660
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
47060
diff
changeset

598 
commas_quote (map (Syntax.string_of_term ctxt o Syntax_Trans.mark_bound_abs) params)); 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

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

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

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

602 
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

603 
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

604 
in 
32032  605 
Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule')) 
43333
2bdec7f430d3
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents:
43326
diff
changeset

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

607 
end 
43333
2bdec7f430d3
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents:
43326
diff
changeset

608 
end 
2bdec7f430d3
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents:
43326
diff
changeset

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

610 

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

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

612 

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

613 

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

614 
(* 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

615 

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

616 
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

617 
let 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42361
diff
changeset

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

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

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

621 
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

622 
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

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

624 
 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

625 
(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

626 
 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

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

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

629 
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

630 
val xs' = 
28375  631 
(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

632 
[] => xs  [_] => xs  _ => index 1 xs); 
45328  633 
in Logic.list_rename_params xs' A end; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

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

635 
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

636 
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

637 
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

638 
val thm' = Thm.equal_elim (Thm.reflexive cp') thm; 
33368  639 
in [Rule_Cases.save thm thm'] end 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

640 
 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

641 

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

642 

45132  643 
(* arbitrary_tac *) 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

644 

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

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

646 

56245  647 
fun goal_prefix k ((c as Const (@{const_name Pure.all}, _)) $ Abs (a, T, B)) = 
648 
c $ Abs (a, T, goal_prefix k B) 

45156  649 
 goal_prefix 0 _ = Term.dummy_prop 
56245  650 
 goal_prefix k ((c as Const (@{const_name Pure.imp}, _)) $ A $ B) = 
651 
c $ A $ goal_prefix (k  1) B 

45156  652 
 goal_prefix _ _ = Term.dummy_prop; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

653 

56245  654 
fun goal_params k (Const (@{const_name Pure.all}, _) $ Abs (_, _, B)) = goal_params k B + 1 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

655 
 goal_params 0 _ = 0 
56245  656 
 goal_params k (Const (@{const_name Pure.imp}, _) $ _ $ B) = goal_params (k  1) B 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

657 
 goal_params _ _ = 0; 
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 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

660 
let 
42361  661 
val thy = Proof_Context.theory_of ctxt; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

662 
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

663 

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

664 
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

665 
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

666 
@{thm Pure.meta_spec} 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42361
diff
changeset

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

668 
> 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

669 
> `(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

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

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

672 
[(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

673 
(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

674 

56245  675 
fun goal_concl k xs (Const (@{const_name Pure.all}, _) $ Abs (a, T, B)) = 
676 
goal_concl k ((a, T) :: xs) B 

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

677 
 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

678 
if not (Term.exists_subterm (fn t => t aconv v) B) then NONE 
44241  679 
else SOME (xs, absfree (x, T) (Term.incr_boundvars 1 B)) 
56245  680 
 goal_concl k xs (Const (@{const_name Pure.imp}, _) $ _ $ B) = 
681 
goal_concl (k  1) xs B 

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

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

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

684 
(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

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

686 
(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

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

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

689 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

690 
fun miniscope_tac p = 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

691 
CONVERSION o 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

692 
Conv.params_conv p (fn ctxt => 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

693 
Raw_Simplifier.rewrite ctxt 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

694 

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

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

696 

45132  697 
fun arbitrary_tac _ _ [] = K all_tac 
698 
 arbitrary_tac ctxt n xs = SUBGOAL (fn (goal, i) => 

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

699 
(EVERY' (map (meta_spec_tac ctxt n) xs) THEN' 
24832  700 
(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

701 

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

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

703 

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

704 

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

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

706 

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

707 
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

708 
let 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

709 
fun add (SOME (_, (t, true))) ctxt = ((SOME t, []), ctxt) 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

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

711 
let val ([(lhs, (_, th))], ctxt') = 
49748
a346daa8a1f4
clarified Local_Defs.add_def(s): refrain from hardwiring Thm.def_binding_optional;
wenzelm
parents:
49660
diff
changeset

712 
Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))] ctxt 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

713 
in ((SOME lhs, [th]), ctxt') end 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

714 
 add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt) 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

715 
 add (SOME (NONE, (t, _))) ctxt = 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

716 
let 
43326
47cf4bc789aa
simplified Name.variant  discontinued builtin fold_map;
wenzelm
parents:
43278
diff
changeset

717 
val (s, _) = Name.variant "x" (Variable.names_of ctxt); 
49748
a346daa8a1f4
clarified Local_Defs.add_def(s): refrain from hardwiring Thm.def_binding_optional;
wenzelm
parents:
49660
diff
changeset

718 
val x = Binding.name s; 
a346daa8a1f4
clarified Local_Defs.add_def(s): refrain from hardwiring Thm.def_binding_optional;
wenzelm
parents:
49660
diff
changeset

719 
val ([(lhs, (_, th))], ctxt') = ctxt 
a346daa8a1f4
clarified Local_Defs.add_def(s): refrain from hardwiring Thm.def_binding_optional;
wenzelm
parents:
49660
diff
changeset

720 
> Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))]; 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

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

722 
 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

723 
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

724 

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 
(* induct_tac *) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

727 

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

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

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

730 
`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

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

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

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

734 

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

735 
fun get_inductT ctxt insts = 
32188  736 
fold_rev (map_product cons) (insts > map 
27323
385c0ce33173
tuned get_inductT: *all* rules for missing instantiation;
wenzelm
parents:
27140
diff
changeset

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

738 
(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

739 
find_inductT ctxt)) [[]] 
33368  740 
> filter_out (forall Rule_Cases.is_inner_rule); 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

741 

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

742 
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

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

744 

45130  745 
type case_data = (((string * string list) * string list) list * int); 
45014
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
44942
diff
changeset

746 

0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
44942
diff
changeset

747 
fun gen_induct_tac mod_cases ctxt simp def_insts arbitrary taking opt_rule facts = 
56231
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

748 
SUBGOAL_CASES (fn (_, i, st) => 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

749 
let 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

750 
val thy = Proof_Context.theory_of ctxt; 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

751 

b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

752 
val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt >> split_list; 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

753 
val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs; 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

754 

b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

755 
fun inst_rule (concls, r) = 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

756 
(if null insts then `Rule_Cases.get r 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

757 
else (align_left "Rule has fewer conclusions than arguments given" 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

758 
(map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

759 
> maps (prep_inst ctxt align_right (atomize_term thy)) 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

760 
> Drule.cterm_instantiate) r > pair (Rule_Cases.get r)) 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

761 
> mod_cases thy 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

762 
> (fn ((cases, consumes), th) => (((cases, concls), consumes), th)); 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

763 

b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

764 
val ruleq = 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

765 
(case opt_rule of 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

766 
SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs)) 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

767 
 NONE => 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

768 
(get_inductP ctxt facts @ 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

769 
map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts)) 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

770 
> map_filter (Rule_Cases.mutual_rule ctxt) 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

771 
> tap (trace_rules ctxt inductN o map #2) 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

772 
> Seq.of_list > Seq.maps (Seq.try inst_rule)); 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

773 

b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

774 
fun rule_cases ctxt rule cases = 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

775 
let 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

776 
val rule' = Rule_Cases.internalize_params rule; 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

777 
val rule'' = rule' > simp ? simplified_rule ctxt; 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

778 
val nonames = map (fn ((cn, _), cls) => ((cn, []), cls)); 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

779 
val cases' = if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases; 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

780 
in Rule_Cases.make_nested (Thm.prop_of rule'') (rulified_term rule'') cases' end; 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

781 
in 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

782 
fn st => 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

783 
ruleq 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

784 
> Seq.maps (Rule_Cases.consume defs_ctxt (flat defs) facts) 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

785 
> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) => 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

786 
(PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j => 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

787 
(CONJUNCTS (ALLGOALS 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

788 
let 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

789 
val adefs = nth_list atomized_defs (j  1); 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

790 
val frees = fold (Term.add_frees o Thm.prop_of) adefs []; 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

791 
val xs = nth_list arbitrary (j  1); 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

792 
val k = nth concls (j  1) + more_consumes 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

793 
in 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

794 
Method.insert_tac (more_facts @ adefs) THEN' 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

795 
(if simp then 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

796 
rotate_tac k (length adefs) THEN' 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

797 
arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs > op @) 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

798 
else 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

799 
arbitrary_tac defs_ctxt k xs) 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

800 
end) 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

801 
THEN' inner_atomize_tac defs_ctxt) j)) 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

802 
THEN' atomize_tac defs_ctxt) i st > Seq.maps (fn st' => 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

803 
guess_instance ctxt (internalize ctxt more_consumes rule) i st' 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

804 
> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking)) 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

805 
> Seq.maps (fn rule' => 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

806 
CASES (rule_cases ctxt rule' cases) 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

807 
(rtac rule' i THEN 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

808 
PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))) 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

809 
end) 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

810 
THEN_ALL_NEW_CASES 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

811 
((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac) else K all_tac) 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

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

813 

45014
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
44942
diff
changeset

814 
val induct_tac = gen_induct_tac (K I); 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

815 

45130  816 

817 

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

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

819 

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

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

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

822 
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

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

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

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

826 

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

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

828 

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

829 
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

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

831 

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

832 
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

833 

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

834 
fun main_prop_of th = 
33368  835 
if Rule_Cases.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

836 

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

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

838 

56231
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

839 
fun coinduct_tac ctxt inst taking opt_rule facts = SUBGOAL_CASES (fn (goal, i, st) => 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

840 
let 
42361  841 
val thy = Proof_Context.theory_of ctxt; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

842 

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

843 
fun inst_rule r = 
33368  844 
if null inst then `Rule_Cases.get r 
32432
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32188
diff
changeset

845 
else Drule.cterm_instantiate (prep_inst ctxt align_right I (main_prop_of r, inst)) r 
33368  846 
> pair (Rule_Cases.get r); 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

847 

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

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

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

850 
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

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

852 
(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

853 
> 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

854 
> 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

855 
in 
56231
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

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

857 
ruleq goal 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53168
diff
changeset

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

859 
> Seq.maps (fn ((cases, (_, more_facts)), rule) => 
26940  860 
guess_instance ctxt rule i st 
32432
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32188
diff
changeset

861 
> Seq.map (rule_instance ctxt (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

862 
> Seq.maps (fn rule' => 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

863 
CASES (Rule_Cases.make_common (thy, 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

864 
Thm.prop_of (Rule_Cases.internalize_params rule')) cases) 
56231
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

865 
(Method.insert_tac more_facts i THEN rtac rule' i) st)) 
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES  clean tactical failure if outofrange;
wenzelm
parents:
55954
diff
changeset

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

867 

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

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

869 

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

870 

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

871 

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

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

873 

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

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

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

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

877 

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

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

879 

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

880 
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

881 
 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

882 

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

883 
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

884 
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

885 
(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

886 
(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

887 
 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

888 

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

889 
fun rule get_type get_pred = 
55951
c07d184aebe9
tuned signature  more uniform check_type_name/read_type_name;
wenzelm
parents:
54742
diff
changeset

890 
named_rule typeN (Args.type_name {proper = false, strict = false}) get_type  
55954  891 
named_rule predN (Args.const {proper = false, strict = false}) get_pred  
892 
named_rule setN (Args.const {proper = false, strict = false}) get_pred  

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

893 
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

894 

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

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

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

897 
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

898 

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

899 
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

900 

34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

901 
val inst' = Scan.lift (Args.$$$ "_") >> K NONE  
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

902 
Args.term >> (SOME o rpair false)  
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

903 
Scan.lift (Args.$$$ "(")  (Args.term >> (SOME o rpair true))  
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

904 
Scan.lift (Args.$$$ ")"); 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

905 

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

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

907 
((Scan.lift (Args.binding  (Args.$$$ "\<equiv>"  Args.$$$ "==")) >> SOME) 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

908 
 (Args.term >> rpair false)) >> SOME  
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

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

910 

27370  911 
val free = Args.context  Args.term >> (fn (_, Free v) => v  (ctxt, t) => 
912 
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

913 

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

914 
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

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

916 
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

917 

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

918 
val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN  Args.colon)  
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36602
diff
changeset

919 
Parse.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

920 

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

921 
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

922 
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

923 

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

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

925 

30722
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30560
diff
changeset

926 
val cases_setup = 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30560
diff
changeset

927 
Method.setup @{binding cases} 
53168  928 
(Scan.lift (Args.mode no_simpN)  
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36602
diff
changeset

929 
(Parse.and_list' (Scan.repeat (unless_more_args inst))  Scan.option cases_rule) >> 
34987
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

930 
(fn (no_simp, (insts, opt_rule)) => fn ctxt => 
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

931 
METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL 
c1e8af37ee75
Added infrastructure for simplifying equality constraints in cases rules.
berghofe
parents:
34907
diff
changeset

932 
(cases_tac ctxt (not no_simp) insts opt_rule facts))))) 
30722
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30560
diff
changeset

933 
"case analysis 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

934 

58002  935 
fun gen_induct_setup binding tac = 
45014
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
44942
diff
changeset

936 
Method.setup binding 
53168  937 
(Scan.lift (Args.mode no_simpN)  
938 
(Parse.and_list' (Scan.repeat (unless_more_args def_inst))  

939 
(arbitrary  taking  Scan.option induct_rule)) >> 

58002  940 
(fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt => fn facts => 
941 
Seq.DETERM (HEADGOAL (tac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))) 

30722
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30560
diff
changeset

942 
"induction 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

943 

45014
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
44942
diff
changeset

944 
val induct_setup = gen_induct_setup @{binding induct} induct_tac; 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
44942
diff
changeset

945 

30722
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30560
diff
changeset

946 
val coinduct_setup = 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30560
diff
changeset

947 
Method.setup @{binding coinduct} 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30560
diff
changeset

948 
(Scan.repeat (unless_more_args inst)  taking  Scan.option coinduct_rule >> 
58002  949 
(fn ((insts, taking), opt_rule) => fn ctxt => fn facts => 
950 
Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts)))) 

30722
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30560
diff
changeset

951 
"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

952 

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

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

954 

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

955 

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

956 

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

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

958 

30722
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30560
diff
changeset

959 
val setup = attrib_setup #> cases_setup #> induct_setup #> coinduct_setup; 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
diff
changeset

960 

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

961 
end; 