author  traytel 
Thu, 19 Sep 2013 17:38:03 +0200  
changeset 53736  82799e03fff7 
parent 53735  99331dac1e1c 
child 53743  87585d506db4 
permissions  rwrr 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

1 
(* Title: HOL/BNF/Tools/bnf_fp_rec_sugar.ML 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

2 
Author: Lorenz Panny, TU Muenchen 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

3 
Copyright 2013 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

4 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

5 
Recursor and corecursor sugar. 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

6 
*) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

7 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

8 
signature BNF_FP_REC_SUGAR = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

9 
sig 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

10 
val add_primrec_cmd: (binding * string option * mixfix) list > 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

11 
(Attrib.binding * string) list > local_theory > local_theory; 
53310  12 
val add_primcorec_cmd: bool > 
13 
(binding * string option * mixfix) list * (Attrib.binding * string) list > Proof.context > 

14 
Proof.state 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

15 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

16 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

17 
structure BNF_FP_Rec_Sugar : BNF_FP_REC_SUGAR = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

18 
struct 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

19 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

20 
open BNF_Util 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

21 
open BNF_FP_Util 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

22 
open BNF_FP_Rec_Sugar_Util 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

23 
open BNF_FP_Rec_Sugar_Tactics 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

24 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

25 
exception Primrec_Error of string * term list; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

26 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

27 
fun primrec_error str = raise Primrec_Error (str, []); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

28 
fun primrec_error_eqn str eqn = raise Primrec_Error (str, [eqn]); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

29 
fun primrec_error_eqns str eqns = raise Primrec_Error (str, eqns); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

30 

53358  31 
fun finds eq = fold_map (fn x => List.partition (curry eq x) #>> pair x); 
32 

53357  33 
val free_name = try (fn Free (v, _) => v); 
34 
val const_name = try (fn Const (v, _) => v); 

53358  35 
val undef_const = Const (@{const_name undefined}, dummyT); 
53357  36 

53358  37 
fun permute_args n t = list_comb (t, map Bound (0 :: (n downto 1))) 
53720  38 
> fold (K (Term.abs (Name.uu, dummyT))) (0 upto n); 
53401  39 
val abs_tuple = HOLogic.tupled_lambda o HOLogic.mk_tuple; 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

40 
fun drop_All t = subst_bounds (strip_qnt_vars @{const_name all} t > map Free > rev, 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

41 
strip_qnt_body @{const_name all} t) 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

42 
fun mk_not @{const True} = @{const False} 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

43 
 mk_not @{const False} = @{const True} 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

44 
 mk_not (@{const Not} $ t) = t 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

45 
 mk_not (@{const Trueprop} $ t) = @{const Trueprop} $ mk_not t 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

46 
 mk_not t = HOLogic.mk_not t 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

47 
val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True}; 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

48 
val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False}; 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

49 
fun invert_prems [t] = map mk_not (HOLogic.disjuncts t) 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

50 
 invert_prems ts = [mk_disjs (map mk_not ts)]; 
53720  51 
fun invert_prems_disj [t] = map mk_not (HOLogic.disjuncts t) 
52 
 invert_prems_disj ts = [mk_disjs (map (mk_conjs o map mk_not o HOLogic.disjuncts) ts)]; 

53 
fun abstract vs = 

54 
let fun a n (t $ u) = a n t $ a n u 

55 
 a n (Abs (v, T, b)) = Abs (v, T, a (n + 1) b) 

56 
 a n t = let val idx = find_index (equal t) vs in 

57 
if idx < 0 then t else Bound (n + idx) end 

58 
in a 0 end; 

53735  59 
fun mk_prod1 Ts (t, u) = HOLogic.pair_const (fastype_of1 (Ts, t)) (fastype_of1 (Ts, u)) $ t $ u; 
60 
fun mk_tuple1 Ts = the_default HOLogic.unit o try (foldr1 (mk_prod1 Ts)); 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

61 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

62 
val simp_attrs = @{attributes [simp]}; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

63 

53310  64 

65 
(* Primrec *) 

66 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

67 
type eqn_data = { 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

68 
fun_name: string, 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

69 
rec_type: typ, 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

70 
ctr: term, 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

71 
ctr_args: term list, 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

72 
left_args: term list, 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

73 
right_args: term list, 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

74 
res_type: typ, 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

75 
rhs_term: term, 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

76 
user_eqn: term 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

77 
}; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

78 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

79 
fun dissect_eqn lthy fun_names eqn' = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

80 
let 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

81 
val eqn = drop_All eqn' > HOLogic.dest_Trueprop 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

82 
handle TERM _ => 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

83 
primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn'; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

84 
val (lhs, rhs) = HOLogic.dest_eq eqn 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

85 
handle TERM _ => 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

86 
primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn'; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

87 
val (fun_name, args) = strip_comb lhs 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

88 
>> (fn x => if is_Free x then fst (dest_Free x) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

89 
else primrec_error_eqn "malformed function equation (does not start with free)" eqn); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

90 
val (left_args, rest) = take_prefix is_Free args; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

91 
val (nonfrees, right_args) = take_suffix is_Free rest; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

92 
val _ = length nonfrees = 1 orelse if length nonfrees = 0 then 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

93 
primrec_error_eqn "constructor pattern missing in lefthand side" eqn else 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

94 
primrec_error_eqn "more than one nonvariable argument in lefthand side" eqn; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

95 
val _ = member (op =) fun_names fun_name orelse 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

96 
primrec_error_eqn "malformed function equation (does not start with function name)" eqn 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

97 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

98 
val (ctr, ctr_args) = strip_comb (the_single nonfrees); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

99 
val _ = try (num_binder_types o fastype_of) ctr = SOME (length ctr_args) orelse 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

100 
primrec_error_eqn "partially applied constructor in pattern" eqn; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

101 
val _ = let val d = duplicates (op =) (left_args @ ctr_args @ right_args) in null d orelse 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

102 
primrec_error_eqn ("duplicate variable \"" ^ Syntax.string_of_term lthy (hd d) ^ 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

103 
"\" in lefthand side") eqn end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

104 
val _ = forall is_Free ctr_args orelse 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

105 
primrec_error_eqn "nonprimitive pattern in lefthand side" eqn; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

106 
val _ = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

107 
let val b = fold_aterms (fn x as Free (v, _) => 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

108 
if (not (member (op =) (left_args @ ctr_args @ right_args) x) andalso 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

109 
not (member (op =) fun_names v) andalso 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

110 
not (Variable.is_fixed lthy v)) then cons x else I  _ => I) rhs [] 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

111 
in 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

112 
null b orelse 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

113 
primrec_error_eqn ("extra variable(s) in righthand side: " ^ 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

114 
commas (map (Syntax.string_of_term lthy) b)) eqn 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

