author  blanchet 
Fri, 10 Jan 2014 14:39:37 +0100  
changeset 54972  5747fdd4ad3b 
parent 54970  891141de5672 
child 54973  b35859240103 
permissions  rwrr 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

1 
(* Title: HOL/BNF/Tools/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 

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

6 
Corecursor sugar. 
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 

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

45 
exception Primcorec_Error of string * 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

46 

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

47 
fun primcorec_error str = raise Primcorec_Error (str, []); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

48 
fun primcorec_error_eqn str eqn = raise Primcorec_Error (str, [eqn]); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

49 
fun primcorec_error_eqns str eqns = raise Primcorec_Error (str, eqns); 
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, 
54955
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

81 
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

82 
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

83 
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

84 
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

85 

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

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

87 

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

88 
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

89 
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

90 
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

91 
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

92 
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

93 
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

94 
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

95 
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

96 

54948  97 
fun order_list_duplicates xs = map snd (sort (int_ord o pairself fst) xs) 
98 

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

99 
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

100 
val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False}; 
54900  101 
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

102 

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

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

104 

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

105 
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

106 
 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

107 
 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

108 
 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

109 
 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

110 
 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

111 

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

112 
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

113 

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

114 
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

115 

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

116 
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

117 

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

118 
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

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

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

121 
 ([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

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

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

124 

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

125 
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

126 
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

127 
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

128 

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

129 
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

130 
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

131 
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

132 

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

133 
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

134 
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

135 
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

136 
[@{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

137 
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

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

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

140 
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

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

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

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

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

145 

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

146 
fun fold_rev_let_if_case ctxt f 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

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

148 
val thy = Proof_Context.theory_of ctxt; 
53794  149 

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

150 
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

151 
(case Term.strip_comb 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

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

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

154 
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

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

156 
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

157 
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

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

159 
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

160 
(case dest_case ctxt s Ts t of 
54970
891141de5672
only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents:
54969
diff
changeset

161 
SOME (ctr_sugar as {sel_splits = _ :: _, ...}, conds', branches) => 
891141de5672
only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents:
54969
diff
changeset

162 
apfst (cons ctr_sugar) o fold_rev (uncurry fld) 
891141de5672
only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents:
54969
diff
changeset

163 
(map (append conds o conjuncts_s) conds' ~~ branches) 
891141de5672
only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents:
54969
diff
changeset

164 
 _ => apsnd (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

165 
 _ => apsnd (f 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

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

167 
apsnd (f 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

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

169 
 _ => apsnd (f 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

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

171 
fld [] t o pair [] 
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 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

194 
(Const (@{const_name Let}, _), [_, _]) => massage_rec bound_Ts (unfold_let t) 
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 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

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

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

201 
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

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

203 
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

204 
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

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

206 
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

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

208 
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

209 
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

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

211 
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

212 
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

213 
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

214 
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

215 
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

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

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

218 
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

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

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

221 
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

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

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 
end 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

226 
 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

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 
in 
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_rec 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

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

232 

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

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

234 

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

235 
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

236 

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

237 
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

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

239 
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

240 

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

241 
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

242 

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

243 
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

244 
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

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

246 
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

247 
 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

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

249 
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

250 

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

251 
fun massage_mutual_fun 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

252 
(case 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

253 
Const (@{const_name comp}, _) $ t1 $ t2 => 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

254 
mk_comp bound_Ts (massage_mutual_fun bound_Ts U T t1, tap check_no_call t2) 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

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

256 
let 
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 var = Var ((Name.uu, Term.maxidx_of_term t + 1), 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

258 
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

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

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

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

262 

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

263 
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

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

265 
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

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

267 
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

268 
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

269 
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

270 
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

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

272 
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

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

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

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

276 
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

277 
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

278 
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

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

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

281 
handle AINT_NO_MAP _ => massage_mutual_fun 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

282 

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

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

284 
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

285 
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

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

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

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

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

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

291 
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

292 
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

293 
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

294 
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

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

296 
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

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

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

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

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

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

302 
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

303 
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

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

305 
Const (@{const_name prod_case}, U' > U) $ massage_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

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

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

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

309 
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

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

311 
massage_map bound_Ts U T t1 $ t2 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

312 
handle AINT_NO_MAP _ => 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

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

314 
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

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

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

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

318 
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

319 

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

320 
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

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

322 
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

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

324 

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

325 
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

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

327 
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

328 
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

329 
 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

330 

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

331 
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

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

333 
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

334 
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

335 
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

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

337 

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

338 
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

339 
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

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

341 

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

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

343 
snd ooo fold_rev_let_if_case ctxt (fn conds => uncurry (f conds) 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

344 

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

345 
fun case_thms_of_term ctxt bound_Ts t = 
54970
891141de5672
only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents:
54969
diff
changeset

346 
let val (ctr_sugars, _) = fold_rev_let_if_case ctxt (K (K I)) bound_Ts t () in 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

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

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

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

350 

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

351 
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

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

353 
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

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

355 
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

356 
 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

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

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

359 

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

361 
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

362 
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

363 

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

364 
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

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

366 
map3 mk_spec ctrs discs selss 
54911  367 
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

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

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

370 

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

371 
fun map_thms_of_typ ctxt (Type (s, _)) = 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

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

373 
SOME {index, mapss, ...} => nth mapss index 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

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

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

376 

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 
fun corec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

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

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

380 

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

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

382 
fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...}, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

383 
co_inducts = coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy') = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

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

385 

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

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

387 

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

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

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

390 

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 perm_ctrss = map (#ctrs o of_fp_sugar #ctr_sugars) perm_fp_sugars; 
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 perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

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

394 

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

395 
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

396 
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

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

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

399 

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

400 
val perm_Cs = map (domain_type o body_fun_type o fastype_of o co_rec_of o 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

401 
of_fp_sugar (#xtor_co_iterss o #fp_res)) perm_fp_sugars; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

402 
val (perm_p_Tss, (perm_q_Tssss, _, 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

403 
mk_coiter_fun_arg_types perm_ctr_Tsss perm_Cs perm_ns (co_rec_of dtor_coiters1); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

404 

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

405 
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

406 
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

407 
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

408 

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

409 
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

410 
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

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 
fun unpermute0 perm0_xs = permute_like (op =) perm0_kks kks perm0_xs; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

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

414 

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

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

416 

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

417 
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

418 
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

419 
val f_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_f_hssss); 
53358  420 

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

422 
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

423 
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

424 

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

426 
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

427 

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

429 
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

430 
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

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

433 

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

434 
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

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

436 
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

437 
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

438 
 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

439 

54900  440 
fun mk_ctr_spec ctr disc sels p_io q_iss f_iss f_Tss discI sel_thms disc_excludess collapse 
441 
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

442 
let val nullary = not (can dest_funT (fastype_of ctr)) in 
54900  443 
{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

444 
calls = map3 (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms, 
54900  445 
disc_excludess = disc_excludess, collapse = collapse, corec_thm = corec_thm, 
446 
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

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

448 

54900  449 
fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss disc_coitersss 
450 
sel_coiterssss = 

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 
let 
54900  452 
val {ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...} : ctr_sugar = 
453 
nth ctr_sugars index; 

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 
val p_ios = map SOME p_is @ [NONE]; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

455 
val discIs = #discIs (nth ctr_sugars index); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

456 
val corec_thms = co_rec_of (nth coiter_thmsss index); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

457 
val disc_corecs = co_rec_of (nth disc_coitersss index); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

458 
val sel_corecss = co_rec_of (nth sel_coiterssss index); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

459 
in 
54900  460 
map14 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss 
461 
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

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

463 

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

464 
fun mk_spec ({T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

465 
disc_co_itersss = disc_coitersss, sel_co_iterssss = sel_coiterssss, ...} : fp_sugar) 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

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

467 
{corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of (nth coiterss index)), 
54924  468 
disc_exhausts = #disc_exhausts (nth ctr_sugars index), 
54955
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

469 
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

470 
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

471 
nested_map_comps = map map_comp_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

472 
ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

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

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

475 
((is_some gfp_sugar_thms, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_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

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

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

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

479 

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

53401  482 
val abs_tuple = HOLogic.tupled_lambda o HOLogic.mk_tuple; 
53720  483 
fun abstract vs = 
484 
let fun a n (t $ u) = a n t $ a n u 

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

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

486 
 a n t = let val idx = find_index (curry (op =) t) vs in 
53720  487 
if idx < 0 then t else Bound (n + idx) end 
488 
in a 0 end; 

54271  489 

490 
fun mk_prod1 bound_Ts (t, u) = 

491 
HOLogic.pair_const (fastype_of1 (bound_Ts, t)) (fastype_of1 (bound_Ts, u)) $ t $ u; 

492 
fun mk_tuple1 bound_Ts = the_default HOLogic.unit o try (foldr1 (mk_prod1 bound_Ts)); 

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

493 

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

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

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

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

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

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

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

507 
}; 
54001  508 

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

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

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

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

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

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

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

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

520 
}; 
54001  521 

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

522 
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

523 
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

524 
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

525 

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

526 
fun dissect_coeqn_disc fun_names sequentials (basic_ctr_specss : basic_corec_ctr_spec list list) 
54948  527 
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

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

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

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

531 
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

532 
 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

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

534 

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

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

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

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

538 
handle Option.Option => primcorec_error_eqn "malformed discriminator formula" concl; 
53720  539 
val ((fun_name, fun_T), fun_args) = strip_comb applied_fun >> dest_Free; 
54902
a9291e4d2366
internally allow different values for 'sequential' for different constructors
blanchet
parents:
54901
diff
changeset

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

541 
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

542 

54160  543 
val discs = map #disc basic_ctr_specs; 
544 
val ctrs = map #ctr basic_ctr_specs; 

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

545 
val not_disc = head_of concl = @{term Not}; 
53401  546 
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

547 
primcorec_error_eqn "negated discriminator for a type with \<noteq> 2 constructors" concl; 
54160  548 
val disc' = find_subterm (member (op =) discs o head_of) concl; 
54209  549 
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

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

551 
if n >= 0 then SOME n else NONE end  _ => NONE); 
54160  552 
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

553 
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

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

555 
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

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

558 

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

559 
val catch_all = try (fst o dest_Free o the_single) prems' = SOME Name.uu_; 
53720  560 
val matchedss = AList.lookup (op =) matchedsss fun_name > the_default []; 
561 
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

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

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

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

565 

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

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

568 

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

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

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

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

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

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

575 
fun_name = fun_name, 
53720  576 
fun_T = fun_T, 
53401  577 
fun_args = fun_args, 
53720  578 
ctr = ctr, 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

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

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

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

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

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

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

589 

54948  590 
fun dissect_coeqn_sel 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

591 
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

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

593 
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

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

595 
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

596 
val sel = head_of lhs; 
53720  597 
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

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

599 
primcorec_error_eqn "malformed selector argument in lefthand side" eqn; 
54160  600 
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

601 
handle Option.Option => 
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

602 
primcorec_error_eqn "malformed selector argument in lefthand side" eqn; 
54160  603 
val {ctr, ...} = 
54926
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

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

605 
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

606 
 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

607 
handle List.Empty => primcorec_error_eqn "ambiguous selector  use \"of\"" eqn); 
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

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

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

611 
fun_name = fun_name, 
53720  612 
fun_T = fun_T, 
53401  613 
fun_args = fun_args, 
54160  614 
ctr = ctr, 
53341  615 
sel = sel, 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

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

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

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

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

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

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

623 

54948  624 
fun dissect_coeqn_ctr 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

625 
eqn_pos eqn0 code_rhs_opt prems concl matchedsss = 
53910  626 
let 
54065  627 
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

628 
val (fun_name, fun_args) = strip_comb lhs >> fst o dest_Free; 
54209  629 
val SOME basic_ctr_specs = AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name; 
54074
43cdae9524bf
allow 'let's around constructors in constructor view
blanchet
parents:
54068
diff
changeset

630 
val (ctr, ctr_args) = strip_comb (unfold_let rhs); 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

631 
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

632 
handle Option.Option => primcorec_error_eqn "not a constructor" ctr; 
53341  633 

54065  634 
val disc_concl = betapply (disc, lhs); 
54926
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

635 
val (eqn_data_disc_opt, matchedsss') = if length basic_ctr_specs = 1 
53720  636 
then (NONE, matchedsss) 
54948  637 
else apfst SOME (dissect_coeqn_disc fun_names sequentials basic_ctr_specss eqn_pos 
54926
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

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

639 

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

640 
val sel_concls = sels ~~ ctr_args 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

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

642 

53856  643 
(* 
54065  644 
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

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

646 
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

647 
"\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

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

650 

54160  651 
val eqns_data_sel = 
54948  652 
map (dissect_coeqn_sel 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

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

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

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

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

657 

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

658 
fun dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss = 
54065  659 
let 
660 
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

661 
val (fun_name, fun_args) = strip_comb lhs >> fst o dest_Free; 
54209  662 
val SOME basic_ctr_specs = AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name; 
54065  663 

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

54160  665 
if member ((op =) o apsnd #ctr) basic_ctr_specs ctr 
54065  666 
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

667 
else primcorec_error_eqn "not a constructor" ctr) [] rhs' [] 
54065  668 
> AList.group (op =); 
669 

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

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

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

675 
> curry list_comb ctr 

676 
> curry HOLogic.mk_eq lhs); 

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

677 

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

678 
val sequentials = replicate (length fun_names) false; 
54065  679 
in 
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

680 
fold_map2 (dissect_coeqn_ctr 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

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

682 
ctr_premss ctr_concls matchedsss 
54065  683 
end; 
684 

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

685 
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

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

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

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

689 
handle TERM _ => primcorec_error_eqn "malformed function equation" eqn0; 
54065  690 
val (prems, concl) = Logic.strip_horn eqn 
53341  691 
> apfst (map HOLogic.dest_Trueprop) o apsnd HOLogic.dest_Trueprop; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

692 

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

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

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

696 

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

697 
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

698 

54160  699 
val discs = maps (map #disc) basic_ctr_specss; 
700 
val sels = maps (maps #sels) basic_ctr_specss; 

701 
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

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

703 
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

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

705 
member (op =) (filter (null o binder_types o fastype_of) ctrs) (the rhs_opt) 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

706 
dissect_coeqn_disc fun_names sequentials basic_ctr_specss eqn_pos NONE NONE prems concl 
e25b4d22082b
for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents:
54948
diff
changeset

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

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

709 
else if member (op =) sels head then 
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

710 
([dissect_coeqn_sel 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

711 
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

712 
else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) 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

713 
if member (op =) ctrs (head_of (unfold_let (the rhs_opt))) 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

714 
dissect_coeqn_ctr fun_names sequentials basic_ctr_specss eqn_pos eqn0 
e25b4d22082b
for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents:
54948
diff
changeset

715 
(if null prems then SOME eqn0 else NONE) prems 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

716 
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

717 
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

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

719 
else 
54956  720 
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

721 
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

722 
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

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

724 

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

726 
({fun_args, ctr_no, prems, ...} : coeqn_data_disc) = 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

727 
if is_none (#pred (nth ctr_specs ctr_no)) then I else 
54068  728 
s_conjs prems 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

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

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

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

732 

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

733 
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

734 
find_first (curry (op =) sel o #sel) sel_eqns 
53720  735 
> try (fn SOME {fun_args, rhs_term, ...} => abs_tuple fun_args rhs_term) 
736 
> the_default undef_const 

53411  737 
> K; 
53360  738 

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

739 
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

740 
(case find_first (curry (op =) sel o #sel) sel_eqns of 
54208  741 
NONE => (I, I, I) 
742 
 SOME {fun_args, rhs_term, ... } => 

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

744 
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

745 
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

746 
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

747 
fun rewrite_cont bound_Ts t = 
53899  748 
if has_call t then mk_tuple1 bound_Ts (snd (strip_comb t)) else undef_const; 
54102  749 
fun massage f _ = massage_mutual_corec_call lthy has_call f bound_Ts rhs_term 
54097
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

750 
> abs_tuple fun_args; 
53876  751 
in 
54207
9296ebf40db0
tuned names (to make them independent from temporary naming convention used in characteristic theorems)
blanchet
parents:
54206
diff
changeset

752 
(massage rewrite_stop, massage rewrite_end, massage rewrite_cont) 
54208  753 
end); 
53360  754 

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

755 
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

756 
(case find_first (curry (op =) sel o #sel) sel_eqns of 
54208  757 
NONE => I 
758 
 SOME {fun_args, rhs_term, ...} => 

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

760 
val bound_Ts = List.rev (map fastype_of fun_args); 
53899  761 
fun rewrite bound_Ts U T (Abs (v, V, b)) = Abs (v, V, rewrite (V :: bound_Ts) U T b) 
762 
 rewrite bound_Ts U T (t as _ $ _) = 

763 
let val (u, vs) = strip_comb t in 

764 
if is_Free u andalso has_call u then 

765 
Inr_const U T $ mk_tuple1 bound_Ts vs 

54271  766 
else if try (fst o dest_Const) u = SOME @{const_name prod_case} then 
53899  767 
map (rewrite bound_Ts U T) vs > chop 1 >> HOLogic.mk_split o the_single > list_comb 
768 
else 

769 
list_comb (rewrite bound_Ts U T u, map (rewrite bound_Ts U T) vs) 

770 
end 

771 
 rewrite _ U T t = 

772 
if is_Free t andalso has_call t then Inr_const U T $ HOLogic.unit else t; 

773 
fun massage t = 

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

774 
rhs_term 
54102  775 
> massage_nested_corec_call lthy has_call rewrite bound_Ts (range_type (fastype_of t)) 
53735  776 
> abs_tuple fun_args; 
53899  777 
in 
778 
massage 

54208  779 
end); 
53360  780 

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

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

783 
(case filter (curry (op =) (#ctr ctr_spec) o #ctr) all_sel_eqns of 
54208  784 
[] => I 
785 
 sel_eqns => 

786 
let 

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

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

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

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

791 
in 

792 
I 

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

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

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

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

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

798 
(build_corec_arg_nested_call lthy has_call sel_eqns sel)) nested_calls' 

799 
end); 

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

800 

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

801 
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

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

803 
let 
54160  804 
val corecs = map #corec corec_specs; 
805 
val ctr_specss = map #ctr_specs corec_specs; 

53360  806 
val corec_args = hd corecs 
807 
> fst o split_last o binder_types o fastype_of 

54806
a0f024caa04c
pass autoproved exhaustiveness properties to tactic;
panny
parents:
54628
diff
changeset

808 
> map (fn T => if range_type T = @{typ bool} 
a0f024caa04c
pass autoproved exhaustiveness properties to tactic;
panny
parents:
54628
diff
changeset

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

810 
else Const (@{const_name undefined}, T)) 
53720  811 
> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss 
53360  812 
> fold2 (fold o build_corec_args_sel lthy has_call) sel_eqnss ctr_specss; 
53735  813 
fun currys [] t = t 
814 
 currys Ts t = t $ mk_tuple1 (List.rev Ts) (map Bound (length Ts  1 downto 0)) 

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

53401  816 

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

821 

54835  822 
val excludess' = 
53720  823 
disc_eqnss 
53822  824 
> 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

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

826 
#> maps (uncurry (map o pair) 
53822  827 
#> map (fn ((fun_args, c, x, a), (_, c', y, a')) => 
54068  828 
((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

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

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

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

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

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

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

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

836 
> Syntax.check_terms lthy 
54155  837 
> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t))) 
838 
bs mxs 

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

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

841 

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

842 
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

843 
(sel_eqns : coeqn_data_sel list) (disc_eqns : coeqn_data_disc list) = 
54910  844 
let val num_disc_eqns = length disc_eqns in 
54912  845 
if (exhaustive andalso num_disc_eqns <> 0) orelse num_disc_eqns <> length ctr_specs  1 then 
54910  846 
disc_eqns 
847 
else 

848 
let 

849 
val n = 0 upto length ctr_specs 

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

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

851 
val {ctr, disc, ...} = nth ctr_specs n; 
54910  852 
val fun_args = (try (#fun_args o hd) disc_eqns, try (#fun_args o hd) sel_eqns) 
853 
> 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

854 
val sel_eqn_opt = find_first (equal ctr o #ctr) sel_eqns; 
54910  855 
val extra_disc_eqn = { 
856 
fun_name = Binding.name_of fun_binding, 

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

858 
fun_args = fun_args, 

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

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

861 
disc = disc, 
54910  862 
prems = maps (s_not_conj o #prems) disc_eqns, 
863 
auto_gen = true, 

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

864 
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

865 
code_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt > the_default NONE, 
54959
30ded82ff806
fixed 'disc_iff' tactic in the case where different equations use different variable names for the function arguments
blanchet
parents:
54958
diff
changeset

866 
eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt > the_default 100000 (*###*), 
54910  867 
user_eqn = undef_const}; 
868 
in 

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

870 
end 

871 
end; 

53720  872 

54243  873 
fun find_corec_calls ctxt has_call basic_ctr_specs ({ctr, sel, rhs_term, ...} : coeqn_data_sel) = 
54160  874 
let 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

875 
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

876 
> find_index (curry (op =) sel) o #sels o the; 
54970
891141de5672
only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents:
54969
diff
changeset

877 
fun find t = if has_call t then snd (fold_rev_let_if_case ctxt (K cons) [] t []) else []; 
54160  878 
in 
879 
find rhs_term 

880 
> K > nth_map sel_no > AList.map_entry (op =) ctr 

881 
end; 

882 

54900  883 
fun applied_fun_of fun_name fun_T fun_args = 
884 
list_comb (Free (fun_name, fun_T), map Bound (length fun_args  1 downto 0)); 

885 

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

886 
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

887 
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

888 

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

889 
fun add_primcorec_ursive tac_opt 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

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

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

892 

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

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

895 

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

896 
val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, HOLogic.typeS)) (bs ~~ arg_Ts) of 
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

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

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

899 

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

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

901 

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

902 
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

903 
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

904 

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

907 
val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes > member (op =)); 

908 
val eqns_data = 

54948  909 
fold_map2 (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss) (tag_list 0 (map snd specs)) 
54926
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

910 
of_specs_opt [] 
54160  911 
> flat o fst; 
912 

913 
val callssss = 

914 
map_filter (try (fn Sel x => x)) eqns_data 

915 
> partition_eq ((op =) o pairself #fun_name) 

916 
> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names 

54161  917 
> map (flat o snd) 
54243  918 
> map2 (fold o find_corec_calls lthy has_call) basic_ctr_specss 
54160  919 
> map2 (curry (op >)) (map (map (fn {ctr, sels, ...} => 
920 
(ctr, map (K []) sels))) basic_ctr_specss); 

921 

922 
(* 

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

924 
*) 

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

925 

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

926 
val ((n2m, corec_specs', _, coinduct_thm, strong_coinduct_thm, coinduct_thms, 
53797  927 
strong_coinduct_thms), lthy') = 
53794  928 
corec_specs_of bs arg_Ts res_Ts (get_indices fixes) callssss lthy; 
54948  929 
val corec_specs = take actual_nn corec_specs'; 
54178  930 
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

931 

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

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

935 
> map (sort ((op <) o pairself #ctr_no > make_ord) o flat o snd); 
53720  936 
val _ = disc_eqnss' > map (fn x => 
937 
let val d = duplicates ((op =) o pairself #ctr_no) x in null d 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

938 
primcorec_error_eqns "excess discriminator formula in definition" 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

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

940 

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

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

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

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

945 

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

947 
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

948 
disc_eqnss'; 
54835  949 
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

950 
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

951 

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

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

953 
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

954 
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

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

956 
tac_opt; 
53822  957 

53856  958 
(* 
53822  959 
val _ = tracing ("exclusiveness properties:\n \<cdot> " ^ 
54835  960 
space_implode "\n \<cdot> " (maps (map (Syntax.string_of_term lthy o snd)) excludess')); 
53856  961 
*) 
53822  962 

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

963 
val excludess'' = map2 (fn sequential => map (fn (idx, goal) => 
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

964 
(idx, (Option.map (Goal.prove_sorry lthy [] [] goal #> Thm.close_derivation) 
54902
a9291e4d2366
internally allow different values for 'sequential' for different constructors
blanchet
parents:
54901
diff
changeset

965 
(exclude_tac sequential idx), goal)))) 
a9291e4d2366
internally allow different values for 'sequential' for different constructors
blanchet
parents:
54901
diff
changeset

966 
sequentials excludess'; 
54835  967 
val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) excludess''; 
968 
val (goal_idxss, goalss') = excludess'' 

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

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

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

971 

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

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

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

975 
disc_eqnss; 
54844  976 

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

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

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

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

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

982 
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

983 

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

984 
fun map_prove_with_tac tac = 
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

985 
map (fn goal => Goal.prove_sorry lthy [] [] goal tac > Thm.close_derivation); 
54905
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54904
diff
changeset

986 

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

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

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

990 
> list_all_fun_args [] 
54903
c664bd02bf94
internally allow different values for 'exhaustive' for different constructors
blanchet
parents:
54902
diff
changeset

991 
val nchotomy_taut_thmss = 
54972
5747fdd4ad3b
fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents:
54970
diff
changeset

992 
map3 (fn {disc_exhausts, ...} => fn syntactic_exhaustive => 
5747fdd4ad3b
fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents:
54970
diff
changeset

993 
if syntactic_exhaustive then 
5747fdd4ad3b
fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents:
54970
diff
changeset

994 
map_prove_with_tac (fn {context = ctxt, ...} => 
5747fdd4ad3b
fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents:
54970
diff
changeset

995 
mk_primcorec_nchotomy_tac ctxt disc_exhausts) 
5747fdd4ad3b
fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents:
54970
diff
changeset

996 
else 
5747fdd4ad3b
fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents:
54970
diff
changeset

997 
(case tac_opt of 
5747fdd4ad3b
fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents:
54970
diff
changeset

998 
SOME tac => map_prove_with_tac tac 
5747fdd4ad3b
fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents:
54970
diff
changeset

999 
 NONE => K [])) 
54924  1000 
corec_specs syntactic_exhaustives nchotomy_goalss; 
54903
c664bd02bf94
internally allow different values for 'exhaustive' for different constructors
blanchet
parents:
54902
diff
changeset

1001 
val goalss = goalss' 
54926
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

1002 
> (if is_none tac_opt then 
54905
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54904
diff
changeset

1003 
append (map2 (fn true => K []  false => map (rpair [])) syntactic_exhaustives 
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54904
diff
changeset

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

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

1006 
I); 
54844  1007 

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

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

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

1011 

54972
5747fdd4ad3b
fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents:
54970
diff
changeset

1012 
val (nchotomy_thmss, exclude_thmss) = 
5747fdd4ad3b
fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents:
54970
diff
changeset

1013 
if is_none tac_opt then 
5747fdd4ad3b
fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents:
54970
diff
changeset

1014 
(map2 append (take actual_nn thmss'') nchotomy_taut_thmss, drop actual_nn thmss'') 
5747fdd4ad3b
fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents:
54970
diff
changeset

1015 
else 
5747fdd4ad3b
fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents:
54970
diff
changeset

1016 
(nchotomy_taut_thmss, thmss''); 
54613  1017 

54927
a5a2598f0651
proper name generation to avoid clash with 'P' in user specification
blanchet
parents:
54926
diff
changeset

1018 
val ps = 
a5a2598f0651
proper name generation to avoid clash with 'P' in user specification
blanchet
parents:
54926
diff
changeset

1019 
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

1020 

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

1021 
val exhaust_thmss = 
c664bd02bf94
internally allow different values for 'exhaustive' for different constructors
blanchet
parents:
54902
diff
changeset

1022 
map2 (fn false => K [] 
54921
862c36b6e57c
avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents:
54917
diff
changeset

1023 
 true => fn disc_eqns as {fun_args, ...} :: _ => 
862c36b6e57c
avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents:
54917
diff
changeset

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

1025 
val p = Bound (length fun_args); 
862c36b6e57c
avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents:
54917
diff
changeset

1026 
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

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

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

1029 
end) 
54904  1030 
de_facto_exhaustives disc_eqnss 
54927
a5a2598f0651
proper name generation to avoid clash with 'P' in user specification
blanchet
parents:
54926
diff
changeset

1031 
> list_all_fun_args ps 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

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

1033 
 [nchotomy_thm] => fn [goal] => 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

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

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

1036 
> K > Goal.prove_sorry lthy [] [] goal 
54903
c664bd02bf94
internally allow different values for 'exhaustive' for different constructors
blanchet
parents:
54902
diff
changeset

1037 
> Thm.close_derivation]) 
c664bd02bf94
internally allow different values for 'exhaustive' for different constructors
blanchet
parents:
54902
diff
changeset

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

1039 
val nontriv_exhaust_thmss = map (filter_out is_trivial_implies) exhaust_thmss; 
54844  1040 

54835  1041 
val excludess' = map (op ~~) (goal_idxss ~~ exclude_thmss); 
1042 
fun mk_excludesss excludes n = 

1043 
(excludes, map (fn k => replicate k [TrueI] @ replicate (n  k) []) (0 upto n  1)) 

53822  1044 
> fold (fn ((c, c', _), thm) => nth_map c (nth_map c' (K [thm]))); 
54835  1045 
val excludessss = (excludess' ~~ taut_thmss > map (op @), fun_names ~~ corec_specs) 
1046 
> map2 (fn excludes => fn (_, {ctr_specs, ...}) => 

1047 
mk_excludesss excludes (length ctr_specs)); 

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

1048 

54835  1049 
fun prove_disc ({ctr_specs, ...} : corec_spec) excludesss 
54948  1050 
({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

1051 
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

1052 
[] 
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

1053 
else 
53720  1054 
let 
54900  1055 
val {disc, disc_corec, ...} = nth ctr_specs ctr_no; 
53720  1056 
val k = 1 + ctr_no; 
1057 
val m = length prems; 

54900  1058 
val goal = 
1059 
applied_fun_of fun_name fun_T fun_args 

1060 
> curry betapply disc 

53720  1061 
> HOLogic.mk_Trueprop 
1062 
> curry Logic.list_implies (map HOLogic.mk_Trueprop prems) 

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

1064 
in 

54900  1065 
if prems = [@{term False}] then 
1066 
[] 

1067 
else 

1068 
mk_primcorec_disc_tac lthy def_thms disc_corec k m excludesss 

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

1069 
> K > Goal.prove_sorry lthy [] [] goal 
54900  1070 
> Thm.close_derivation 
1071 
> pair (#disc (nth ctr_specs ctr_no)) 

54948  1072 
> pair eqn_pos 
54900  1073 
> single 
53720  1074 
end; 
1075 

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

1076 
fun prove_sel ({nested_maps, nested_map_idents, nested_map_comps, ctr_specs, ...} 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

1077 
: corec_spec) (disc_eqns : coeqn_data_disc list) excludesss 
54948  1078 
({fun_name, fun_T, fun_args, ctr, sel, rhs_term, eqn_pos, ...} : coeqn_data_sel) = 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

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

1080 
val SOME ctr_spec = find_first (curry (op =) ctr o #ctr) ctr_specs; 
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

1081 
val ctr_no = find_index (curry (op =) ctr o #ctr) ctr_specs; 
54067  1082 
val prems = the_default (maps (s_not_conj o #prems) disc_eqns) 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

1083 
(find_first (curry (op =) ctr_no o #ctr_no) disc_eqns > Option.map #prems); 
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

1084 
val sel_corec = find_index (curry (op =) sel) (#sels ctr_spec) 
53720  1085 
> nth (#sel_corecs ctr_spec); 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

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

1087 
val m = length prems; 
54900  1088 
val goal = 
1089 
applied_fun_of fun_name fun_T fun_args 

53720  1090 
> curry betapply sel 
1091 
> rpair (abstract (List.rev fun_args) rhs_term) 

1092 
> HOLogic.mk_Trueprop o HOLogic.mk_eq 

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

1093 
> curry Logic.list_implies (map HOLogic.mk_Trueprop prems) 
53720  1094 
> curry Logic.list_all (map dest_Free fun_args); 
53925  1095 
val (distincts, _, sel_splits, sel_split_asms) = case_thms_of_term lthy [] rhs_term; 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

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

1097 
mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_maps 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

1098 
nested_map_idents nested_map_comps sel_corec k m excludesss 
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

1099 
> K > Goal.prove_sorry lthy [] [] goal 
54176  1100 
> Thm.close_derivation 
53720  1101 
> pair sel 
54948  1102 
> pair eqn_pos 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

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

1104 

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

1105 
fun prove_ctr disc_alist sel_alist (disc_eqns : coeqn_data_disc list) 
67487a607ce2
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents:
54145
diff
changeset

1106 
(sel_eqns : coeqn_data_sel list) ({ctr, disc, sels, collapse, ...} : corec_ctr_spec) = 
54097
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

1107 
(* don't try to prove theorems when some sel_eqns are missing *) 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

1108 
if not (exists (curry (op =) ctr o #ctr) disc_eqns) 
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

1109 
andalso not (exists (curry (op =) ctr o #ctr) sel_eqns) 
54097
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

1110 
orelse 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

1111 
filter (curry (op =) ctr o #ctr) sel_eqns 
53720  1112 
> fst o finds ((op =) o apsnd #sel) sels 
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

1113 
> exists (null o snd) 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

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

1115 
else 
53720  1116 
let 
54948  1117 
val (fun_name, fun_T, fun_args, prems, rhs_opt, eqn_pos) = 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

1118 
(find_first (curry (op =) ctr o #ctr) disc_eqns, 
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

1119 
find_first (curry (op =) ctr o #ctr) sel_eqns) 
54097
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

1120 
>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #prems x, 
54948  1121 
#ctr_rhs_opt x, #eqn_pos x)) 
1122 
> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, [], #ctr_rhs_opt x, 

1123 
#eqn_pos x)) 

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

1124 
> the o merge_options; 
53720  1125 
val m = length prems; 
54900  1126 
val goal = 
54926
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

1127 
(case rhs_opt of 
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

1128 
SOME rhs => rhs 
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

1129 
 NONE => 
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

1130 
filter (curry (op =) ctr o #ctr) sel_eqns 
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

1131 
> fst o finds ((op =) o apsnd #sel) sels 
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

1132 
> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x)) #> abstract) 
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

1133 
> curry list_comb ctr) 
54900  1134 
> curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args) 
53720  1135 
> curry Logic.list_implies (map HOLogic.mk_Trueprop prems) 
1136 
> curry Logic.list_all (map dest_Free fun_args); 

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

1137 
val disc_thm_opt = AList.lookup (op =) disc_alist disc; 
53791  1138 
val sel_thms = map snd (filter (member (op =) sels o fst) sel_alist); 
53720  1139 
in 
54097
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

1140 
if prems = [@{term False}] then [] else 
54954  1141 
mk_primcorec_ctr_tac lthy m collapse disc_thm_opt sel_thms 
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

1142 
> K > Goal.prove_sorry lthy [] [] goal 
54176  1143 
> Thm.close_derivation 
54097
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

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

1146 
> single 
53876  1147 
end; 
53720  1148 

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

1149 
fun prove_code exhaustive disc_eqns sel_eqns nchotomys ctr_alist ctr_specs = 
54098  1150 
let 
54926
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

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

1152 
(find_first (member (op =) (map #ctr ctr_specs) o #ctr) disc_eqns, 
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

1153 
find_first (member (op =) (map #ctr ctr_specs) o #ctr) sel_eqns) 
54926
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

1154 
>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #code_rhs_opt x)) 
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

1155 
> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #code_rhs_opt x)) 
54591
c822230fd22b
prevent exception when equations for a function are missing;
panny
parents:
54279
diff
changeset

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

1157 
in 
54926 