author  wenzelm 
Mon, 01 Aug 2005 19:20:32 +0200  
changeset 16978  e35b518bffc9 
parent 16935  4d7f19d340e8 
child 17227  398a7353ca69 
permissions  rwrr 
16978  1 
(* ================================= *) 
15150
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 
*) 
16978  7 
(* ================================= *) 
15150
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 

16978  10 
A structure that defines a tactic to program case splits. 
15150
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 : 
16978  13 
string * typ > int > thm > thm Seq.seq 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

14 

16978  15 
casesplit_name : 
16 
string > int > thm > thm Seq.seq 

15150
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 
16978  19 
type to be split. 
15150
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 
16978  22 
conjecture into a list subtheorems: 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

23 

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

25 
*) 
16978  26 
(* ================================= *) 
15150
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 
16978  31 
val dest_Trueprop : term > term 
32 
val mk_Trueprop : term > term 

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

33 

16978  34 
val localize : thm list 
35 
val local_impI : thm 

36 
val atomize : thm list 

37 
val rulify1 : thm list 

38 
val rulify2 : thm list 

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

39 

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

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

41 

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

42 
(* for HOL *) 
16978  43 
structure CaseSplitData_HOL : CASE_SPLIT_DATA = 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

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

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

46 
val mk_Trueprop = HOLogic.mk_Trueprop; 
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

47 

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

48 
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

49 
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

50 
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

51 
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

52 
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

53 

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

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

55 

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

56 

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

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

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

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

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

61 

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

62 
(* getting a case split thm from the induction thm *) 
16978  63 
val case_thm_of_ty : theory > typ > thm 
64 
val cases_thm_of_induct_thm : thm > thm 

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

65 

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

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

67 
val casesplit_free : 
16978  68 
string * typ > int > thm > thm Seq.seq 
69 
val casesplit_name : string > int > thm > thm Seq.seq 

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

70 

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

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

72 
val find_term_split : 
16978  73 
term * term > (string * typ) option 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

74 
val find_thm_split : 
16978  75 
thm > int > thm > (string * typ) option 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

76 
val find_thms_split : 
16978  77 
thm list > int > thm > (string * typ) option 
15150
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 
(* try to recursively split conjectured thm to given list of thms *) 
16978  80 
val splitto : thm list > thm > thm 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

81 

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

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

83 
val derive_init_eqs : 
16978  84 
theory > 
85 
(thm * int) list > term list > (thm * int) list 

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

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

87 

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

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

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

90 

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

91 
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

92 
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

93 

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

95 
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

96 
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

97 
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

98 
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

99 
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

100 
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

101 
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

102 
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

103 
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

104 
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

105 
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

106 
*) 
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 

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

108 
(* betaeta contract the theorem *) 
16978  109 
fun beta_eta_contract thm = 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

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

111 
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

112 
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

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

114 

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

115 
(* make a casethm from an induction thm *) 
16978  116 
val cases_thm_of_induct_thm = 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

117 
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

118 

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

119 
(* get the case_thm (my version) from a type *) 
16978  120 
fun case_thm_of_ty sgn ty = 
121 
let 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15798
diff
changeset

122 
val dtypestab = DatatypePackage.get_datatypes sgn; 
16978  123 
val ty_str = case ty of 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

124 
Type(ty_str, _) => ty_str 
16978  125 
 TFree(s,_) => raise ERROR_MESSAGE 
126 
("Free type: " ^ s) 

127 
 TVar((s,i),_) => raise ERROR_MESSAGE 

128 
("Free variable: " ^ s) 

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

129 
val dt = case (Symtab.lookup (dtypestab,ty_str)) 
15531  130 
of SOME dt => dt 
131 
 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

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

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

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

135 

