author  wenzelm 
Tue, 29 Sep 2009 22:48:24 +0200  
changeset 32765  3032c0308019 
parent 32603  e08fdd615333 
child 32950  5d5e123443b3 
permissions  rwrr 
31775  1 
(* Title: HOL/Tools/Function/induction_scheme.ML 
25589  2 
Author: Alexander Krauss, TU Muenchen 
3 

4 
A method to prove induction schemes. 

5 
*) 

25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

6 

5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

7 
signature INDUCTION_SCHEME = 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

8 
sig 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

9 
val mk_ind_tac : (int > tactic) > (int > tactic) > (int > tactic) 
30493
b8570ea1ce25
provide regular ML interfaces for Isar source language elements;
wenzelm
parents:
29183
diff
changeset

10 
> Proof.context > thm list > tactic 
b8570ea1ce25
provide regular ML interfaces for Isar source language elements;
wenzelm
parents:
29183
diff
changeset

11 
val induct_scheme_tac : Proof.context > thm list > tactic 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

12 
val setup : theory > theory 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

13 
end 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

14 

5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

15 

5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

16 
structure InductionScheme : INDUCTION_SCHEME = 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

17 
struct 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

18 

5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

19 
open FundefLib 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

20 

27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

21 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

22 
type rec_call_info = int * (string * typ) list * term list * term list 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

23 

5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

24 
datatype scheme_case = 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

25 
SchemeCase of 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

26 
{ 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

27 
bidx : int, 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

28 
qs: (string * typ) list, 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

29 
oqnames: string list, 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

30 
gs: term list, 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

31 
lhs: term list, 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

32 
rs: rec_call_info list 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

33 
} 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

34 

27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

35 
datatype scheme_branch = 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

36 
SchemeBranch of 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

37 
{ 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

38 
P : term, 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

39 
xs: (string * typ) list, 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

40 
ws: (string * typ) list, 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

41 
Cs: term list 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

42 
} 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

43 

25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

44 
datatype ind_scheme = 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

45 
IndScheme of 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

46 
{ 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

47 
T: typ, (* sum of products *) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

48 
branches: scheme_branch list, 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

49 
cases: scheme_case list 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

50 
} 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

51 

27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

52 
val ind_atomize = MetaSimplifier.rewrite true @{thms induct_atomize} 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

53 
val ind_rulify = MetaSimplifier.rewrite true @{thms induct_rulify} 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

54 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

55 
fun meta thm = thm RS eq_reflection 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

56 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

57 
val sum_prod_conv = MetaSimplifier.rewrite true 
29183
f1648e009dc1
removed duplicate sum_case used only by function package;
krauss
parents:
27369
diff
changeset

58 
(map meta (@{thm split_conv} :: @{thms sum.cases})) 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

59 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

60 
fun term_conv thy cv t = 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

61 
cv (cterm_of thy t) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

62 
> prop_of > Logic.dest_equals > snd 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

63 

5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

64 
fun mk_relT T = HOLogic.mk_setT (HOLogic.mk_prodT (T, T)) 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

65 

5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

66 
fun dest_hhf ctxt t = 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

67 
let 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

