author  huffman 
Thu, 14 Jul 2005 01:04:30 +0200  
changeset 16823  13f3768a6f14 
parent 16425  2427be27cc60 
child 16935  4d7f19d340e8 
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 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15798
diff
changeset

124 
val dtypestab = DatatypePackage.get_datatypes sgn; 
15150
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, 
15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset

165 
Type.typ_match tsig (Vartab.empty, (Dty, ty))) 
15150
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"); 
15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset

167 
val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T)) 
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset

168 
(Vartab.dest type_insts); 
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset

169 
val cPv = ctermify (Envir.subst_TVars type_insts Pv); 
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset

170 
val cDv = ctermify (Envir.subst_TVars type_insts Dv); 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

182 
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

183 
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

184 
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

185 
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

186 
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

187 

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

189 
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

190 

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

192 
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

193 
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

194 
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

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

196 

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

197 

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

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

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

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

201 
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

202 
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

203 
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

204 
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

205 

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

206 
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

207 
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

208 
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

209 
(if vstr = n orelse vstr = Syntax.dest_skolem n 
15531  210 
then SOME (n,ty) else NONE ) 
15570  211 
handle Fail _ => NONE (* dest_skolem *) 
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

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

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

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

216 
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

217 

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

219 
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

220 

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

222 

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

223 
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

224 
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

225 
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

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

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

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

230 
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

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

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

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

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

235 

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

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

237 

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

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

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

240 
val th' = casesplit_name "x" i th; 
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 

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

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

245 
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

246 

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

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

248 
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

249 
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

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

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

254 
 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

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

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

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

259 
 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

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

261 
 find_term_split (Const (x,ty), Const(x2,ty2)) = 
15531  262 
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

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

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

265 
 find_term_split (Bound i, Bound j) = 
15531  266 
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

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

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

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

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

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

272 

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

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

274 
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

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

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

277 
find_term_split (Logic.get_goal (Thm.prop_of genth) i, 
15531  278 
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

279 

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

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

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

282 
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

283 

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

284 

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

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

286 
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

287 
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

288 
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

289 
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

290 
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

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

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

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

294 
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

295 
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

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

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

298 
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

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

300 

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

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

302 
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

303 
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

304 
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

305 

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

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

307 
(case find_thms_split splitths 1 th of 
15531  308 
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

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

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

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

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

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

316 
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

317 
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

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

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

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

321 

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

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

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

324 
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

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

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

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

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

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

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

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

334 
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

335 
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

336 
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

337 
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

338 
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

339 

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

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

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

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

343 
fun get_related_thms i = 
15570  344 
List.mapPartial ((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

345 

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

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

347 
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

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

349 
 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

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

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

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

353 
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

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

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

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

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

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

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

360 
eqths []) 
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 
end; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

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

364 
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

365 
(map2 (op >) (ths, expfs)) 
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 

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

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

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

371 
structure CaseSplit = CaseSplitFUN(CaseSplitData_HOL); 