author  krauss 
Mon, 23 Oct 2006 17:46:11 +0200  
changeset 21100  cda93bbf35db 
parent 20081  c9da24b69fda 
child 21708  45e7491bea47 
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 

33 
val atomize : thm list 

18479  34 
val rulify : thm list 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

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

36 

16978  37 
structure CaseSplitData_HOL : CASE_SPLIT_DATA = 
15150
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; 
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

41 

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

42 
val atomize = thms "induct_atomize"; 
18479  43 
val rulify = thms "induct_rulify"; 
44 
val rulify_fallback = thms "induct_rulify_fallback"; 

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

45 

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

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

47 

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

48 

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

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

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

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

52 
exception find_split_exp of string 
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 
(* getting a case split thm from the induction thm *) 
16978  55 
val case_thm_of_ty : theory > typ > thm 
56 
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

57 

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

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

59 
val casesplit_free : 
16978  60 
string * typ > int > thm > thm Seq.seq 
61 
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

62 

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

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

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

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

68 
val find_thms_split : 
16978  69 
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

70 

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

71 
(* try to recursively split conjectured thm to given list of thms *) 
16978  72 
val splitto : thm list > thm > thm 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

73 

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

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

75 
val derive_init_eqs : 
16978  76 
theory > 
77 
(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

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

79 

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

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

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

82 

18479  83 
val rulify_goals = Tactic.rewrite_goals_rule Data.rulify; 
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

84 
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

85 

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

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

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

89 
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

90 
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

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

92 

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

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

95 
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

96 

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

97 
(* get the case_thm (my version) from a type *) 
16978  98 
fun case_thm_of_ty sgn ty = 
99 
let 

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

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

102 
Type(ty_str, _) => ty_str 
18678  103 
 TFree(s,_) => error ("Free type: " ^ s) 
104 
 TVar((s,i),_) => error ("Free variable: " ^ s) 

17412  105 
val dt = case Symtab.lookup dtypestab ty_str 
15531  106 
of SOME dt => dt 
18678  107 
 NONE => error ("Not a Datatype: " ^ ty_str) 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

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

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

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

111 

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

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

115 

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

116 

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

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

118 
(* does a case split on the given variable *) 
16978  119 
fun mk_casesplit_goal_thm sgn (vstr,ty) gt = 
120 
let 

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

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

122 
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

123 

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

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

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

126 
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

127 

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

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

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

130 

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

131 
val casethm_vars = rev (Term.term_vars (Thm.concl_of case_thm)); 
16978  132 

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

133 
val casethm_tvars = Term.term_tvars (Thm.concl_of case_thm); 
16978  134 
val (Pv, Dv, type_insts) = 
135 
case (Thm.concl_of case_thm) of 

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

137 
(Pv, Dv, 

16935  138 
Sign.typ_match sgn (Dty, ty) Vartab.empty) 
18678  139 
 _ => error "not a valid case thm"; 
15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset

140 
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

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

142 
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

143 
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

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

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

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

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

150 

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

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

156 
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

157 
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

158 
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

159 
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

160 

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

161 
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

162 
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

163 

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

164 
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

165 
val rulified_split_goal_th = rulify_goals split_goal_th; 
16978  166 
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

167 
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

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

169 

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

170 

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

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

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

175 
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

176 
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

177 
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

178 

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

179 
val freets = Term.term_frees gt; 
16978  180 
fun getter x = 
181 
let val (n,ty) = Term.dest_Free x in 

20081  182 
(if vstr = n orelse vstr = Name.dest_skolem n 
15531  183 
then SOME (n,ty) else NONE ) 
15570  184 
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

185 
end; 
16978  186 
val (n,ty) = case Library.get_first getter freets 
15531  187 
of SOME (n, ty) => (n, ty) 
18678  188 
 _ => error ("no such variable " ^ vstr); 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset

189 
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

190 

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

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

192 
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

193 

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

195 

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

196 
val rulified_split_goal_th = rulify_goals split_goal_th; 
16978  197 
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

198 
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

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

200 

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

201 

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

203 
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

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

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

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

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

208 

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

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

210 

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

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

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

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

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

215 

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

218 
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

219 

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

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

221 
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

222 
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

223 
exception find_split_exp of string 
15531  224 
fun find_term_split (Free v, _ $ _) = SOME v 
225 
 find_term_split (Free v, Const _) = SOME v 

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

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

16978  228 
 find_term_split (a $ b, a2 $ b2) = 
229 
(case find_term_split (a, a2) of 

230 
NONE => find_term_split (b,b2) 

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

231 
 vopt => vopt) 
16978  232 
 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

233 
find_term_split (t1, t2) 
16978  234 
 find_term_split (Const (x,ty), Const(x2,ty2)) = 
15531  235 
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

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

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

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

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

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

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

245 

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

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

247 
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

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

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

252 

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

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

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

255 
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

256 

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

257 

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

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

259 
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

260 
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

261 
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

262 
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

263 
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

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

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

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

267 
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

268 
having to (re)search for variables to split. *) 
16978  269 
fun splitto splitths genth = 
270 
let 

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

271 
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

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

273 

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

275 
more flexible with discrim net. *) 
16978  276 
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

277 
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

278 

16978  279 
fun split th = 
280 
(case find_thms_split splitths 1 th of 

281 
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

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

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

284 
Display.print_thms splitths; writeln "\n"; 
18678  285 
error "splitto: cannot find variable to split on") 
16978  286 
 SOME v => 
287 
let 

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

289 
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

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

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

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

294 

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

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

297 
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

298 
(case Library.get_first (Seq.pull o solve_by_splitth th) splitths of 
15531  299 
NONE => split th 
300 
 SOME (solved_th, more) => solved_th) 

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

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

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

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

304 

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

305 

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

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

307 
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

308 
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

309 
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

310 
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

311 
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

312 

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

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

314 
the wellfoundness conditions have been solved. *) 
16978  315 
fun derive_init_eqs sgn rules eqs = 
18050  316 
let 
317 
fun get_related_thms i = 

318 
List.mapPartial ((fn (r, x) => if x = i then SOME r else NONE)); 

319 
fun add_eq (i, e) xs = 

320 
(e, (get_related_thms i rules), i) :: xs 

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

18678  322 
error "derive_init_eqs: missing rules" 
18050  323 
 solve_eq (th, [a], i) = (a, i) 
324 
 solve_eq (th, splitths as (_ :: _), i) = (splitto splitths th, i); 

325 
val eqths = 

326 
map (Thm.trivial o Thm.cterm_of sgn o Data.mk_Trueprop) eqs; 

327 
in 

328 
[] 

329 
> fold_index add_eq eqths 

330 
> map solve_eq 

331 
> rev 

332 
end; 

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

333 

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

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

335 

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