68 
val (ctxt', vars, imp) = dest_all_all_ctx ctxt t 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

69 
in 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

70 
(ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp) 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

71 
end 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

72 

27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

73 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

74 
fun mk_scheme' ctxt cases concl = 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

75 
let 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

76 
fun mk_branch concl = 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

77 
let 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

78 
val (ctxt', ws, Cs, _ $ Pxs) = dest_hhf ctxt concl 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

79 
val (P, xs) = strip_comb Pxs 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

80 
in 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

81 
SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs } 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

82 
end 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

83 

27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

84 
val (branches, cases') = (* correction *) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

85 
case Logic.dest_conjunction_list concl of 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

86 
[conc] => 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

87 
let 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

88 
val _ $ Pxs = Logic.strip_assums_concl conc 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

89 
val (P, _) = strip_comb Pxs 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

90 
val (cases', conds) = take_prefix (Term.exists_subterm (curry op aconv P)) cases 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

91 
val concl' = fold_rev (curry Logic.mk_implies) conds conc 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

92 
in 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

93 
([mk_branch concl'], cases') 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

94 
end 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

95 
 concls => (map mk_branch concls, cases) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

96 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

97 
fun mk_case premise = 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

98 
let 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

99 
val (ctxt', qs, prems, _ $ Plhs) = dest_hhf ctxt premise 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

100 
val (P, lhs) = strip_comb Plhs 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

101 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

102 
fun bidx Q = find_index (fn SchemeBranch {P=P',...} => Q aconv P') branches 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

103 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

104 
fun mk_rcinfo pr = 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

105 
let 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

106 
val (ctxt'', Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

107 
val (P', rcs) = strip_comb Phyp 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

108 
in 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

109 
(bidx P', Gvs, Gas, rcs) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

110 
end 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

111 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

112 
fun is_pred v = exists (fn SchemeBranch {P,...} => v aconv P) branches 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

113 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

114 
val (gs, rcprs) = 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

115 
take_prefix (not o Term.exists_subterm is_pred) prems 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

116 
in 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

117 
SchemeCase {bidx=bidx P, qs=qs, oqnames=map fst qs(*FIXME*), gs=gs, lhs=lhs, rs=map mk_rcinfo rcprs} 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

118 
end 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

119 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

120 
fun PT_of (SchemeBranch { xs, ...}) = 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

121 
foldr1 HOLogic.mk_prodT (map snd xs) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

122 

32765  123 
val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches) 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

124 
in 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

125 
IndScheme {T=ST, cases=map mk_case cases', branches=branches } 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

126 
end 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

127 

27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

128 

25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

129 

27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

130 
fun mk_completeness ctxt (IndScheme {cases, branches, ...}) bidx = 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

131 
let 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

132 
val SchemeBranch { xs, ws, Cs, ... } = nth branches bidx 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

133 
val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

134 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

135 
val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases [] 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

136 
val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs)) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

137 
val Cs' = map (Pattern.rewrite_term (ProofContext.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

138 

27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

139 
fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) = 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

140 
HOLogic.mk_Trueprop Pbool 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

141 
> fold_rev (fn x_l => curry Logic.mk_implies (HOLogic.mk_Trueprop(HOLogic.mk_eq x_l))) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

142 
(xs' ~~ lhs) 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

143 
> fold_rev (curry Logic.mk_implies) gs 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

144 
> fold_rev mk_forall_rename (oqnames ~~ map Free qs) 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

145 
in 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

146 
HOLogic.mk_Trueprop Pbool 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

147 
> fold_rev (curry Logic.mk_implies o mk_case) relevant_cases 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

148 
> fold_rev (curry Logic.mk_implies) Cs' 
27330  149 
> fold_rev (Logic.all o Free) ws 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

150 
> fold_rev mk_forall_rename (map fst xs ~~ xs') 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

151 
> mk_forall_rename ("P", Pbool) 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

152 
end 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

153 

5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

154 
fun mk_wf ctxt R (IndScheme {T, ...}) = 
32603  155 
HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T > HOLogic.boolT) $ R) 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

156 

27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

157 
fun mk_ineqs R (IndScheme {T, cases, branches}) = 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

158 
let 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

159 
fun inject i ts = 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

160 
SumTree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

161 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

162 
val thesis = Free ("thesis", HOLogic.boolT) (* FIXME *) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

163 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

164 
fun mk_pres bdx args = 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

165 
let 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

166 
val SchemeBranch { xs, ws, Cs, ... } = nth branches bdx 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

167 
fun replace (x, v) t = betapply (lambda (Free x) t, v) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

168 
val Cs' = map (fold replace (xs ~~ args)) Cs 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

169 
val cse = 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

170 
HOLogic.mk_Trueprop thesis 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

171 
> fold_rev (curry Logic.mk_implies) Cs' 
27330  172 
> fold_rev (Logic.all o Free) ws 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

173 
in 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

174 
Logic.mk_implies (cse, HOLogic.mk_Trueprop thesis) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

175 
end 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

176 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

177 
fun f (SchemeCase {bidx, qs, oqnames, gs, lhs, rs, ...}) = 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

178 
let 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

179 
fun g (bidx', Gvs, Gas, rcarg) = 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

180 
let val export = 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

181 
fold_rev (curry Logic.mk_implies) Gas 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

182 
#> fold_rev (curry Logic.mk_implies) gs 
27330  183 
#> fold_rev (Logic.all o Free) Gvs 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

184 
#> fold_rev mk_forall_rename (oqnames ~~ map Free qs) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

185 
in 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

186 
(HOLogic.mk_mem (HOLogic.mk_prod (inject bidx' rcarg, inject bidx lhs), R) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

187 
> HOLogic.mk_Trueprop 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

188 
> export, 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

189 
mk_pres bidx' rcarg 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

190 
> export 
27330  191 
> Logic.all thesis) 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

192 
end 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

193 
in 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

194 
map g rs 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

195 
end 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

196 
in 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

197 
map f cases 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

198 
end 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

199 

5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

200 

27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

201 
fun mk_hol_imp a b = HOLogic.imp $ a $ b 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

202 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

203 
fun mk_ind_goal thy branches = 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

204 
let 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

205 
fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) = 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

206 
HOLogic.mk_Trueprop (list_comb (P, map Free xs)) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

207 
> fold_rev (curry Logic.mk_implies) Cs 
27330  208 
> fold_rev (Logic.all o Free) ws 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

209 
> term_conv thy ind_atomize 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

210 
> ObjectLogic.drop_judgment thy 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

211 
> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs)) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

212 
in 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

213 
SumTree.mk_sumcases HOLogic.boolT (map brnch branches) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

214 
end 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

215 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

216 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

217 
fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss (IndScheme {T, cases=scases, branches}) = 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

218 
let 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

219 
val n = length branches 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

220 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

221 
val scases_idx = map_index I scases 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

222 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

223 
fun inject i ts = 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

224 
SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

225 
val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

226 

26644  227 
val thy = ProofContext.theory_of ctxt 
228 
val cert = cterm_of thy 

25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

229 

27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

230 
val P_comp = mk_ind_goal thy branches 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

231 

25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

232 
(* Inductive Hypothesis: !!z. (z,x):R ==> P z *) 
27330  233 
val ihyp = Term.all T $ Abs ("z", T, 
234 
Logic.mk_implies 

235 
(HOLogic.mk_Trueprop ( 

25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

236 
Const ("op :", HOLogic.mk_prodT (T, T) > mk_relT T > HOLogic.boolT) 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

237 
$ (HOLogic.pair_const T T $ Bound 0 $ x) 
27330  238 
$ R), 
239 
HOLogic.mk_Trueprop (P_comp $ Bound 0))) 

25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

240 
> cert 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

241 

5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

242 
val aihyp = assume ihyp 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

243 

27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

244 
(* Rule for case splitting along the sum types *) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

245 
val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

246 
val pats = map_index (uncurry inject) xss 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

247 
val sum_split_rule = FundefDatatype.prove_completeness thy [x] (P_comp $ x) xss (map single pats) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

248 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

249 
fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) = 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

250 
let 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

251 
val fxs = map Free xs 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

252 
val branch_hyp = assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat)))) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

253 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

254 
val C_hyps = map (cert #> assume) Cs 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

255 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

256 
val (relevant_cases, ineqss') = filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx) (scases_idx ~~ ineqss) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

257 
> split_list 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

258 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

259 
fun prove_case (cidx, SchemeCase {qs, oqnames, gs, lhs, rs, ...}) ineq_press = 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

260 
let 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

261 
val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs) 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

262 

27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

263 
val cqs = map (cert o Free) qs 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

264 
val ags = map (assume o cert) gs 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

265 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

266 
val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

267 
val sih = full_simplify replace_x_ss aihyp 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

268 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

269 
fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) = 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

270 
let 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

271 
val cGas = map (assume o cert) Gas 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

272 
val cGvs = map (cert o Free) Gvs 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

273 
val import = fold forall_elim (cqs @ cGvs) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

274 
#> fold Thm.elim_implies (ags @ cGas) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

275 
val ipres = pres 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

276 
> forall_elim (cert (list_comb (P_of idx, rcargs))) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

277 
> import 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

278 
in 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

279 
sih > forall_elim (cert (inject idx rcargs)) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

280 
> Thm.elim_implies (import ineq) (* Psum rcargs *) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

281 
> Conv.fconv_rule sum_prod_conv 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

282 
> Conv.fconv_rule ind_rulify 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

283 
> (fn th => th COMP ipres) (* P rs *) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

284 
> fold_rev (implies_intr o cprop_of) cGas 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

285 
> fold_rev forall_intr cGvs 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

286 
end 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

287 

27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

288 
val P_recs = map2 mk_Prec rs ineq_press (* [P rec1, P rec2, ... ] *) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

289 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

290 
val step = HOLogic.mk_Trueprop (list_comb (P, lhs)) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

291 
> fold_rev (curry Logic.mk_implies o prop_of) P_recs 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

292 
> fold_rev (curry Logic.mk_implies) gs 
27330  293 
> fold_rev (Logic.all o Free) qs 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

294 
> cert 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

295 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

296 
val Plhs_to_Pxs_conv = 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

297 
foldl1 (uncurry Conv.combination_conv) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

298 
(Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

299 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

300 
val res = assume step 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

301 
> fold forall_elim cqs 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

302 
> fold Thm.elim_implies ags 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

303 
> fold Thm.elim_implies P_recs (* P lhs *) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

304 
> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

305 
> fold_rev (implies_intr o cprop_of) (ags @ case_hyps) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

306 
> fold_rev forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *) 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

307 
in 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

308 
(res, (cidx, step)) 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

309 
end 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

310 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

311 
val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss') 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

312 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

313 
val bstep = complete_thm 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

314 
> forall_elim (cert (list_comb (P, fxs))) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

315 
> fold (forall_elim o cert) (fxs @ map Free ws) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

316 
> fold Thm.elim_implies C_hyps (* FIXME: optimization using rotate_prems *) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

317 
> fold Thm.elim_implies cases (* P xs *) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

318 
> fold_rev (implies_intr o cprop_of) C_hyps 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

319 
> fold_rev (forall_intr o cert o Free) ws 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

320 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

321 
val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x)) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