115 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

116 
in 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

117 
{fun_name = fun_name, 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

118 
rec_type = body_type (type_of ctr), 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

119 
ctr = ctr, 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

120 
ctr_args = ctr_args, 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

121 
left_args = left_args, 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

122 
right_args = right_args, 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

123 
res_type = map fastype_of (left_args @ right_args) > fastype_of rhs, 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

124 
rhs_term = rhs, 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

125 
user_eqn = eqn'} 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

126 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

127 

53401  128 
fun rewrite_map_arg get_ctr_pos rec_type res_type = 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

129 
let 
53357  130 
val pT = HOLogic.mk_prodT (rec_type, res_type); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

131 

53357  132 
val maybe_suc = Option.map (fn x => x + 1); 
133 
fun subst d (t as Bound d') = t > d = SOME d' ? curry (op $) (fst_const pT) 

134 
 subst d (Abs (v, T, b)) = Abs (v, if d = SOME ~1 then pT else T, subst (maybe_suc d) b) 

135 
 subst d t = 

53358  136 
let 
137 
val (u, vs) = strip_comb t; 

53401  138 
val ctr_pos = try (get_ctr_pos o the) (free_name u) > the_default ~1; 
53358  139 
in 
53401  140 
if ctr_pos >= 0 then 
53357  141 
if d = SOME ~1 andalso length vs = ctr_pos then 
142 
list_comb (permute_args ctr_pos (snd_const pT), vs) 

143 
else if length vs > ctr_pos andalso is_some d 

144 
andalso d = try (fn Bound n => n) (nth vs ctr_pos) then 

145 
list_comb (snd_const pT $ nth vs ctr_pos, map (subst d) (nth_drop ctr_pos vs)) 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

146 
else 
53357  147 
primrec_error_eqn ("recursive call not directly applied to constructor argument") t 
148 
else if d = SOME ~1 andalso const_name u = SOME @{const_name comp} then 

149 
list_comb (map_types (K dummyT) u, map2 subst [NONE, d] vs) 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

150 
else 
53357  151 
list_comb (u, map (subst (d > d = SOME ~1 ? K NONE)) vs) 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

152 
end 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

153 
in 
53357  154 
subst (SOME ~1) 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

155 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

156 

53401  157 
fun subst_rec_calls lthy get_ctr_pos has_call ctr_args direct_calls indirect_calls t = 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

158 
let 
53350  159 
fun subst bound_Ts (Abs (v, T, b)) = Abs (v, T, subst (T :: bound_Ts) b) 
53358  160 
 subst bound_Ts (t as g' $ y) = 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

161 
let 
53350  162 
val maybe_direct_y' = AList.lookup (op =) direct_calls y; 
163 
val maybe_indirect_y' = AList.lookup (op =) indirect_calls y; 

53358  164 
val (g, g_args) = strip_comb g'; 
53401  165 
val ctr_pos = try (get_ctr_pos o the) (free_name g) > the_default ~1; 
166 
val _ = ctr_pos < 0 orelse length g_args >= ctr_pos orelse 

53358  167 
primrec_error_eqn "too few arguments in recursive call" t; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

168 
in 
53358  169 
if not (member (op =) ctr_args y) then 
170 
pairself (subst bound_Ts) (g', y) > (op $) 

53401  171 
else if ctr_pos >= 0 then 
53358  172 
list_comb (the maybe_direct_y', g_args) 
53350  173 
else if is_some maybe_indirect_y' then 
53358  174 
(if has_call g' then t else y) 
175 
> massage_indirect_rec_call lthy has_call 

53401  176 
(rewrite_map_arg get_ctr_pos) bound_Ts y (the maybe_indirect_y') 
53358  177 
> (if has_call g' then I else curry (op $) g') 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

178 
else 
53350  179 
t 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

180 
end 
53350  181 
 subst _ t = t 
182 
in 

183 
subst [] t 

53358  184 
> tap (fn u => has_call u andalso (* FIXME detect this case earlier *) 
185 
primrec_error_eqn "recursive call not directly applied to constructor argument" t) 

53350  186 
end; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

187 

53358  188 
fun build_rec_arg lthy funs_data has_call ctr_spec maybe_eqn_data = 
189 
if is_none maybe_eqn_data then undef_const else 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

190 
let 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

191 
val eqn_data = the maybe_eqn_data; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

192 
val t = #rhs_term eqn_data; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

193 
val ctr_args = #ctr_args eqn_data; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

194 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

195 
val calls = #calls ctr_spec; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

196 
val n_args = fold (curry (op +) o (fn Direct_Rec _ => 2  _ => 1)) calls 0; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

197 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

198 
val no_calls' = tag_list 0 calls 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

199 
> map_filter (try (apsnd (fn No_Rec n => n  Direct_Rec (n, _) => n))); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

200 
val direct_calls' = tag_list 0 calls 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

201 
> map_filter (try (apsnd (fn Direct_Rec (_, n) => n))); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

202 
val indirect_calls' = tag_list 0 calls 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

203 
> map_filter (try (apsnd (fn Indirect_Rec n => n))); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

204 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

205 
fun make_direct_type T = dummyT; (* FIXME? *) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

206 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

207 
val rec_res_type_list = map (fn (x :: _) => (#rec_type x, #res_type x)) funs_data; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

208 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

209 
fun make_indirect_type (Type (Tname, Ts)) = Type (Tname, Ts > map (fn T => 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

210 
let val maybe_res_type = AList.lookup (op =) rec_res_type_list T in 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

211 
if is_some maybe_res_type 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

212 
then HOLogic.mk_prodT (T, the maybe_res_type) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

213 
else make_indirect_type T end)) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

214 
 make_indirect_type T = T; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

215 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

216 
val args = replicate n_args ("", dummyT) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

217 
> Term.rename_wrt_term t 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

218 
> map Free 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

219 
> fold (fn (ctr_arg_idx, arg_idx) => 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

220 
nth_map arg_idx (K (nth ctr_args ctr_arg_idx))) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

221 
no_calls' 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

222 
> fold (fn (ctr_arg_idx, arg_idx) => 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

223 
nth_map arg_idx (K (nth ctr_args ctr_arg_idx > map_types make_direct_type))) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

224 
direct_calls' 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

225 
> fold (fn (ctr_arg_idx, arg_idx) => 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

226 
nth_map arg_idx (K (nth ctr_args ctr_arg_idx > map_types make_indirect_type))) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

227 
indirect_calls'; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

228 

53401  229 
val fun_name_ctr_pos_list = 
230 
map (fn (x :: _) => (#fun_name x, length (#left_args x))) funs_data; 

231 
val get_ctr_pos = try (the o AList.lookup (op =) fun_name_ctr_pos_list) #> the_default ~1; 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

232 
val direct_calls = map (apfst (nth ctr_args) o apsnd (nth args)) direct_calls'; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

233 
val indirect_calls = map (apfst (nth ctr_args) o apsnd (nth args)) indirect_calls'; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

234 

53401  235 
val abstractions = args @ #left_args eqn_data @ #right_args eqn_data; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

236 
in 
53350  237 
t 
53401  238 
> subst_rec_calls lthy get_ctr_pos has_call ctr_args direct_calls indirect_calls 
239 
> fold_rev lambda abstractions 

53350  240 
end; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

241 

53358  242 
fun build_defs lthy bs mxs funs_data rec_specs has_call = 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

243 
let 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

244 
val n_funs = length funs_data; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

245 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

246 
val ctr_spec_eqn_data_list' = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

247 
(take n_funs rec_specs > map #ctr_specs) ~~ funs_data 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

248 
> maps (uncurry (finds (fn (x, y) => #ctr x = #ctr y)) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

249 
##> (fn x => null x orelse 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

250 
primrec_error_eqns "excess equations in definition" (map #rhs_term x)) #> fst); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

251 
val _ = ctr_spec_eqn_data_list' > map (fn (_, x) => length x <= 1 orelse 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

252 
primrec_error_eqns ("multiple equations for constructor") (map #user_eqn x)); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

253 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

254 
val ctr_spec_eqn_data_list = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

255 
ctr_spec_eqn_data_list' @ (drop n_funs rec_specs > maps #ctr_specs > map (rpair [])); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

256 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

257 
val recs = take n_funs rec_specs > map #recx; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

258 
val rec_args = ctr_spec_eqn_data_list 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

259 
> sort ((op <) o pairself (#offset o fst) > make_ord) 
53358  260 
> map (uncurry (build_rec_arg lthy funs_data has_call) o apsnd (try the_single)); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

261 
val ctr_poss = map (fn x => 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

262 
if length (distinct ((op =) o pairself (length o #left_args)) x) <> 1 then 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

263 
primrec_error ("inconstant constructor pattern position for function " ^ 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

264 
quote (#fun_name (hd x))) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

265 
else 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

266 
hd x > #left_args > length) funs_data; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

267 
in 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

268 
(recs, ctr_poss) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

269 
> map2 (fn recx => fn ctr_pos => list_comb (recx, rec_args) > permute_args ctr_pos) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

270 
> Syntax.check_terms lthy 
53352  271 
> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.map_name Thm.def_name b, []), t))) bs mxs 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

272 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

273 

53358  274 
fun find_rec_calls has_call eqn_data = 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

275 
let 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

276 
fun find (Abs (_, _, b)) ctr_arg = find b ctr_arg 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

277 
 find (t as _ $ _) ctr_arg = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

278 
let 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

279 
val (f', args') = strip_comb t; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

280 
val n = find_index (equal ctr_arg) args'; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

281 
in 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

282 
if n < 0 then 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

283 
find f' ctr_arg @ maps (fn x => find x ctr_arg) args' 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

284 
else 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

285 
let val (f, args) = chop n args' >> curry list_comb f' in 
53358  286 
if has_call f then 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

287 
f :: maps (fn x => find x ctr_arg) args 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

288 
else 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

289 
find f ctr_arg @ maps (fn x => find x ctr_arg) args 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

290 
end 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

291 
end 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

292 
 find _ _ = []; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

293 
in 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

294 
map (find (#rhs_term eqn_data)) (#ctr_args eqn_data) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

295 
> (fn [] => NONE  callss => SOME (#ctr eqn_data, callss)) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

296 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

297 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

298 
fun add_primrec fixes specs lthy = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

299 
let 
53352  300 
val (bs, mxs) = map_split (apfst fst) fixes; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

301 
val fun_names = map Binding.name_of bs; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

302 
val eqns_data = map (snd #> dissect_eqn lthy fun_names) specs; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

303 
val funs_data = eqns_data 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

304 
> partition_eq ((op =) o pairself #fun_name) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

305 
> finds (fn (x, y) => x = #fun_name (hd y)) fun_names > fst 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

306 
> map (fn (x, y) => the_single y handle List.Empty => 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

307 
primrec_error ("missing equations for function " ^ quote x)); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

308 

53358  309 
val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes > member (op =)); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

310 
val arg_Ts = map (#rec_type o hd) funs_data; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

311 
val res_Ts = map (#res_type o hd) funs_data; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

312 
val callssss = funs_data 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

313 
> map (partition_eq ((op =) o pairself #ctr)) 
53358  314 
> map (maps (map_filter (find_rec_calls has_call))); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

315 

53358  316 
fun get_indices t = map (fst #>> Binding.name_of #> Free) fixes 
317 
> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE) 

318 
> map_filter I; 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

319 
val ((nontriv, rec_specs, _, induct_thm, induct_thms), lthy') = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

320 
rec_specs_of bs arg_Ts res_Ts get_indices callssss lthy; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

321 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

322 
val actual_nn = length funs_data; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

323 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

324 
val _ = let val ctrs = (maps (map #ctr o #ctr_specs) rec_specs) in 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

325 
map (fn {ctr, user_eqn, ...} => member (op =) ctrs ctr orelse 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

326 
primrec_error_eqn ("argument " ^ quote (Syntax.string_of_term lthy' ctr) ^ 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

327 
" is not a constructor in lefthand side") user_eqn) eqns_data end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

328 

53358  329 
val defs = build_defs lthy' bs mxs funs_data rec_specs has_call; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

330 

53329  331 
fun prove def_thms' {ctr_specs, nested_map_idents, nested_map_comps, ...} induct_thm fun_data 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

332 
lthy = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

333 
let 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

334 
val fun_name = #fun_name (hd fun_data); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

335 
val def_thms = map (snd o snd) def_thms'; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

336 
val simp_thms = finds (fn (x, y) => #ctr x = #ctr y) fun_data ctr_specs 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

337 
> fst 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

338 
> map_filter (try (fn (x, [y]) => 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

339 
(#user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y))) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

340 
> map (fn (user_eqn, num_extra_args, rec_thm) => 
53329  341 
mk_primrec_tac lthy num_extra_args nested_map_idents nested_map_comps def_thms rec_thm 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

342 
> K > Goal.prove lthy [] [] user_eqn) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

343 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

344 
val notes = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

345 
[(inductN, if actual_nn > 1 then [induct_thm] else [], []), 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

346 
(simpsN, simp_thms, simp_attrs)] 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

347 
> filter_out (null o #2) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

348 
> map (fn (thmN, thms, attrs) => 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

349 
((Binding.qualify true fun_name (Binding.name thmN), attrs), [(thms, [])])); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

350 
in 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

351 
lthy > Local_Theory.notes notes 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

352 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

353 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

354 
val common_name = mk_common_name fun_names; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

355 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

356 
val common_notes = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

357 
[(inductN, if nontriv andalso actual_nn > 1 then [induct_thm] else [], [])] 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

358 
> filter_out (null o #2) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

359 
> map (fn (thmN, thms, attrs) => 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

360 
((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])])); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

361 
in 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

362 
lthy' 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

363 
> fold_map Local_Theory.define defs 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

364 
> snd oo (fn def_thms' => fold_map3 (prove def_thms') (take actual_nn rec_specs) 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

365 
(take actual_nn induct_thms) funs_data) 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

366 
> snd o Local_Theory.notes common_notes 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

367 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

368 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

369 
fun add_primrec_cmd raw_fixes raw_specs lthy = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

370 
let 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

371 
val _ = let val d = duplicates (op =) (map (Binding.name_of o #1) raw_fixes) in null d orelse 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

372 
primrec_error ("duplicate function name(s): " ^ commas d) end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

373 
val (fixes, specs) = fst (Specification.read_spec raw_fixes raw_specs lthy); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

374 
in 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

375 
add_primrec fixes specs lthy 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

376 
handle ERROR str => primrec_error str 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

377 
end 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

378 
handle Primrec_Error (str, eqns) => 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

379 
if null eqns 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

380 
then error ("primrec_new error:\n " ^ str) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

381 
else error ("primrec_new error:\n " ^ str ^ "\nin\n " ^ 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

382 
space_implode "\n " (map (quote o Syntax.string_of_term lthy) eqns)) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

383 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

384 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

385 

53310  386 
(* Primcorec *) 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

387 

53341  388 
type co_eqn_data_disc = { 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

389 
fun_name: string, 
53720  390 
fun_T: typ, 
53401  391 
fun_args: term list, 
53720  392 
ctr: term, 
53341  393 
ctr_no: int, (*###*) 
53720  394 
disc: term, 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

395 
prems: term list, 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

396 
user_eqn: term 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

397 
}; 
53341  398 
type co_eqn_data_sel = { 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

399 
fun_name: string, 
53720  400 
fun_T: typ, 
53401  401 
fun_args: term list, 
53341  402 
ctr: term, 
403 
sel: term, 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

404 
rhs_term: term, 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

405 
user_eqn: term 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

406 
}; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

407 
datatype co_eqn_data = 
53341  408 
Disc of co_eqn_data_disc  
409 
Sel of co_eqn_data_sel; 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

410 

53720  411 
fun co_dissect_eqn_disc sequential fun_names corec_specs prems' concl matchedsss = 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

412 
let 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

413 
fun find_subterm p = let (* FIXME \<exists>? *) 
53401  414 
fun f (t as u $ v) = if p t then SOME t else merge_options (f u, f v) 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

415 
 f t = if p t then SOME t else NONE 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

416 
in f end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

417 

53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

418 
val applied_fun = concl 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

419 
> find_subterm (member ((op =) o apsnd SOME) fun_names o try (fst o dest_Free o head_of)) 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

420 
> the 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

421 
handle Option.Option => primrec_error_eqn "malformed discriminator equation" concl; 
53720  422 
val ((fun_name, fun_T), fun_args) = strip_comb applied_fun >> dest_Free; 
423 
val {ctr_specs, ...} = the (AList.lookup (op =) (fun_names ~~ corec_specs) fun_name); 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

424 

53720  425 
val discs = map #disc ctr_specs; 
426 
val ctrs = map #ctr ctr_specs; 

53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

427 
val not_disc = head_of concl = @{term Not}; 
53401  428 
val _ = not_disc andalso length ctrs <> 2 andalso 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

429 
primrec_error_eqn "\<not>ed discriminator for a type with \<noteq> 2 constructors" concl; 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

430 
val disc = find_subterm (member (op =) discs o head_of) concl; 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

431 
val eq_ctr0 = concl > perhaps (try (HOLogic.dest_not)) > try (HOLogic.dest_eq #> snd) 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

432 
> (fn SOME t => let val n = find_index (equal t) ctrs in 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

433 
if n >= 0 then SOME n else NONE end  _ => NONE); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

434 
val _ = is_some disc orelse is_some eq_ctr0 orelse 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

435 
primrec_error_eqn "no discriminator in equation" concl; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

436 
val ctr_no' = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

437 
if is_none disc then the eq_ctr0 else find_index (equal (head_of (the disc))) discs; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

438 
val ctr_no = if not_disc then 1  ctr_no' else ctr_no'; 
53720  439 
val ctr = #ctr (nth ctr_specs ctr_no); 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

440 

8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

441 
val catch_all = try (fst o dest_Free o the_single) prems' = SOME Name.uu_; 
53720  442 
val matchedss = AList.lookup (op =) matchedsss fun_name > the_default []; 
443 
val prems = map (abstract (List.rev fun_args)) prems'; 

444 
val real_prems = 

445 
(if catch_all orelse sequential then maps invert_prems_disj matchedss else []) @ 

53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

446 
(if catch_all then [] else prems); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

447 

53720  448 
val matchedsss' = AList.delete (op =) fun_name matchedsss 
449 
> cons (fun_name, if sequential then matchedss @ [prems] else matchedss @ [real_prems]); 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

450 

53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

451 
val user_eqn = 
53720  452 
(real_prems, betapply (#disc (nth ctr_specs ctr_no), applied_fun)) 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

453 
>> map HOLogic.mk_Trueprop > HOLogic.mk_Trueprop 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

454 
> Logic.list_implies; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

455 
in 
53341  456 
(Disc { 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

457 
fun_name = fun_name, 
53720  458 
fun_T = fun_T, 
53401  459 
fun_args = fun_args, 
53720  460 
ctr = ctr, 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

461 
ctr_no = ctr_no, 
53720  462 
disc = #disc (nth ctr_specs ctr_no), 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

463 
prems = real_prems, 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

464 
user_eqn = user_eqn 
53720  465 
}, matchedsss') 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

466 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

467 

53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

468 
fun co_dissect_eqn_sel fun_names corec_specs eqn' eqn = 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

469 
let 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

470 
val (lhs, rhs) = HOLogic.dest_eq eqn 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

471 
handle TERM _ => 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

472 
primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

473 
val sel = head_of lhs; 
53720  474 
val ((fun_name, fun_T), fun_args) = dest_comb lhs > snd > strip_comb > apfst dest_Free 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

475 
handle TERM _ => 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

476 
primrec_error_eqn "malformed selector argument in lefthand side" eqn; 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

477 
val corec_spec = the (AList.lookup (op =) (fun_names ~~ corec_specs) fun_name) 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

478 
handle Option.Option => primrec_error_eqn "malformed selector argument in lefthand side" eqn; 
53341  479 
val (ctr_spec, sel) = #ctr_specs corec_spec 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

480 
> the o get_index (try (the o find_first (equal sel) o #sels)) 
53341  481 
>> nth (#ctr_specs corec_spec); 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

482 
val user_eqn = drop_All eqn'; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

483 
in 
53341  484 
Sel { 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

485 
fun_name = fun_name, 
53720  486 
fun_T = fun_T, 
53401  487 
fun_args = fun_args, 
53341  488 
ctr = #ctr ctr_spec, 
489 
sel = sel, 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

490 
rhs_term = rhs, 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

491 
user_eqn = user_eqn 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

492 
} 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

493 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

494 

53720  495 
fun co_dissect_eqn_ctr sequential fun_names corec_specs eqn' imp_prems imp_rhs matchedsss = 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

496 
let 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

497 
val (lhs, rhs) = HOLogic.dest_eq imp_rhs; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

498 
val fun_name = head_of lhs > fst o dest_Free; 
53720  499 
val {ctr_specs, ...} = the (AList.lookup (op =) (fun_names ~~ corec_specs) fun_name); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

500 
val (ctr, ctr_args) = strip_comb rhs; 
53720  501 
val {disc, sels, ...} = the (find_first (equal ctr o #ctr) ctr_specs) 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

502 
handle Option.Option => primrec_error_eqn "not a constructor" ctr; 
53341  503 

53720  504 
val disc_imp_rhs = betapply (disc, lhs); 
505 
val (maybe_eqn_data_disc, matchedsss') = if length ctr_specs = 1 

506 
then (NONE, matchedsss) 

53341  507 
else apfst SOME (co_dissect_eqn_disc 
53720  508 
sequential fun_names corec_specs imp_prems disc_imp_rhs matchedsss); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

509 

53720  510 
val sel_imp_rhss = (sels ~~ ctr_args) 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

511 
> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg)); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

512 

53360  513 
val _ = tracing ("reduced\n " ^ Syntax.string_of_term @{context} imp_rhs ^ "\nto\n \<cdot> " ^ 
53341  514 
(is_some maybe_eqn_data_disc ? K (Syntax.string_of_term @{context} disc_imp_rhs ^ "\n \<cdot> ")) "" ^ 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

515 
space_implode "\n \<cdot> " (map (Syntax.string_of_term @{context}) sel_imp_rhss)); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

516 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

517 
val eqns_data_sel = 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

518 
map (co_dissect_eqn_sel fun_names corec_specs eqn') sel_imp_rhss; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

519 
in 
53720  520 
(the_list maybe_eqn_data_disc @ eqns_data_sel, matchedsss') 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

521 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

522 

53720  523 
fun co_dissect_eqn sequential fun_names corec_specs eqn' matchedsss = 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

524 
let 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

525 
val eqn = drop_All eqn' 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

526 
handle TERM _ => primrec_error_eqn "malformed function equation" eqn'; 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

527 
val (imp_prems, imp_rhs) = Logic.strip_horn eqn 
53341  528 
> apfst (map HOLogic.dest_Trueprop) o apsnd HOLogic.dest_Trueprop; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

529 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

530 
val head = imp_rhs 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

531 
> perhaps (try HOLogic.dest_not) > perhaps (try (fst o HOLogic.dest_eq)) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

532 
> head_of; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

533 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

534 
val maybe_rhs = imp_rhs > perhaps (try (HOLogic.dest_not)) > try (snd o HOLogic.dest_eq); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

535 

53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

536 
val discs = maps #ctr_specs corec_specs > map #disc; 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

537 
val sels = maps #ctr_specs corec_specs > maps #sels; 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

538 
val ctrs = maps #ctr_specs corec_specs > map #ctr; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

539 
in 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

540 
if member (op =) discs head orelse 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

541 
is_some maybe_rhs andalso 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

542 
member (op =) (filter (null o binder_types o fastype_of) ctrs) (the maybe_rhs) then 
53720  543 
co_dissect_eqn_disc sequential fun_names corec_specs imp_prems imp_rhs matchedsss 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

544 
>> single 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

545 
else if member (op =) sels head then 
53720  546 
([co_dissect_eqn_sel fun_names corec_specs eqn' imp_rhs], matchedsss) 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

547 
else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) then 
53720  548 
co_dissect_eqn_ctr sequential fun_names corec_specs eqn' imp_prems imp_rhs matchedsss 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

549 
else 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

550 
primrec_error_eqn "malformed function equation" eqn 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

551 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

552 

53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

553 
fun build_corec_arg_disc ctr_specs {fun_args, ctr_no, prems, ...} = 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

554 
if is_none (#pred (nth ctr_specs ctr_no)) then I else 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

555 
mk_conjs prems 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

556 
> curry subst_bounds (List.rev fun_args) 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

557 
> HOLogic.tupled_lambda (HOLogic.mk_tuple fun_args) 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

558 
> K > nth_map (the (#pred (nth ctr_specs ctr_no))); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

559 

53720  560 
fun build_corec_arg_no_call sel_eqns sel = 
561 
find_first (equal sel o #sel) sel_eqns 

562 
> try (fn SOME {fun_args, rhs_term, ...} => abs_tuple fun_args rhs_term) 

563 
> the_default undef_const 

53411  564 
> K; 
53360  565 

53735  566 
fun build_corec_args_direct_call lthy has_call sel_eqns sel = 
53360  567 
let 
53411  568 
val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns; 
53735  569 
fun rewrite_q t = if has_call t then @{term False} else @{term True}; 
570 
fun rewrite_g t = if has_call t then undef_const else t; 

571 
fun rewrite_h t = if has_call t then HOLogic.mk_tuple (snd (strip_comb t)) else undef_const; 

572 
fun massage _ NONE t = t 

573 
 massage f (SOME {fun_args, rhs_term, ...}) t = 

574 
massage_direct_corec_call lthy has_call f (range_type (fastype_of t)) rhs_term 

575 
> abs_tuple fun_args; 

53360  576 
in 
53735  577 
(massage rewrite_q maybe_sel_eqn, 
578 
massage rewrite_g maybe_sel_eqn, 

579 
massage rewrite_h maybe_sel_eqn) 

53360  580 
end; 
581 

53411  582 
fun build_corec_arg_indirect_call lthy has_call sel_eqns sel = 
583 
let 

584 
val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns; 

53735  585 
fun rewrite bound_Ts U T (Abs (v, V, b)) = Abs (v, V, rewrite (V :: bound_Ts) U T b) 
586 
 rewrite bound_Ts U T (t as _ $ _) = 

53734
7613573f023a
avoid infinite loop for unapplied terms + tuning
blanchet
parents:
53733
diff
changeset

587 
let val (u, vs) = strip_comb t in 
7613573f023a
avoid infinite loop for unapplied terms + tuning
blanchet
parents:
53733
diff
changeset

588 
if is_Free u andalso has_call u then 
53735  589 
Inr_const U T $ mk_tuple1 bound_Ts vs 
53734
7613573f023a
avoid infinite loop for unapplied terms + tuning
blanchet
parents:
53733
diff
changeset

590 
else if try (fst o dest_Const) u = SOME @{const_name prod_case} then 
53735  591 
list_comb (map_types (K dummyT) u, map (rewrite bound_Ts U T) vs) 
53734
7613573f023a
avoid infinite loop for unapplied terms + tuning
blanchet
parents:
53733
diff
changeset

592 
else 
53735  593 
list_comb (rewrite bound_Ts U T u, map (rewrite bound_Ts U T) vs) 
594 
end 

595 
 rewrite _ U T t = if is_Free t andalso has_call t then Inr_const U T $ HOLogic.unit else t; 

596 
fun massage NONE t = t 

597 
 massage (SOME {fun_args, rhs_term, ...}) t = 

598 
massage_indirect_corec_call lthy has_call (rewrite []) [] 

599 
(range_type (fastype_of t)) rhs_term 

600 
> abs_tuple fun_args; 

53411  601 
in 
53735  602 
massage maybe_sel_eqn 
53411  603 
end; 
53360  604 

605 
fun build_corec_args_sel lthy has_call all_sel_eqns ctr_spec = 

53341  606 
let val sel_eqns = filter (equal (#ctr ctr_spec) o #ctr) all_sel_eqns in 
607 
if null sel_eqns then I else 

608 
let 

609 
val sel_call_list = #sels ctr_spec ~~ #calls ctr_spec; 

610 

611 
val no_calls' = map_filter (try (apsnd (fn No_Corec n => n))) sel_call_list; 

612 
val direct_calls' = map_filter (try (apsnd (fn Direct_Corec n => n))) sel_call_list; 

613 
val indirect_calls' = map_filter (try (apsnd (fn Indirect_Corec n => n))) sel_call_list; 

614 
in 

53360  615 
I 
53735  616 
#> fold (fn (sel, n) => nth_map n (build_corec_arg_no_call sel_eqns sel)) no_calls' 
53360  617 
#> fold (fn (sel, (q, g, h)) => 
53735  618 
let val (fq, fg, fh) = build_corec_args_direct_call lthy has_call sel_eqns sel in 
619 
nth_map q fq o nth_map g fg o nth_map h fh end) direct_calls' 

53360  620 
#> fold (fn (sel, n) => nth_map n 
53411  621 
(build_corec_arg_indirect_call lthy has_call sel_eqns sel)) indirect_calls' 
53341  622 
end 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

623 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

624 

53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

625 
fun co_build_defs lthy bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss = 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

626 
let 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

627 
val corec_specs' = take (length bs) corec_specs; 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

628 
val corecs = map #corec corec_specs'; 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

629 
val ctr_specss = map #ctr_specs corec_specs'; 
53360  630 
val corec_args = hd corecs 
631 
> fst o split_last o binder_types o fastype_of 

632 
> map (Const o pair @{const_name undefined}) 

53720  633 
> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss 
53360  634 
> fold2 (fold o build_corec_args_sel lthy has_call) sel_eqnss ctr_specss; 
53735  635 
fun currys [] t = t 
636 
 currys Ts t = t $ mk_tuple1 (List.rev Ts) (map Bound (length Ts  1 downto 0)) 

637 
> fold_rev (Term.abs o pair Name.uu) Ts; 

53401  638 

53360  639 
val _ = tracing ("corecursor arguments:\n \<cdot> " ^ 
53411  640 
space_implode "\n \<cdot> " (map (Syntax.string_of_term lthy) corec_args)); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

641 

53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

642 
val exclss' = 
53720  643 
disc_eqnss 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

644 
> map (map (fn {fun_args, ctr_no, prems, ...} => (fun_args, ctr_no, prems)) 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

645 
#> fst o (fn xs => fold_map (fn x => fn ys => ((x, ys), ys @ [x])) xs []) 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

646 
#> maps (uncurry (map o pair) 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

647 
#> map (fn ((fun_args, c, x), (_, c', y)) => ((c, c'), (x, mk_not (mk_conjs y))) 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

648 
> apfst (map HOLogic.mk_Trueprop) o apsnd HOLogic.mk_Trueprop 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

649 
> Logic.list_implies 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

650 
> curry Logic.list_all (map dest_Free fun_args)))) 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

651 
in 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

652 
map (list_comb o rpair corec_args) corecs 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

653 
> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

654 
> map2 currys arg_Tss 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

655 
> Syntax.check_terms lthy 
53352  656 
> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.map_name Thm.def_name b, []), t))) bs mxs 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

657 
> rpair exclss' 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

658 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

659 

53722
e176d6d3345f
generate more theorems (e.g. for types with only one constructor)
panny
parents:
53720
diff
changeset

660 
fun mk_real_disc_eqns fun_binding arg_Ts {ctr_specs, ...} sel_eqns disc_eqns = 
53720  661 
if length disc_eqns <> length ctr_specs  1 then disc_eqns else 
662 
let 

663 
val n = 0 upto length ctr_specs 

664 
> the o find_first (fn idx => not (exists (equal idx o #ctr_no) disc_eqns)); 

53722
e176d6d3345f
generate more theorems (e.g. for types with only one constructor)
panny
parents:
53720
diff
changeset

665 
val fun_args = (try (#fun_args o hd) disc_eqns, try (#fun_args o hd) sel_eqns) 
e176d6d3345f
generate more theorems (e.g. for types with only one constructor)
panny
parents:
53720
diff
changeset

666 
> the_default (map (curry Free Name.uu) arg_Ts) o merge_options; 
53720  667 
val extra_disc_eqn = { 
668 
fun_name = Binding.name_of fun_binding, 

669 
fun_T = arg_Ts > body_type (fastype_of (#ctr (hd ctr_specs))), 

53722
e176d6d3345f
generate more theorems (e.g. for types with only one constructor)
panny
parents:
53720
diff
changeset

670 
fun_args = fun_args, 
53720  671 
ctr = #ctr (nth ctr_specs n), 
672 
ctr_no = n, 

673 
disc = #disc (nth ctr_specs n), 

674 
prems = maps (invert_prems o #prems) disc_eqns, 

675 
user_eqn = undef_const}; 

676 
in 

677 
chop n disc_eqns > cons extra_disc_eqn > (op @) 

678 
end; 

679 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

680 
fun add_primcorec sequential fixes specs lthy = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

681 
let 
53352  682 
val (bs, mxs) = map_split (apfst fst) fixes; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

683 
val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> HOLogic.mk_tupleT) fixes > split_list; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

684 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

685 
(* copied from primrec_new *) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

686 
fun get_indices t = map (fst #>> Binding.name_of #> Free) fixes 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

687 
> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

688 
> map_filter I; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

689 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

690 
val callssss = []; (* FIXME *) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

691 

53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

692 
val ((nontriv, corec_specs', _, coinduct_thm, strong_co_induct_thm, coinduct_thmss, 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

693 
strong_coinduct_thmss), lthy') = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

694 
corec_specs_of bs arg_Ts res_Ts get_indices callssss lthy; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

695 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

696 
val fun_names = map Binding.name_of bs; 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

697 
val corec_specs = take (length fun_names) corec_specs'; (*###*) 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

698 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

699 
val (eqns_data, _) = 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

700 
fold_map (co_dissect_eqn sequential fun_names corec_specs) (map snd specs) [] 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

701 
>> flat; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

702 

53720  703 
val disc_eqnss' = map_filter (try (fn Disc x => x)) eqns_data 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

704 
> partition_eq ((op =) o pairself #fun_name) 
53720  705 
> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

706 
> map (sort ((op <) o pairself #ctr_no > make_ord) o flat o snd); 
53720  707 
val _ = disc_eqnss' > map (fn x => 
708 
let val d = duplicates ((op =) o pairself #ctr_no) x in null d orelse 

709 
primrec_error_eqns "excess discriminator equations in definition" 

710 
(maps (fn t => filter (equal (#ctr_no t) o #ctr_no) x) d > map #user_eqn) end); 

53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

711 

8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

712 
val sel_eqnss = map_filter (try (fn Sel x => x)) eqns_data 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

713 
> partition_eq ((op =) o pairself #fun_name) 
53720  714 
> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

715 
> map (flat o snd); 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

716 

53360  717 
val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes > member (op =)); 
718 
val arg_Tss = map (binder_types o snd o fst) fixes; 

53722
e176d6d3345f
generate more theorems (e.g. for types with only one constructor)
panny
parents:
53720
diff
changeset

719 
val disc_eqnss = map5 mk_real_disc_eqns bs arg_Tss corec_specs sel_eqnss disc_eqnss'; 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

720 
val (defs, exclss') = 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

721 
co_build_defs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss; 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

722 

8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

723 
(* try to prove (automatically generated) tautologies by ourselves *) 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

724 
val exclss'' = exclss' 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

725 
> map (map (apsnd 
53699  726 
(`(try (fn t => Goal.prove lthy [] [] t (mk_primcorec_assumption_tac lthy > K)))))); 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

727 
val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) exclss''; 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

728 
val (obligation_idxss, obligationss) = exclss'' 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

729 
> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd)) 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

730 
> split_list o map split_list; 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

731 

8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

732 
fun prove thmss' def_thms' lthy = 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

733 
let 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

734 
val def_thms = map (snd o snd) def_thms'; 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

735 

8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

736 
val exclss' = map (op ~~) (obligation_idxss ~~ thmss'); 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

737 
fun mk_exclsss excls n = 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

738 
(excls, map (fn k => replicate k [TrueI] @ replicate (n  k) []) (0 upto n  1)) 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

739 
> fold (fn ((c, c'), thm) => nth_map c (nth_map c' (K [thm]))); 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

740 
val exclssss = (exclss' ~~ taut_thmss > map (op @), fun_names ~~ corec_specs) 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

741 
> map2 (fn excls => fn (_, {ctr_specs, ...}) => mk_exclsss excls (length ctr_specs)); 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

742 

8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

743 
fun prove_disc {ctr_specs, ...} exclsss 
53720  744 
{fun_name, fun_T, fun_args, ctr_no, prems, user_eqn, ...} = 
53722
e176d6d3345f
generate more theorems (e.g. for types with only one constructor)
panny
parents:
53720
diff
changeset

745 
if Term.aconv_untyped (#disc (nth ctr_specs ctr_no), @{term "\<lambda>x. x = x"}) then [] else 
53720  746 
let 
53722
e176d6d3345f
generate more theorems (e.g. for types with only one constructor)
panny
parents:
53720
diff
changeset

747 
val {disc_corec, ...} = nth ctr_specs ctr_no; 
53720  748 
val k = 1 + ctr_no; 
749 
val m = length prems; 

750 
val t = 

751 
list_comb (Free (fun_name, fun_T), map Bound (length fun_args  1 downto 0)) 

752 
> curry betapply (#disc (nth ctr_specs ctr_no)) (*###*) 

753 
> HOLogic.mk_Trueprop 

754 
> curry Logic.list_implies (map HOLogic.mk_Trueprop prems) 

755 
> curry Logic.list_all (map dest_Free fun_args); 

756 
in 

757 
mk_primcorec_disc_tac lthy def_thms disc_corec k m exclsss 

758 
> K > Goal.prove lthy [] [] t 

759 
> pair (#disc (nth ctr_specs ctr_no)) 

760 
> single 

761 
end; 

762 

763 
fun prove_sel {ctr_specs, nested_maps, nested_map_idents, nested_map_comps, ...} 

764 
disc_eqns exclsss {fun_name, fun_T, fun_args, ctr, sel, rhs_term, ...} = 

53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

765 
let 
53720  766 
val (SOME ctr_spec) = find_first (equal ctr o #ctr) ctr_specs; 
767 
val ctr_no = find_index (equal ctr o #ctr) ctr_specs; 

768 
val prems = the_default (maps (invert_prems o #prems) disc_eqns) 

769 
(find_first (equal ctr_no o #ctr_no) disc_eqns > Option.map #prems); 

770 
val sel_corec = find_index (equal sel) (#sels ctr_spec) 

771 
> nth (#sel_corecs ctr_spec); 

53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

772 
val k = 1 + ctr_no; 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

773 
val m = length prems; 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

774 
val t = 
53720  775 
list_comb (Free (fun_name, fun_T), map Bound (length fun_args  1 downto 0)) 
776 
> curry betapply sel 

777 
> rpair (abstract (List.rev fun_args) rhs_term) 

778 
> HOLogic.mk_Trueprop o HOLogic.mk_eq 

53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

779 
> curry Logic.list_implies (map HOLogic.mk_Trueprop prems) 
53720  780 
> curry Logic.list_all (map dest_Free fun_args); 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

781 
in 
53692  782 
mk_primcorec_ctr_or_sel_tac lthy def_thms sel_corec k m exclsss 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

783 
nested_maps nested_map_idents nested_map_comps 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

784 
> K > Goal.prove lthy [] [] t 
53720  785 
> pair sel 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

786 
end; 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

787 

53720  788 
fun prove_ctr (_, disc_thms) (_, sel_thms') disc_eqns sel_eqns 
789 
{ctr, disc, sels, collapse, ...} = 

790 
if not (exists (equal ctr o #ctr) disc_eqns) 

53722
e176d6d3345f
generate more theorems (e.g. for types with only one constructor)
panny
parents:
53720
diff
changeset

791 
andalso not (exists (equal ctr o #ctr) sel_eqns) 
e176d6d3345f
generate more theorems (e.g. for types with only one constructor)
panny
parents:
53720
diff
changeset

792 
andalso (warning ("no eqns for ctr " ^ Syntax.string_of_term lthy ctr); true) 
e176d6d3345f
generate more theorems (e.g. for types with only one constructor)
panny
parents:
53720
diff
changeset

793 
orelse (* don't try to prove theorems when some sel_eqns are missing *) 
53720  794 
filter (equal ctr o #ctr) sel_eqns 
795 
> fst o finds ((op =) o apsnd #sel) sels 

796 
> exists (null o snd) 

797 
andalso (warning ("sel_eqn(s) missing for ctr " ^ Syntax.string_of_term lthy ctr); true) 

798 
then [] else 

799 
let 

800 
val _ = tracing ("ctr = " ^ Syntax.string_of_term lthy ctr); 

53735  801 
val _ = tracing (the_default "no disc_eqn" (Option.map (curry (op ^) "disc = " o Syntax.string_of_term lthy o #disc) (find_first (equal ctr o #ctr) disc_eqns))); 
53722
e176d6d3345f
generate more theorems (e.g. for types with only one constructor)
panny
parents:
53720
diff
changeset

802 
val (fun_name, fun_T, fun_args, prems) = 
e176d6d3345f
generate more theorems (e.g. for types with only one constructor)
panny
parents:
53720
diff
changeset

803 
(find_first (equal ctr o #ctr) disc_eqns, find_first (equal ctr o #ctr) sel_eqns) 
e176d6d3345f
generate more theorems (e.g. for types with only one constructor)
panny
parents:
53720
diff
changeset

804 
>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #prems x)) 
e176d6d3345f
generate more theorems (e.g. for types with only one constructor)
panny
parents:
53720
diff
changeset

805 
> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, [])) 
e176d6d3345f
generate more theorems (e.g. for types with only one constructor)
panny
parents:
53720
diff
changeset

806 
> the o merge_options; 
53720  807 
val m = length prems; 
808 
val t = sel_eqns 

809 
> fst o finds ((op =) o apsnd #sel) sels 

810 
> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x)) #> abstract) 

811 
> curry list_comb ctr 

812 
> curry HOLogic.mk_eq (list_comb (Free (fun_name, fun_T), 

813 
map Bound (length fun_args  1 downto 0))) 

814 
> HOLogic.mk_Trueprop 

815 
> curry Logic.list_implies (map HOLogic.mk_Trueprop prems) 

816 
> curry Logic.list_all (map dest_Free fun_args); 

53722
e176d6d3345f
generate more theorems (e.g. for types with only one constructor)
panny
parents:
53720
diff
changeset

817 
val maybe_disc_thm = AList.lookup (op =) disc_thms disc; 
53720  818 
val sel_thms = map snd (filter (member (op =) sels o fst) sel_thms'); 
819 
val _ = tracing ("t = " ^ Syntax.string_of_term lthy t); 

820 
val _ = tracing ("m = " ^ @{make_string} m); 

821 
val _ = tracing ("collapse = " ^ @{make_string} collapse); 

53722
e176d6d3345f
generate more theorems (e.g. for types with only one constructor)
panny
parents:
53720
diff
changeset

822 
val _ = tracing ("maybe_disc_thm = " ^ @{make_string} maybe_disc_thm); 
53720  823 
val _ = tracing ("sel_thms = " ^ @{make_string} sel_thms); 
824 
in 

53722
e176d6d3345f
generate more theorems (e.g. for types with only one constructor)
panny
parents:
53720
diff
changeset

825 
mk_primcorec_ctr_of_dtr_tac lthy m collapse maybe_disc_thm sel_thms 
53720  826 
> K > Goal.prove lthy [] [] t 
827 
> single 

828 
end; 

829 

830 
val (disc_notes, disc_thmss) = 

831 
fun_names ~~ map3 (maps oo prove_disc) corec_specs exclssss disc_eqnss 

832 
> `(map (fn (fun_name, thms) => 

833 
((Binding.qualify true fun_name (@{binding disc}), simp_attrs), [(map snd thms, [])]))); 

834 
val (sel_notes, sel_thmss) = 

835 
fun_names ~~ map4 (map ooo prove_sel) corec_specs disc_eqnss exclssss sel_eqnss 

836 
> `(map (fn (fun_name, thms) => 

837 
((Binding.qualify true fun_name (@{binding sel}), simp_attrs), [(map snd thms, [])]))); 

838 
val ctr_notes = 

839 
fun_names ~~ map5 (maps oooo prove_ctr) disc_thmss sel_thmss 

840 
disc_eqnss sel_eqnss (map #ctr_specs corec_specs) 

53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

841 
> map (fn (fun_name, thms) => 
53736
82799e03fff7
don't declare ctr view primcorec theorems as simp (they loop)
traytel
parents:
53735
diff
changeset

842 
((Binding.qualify true fun_name (@{binding ctr}), []), [(thms, [])])); 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

843 
in 
53720  844 
lthy > snd o Local_Theory.notes 
845 
(filter (not o null o fst o the_single o snd) (disc_notes @ sel_notes @ ctr_notes)) 

53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

846 
end; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

847 
in 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

848 
lthy' 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

849 
> Proof.theorem NONE (curry (op #>) (fold_map Local_Theory.define defs) o prove) obligationss 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

850 
> Proof.refine (Method.primitive_text I) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

851 
> Seq.hd 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

852 
end 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

853 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

854 
fun add_primcorec_cmd seq (raw_fixes, raw_specs) lthy = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

855 
let 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

856 
val (fixes, specs) = fst (Specification.read_spec raw_fixes raw_specs lthy); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

857 
in 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

858 
add_primcorec seq fixes specs lthy 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

859 
handle ERROR str => primrec_error str 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

860 
end 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

861 
handle Primrec_Error (str, eqns) => 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

862 
if null eqns 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

863 
then error ("primcorec error:\n " ^ str) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

864 
else error ("primcorec error:\n " ^ str ^ "\nin\n " ^ 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

865 
space_implode "\n " (map (quote o Syntax.string_of_term lthy) eqns)) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

866 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

867 
end; 