16978  136 
(* 
137 
val ty = (snd o hd o map Term.dest_Free o Term.term_frees) t; 

15150
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 

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

142 
(* does a case split on the given variable *) 
16978  143 
fun mk_casesplit_goal_thm sgn (vstr,ty) gt = 
144 
let 

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

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

146 
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

147 

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

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

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

150 
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

151 

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

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

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

154 

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

155 
val casethm_vars = rev (Term.term_vars (Thm.concl_of case_thm)); 
16978  156 

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

157 
val casethm_tvars = Term.term_tvars (Thm.concl_of case_thm); 
16978  158 
val (Pv, Dv, type_insts) = 
159 
case (Thm.concl_of case_thm) of 

160 
(_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) => 

161 
(Pv, Dv, 

16935  162 
Sign.typ_match sgn (Dty, ty) Vartab.empty) 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

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

164 
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

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

166 
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

167 
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

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

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

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

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

174 

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

175 

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

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

177 
(* does a case split on the given variable (Free fv) *) 
16978  178 
fun casesplit_free fv i th = 
179 
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

180 
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

181 
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

182 
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

183 
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

184 

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

186 
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

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

189 
val rulified_split_goal_th = rulify_goals split_goal_th; 
16978  190 
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

191 
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

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

193 

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 

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

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

196 
(* does a case split on the given variable *) 
16978  197 
fun casesplit_name vstr i th = 
198 
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

199 
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

200 
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

201 
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

202 

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

203 
val freets = Term.term_frees gt; 
16978  204 
fun getter x = 
205 
let val (n,ty) = Term.dest_Free x in 

206 
(if vstr = n orelse vstr = Syntax.dest_skolem n 

15531  207 
then SOME (n,ty) else NONE ) 
15570  208 
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

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

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

213 
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

214 

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

215 
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

216 
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

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

219 

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

220 
val rulified_split_goal_th = rulify_goals split_goal_th; 
16978  221 
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

222 
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

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

224 

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

225 

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

227 
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

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

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

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

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

232 

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

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

234 

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

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

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

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

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

239 

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

240 

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

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

242 
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

243 

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

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

245 
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

246 
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

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

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

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

16978  252 
 find_term_split (a $ b, a2 $ b2) = 
253 
(case find_term_split (a, a2) of 

254 
NONE => find_term_split (b,b2) 

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

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

257 
find_term_split (t1, t2) 
16978  258 
 find_term_split (Const (x,ty), Const(x2,ty2)) = 
15531  259 
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

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

261 
"Terms are not identical upto a free varaible! (Consts)" 
16978  262 
 find_term_split (Bound i, Bound j) = 
15531  263 
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

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

265 
"Terms are not identical upto a free varaible! (Bound)" 
16978  266 
 find_term_split (a, b) = 
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! (Other)"; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

269 

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

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

271 
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

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

273 
fun find_thm_split splitth i genth = 
16978  274 
find_term_split (Logic.get_goal (Thm.prop_of genth) i, 
15531  275 
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

276 

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

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

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

279 
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

280 

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

281 

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

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

283 
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

284 
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

285 
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

286 
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

287 
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

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

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

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

291 
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

292 
having to (re)search for variables to split. *) 
16978  293 
fun splitto splitths genth = 
294 
let 

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

295 
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

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

297 

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

299 
more flexible with discrim net. *) 
16978  300 
fun solve_by_splitth th split = 
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

301 
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

302 

16978  303 
fun split th = 
304 
(case find_thms_split splitths 1 th of 

305 
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

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

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

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

309 
raise ERROR_MESSAGE "splitto: cannot find variable to split on") 
16978  310 
 SOME v => 
311 
let 

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

313 
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

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

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

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

318 

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

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

321 
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

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

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

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

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

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

328 

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

329 

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

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

331 
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

332 
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

333 
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

334 
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

335 
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

336 

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

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

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

339 
local 
16978  340 
fun get_related_thms i = 
15570  341 
List.mapPartial ((fn (r,x) => if x = i then SOME r else NONE)); 
16978  342 

343 
fun solve_eq (th, [], i) = 

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

344 
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

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

346 
 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

347 
in 
16978  348 
fun derive_init_eqs sgn rules eqs = 
349 
let 

350 
val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o Data.mk_Trueprop) 

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

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

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

353 
(rev o map solve_eq) 
16978  354 
(Library.foldln 
355 
(fn (e,i) => 

356 
(curry (op ::)) (e, (get_related_thms (i  1) rules), i  1)) 

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

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

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

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

361 
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

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

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

365 
end; 
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 
structure CaseSplit = CaseSplitFUN(CaseSplitData_HOL); 