src/HOL/Codatatype/BNF_LFP.thy
author blanchet
Wed, 12 Sep 2012 05:21:47 +0200
changeset 49309 f20b24214ac2
parent 49308 6190b701e4f4
child 49312 c874ff5658dc
permissions -rw-r--r--
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/Codatatype/BNF_LFP.thy
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     2
    Author:     Dmitriy Traytel, TU Muenchen
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     3
    Copyright   2012
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     4
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     5
Least fixed point operation on bounded natural functors.
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     6
*)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     7
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     8
header {* Least Fixed Point Operation on Bounded Natural Functors *}
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     9
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    10
theory BNF_LFP
49308
6190b701e4f4 reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
blanchet
parents: 49074
diff changeset
    11
imports BNF_FP
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    12
keywords
49308
6190b701e4f4 reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
blanchet
parents: 49074
diff changeset
    13
  "data_raw" :: thy_decl and
6190b701e4f4 reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
blanchet
parents: 49074
diff changeset
    14
  "data" :: thy_decl
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    15
begin
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    16
49309
f20b24214ac2 split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents: 49308
diff changeset
    17
ML_file "Tools/bnf_lfp_util.ML"
f20b24214ac2 split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents: 49308
diff changeset
    18
ML_file "Tools/bnf_lfp_tactics.ML"
f20b24214ac2 split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents: 49308
diff changeset
    19
ML_file "Tools/bnf_lfp.ML"
f20b24214ac2 split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents: 49308
diff changeset
    20
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    21
end