author  blanchet 
Tue, 13 May 2014 11:10:22 +0200  
changeset 56945  3d1ead21a055 
parent 56858  0c3d0bc98abe 
child 57303  498a62e65f5f 
permissions  rwrr 
55061  1 
(* Title: HOL/Tools/BNF/bnf_gfp_rec_sugar.ML 
53303
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 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

3 
Author: Jasmin Blanchette, TU Muenchen 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

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

5 

55538  6 
Corecursor sugar ("primcorec" and "primcorecursive"). 
53303
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 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

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

10 
sig 
54899
7a01387c47d5
added tactic to prove 'disc_iff' properties in 'primcorec'
blanchet
parents:
54883
diff
changeset

11 
datatype primcorec_option = Sequential_Option  Exhaustive_Option 
7a01387c47d5
added tactic to prove 'disc_iff' properties in 'primcorec'
blanchet
parents:
54883
diff
changeset

12 

54591
c822230fd22b
prevent exception when equations for a function are missing;
panny
parents:
54279
diff
changeset

13 
val add_primcorecursive_cmd: primcorec_option list > 
53831
80423b9080cf
support "of" syntax to disambiguate selector equations
panny
parents:
53830
diff
changeset

14 
(binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list > 
80423b9080cf
support "of" syntax to disambiguate selector equations
panny
parents:
53830
diff
changeset

15 
Proof.context > Proof.state 
54591
c822230fd22b
prevent exception when equations for a function are missing;
panny
parents:
54279
diff
changeset

16 
val add_primcorec_cmd: primcorec_option list > 
53831
80423b9080cf
support "of" syntax to disambiguate selector equations
panny
parents:
53830
diff
changeset

17 
(binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list > 
80423b9080cf
support "of" syntax to disambiguate selector equations
panny
parents:
53830
diff
changeset

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

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

20 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

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

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

23 

54905
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54904
diff
changeset

24 
open Ctr_Sugar_General_Tactics 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

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

26 
open BNF_Util 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

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

28 
open BNF_FP_Util 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

29 
open BNF_FP_Def_Sugar 
54243  30 
open BNF_FP_N2M_Sugar 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

31 
open BNF_FP_Rec_Sugar_Util 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

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

33 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

34 
val codeN = "code" 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

35 
val ctrN = "ctr" 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

36 
val discN = "disc" 
54900  37 
val disc_iffN = "disc_iff" 
54835  38 
val excludeN = "exclude" 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

39 
val selN = "sel" 
53791  40 

54145
297d1c603999
make sure that registered code equations are actually equations
blanchet
parents:
54133
diff
changeset

41 
val nitpicksimp_attrs = @{attributes [nitpick_simp]}; 
53794  42 
val simp_attrs = @{attributes [simp]}; 
54145
297d1c603999
make sure that registered code equations are actually equations
blanchet
parents:
54133
diff
changeset

43 
val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

44 

55527  45 
exception PRIMCOREC of string * term list; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

46 

55527  47 
fun primcorec_error str = raise PRIMCOREC (str, []); 
48 
fun primcorec_error_eqn str eqn = raise PRIMCOREC (str, [eqn]); 

49 
fun primcorec_error_eqns str eqns = raise PRIMCOREC (str, eqns); 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

50 

54899
7a01387c47d5
added tactic to prove 'disc_iff' properties in 'primcorec'
blanchet
parents:
54883
diff
changeset

51 
datatype primcorec_option = Sequential_Option  Exhaustive_Option; 
54591
c822230fd22b
prevent exception when equations for a function are missing;
panny
parents:
54279
diff
changeset

52 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

53 
datatype corec_call = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

54 
Dummy_No_Corec of int  
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

55 
No_Corec of int  
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

56 
Mutual_Corec of int * int * int  
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

57 
Nested_Corec of int; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

58 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

59 
type basic_corec_ctr_spec = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

60 
{ctr: term, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

61 
disc: term, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

62 
sels: term list}; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

63 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

64 
type corec_ctr_spec = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

65 
{ctr: term, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

66 
disc: term, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

67 
sels: term list, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

68 
pred: int option, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

69 
calls: corec_call list, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

70 
discI: thm, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

71 
sel_thms: thm list, 
54900  72 
disc_excludess: thm list list, 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

73 
collapse: thm, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

74 
corec_thm: thm, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

75 
disc_corec: thm, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

76 
sel_corecs: thm list}; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

77 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

78 
type corec_spec = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

79 
{corec: term, 
54924  80 
disc_exhausts: thm list, 
56858  81 
sel_defs: thm list, 
54955
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

82 
nested_maps: thm list, 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

83 
nested_map_idents: thm list, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

84 
nested_map_comps: thm list, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

85 
ctr_specs: corec_ctr_spec list}; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

86 

55527  87 
exception NOT_A_MAP of term; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

88 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

89 
fun not_codatatype ctxt T = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

90 
error ("Not a codatatype: " ^ Syntax.string_of_typ ctxt T); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

91 
fun ill_formed_corec_call ctxt t = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

92 
error ("Illformed corecursive call: " ^ quote (Syntax.string_of_term ctxt t)); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

93 
fun invalid_map ctxt t = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

94 
error ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t)); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

95 
fun unexpected_corec_call ctxt t = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

96 
error ("Unexpected corecursive call: " ^ quote (Syntax.string_of_term ctxt t)); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

97 

55870  98 
fun sort_list_duplicates xs = map snd (sort (int_ord o pairself fst) xs); 
54948  99 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

100 
val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True}; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

101 
val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False}; 
54900  102 
val mk_dnf = mk_disjs o map mk_conjs; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

103 

55008
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

104 
val conjuncts_s = filter_out (curry (op aconv) @{const True}) o HOLogic.conjuncts; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

105 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

106 
fun s_not @{const True} = @{const False} 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

107 
 s_not @{const False} = @{const True} 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

108 
 s_not (@{const Not} $ t) = t 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

109 
 s_not (@{const conj} $ t $ u) = @{const disj} $ s_not t $ s_not u 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

110 
 s_not (@{const disj} $ t $ u) = @{const conj} $ s_not t $ s_not u 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

111 
 s_not t = @{const Not} $ t; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

112 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

113 
val s_not_conj = conjuncts_s o s_not o mk_conjs; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

114 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

115 
fun propagate_unit_pos u cs = if member (op aconv) cs u then [@{const False}] else cs; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

116 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

117 
fun propagate_unit_neg not_u cs = remove (op aconv) not_u cs; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

118 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

119 
fun propagate_units css = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

