author  skalberg 
Sun, 13 Feb 2005 17:15:14 +0100  
changeset 15531  08c8dad8e399 
parent 15252  d4f1b11c336b 
child 15570  8d8c70b41bab 
permissions  rwrr 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

1 
(* ================================= *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

2 
(* Title: TFL/casesplit.ML 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

3 
Author: Lucas Dixon, University of Edinburgh 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

4 
lucas.dixon@ed.ac.uk 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

5 
Date: 17 Aug 2004 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

6 
*) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

7 
(* ================================= *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

8 
(* DESCRIPTION: 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

9 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

10 
A structure that defines a tactic to program case splits. 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

11 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

12 
casesplit_free : 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

13 
string * Term.type > int > Thm.thm > Thm.thm Seq.seq 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

14 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

15 
casesplit_name : 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

16 
string > int > Thm.thm > Thm.thm Seq.seq 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

17 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

18 
These use the induction theorem associated with the recursive data 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

19 
type to be split. 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

20 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

21 
The structure includes a function to try and recursively split a 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

22 
conjecture into a list subtheorems: 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

23 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

24 
splitto : Thm.thm list > Thm.thm > Thm.thm 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

25 
*) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

26 
(* ================================= *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

27 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

28 
(* logicspecific *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

29 
signature CASE_SPLIT_DATA = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

30 
sig 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

31 
val dest_Trueprop : Term.term > Term.term 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

32 
val mk_Trueprop : Term.term > Term.term 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

33 
val read_cterm : Sign.sg > string > Thm.cterm 
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

34 

217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

35 
val localize : Thm.thm list 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

36 
val local_impI : Thm.thm 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

37 
val atomize : Thm.thm list 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

38 
val rulify1 : Thm.thm list 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

39 
val rulify2 : Thm.thm list 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

40 

15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

41 
end; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

42 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

43 
(* for HOL *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

44 
structure CaseSplitData_HOL : CASE_SPLIT_DATA = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

45 
struct 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

46 
val dest_Trueprop = HOLogic.dest_Trueprop; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

47 
val mk_Trueprop = HOLogic.mk_Trueprop; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

48 
val read_cterm = HOLogic.read_cterm; 
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

49 

217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

50 
val localize = [Thm.symmetric (thm "induct_implies_def")]; 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

51 
val local_impI = thm "induct_impliesI"; 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

52 
val atomize = thms "induct_atomize"; 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

53 
val rulify1 = thms "induct_rulify1"; 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

54 
val rulify2 = thms "induct_rulify2"; 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

55 

15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

56 
end; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

57 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

58 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

59 
signature CASE_SPLIT = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

60 
sig 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

61 
(* failure to find a free to split on *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

62 
exception find_split_exp of string 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

63 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

64 
(* getting a case split thm from the induction thm *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

65 
val case_thm_of_ty : Sign.sg > Term.typ > Thm.thm 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

66 
val cases_thm_of_induct_thm : Thm.thm > Thm.thm 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

67 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

68 
(* case split tactics *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

69 
val casesplit_free : 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

70 
string * Term.typ > int > Thm.thm > Thm.thm Seq.seq 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

71 
val casesplit_name : string > int > Thm.thm > Thm.thm Seq.seq 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

72 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

73 
(* finding a free var to split *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

74 
val find_term_split : 
15531  75 
Term.term * Term.term > (string * Term.typ) option 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

76 
val find_thm_split : 
15531  77 
Thm.thm > int > Thm.thm > (string * Term.typ) option 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

78 
val find_thms_split : 
15531  79 
Thm.thm list > int > Thm.thm > (string * Term.typ) option 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

80 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

81 
(* try to recursively split conjectured thm to given list of thms *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

82 
val splitto : Thm.thm list > Thm.thm > Thm.thm 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

83 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

84 
(* for use with the recdef package *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

85 
val derive_init_eqs : 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

86 
Sign.sg > 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

87 
(Thm.thm * int) list > Term.term list > (Thm.thm * int) list 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

88 
end; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

89 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

90 
functor CaseSplitFUN(Data : CASE_SPLIT_DATA) = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

91 
struct 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

92 

15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

93 
val rulify_goals = Tactic.rewrite_goals_rule Data.rulify1; 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

94 
val atomize_goals = Tactic.rewrite_goals_rule Data.atomize; 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

95 

217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

96 
(* 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

97 
val localize = Tactic.norm_hhf_rule o Tactic.simplify false Data.localize; 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

98 
fun atomize_term sg = 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

99 
ObjectLogic.drop_judgment sg o MetaSimplifier.rewrite_term sg Data.atomize []; 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

100 
val rulify_tac = Tactic.rewrite_goal_tac Data.rulify1; 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

101 
val atomize_tac = Tactic.rewrite_goal_tac Data.atomize; 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

102 
Tactic.simplify_goal 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

103 
val rulify_tac = 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

104 
Tactic.rewrite_goal_tac Data.rulify1 THEN' 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

105 
Tactic.rewrite_goal_tac Data.rulify2 THEN' 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

106 
Tactic.norm_hhf_tac; 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

107 
val atomize = Tactic.norm_hhf_rule o Tactic.simplify true Data.atomize; 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

108 
*) 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

109 

15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

110 
(* betaeta contract the theorem *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

111 
fun beta_eta_contract thm = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

112 
let 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

113 
val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

114 
val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

115 
in thm3 end; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

116 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

117 
(* make a casethm from an induction thm *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

118 
val cases_thm_of_induct_thm = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

119 
Seq.hd o (ALLGOALS (fn i => REPEAT (etac Drule.thin_rl i))); 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

120 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

121 
(* get the case_thm (my version) from a type *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

122 
fun case_thm_of_ty sgn ty = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

123 
let 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

124 
val dtypestab = DatatypePackage.get_datatypes_sg sgn; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

125 
val ty_str = case ty of 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

126 
Type(ty_str, _) => ty_str 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

127 
 TFree(s,_) => raise ERROR_MESSAGE 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

128 
("Free type: " ^ s) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

129 
 TVar((s,i),_) => raise ERROR_MESSAGE 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

130 
("Free variable: " ^ s) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

131 
val dt = case (Symtab.lookup (dtypestab,ty_str)) 
15531  132 
of SOME dt => dt 
133 
 NONE => raise ERROR_MESSAGE ("Not a Datatype: " ^ ty_str) 

15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

134 
in 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

135 
cases_thm_of_induct_thm (#induction dt) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

136 
end; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

137 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

138 
(* 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

139 
val ty = (snd o hd o map Term.dest_Free o Term.term_frees) t; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

140 
*) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

141 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

142 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

143 
(* for use when there are no prems to the subgoal *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

144 
(* does a case split on the given variable *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

145 
fun mk_casesplit_goal_thm sgn (vstr,ty) gt = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

146 
let 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

147 
val x = Free(vstr,ty) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

148 
val abst = Abs(vstr, ty, Term.abstract_over (x, gt)); 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

149 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

150 
val ctermify = Thm.cterm_of sgn; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

151 
val ctypify = Thm.ctyp_of sgn; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

152 
val case_thm = case_thm_of_ty sgn ty; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

153 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

154 
val abs_ct = ctermify abst; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

155 
val free_ct = ctermify x; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

156 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

157 
val casethm_vars = rev (Term.term_vars (Thm.concl_of case_thm)); 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

158 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

159 
val tsig = Sign.tsig_of sgn; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

160 
val casethm_tvars = Term.term_tvars (Thm.concl_of case_thm); 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

161 
val (Pv, Dv, type_insts) = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

162 
case (Thm.concl_of case_thm) of 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

163 
(_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) => 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

164 
(Pv, Dv, 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

165 
Vartab.dest (Type.typ_match tsig (Vartab.empty, (Dty, ty)))) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

166 
 _ => raise ERROR_MESSAGE ("not a valid case thm"); 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

167 
val type_cinsts = map (apsnd ctypify) type_insts; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

168 
val cPv = ctermify (Sign.inst_term_tvars sgn type_insts Pv); 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

169 
val cDv = ctermify (Sign.inst_term_tvars sgn type_insts Dv); 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

170 
in 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

171 
(beta_eta_contract 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

172 
(case_thm 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

173 
> Thm.instantiate (type_cinsts, []) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

174 
> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)]))) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

175 
end; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

176 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

177 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

178 
(* for use when there are no prems to the subgoal *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

179 
(* does a case split on the given variable (Free fv) *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

180 
fun casesplit_free fv i th = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

181 
let 
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

182 
val (subgoalth, exp) = IsaND.fix_alls i th; 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

183 
val subgoalth' = atomize_goals subgoalth; 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

184 
val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1); 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

185 
val sgn = Thm.sign_of_thm th; 
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

186 

217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

187 
val splitter_thm = mk_casesplit_goal_thm sgn fv gt; 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

188 
val nsplits = Thm.nprems_of splitter_thm; 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

189 

217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

190 
val split_goal_th = splitter_thm RS subgoalth'; 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

191 
val rulified_split_goal_th = rulify_goals split_goal_th; 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

192 
in 
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

193 
IsaND.export_back exp rulified_split_goal_th 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

194 
end; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

195 

15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

196 

15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

197 
(* for use when there are no prems to the subgoal *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

198 
(* does a case split on the given variable *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

199 
fun casesplit_name vstr i th = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

200 
let 
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

201 
val (subgoalth, exp) = IsaND.fix_alls i th; 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

202 
val subgoalth' = atomize_goals subgoalth; 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

203 
val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1); 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

204 

15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

205 
val freets = Term.term_frees gt; 
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

206 
fun getter x = 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

207 
let val (n,ty) = Term.dest_Free x in 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

208 
(if vstr = n orelse vstr = Syntax.dest_skolem n 
15531  209 
then SOME (n,ty) else NONE ) 
210 
handle LIST _ => NONE 

15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

211 
end; 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

212 
val (n,ty) = case Library.get_first getter freets 
15531  213 
of SOME (n, ty) => (n, ty) 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

214 
 _ => raise ERROR_MESSAGE ("no such variable " ^ vstr); 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

215 
val sgn = Thm.sign_of_thm th; 
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

216 

217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

217 
val splitter_thm = mk_casesplit_goal_thm sgn (n,ty) gt; 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

218 
val nsplits = Thm.nprems_of splitter_thm; 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

219 

217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

220 
val split_goal_th = splitter_thm RS subgoalth'; 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

221 

217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

222 
val rulified_split_goal_th = rulify_goals split_goal_th; 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

223 
in 
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

224 
IsaND.export_back exp rulified_split_goal_th 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

225 
end; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

226 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

227 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

228 
(* small example: 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

229 
Goal "P (x :: nat) & (C y > Q (y :: nat))"; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

230 
by (rtac (thm "conjI") 1); 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

231 
val th = topthm(); 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

232 
val i = 2; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

233 
val vstr = "y"; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

234 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

235 
by (casesplit_name "y" 2); 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

236 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

237 
val th = topthm(); 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

238 
val i = 1; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

239 
val th' = casesplit_name "x" i th; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

240 
*) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

241 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

242 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

243 
(* the find_XXX_split functions are simply doing a lightwieght (I 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

244 
think) term matching equivalent to find where to do the next split *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

245 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

246 
(* assuming two twems are identical except for a free in one at a 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

247 
subterm, or constant in another, ie assume that one term is a plit of 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

248 
another, then gives back the free variable that has been split. *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

249 
exception find_split_exp of string 
15531  250 
fun find_term_split (Free v, _ $ _) = SOME v 
251 
 find_term_split (Free v, Const _) = SOME v 

252 
 find_term_split (Free v, Abs _) = SOME v (* do we really want this case? *) 

253 
 find_term_split (Free v, Var _) = NONE (* keep searching *) 

15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

254 
 find_term_split (a $ b, a2 $ b2) = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

255 
(case find_term_split (a, a2) of 
15531  256 
NONE => find_term_split (b,b2) 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

257 
 vopt => vopt) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

258 
 find_term_split (Abs(_,ty,t1), Abs(_,ty2,t2)) = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

259 
find_term_split (t1, t2) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

260 
 find_term_split (Const (x,ty), Const(x2,ty2)) = 
15531  261 
if x = x2 then NONE else (* keep searching *) 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

262 
raise find_split_exp (* stop now *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

263 
"Terms are not identical upto a free varaible! (Consts)" 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

264 
 find_term_split (Bound i, Bound j) = 
15531  265 
if i = j then NONE else (* keep searching *) 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

266 
raise find_split_exp (* stop now *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

267 
"Terms are not identical upto a free varaible! (Bound)" 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

268 
 find_term_split (a, b) = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

269 
raise find_split_exp (* stop now *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

270 
"Terms are not identical upto a free varaible! (Other)"; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

271 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

272 
(* assume that "splitth" is a case split form of subgoal i of "genth", 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

273 
then look for a free variable to split, breaking the subgoal closer to 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

274 
splitth. *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

275 
fun find_thm_split splitth i genth = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

276 
find_term_split (Logic.get_goal (Thm.prop_of genth) i, 
15531  277 
Thm.concl_of splitth) handle find_split_exp _ => NONE; 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

278 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

279 
(* as above but searches "splitths" for a theorem that suggest a case split *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

280 
fun find_thms_split splitths i genth = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

281 
Library.get_first (fn sth => find_thm_split sth i genth) splitths; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

282 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

283 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

284 
(* split the subgoal i of "genth" until we get to a member of 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

285 
splitths. Assumes that genth will be a general form of splitths, that 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

286 
can be casesplit, as needed. Otherwise fails. Note: We assume that 
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

287 
all of "splitths" are split to the same level, and thus it doesn't 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

288 
matter which one we choose to look for the next split. Simply add 
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

289 
search on splitthms and split variable, to change this. *) 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

290 
(* Note: possible efficiency measure: when a case theorem is no longer 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

291 
useful, drop it? *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

292 
(* Note: This should not be a separate tactic but integrated into the 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

293 
case split done during recdef's case analysis, this would avoid us 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

294 
having to (re)search for variables to split. *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

295 
fun splitto splitths genth = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

296 
let 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

297 
val _ = assert (not (null splitths)) "splitto: no given splitths"; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

298 
val sgn = Thm.sign_of_thm genth; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

299 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

300 
(* check if we are a member of splitths  FIXME: quicker and 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

301 
more flexible with discrim net. *) 
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

302 
fun solve_by_splitth th split = 
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

303 
Thm.biresolution false [(false,split)] 1 th; 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

304 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

305 
fun split th = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

306 
(case find_thms_split splitths 1 th of 
15531  307 
NONE => 
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset

308 
(writeln "th:"; 
15252
d4f1b11c336b
Replaced PolyML specific print function by Display.print_thm(s)
berghofe
parents:
15250
diff
changeset

309 
Display.print_thm th; writeln "split ths:"; 
d4f1b11c336b
Replaced PolyML specific print function by Display.print_thm(s)
berghofe
parents:
15250
diff
changeset

310 
Display.print_thms splitths; writeln "\n"; 
d4f1b11c336b
Replaced PolyML specific print function by Display.print_thm(s)
berghofe
parents:
15250
diff
changeset

311 
raise ERROR_MESSAGE "splitto: cannot find variable to split on") 
15531  312 
 SOME v => 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

313 
let 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

314 
val gt = Data.dest_Trueprop (nth_elem(0, Thm.prems_of th)); 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

315 
val split_thm = mk_casesplit_goal_thm sgn v gt; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

316 
val (subthms, expf) = IsaND.fixed_subgoal_thms split_thm; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

317 
in 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

318 
expf (map recsplitf subthms) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

319 
end) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

320 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

321 
and recsplitf th = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

322 
(* note: multiple unifiers! we only take the first element, 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

323 
probably fine  there is probably only one anyway. *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

324 
(case Library.get_first (Seq.pull o solve_by_splitth th) splitths of 
15531  325 
NONE => split th 
326 
 SOME (solved_th, more) => solved_th) 

15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

327 
in 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

328 
recsplitf genth 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

329 
end; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

330 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

331 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

332 
(* Note: We dont do this if wf conditions fail to be solved, as each 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

333 
case may have a different wf condition  we could group the conditions 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

334 
togeather and say that they must be true to solve the general case, 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

335 
but that would hide from the user which subcase they were related 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

336 
to. Probably this is not important, and it would work fine, but I 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

337 
prefer leaving more fine grain control to the user. *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

338 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

339 
(* derive eqs, assuming strict, ie the rules have no assumptions = all 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

340 
the wellfoundness conditions have been solved. *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

341 
local 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

342 
fun get_related_thms i = 
15531  343 
mapfilter ((fn (r,x) => if x = i then SOME r else NONE)); 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

344 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

345 
fun solve_eq (th, [], i) = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

346 
raise ERROR_MESSAGE "derive_init_eqs: missing rules" 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

347 
 solve_eq (th, [a], i) = (a, i) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

348 
 solve_eq (th, splitths as (_ :: _), i) = (splitto splitths th,i); 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

349 
in 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

350 
fun derive_init_eqs sgn rules eqs = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

351 
let 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

352 
val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o Data.mk_Trueprop) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

353 
eqs 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

354 
in 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

355 
(rev o map solve_eq) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

356 
(Library.foldln 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

357 
(fn (e,i) => 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

358 
(curry (op ::)) (e, (get_related_thms (i  1) rules), i  1)) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

359 
eqths []) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

360 
end; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

361 
end; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

362 
(* 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

363 
val (rs_hwfc, unhidefs) = Library.split_list (map hide_prems rules) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

364 
(map2 (op >) (ths, expfs)) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

365 
*) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

366 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

367 
end; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

368 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

369 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

370 
structure CaseSplit = CaseSplitFUN(CaseSplitData_HOL); 