author  paulson 
Fri, 20 Aug 2004 12:20:09 +0200  
changeset 15150  c7af682b9ee5 
child 15250  217bececa2bd 
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 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

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

35 

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

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

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

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

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

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

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

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

43 

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

44 

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

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

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

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

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

49 

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

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

51 
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

52 
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

53 

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

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

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

56 
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

57 
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

58 

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

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

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

61 
Term.term * Term.term > (string * Term.typ) Library.option 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

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

63 
Thm.thm > int > Thm.thm > (string * Term.typ) Library.option 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

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

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

66 

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

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

68 
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

69 

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

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

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

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

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

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

75 

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

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

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

78 

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

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

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

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

82 
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

83 
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

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

85 

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

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

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

88 
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

89 

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

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

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

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

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

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

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

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

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

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

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

100 
val dt = case (Symtab.lookup (dtypestab,ty_str)) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

101 
of Some dt => dt 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

102 
 None => raise ERROR_MESSAGE ("Not a Datatype: " ^ ty_str) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

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

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

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

106 

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

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

108 
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

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

110 

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

111 

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

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

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

114 
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

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

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

117 
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

118 

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

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

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

121 
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

122 

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

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

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

125 

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

126 
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

127 

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

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

129 
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

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

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

132 
(_ $ ((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

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

134 
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

135 
 _ => 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

136 
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

137 
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

138 
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

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

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

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

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

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

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

145 

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

146 

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

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

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

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

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

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

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

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

154 
Tactic.rtac (mk_casesplit_goal_thm sgn fv gt) i th 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

155 
end; 
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 
(* 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

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

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

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

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

162 
val freets = Term.term_frees gt; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

163 
fun getter x = let val (n,ty) = Term.dest_Free x in 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

164 
if vstr = n then Some (n,ty) else None end; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

165 
val (n,ty) = case Library.get_first getter freets 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

166 
of Some (n, ty) => (n, ty) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

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

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

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

170 
Tactic.rtac (mk_casesplit_goal_thm sgn (n,ty) gt) i th 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

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

172 

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

173 

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

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

175 
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

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

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

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

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

180 

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

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

182 

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

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

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

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

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

187 

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

188 

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

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

190 
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

191 

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

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

193 
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

194 
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

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

196 
fun find_term_split (Free v, _ $ _) = Some v 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

197 
 find_term_split (Free v, Const _) = Some v 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

198 
 find_term_split (Free v, Abs _) = Some v (* do we really want this case? *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

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

200 
(case find_term_split (a, a2) of 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

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

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

203 
 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

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

205 
 find_term_split (Const (x,ty), Const(x2,ty2)) = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

206 
if x = x2 then None else (* keep searching *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

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

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

209 
 find_term_split (Bound i, Bound j) = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

210 
if i = j then None else (* keep searching *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

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

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

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

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

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

216 

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

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

218 
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

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

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

221 
find_term_split (Logic.get_goal (Thm.prop_of genth) i, 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

222 
Thm.concl_of splitth) handle find_split_exp _ => None; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

223 

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

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

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

226 
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

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

230 
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

231 
can be casesplit, as needed. Otherwise fails. Note: We assume that 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

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

233 
matter which one we choose to look for the next split. Simply add 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

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

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

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

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

238 
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

239 
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

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

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

242 
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

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

244 

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

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

246 
more flexible with discrim net. *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

247 
fun solve_by_splitth th split = biresolution false [(false,split)] 1 th; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

248 

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

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

250 
(case find_thms_split splitths 1 th of 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

251 
None => raise ERROR_MESSAGE "splitto: cannot find variable to split on" 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

252 
 Some v => 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

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

254 
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

255 
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

256 
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

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

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

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

260 

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

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

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

263 
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

264 
(case Library.get_first (Seq.pull o solve_by_splitth th) splitths of 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

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

266 
 Some (solved_th, more) => solved_th) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

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

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

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

270 

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

273 
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

274 
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

275 
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

276 
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

277 
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

278 

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

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

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

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

282 
fun get_related_thms i = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

283 
mapfilter ((fn (r,x) => if x = i then Some r else None)); 
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 
fun solve_eq (th, [], i) = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

286 
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

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

288 
 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

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

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

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

292 
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

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

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

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

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

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

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

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

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

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

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

303 
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

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

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

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

308 

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

309 

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

310 
structure CaseSplit = CaseSplitFUN(CaseSplitData_HOL); 