120 
(case List.partition (can the_single) css of 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

121 
([], _) => css 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

122 
 ([u] :: uss, css') => 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

123 
[u] :: propagate_units (map (propagate_unit_neg (s_not u)) 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

124 
(map (propagate_unit_pos u) (uss @ css')))); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

125 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

126 
fun s_conjs cs = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

127 
if member (op aconv) cs @{const False} then @{const False} 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

128 
else mk_conjs (remove (op aconv) @{const True} cs); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

129 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

130 
fun s_disjs ds = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

131 
if member (op aconv) ds @{const True} then @{const True} 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

132 
else mk_disjs (remove (op aconv) @{const False} ds); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

133 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

134 
fun s_dnf css0 = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

135 
let val css = propagate_units css0 in 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

136 
if null css then 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

137 
[@{const False}] 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

138 
else if exists null css then 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

139 
[] 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

140 
else 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

141 
map (fn c :: cs => (c, cs)) css 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

142 
> AList.coalesce (op =) 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

143 
> map (fn (c, css) => c :: s_dnf css) 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

144 
> (fn [cs] => cs  css => [s_disjs (map s_conjs css)]) 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

145 
end; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

146 

55341
3d2c97392e25
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents:
55339
diff
changeset

147 
fun fold_rev_let_if_case ctxt f bound_Ts = 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

148 
let 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

149 
val thy = Proof_Context.theory_of ctxt; 
53794  150 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

151 
fun fld conds t = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

152 
(case Term.strip_comb t of 
55343  153 
(Const (@{const_name Let}, _), [_, _]) => fld conds (unfold_lets_splits t) 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

154 
 (Const (@{const_name If}, _), [cond, then_branch, else_branch]) => 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

155 
fld (conds @ conjuncts_s cond) then_branch o fld (conds @ s_not_conj [cond]) else_branch 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

156 
 (Const (c, _), args as _ :: _ :: _) => 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

157 
let val n = num_binder_types (Sign.the_const_type thy c)  1 in 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

158 
if n >= 0 andalso n < length args then 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

159 
(case fastype_of1 (bound_Ts, nth args n) of 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

160 
Type (s, Ts) => 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

161 
(case dest_case ctxt s Ts t of 
55341
3d2c97392e25
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents:
55339
diff
changeset

162 
SOME ({sel_splits = _ :: _, ...}, conds', branches) => 
3d2c97392e25
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents:
55339
diff
changeset

163 
fold_rev (uncurry fld) (map (append conds o conjuncts_s) conds' ~~ branches) 
3d2c97392e25
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents:
55339
diff
changeset

164 
 _ => f conds t) 
3d2c97392e25
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents:
55339
diff
changeset

165 
 _ => f conds t) 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

166 
else 
55341
3d2c97392e25
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents:
55339
diff
changeset

167 
f conds t 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

168 
end 
55342  169 
 _ => f conds t); 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

170 
in 
55341
3d2c97392e25
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents:
55339
diff
changeset

171 
fld [] 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

172 
end; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

173 

54970
891141de5672
only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents:
54969
diff
changeset

174 
fun case_of ctxt s = 
891141de5672
only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents:
54969
diff
changeset

175 
(case ctr_sugar_of ctxt s of 
891141de5672
only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents:
54969
diff
changeset

176 
SOME {casex = Const (s', _), sel_splits = _ :: _, ...} => SOME s' 
891141de5672
only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents:
54969
diff
changeset

177 
 _ => NONE); 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

178 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

179 
fun massage_let_if_case ctxt has_call massage_leaf = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

180 
let 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

181 
val thy = Proof_Context.theory_of ctxt; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

182 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

183 
fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else (); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

184 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

185 
fun massage_abs bound_Ts 0 t = massage_rec bound_Ts t 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

186 
 massage_abs bound_Ts m (Abs (s, T, t)) = Abs (s, T, massage_abs (T :: bound_Ts) (m  1) t) 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

187 
 massage_abs bound_Ts m t = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

188 
let val T = domain_type (fastype_of1 (bound_Ts, t)) in 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

189 
Abs (Name.uu, T, massage_abs (T :: bound_Ts) (m  1) (incr_boundvars 1 t $ Bound 0)) 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

190 
end 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

191 
and massage_rec bound_Ts t = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

192 
let val typof = curry fastype_of1 bound_Ts in 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

193 
(case Term.strip_comb t of 
55343  194 
(Const (@{const_name Let}, _), [_, _]) => massage_rec bound_Ts (unfold_lets_splits t) 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

195 
 (Const (@{const_name If}, _), obj :: (branches as [_, _])) => 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

196 
let val branches' = map (massage_rec bound_Ts) branches in 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

197 
Term.list_comb (If_const (typof (hd branches')) $ tap check_no_call obj, branches') 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

198 
end 
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55400
diff
changeset

199 
 (c as Const (@{const_name case_prod}, _), arg :: args) => 
55343  200 
massage_rec bound_Ts 
201 
(unfold_lets_splits (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args))) 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

202 
 (Const (c, _), args as _ :: _ :: _) => 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

203 
(case try strip_fun_type (Sign.the_const_type thy c) of 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

204 
SOME (gen_branch_Ts, gen_body_fun_T) => 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

205 
let 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

206 
val gen_branch_ms = map num_binder_types gen_branch_Ts; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

207 
val n = length gen_branch_ms; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

208 
in 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

209 
if n < length args then 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

210 
(case gen_body_fun_T of 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

211 
Type (_, [Type (T_name, _), _]) => 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

212 
if case_of ctxt T_name = SOME c then 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

213 
let 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

214 
val (branches, obj_leftovers) = chop n args; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

215 
val branches' = map2 (massage_abs bound_Ts) gen_branch_ms branches; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

216 
val branch_Ts' = map typof branches'; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

217 
val body_T' = snd (strip_typeN (hd gen_branch_ms) (hd branch_Ts')); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

218 
val casex' = Const (c, branch_Ts' > map typof obj_leftovers > body_T'); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

219 
in 
54272
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

220 
Term.list_comb (casex', 
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

221 
branches' @ tap (List.app check_no_call) obj_leftovers) 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

222 
end 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

223 
else 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

224 
massage_leaf bound_Ts t 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

225 
 _ => massage_leaf bound_Ts t) 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

226 
else 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

227 
massage_leaf bound_Ts t 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

228 
end 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

229 
 NONE => massage_leaf bound_Ts t) 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

230 
 _ => massage_leaf bound_Ts t) 
55342  231 
end; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

232 
in 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

233 
massage_rec 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

234 
end; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

235 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

236 
fun curried_type (Type (@{type_name fun}, [Type (@{type_name prod}, Ts), T])) = Ts > T; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

237 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

238 
fun massage_nested_corec_call ctxt has_call raw_massage_call bound_Ts U t = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

239 
let 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

240 
fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else (); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

241 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

242 
val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

243 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

244 
fun massage_mutual_call bound_Ts U T t = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

245 
if has_call t then 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

246 
(case try dest_sumT U of 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

247 
SOME (U1, U2) => if U1 = T then raw_massage_call bound_Ts T U2 t else invalid_map ctxt t 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

248 
 NONE => invalid_map ctxt t) 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

249 
else 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

250 
build_map_Inl (T, U) $ t; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

251 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

252 
fun massage_map bound_Ts (Type (_, Us)) (Type (s, Ts)) t = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

253 
(case try (dest_map ctxt s) t of 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

254 
SOME (map0, fs) => 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

255 
let 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

256 
val Type (_, dom_Ts) = domain_type (fastype_of1 (bound_Ts, t)); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

257 
val map' = mk_map (length fs) dom_Ts Us map0; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

258 
val fs' = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

259 
map_flattened_map_args ctxt s (map3 (massage_map_or_map_arg bound_Ts) Us Ts) fs; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

260 
in 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

261 
Term.list_comb (map', fs') 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

262 
end 
55527  263 
 NONE => raise NOT_A_MAP t) 
264 
 massage_map _ _ _ t = raise NOT_A_MAP t 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

265 
and massage_map_or_map_arg bound_Ts U T t = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

266 
if T = U then 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

267 
tap check_no_call t 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

268 
else 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

269 
massage_map bound_Ts U T t 
55527  270 
handle NOT_A_MAP _ => massage_mutual_fun bound_Ts U T t 
55339
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

271 
and massage_mutual_fun bound_Ts U T t = 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

272 
(case t of 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

273 
Const (@{const_name comp}, _) $ t1 $ t2 => 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

274 
mk_comp bound_Ts (massage_mutual_fun bound_Ts U T t1, tap check_no_call t2) 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

275 
 _ => 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

276 
let 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

277 
val var = Var ((Name.uu, Term.maxidx_of_term t + 1), 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

278 
domain_type (fastype_of1 (bound_Ts, t))); 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

279 
in 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

280 
Term.lambda var (massage_call bound_Ts U T (betapply (t, var))) 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

281 
end) 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

282 
and massage_call bound_Ts U T = 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

283 
massage_let_if_case ctxt has_call (fn bound_Ts => fn t => 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

284 
if has_call t then 
54955
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

285 
(case U of 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

286 
Type (s, Us) => 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

287 
(case try (dest_ctr ctxt s) t of 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

288 
SOME (f, args) => 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

289 
let 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

290 
val typof = curry fastype_of1 bound_Ts; 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

291 
val f' = mk_ctr Us f 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

292 
val f'_T = typof f'; 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

293 
val arg_Ts = map typof args; 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

294 
in 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

295 
Term.list_comb (f', map3 (massage_call bound_Ts) (binder_types f'_T) arg_Ts args) 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

296 
end 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

297 
 NONE => 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

298 
(case t of 
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55400
diff
changeset

299 
Const (@{const_name case_prod}, _) $ t' => 
54955
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

300 
let 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

301 
val U' = curried_type U; 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

302 
val T' = curried_type T; 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

303 
in 
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55400
diff
changeset

304 
Const (@{const_name case_prod}, U' > U) $ massage_call bound_Ts U' T' t' 
54955
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

305 
end 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

306 
 t1 $ t2 => 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

307 
(if has_call t2 then 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

308 
massage_mutual_call bound_Ts U T t 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

309 
else 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

310 
massage_map bound_Ts U T t1 $ t2 
55527  311 
handle NOT_A_MAP _ => massage_mutual_call bound_Ts U T t) 
54955
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

312 
 Abs (s, T', t') => 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

313 
Abs (s, T', massage_call (T' :: bound_Ts) (range_type U) (range_type T) t') 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

314 
 _ => massage_mutual_call bound_Ts U T t)) 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

315 
 _ => ill_formed_corec_call ctxt t) 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

316 
else 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

317 
build_map_Inl (T, U) $ t) bound_Ts; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

318 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

319 
val T = fastype_of1 (bound_Ts, t); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

320 
in 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

321 
if has_call t then massage_call bound_Ts U T t else build_map_Inl (T, U) $ t 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

322 
end; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

323 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

324 
fun expand_to_ctr_term ctxt s Ts t = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

325 
(case ctr_sugar_of ctxt s of 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

326 
SOME {ctrs, casex, ...} => 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

327 
Term.list_comb (mk_case Ts (Type (s, Ts)) casex, map (mk_ctr Ts) ctrs) $ t 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

328 
 NONE => raise Fail "expand_to_ctr_term"); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

329 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

330 
fun expand_corec_code_rhs ctxt has_call bound_Ts t = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

331 
(case fastype_of1 (bound_Ts, t) of 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

332 
Type (s, Ts) => 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

333 
massage_let_if_case ctxt has_call (fn _ => fn t => 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

334 
if can (dest_ctr ctxt s) t then t else expand_to_ctr_term ctxt s Ts t) bound_Ts t 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

335 
 _ => raise Fail "expand_corec_code_rhs"); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

336 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

337 
fun massage_corec_code_rhs ctxt massage_ctr = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

338 
massage_let_if_case ctxt (K false) 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

339 
(fn bound_Ts => uncurry (massage_ctr bound_Ts) o Term.strip_comb); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

340 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

341 
fun fold_rev_corec_code_rhs ctxt f = 
55341
3d2c97392e25
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents:
55339
diff
changeset

342 
fold_rev_let_if_case ctxt (fn conds => uncurry (f conds) o Term.strip_comb); 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

343 

55400  344 
fun case_thms_of_term ctxt t = 
345 
let val ctr_sugars = map_filter (Ctr_Sugar.ctr_sugar_of_case ctxt o fst) (Term.add_consts t []) in 

55008
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

346 
(maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #disc_exhausts ctr_sugars, 
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

347 
maps #sel_splits ctr_sugars, maps #sel_split_asms ctr_sugars) 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

348 
end; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

349 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

350 
fun basic_corec_specs_of ctxt res_T = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

351 
(case res_T of 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

352 
Type (T_name, _) => 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

353 
(case Ctr_Sugar.ctr_sugar_of ctxt T_name of 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

354 
NONE => not_codatatype ctxt res_T 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

355 
 SOME {ctrs, discs, selss, ...} => 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

356 
let 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

357 
val thy = Proof_Context.theory_of ctxt; 
54272
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

358 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

359 
val gfpT = body_type (fastype_of (hd ctrs)); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

360 
val As_rho = tvar_subst thy [gfpT] [res_T]; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

361 
val substA = Term.subst_TVars As_rho; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

362 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

363 
fun mk_spec ctr disc sels = {ctr = substA ctr, disc = substA disc, sels = map substA sels}; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

364 
in 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

365 
map3 mk_spec ctrs discs selss 
54911  366 
handle ListPair.UnequalLengths => not_codatatype ctxt res_T 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

367 
end) 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

368 
 _ => not_codatatype ctxt res_T); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

369 

54955
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

370 
fun map_thms_of_typ ctxt (Type (s, _)) = 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55538
diff
changeset

371 
(case fp_sugar_of ctxt s of SOME {maps, ...} => maps  NONE => []) 
54955
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

372 
 map_thms_of_typ _ _ = []; 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

373 

55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

374 
fun corec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 = 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

375 
let 
55005  376 
val thy = Proof_Context.theory_of lthy0; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

377 

55871  378 
val ((missing_res_Ts, perm0_kks, fp_sugars as {nested_bnfs, 
379 
common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) = 

55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

380 
nested_to_mutual_fps Greatest_FP bs res_Ts callers callssss0 lthy0; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

381 

55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55538
diff
changeset

382 
val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

383 

55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55538
diff
changeset

384 
val indices = map #fp_res_index fp_sugars; 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55538
diff
changeset

385 
val perm_indices = map #fp_res_index perm_fp_sugars; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

386 

55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

387 
val perm_gfpTs = map #T perm_fp_sugars; 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

388 
val perm_ctrXs_Tsss' = map (repair_nullary_single_ctr o #ctrXs_Tss) perm_fp_sugars; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

389 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

390 
val nn0 = length res_Ts; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

391 
val nn = length perm_gfpTs; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

392 
val kks = 0 upto nn  1; 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

393 
val perm_ns' = map length perm_ctrXs_Tsss'; 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

394 

367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

395 
val perm_Ts = map #T perm_fp_sugars; 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

396 
val perm_Xs = map #X perm_fp_sugars; 
55863  397 
val perm_Cs = map (domain_type o body_fun_type o fastype_of o #co_rec) perm_fp_sugars; 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

398 
val Xs_TCs = perm_Xs ~~ (perm_Ts ~~ perm_Cs); 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

399 

55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

400 
fun zip_corecT (Type (s, Us)) = [Type (s, map (mk_sumTN o zip_corecT) Us)] 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

401 
 zip_corecT U = 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

402 
(case AList.lookup (op =) Xs_TCs U of 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

403 
SOME (T, C) => [T, C] 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

404 
 NONE => [U]); 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

405 

55869  406 
val perm_p_Tss = mk_corec_p_pred_types perm_Cs perm_ns'; 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

407 
val perm_f_Tssss = 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

408 
map2 (fn C => map (map (map (curry (op >) C) o zip_corecT))) perm_Cs perm_ctrXs_Tsss'; 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

409 
val perm_q_Tssss = 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

410 
map (map (map (fn [_] => []  [_, T] => [mk_pred1T (domain_type T)]))) perm_f_Tssss; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

411 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

412 
val (perm_p_hss, h) = indexedd perm_p_Tss 0; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

413 
val (perm_q_hssss, h') = indexedddd perm_q_Tssss h; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

414 
val (perm_f_hssss, _) = indexedddd perm_f_Tssss h'; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

415 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

416 
val fun_arg_hs = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

417 
flat (map3 flat_corec_preds_predsss_gettersss perm_p_hss perm_q_hssss perm_f_hssss); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

418 

55480
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55462
diff
changeset

419 
fun unpermute0 perm0_xs = permute_like_unique (op =) perm0_kks kks perm0_xs; 
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55462
diff
changeset

420 
fun unpermute perm_xs = permute_like_unique (op =) perm_indices indices perm_xs; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

421 

55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55538
diff
changeset

422 
val coinduct_thmss = map (unpermute0 o conj_dests nn) common_coinduct_thms; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

423 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

424 
val p_iss = map (map (find_index_eq fun_arg_hs)) (unpermute perm_p_hss); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

425 
val q_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_q_hssss); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

426 
val f_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_f_hssss); 
53358  427 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

428 
val f_Tssss = unpermute perm_f_Tssss; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

429 
val gfpTs = unpermute perm_gfpTs; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

430 
val Cs = unpermute perm_Cs; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

431 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

432 
val As_rho = tvar_subst thy (take nn0 gfpTs) res_Ts; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

433 
val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn arg_Ts; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

434 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

435 
val substA = Term.subst_TVars As_rho; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

436 
val substAT = Term.typ_subst_TVars As_rho; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

437 
val substCT = Term.typ_subst_TVars Cs_rho; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

438 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

439 
val perm_Cs' = map substCT perm_Cs; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

440 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

441 
fun call_of nullary [] [g_i] [Type (@{type_name fun}, [_, T])] = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

442 
(if exists_subtype_in Cs T then Nested_Corec 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

443 
else if nullary then Dummy_No_Corec 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

444 
else No_Corec) g_i 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

445 
 call_of _ [q_i] [g_i, g_i'] _ = Mutual_Corec (q_i, g_i, g_i'); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

446 

54900  447 
fun mk_ctr_spec ctr disc sels p_io q_iss f_iss f_Tss discI sel_thms disc_excludess collapse 
448 
corec_thm disc_corec sel_corecs = 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

449 
let val nullary = not (can dest_funT (fastype_of ctr)) in 
54900  450 
{ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_io, 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

451 
calls = map3 (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms, 
54900  452 
disc_excludess = disc_excludess, collapse = collapse, corec_thm = corec_thm, 
453 
disc_corec = disc_corec, sel_corecs = sel_corecs} 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

454 
end; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

455 

55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55538
diff
changeset

456 
fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...} 
55863  457 
: ctr_sugar) p_is q_isss f_isss f_Tsss corec_thms disc_corecs sel_corecss = 
458 
let val p_ios = map SOME p_is @ [NONE] in 

54900  459 
map14 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss 
460 
disc_excludesss collapses corec_thms disc_corecs sel_corecss 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

461 
end; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

462 

56858  463 
fun mk_spec ({T, ctr_sugar as {disc_exhausts, sel_defs, ...}, co_rec = corec, 
55863  464 
co_rec_thms = corec_thms, disc_co_recs = disc_corecs, 
465 
sel_co_recss = sel_corecss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss = 

56858  466 
{corec = mk_co_rec thy Greatest_FP (substAT T) perm_Cs' corec, disc_exhausts = disc_exhausts, 
467 
sel_defs = sel_defs, nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs, 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

468 
nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

469 
nested_map_comps = map map_comp_of_bnf nested_bnfs, 
55863  470 
ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms disc_corecs 
471 
sel_corecss}; 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

472 
in 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

473 
((is_some gfp_sugar_thms, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts, 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55538
diff
changeset

474 
co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms, 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55538
diff
changeset

475 
co_induct_of coinduct_thmss, strong_co_induct_of coinduct_thmss), lthy) 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

476 
end; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

477 

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

55969  480 
val abs_tuple_balanced = HOLogic.tupled_lambda o mk_tuple_balanced; 
55005  481 

53720  482 
fun abstract vs = 
55342  483 
let 
484 
fun abs n (t $ u) = abs n t $ abs n u 

485 
 abs n (Abs (v, T, b)) = Abs (v, T, abs (n + 1) b) 

486 
 abs n t = 

487 
let val j = find_index (curry (op =) t) vs in 

488 
if j < 0 then t else Bound (n + j) 

489 
end; 

490 
in abs 0 end; 

54271  491 

54153
67487a607ce2
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents:
54145
diff
changeset

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

493 
fun_name: string, 
53720  494 
fun_T: typ, 
53401  495 
fun_args: term list, 
53720  496 
ctr: term, 
54948  497 
ctr_no: int, 
53720  498 
disc: term, 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

499 
prems: term list, 
53822  500 
auto_gen: bool, 
54926
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

501 
ctr_rhs_opt: term option, 
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

502 
code_rhs_opt: term option, 
54948  503 
eqn_pos: int, 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

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

505 
}; 
54001  506 

54153
67487a607ce2
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents:
54145
diff
changeset

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

508 
fun_name: string, 
53720  509 
fun_T: typ, 
53401  510 
fun_args: term list, 
53341  511 
ctr: term, 
512 
sel: term, 

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

513 
rhs_term: term, 
54926
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

514 
ctr_rhs_opt: term option, 
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

515 
code_rhs_opt: term option, 
54948  516 
eqn_pos: int, 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

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

518 
}; 
54001  519 

54153
67487a607ce2
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents:
54145
diff
changeset

520 
datatype coeqn_data = 
67487a607ce2
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents:
54145
diff
changeset

521 
Disc of coeqn_data_disc  
67487a607ce2
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents:
54145
diff
changeset

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

523 

56152  524 
fun check_extra_variables lthy vars names eqn = 
525 
let val b = fold_aterms (fn x as Free (v, _) => 

526 
if (not (member (op =) vars x) andalso 

527 
not (member (op =) names v) andalso 

528 
v <> Name.uu_ andalso 

529 
not (Variable.is_fixed lthy v)) then cons x else I  _ => I) eqn [] 

530 
in 

531 
null b orelse 

532 
primcorec_error_eqn ("extra variable(s) in equation: " ^ 

533 
commas (map (Syntax.string_of_term lthy) b)) eqn 

534 
end; 

535 

536 
fun dissect_coeqn_disc lthy fun_names sequentials (basic_ctr_specss : basic_corec_ctr_spec list list) 

54948  537 
eqn_pos ctr_rhs_opt code_rhs_opt prems' concl matchedsss = 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

538 
let 
54272
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

539 
fun find_subterm p = 
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

540 
let (* FIXME \<exists>? *) 
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

541 
fun find (t as u $ v) = if p t then SOME t else merge_options (find u, find v) 
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

542 
 find t = if p t then SOME t else NONE; 
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

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

544 

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

545 
val applied_fun = concl 
55008
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

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

547 
> the 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

548 
handle Option.Option => primcorec_error_eqn "malformed discriminator formula" concl; 
53720  549 
val ((fun_name, fun_T), fun_args) = strip_comb applied_fun >> dest_Free; 
56152  550 

551 
val _ = let val fixeds = filter (Variable.is_fixed lthy o fst o dest_Free) fun_args in 

552 
null fixeds orelse primcorec_error_eqns "function argument(s) are fixed in context" fixeds 

553 
end; 

554 

555 
val _ = 

556 
let 

557 
val bad = prems' 

558 
> filter (exists_subterm (fn Free (v, _) => member (op =) fun_names v  _ => false)) 

559 
in 

560 
null bad orelse primcorec_error_eqns "corecursive call(s) in condition(s)" bad 

561 
end; 

562 

563 
val _ = forall is_Free fun_args orelse 

564 
primcorec_error_eqn ("nonvariable function argument \"" ^ 

565 
Syntax.string_of_term lthy (find_first (not o is_Free) fun_args > the) ^ 

566 
"\" (pattern matching is not supported by primcorec(ursive))") applied_fun 

567 

568 
val _ = let val d = duplicates (op =) fun_args in null d orelse 

569 
primcorec_error_eqn ("duplicate variable \"" ^ Syntax.string_of_term lthy (hd d) ^ "\"") 

570 
applied_fun end; 

571 

54902
a9291e4d2366
internally allow different values for 'sequential' for different constructors
blanchet
parents:
54901
diff
changeset

572 
val SOME (sequential, basic_ctr_specs) = 
a9291e4d2366
internally allow different values for 'sequential' for different constructors
blanchet
parents:
54901
diff
changeset

573 
AList.lookup (op =) (fun_names ~~ (sequentials ~~ basic_ctr_specss)) fun_name; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

574 

54160  575 
val discs = map #disc basic_ctr_specs; 
576 
val ctrs = map #ctr basic_ctr_specs; 

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

577 
val not_disc = head_of concl = @{term Not}; 
53401  578 
val _ = not_disc andalso length ctrs <> 2 andalso 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

579 
primcorec_error_eqn "negated discriminator for a type with \<noteq> 2 constructors" concl; 
54160  580 
val disc' = find_subterm (member (op =) discs o head_of) concl; 
54209  581 
val eq_ctr0 = concl > perhaps (try HOLogic.dest_not) > try (HOLogic.dest_eq #> snd) 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

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

583 
if n >= 0 then SOME n else NONE end  _ => NONE); 
56152  584 

585 
val _ = if is_some disc' andalso perhaps (try HOLogic.dest_not) concl <> the disc' 

586 
then primcorec_error_eqn "malformed discriminator formula" concl else (); 

587 

588 

54160  589 
val _ = is_some disc' orelse is_some eq_ctr0 orelse 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

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

591 
val ctr_no' = 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

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

593 
val ctr_no = if not_disc then 1  ctr_no' else ctr_no'; 
54160  594 
val {ctr, disc, ...} = nth basic_ctr_specs ctr_no; 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

595 

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

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

54905
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54904
diff
changeset

599 
val actual_prems = 
54901
0b8871677e0b
use same name for feature internally as in user interface, to facilitate grepping
blanchet
parents:
54900
diff
changeset

600 
(if catch_all orelse sequential then maps s_not_conj matchedss else []) @ 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

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

602 

53720  603 
val matchedsss' = AList.delete (op =) fun_name matchedsss 
54905
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54904
diff
changeset

604 
> cons (fun_name, if sequential then matchedss @ [prems] else matchedss @ [actual_prems]); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

605 

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

606 
val user_eqn = 
54905
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54904
diff
changeset

607 
(actual_prems, concl) 
54097
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

608 
>> map HOLogic.mk_Trueprop > HOLogic.mk_Trueprop o abstract (List.rev fun_args) 
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

609 
> curry Logic.list_all (map dest_Free fun_args) o Logic.list_implies; 
56152  610 

611 
val _ = check_extra_variables lthy fun_args fun_names user_eqn; 

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

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

614 
fun_name = fun_name, 
53720  615 
fun_T = fun_T, 
53401  616 
fun_args = fun_args, 
53720  617 
ctr = ctr, 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

618 
ctr_no = ctr_no, 
54160  619 
disc = disc, 
54905
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54904
diff
changeset

620 
prems = actual_prems, 
53822  621 
auto_gen = catch_all, 
54926
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

622 
ctr_rhs_opt = ctr_rhs_opt, 
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

623 
code_rhs_opt = code_rhs_opt, 
54948  624 
eqn_pos = eqn_pos, 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

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

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

628 

56152  629 
fun dissect_coeqn_sel lthy fun_names (basic_ctr_specss : basic_corec_ctr_spec list list) eqn_pos 
54951
e25b4d22082b
for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents:
54948
diff
changeset

630 
ctr_rhs_opt code_rhs_opt eqn0 of_spec_opt eqn = 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

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

632 
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

633 
handle TERM _ => 
55527  634 
primcorec_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

635 
val sel = head_of lhs; 
53720  636 
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

637 
handle TERM _ => 
55527  638 
primcorec_error_eqn "malformed selector argument in lefthand side" eqn; 
56152  639 

640 
val _ = let val fixeds = filter (Variable.is_fixed lthy o fst o dest_Free) fun_args in 

641 
null fixeds orelse primcorec_error_eqns "function argument(s) are fixed in context" fixeds 

642 
end; 

643 

54160  644 
val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name) 
54272
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

645 
handle Option.Option => 
55527  646 
primcorec_error_eqn "malformed selector argument in lefthand side" eqn; 
54160  647 
val {ctr, ...} = 
54926
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

648 
(case of_spec_opt of 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

649 
SOME of_spec => the (find_first (curry (op =) of_spec o #ctr) basic_ctr_specs) 
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

650 
 NONE => filter (exists (curry (op =) sel) o #sels) basic_ctr_specs > the_single 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

651 
handle List.Empty => primcorec_error_eqn "ambiguous selector  use \"of\"" eqn); 
54979
d7593bfccf25
correctly extract code RHS, with loose bound variables
blanchet
parents:
54978
diff
changeset

652 
val user_eqn = drop_all eqn0; 
56152  653 

654 
val _ = check_extra_variables lthy fun_args fun_names user_eqn; 

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

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

657 
fun_name = fun_name, 
53720  658 
fun_T = fun_T, 
53401  659 
fun_args = fun_args, 
54160  660 
ctr = ctr, 
53341  661 
sel = sel, 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

662 
rhs_term = rhs, 
54926
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

663 
ctr_rhs_opt = ctr_rhs_opt, 
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

664 
code_rhs_opt = code_rhs_opt, 
54948  665 
eqn_pos = eqn_pos, 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

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

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

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

669 

56152  670 
fun dissect_coeqn_ctr lthy fun_names sequentials (basic_ctr_specss : basic_corec_ctr_spec list list) 
54951
e25b4d22082b
for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents:
54948
diff
changeset

671 
eqn_pos eqn0 code_rhs_opt prems concl matchedsss = 
53910  672 
let 
54065  673 
val (lhs, rhs) = HOLogic.dest_eq concl; 
54097
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

674 
val (fun_name, fun_args) = strip_comb lhs >> fst o dest_Free; 
56152  675 

676 
val _ = check_extra_variables lthy fun_args fun_names (drop_all eqn0); 

677 

54209  678 
val SOME basic_ctr_specs = AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name; 
55343  679 
val (ctr, ctr_args) = strip_comb (unfold_lets_splits rhs); 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

680 
val {disc, sels, ...} = the (find_first (curry (op =) ctr o #ctr) basic_ctr_specs) 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

681 
handle Option.Option => primcorec_error_eqn "not a constructor" ctr; 
53341  682 

54065  683 
val disc_concl = betapply (disc, lhs); 
54976
b502f04c0442
repair 'exhaustive' feature for oneconstructor types
blanchet
parents:
54975
diff
changeset

684 
val (eqn_data_disc_opt, matchedsss') = 
b502f04c0442
repair 'exhaustive' feature for oneconstructor types
blanchet
parents:
54975
diff
changeset

685 
if null (tl basic_ctr_specs) then 
b502f04c0442
repair 'exhaustive' feature for oneconstructor types
blanchet
parents:
54975
diff
changeset

686 
(NONE, matchedsss) 
b502f04c0442
repair 'exhaustive' feature for oneconstructor types
blanchet
parents:
54975
diff
changeset

687 
else 
56152  688 
apfst SOME (dissect_coeqn_disc lthy fun_names sequentials basic_ctr_specss eqn_pos 
54926
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

689 
(SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt prems disc_concl matchedsss); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

690 

54159
eb5d58c99049
set stage for more flexible 'primrec' syntax for recursion through functions
blanchet
parents:
54157
diff
changeset

691 
val sel_concls = sels ~~ ctr_args 
56152  692 
> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg)) 
56806
f7d0520e7be2
use qualified name (was interpreted as a catchall variable name)
panny
parents:
56805
diff
changeset

693 
handle ListPair.UnequalLengths => 
56152  694 
primcorec_error_eqn "partially applied constructor in righthand side" rhs; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

695 

53856  696 
(* 
54065  697 
val _ = tracing ("reduced\n " ^ Syntax.string_of_term @{context} concl ^ "\nto\n \<cdot> " ^ 
54926
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

698 
(is_some eqn_data_disc_opt ? K (Syntax.string_of_term @{context} disc_concl ^ "\n \<cdot> ")) "" ^ 
54097
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

699 
space_implode "\n \<cdot> " (map (Syntax.string_of_term @{context}) sel_concls) ^ 
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

700 
"\nfor premise(s)\n \<cdot> " ^ 
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

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

703 

54160  704 
val eqns_data_sel = 
56152  705 
map (dissect_coeqn_sel lthy fun_names basic_ctr_specss eqn_pos 
54951
e25b4d22082b
for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents:
54948
diff
changeset

706 
(SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt eqn0 (SOME ctr)) sel_concls; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

707 
in 
54926
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

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

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

710 

54951
e25b4d22082b
for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents:
54948
diff
changeset

711 
fun dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss = 
54065  712 
let 
713 
val (lhs, (rhs', rhs)) = HOLogic.dest_eq concl > `(expand_corec_code_rhs lthy has_call []); 

54097
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

714 
val (fun_name, fun_args) = strip_comb lhs >> fst o dest_Free; 
56152  715 

716 
val _ = check_extra_variables lthy fun_args fun_names concl; 

717 

54209  718 
val SOME basic_ctr_specs = AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name; 
54065  719 

720 
val cond_ctrs = fold_rev_corec_code_rhs lthy (fn cs => fn ctr => fn _ => 

55008
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

721 
if member (op = o apsnd #ctr) basic_ctr_specs ctr then cons (ctr, cs) 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

722 
else primcorec_error_eqn "not a constructor" ctr) [] rhs' [] 
54065  723 
> AList.group (op =); 
724 

54068  725 
val ctr_premss = (case cond_ctrs of [_] => [[]]  _ => map (s_dnf o snd) cond_ctrs); 
54065  726 
val ctr_concls = cond_ctrs > map (fn (ctr, _) => 
727 
binder_types (fastype_of ctr) 

728 
> map_index (fn (n, T) => massage_corec_code_rhs lthy (fn _ => fn ctr' => fn args => 

729 
if ctr' = ctr then nth args n else Const (@{const_name undefined}, T)) [] rhs') 

55343  730 
> curry Term.list_comb ctr 
54065  731 
> curry HOLogic.mk_eq lhs); 
54902
a9291e4d2366
internally allow different values for 'sequential' for different constructors
blanchet
parents:
54901
diff
changeset

732 

a9291e4d2366
internally allow different values for 'sequential' for different constructors
blanchet
parents:
54901
diff
changeset

733 
val sequentials = replicate (length fun_names) false; 
54065  734 
in 
56152  735 
fold_map2 (dissect_coeqn_ctr lthy fun_names sequentials basic_ctr_specss eqn_pos eqn0 
54097
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

736 
(SOME (abstract (List.rev fun_args) rhs))) 
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

737 
ctr_premss ctr_concls matchedsss 
54065  738 
end; 
739 

54902
a9291e4d2366
internally allow different values for 'sequential' for different constructors
blanchet
parents:
54901
diff
changeset

740 
fun dissect_coeqn lthy has_call fun_names sequentials 
54951
e25b4d22082b
for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents:
54948
diff
changeset

741 
(basic_ctr_specss : basic_corec_ctr_spec list list) (eqn_pos, eqn0) of_spec_opt matchedsss = 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

742 
let 
54979
d7593bfccf25
correctly extract code RHS, with loose bound variables
blanchet
parents:
54978
diff
changeset

743 
val eqn = drop_all eqn0 
54951
e25b4d22082b
for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents:
54948
diff
changeset

744 
handle TERM _ => primcorec_error_eqn "malformed function equation" eqn0; 
54065  745 
val (prems, concl) = Logic.strip_horn eqn 
56152  746 
> apfst (map HOLogic.dest_Trueprop) o apsnd HOLogic.dest_Trueprop 
747 
handle TERM _ => primcorec_error_eqn "malformed function equation" eqn; 

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

748 

54065  749 
val head = concl 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

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

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

752 

54926
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

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

754 

54160  755 
val discs = maps (map #disc) basic_ctr_specss; 
756 
val sels = maps (maps #sels) basic_ctr_specss; 

757 
val ctrs = maps (map #ctr) basic_ctr_specss; 

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

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

759 
if member (op =) discs head orelse 
54951
e25b4d22082b
for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents:
54948
diff
changeset

760 
is_some rhs_opt andalso 
56805
8a87502c7da3
add additional check to avoid selector formula righthand side consisting of a nullary constructor getting interpreted as a discriminator formula
panny
parents:
56254
diff
changeset

761 
member (op =) (map SOME fun_names) (try (fst o dest_Free) head) andalso 
54951
e25b4d22082b
for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents:
54948
diff
changeset

762 
member (op =) (filter (null o binder_types o fastype_of) ctrs) (the rhs_opt) then 
56152  763 
dissect_coeqn_disc lthy fun_names sequentials basic_ctr_specss eqn_pos NONE NONE prems concl 
54951
e25b4d22082b
for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents:
54948
diff
changeset

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

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

766 
else if member (op =) sels head then 
56152  767 
([dissect_coeqn_sel lthy fun_names basic_ctr_specss eqn_pos NONE NONE eqn0 of_spec_opt concl], 
54901
0b8871677e0b
use same name for feature internally as in user interface, to facilitate grepping
blanchet
parents:
54900
diff
changeset

768 
matchedsss) 
56152  769 
else if is_some rhs_opt andalso 
770 
is_Free head andalso member (op =) fun_names (fst (dest_Free head)) then 

55343  771 
if member (op =) ctrs (head_of (unfold_lets_splits (the rhs_opt))) then 
56152  772 
dissect_coeqn_ctr lthy fun_names sequentials basic_ctr_specss eqn_pos eqn0 
54979
d7593bfccf25
correctly extract code RHS, with loose bound variables
blanchet
parents:
54978
diff
changeset

773 
(if null prems then 
d7593bfccf25
correctly extract code RHS, with loose bound variables
blanchet
parents:
54978
diff
changeset

774 
SOME (snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_assums_concl eqn0)))) 
d7593bfccf25
correctly extract code RHS, with loose bound variables
blanchet
parents:
54978
diff
changeset

775 
else 
d7593bfccf25
correctly extract code RHS, with loose bound variables
blanchet
parents:
54978
diff
changeset

776 
NONE) 
54975  777 
prems concl matchedsss 
54951
e25b4d22082b
for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents:
54948
diff
changeset

778 
else if null prems then 
e25b4d22082b
for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents:
54948
diff
changeset

779 
dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss 
e25b4d22082b
for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents:
54948
diff
changeset

780 
>> flat 
e25b4d22082b
for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents:
54948
diff
changeset

781 
else 
54956  782 
primcorec_error_eqn "cannot mix constructor and code views (see manual for details)" eqn 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

783 
else 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

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

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

786 

54002  787 
fun build_corec_arg_disc (ctr_specs : corec_ctr_spec list) 
54153
67487a607ce2
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents:
54145
diff
changeset

788 
({fun_args, ctr_no, prems, ...} : coeqn_data_disc) = 
56858  789 
if is_none (#pred (nth ctr_specs ctr_no)) then 
790 
I 

791 
else 

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

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

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

796 

54153
67487a607ce2
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents:
54145
diff
changeset

797 
fun build_corec_arg_no_call (sel_eqns : coeqn_data_sel list) sel = 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

798 
find_first (curry (op =) sel o #sel) sel_eqns 
55969  799 
> try (fn SOME {fun_args, rhs_term, ...} => abs_tuple_balanced fun_args rhs_term) 
53720  800 
> the_default undef_const 
53411  801 
> K; 
53360  802 

54153
67487a607ce2
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents:
54145
diff
changeset

803 
fun build_corec_args_mutual_call lthy has_call (sel_eqns : coeqn_data_sel list) sel = 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

804 
(case find_first (curry (op =) sel o #sel) sel_eqns of 
54208  805 
NONE => (I, I, I) 
806 
 SOME {fun_args, rhs_term, ... } => 

53876  807 
let 
54097
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

808 
val bound_Ts = List.rev (map fastype_of fun_args); 
54207
9296ebf40db0
tuned names (to make them independent from temporary naming convention used in characteristic theorems)
blanchet
parents:
54206
diff
changeset

809 
fun rewrite_stop _ t = if has_call t then @{term False} else @{term True}; 
9296ebf40db0
tuned names (to make them independent from temporary naming convention used in characteristic theorems)
blanchet
parents:
54206
diff
changeset

810 
fun rewrite_end _ t = if has_call t then undef_const else t; 
9296ebf40db0
tuned names (to make them independent from temporary naming convention used in characteristic theorems)
blanchet
parents:
54206
diff
changeset

811 
fun rewrite_cont bound_Ts t = 
55969  812 
if has_call t then mk_tuple1_balanced bound_Ts (snd (strip_comb t)) else undef_const; 
55339
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

813 
fun massage f _ = massage_let_if_case lthy has_call f bound_Ts rhs_term 
55969  814 
> abs_tuple_balanced fun_args; 
53876  815 
in 
54207
9296ebf40db0
tuned names (to make them independent from temporary naming convention used in characteristic theorems)
blanchet
parents:
54206
diff
changeset

816 
(massage rewrite_stop, massage rewrite_end, massage rewrite_cont) 
54208  817 
end); 
53360  818 

54153
67487a607ce2
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents:
54145
diff
changeset

819 
fun build_corec_arg_nested_call lthy has_call (sel_eqns : coeqn_data_sel list) sel = 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

820 
(case find_first (curry (op =) sel o #sel) sel_eqns of 
54208  821 
NONE => I 
822 
 SOME {fun_args, rhs_term, ...} => 

53899  823 
let 
55339
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

824 
fun massage bound_Ts U T = 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

825 
let 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

826 
fun rewrite bound_Ts (Abs (v, V, b)) = Abs (v, V, rewrite (V :: bound_Ts) b) 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

827 
 rewrite bound_Ts (t as _ $ _) = 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

828 
let val (u, vs) = strip_comb t in 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

829 
if is_Free u andalso has_call u then 
55969  830 
Inr_const U T $ mk_tuple1_balanced bound_Ts vs 
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55400
diff
changeset

831 
else if try (fst o dest_Const) u = SOME @{const_name case_prod} then 
55343  832 
map (rewrite bound_Ts) vs > chop 1 
833 
>> HOLogic.mk_split o the_single 

834 
> Term.list_comb 

55339
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

835 
else 
55343  836 
Term.list_comb (rewrite bound_Ts u, map (rewrite bound_Ts) vs) 
55339
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

837 
end 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

838 
 rewrite _ t = 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

839 
if is_Free t andalso has_call t then Inr_const U T $ HOLogic.unit else t; 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

840 
in 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

841 
rewrite bound_Ts 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

842 
end; 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

843 

54097
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

844 
val bound_Ts = List.rev (map fastype_of fun_args); 
55339
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

845 

f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

846 
fun build t = 
54097
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

847 
rhs_term 
55339
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

848 
> massage_nested_corec_call lthy has_call massage bound_Ts (range_type (fastype_of t)) 
55969  849 
> abs_tuple_balanced fun_args; 
53899  850 
in 
55339
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

851 
build 
54208  852 
end); 
53360  853 

54153
67487a607ce2
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents:
54145
diff
changeset

854 
fun build_corec_args_sel lthy has_call (all_sel_eqns : coeqn_data_sel list) 
54002  855 
(ctr_spec : corec_ctr_spec) = 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

856 
(case filter (curry (op =) (#ctr ctr_spec) o #ctr) all_sel_eqns of 
54208  857 
[] => I 
858 
 sel_eqns => 

859 
let 

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

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

862 
val mutual_calls' = map_filter (try (apsnd (fn Mutual_Corec n => n))) sel_call_list; 

863 
val nested_calls' = map_filter (try (apsnd (fn Nested_Corec n => n))) sel_call_list; 

864 
in 

865 
I 

866 
#> fold (fn (sel, n) => nth_map n (build_corec_arg_no_call sel_eqns sel)) no_calls' 

867 
#> fold (fn (sel, (q, g, h)) => 

868 
let val (fq, fg, fh) = build_corec_args_mutual_call lthy has_call sel_eqns sel in 

869 
nth_map q fq o nth_map g fg o nth_map h fh end) mutual_calls' 

870 
#> fold (fn (sel, n) => nth_map n 

871 
(build_corec_arg_nested_call lthy has_call sel_eqns sel)) nested_calls' 

872 
end); 

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

873 

54153
67487a607ce2
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents:
54145
diff
changeset

874 
fun build_codefs lthy bs mxs has_call arg_Tss (corec_specs : corec_spec list) 
67487a607ce2
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents:
54145
diff
changeset

875 
(disc_eqnss : coeqn_data_disc list list) (sel_eqnss : coeqn_data_sel list list) = 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

876 
let 
54160  877 
val corecs = map #corec corec_specs; 
878 
val ctr_specss = map #ctr_specs corec_specs; 

53360  879 
val corec_args = hd corecs 
880 
> fst o split_last o binder_types o fastype_of 

55966  881 
> map (fn T => if range_type T = HOLogic.boolT 
54806
a0f024caa04c
pass autoproved exhaustiveness properties to tactic;
panny
parents:
54628
diff
changeset

882 
then Abs (Name.uu_, domain_type T, @{term False}) 
a0f024caa04c
pass autoproved exhaustiveness properties to tactic;
panny
parents:
54628
diff
changeset

883 
else Const (@{const_name undefined}, T)) 
53720  884 
> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss 
53360  885 
> fold2 (fold o build_corec_args_sel lthy has_call) sel_eqnss ctr_specss; 
53735  886 
fun currys [] t = t 
55969  887 
 currys Ts t = t $ mk_tuple1_balanced (List.rev Ts) (map Bound (length Ts  1 downto 0)) 
53735  888 
> fold_rev (Term.abs o pair Name.uu) Ts; 
53401  889 

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

894 

54835  895 
val excludess' = 
53720  896 
disc_eqnss 
53822  897 
> map (map (fn x => (#fun_args x, #ctr_no x, #prems x, #auto_gen x)) 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

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

899 
#> maps (uncurry (map o pair) 
53822  900 
#> map (fn ((fun_args, c, x, a), (_, c', y, a')) => 
54068  901 
((c, c', a orelse a'), (x, s_not (s_conjs y))) 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

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

903 
> Logic.list_implies 
55342  904 
> 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

905 
in 
55343  906 
map (Term.list_comb o rpair corec_args) corecs 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

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

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

909 
> Syntax.check_terms lthy 
54155  910 
> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t))) 
911 
bs mxs 

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

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

914 

54905
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54904
diff
changeset

915 
fun mk_actual_disc_eqns fun_binding arg_Ts exhaustive ({ctr_specs, ...} : corec_spec) 
54153
67487a607ce2
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents:
54145
diff
changeset

916 
(sel_eqns : coeqn_data_sel list) (disc_eqns : coeqn_data_disc list) = 
54910  917 
let val num_disc_eqns = length disc_eqns in 
54912  918 
if (exhaustive andalso num_disc_eqns <> 0) orelse num_disc_eqns <> length ctr_specs  1 then 
54910  919 
disc_eqns 
920 
else 

921 
let 

922 
val n = 0 upto length ctr_specs 

55342  923 
> the o find_first (fn j => not (exists (curry (op =) j o #ctr_no) disc_eqns)); 
54958
4933165fd112
do not use wrong constructor in autogenerated proof goal
panny
parents:
54956
diff
changeset

924 
val {ctr, disc, ...} = nth ctr_specs n; 
54910  925 
val fun_args = (try (#fun_args o hd) disc_eqns, try (#fun_args o hd) sel_eqns) 
926 
> the_default (map (curry Free Name.uu) arg_Ts) o merge_options; 

54958
4933165fd112
do not use wrong constructor in autogenerated proof goal
panny
parents:
54956
diff
changeset

927 
val sel_eqn_opt = find_first (equal ctr o #ctr) sel_eqns; 
54910  928 
val extra_disc_eqn = { 
929 
fun_name = Binding.name_of fun_binding, 

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

931 
fun_args = fun_args, 

54958
4933165fd112
do not use wrong constructor in autogenerated proof goal
panny
parents:
54956
diff
changeset

932 
ctr = ctr, 
54910  933 
ctr_no = n, 
54958
4933165fd112
do not use wrong constructor in autogenerated proof goal
panny
parents:
54956
diff
changeset

934 
disc = disc, 
54910  935 
prems = maps (s_not_conj o #prems) disc_eqns, 
936 
auto_gen = true, 

54926
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

937 
ctr_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt > the_default NONE, 
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

938 
code_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt > the_default NONE, 
54979
d7593bfccf25
correctly extract code RHS, with loose bound variables
blanchet
parents:
54978
diff
changeset

939 
eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt > the_default 100000 (* FIXME *), 
54910  940 
user_eqn = undef_const}; 
941 
in 

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

943 
end 

944 
end; 

53720  945 

55100  946 
fun find_corec_calls ctxt has_call (basic_ctr_specs : basic_corec_ctr_spec list) 
947 
({ctr, sel, rhs_term, ...} : coeqn_data_sel) = 

54160  948 
let 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

949 
val sel_no = find_first (curry (op =) ctr o #ctr) basic_ctr_specs 
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

950 
> find_index (curry (op =) sel) o #sels o the; 
54160  951 
in 
55341
3d2c97392e25
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents:
55339
diff
changeset

952 
K (if has_call rhs_term then fold_rev_let_if_case ctxt (K cons) [] rhs_term [] else []) 
3d2c97392e25
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents:
55339
diff
changeset

953 
> nth_map sel_no > AList.map_entry (op =) ctr 
54160  954 
end; 
955 

54900  956 
fun applied_fun_of fun_name fun_T fun_args = 
55343  957 
Term.list_comb (Free (fun_name, fun_T), map Bound (length fun_args  1 downto 0)); 
54900  958 

54921
862c36b6e57c
avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents:
54917
diff
changeset

959 
fun is_trivial_implies thm = 
54967
78de75e3e52a
exhaustive rules like '(False ==> P) ==> P ==> P' are now filtered out as trivial
blanchet
parents:
54959
diff
changeset

960 
uncurry (member (op aconv)) (Logic.strip_horn (Thm.prop_of thm)); 
54921
862c36b6e57c
avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents:
54917
diff
changeset

961 

55009
d4b69107a86a
automatically solve proof obligations produced for code equations
blanchet
parents:
55008
diff
changeset

962 
fun add_primcorec_ursive auto opts fixes specs of_specs_opt lthy = 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

963 
let 
54272
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

964 
val thy = Proof_Context.theory_of lthy; 
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

965 

53352  966 
val (bs, mxs) = map_split (apfst fst) fixes; 
55969  967 
val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> mk_tupleT_balanced) fixes > split_list; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

968 

56254  969 
val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, @{sort type})) (bs ~~ arg_Ts) of 
54272
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

970 
[] => () 
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

971 
 (b, _) :: _ => primcorec_error ("type of " ^ Binding.print b ^ " contains top sort")); 
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

972 

54902
a9291e4d2366
internally allow different values for 'sequential' for different constructors
blanchet
parents:
54901
diff
changeset

973 
val actual_nn = length bs; 
a9291e4d2366
internally allow different values for 'sequential' for different constructors
blanchet
parents:
54901
diff
changeset

974 

a9291e4d2366
internally allow different values for 'sequential' for different constructors
blanchet
parents:
54901
diff
changeset

975 
val sequentials = replicate actual_nn (member (op =) opts Sequential_Option); 
a9291e4d2366
internally allow different values for 'sequential' for different constructors
blanchet
parents:
54901
diff
changeset

976 
val exhaustives = replicate actual_nn (member (op =) opts Exhaustive_Option); 
54591
c822230fd22b
prevent exception when equations for a function are missing;
panny
parents:
54279
diff
changeset

977 

54160  978 
val fun_names = map Binding.name_of bs; 
979 
val basic_ctr_specss = map (basic_corec_specs_of lthy) res_Ts; 

55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

980 
val frees = map (fst #>> Binding.name_of #> Free) fixes; 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

981 
val has_call = exists_subterm (member (op =) frees); 
54160  982 
val eqns_data = 
55871  983 
fold_map2 (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss) 
984 
(tag_list 0 (map snd specs)) of_specs_opt [] 

54160  985 
> flat o fst; 
986 

56152  987 
val _ = 
988 
let 

989 
val missing = fun_names 

990 
> filter (map (fn Disc x => #fun_name x  Sel x => #fun_name x) eqns_data 

991 
> not oo member (op =)) 

992 
in 

993 
null missing 

994 
orelse primcorec_error_eqns ("missing equations for function(s): " ^ commas missing) [] 

995 
end; 

996 

54160  997 
val callssss = 
998 
map_filter (try (fn Sel x => x)) eqns_data 

55008
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

999 
> partition_eq (op = o pairself #fun_name) 
54160  1000 
> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names 
54161  1001 
> map (flat o snd) 
54243  1002 
> map2 (fold o find_corec_calls lthy has_call) basic_ctr_specss 
54160  1003 
> map2 (curry (op >)) (map (map (fn {ctr, sels, ...} => 
1004 
(ctr, map (K []) sels))) basic_ctr_specss); 

1005 

1006 
(* 

1007 
val _ = tracing ("callssss = " ^ @{make_string} callssss); 

1008 
*) 

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

1009 

53830
ed2eb7df2aac
don't note more induction principles than there are functions + tuning
blanchet
parents:
53822
diff
changeset

1010 
val ((n2m, corec_specs', _, coinduct_thm, strong_coinduct_thm, coinduct_thms, 
53797  1011 
strong_coinduct_thms), lthy') = 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

1012 
corec_specs_of bs arg_Ts res_Ts frees callssss lthy; 
54948  1013 
val corec_specs = take actual_nn corec_specs'; 
54178  1014 
val ctr_specss = map #ctr_specs corec_specs; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

1015 

53720  1016 
val disc_eqnss' = map_filter (try (fn Disc x => x)) eqns_data 
55008
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

1017 
> partition_eq (op = o pairself #fun_name) 
53720  1018 
> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names 
55008
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

1019 
> map (sort (op < o pairself #ctr_no > make_ord) o flat o snd); 
56152  1020 

53720  1021 
val _ = disc_eqnss' > map (fn x => 
55008
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

1022 
let val d = duplicates (op = o pairself #ctr_no) x in null d orelse 
56152  1023 
(if forall (is_some o #ctr_rhs_opt) x then 
1024 
primcorec_error_eqns "multiple equations for constructor(s)" 

1025 
(maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d 

1026 
> map (the o #ctr_rhs_opt)) else 

1027 
primcorec_error_eqns "excess discriminator formula in definition" 

1028 
(maps (fn t => filter (curry (op =) (#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

1029 

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

1030 
val sel_eqnss = map_filter (try (fn Sel x => x)) eqns_data 
55008
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

1031 
> partition_eq (op = o pairself #fun_name) 
53720  1032 
> 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

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

1034 

53360  1035 
val arg_Tss = map (binder_types o snd o fst) fixes; 
54905
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54904
diff
changeset

1036 
val disc_eqnss = map6 mk_actual_disc_eqns bs arg_Tss exhaustives corec_specs sel_eqnss 
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54904
diff
changeset

1037 
disc_eqnss'; 
54835  1038 
val (defs, excludess') = 
54153
67487a607ce2
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents:
54145
diff
changeset

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

1040 

55009
d4b69107a86a
automatically solve proof obligations produced for code equations
blanchet
parents:
55008
diff
changeset

1041 
val tac_opts = 
d4b69107a86a
automatically solve proof obligations produced for code equations
blanchet
parents:
55008
diff
changeset

1042 
map (fn {code_rhs_opt, ...} :: _ => 
d4b69107a86a
automatically solve proof obligations produced for code equations
blanchet
parents:
55008
diff
changeset

1043 
if auto orelse is_some code_rhs_opt then SOME (auto_tac o #context) else NONE) disc_eqnss; 
d4b69107a86a
automatically solve proof obligations produced for code equations
blanchet
parents:
55008
diff
changeset

1044 

d4b69107a86a
automatically solve proof obligations produced for code equations
blanchet
parents:
55008
diff
changeset

1045 
fun exclude_tac tac_opt sequential (c, c', a) = 
54901
0b8871677e0b
use same name for feature internally as in user interface, to facilitate grepping
blanchet
parents:
54900
diff
changeset

1046 
if a orelse c = c' orelse sequential then 
0b8871677e0b
use same name for feature internally as in user interface, to facilitate grepping
blanchet
parents:
54900
diff
changeset

1047 
SOME (K (HEADGOAL (mk_primcorec_assumption_tac lthy []))) 
0b8871677e0b
use same name for feature internally as in user interface, to facilitate grepping
blanchet
parents:
54900
diff
changeset

1048 
else 
54926
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

1049 
tac_opt; 
53822  1050 

53856  1051 
(* 
53822  1052 
val _ = tracing ("exclusiveness properties:\n \<cdot> " ^ 
54835  1053 
space_implode "\n \<cdot> " (maps (map (Syntax.string_of_term lthy o snd)) excludess')); 
53856  1054 
*) 
53822  1055 

55342  1056 
val excludess'' = map3 (fn tac_opt => fn sequential => map (fn (j, goal) => 
1057 
(j, (Option.map (Goal.prove_sorry lthy [] [] goal #> Thm.close_derivation) 

1058 
(exclude_tac tac_opt sequential j), goal)))) 

55009
d4b69107a86a
automatically solve proof obligations produced for code equations
blanchet
parents:
55008
diff
changeset

1059 
tac_opts sequentials excludess'; 
56152  1060 

54835  1061 
val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) excludess''; 
55009
d4b69107a86a
automatically solve proof obligations produced for code equations
blanchet
parents:
55008
diff
changeset

1062 
val (goal_idxss, exclude_goalss) = excludess'' 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

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

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

1065 

54921
862c36b6e57c
avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents:
54917
diff
changeset

1066 
fun list_all_fun_args extras = 
54910  1067 
map2 (fn [] => I 
54921
862c36b6e57c
avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents:
54917
diff
changeset

1068 
 {fun_args, ...} :: _ => map (curry Logic.list_all (extras @ map dest_Free fun_args))) 
54903
c664bd02bf94
internally allow different values for 'exhaustive' for different constructors
blanchet
parents:
54902
diff
changeset

1069 
disc_eqnss; 
54844  1070 

54905
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54904
diff
changeset

1071 
val syntactic_exhaustives = 
54926
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

1072 
map (fn disc_eqns => forall (null o #prems orf is_some o #code_rhs_opt) disc_eqns 
54913  1073 
orelse exists #auto_gen disc_eqns) 
54905
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54904
diff
changeset

1074 
disc_eqnss; 
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54904
diff
changeset

1075 
val de_facto_exhaustives = 
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54904
diff
changeset

1076 
map2 (fn b => fn b' => b orelse b') exhaustives syntactic_exhaustives; 
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54904
diff
changeset

1077 

54903
c664bd02bf94
internally allow different values for 'exhaustive' for different constructors
blanchet
parents:
54902
diff
changeset

1078 
val nchotomy_goalss = 
54904  1079 
map2 (fn false => K []  true => single o HOLogic.mk_Trueprop o mk_dnf o map #prems) 
1080 
de_facto_exhaustives disc_eqnss 

54921
862c36b6e57c
avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents:
54917
diff
changeset

1081 
> list_all_fun_args [] 
54903
c664bd02bf94
internally allow different values for 'exhaustive' for different constructors
blanchet
parents:
54902
diff
changeset

1082 
val nchotomy_taut_thmss = 
55400  1083 
map5 (fn tac_opt => fn {disc_exhausts = res_disc_exhausts, ...} => 
55008
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

1084 
fn {code_rhs_opt, ...} :: _ => fn [] => K [] 
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

1085 
 [goal] => fn true => 
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

1086 
let 
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

1087 
val (_, _, arg_disc_exhausts, _, _) = 
55400  1088 
case_thms_of_term lthy (the_default Term.dummy code_rhs_opt); 
55008
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

1089 
in 
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

1090 
[Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => 
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

1091 
mk_primcorec_nchotomy_tac ctxt (res_disc_exhausts @ arg_disc_exhausts)) 
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

1092 
> Thm.close_derivation] 
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

1093 
end 
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

1094 
 false => 
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

1095 
(case tac_opt of 
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

1096 
SOME tac => [Goal.prove_sorry lthy [] [] goal tac > Thm.close_derivation] 
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

1097 
 NONE => [])) 
55400  1098 
tac_opts corec_specs disc_eqnss nchotomy_goalss syntactic_exhaustives; 
55008
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

1099 

b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

1100 
val syntactic_exhaustives = 
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

1101 
map (fn disc_eqns => forall (null o #prems orf is_some o #code_rhs_opt) disc_eqns 
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

1102 
orelse exists #auto_gen disc_eqns) 
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

1103 
disc_eqnss; 
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

1104 

55009
d4b69107a86a
automatically solve proof obligations produced for code equations
blanchet
parents:
55008
diff
changeset

1105 
val nchotomy_goalss = 
d4b69107a86a
automatically solve proof obligations produced for code equations
blanchet
parents:
55008
diff
changeset

1106 
map2 (fn (NONE, false) => map (rpair [])  _ => K []) (tac_opts ~~ syntactic_exhaustives) 
d4b69107a86a
automatically solve proof obligations produced for code equations
blanchet
parents:
55008
diff
changeset

1107 
nchotomy_goalss; 
d4b69107a86a
automatically solve proof obligations produced for code equations
blanchet
parents:
55008
diff
changeset

1108 

d4b69107a86a
automatically solve proof obligations produced for code equations
blanchet
parents:
55008
diff
changeset

1109 
val goalss = nchotomy_goalss @ exclude_goalss; 
54844  1110 

55462  1111 
fun prove thmss'' def_infos lthy = 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

1112 
let 
55462  1113 
val def_thms = map (snd o snd) def_infos; 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

1114 

54972
5747fdd4ad3b
fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents:
54970
diff
changeset

1115 
val (nchotomy_thmss, exclude_thmss) = 
55009
d4b69107a86a
automatically solve proof obligations produced for code equations
blanchet
parents:
55008
diff
changeset

1116 
(map2 append (take actual_nn thmss'') nchotomy_taut_thmss, drop actual_nn thmss''); 
54613  1117 

54927
a5a2598f0651
proper name generation to avoid clash with 'P' in user specification
blanchet
parents:
54926
diff
changeset

1118 
val ps = 
a5a2598f0651
proper name generation to avoid clash with 'P' in user specification
blanchet
parents:
54926
diff
changeset

1119 
Variable.variant_frees lthy (maps (maps #fun_args) disc_eqnss) [("P", HOLogic.boolT)]; 
a5a2598f0651
proper name generation to avoid clash with 'P' in user specification
blanchet
parents:
54926
diff
changeset

1120 

54903
c664bd02bf94
internally allow different values for 'exhaustive' for different constructors
blanchet
parents:
54902
diff
changeset

1121 
val exhaust_thmss = 
c664bd02bf94
internally allow different values for 'exhaustive' for different constructors
blanchet
parents:
54902
diff
changeset

1122 
map2 (fn false => K [] 
54921
862c36b6e57c
avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents:
54917
diff
changeset

1123 
 true => fn disc_eqns as {fun_args, ...} :: _ => 
862c36b6e57c
avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents:
54917
diff
changeset

1124 
let 
862c36b6e57c
avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents:
54917
diff
changeset

1125 
val p = Bound (length fun_args); 
862c36b6e57c
avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents:
54917
diff
changeset

1126 
fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p); 
862c36b6e57c
avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents:
54917
diff
changeset

1127 
in 
862c36b6e57c
avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents:
54917
diff
changeset

1128 
[mk_imp_p (map (mk_imp_p o map HOLogic.mk_Trueprop o #prems) disc_eqns)] 
862c36b6e57c
avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents:
54917
diff
changeset

1129 
end) 
54904  1130 
de_facto_exhaustives disc_eqnss 
54927
a5a2598f0651
proper name generation to avoid clash with 'P' in user specification
blanchet
parents:
54926
diff
changeset

1131 
> list_all_fun_args ps 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

1132 
> map3 (fn disc_eqns as {fun_args, ...} :: _ => fn [] => K [] 
54903
c664bd02bf94
internally allow different values for 'exhaustive' for different constructors
blanchet
parents:
54902
diff
changeset

1133 
 [nchotomy_thm] => fn [goal] => 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

1134 
[mk_primcorec_exhaust_tac lthy ("" (* for "P" *) :: map (fst o dest_Free) fun_args) 
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

1135 
(length disc_eqns) nchotomy_thm 
54951
e25b4d22082b
for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents:
54948
diff
changeset

1136 
> K > Goal.prove_sorry lthy [] [] goal 
54903
c664bd02bf94
internally allow different values for 'exhaustive' for different constructors
blanchet
parents:
54902
diff
changeset

1137 
> Thm.close_derivation]) 
c664bd02bf94
internally allow different values for 'exhaustive' for different constructors
blanchet
parents:
54902
diff
changeset

1138 
disc_eqnss nchotomy_thmss; 
54921
862c36b6e57c
avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents:
54917
diff
changeset

1139 
val nontriv_exhaust_thmss = map (filter_out is_trivial_implies) exhaust_thmss; 
54844  1140 

54835  1141 
val excludess' = map (op ~~) (goal_idxss ~~ exclude_thmss); 
1142 
fun mk_excludesss excludes n = 

54973  1143 
fold (fn ((c, c', _), thm) => nth_map c (nth_map c' (K [thm]))) 
54974
d1c76303244e
use correct default for exclude rules to avoid weird tactic failures
blanchet
parents:
54973
diff
changeset

1144 
excludes (map (fn k => replicate k [asm_rl] @ replicate (n  k) []) (0 upto n  1)); 
54973  1145 
val excludessss = 
1146 
map2 (fn excludes => mk_excludesss excludes o length o #ctr_specs) 

1147 
(map2 append excludess' taut_thmss) corec_specs; 

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

1148 

54835  1149 
fun prove_disc ({ctr_specs, ...} : corec_spec) excludesss 
54948  1150 
({fun_name, fun_T, fun_args, ctr_no, prems, eqn_pos, ...} : coeqn_data_disc) = 
54272
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

1151 
if Term.aconv_untyped (#disc (nth ctr_specs ctr_no), @{term "\<lambda>x. x = x"}) then 
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

1152 
[] 
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

1153 
else 
53720  1154 
let 
54900  1155 
val {disc, disc_corec, ...} = nth ctr_specs ctr_no; 
53720  1156 
val k = 1 + ctr_no; 
1157 
val m = length prems; 

54900  1158 
val goal = 
1159 
applied_fun_of fun_name fun_T fun_args 