322 
> Goal.init 
29183
f1648e009dc1
removed duplicate sum_case used only by function package;
krauss
parents:
27369
diff
changeset

323 
> (MetaSimplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases})) 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

324 
THEN CONVERSION ind_rulify 1) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

325 
> Seq.hd 
27369  326 
> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep) 
32197  327 
> Goal.finish ctxt 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

328 
> implies_intr (cprop_of branch_hyp) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

329 
> fold_rev (forall_intr o cert) fxs 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

330 
in 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

331 
(Pxs, steps) 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

332 
end 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

333 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

334 
val (branches, steps) = split_list (map_index prove_branch (branches ~~ (complete_thms ~~ pats))) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

335 
> apsnd flat 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

336 

27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

337 
val istep = sum_split_rule 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

338 
> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

339 
> implies_intr ihyp 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

340 
> forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *) 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

341 

5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

342 
val induct_rule = 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

343 
@{thm "wf_induct_rule"} 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

344 
> (curry op COMP) wf_thm 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

345 
> (curry op COMP) istep 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

346 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

347 
val steps_sorted = map snd (sort (int_ord o pairself fst) steps) 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

348 
in 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

349 
(steps_sorted, induct_rule) 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

350 
end 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

351 

27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

352 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

353 
fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts = (ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

354 
(SUBGOAL (fn (t, i) => 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

355 
let 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

356 
val (ctxt', _, cases, concl) = dest_hhf ctxt t 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

357 
val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

358 
(* val _ = Output.tracing (makestring scheme)*) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

359 
val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt' 
26644  360 
val R = Free (Rn, mk_relT ST) 
361 
val x = Free (xn, ST) 

27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

362 
val cert = cterm_of (ProofContext.theory_of ctxt) 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

363 

5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

364 
val ineqss = mk_ineqs R scheme 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

365 
> map (map (pairself (assume o cert))) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

366 
val complete = map (mk_completeness ctxt scheme #> cert #> assume) (0 upto (length branches  1)) 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

367 
val wf_thm = mk_wf ctxt R scheme > cert > assume 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

368 

27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

369 
val (descent, pres) = split_list (flat ineqss) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

370 
val newgoals = complete @ pres @ wf_thm :: descent 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

371 

27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

372 
val (steps, indthm) = mk_induct_rule ctxt'' R x complete wf_thm ineqss scheme 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

373 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

374 
fun project (i, SchemeBranch {xs, ...}) = 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

375 
let 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

376 
val inst = cert (SumTree.mk_inj ST (length branches) (i + 1) (foldr1 HOLogic.mk_prod (map Free xs))) 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

377 
in 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

378 
indthm > Drule.instantiate' [] [SOME inst] 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

379 
> simplify SumTree.sumcase_split_ss 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

380 
> Conv.fconv_rule ind_rulify 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

381 
(* > (fn thm => (Output.tracing (makestring thm); thm))*) 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

382 
end 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

383 

27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

384 
val res = Conjunction.intr_balanced (map_index project branches) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

385 
> fold_rev implies_intr (map cprop_of newgoals @ steps) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

386 
> (fn thm => Thm.generalize ([], [Rn]) (Thm.maxidx_of thm + 1) thm) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

387 

ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

388 
val nbranches = length branches 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

389 
val npres = length pres 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

390 
in 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

391 
Thm.compose_no_flatten false (res, length newgoals) i 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

392 
THEN term_tac (i + nbranches + npres) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

393 
THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres  1) downto (i + nbranches)))) 
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26653
diff
changeset

394 
THEN (EVERY (map (TRY o comp_tac) ((i + nbranches  1) downto i))) 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

395 
end)) 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

396 

5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

397 

30493
b8570ea1ce25
provide regular ML interfaces for Isar source language elements;
wenzelm
parents:
29183
diff
changeset

398 
fun induct_scheme_tac ctxt = 
b8570ea1ce25
provide regular ML interfaces for Isar source language elements;
wenzelm
parents:
29183
diff
changeset

399 
mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt; 
b8570ea1ce25
provide regular ML interfaces for Isar source language elements;
wenzelm
parents:
29183
diff
changeset

400 

30515  401 
val setup = 
402 
Method.setup @{binding induct_scheme} (Scan.succeed (RAW_METHOD o induct_scheme_tac)) 

403 
"proves an induction principle" 

25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

404 

5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
diff
changeset

405 
end 