# HG changeset patch # User blanchet # Date 1346666061 -7200 # Node ID d8af889dcbe31e3bb974d28e1947f1e2ddca21f3 # Parent 88fe93ae61cf202489a5be53ccf83c7fce3d1907 renamed three BNF/(co)datatype-related commands diff -r 88fe93ae61cf -r d8af889dcbe3 etc/isar-keywords.el --- a/etc/isar-keywords.el Mon Sep 03 11:30:29 2012 +0200 +++ b/etc/isar-keywords.el Mon Sep 03 11:54:21 2012 +0200 @@ -32,10 +32,7 @@ "axiomatization" "axioms" "back" - "bnf_codata" - "bnf_data" "bnf_def" - "bnf_sugar" "boogie_end" "boogie_open" "boogie_status" @@ -50,6 +47,7 @@ "class_deps" "classes" "classrel" + "codata_raw" "code_abort" "code_class" "code_const" @@ -71,6 +69,7 @@ "context" "corollary" "cpodef" + "data_raw" "datatype" "declaration" "declare" @@ -294,6 +293,7 @@ "values" "welcome" "with" + "wrap_data" "write" "{" "}")) @@ -469,14 +469,13 @@ "attribute_setup" "axiomatization" "axioms" - "bnf_codata" - "bnf_data" "boogie_end" "boogie_open" "bundle" "class" "classes" "classrel" + "codata_raw" "code_abort" "code_class" "code_const" @@ -492,6 +491,7 @@ "coinductive_set" "consts" "context" + "data_raw" "datatype" "declaration" "declare" @@ -577,7 +577,6 @@ (defconst isar-keywords-theory-goal '("ax_specification" "bnf_def" - "bnf_sugar" "boogie_vc" "code_pred" "corollary" @@ -605,7 +604,8 @@ "sublocale" "termination" "theorem" - "typedef")) + "typedef" + "wrap_data")) (defconst isar-keywords-qed '("\\." diff -r 88fe93ae61cf -r d8af889dcbe3 src/HOL/Codatatype/BNF_GFP.thy --- a/src/HOL/Codatatype/BNF_GFP.thy Mon Sep 03 11:30:29 2012 +0200 +++ b/src/HOL/Codatatype/BNF_GFP.thy Mon Sep 03 11:54:21 2012 +0200 @@ -10,7 +10,7 @@ theory BNF_GFP imports BNF_Comp keywords - "bnf_codata" :: thy_decl + "codata_raw" :: thy_decl uses "Tools/bnf_gfp_util.ML" "Tools/bnf_gfp_tactics.ML" diff -r 88fe93ae61cf -r d8af889dcbe3 src/HOL/Codatatype/BNF_LFP.thy --- a/src/HOL/Codatatype/BNF_LFP.thy Mon Sep 03 11:30:29 2012 +0200 +++ b/src/HOL/Codatatype/BNF_LFP.thy Mon Sep 03 11:54:21 2012 +0200 @@ -10,7 +10,7 @@ theory BNF_LFP imports BNF_Comp keywords - "bnf_data" :: thy_decl + "data_raw" :: thy_decl uses "Tools/bnf_lfp_util.ML" "Tools/bnf_lfp_tactics.ML" diff -r 88fe93ae61cf -r d8af889dcbe3 src/HOL/Codatatype/Codatatype.thy --- a/src/HOL/Codatatype/Codatatype.thy Mon Sep 03 11:30:29 2012 +0200 +++ b/src/HOL/Codatatype/Codatatype.thy Mon Sep 03 11:54:21 2012 +0200 @@ -12,10 +12,10 @@ theory Codatatype imports BNF_LFP BNF_GFP keywords - "bnf_sugar" :: thy_goal -uses - "Tools/bnf_sugar_tactics.ML" - "Tools/bnf_sugar.ML" + "wrap_data" :: thy_goal +usesy + "Tools/bnf_wrap_tactics.ML" + "Tools/bnf_wrap.ML" begin end diff -r 88fe93ae61cf -r d8af889dcbe3 src/HOL/Codatatype/Examples/HFset.thy --- a/src/HOL/Codatatype/Examples/HFset.thy Mon Sep 03 11:30:29 2012 +0200 +++ b/src/HOL/Codatatype/Examples/HFset.thy Mon Sep 03 11:54:21 2012 +0200 @@ -14,7 +14,7 @@ section {* Datatype definition *} -bnf_data hfset: 'hfset = "'hfset fset" +data_raw hfset: 'hfset = "'hfset fset" section {* Customization of terms *} diff -r 88fe93ae61cf -r d8af889dcbe3 src/HOL/Codatatype/Examples/Lambda_Term.thy --- a/src/HOL/Codatatype/Examples/Lambda_Term.thy Mon Sep 03 11:30:29 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Lambda_Term.thy Mon Sep 03 11:54:21 2012 +0200 @@ -15,7 +15,7 @@ section {* Datatype definition *} -bnf_data trm: 'trm = "'a + 'trm \ 'trm + 'a \ 'trm + ('a \ 'trm) fset \ 'trm" +data_raw trm: 'trm = "'a + 'trm \ 'trm + 'a \ 'trm + ('a \ 'trm) fset \ 'trm" section {* Customization of terms *} diff -r 88fe93ae61cf -r d8af889dcbe3 src/HOL/Codatatype/Examples/ListF.thy --- a/src/HOL/Codatatype/Examples/ListF.thy Mon Sep 03 11:30:29 2012 +0200 +++ b/src/HOL/Codatatype/Examples/ListF.thy Mon Sep 03 11:54:21 2012 +0200 @@ -12,7 +12,7 @@ imports "../Codatatype" begin -bnf_data listF: 'list = "unit + 'a \ 'list" +data_raw listF: 'list = "unit + 'a \ 'list" definition "NilF = listF_fld (Inl ())" definition "Conss a as \ listF_fld (Inr (a, as))" diff -r 88fe93ae61cf -r d8af889dcbe3 src/HOL/Codatatype/Examples/Misc_Codata.thy --- a/src/HOL/Codatatype/Examples/Misc_Codata.thy Mon Sep 03 11:30:29 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Misc_Codata.thy Mon Sep 03 11:54:21 2012 +0200 @@ -16,33 +16,33 @@ ML {* PolyML.fullGC (); *} -bnf_codata simple: 'a = "unit + unit + unit + unit" +codata_raw simple: 'a = "unit + unit + unit + unit" -bnf_codata stream: 's = "'a \ 's" +codata_raw stream: 's = "'a \ 's" -bnf_codata llist: 'llist = "unit + 'a \ 'llist" +codata_raw llist: 'llist = "unit + 'a \ 'llist" -bnf_codata some_passive: 'a = "'a + 'b + 'c + 'd + 'e" +codata_raw some_passive: 'a = "'a + 'b + 'c + 'd + 'e" (* ('a, 'b1, 'b2) F1 = 'a * 'b1 + 'a * 'b2 ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2 *) -bnf_codata F1: 'b1 = "'a \ 'b1 + 'a \ 'b2" +codata_raw F1: 'b1 = "'a \ 'b1 + 'a \ 'b2" and F2: 'b2 = "unit + 'b1 * 'b2" -bnf_codata EXPR: 'E = "'T + 'T \ 'E" +codata_raw EXPR: 'E = "'T + 'T \ 'E" and TERM: 'T = "'F + 'F \ 'T" and FACTOR: 'F = "'a + 'b + 'E" -bnf_codata llambda: +codata_raw llambda: 'trm = "string + 'trm \ 'trm + string \ 'trm + (string \ 'trm) fset \ 'trm" -bnf_codata par_llambda: +codata_raw par_llambda: 'trm = "'a + 'trm \ 'trm + 'a \ 'trm + @@ -53,29 +53,29 @@ 'a forest = Nil | Cons of 'a tree * 'a forest ('c = unit + 'b * 'c) *) -bnf_codata tree: 'tree = "unit + 'a \ 'forest" +codata_raw tree: 'tree = "unit + 'a \ 'forest" and forest: 'forest = "unit + 'tree \ 'forest" -bnf_codata CPS: 'a = "'b + 'b \ 'a" +codata_raw CPS: 'a = "'b + 'b \ 'a" -bnf_codata fun_rhs: 'a = "'b1 \ 'b2 \ 'b3 \ 'b4 \ 'b5 \ 'b6 \ 'b7 \ 'b8 \ 'b9 \ 'a" +codata_raw fun_rhs: 'a = "'b1 \ 'b2 \ 'b3 \ 'b4 \ 'b5 \ 'b6 \ 'b7 \ 'b8 \ 'b9 \ 'a" -bnf_codata fun_rhs': 'a = "'b1 \ 'b2 \ 'b3 \ 'b4 \ 'b5 \ 'b6 \ 'b7 \ 'b8 \ 'b9 \ 'b10 \ +codata_raw fun_rhs': 'a = "'b1 \ 'b2 \ 'b3 \ 'b4 \ 'b5 \ 'b6 \ 'b7 \ 'b8 \ 'b9 \ 'b10 \ 'b11 \ 'b12 \ 'b13 \ 'b14 \ 'b15 \ 'b16 \ 'b17 \ 'b18 \ 'b19 \ 'b20 \ 'a" -bnf_codata some_killing: 'a = "'b \ 'd \ ('a + 'c)" +codata_raw some_killing: 'a = "'b \ 'd \ ('a + 'c)" and in_here: 'c = "'d \ 'b + 'e" -bnf_codata some_killing': 'a = "'b \ 'd \ ('a + 'c)" +codata_raw some_killing': 'a = "'b \ 'd \ ('a + 'c)" and in_here': 'c = "'d + 'e" -bnf_codata some_killing'': 'a = "'b \ 'c" +codata_raw some_killing'': 'a = "'b \ 'c" and in_here'': 'c = "'d \ 'b + 'e" -bnf_codata less_killing: 'a = "'b \ 'c" +codata_raw less_killing: 'a = "'b \ 'c" (* SLOW, MEMORY-HUNGRY -bnf_codata K1': 'K1 = "'K2 + 'a list" +codata_raw K1': 'K1 = "'K2 + 'a list" and K2': 'K2 = "'K3 + 'c fset" and K3': 'K3 = "'K3 + 'K4 + 'K4 \ 'K5" and K4': 'K4 = "'K5 + 'a list list list" diff -r 88fe93ae61cf -r d8af889dcbe3 src/HOL/Codatatype/Examples/Misc_Data.thy --- a/src/HOL/Codatatype/Examples/Misc_Data.thy Mon Sep 03 11:30:29 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Misc_Data.thy Mon Sep 03 11:54:21 2012 +0200 @@ -16,19 +16,19 @@ ML {* PolyML.fullGC (); *} -bnf_data simple: 'a = "unit + unit + unit + unit" +data_raw simple: 'a = "unit + unit + unit + unit" -bnf_data mylist: 'list = "unit + 'a \ 'list" +data_raw mylist: 'list = "unit + 'a \ 'list" -bnf_data some_passive: 'a = "'a + 'b + 'c + 'd + 'e" +data_raw some_passive: 'a = "'a + 'b + 'c + 'd + 'e" -bnf_data lambda: +data_raw lambda: 'trm = "string + 'trm \ 'trm + string \ 'trm + (string \ 'trm) fset \ 'trm" -bnf_data par_lambda: +data_raw par_lambda: 'trm = "'a + 'trm \ 'trm + 'a \ 'trm + @@ -39,7 +39,7 @@ ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2 *) -bnf_data F1: 'b1 = "'a \ 'b1 + 'a \ 'b2" +data_raw F1: 'b1 = "'a \ 'b1 + 'a \ 'b2" and F2: 'b2 = "unit + 'b1 * 'b2" (* @@ -47,7 +47,7 @@ 'a forest = Nil | Cons of 'a tree * 'a forest ('c = unit + 'b * 'c) *) -bnf_data tree: 'tree = "unit + 'a \ 'forest" +data_raw tree: 'tree = "unit + 'a \ 'forest" and forest: 'forest = "unit + 'tree \ 'forest" (* @@ -55,7 +55,7 @@ ' a branch = Branch of 'a * 'a tree ('c = 'a * 'b) *) -bnf_data tree': 'tree = "unit + 'branch \ 'branch" +data_raw tree': 'tree = "unit + 'branch \ 'branch" and branch: 'branch = "'a \ 'tree" (* @@ -64,54 +64,54 @@ factor = C 'a | V 'b | Paren exp ('e = 'a + 'b + 'c) *) -bnf_data EXPR: 'E = "'T + 'T \ 'E" +data_raw EXPR: 'E = "'T + 'T \ 'E" and TERM: 'T = "'F + 'F \ 'T" and FACTOR: 'F = "'a + 'b + 'E" -bnf_data some_killing: 'a = "'b \ 'd \ ('a + 'c)" +data_raw some_killing: 'a = "'b \ 'd \ ('a + 'c)" and in_here: 'c = "'d \ 'b + 'e" -bnf_data nofail1: 'a = "'a \ 'b + 'b" -bnf_data nofail2: 'a = "('a \ 'b \ 'a \ 'b) list" -bnf_data nofail3: 'a = "'b \ ('a \ 'b \ 'a \ 'b) fset" -bnf_data nofail4: 'a = "('a \ ('a \ 'b \ 'a \ 'b) fset) list" +data_raw nofail1: 'a = "'a \ 'b + 'b" +data_raw nofail2: 'a = "('a \ 'b \ 'a \ 'b) list" +data_raw nofail3: 'a = "'b \ ('a \ 'b \ 'a \ 'b) fset" +data_raw nofail4: 'a = "('a \ ('a \ 'b \ 'a \ 'b) fset) list" (* -bnf_data fail: 'a = "'a \ 'b \ 'a \ 'b list" -bnf_data fail: 'a = "'a \ 'b \ 'a \ 'b" -bnf_data fail: 'a = "'a \ 'b + 'a" -bnf_data fail: 'a = "'a \ 'b" +data_raw fail: 'a = "'a \ 'b \ 'a \ 'b list" +data_raw fail: 'a = "'a \ 'b \ 'a \ 'b" +data_raw fail: 'a = "'a \ 'b + 'a" +data_raw fail: 'a = "'a \ 'b" *) -bnf_data L1: 'L1 = "'L2 list" +data_raw L1: 'L1 = "'L2 list" and L2: 'L2 = "'L1 fset + 'L2" -bnf_data K1: 'K1 = "'K2" +data_raw K1: 'K1 = "'K2" and K2: 'K2 = "'K3" and K3: 'K3 = "'K1 list" -bnf_data t1: 't1 = "'t3 + 't2" +data_raw t1: 't1 = "'t3 + 't2" and t2: 't2 = "'t1" and t3: 't3 = "unit" -bnf_data t1': 't1 = "'t2 + 't3" +data_raw t1': 't1 = "'t2 + 't3" and t2': 't2 = "'t1" and t3': 't3 = "unit" (* -bnf_data fail1: 'L1 = "'L2" +data_raw fail1: 'L1 = "'L2" and fail2: 'L2 = "'L3" and fail2: 'L3 = "'L1" -bnf_data fail1: 'L1 = "'L2 list \ 'L2" +data_raw fail1: 'L1 = "'L2 list \ 'L2" and fail2: 'L2 = "'L2 fset \ 'L3" and fail2: 'L3 = "'L1" -bnf_data fail1: 'L1 = "'L2 list \ 'L2" +data_raw fail1: 'L1 = "'L2 list \ 'L2" and fail2: 'L2 = "'L1 fset \ 'L1" *) (* SLOW -bnf_data K1': 'K1 = "'K2 + 'a list" +data_raw K1': 'K1 = "'K2 + 'a list" and K2': 'K2 = "'K3 + 'c fset" and K3': 'K3 = "'K3 + 'K4 + 'K4 \ 'K5" and K4': 'K4 = "'K5 + 'a list list list" @@ -132,23 +132,23 @@ *) (* fail: -bnf_data t1: 't1 = "'t2 * 't3 + 't2 * 't4" +data_raw t1: 't1 = "'t2 * 't3 + 't2 * 't4" and t2: 't2 = "unit" and t3: 't3 = 't4 and t4: 't4 = 't1 *) -bnf_data k1: 'k1 = "'k2 * 'k3 + 'k2 * 'k4" +data_raw k1: 'k1 = "'k2 * 'k3 + 'k2 * 'k4" and k2: 'k2 = unit and k3: 'k3 = 'k4 and k4: 'k4 = unit -bnf_data tt1: 'tt1 = "'tt3 * 'tt2 + 'tt2 * 'tt4" +data_raw tt1: 'tt1 = "'tt3 * 'tt2 + 'tt2 * 'tt4" and tt2: 'tt2 = unit and tt3: 'tt3 = 'tt1 and tt4: 'tt4 = unit (* SLOW -bnf_data s1: 's1 = "'s2 * 's3 * 's4 + 's3 + 's2 * 's6 + 's4 * 's2 + 's2 * 's2" +data_raw s1: 's1 = "'s2 * 's3 * 's4 + 's3 + 's2 * 's6 + 's4 * 's2 + 's2 * 's2" and s2: 's2 = "'s7 * 's5 + 's5 * 's4 * 's6" and s3: 's3 = "'s1 * 's7 * 's2 + 's3 * 's3 + 's4 * 's5" and s4: 's4 = 's5 diff -r 88fe93ae61cf -r d8af889dcbe3 src/HOL/Codatatype/Examples/Process.thy --- a/src/HOL/Codatatype/Examples/Process.thy Mon Sep 03 11:30:29 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Process.thy Mon Sep 03 11:54:21 2012 +0200 @@ -11,7 +11,7 @@ imports "../Codatatype" begin -bnf_codata process: 'p = "'a * 'p + 'p * 'p" +codata_raw process: 'p = "'a * 'p + 'p * 'p" (* codatatype 'a process = Action (prefOf :: 'a) (contOf :: 'a process) | Choice (ch1Of :: 'a process) (ch2Of :: 'a process) diff -r 88fe93ae61cf -r d8af889dcbe3 src/HOL/Codatatype/Examples/Stream.thy --- a/src/HOL/Codatatype/Examples/Stream.thy Mon Sep 03 11:30:29 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Stream.thy Mon Sep 03 11:54:21 2012 +0200 @@ -12,7 +12,7 @@ imports TreeFI begin -bnf_codata stream: 's = "'a \ 's" +codata_raw stream: 's = "'a \ 's" (* selectors for streams *) definition "hdd as \ fst (stream_unf as)" diff -r 88fe93ae61cf -r d8af889dcbe3 src/HOL/Codatatype/Examples/TreeFI.thy --- a/src/HOL/Codatatype/Examples/TreeFI.thy Mon Sep 03 11:30:29 2012 +0200 +++ b/src/HOL/Codatatype/Examples/TreeFI.thy Mon Sep 03 11:54:21 2012 +0200 @@ -12,7 +12,7 @@ imports ListF begin -bnf_codata treeFI: 'tree = "'a \ 'tree listF" +codata_raw treeFI: 'tree = "'a \ 'tree listF" lemma treeFIBNF_listF_set[simp]: "treeFIBNF_set2 (i, xs) = listF_set xs" unfolding treeFIBNF_set2_def collect_def[abs_def] prod_set_defs diff -r 88fe93ae61cf -r d8af889dcbe3 src/HOL/Codatatype/Examples/TreeFsetI.thy --- a/src/HOL/Codatatype/Examples/TreeFsetI.thy Mon Sep 03 11:30:29 2012 +0200 +++ b/src/HOL/Codatatype/Examples/TreeFsetI.thy Mon Sep 03 11:54:21 2012 +0200 @@ -15,7 +15,7 @@ definition pair_fun (infixr "\" 50) where "f \ g \ \x. (f x, g x)" -bnf_codata treeFsetI: 't = "'a \ 't fset" +codata_raw treeFsetI: 't = "'a \ 't fset" (* selectors for trees *) definition "lab t \ fst (treeFsetI_unf t)" diff -r 88fe93ae61cf -r d8af889dcbe3 src/HOL/Codatatype/Tools/bnf_gfp.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Mon Sep 03 11:30:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Mon Sep 03 11:54:21 2012 +0200 @@ -2776,7 +2776,7 @@ end; val _ = - Outer_Syntax.local_theory @{command_spec "bnf_codata"} "greatest fixed points for BNF equations" + Outer_Syntax.local_theory @{command_spec "codata_raw"} "greatest fixed points for BNF equations" (Parse.and_list1 ((Parse.binding --| Parse.$$$ ":") -- (Parse.typ --| Parse.$$$ "=" -- Parse.typ)) >> (fp_bnf_cmd bnf_gfp o apsnd split_list o split_list)); diff -r 88fe93ae61cf -r d8af889dcbe3 src/HOL/Codatatype/Tools/bnf_lfp.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Mon Sep 03 11:30:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Mon Sep 03 11:54:21 2012 +0200 @@ -1755,7 +1755,7 @@ end; val _ = - Outer_Syntax.local_theory @{command_spec "bnf_data"} "least fixed points for BNF equations" + Outer_Syntax.local_theory @{command_spec "data_raw"} "least fixed points for BNF equations" (Parse.and_list1 ((Parse.binding --| Parse.$$$ ":") -- (Parse.typ --| Parse.$$$ "=" -- Parse.typ)) >> (fp_bnf_cmd bnf_lfp o apsnd split_list o split_list)); diff -r 88fe93ae61cf -r d8af889dcbe3 src/HOL/Codatatype/Tools/bnf_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_sugar.ML Mon Sep 03 11:30:29 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,420 +0,0 @@ -(* Title: HOL/Codatatype/Tools/bnf_sugar.ML - Author: Jasmin Blanchette, TU Muenchen - Copyright 2012 - -Sugar on top of a BNF. -*) - -signature BNF_SUGAR = -sig -end; - -structure BNF_Sugar : BNF_SUGAR = -struct - -open BNF_Util -open BNF_FP_Util -open BNF_Sugar_Tactics - -val is_N = "is_"; -val un_N = "un_"; -fun mk_un_N 1 1 suf = un_N ^ suf - | mk_un_N _ l suf = un_N ^ suf ^ string_of_int l; - -val case_congN = "case_cong"; -val case_discsN = "case_discs"; -val casesN = "cases"; -val ctr_selsN = "ctr_sels"; -val disc_exclusN = "disc_exclus"; -val disc_exhaustN = "disc_exhaust"; -val discsN = "discs"; -val distinctN = "distinct"; -val selsN = "sels"; -val splitN = "split"; -val split_asmN = "split_asm"; -val weak_case_cong_thmsN = "weak_case_cong"; - -val default_name = @{binding _}; - -fun pad_list x n xs = xs @ replicate (n - length xs) x; - -fun mk_half_pairss' _ [] = [] - | mk_half_pairss' indent (y :: ys) = - indent @ fold_rev (cons o single o pair y) ys (mk_half_pairss' ([] :: indent) ys); - -fun mk_half_pairss ys = mk_half_pairss' [[]] ys; - -val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq; - -fun mk_undef T Ts = Const (@{const_name undefined}, Ts ---> T); - -fun eta_expand_caseof_arg xs f_xs = fold_rev Term.lambda xs f_xs; - -fun name_of_ctr t = - case head_of t of - Const (s, _) => s - | Free (s, _) => s - | _ => error "Cannot extract name of constructor"; - -fun prepare_sugar prep_term ((raw_ctrs, raw_caseof), (raw_disc_names, raw_sel_namess)) - no_defs_lthy = - let - (* TODO: sanity checks on arguments *) - - (* TODO: normalize types of constructors w.r.t. each other *) - - val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs; - val caseof0 = prep_term no_defs_lthy raw_caseof; - - val n = length ctrs0; - val ks = 1 upto n; - - val (T_name, As0) = dest_Type (body_type (fastype_of (hd ctrs0))); - val b = Binding.qualified_name T_name; - - val (As, B) = - no_defs_lthy - |> mk_TFrees (length As0) - ||> the_single o fst o mk_TFrees 1; - - fun mk_ctr Ts ctr = - let val Ts0 = snd (dest_Type (body_type (fastype_of ctr))) in - Term.subst_atomic_types (Ts0 ~~ Ts) ctr - end; - - val T = Type (T_name, As); - val ctrs = map (mk_ctr As) ctrs0; - val ctr_Tss = map (binder_types o fastype_of) ctrs; - - val ms = map length ctr_Tss; - - val disc_names = - pad_list default_name n raw_disc_names - |> map2 (fn ctr => fn disc => - if Binding.eq_name (disc, default_name) then - Binding.name (prefix is_N (Long_Name.base_name (name_of_ctr ctr))) - else - disc) ctrs0; - - val sel_namess = - pad_list [] n raw_sel_namess - |> map3 (fn ctr => fn m => map2 (fn l => fn sel => - if Binding.eq_name (sel, default_name) then - Binding.name (mk_un_N m l (Long_Name.base_name (name_of_ctr ctr))) - else - sel) (1 upto m) o pad_list default_name m) ctrs0 ms; - - fun mk_caseof Ts T = - let val (binders, body) = strip_type (fastype_of caseof0) in - Term.subst_atomic_types ((body, T) :: (snd (dest_Type (List.last binders)) ~~ Ts)) caseof0 - end; - - val caseofB = mk_caseof As B; - val caseofB_Ts = map (fn Ts => Ts ---> B) ctr_Tss; - - fun mk_caseofB_term eta_fs = Term.list_comb (caseofB, eta_fs); - - val (((((((xss, yss), fs), gs), (v, v')), w), (p, p')), names_lthy) = no_defs_lthy |> - mk_Freess "x" ctr_Tss - ||>> mk_Freess "y" ctr_Tss - ||>> mk_Frees "f" caseofB_Ts - ||>> mk_Frees "g" caseofB_Ts - ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "v") T - ||>> yield_singleton (mk_Frees "w") T - ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT; - - val q = Free (fst p', B --> HOLogic.boolT); - - val xctrs = map2 (curry Term.list_comb) ctrs xss; - val yctrs = map2 (curry Term.list_comb) ctrs yss; - - val xfs = map2 (curry Term.list_comb) fs xss; - val xgs = map2 (curry Term.list_comb) gs xss; - - val eta_fs = map2 eta_expand_caseof_arg xss xfs; - val eta_gs = map2 eta_expand_caseof_arg xss xgs; - - val caseofB_fs = Term.list_comb (caseofB, eta_fs); - - val exist_xs_v_eq_ctrs = - map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (v, xctr))) xctrs xss; - - fun mk_sel_caseof_args k xs x T = - map2 (fn Ts => fn i => if i = k then fold_rev Term.lambda xs x else mk_undef T Ts) ctr_Tss ks; - - fun disc_spec b exist_xs_v_eq_ctr = - mk_Trueprop_eq (Free (Binding.name_of b, T --> HOLogic.boolT) $ v, exist_xs_v_eq_ctr); - - fun sel_spec b x xs k = - let val T' = fastype_of x in - mk_Trueprop_eq (Free (Binding.name_of b, T --> T') $ v, - Term.list_comb (mk_caseof As T', mk_sel_caseof_args k xs x T') $ v) - end; - - val (((raw_discs, (_, raw_disc_defs)), (raw_selss, (_, raw_sel_defss))), (lthy', lthy)) = - no_defs_lthy - |> apfst (apsnd split_list o split_list) o fold_map2 (fn b => fn exist_xs_v_eq_ctr => - Specification.definition (SOME (b, NONE, NoSyn), - ((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr))) disc_names exist_xs_v_eq_ctrs - ||>> apfst (apsnd split_list o split_list) o fold_map3 (fn bs => fn xs => fn k => - apfst (apsnd split_list o split_list) o fold_map2 (fn b => fn x => - Specification.definition (SOME (b, NONE, NoSyn), - ((Thm.def_binding b, []), sel_spec b x xs k))) bs xs) sel_namess xss ks - ||> `Local_Theory.restore; - - (*transforms defined frees into consts (and more)*) - val phi = Proof_Context.export_morphism lthy lthy'; - - val disc_defs = map (Morphism.thm phi) raw_disc_defs; - val sel_defss = map (map (Morphism.thm phi)) raw_sel_defss; - - val discs0 = map (Morphism.term phi) raw_discs; - val selss0 = map (map (Morphism.term phi)) raw_selss; - - fun mk_disc_or_sel Ts t = - Term.subst_atomic_types (snd (dest_Type (domain_type (fastype_of t))) ~~ Ts) t; - - val discs = map (mk_disc_or_sel As) discs0; - val selss = map (map (mk_disc_or_sel As)) selss0; - - fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p); - - val goal_exhaust = - let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (v, xctr)]) in - mk_imp_p (map2 mk_prem xctrs xss) - end; - - val goal_injectss = - let - fun mk_goal _ _ [] [] = [] - | mk_goal xctr yctr xs ys = - [mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr), - Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys))]; - in - map4 mk_goal xctrs yctrs xss yss - end; - - val goal_half_distinctss = - map (map (HOLogic.mk_Trueprop o HOLogic.mk_not o HOLogic.mk_eq)) (mk_half_pairss xctrs); - - val goal_cases = map2 (fn xctr => fn xf => mk_Trueprop_eq (caseofB_fs $ xctr, xf)) xctrs xfs; - - val goals = [goal_exhaust] :: goal_injectss @ goal_half_distinctss @ [goal_cases]; - - fun after_qed thmss lthy = - let - val ([exhaust_thm], (inject_thmss, (half_distinct_thmss, [case_thms]))) = - (hd thmss, apsnd (chop (n * n)) (chop n (tl thmss))); - - val exhaust_thm' = - let val Tinst = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As) in - Drule.instantiate' [] [SOME (certify lthy v)] - (Thm.instantiate (Tinst, []) (Drule.zero_var_indexes exhaust_thm)) - end; - - val other_half_distinct_thmss = map (map (fn thm => thm RS not_sym)) half_distinct_thmss; - - val (distinct_thmsss', distinct_thmsss) = - map2 (map2 append) (Library.chop_groups n half_distinct_thmss) - (transpose (Library.chop_groups n other_half_distinct_thmss)) - |> `transpose; - val distinct_thms = interleave (flat half_distinct_thmss) (flat other_half_distinct_thmss); - - val nchotomy_thm = - let - val goal = - HOLogic.mk_Trueprop (HOLogic.mk_all (fst v', snd v', - Library.foldr1 HOLogic.mk_disj exist_xs_v_eq_ctrs)); - in - Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm) - end; - - val sel_thmss = - let - fun mk_thm k xs goal_case case_thm x sel_def = - let - val T = fastype_of x; - val cTs = - map ((fn T' => certifyT lthy (if T' = B then T else T')) o TFree) - (rev (Term.add_tfrees goal_case [])); - val cxs = map (certify lthy) (mk_sel_caseof_args k xs x T); - in - Local_Defs.fold lthy [sel_def] - (Drule.instantiate' (map SOME cTs) (map SOME cxs) case_thm) - end; - fun mk_thms k xs goal_case case_thm sel_defs = - map2 (mk_thm k xs goal_case case_thm) xs sel_defs; - in - map5 mk_thms ks xss goal_cases case_thms sel_defss - end; - - val discD_thms = map (fn def => def RS iffD1) disc_defs; - val discI_thms = - map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms disc_defs; - val not_disc_thms = - map2 (fn m => fn def => funpow m (fn thm => allI RS thm) - (Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) - ms disc_defs; - - val (disc_thmss', disc_thmss) = - let - fun mk_thm discI _ [] = refl RS discI - | mk_thm _ not_disc [distinct] = distinct RS not_disc; - fun mk_thms discI not_disc distinctss = map (mk_thm discI not_disc) distinctss; - in - map3 mk_thms discI_thms not_disc_thms distinct_thmsss' - |> `transpose - end; - - val disc_exclus_thms = - let - fun mk_goal ((_, disc), (_, disc')) = - Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v), - HOLogic.mk_Trueprop (HOLogic.mk_not (disc' $ v)))); - fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac); - - val bundles = ms ~~ discD_thms ~~ discs; - val half_pairss = mk_half_pairss bundles; - - val goal_halvess = map (map mk_goal) half_pairss; - val half_thmss = - map3 (fn [] => K (K []) - | [(((m, discD), _), _)] => fn disc_thm => fn [goal] => - [prove (mk_half_disc_exclus_tac m discD disc_thm) goal]) - half_pairss (flat disc_thmss') goal_halvess; - - val goal_other_halvess = map (map (mk_goal o swap)) half_pairss; - val other_half_thmss = - map2 (map2 (prove o mk_other_half_disc_exclus_tac)) half_thmss goal_other_halvess; - in - interleave (flat half_thmss) (flat other_half_thmss) - end; - - val disc_exhaust_thm = - let - fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (disc $ v)]; - val goal = fold Logic.all [p, v] (mk_imp_p (map mk_prem discs)); - in - Skip_Proof.prove lthy [] [] goal (fn _ => mk_disc_exhaust_tac n exhaust_thm discI_thms) - end; - - val ctr_sel_thms = - let - fun mk_goal ctr disc sels = - Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v), - mk_Trueprop_eq ((null sels ? swap) - (Term.list_comb (ctr, map (fn sel => sel $ v) sels), v)))); - val goals = map3 mk_goal ctrs discs selss; - in - map4 (fn goal => fn m => fn discD => fn sel_thms => - Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => - mk_ctr_sel_tac ctxt m discD sel_thms)) - goals ms discD_thms sel_thmss - end; - - val case_disc_thm = - let - fun mk_core f sels = Term.list_comb (f, map (fn sel => sel $ v) sels); - fun mk_rhs _ [f] [sels] = mk_core f sels - | mk_rhs (disc :: discs) (f :: fs) (sels :: selss) = - Const (@{const_name If}, HOLogic.boolT --> B --> B --> B) $ - (disc $ v) $ mk_core f sels $ mk_rhs discs fs selss; - val goal = mk_Trueprop_eq (caseofB_fs $ v, mk_rhs discs fs selss); - in - Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => - mk_case_disc_tac ctxt exhaust_thm' case_thms disc_thmss' sel_thmss) - |> singleton (Proof_Context.export names_lthy lthy) - end; - - val (case_cong_thm, weak_case_cong_thm) = - let - fun mk_prem xctr xs f g = - fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (w, xctr), - mk_Trueprop_eq (f, g))); - - val v_eq_w = mk_Trueprop_eq (v, w); - val caseof_fs = mk_caseofB_term eta_fs; - val caseof_gs = mk_caseofB_term eta_gs; - - val goal = - Logic.list_implies (v_eq_w :: map4 mk_prem xctrs xss fs gs, - mk_Trueprop_eq (caseof_fs $ v, caseof_gs $ w)); - val goal_weak = - Logic.mk_implies (v_eq_w, mk_Trueprop_eq (caseof_fs $ v, caseof_fs $ w)); - in - (Skip_Proof.prove lthy [] [] goal (fn _ => mk_case_cong_tac exhaust_thm' case_thms), - Skip_Proof.prove lthy [] [] goal_weak (K (etac arg_cong 1))) - |> pairself (singleton (Proof_Context.export names_lthy lthy)) - end; - - val (split_thm, split_asm_thm) = - let - fun mk_conjunct xctr xs f_xs = - list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (v, xctr), q $ f_xs)); - fun mk_disjunct xctr xs f_xs = - list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (v, xctr), - HOLogic.mk_not (q $ f_xs))); - - val lhs = q $ (mk_caseofB_term eta_fs $ v); - - val goal = - mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs)); - val goal_asm = - mk_Trueprop_eq (lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj - (map3 mk_disjunct xctrs xss xfs))); - - val split_thm = - Skip_Proof.prove lthy [] [] goal - (fn _ => mk_split_tac exhaust_thm' case_thms inject_thmss distinct_thmsss) - |> singleton (Proof_Context.export names_lthy lthy) - val split_asm_thm = - Skip_Proof.prove lthy [] [] goal_asm (fn {context = ctxt, ...} => - mk_split_asm_tac ctxt split_thm) - |> singleton (Proof_Context.export names_lthy lthy) - in - (split_thm, split_asm_thm) - end; - - (* TODO: case syntax *) - (* TODO: attributes (simp, case_names, etc.) *) - - val notes = - [(case_congN, [case_cong_thm]), - (case_discsN, [case_disc_thm]), - (casesN, case_thms), - (ctr_selsN, ctr_sel_thms), - (discsN, (flat disc_thmss)), - (disc_exclusN, disc_exclus_thms), - (disc_exhaustN, [disc_exhaust_thm]), - (distinctN, distinct_thms), - (exhaustN, [exhaust_thm]), - (injectN, (flat inject_thmss)), - (nchotomyN, [nchotomy_thm]), - (selsN, (flat sel_thmss)), - (splitN, [split_thm]), - (split_asmN, [split_asm_thm]), - (weak_case_cong_thmsN, [weak_case_cong_thm])] - |> map (fn (thmN, thms) => - ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); - in - lthy |> Local_Theory.notes notes |> snd - end; - in - (goals, after_qed, lthy') - end; - -val parse_bindings = Parse.$$$ "[" |-- Parse.list Parse.binding --| Parse.$$$ "]"; - -val parse_bindingss = Parse.$$$ "[" |-- Parse.list parse_bindings --| Parse.$$$ "]"; - -val bnf_sugar_cmd = (fn (goalss, after_qed, lthy) => - Proof.theorem NONE after_qed (map (map (rpair [])) goalss) lthy) oo - prepare_sugar Syntax.read_term; - -val _ = - Outer_Syntax.local_theory_to_proof @{command_spec "bnf_sugar"} "adds sugar on top of a BNF" - (((Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") -- Parse.term -- - Scan.optional (parse_bindings -- Scan.optional parse_bindingss []) ([], [])) - >> bnf_sugar_cmd); - -end; diff -r 88fe93ae61cf -r d8af889dcbe3 src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML Mon Sep 03 11:30:29 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,93 +0,0 @@ -(* Title: HOL/Codatatype/Tools/bnf_sugar_tactics.ML - Author: Jasmin Blanchette, TU Muenchen - Copyright 2012 - -Tactics for sugar on top of a BNF. -*) - -signature BNF_SUGAR_TACTICS = -sig - val mk_case_cong_tac: thm -> thm list -> tactic - val mk_case_disc_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> tactic - val mk_ctr_sel_tac: Proof.context -> int -> thm -> thm list -> tactic - val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic - val mk_half_disc_exclus_tac: int -> thm -> thm -> tactic - val mk_nchotomy_tac: int -> thm -> tactic - val mk_other_half_disc_exclus_tac: thm -> tactic - val mk_split_tac: thm -> thm list -> thm list list -> thm list list list -> tactic - val mk_split_asm_tac: Proof.context -> thm -> tactic -end; - -structure BNF_Sugar_Tactics : BNF_SUGAR_TACTICS = -struct - -open BNF_Util -open BNF_Tactics -open BNF_FP_Util - -fun triangle _ [] = [] - | triangle k (xs :: xss) = take k xs :: triangle (k + 1) xss - -fun mk_if_P_or_not_P thm = - thm RS @{thm if_not_P} handle THM _ => thm RS @{thm if_P} - -fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms - -fun mk_nchotomy_tac n exhaust = - (rtac allI THEN' rtac exhaust THEN' - EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1; - -fun mk_half_disc_exclus_tac m discD disc'_thm = - (dtac discD THEN' - REPEAT_DETERM_N m o etac exE THEN' - hyp_subst_tac THEN' - rtac disc'_thm) 1; - -fun mk_other_half_disc_exclus_tac half_thm = - (etac @{thm contrapos_pn} THEN' etac half_thm) 1; - -fun mk_disc_exhaust_tac n exhaust discIs = - (rtac exhaust THEN' - EVERY' (map2 (fn k => fn discI => - dtac discI THEN' select_prem_tac n (etac @{thm meta_mp}) k THEN' atac) (1 upto n) discIs)) 1; - -fun mk_ctr_sel_tac ctxt m discD sel_thms = - (dtac discD THEN' - (if m = 0 then - atac - else - REPEAT_DETERM_N m o etac exE THEN' - hyp_subst_tac THEN' - SELECT_GOAL (Local_Defs.unfold_tac ctxt sel_thms) THEN' - rtac refl)) 1; - -fun mk_case_disc_tac ctxt exhaust' case_thms disc_thmss' sel_thmss = - (rtac exhaust' THEN' - EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms => EVERY' [ - hyp_subst_tac THEN' - SELECT_GOAL (Local_Defs.unfold_tac ctxt (if_disc_thms @ sel_thms)) THEN' - rtac case_thm]) case_thms - (map (map mk_if_P_or_not_P) (triangle 1 (map (fst o split_last) disc_thmss'))) sel_thmss)) 1; - -fun mk_case_cong_tac exhaust' case_thms = - (rtac exhaust' THEN' - EVERY' (maps (fn case_thm => [dtac sym, asm_simp_tac (ss_only [case_thm])]) case_thms)) 1; - -val naked_ctxt = Proof_Context.init_global @{theory HOL}; - -fun mk_split_tac exhaust' case_thms injectss distinctsss = - rtac exhaust' 1 THEN - ALLGOALS (fn k => - (hyp_subst_tac THEN' - simp_tac (ss_only (@{thms simp_thms} @ case_thms @ nth injectss (k - 1) @ - flat (nth distinctsss (k - 1))))) k) THEN - ALLGOALS (blast_tac naked_ctxt); - -val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex}; - -fun mk_split_asm_tac ctxt split = - rtac (split RS trans) 1 THEN - Local_Defs.unfold_tac ctxt split_asm_thms THEN - rtac refl 1; - -end; diff -r 88fe93ae61cf -r d8af889dcbe3 src/HOL/Codatatype/Tools/bnf_wrap.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Mon Sep 03 11:54:21 2012 +0200 @@ -0,0 +1,420 @@ +(* Title: HOL/Codatatype/Tools/bnf_wrap.ML + Author: Jasmin Blanchette, TU Muenchen + Copyright 2012 + +Wrapping existing datatypes. +*) + +signature BNF_WRAP = +sig +end; + +structure BNF_Wrap : BNF_WRAP = +struct + +open BNF_Util +open BNF_FP_Util +open BNF_Wrap_Tactics + +val is_N = "is_"; +val un_N = "un_"; +fun mk_un_N 1 1 suf = un_N ^ suf + | mk_un_N _ l suf = un_N ^ suf ^ string_of_int l; + +val case_congN = "case_cong"; +val case_discsN = "case_discs"; +val casesN = "cases"; +val ctr_selsN = "ctr_sels"; +val disc_exclusN = "disc_exclus"; +val disc_exhaustN = "disc_exhaust"; +val discsN = "discs"; +val distinctN = "distinct"; +val selsN = "sels"; +val splitN = "split"; +val split_asmN = "split_asm"; +val weak_case_cong_thmsN = "weak_case_cong"; + +val default_name = @{binding _}; + +fun pad_list x n xs = xs @ replicate (n - length xs) x; + +fun mk_half_pairss' _ [] = [] + | mk_half_pairss' indent (y :: ys) = + indent @ fold_rev (cons o single o pair y) ys (mk_half_pairss' ([] :: indent) ys); + +fun mk_half_pairss ys = mk_half_pairss' [[]] ys; + +val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq; + +fun mk_undef T Ts = Const (@{const_name undefined}, Ts ---> T); + +fun eta_expand_caseof_arg xs f_xs = fold_rev Term.lambda xs f_xs; + +fun name_of_ctr t = + case head_of t of + Const (s, _) => s + | Free (s, _) => s + | _ => error "Cannot extract name of constructor"; + +fun prepare_wrap prep_term ((raw_ctrs, raw_caseof), (raw_disc_names, raw_sel_namess)) + no_defs_lthy = + let + (* TODO: sanity checks on arguments *) + + (* TODO: normalize types of constructors w.r.t. each other *) + + val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs; + val caseof0 = prep_term no_defs_lthy raw_caseof; + + val n = length ctrs0; + val ks = 1 upto n; + + val (T_name, As0) = dest_Type (body_type (fastype_of (hd ctrs0))); + val b = Binding.qualified_name T_name; + + val (As, B) = + no_defs_lthy + |> mk_TFrees (length As0) + ||> the_single o fst o mk_TFrees 1; + + fun mk_ctr Ts ctr = + let val Ts0 = snd (dest_Type (body_type (fastype_of ctr))) in + Term.subst_atomic_types (Ts0 ~~ Ts) ctr + end; + + val T = Type (T_name, As); + val ctrs = map (mk_ctr As) ctrs0; + val ctr_Tss = map (binder_types o fastype_of) ctrs; + + val ms = map length ctr_Tss; + + val disc_names = + pad_list default_name n raw_disc_names + |> map2 (fn ctr => fn disc => + if Binding.eq_name (disc, default_name) then + Binding.name (prefix is_N (Long_Name.base_name (name_of_ctr ctr))) + else + disc) ctrs0; + + val sel_namess = + pad_list [] n raw_sel_namess + |> map3 (fn ctr => fn m => map2 (fn l => fn sel => + if Binding.eq_name (sel, default_name) then + Binding.name (mk_un_N m l (Long_Name.base_name (name_of_ctr ctr))) + else + sel) (1 upto m) o pad_list default_name m) ctrs0 ms; + + fun mk_caseof Ts T = + let val (binders, body) = strip_type (fastype_of caseof0) in + Term.subst_atomic_types ((body, T) :: (snd (dest_Type (List.last binders)) ~~ Ts)) caseof0 + end; + + val caseofB = mk_caseof As B; + val caseofB_Ts = map (fn Ts => Ts ---> B) ctr_Tss; + + fun mk_caseofB_term eta_fs = Term.list_comb (caseofB, eta_fs); + + val (((((((xss, yss), fs), gs), (v, v')), w), (p, p')), names_lthy) = no_defs_lthy |> + mk_Freess "x" ctr_Tss + ||>> mk_Freess "y" ctr_Tss + ||>> mk_Frees "f" caseofB_Ts + ||>> mk_Frees "g" caseofB_Ts + ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "v") T + ||>> yield_singleton (mk_Frees "w") T + ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT; + + val q = Free (fst p', B --> HOLogic.boolT); + + val xctrs = map2 (curry Term.list_comb) ctrs xss; + val yctrs = map2 (curry Term.list_comb) ctrs yss; + + val xfs = map2 (curry Term.list_comb) fs xss; + val xgs = map2 (curry Term.list_comb) gs xss; + + val eta_fs = map2 eta_expand_caseof_arg xss xfs; + val eta_gs = map2 eta_expand_caseof_arg xss xgs; + + val caseofB_fs = Term.list_comb (caseofB, eta_fs); + + val exist_xs_v_eq_ctrs = + map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (v, xctr))) xctrs xss; + + fun mk_sel_caseof_args k xs x T = + map2 (fn Ts => fn i => if i = k then fold_rev Term.lambda xs x else mk_undef T Ts) ctr_Tss ks; + + fun disc_spec b exist_xs_v_eq_ctr = + mk_Trueprop_eq (Free (Binding.name_of b, T --> HOLogic.boolT) $ v, exist_xs_v_eq_ctr); + + fun sel_spec b x xs k = + let val T' = fastype_of x in + mk_Trueprop_eq (Free (Binding.name_of b, T --> T') $ v, + Term.list_comb (mk_caseof As T', mk_sel_caseof_args k xs x T') $ v) + end; + + val (((raw_discs, (_, raw_disc_defs)), (raw_selss, (_, raw_sel_defss))), (lthy', lthy)) = + no_defs_lthy + |> apfst (apsnd split_list o split_list) o fold_map2 (fn b => fn exist_xs_v_eq_ctr => + Specification.definition (SOME (b, NONE, NoSyn), + ((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr))) disc_names exist_xs_v_eq_ctrs + ||>> apfst (apsnd split_list o split_list) o fold_map3 (fn bs => fn xs => fn k => + apfst (apsnd split_list o split_list) o fold_map2 (fn b => fn x => + Specification.definition (SOME (b, NONE, NoSyn), + ((Thm.def_binding b, []), sel_spec b x xs k))) bs xs) sel_namess xss ks + ||> `Local_Theory.restore; + + (*transforms defined frees into consts (and more)*) + val phi = Proof_Context.export_morphism lthy lthy'; + + val disc_defs = map (Morphism.thm phi) raw_disc_defs; + val sel_defss = map (map (Morphism.thm phi)) raw_sel_defss; + + val discs0 = map (Morphism.term phi) raw_discs; + val selss0 = map (map (Morphism.term phi)) raw_selss; + + fun mk_disc_or_sel Ts t = + Term.subst_atomic_types (snd (dest_Type (domain_type (fastype_of t))) ~~ Ts) t; + + val discs = map (mk_disc_or_sel As) discs0; + val selss = map (map (mk_disc_or_sel As)) selss0; + + fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p); + + val goal_exhaust = + let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (v, xctr)]) in + mk_imp_p (map2 mk_prem xctrs xss) + end; + + val goal_injectss = + let + fun mk_goal _ _ [] [] = [] + | mk_goal xctr yctr xs ys = + [mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr), + Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys))]; + in + map4 mk_goal xctrs yctrs xss yss + end; + + val goal_half_distinctss = + map (map (HOLogic.mk_Trueprop o HOLogic.mk_not o HOLogic.mk_eq)) (mk_half_pairss xctrs); + + val goal_cases = map2 (fn xctr => fn xf => mk_Trueprop_eq (caseofB_fs $ xctr, xf)) xctrs xfs; + + val goals = [goal_exhaust] :: goal_injectss @ goal_half_distinctss @ [goal_cases]; + + fun after_qed thmss lthy = + let + val ([exhaust_thm], (inject_thmss, (half_distinct_thmss, [case_thms]))) = + (hd thmss, apsnd (chop (n * n)) (chop n (tl thmss))); + + val exhaust_thm' = + let val Tinst = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As) in + Drule.instantiate' [] [SOME (certify lthy v)] + (Thm.instantiate (Tinst, []) (Drule.zero_var_indexes exhaust_thm)) + end; + + val other_half_distinct_thmss = map (map (fn thm => thm RS not_sym)) half_distinct_thmss; + + val (distinct_thmsss', distinct_thmsss) = + map2 (map2 append) (Library.chop_groups n half_distinct_thmss) + (transpose (Library.chop_groups n other_half_distinct_thmss)) + |> `transpose; + val distinct_thms = interleave (flat half_distinct_thmss) (flat other_half_distinct_thmss); + + val nchotomy_thm = + let + val goal = + HOLogic.mk_Trueprop (HOLogic.mk_all (fst v', snd v', + Library.foldr1 HOLogic.mk_disj exist_xs_v_eq_ctrs)); + in + Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm) + end; + + val sel_thmss = + let + fun mk_thm k xs goal_case case_thm x sel_def = + let + val T = fastype_of x; + val cTs = + map ((fn T' => certifyT lthy (if T' = B then T else T')) o TFree) + (rev (Term.add_tfrees goal_case [])); + val cxs = map (certify lthy) (mk_sel_caseof_args k xs x T); + in + Local_Defs.fold lthy [sel_def] + (Drule.instantiate' (map SOME cTs) (map SOME cxs) case_thm) + end; + fun mk_thms k xs goal_case case_thm sel_defs = + map2 (mk_thm k xs goal_case case_thm) xs sel_defs; + in + map5 mk_thms ks xss goal_cases case_thms sel_defss + end; + + val discD_thms = map (fn def => def RS iffD1) disc_defs; + val discI_thms = + map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms disc_defs; + val not_disc_thms = + map2 (fn m => fn def => funpow m (fn thm => allI RS thm) + (Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) + ms disc_defs; + + val (disc_thmss', disc_thmss) = + let + fun mk_thm discI _ [] = refl RS discI + | mk_thm _ not_disc [distinct] = distinct RS not_disc; + fun mk_thms discI not_disc distinctss = map (mk_thm discI not_disc) distinctss; + in + map3 mk_thms discI_thms not_disc_thms distinct_thmsss' + |> `transpose + end; + + val disc_exclus_thms = + let + fun mk_goal ((_, disc), (_, disc')) = + Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v), + HOLogic.mk_Trueprop (HOLogic.mk_not (disc' $ v)))); + fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac); + + val bundles = ms ~~ discD_thms ~~ discs; + val half_pairss = mk_half_pairss bundles; + + val goal_halvess = map (map mk_goal) half_pairss; + val half_thmss = + map3 (fn [] => K (K []) + | [(((m, discD), _), _)] => fn disc_thm => fn [goal] => + [prove (mk_half_disc_exclus_tac m discD disc_thm) goal]) + half_pairss (flat disc_thmss') goal_halvess; + + val goal_other_halvess = map (map (mk_goal o swap)) half_pairss; + val other_half_thmss = + map2 (map2 (prove o mk_other_half_disc_exclus_tac)) half_thmss goal_other_halvess; + in + interleave (flat half_thmss) (flat other_half_thmss) + end; + + val disc_exhaust_thm = + let + fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (disc $ v)]; + val goal = fold Logic.all [p, v] (mk_imp_p (map mk_prem discs)); + in + Skip_Proof.prove lthy [] [] goal (fn _ => mk_disc_exhaust_tac n exhaust_thm discI_thms) + end; + + val ctr_sel_thms = + let + fun mk_goal ctr disc sels = + Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v), + mk_Trueprop_eq ((null sels ? swap) + (Term.list_comb (ctr, map (fn sel => sel $ v) sels), v)))); + val goals = map3 mk_goal ctrs discs selss; + in + map4 (fn goal => fn m => fn discD => fn sel_thms => + Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => + mk_ctr_sel_tac ctxt m discD sel_thms)) + goals ms discD_thms sel_thmss + end; + + val case_disc_thm = + let + fun mk_core f sels = Term.list_comb (f, map (fn sel => sel $ v) sels); + fun mk_rhs _ [f] [sels] = mk_core f sels + | mk_rhs (disc :: discs) (f :: fs) (sels :: selss) = + Const (@{const_name If}, HOLogic.boolT --> B --> B --> B) $ + (disc $ v) $ mk_core f sels $ mk_rhs discs fs selss; + val goal = mk_Trueprop_eq (caseofB_fs $ v, mk_rhs discs fs selss); + in + Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => + mk_case_disc_tac ctxt exhaust_thm' case_thms disc_thmss' sel_thmss) + |> singleton (Proof_Context.export names_lthy lthy) + end; + + val (case_cong_thm, weak_case_cong_thm) = + let + fun mk_prem xctr xs f g = + fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (w, xctr), + mk_Trueprop_eq (f, g))); + + val v_eq_w = mk_Trueprop_eq (v, w); + val caseof_fs = mk_caseofB_term eta_fs; + val caseof_gs = mk_caseofB_term eta_gs; + + val goal = + Logic.list_implies (v_eq_w :: map4 mk_prem xctrs xss fs gs, + mk_Trueprop_eq (caseof_fs $ v, caseof_gs $ w)); + val goal_weak = + Logic.mk_implies (v_eq_w, mk_Trueprop_eq (caseof_fs $ v, caseof_fs $ w)); + in + (Skip_Proof.prove lthy [] [] goal (fn _ => mk_case_cong_tac exhaust_thm' case_thms), + Skip_Proof.prove lthy [] [] goal_weak (K (etac arg_cong 1))) + |> pairself (singleton (Proof_Context.export names_lthy lthy)) + end; + + val (split_thm, split_asm_thm) = + let + fun mk_conjunct xctr xs f_xs = + list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (v, xctr), q $ f_xs)); + fun mk_disjunct xctr xs f_xs = + list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (v, xctr), + HOLogic.mk_not (q $ f_xs))); + + val lhs = q $ (mk_caseofB_term eta_fs $ v); + + val goal = + mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs)); + val goal_asm = + mk_Trueprop_eq (lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj + (map3 mk_disjunct xctrs xss xfs))); + + val split_thm = + Skip_Proof.prove lthy [] [] goal + (fn _ => mk_split_tac exhaust_thm' case_thms inject_thmss distinct_thmsss) + |> singleton (Proof_Context.export names_lthy lthy) + val split_asm_thm = + Skip_Proof.prove lthy [] [] goal_asm (fn {context = ctxt, ...} => + mk_split_asm_tac ctxt split_thm) + |> singleton (Proof_Context.export names_lthy lthy) + in + (split_thm, split_asm_thm) + end; + + (* TODO: case syntax *) + (* TODO: attributes (simp, case_names, etc.) *) + + val notes = + [(case_congN, [case_cong_thm]), + (case_discsN, [case_disc_thm]), + (casesN, case_thms), + (ctr_selsN, ctr_sel_thms), + (discsN, (flat disc_thmss)), + (disc_exclusN, disc_exclus_thms), + (disc_exhaustN, [disc_exhaust_thm]), + (distinctN, distinct_thms), + (exhaustN, [exhaust_thm]), + (injectN, (flat inject_thmss)), + (nchotomyN, [nchotomy_thm]), + (selsN, (flat sel_thmss)), + (splitN, [split_thm]), + (split_asmN, [split_asm_thm]), + (weak_case_cong_thmsN, [weak_case_cong_thm])] + |> map (fn (thmN, thms) => + ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); + in + lthy |> Local_Theory.notes notes |> snd + end; + in + (goals, after_qed, lthy') + end; + +val parse_bindings = Parse.$$$ "[" |-- Parse.list Parse.binding --| Parse.$$$ "]"; + +val parse_bindingss = Parse.$$$ "[" |-- Parse.list parse_bindings --| Parse.$$$ "]"; + +val wrap_data_cmd = (fn (goalss, after_qed, lthy) => + Proof.theorem NONE after_qed (map (map (rpair [])) goalss) lthy) oo + prepare_wrap Syntax.read_term; + +val _ = + Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wraps an existing datatype" + (((Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") -- Parse.term -- + Scan.optional (parse_bindings -- Scan.optional parse_bindingss []) ([], [])) + >> wrap_data_cmd); + +end; diff -r 88fe93ae61cf -r d8af889dcbe3 src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML Mon Sep 03 11:54:21 2012 +0200 @@ -0,0 +1,93 @@ +(* Title: HOL/Codatatype/Tools/bnf_wrap_tactics.ML + Author: Jasmin Blanchette, TU Muenchen + Copyright 2012 + +Tactics for wrapping datatypes. +*) + +signature BNF_WRAP_TACTICS = +sig + val mk_case_cong_tac: thm -> thm list -> tactic + val mk_case_disc_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> tactic + val mk_ctr_sel_tac: Proof.context -> int -> thm -> thm list -> tactic + val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic + val mk_half_disc_exclus_tac: int -> thm -> thm -> tactic + val mk_nchotomy_tac: int -> thm -> tactic + val mk_other_half_disc_exclus_tac: thm -> tactic + val mk_split_tac: thm -> thm list -> thm list list -> thm list list list -> tactic + val mk_split_asm_tac: Proof.context -> thm -> tactic +end; + +structure BNF_Wrap_Tactics : BNF_WRAP_TACTICS = +struct + +open BNF_Util +open BNF_Tactics +open BNF_FP_Util + +fun triangle _ [] = [] + | triangle k (xs :: xss) = take k xs :: triangle (k + 1) xss + +fun mk_if_P_or_not_P thm = + thm RS @{thm if_not_P} handle THM _ => thm RS @{thm if_P} + +fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms + +fun mk_nchotomy_tac n exhaust = + (rtac allI THEN' rtac exhaust THEN' + EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1; + +fun mk_half_disc_exclus_tac m discD disc'_thm = + (dtac discD THEN' + REPEAT_DETERM_N m o etac exE THEN' + hyp_subst_tac THEN' + rtac disc'_thm) 1; + +fun mk_other_half_disc_exclus_tac half_thm = + (etac @{thm contrapos_pn} THEN' etac half_thm) 1; + +fun mk_disc_exhaust_tac n exhaust discIs = + (rtac exhaust THEN' + EVERY' (map2 (fn k => fn discI => + dtac discI THEN' select_prem_tac n (etac @{thm meta_mp}) k THEN' atac) (1 upto n) discIs)) 1; + +fun mk_ctr_sel_tac ctxt m discD sel_thms = + (dtac discD THEN' + (if m = 0 then + atac + else + REPEAT_DETERM_N m o etac exE THEN' + hyp_subst_tac THEN' + SELECT_GOAL (Local_Defs.unfold_tac ctxt sel_thms) THEN' + rtac refl)) 1; + +fun mk_case_disc_tac ctxt exhaust' case_thms disc_thmss' sel_thmss = + (rtac exhaust' THEN' + EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms => EVERY' [ + hyp_subst_tac THEN' + SELECT_GOAL (Local_Defs.unfold_tac ctxt (if_disc_thms @ sel_thms)) THEN' + rtac case_thm]) case_thms + (map (map mk_if_P_or_not_P) (triangle 1 (map (fst o split_last) disc_thmss'))) sel_thmss)) 1; + +fun mk_case_cong_tac exhaust' case_thms = + (rtac exhaust' THEN' + EVERY' (maps (fn case_thm => [dtac sym, asm_simp_tac (ss_only [case_thm])]) case_thms)) 1; + +val naked_ctxt = Proof_Context.init_global @{theory HOL}; + +fun mk_split_tac exhaust' case_thms injectss distinctsss = + rtac exhaust' 1 THEN + ALLGOALS (fn k => + (hyp_subst_tac THEN' + simp_tac (ss_only (@{thms simp_thms} @ case_thms @ nth injectss (k - 1) @ + flat (nth distinctsss (k - 1))))) k) THEN + ALLGOALS (blast_tac naked_ctxt); + +val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex}; + +fun mk_split_asm_tac ctxt split = + rtac (split RS trans) 1 THEN + Local_Defs.unfold_tac ctxt split_asm_thms THEN + rtac refl 1; + +end;