1.1 --- a/etc/isar-keywords.el Mon Sep 03 11:30:29 2012 +0200
1.2 +++ b/etc/isar-keywords.el Mon Sep 03 11:54:21 2012 +0200
1.3 @@ -32,10 +32,7 @@
1.4 "axiomatization"
1.5 "axioms"
1.6 "back"
1.7 - "bnf_codata"
1.8 - "bnf_data"
1.9 "bnf_def"
1.10 - "bnf_sugar"
1.11 "boogie_end"
1.12 "boogie_open"
1.13 "boogie_status"
1.14 @@ -50,6 +47,7 @@
1.15 "class_deps"
1.16 "classes"
1.17 "classrel"
1.18 + "codata_raw"
1.19 "code_abort"
1.20 "code_class"
1.21 "code_const"
1.22 @@ -71,6 +69,7 @@
1.23 "context"
1.24 "corollary"
1.25 "cpodef"
1.26 + "data_raw"
1.27 "datatype"
1.28 "declaration"
1.29 "declare"
1.30 @@ -294,6 +293,7 @@
1.31 "values"
1.32 "welcome"
1.33 "with"
1.34 + "wrap_data"
1.35 "write"
1.36 "{"
1.37 "}"))
1.38 @@ -469,14 +469,13 @@
1.39 "attribute_setup"
1.40 "axiomatization"
1.41 "axioms"
1.42 - "bnf_codata"
1.43 - "bnf_data"
1.44 "boogie_end"
1.45 "boogie_open"
1.46 "bundle"
1.47 "class"
1.48 "classes"
1.49 "classrel"
1.50 + "codata_raw"
1.51 "code_abort"
1.52 "code_class"
1.53 "code_const"
1.54 @@ -492,6 +491,7 @@
1.55 "coinductive_set"
1.56 "consts"
1.57 "context"
1.58 + "data_raw"
1.59 "datatype"
1.60 "declaration"
1.61 "declare"
1.62 @@ -577,7 +577,6 @@
1.63 (defconst isar-keywords-theory-goal
1.64 '("ax_specification"
1.65 "bnf_def"
1.66 - "bnf_sugar"
1.67 "boogie_vc"
1.68 "code_pred"
1.69 "corollary"
1.70 @@ -605,7 +604,8 @@
1.71 "sublocale"
1.72 "termination"
1.73 "theorem"
1.74 - "typedef"))
1.75 + "typedef"
1.76 + "wrap_data"))
1.77
1.78 (defconst isar-keywords-qed
1.79 '("\\."
2.1 --- a/src/HOL/Codatatype/BNF_GFP.thy Mon Sep 03 11:30:29 2012 +0200
2.2 +++ b/src/HOL/Codatatype/BNF_GFP.thy Mon Sep 03 11:54:21 2012 +0200
2.3 @@ -10,7 +10,7 @@
2.4 theory BNF_GFP
2.5 imports BNF_Comp
2.6 keywords
2.7 - "bnf_codata" :: thy_decl
2.8 + "codata_raw" :: thy_decl
2.9 uses
2.10 "Tools/bnf_gfp_util.ML"
2.11 "Tools/bnf_gfp_tactics.ML"
3.1 --- a/src/HOL/Codatatype/BNF_LFP.thy Mon Sep 03 11:30:29 2012 +0200
3.2 +++ b/src/HOL/Codatatype/BNF_LFP.thy Mon Sep 03 11:54:21 2012 +0200
3.3 @@ -10,7 +10,7 @@
3.4 theory BNF_LFP
3.5 imports BNF_Comp
3.6 keywords
3.7 - "bnf_data" :: thy_decl
3.8 + "data_raw" :: thy_decl
3.9 uses
3.10 "Tools/bnf_lfp_util.ML"
3.11 "Tools/bnf_lfp_tactics.ML"
4.1 --- a/src/HOL/Codatatype/Codatatype.thy Mon Sep 03 11:30:29 2012 +0200
4.2 +++ b/src/HOL/Codatatype/Codatatype.thy Mon Sep 03 11:54:21 2012 +0200
4.3 @@ -12,10 +12,10 @@
4.4 theory Codatatype
4.5 imports BNF_LFP BNF_GFP
4.6 keywords
4.7 - "bnf_sugar" :: thy_goal
4.8 -uses
4.9 - "Tools/bnf_sugar_tactics.ML"
4.10 - "Tools/bnf_sugar.ML"
4.11 + "wrap_data" :: thy_goal
4.12 +usesy
4.13 + "Tools/bnf_wrap_tactics.ML"
4.14 + "Tools/bnf_wrap.ML"
4.15 begin
4.16
4.17 end
5.1 --- a/src/HOL/Codatatype/Examples/HFset.thy Mon Sep 03 11:30:29 2012 +0200
5.2 +++ b/src/HOL/Codatatype/Examples/HFset.thy Mon Sep 03 11:54:21 2012 +0200
5.3 @@ -14,7 +14,7 @@
5.4
5.5 section {* Datatype definition *}
5.6
5.7 -bnf_data hfset: 'hfset = "'hfset fset"
5.8 +data_raw hfset: 'hfset = "'hfset fset"
5.9
5.10
5.11 section {* Customization of terms *}
6.1 --- a/src/HOL/Codatatype/Examples/Lambda_Term.thy Mon Sep 03 11:30:29 2012 +0200
6.2 +++ b/src/HOL/Codatatype/Examples/Lambda_Term.thy Mon Sep 03 11:54:21 2012 +0200
6.3 @@ -15,7 +15,7 @@
6.4
6.5 section {* Datatype definition *}
6.6
6.7 -bnf_data trm: 'trm = "'a + 'trm \<times> 'trm + 'a \<times> 'trm + ('a \<times> 'trm) fset \<times> 'trm"
6.8 +data_raw trm: 'trm = "'a + 'trm \<times> 'trm + 'a \<times> 'trm + ('a \<times> 'trm) fset \<times> 'trm"
6.9
6.10
6.11 section {* Customization of terms *}
7.1 --- a/src/HOL/Codatatype/Examples/ListF.thy Mon Sep 03 11:30:29 2012 +0200
7.2 +++ b/src/HOL/Codatatype/Examples/ListF.thy Mon Sep 03 11:54:21 2012 +0200
7.3 @@ -12,7 +12,7 @@
7.4 imports "../Codatatype"
7.5 begin
7.6
7.7 -bnf_data listF: 'list = "unit + 'a \<times> 'list"
7.8 +data_raw listF: 'list = "unit + 'a \<times> 'list"
7.9
7.10 definition "NilF = listF_fld (Inl ())"
7.11 definition "Conss a as \<equiv> listF_fld (Inr (a, as))"
8.1 --- a/src/HOL/Codatatype/Examples/Misc_Codata.thy Mon Sep 03 11:30:29 2012 +0200
8.2 +++ b/src/HOL/Codatatype/Examples/Misc_Codata.thy Mon Sep 03 11:54:21 2012 +0200
8.3 @@ -16,33 +16,33 @@
8.4
8.5 ML {* PolyML.fullGC (); *}
8.6
8.7 -bnf_codata simple: 'a = "unit + unit + unit + unit"
8.8 +codata_raw simple: 'a = "unit + unit + unit + unit"
8.9
8.10 -bnf_codata stream: 's = "'a \<times> 's"
8.11 +codata_raw stream: 's = "'a \<times> 's"
8.12
8.13 -bnf_codata llist: 'llist = "unit + 'a \<times> 'llist"
8.14 +codata_raw llist: 'llist = "unit + 'a \<times> 'llist"
8.15
8.16 -bnf_codata some_passive: 'a = "'a + 'b + 'c + 'd + 'e"
8.17 +codata_raw some_passive: 'a = "'a + 'b + 'c + 'd + 'e"
8.18
8.19 (*
8.20 ('a, 'b1, 'b2) F1 = 'a * 'b1 + 'a * 'b2
8.21 ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2
8.22 *)
8.23
8.24 -bnf_codata F1: 'b1 = "'a \<times> 'b1 + 'a \<times> 'b2"
8.25 +codata_raw F1: 'b1 = "'a \<times> 'b1 + 'a \<times> 'b2"
8.26 and F2: 'b2 = "unit + 'b1 * 'b2"
8.27
8.28 -bnf_codata EXPR: 'E = "'T + 'T \<times> 'E"
8.29 +codata_raw EXPR: 'E = "'T + 'T \<times> 'E"
8.30 and TERM: 'T = "'F + 'F \<times> 'T"
8.31 and FACTOR: 'F = "'a + 'b + 'E"
8.32
8.33 -bnf_codata llambda:
8.34 +codata_raw llambda:
8.35 'trm = "string +
8.36 'trm \<times> 'trm +
8.37 string \<times> 'trm +
8.38 (string \<times> 'trm) fset \<times> 'trm"
8.39
8.40 -bnf_codata par_llambda:
8.41 +codata_raw par_llambda:
8.42 'trm = "'a +
8.43 'trm \<times> 'trm +
8.44 'a \<times> 'trm +
8.45 @@ -53,29 +53,29 @@
8.46 'a forest = Nil | Cons of 'a tree * 'a forest ('c = unit + 'b * 'c)
8.47 *)
8.48
8.49 -bnf_codata tree: 'tree = "unit + 'a \<times> 'forest"
8.50 +codata_raw tree: 'tree = "unit + 'a \<times> 'forest"
8.51 and forest: 'forest = "unit + 'tree \<times> 'forest"
8.52
8.53 -bnf_codata CPS: 'a = "'b + 'b \<Rightarrow> 'a"
8.54 +codata_raw CPS: 'a = "'b + 'b \<Rightarrow> 'a"
8.55
8.56 -bnf_codata fun_rhs: 'a = "'b1 \<Rightarrow> 'b2 \<Rightarrow> 'b3 \<Rightarrow> 'b4 \<Rightarrow> 'b5 \<Rightarrow> 'b6 \<Rightarrow> 'b7 \<Rightarrow> 'b8 \<Rightarrow> 'b9 \<Rightarrow> 'a"
8.57 +codata_raw fun_rhs: 'a = "'b1 \<Rightarrow> 'b2 \<Rightarrow> 'b3 \<Rightarrow> 'b4 \<Rightarrow> 'b5 \<Rightarrow> 'b6 \<Rightarrow> 'b7 \<Rightarrow> 'b8 \<Rightarrow> 'b9 \<Rightarrow> 'a"
8.58
8.59 -bnf_codata fun_rhs': 'a = "'b1 \<Rightarrow> 'b2 \<Rightarrow> 'b3 \<Rightarrow> 'b4 \<Rightarrow> 'b5 \<Rightarrow> 'b6 \<Rightarrow> 'b7 \<Rightarrow> 'b8 \<Rightarrow> 'b9 \<Rightarrow> 'b10 \<Rightarrow>
8.60 +codata_raw fun_rhs': 'a = "'b1 \<Rightarrow> 'b2 \<Rightarrow> 'b3 \<Rightarrow> 'b4 \<Rightarrow> 'b5 \<Rightarrow> 'b6 \<Rightarrow> 'b7 \<Rightarrow> 'b8 \<Rightarrow> 'b9 \<Rightarrow> 'b10 \<Rightarrow>
8.61 'b11 \<Rightarrow> 'b12 \<Rightarrow> 'b13 \<Rightarrow> 'b14 \<Rightarrow> 'b15 \<Rightarrow> 'b16 \<Rightarrow> 'b17 \<Rightarrow> 'b18 \<Rightarrow> 'b19 \<Rightarrow> 'b20 \<Rightarrow> 'a"
8.62
8.63 -bnf_codata some_killing: 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)"
8.64 +codata_raw some_killing: 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)"
8.65 and in_here: 'c = "'d \<times> 'b + 'e"
8.66
8.67 -bnf_codata some_killing': 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)"
8.68 +codata_raw some_killing': 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)"
8.69 and in_here': 'c = "'d + 'e"
8.70
8.71 -bnf_codata some_killing'': 'a = "'b \<Rightarrow> 'c"
8.72 +codata_raw some_killing'': 'a = "'b \<Rightarrow> 'c"
8.73 and in_here'': 'c = "'d \<times> 'b + 'e"
8.74
8.75 -bnf_codata less_killing: 'a = "'b \<Rightarrow> 'c"
8.76 +codata_raw less_killing: 'a = "'b \<Rightarrow> 'c"
8.77
8.78 (* SLOW, MEMORY-HUNGRY
8.79 -bnf_codata K1': 'K1 = "'K2 + 'a list"
8.80 +codata_raw K1': 'K1 = "'K2 + 'a list"
8.81 and K2': 'K2 = "'K3 + 'c fset"
8.82 and K3': 'K3 = "'K3 + 'K4 + 'K4 \<times> 'K5"
8.83 and K4': 'K4 = "'K5 + 'a list list list"
9.1 --- a/src/HOL/Codatatype/Examples/Misc_Data.thy Mon Sep 03 11:30:29 2012 +0200
9.2 +++ b/src/HOL/Codatatype/Examples/Misc_Data.thy Mon Sep 03 11:54:21 2012 +0200
9.3 @@ -16,19 +16,19 @@
9.4
9.5 ML {* PolyML.fullGC (); *}
9.6
9.7 -bnf_data simple: 'a = "unit + unit + unit + unit"
9.8 +data_raw simple: 'a = "unit + unit + unit + unit"
9.9
9.10 -bnf_data mylist: 'list = "unit + 'a \<times> 'list"
9.11 +data_raw mylist: 'list = "unit + 'a \<times> 'list"
9.12
9.13 -bnf_data some_passive: 'a = "'a + 'b + 'c + 'd + 'e"
9.14 +data_raw some_passive: 'a = "'a + 'b + 'c + 'd + 'e"
9.15
9.16 -bnf_data lambda:
9.17 +data_raw lambda:
9.18 'trm = "string +
9.19 'trm \<times> 'trm +
9.20 string \<times> 'trm +
9.21 (string \<times> 'trm) fset \<times> 'trm"
9.22
9.23 -bnf_data par_lambda:
9.24 +data_raw par_lambda:
9.25 'trm = "'a +
9.26 'trm \<times> 'trm +
9.27 'a \<times> 'trm +
9.28 @@ -39,7 +39,7 @@
9.29 ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2
9.30 *)
9.31
9.32 -bnf_data F1: 'b1 = "'a \<times> 'b1 + 'a \<times> 'b2"
9.33 +data_raw F1: 'b1 = "'a \<times> 'b1 + 'a \<times> 'b2"
9.34 and F2: 'b2 = "unit + 'b1 * 'b2"
9.35
9.36 (*
9.37 @@ -47,7 +47,7 @@
9.38 'a forest = Nil | Cons of 'a tree * 'a forest ('c = unit + 'b * 'c)
9.39 *)
9.40
9.41 -bnf_data tree: 'tree = "unit + 'a \<times> 'forest"
9.42 +data_raw tree: 'tree = "unit + 'a \<times> 'forest"
9.43 and forest: 'forest = "unit + 'tree \<times> 'forest"
9.44
9.45 (*
9.46 @@ -55,7 +55,7 @@
9.47 ' a branch = Branch of 'a * 'a tree ('c = 'a * 'b)
9.48 *)
9.49
9.50 -bnf_data tree': 'tree = "unit + 'branch \<times> 'branch"
9.51 +data_raw tree': 'tree = "unit + 'branch \<times> 'branch"
9.52 and branch: 'branch = "'a \<times> 'tree"
9.53
9.54 (*
9.55 @@ -64,54 +64,54 @@
9.56 factor = C 'a | V 'b | Paren exp ('e = 'a + 'b + 'c)
9.57 *)
9.58
9.59 -bnf_data EXPR: 'E = "'T + 'T \<times> 'E"
9.60 +data_raw EXPR: 'E = "'T + 'T \<times> 'E"
9.61 and TERM: 'T = "'F + 'F \<times> 'T"
9.62 and FACTOR: 'F = "'a + 'b + 'E"
9.63
9.64 -bnf_data some_killing: 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)"
9.65 +data_raw some_killing: 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)"
9.66 and in_here: 'c = "'d \<times> 'b + 'e"
9.67
9.68 -bnf_data nofail1: 'a = "'a \<times> 'b + 'b"
9.69 -bnf_data nofail2: 'a = "('a \<times> 'b \<times> 'a \<times> 'b) list"
9.70 -bnf_data nofail3: 'a = "'b \<times> ('a \<times> 'b \<times> 'a \<times> 'b) fset"
9.71 -bnf_data nofail4: 'a = "('a \<times> ('a \<times> 'b \<times> 'a \<times> 'b) fset) list"
9.72 +data_raw nofail1: 'a = "'a \<times> 'b + 'b"
9.73 +data_raw nofail2: 'a = "('a \<times> 'b \<times> 'a \<times> 'b) list"
9.74 +data_raw nofail3: 'a = "'b \<times> ('a \<times> 'b \<times> 'a \<times> 'b) fset"
9.75 +data_raw nofail4: 'a = "('a \<times> ('a \<times> 'b \<times> 'a \<times> 'b) fset) list"
9.76
9.77 (*
9.78 -bnf_data fail: 'a = "'a \<times> 'b \<times> 'a \<times> 'b list"
9.79 -bnf_data fail: 'a = "'a \<times> 'b \<times> 'a \<times> 'b"
9.80 -bnf_data fail: 'a = "'a \<times> 'b + 'a"
9.81 -bnf_data fail: 'a = "'a \<times> 'b"
9.82 +data_raw fail: 'a = "'a \<times> 'b \<times> 'a \<times> 'b list"
9.83 +data_raw fail: 'a = "'a \<times> 'b \<times> 'a \<times> 'b"
9.84 +data_raw fail: 'a = "'a \<times> 'b + 'a"
9.85 +data_raw fail: 'a = "'a \<times> 'b"
9.86 *)
9.87
9.88 -bnf_data L1: 'L1 = "'L2 list"
9.89 +data_raw L1: 'L1 = "'L2 list"
9.90 and L2: 'L2 = "'L1 fset + 'L2"
9.91
9.92 -bnf_data K1: 'K1 = "'K2"
9.93 +data_raw K1: 'K1 = "'K2"
9.94 and K2: 'K2 = "'K3"
9.95 and K3: 'K3 = "'K1 list"
9.96
9.97 -bnf_data t1: 't1 = "'t3 + 't2"
9.98 +data_raw t1: 't1 = "'t3 + 't2"
9.99 and t2: 't2 = "'t1"
9.100 and t3: 't3 = "unit"
9.101
9.102 -bnf_data t1': 't1 = "'t2 + 't3"
9.103 +data_raw t1': 't1 = "'t2 + 't3"
9.104 and t2': 't2 = "'t1"
9.105 and t3': 't3 = "unit"
9.106
9.107 (*
9.108 -bnf_data fail1: 'L1 = "'L2"
9.109 +data_raw fail1: 'L1 = "'L2"
9.110 and fail2: 'L2 = "'L3"
9.111 and fail2: 'L3 = "'L1"
9.112
9.113 -bnf_data fail1: 'L1 = "'L2 list \<times> 'L2"
9.114 +data_raw fail1: 'L1 = "'L2 list \<times> 'L2"
9.115 and fail2: 'L2 = "'L2 fset \<times> 'L3"
9.116 and fail2: 'L3 = "'L1"
9.117
9.118 -bnf_data fail1: 'L1 = "'L2 list \<times> 'L2"
9.119 +data_raw fail1: 'L1 = "'L2 list \<times> 'L2"
9.120 and fail2: 'L2 = "'L1 fset \<times> 'L1"
9.121 *)
9.122 (* SLOW
9.123 -bnf_data K1': 'K1 = "'K2 + 'a list"
9.124 +data_raw K1': 'K1 = "'K2 + 'a list"
9.125 and K2': 'K2 = "'K3 + 'c fset"
9.126 and K3': 'K3 = "'K3 + 'K4 + 'K4 \<times> 'K5"
9.127 and K4': 'K4 = "'K5 + 'a list list list"
9.128 @@ -132,23 +132,23 @@
9.129 *)
9.130
9.131 (* fail:
9.132 -bnf_data t1: 't1 = "'t2 * 't3 + 't2 * 't4"
9.133 +data_raw t1: 't1 = "'t2 * 't3 + 't2 * 't4"
9.134 and t2: 't2 = "unit"
9.135 and t3: 't3 = 't4
9.136 and t4: 't4 = 't1
9.137 *)
9.138
9.139 -bnf_data k1: 'k1 = "'k2 * 'k3 + 'k2 * 'k4"
9.140 +data_raw k1: 'k1 = "'k2 * 'k3 + 'k2 * 'k4"
9.141 and k2: 'k2 = unit
9.142 and k3: 'k3 = 'k4
9.143 and k4: 'k4 = unit
9.144
9.145 -bnf_data tt1: 'tt1 = "'tt3 * 'tt2 + 'tt2 * 'tt4"
9.146 +data_raw tt1: 'tt1 = "'tt3 * 'tt2 + 'tt2 * 'tt4"
9.147 and tt2: 'tt2 = unit
9.148 and tt3: 'tt3 = 'tt1
9.149 and tt4: 'tt4 = unit
9.150 (* SLOW
9.151 -bnf_data s1: 's1 = "'s2 * 's3 * 's4 + 's3 + 's2 * 's6 + 's4 * 's2 + 's2 * 's2"
9.152 +data_raw s1: 's1 = "'s2 * 's3 * 's4 + 's3 + 's2 * 's6 + 's4 * 's2 + 's2 * 's2"
9.153 and s2: 's2 = "'s7 * 's5 + 's5 * 's4 * 's6"
9.154 and s3: 's3 = "'s1 * 's7 * 's2 + 's3 * 's3 + 's4 * 's5"
9.155 and s4: 's4 = 's5
10.1 --- a/src/HOL/Codatatype/Examples/Process.thy Mon Sep 03 11:30:29 2012 +0200
10.2 +++ b/src/HOL/Codatatype/Examples/Process.thy Mon Sep 03 11:54:21 2012 +0200
10.3 @@ -11,7 +11,7 @@
10.4 imports "../Codatatype"
10.5 begin
10.6
10.7 -bnf_codata process: 'p = "'a * 'p + 'p * 'p"
10.8 +codata_raw process: 'p = "'a * 'p + 'p * 'p"
10.9 (* codatatype
10.10 'a process = Action (prefOf :: 'a) (contOf :: 'a process) |
10.11 Choice (ch1Of :: 'a process) (ch2Of :: 'a process)
11.1 --- a/src/HOL/Codatatype/Examples/Stream.thy Mon Sep 03 11:30:29 2012 +0200
11.2 +++ b/src/HOL/Codatatype/Examples/Stream.thy Mon Sep 03 11:54:21 2012 +0200
11.3 @@ -12,7 +12,7 @@
11.4 imports TreeFI
11.5 begin
11.6
11.7 -bnf_codata stream: 's = "'a \<times> 's"
11.8 +codata_raw stream: 's = "'a \<times> 's"
11.9
11.10 (* selectors for streams *)
11.11 definition "hdd as \<equiv> fst (stream_unf as)"
12.1 --- a/src/HOL/Codatatype/Examples/TreeFI.thy Mon Sep 03 11:30:29 2012 +0200
12.2 +++ b/src/HOL/Codatatype/Examples/TreeFI.thy Mon Sep 03 11:54:21 2012 +0200
12.3 @@ -12,7 +12,7 @@
12.4 imports ListF
12.5 begin
12.6
12.7 -bnf_codata treeFI: 'tree = "'a \<times> 'tree listF"
12.8 +codata_raw treeFI: 'tree = "'a \<times> 'tree listF"
12.9
12.10 lemma treeFIBNF_listF_set[simp]: "treeFIBNF_set2 (i, xs) = listF_set xs"
12.11 unfolding treeFIBNF_set2_def collect_def[abs_def] prod_set_defs
13.1 --- a/src/HOL/Codatatype/Examples/TreeFsetI.thy Mon Sep 03 11:30:29 2012 +0200
13.2 +++ b/src/HOL/Codatatype/Examples/TreeFsetI.thy Mon Sep 03 11:54:21 2012 +0200
13.3 @@ -15,7 +15,7 @@
13.4 definition pair_fun (infixr "\<odot>" 50) where
13.5 "f \<odot> g \<equiv> \<lambda>x. (f x, g x)"
13.6
13.7 -bnf_codata treeFsetI: 't = "'a \<times> 't fset"
13.8 +codata_raw treeFsetI: 't = "'a \<times> 't fset"
13.9
13.10 (* selectors for trees *)
13.11 definition "lab t \<equiv> fst (treeFsetI_unf t)"
14.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Mon Sep 03 11:30:29 2012 +0200
14.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Mon Sep 03 11:54:21 2012 +0200
14.3 @@ -2776,7 +2776,7 @@
14.4 end;
14.5
14.6 val _ =
14.7 - Outer_Syntax.local_theory @{command_spec "bnf_codata"} "greatest fixed points for BNF equations"
14.8 + Outer_Syntax.local_theory @{command_spec "codata_raw"} "greatest fixed points for BNF equations"
14.9 (Parse.and_list1
14.10 ((Parse.binding --| Parse.$$$ ":") -- (Parse.typ --| Parse.$$$ "=" -- Parse.typ)) >>
14.11 (fp_bnf_cmd bnf_gfp o apsnd split_list o split_list));
15.1 --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Mon Sep 03 11:30:29 2012 +0200
15.2 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Mon Sep 03 11:54:21 2012 +0200
15.3 @@ -1755,7 +1755,7 @@
15.4 end;
15.5
15.6 val _ =
15.7 - Outer_Syntax.local_theory @{command_spec "bnf_data"} "least fixed points for BNF equations"
15.8 + Outer_Syntax.local_theory @{command_spec "data_raw"} "least fixed points for BNF equations"
15.9 (Parse.and_list1
15.10 ((Parse.binding --| Parse.$$$ ":") -- (Parse.typ --| Parse.$$$ "=" -- Parse.typ)) >>
15.11 (fp_bnf_cmd bnf_lfp o apsnd split_list o split_list));
16.1 --- a/src/HOL/Codatatype/Tools/bnf_sugar.ML Mon Sep 03 11:30:29 2012 +0200
16.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
16.3 @@ -1,420 +0,0 @@
16.4 -(* Title: HOL/Codatatype/Tools/bnf_sugar.ML
16.5 - Author: Jasmin Blanchette, TU Muenchen
16.6 - Copyright 2012
16.7 -
16.8 -Sugar on top of a BNF.
16.9 -*)
16.10 -
16.11 -signature BNF_SUGAR =
16.12 -sig
16.13 -end;
16.14 -
16.15 -structure BNF_Sugar : BNF_SUGAR =
16.16 -struct
16.17 -
16.18 -open BNF_Util
16.19 -open BNF_FP_Util
16.20 -open BNF_Sugar_Tactics
16.21 -
16.22 -val is_N = "is_";
16.23 -val un_N = "un_";
16.24 -fun mk_un_N 1 1 suf = un_N ^ suf
16.25 - | mk_un_N _ l suf = un_N ^ suf ^ string_of_int l;
16.26 -
16.27 -val case_congN = "case_cong";
16.28 -val case_discsN = "case_discs";
16.29 -val casesN = "cases";
16.30 -val ctr_selsN = "ctr_sels";
16.31 -val disc_exclusN = "disc_exclus";
16.32 -val disc_exhaustN = "disc_exhaust";
16.33 -val discsN = "discs";
16.34 -val distinctN = "distinct";
16.35 -val selsN = "sels";
16.36 -val splitN = "split";
16.37 -val split_asmN = "split_asm";
16.38 -val weak_case_cong_thmsN = "weak_case_cong";
16.39 -
16.40 -val default_name = @{binding _};
16.41 -
16.42 -fun pad_list x n xs = xs @ replicate (n - length xs) x;
16.43 -
16.44 -fun mk_half_pairss' _ [] = []
16.45 - | mk_half_pairss' indent (y :: ys) =
16.46 - indent @ fold_rev (cons o single o pair y) ys (mk_half_pairss' ([] :: indent) ys);
16.47 -
16.48 -fun mk_half_pairss ys = mk_half_pairss' [[]] ys;
16.49 -
16.50 -val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
16.51 -
16.52 -fun mk_undef T Ts = Const (@{const_name undefined}, Ts ---> T);
16.53 -
16.54 -fun eta_expand_caseof_arg xs f_xs = fold_rev Term.lambda xs f_xs;
16.55 -
16.56 -fun name_of_ctr t =
16.57 - case head_of t of
16.58 - Const (s, _) => s
16.59 - | Free (s, _) => s
16.60 - | _ => error "Cannot extract name of constructor";
16.61 -
16.62 -fun prepare_sugar prep_term ((raw_ctrs, raw_caseof), (raw_disc_names, raw_sel_namess))
16.63 - no_defs_lthy =
16.64 - let
16.65 - (* TODO: sanity checks on arguments *)
16.66 -
16.67 - (* TODO: normalize types of constructors w.r.t. each other *)
16.68 -
16.69 - val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs;
16.70 - val caseof0 = prep_term no_defs_lthy raw_caseof;
16.71 -
16.72 - val n = length ctrs0;
16.73 - val ks = 1 upto n;
16.74 -
16.75 - val (T_name, As0) = dest_Type (body_type (fastype_of (hd ctrs0)));
16.76 - val b = Binding.qualified_name T_name;
16.77 -
16.78 - val (As, B) =
16.79 - no_defs_lthy
16.80 - |> mk_TFrees (length As0)
16.81 - ||> the_single o fst o mk_TFrees 1;
16.82 -
16.83 - fun mk_ctr Ts ctr =
16.84 - let val Ts0 = snd (dest_Type (body_type (fastype_of ctr))) in
16.85 - Term.subst_atomic_types (Ts0 ~~ Ts) ctr
16.86 - end;
16.87 -
16.88 - val T = Type (T_name, As);
16.89 - val ctrs = map (mk_ctr As) ctrs0;
16.90 - val ctr_Tss = map (binder_types o fastype_of) ctrs;
16.91 -
16.92 - val ms = map length ctr_Tss;
16.93 -
16.94 - val disc_names =
16.95 - pad_list default_name n raw_disc_names
16.96 - |> map2 (fn ctr => fn disc =>
16.97 - if Binding.eq_name (disc, default_name) then
16.98 - Binding.name (prefix is_N (Long_Name.base_name (name_of_ctr ctr)))
16.99 - else
16.100 - disc) ctrs0;
16.101 -
16.102 - val sel_namess =
16.103 - pad_list [] n raw_sel_namess
16.104 - |> map3 (fn ctr => fn m => map2 (fn l => fn sel =>
16.105 - if Binding.eq_name (sel, default_name) then
16.106 - Binding.name (mk_un_N m l (Long_Name.base_name (name_of_ctr ctr)))
16.107 - else
16.108 - sel) (1 upto m) o pad_list default_name m) ctrs0 ms;
16.109 -
16.110 - fun mk_caseof Ts T =
16.111 - let val (binders, body) = strip_type (fastype_of caseof0) in
16.112 - Term.subst_atomic_types ((body, T) :: (snd (dest_Type (List.last binders)) ~~ Ts)) caseof0
16.113 - end;
16.114 -
16.115 - val caseofB = mk_caseof As B;
16.116 - val caseofB_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
16.117 -
16.118 - fun mk_caseofB_term eta_fs = Term.list_comb (caseofB, eta_fs);
16.119 -
16.120 - val (((((((xss, yss), fs), gs), (v, v')), w), (p, p')), names_lthy) = no_defs_lthy |>
16.121 - mk_Freess "x" ctr_Tss
16.122 - ||>> mk_Freess "y" ctr_Tss
16.123 - ||>> mk_Frees "f" caseofB_Ts
16.124 - ||>> mk_Frees "g" caseofB_Ts
16.125 - ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "v") T
16.126 - ||>> yield_singleton (mk_Frees "w") T
16.127 - ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT;
16.128 -
16.129 - val q = Free (fst p', B --> HOLogic.boolT);
16.130 -
16.131 - val xctrs = map2 (curry Term.list_comb) ctrs xss;
16.132 - val yctrs = map2 (curry Term.list_comb) ctrs yss;
16.133 -
16.134 - val xfs = map2 (curry Term.list_comb) fs xss;
16.135 - val xgs = map2 (curry Term.list_comb) gs xss;
16.136 -
16.137 - val eta_fs = map2 eta_expand_caseof_arg xss xfs;
16.138 - val eta_gs = map2 eta_expand_caseof_arg xss xgs;
16.139 -
16.140 - val caseofB_fs = Term.list_comb (caseofB, eta_fs);
16.141 -
16.142 - val exist_xs_v_eq_ctrs =
16.143 - map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (v, xctr))) xctrs xss;
16.144 -
16.145 - fun mk_sel_caseof_args k xs x T =
16.146 - map2 (fn Ts => fn i => if i = k then fold_rev Term.lambda xs x else mk_undef T Ts) ctr_Tss ks;
16.147 -
16.148 - fun disc_spec b exist_xs_v_eq_ctr =
16.149 - mk_Trueprop_eq (Free (Binding.name_of b, T --> HOLogic.boolT) $ v, exist_xs_v_eq_ctr);
16.150 -
16.151 - fun sel_spec b x xs k =
16.152 - let val T' = fastype_of x in
16.153 - mk_Trueprop_eq (Free (Binding.name_of b, T --> T') $ v,
16.154 - Term.list_comb (mk_caseof As T', mk_sel_caseof_args k xs x T') $ v)
16.155 - end;
16.156 -
16.157 - val (((raw_discs, (_, raw_disc_defs)), (raw_selss, (_, raw_sel_defss))), (lthy', lthy)) =
16.158 - no_defs_lthy
16.159 - |> apfst (apsnd split_list o split_list) o fold_map2 (fn b => fn exist_xs_v_eq_ctr =>
16.160 - Specification.definition (SOME (b, NONE, NoSyn),
16.161 - ((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr))) disc_names exist_xs_v_eq_ctrs
16.162 - ||>> apfst (apsnd split_list o split_list) o fold_map3 (fn bs => fn xs => fn k =>
16.163 - apfst (apsnd split_list o split_list) o fold_map2 (fn b => fn x =>
16.164 - Specification.definition (SOME (b, NONE, NoSyn),
16.165 - ((Thm.def_binding b, []), sel_spec b x xs k))) bs xs) sel_namess xss ks
16.166 - ||> `Local_Theory.restore;
16.167 -
16.168 - (*transforms defined frees into consts (and more)*)
16.169 - val phi = Proof_Context.export_morphism lthy lthy';
16.170 -
16.171 - val disc_defs = map (Morphism.thm phi) raw_disc_defs;
16.172 - val sel_defss = map (map (Morphism.thm phi)) raw_sel_defss;
16.173 -
16.174 - val discs0 = map (Morphism.term phi) raw_discs;
16.175 - val selss0 = map (map (Morphism.term phi)) raw_selss;
16.176 -
16.177 - fun mk_disc_or_sel Ts t =
16.178 - Term.subst_atomic_types (snd (dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
16.179 -
16.180 - val discs = map (mk_disc_or_sel As) discs0;
16.181 - val selss = map (map (mk_disc_or_sel As)) selss0;
16.182 -
16.183 - fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p);
16.184 -
16.185 - val goal_exhaust =
16.186 - let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (v, xctr)]) in
16.187 - mk_imp_p (map2 mk_prem xctrs xss)
16.188 - end;
16.189 -
16.190 - val goal_injectss =
16.191 - let
16.192 - fun mk_goal _ _ [] [] = []
16.193 - | mk_goal xctr yctr xs ys =
16.194 - [mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr),
16.195 - Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys))];
16.196 - in
16.197 - map4 mk_goal xctrs yctrs xss yss
16.198 - end;
16.199 -
16.200 - val goal_half_distinctss =
16.201 - map (map (HOLogic.mk_Trueprop o HOLogic.mk_not o HOLogic.mk_eq)) (mk_half_pairss xctrs);
16.202 -
16.203 - val goal_cases = map2 (fn xctr => fn xf => mk_Trueprop_eq (caseofB_fs $ xctr, xf)) xctrs xfs;
16.204 -
16.205 - val goals = [goal_exhaust] :: goal_injectss @ goal_half_distinctss @ [goal_cases];
16.206 -
16.207 - fun after_qed thmss lthy =
16.208 - let
16.209 - val ([exhaust_thm], (inject_thmss, (half_distinct_thmss, [case_thms]))) =
16.210 - (hd thmss, apsnd (chop (n * n)) (chop n (tl thmss)));
16.211 -
16.212 - val exhaust_thm' =
16.213 - let val Tinst = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As) in
16.214 - Drule.instantiate' [] [SOME (certify lthy v)]
16.215 - (Thm.instantiate (Tinst, []) (Drule.zero_var_indexes exhaust_thm))
16.216 - end;
16.217 -
16.218 - val other_half_distinct_thmss = map (map (fn thm => thm RS not_sym)) half_distinct_thmss;
16.219 -
16.220 - val (distinct_thmsss', distinct_thmsss) =
16.221 - map2 (map2 append) (Library.chop_groups n half_distinct_thmss)
16.222 - (transpose (Library.chop_groups n other_half_distinct_thmss))
16.223 - |> `transpose;
16.224 - val distinct_thms = interleave (flat half_distinct_thmss) (flat other_half_distinct_thmss);
16.225 -
16.226 - val nchotomy_thm =
16.227 - let
16.228 - val goal =
16.229 - HOLogic.mk_Trueprop (HOLogic.mk_all (fst v', snd v',
16.230 - Library.foldr1 HOLogic.mk_disj exist_xs_v_eq_ctrs));
16.231 - in
16.232 - Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm)
16.233 - end;
16.234 -
16.235 - val sel_thmss =
16.236 - let
16.237 - fun mk_thm k xs goal_case case_thm x sel_def =
16.238 - let
16.239 - val T = fastype_of x;
16.240 - val cTs =
16.241 - map ((fn T' => certifyT lthy (if T' = B then T else T')) o TFree)
16.242 - (rev (Term.add_tfrees goal_case []));
16.243 - val cxs = map (certify lthy) (mk_sel_caseof_args k xs x T);
16.244 - in
16.245 - Local_Defs.fold lthy [sel_def]
16.246 - (Drule.instantiate' (map SOME cTs) (map SOME cxs) case_thm)
16.247 - end;
16.248 - fun mk_thms k xs goal_case case_thm sel_defs =
16.249 - map2 (mk_thm k xs goal_case case_thm) xs sel_defs;
16.250 - in
16.251 - map5 mk_thms ks xss goal_cases case_thms sel_defss
16.252 - end;
16.253 -
16.254 - val discD_thms = map (fn def => def RS iffD1) disc_defs;
16.255 - val discI_thms =
16.256 - map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms disc_defs;
16.257 - val not_disc_thms =
16.258 - map2 (fn m => fn def => funpow m (fn thm => allI RS thm)
16.259 - (Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]})))
16.260 - ms disc_defs;
16.261 -
16.262 - val (disc_thmss', disc_thmss) =
16.263 - let
16.264 - fun mk_thm discI _ [] = refl RS discI
16.265 - | mk_thm _ not_disc [distinct] = distinct RS not_disc;
16.266 - fun mk_thms discI not_disc distinctss = map (mk_thm discI not_disc) distinctss;
16.267 - in
16.268 - map3 mk_thms discI_thms not_disc_thms distinct_thmsss'
16.269 - |> `transpose
16.270 - end;
16.271 -
16.272 - val disc_exclus_thms =
16.273 - let
16.274 - fun mk_goal ((_, disc), (_, disc')) =
16.275 - Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v),
16.276 - HOLogic.mk_Trueprop (HOLogic.mk_not (disc' $ v))));
16.277 - fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac);
16.278 -
16.279 - val bundles = ms ~~ discD_thms ~~ discs;
16.280 - val half_pairss = mk_half_pairss bundles;
16.281 -
16.282 - val goal_halvess = map (map mk_goal) half_pairss;
16.283 - val half_thmss =
16.284 - map3 (fn [] => K (K [])
16.285 - | [(((m, discD), _), _)] => fn disc_thm => fn [goal] =>
16.286 - [prove (mk_half_disc_exclus_tac m discD disc_thm) goal])
16.287 - half_pairss (flat disc_thmss') goal_halvess;
16.288 -
16.289 - val goal_other_halvess = map (map (mk_goal o swap)) half_pairss;
16.290 - val other_half_thmss =
16.291 - map2 (map2 (prove o mk_other_half_disc_exclus_tac)) half_thmss goal_other_halvess;
16.292 - in
16.293 - interleave (flat half_thmss) (flat other_half_thmss)
16.294 - end;
16.295 -
16.296 - val disc_exhaust_thm =
16.297 - let
16.298 - fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (disc $ v)];
16.299 - val goal = fold Logic.all [p, v] (mk_imp_p (map mk_prem discs));
16.300 - in
16.301 - Skip_Proof.prove lthy [] [] goal (fn _ => mk_disc_exhaust_tac n exhaust_thm discI_thms)
16.302 - end;
16.303 -
16.304 - val ctr_sel_thms =
16.305 - let
16.306 - fun mk_goal ctr disc sels =
16.307 - Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v),
16.308 - mk_Trueprop_eq ((null sels ? swap)
16.309 - (Term.list_comb (ctr, map (fn sel => sel $ v) sels), v))));
16.310 - val goals = map3 mk_goal ctrs discs selss;
16.311 - in
16.312 - map4 (fn goal => fn m => fn discD => fn sel_thms =>
16.313 - Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
16.314 - mk_ctr_sel_tac ctxt m discD sel_thms))
16.315 - goals ms discD_thms sel_thmss
16.316 - end;
16.317 -
16.318 - val case_disc_thm =
16.319 - let
16.320 - fun mk_core f sels = Term.list_comb (f, map (fn sel => sel $ v) sels);
16.321 - fun mk_rhs _ [f] [sels] = mk_core f sels
16.322 - | mk_rhs (disc :: discs) (f :: fs) (sels :: selss) =
16.323 - Const (@{const_name If}, HOLogic.boolT --> B --> B --> B) $
16.324 - (disc $ v) $ mk_core f sels $ mk_rhs discs fs selss;
16.325 - val goal = mk_Trueprop_eq (caseofB_fs $ v, mk_rhs discs fs selss);
16.326 - in
16.327 - Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
16.328 - mk_case_disc_tac ctxt exhaust_thm' case_thms disc_thmss' sel_thmss)
16.329 - |> singleton (Proof_Context.export names_lthy lthy)
16.330 - end;
16.331 -
16.332 - val (case_cong_thm, weak_case_cong_thm) =
16.333 - let
16.334 - fun mk_prem xctr xs f g =
16.335 - fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (w, xctr),
16.336 - mk_Trueprop_eq (f, g)));
16.337 -
16.338 - val v_eq_w = mk_Trueprop_eq (v, w);
16.339 - val caseof_fs = mk_caseofB_term eta_fs;
16.340 - val caseof_gs = mk_caseofB_term eta_gs;
16.341 -
16.342 - val goal =
16.343 - Logic.list_implies (v_eq_w :: map4 mk_prem xctrs xss fs gs,
16.344 - mk_Trueprop_eq (caseof_fs $ v, caseof_gs $ w));
16.345 - val goal_weak =
16.346 - Logic.mk_implies (v_eq_w, mk_Trueprop_eq (caseof_fs $ v, caseof_fs $ w));
16.347 - in
16.348 - (Skip_Proof.prove lthy [] [] goal (fn _ => mk_case_cong_tac exhaust_thm' case_thms),
16.349 - Skip_Proof.prove lthy [] [] goal_weak (K (etac arg_cong 1)))
16.350 - |> pairself (singleton (Proof_Context.export names_lthy lthy))
16.351 - end;
16.352 -
16.353 - val (split_thm, split_asm_thm) =
16.354 - let
16.355 - fun mk_conjunct xctr xs f_xs =
16.356 - list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (v, xctr), q $ f_xs));
16.357 - fun mk_disjunct xctr xs f_xs =
16.358 - list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (v, xctr),
16.359 - HOLogic.mk_not (q $ f_xs)));
16.360 -
16.361 - val lhs = q $ (mk_caseofB_term eta_fs $ v);
16.362 -
16.363 - val goal =
16.364 - mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs));
16.365 - val goal_asm =
16.366 - mk_Trueprop_eq (lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj
16.367 - (map3 mk_disjunct xctrs xss xfs)));
16.368 -
16.369 - val split_thm =
16.370 - Skip_Proof.prove lthy [] [] goal
16.371 - (fn _ => mk_split_tac exhaust_thm' case_thms inject_thmss distinct_thmsss)
16.372 - |> singleton (Proof_Context.export names_lthy lthy)
16.373 - val split_asm_thm =
16.374 - Skip_Proof.prove lthy [] [] goal_asm (fn {context = ctxt, ...} =>
16.375 - mk_split_asm_tac ctxt split_thm)
16.376 - |> singleton (Proof_Context.export names_lthy lthy)
16.377 - in
16.378 - (split_thm, split_asm_thm)
16.379 - end;
16.380 -
16.381 - (* TODO: case syntax *)
16.382 - (* TODO: attributes (simp, case_names, etc.) *)
16.383 -
16.384 - val notes =
16.385 - [(case_congN, [case_cong_thm]),
16.386 - (case_discsN, [case_disc_thm]),
16.387 - (casesN, case_thms),
16.388 - (ctr_selsN, ctr_sel_thms),
16.389 - (discsN, (flat disc_thmss)),
16.390 - (disc_exclusN, disc_exclus_thms),
16.391 - (disc_exhaustN, [disc_exhaust_thm]),
16.392 - (distinctN, distinct_thms),
16.393 - (exhaustN, [exhaust_thm]),
16.394 - (injectN, (flat inject_thmss)),
16.395 - (nchotomyN, [nchotomy_thm]),
16.396 - (selsN, (flat sel_thmss)),
16.397 - (splitN, [split_thm]),
16.398 - (split_asmN, [split_asm_thm]),
16.399 - (weak_case_cong_thmsN, [weak_case_cong_thm])]
16.400 - |> map (fn (thmN, thms) =>
16.401 - ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
16.402 - in
16.403 - lthy |> Local_Theory.notes notes |> snd
16.404 - end;
16.405 - in
16.406 - (goals, after_qed, lthy')
16.407 - end;
16.408 -
16.409 -val parse_bindings = Parse.$$$ "[" |-- Parse.list Parse.binding --| Parse.$$$ "]";
16.410 -
16.411 -val parse_bindingss = Parse.$$$ "[" |-- Parse.list parse_bindings --| Parse.$$$ "]";
16.412 -
16.413 -val bnf_sugar_cmd = (fn (goalss, after_qed, lthy) =>
16.414 - Proof.theorem NONE after_qed (map (map (rpair [])) goalss) lthy) oo
16.415 - prepare_sugar Syntax.read_term;
16.416 -
16.417 -val _ =
16.418 - Outer_Syntax.local_theory_to_proof @{command_spec "bnf_sugar"} "adds sugar on top of a BNF"
16.419 - (((Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") -- Parse.term --
16.420 - Scan.optional (parse_bindings -- Scan.optional parse_bindingss []) ([], []))
16.421 - >> bnf_sugar_cmd);
16.422 -
16.423 -end;
17.1 --- a/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML Mon Sep 03 11:30:29 2012 +0200
17.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
17.3 @@ -1,93 +0,0 @@
17.4 -(* Title: HOL/Codatatype/Tools/bnf_sugar_tactics.ML
17.5 - Author: Jasmin Blanchette, TU Muenchen
17.6 - Copyright 2012
17.7 -
17.8 -Tactics for sugar on top of a BNF.
17.9 -*)
17.10 -
17.11 -signature BNF_SUGAR_TACTICS =
17.12 -sig
17.13 - val mk_case_cong_tac: thm -> thm list -> tactic
17.14 - val mk_case_disc_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> tactic
17.15 - val mk_ctr_sel_tac: Proof.context -> int -> thm -> thm list -> tactic
17.16 - val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
17.17 - val mk_half_disc_exclus_tac: int -> thm -> thm -> tactic
17.18 - val mk_nchotomy_tac: int -> thm -> tactic
17.19 - val mk_other_half_disc_exclus_tac: thm -> tactic
17.20 - val mk_split_tac: thm -> thm list -> thm list list -> thm list list list -> tactic
17.21 - val mk_split_asm_tac: Proof.context -> thm -> tactic
17.22 -end;
17.23 -
17.24 -structure BNF_Sugar_Tactics : BNF_SUGAR_TACTICS =
17.25 -struct
17.26 -
17.27 -open BNF_Util
17.28 -open BNF_Tactics
17.29 -open BNF_FP_Util
17.30 -
17.31 -fun triangle _ [] = []
17.32 - | triangle k (xs :: xss) = take k xs :: triangle (k + 1) xss
17.33 -
17.34 -fun mk_if_P_or_not_P thm =
17.35 - thm RS @{thm if_not_P} handle THM _ => thm RS @{thm if_P}
17.36 -
17.37 -fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms
17.38 -
17.39 -fun mk_nchotomy_tac n exhaust =
17.40 - (rtac allI THEN' rtac exhaust THEN'
17.41 - EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1;
17.42 -
17.43 -fun mk_half_disc_exclus_tac m discD disc'_thm =
17.44 - (dtac discD THEN'
17.45 - REPEAT_DETERM_N m o etac exE THEN'
17.46 - hyp_subst_tac THEN'
17.47 - rtac disc'_thm) 1;
17.48 -
17.49 -fun mk_other_half_disc_exclus_tac half_thm =
17.50 - (etac @{thm contrapos_pn} THEN' etac half_thm) 1;
17.51 -
17.52 -fun mk_disc_exhaust_tac n exhaust discIs =
17.53 - (rtac exhaust THEN'
17.54 - EVERY' (map2 (fn k => fn discI =>
17.55 - dtac discI THEN' select_prem_tac n (etac @{thm meta_mp}) k THEN' atac) (1 upto n) discIs)) 1;
17.56 -
17.57 -fun mk_ctr_sel_tac ctxt m discD sel_thms =
17.58 - (dtac discD THEN'
17.59 - (if m = 0 then
17.60 - atac
17.61 - else
17.62 - REPEAT_DETERM_N m o etac exE THEN'
17.63 - hyp_subst_tac THEN'
17.64 - SELECT_GOAL (Local_Defs.unfold_tac ctxt sel_thms) THEN'
17.65 - rtac refl)) 1;
17.66 -
17.67 -fun mk_case_disc_tac ctxt exhaust' case_thms disc_thmss' sel_thmss =
17.68 - (rtac exhaust' THEN'
17.69 - EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms => EVERY' [
17.70 - hyp_subst_tac THEN'
17.71 - SELECT_GOAL (Local_Defs.unfold_tac ctxt (if_disc_thms @ sel_thms)) THEN'
17.72 - rtac case_thm]) case_thms
17.73 - (map (map mk_if_P_or_not_P) (triangle 1 (map (fst o split_last) disc_thmss'))) sel_thmss)) 1;
17.74 -
17.75 -fun mk_case_cong_tac exhaust' case_thms =
17.76 - (rtac exhaust' THEN'
17.77 - EVERY' (maps (fn case_thm => [dtac sym, asm_simp_tac (ss_only [case_thm])]) case_thms)) 1;
17.78 -
17.79 -val naked_ctxt = Proof_Context.init_global @{theory HOL};
17.80 -
17.81 -fun mk_split_tac exhaust' case_thms injectss distinctsss =
17.82 - rtac exhaust' 1 THEN
17.83 - ALLGOALS (fn k =>
17.84 - (hyp_subst_tac THEN'
17.85 - simp_tac (ss_only (@{thms simp_thms} @ case_thms @ nth injectss (k - 1) @
17.86 - flat (nth distinctsss (k - 1))))) k) THEN
17.87 - ALLGOALS (blast_tac naked_ctxt);
17.88 -
17.89 -val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
17.90 -
17.91 -fun mk_split_asm_tac ctxt split =
17.92 - rtac (split RS trans) 1 THEN
17.93 - Local_Defs.unfold_tac ctxt split_asm_thms THEN
17.94 - rtac refl 1;
17.95 -
17.96 -end;
18.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
18.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Mon Sep 03 11:54:21 2012 +0200
18.3 @@ -0,0 +1,420 @@
18.4 +(* Title: HOL/Codatatype/Tools/bnf_wrap.ML
18.5 + Author: Jasmin Blanchette, TU Muenchen
18.6 + Copyright 2012
18.7 +
18.8 +Wrapping existing datatypes.
18.9 +*)
18.10 +
18.11 +signature BNF_WRAP =
18.12 +sig
18.13 +end;
18.14 +
18.15 +structure BNF_Wrap : BNF_WRAP =
18.16 +struct
18.17 +
18.18 +open BNF_Util
18.19 +open BNF_FP_Util
18.20 +open BNF_Wrap_Tactics
18.21 +
18.22 +val is_N = "is_";
18.23 +val un_N = "un_";
18.24 +fun mk_un_N 1 1 suf = un_N ^ suf
18.25 + | mk_un_N _ l suf = un_N ^ suf ^ string_of_int l;
18.26 +
18.27 +val case_congN = "case_cong";
18.28 +val case_discsN = "case_discs";
18.29 +val casesN = "cases";
18.30 +val ctr_selsN = "ctr_sels";
18.31 +val disc_exclusN = "disc_exclus";
18.32 +val disc_exhaustN = "disc_exhaust";
18.33 +val discsN = "discs";
18.34 +val distinctN = "distinct";
18.35 +val selsN = "sels";
18.36 +val splitN = "split";
18.37 +val split_asmN = "split_asm";
18.38 +val weak_case_cong_thmsN = "weak_case_cong";
18.39 +
18.40 +val default_name = @{binding _};
18.41 +
18.42 +fun pad_list x n xs = xs @ replicate (n - length xs) x;
18.43 +
18.44 +fun mk_half_pairss' _ [] = []
18.45 + | mk_half_pairss' indent (y :: ys) =
18.46 + indent @ fold_rev (cons o single o pair y) ys (mk_half_pairss' ([] :: indent) ys);
18.47 +
18.48 +fun mk_half_pairss ys = mk_half_pairss' [[]] ys;
18.49 +
18.50 +val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
18.51 +
18.52 +fun mk_undef T Ts = Const (@{const_name undefined}, Ts ---> T);
18.53 +
18.54 +fun eta_expand_caseof_arg xs f_xs = fold_rev Term.lambda xs f_xs;
18.55 +
18.56 +fun name_of_ctr t =
18.57 + case head_of t of
18.58 + Const (s, _) => s
18.59 + | Free (s, _) => s
18.60 + | _ => error "Cannot extract name of constructor";
18.61 +
18.62 +fun prepare_wrap prep_term ((raw_ctrs, raw_caseof), (raw_disc_names, raw_sel_namess))
18.63 + no_defs_lthy =
18.64 + let
18.65 + (* TODO: sanity checks on arguments *)
18.66 +
18.67 + (* TODO: normalize types of constructors w.r.t. each other *)
18.68 +
18.69 + val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs;
18.70 + val caseof0 = prep_term no_defs_lthy raw_caseof;
18.71 +
18.72 + val n = length ctrs0;
18.73 + val ks = 1 upto n;
18.74 +
18.75 + val (T_name, As0) = dest_Type (body_type (fastype_of (hd ctrs0)));
18.76 + val b = Binding.qualified_name T_name;
18.77 +
18.78 + val (As, B) =
18.79 + no_defs_lthy
18.80 + |> mk_TFrees (length As0)
18.81 + ||> the_single o fst o mk_TFrees 1;
18.82 +
18.83 + fun mk_ctr Ts ctr =
18.84 + let val Ts0 = snd (dest_Type (body_type (fastype_of ctr))) in
18.85 + Term.subst_atomic_types (Ts0 ~~ Ts) ctr
18.86 + end;
18.87 +
18.88 + val T = Type (T_name, As);
18.89 + val ctrs = map (mk_ctr As) ctrs0;
18.90 + val ctr_Tss = map (binder_types o fastype_of) ctrs;
18.91 +
18.92 + val ms = map length ctr_Tss;
18.93 +
18.94 + val disc_names =
18.95 + pad_list default_name n raw_disc_names
18.96 + |> map2 (fn ctr => fn disc =>
18.97 + if Binding.eq_name (disc, default_name) then
18.98 + Binding.name (prefix is_N (Long_Name.base_name (name_of_ctr ctr)))
18.99 + else
18.100 + disc) ctrs0;
18.101 +
18.102 + val sel_namess =
18.103 + pad_list [] n raw_sel_namess
18.104 + |> map3 (fn ctr => fn m => map2 (fn l => fn sel =>
18.105 + if Binding.eq_name (sel, default_name) then
18.106 + Binding.name (mk_un_N m l (Long_Name.base_name (name_of_ctr ctr)))
18.107 + else
18.108 + sel) (1 upto m) o pad_list default_name m) ctrs0 ms;
18.109 +
18.110 + fun mk_caseof Ts T =
18.111 + let val (binders, body) = strip_type (fastype_of caseof0) in
18.112 + Term.subst_atomic_types ((body, T) :: (snd (dest_Type (List.last binders)) ~~ Ts)) caseof0
18.113 + end;
18.114 +
18.115 + val caseofB = mk_caseof As B;
18.116 + val caseofB_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
18.117 +
18.118 + fun mk_caseofB_term eta_fs = Term.list_comb (caseofB, eta_fs);
18.119 +
18.120 + val (((((((xss, yss), fs), gs), (v, v')), w), (p, p')), names_lthy) = no_defs_lthy |>
18.121 + mk_Freess "x" ctr_Tss
18.122 + ||>> mk_Freess "y" ctr_Tss
18.123 + ||>> mk_Frees "f" caseofB_Ts
18.124 + ||>> mk_Frees "g" caseofB_Ts
18.125 + ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "v") T
18.126 + ||>> yield_singleton (mk_Frees "w") T
18.127 + ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT;
18.128 +
18.129 + val q = Free (fst p', B --> HOLogic.boolT);
18.130 +
18.131 + val xctrs = map2 (curry Term.list_comb) ctrs xss;
18.132 + val yctrs = map2 (curry Term.list_comb) ctrs yss;
18.133 +
18.134 + val xfs = map2 (curry Term.list_comb) fs xss;
18.135 + val xgs = map2 (curry Term.list_comb) gs xss;
18.136 +
18.137 + val eta_fs = map2 eta_expand_caseof_arg xss xfs;
18.138 + val eta_gs = map2 eta_expand_caseof_arg xss xgs;
18.139 +
18.140 + val caseofB_fs = Term.list_comb (caseofB, eta_fs);
18.141 +
18.142 + val exist_xs_v_eq_ctrs =
18.143 + map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (v, xctr))) xctrs xss;
18.144 +
18.145 + fun mk_sel_caseof_args k xs x T =
18.146 + map2 (fn Ts => fn i => if i = k then fold_rev Term.lambda xs x else mk_undef T Ts) ctr_Tss ks;
18.147 +
18.148 + fun disc_spec b exist_xs_v_eq_ctr =
18.149 + mk_Trueprop_eq (Free (Binding.name_of b, T --> HOLogic.boolT) $ v, exist_xs_v_eq_ctr);
18.150 +
18.151 + fun sel_spec b x xs k =
18.152 + let val T' = fastype_of x in
18.153 + mk_Trueprop_eq (Free (Binding.name_of b, T --> T') $ v,
18.154 + Term.list_comb (mk_caseof As T', mk_sel_caseof_args k xs x T') $ v)
18.155 + end;
18.156 +
18.157 + val (((raw_discs, (_, raw_disc_defs)), (raw_selss, (_, raw_sel_defss))), (lthy', lthy)) =
18.158 + no_defs_lthy
18.159 + |> apfst (apsnd split_list o split_list) o fold_map2 (fn b => fn exist_xs_v_eq_ctr =>
18.160 + Specification.definition (SOME (b, NONE, NoSyn),
18.161 + ((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr))) disc_names exist_xs_v_eq_ctrs
18.162 + ||>> apfst (apsnd split_list o split_list) o fold_map3 (fn bs => fn xs => fn k =>
18.163 + apfst (apsnd split_list o split_list) o fold_map2 (fn b => fn x =>
18.164 + Specification.definition (SOME (b, NONE, NoSyn),
18.165 + ((Thm.def_binding b, []), sel_spec b x xs k))) bs xs) sel_namess xss ks
18.166 + ||> `Local_Theory.restore;
18.167 +
18.168 + (*transforms defined frees into consts (and more)*)
18.169 + val phi = Proof_Context.export_morphism lthy lthy';
18.170 +
18.171 + val disc_defs = map (Morphism.thm phi) raw_disc_defs;
18.172 + val sel_defss = map (map (Morphism.thm phi)) raw_sel_defss;
18.173 +
18.174 + val discs0 = map (Morphism.term phi) raw_discs;
18.175 + val selss0 = map (map (Morphism.term phi)) raw_selss;
18.176 +
18.177 + fun mk_disc_or_sel Ts t =
18.178 + Term.subst_atomic_types (snd (dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
18.179 +
18.180 + val discs = map (mk_disc_or_sel As) discs0;
18.181 + val selss = map (map (mk_disc_or_sel As)) selss0;
18.182 +
18.183 + fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p);
18.184 +
18.185 + val goal_exhaust =
18.186 + let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (v, xctr)]) in
18.187 + mk_imp_p (map2 mk_prem xctrs xss)
18.188 + end;
18.189 +
18.190 + val goal_injectss =
18.191 + let
18.192 + fun mk_goal _ _ [] [] = []
18.193 + | mk_goal xctr yctr xs ys =
18.194 + [mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr),
18.195 + Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys))];
18.196 + in
18.197 + map4 mk_goal xctrs yctrs xss yss
18.198 + end;
18.199 +
18.200 + val goal_half_distinctss =
18.201 + map (map (HOLogic.mk_Trueprop o HOLogic.mk_not o HOLogic.mk_eq)) (mk_half_pairss xctrs);
18.202 +
18.203 + val goal_cases = map2 (fn xctr => fn xf => mk_Trueprop_eq (caseofB_fs $ xctr, xf)) xctrs xfs;
18.204 +
18.205 + val goals = [goal_exhaust] :: goal_injectss @ goal_half_distinctss @ [goal_cases];
18.206 +
18.207 + fun after_qed thmss lthy =
18.208 + let
18.209 + val ([exhaust_thm], (inject_thmss, (half_distinct_thmss, [case_thms]))) =
18.210 + (hd thmss, apsnd (chop (n * n)) (chop n (tl thmss)));
18.211 +
18.212 + val exhaust_thm' =
18.213 + let val Tinst = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As) in
18.214 + Drule.instantiate' [] [SOME (certify lthy v)]
18.215 + (Thm.instantiate (Tinst, []) (Drule.zero_var_indexes exhaust_thm))
18.216 + end;
18.217 +
18.218 + val other_half_distinct_thmss = map (map (fn thm => thm RS not_sym)) half_distinct_thmss;
18.219 +
18.220 + val (distinct_thmsss', distinct_thmsss) =
18.221 + map2 (map2 append) (Library.chop_groups n half_distinct_thmss)
18.222 + (transpose (Library.chop_groups n other_half_distinct_thmss))
18.223 + |> `transpose;
18.224 + val distinct_thms = interleave (flat half_distinct_thmss) (flat other_half_distinct_thmss);
18.225 +
18.226 + val nchotomy_thm =
18.227 + let
18.228 + val goal =
18.229 + HOLogic.mk_Trueprop (HOLogic.mk_all (fst v', snd v',
18.230 + Library.foldr1 HOLogic.mk_disj exist_xs_v_eq_ctrs));
18.231 + in
18.232 + Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm)
18.233 + end;
18.234 +
18.235 + val sel_thmss =
18.236 + let
18.237 + fun mk_thm k xs goal_case case_thm x sel_def =
18.238 + let
18.239 + val T = fastype_of x;
18.240 + val cTs =
18.241 + map ((fn T' => certifyT lthy (if T' = B then T else T')) o TFree)
18.242 + (rev (Term.add_tfrees goal_case []));
18.243 + val cxs = map (certify lthy) (mk_sel_caseof_args k xs x T);
18.244 + in
18.245 + Local_Defs.fold lthy [sel_def]
18.246 + (Drule.instantiate' (map SOME cTs) (map SOME cxs) case_thm)
18.247 + end;
18.248 + fun mk_thms k xs goal_case case_thm sel_defs =
18.249 + map2 (mk_thm k xs goal_case case_thm) xs sel_defs;
18.250 + in
18.251 + map5 mk_thms ks xss goal_cases case_thms sel_defss
18.252 + end;
18.253 +
18.254 + val discD_thms = map (fn def => def RS iffD1) disc_defs;
18.255 + val discI_thms =
18.256 + map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms disc_defs;
18.257 + val not_disc_thms =
18.258 + map2 (fn m => fn def => funpow m (fn thm => allI RS thm)
18.259 + (Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]})))
18.260 + ms disc_defs;
18.261 +
18.262 + val (disc_thmss', disc_thmss) =
18.263 + let
18.264 + fun mk_thm discI _ [] = refl RS discI
18.265 + | mk_thm _ not_disc [distinct] = distinct RS not_disc;
18.266 + fun mk_thms discI not_disc distinctss = map (mk_thm discI not_disc) distinctss;
18.267 + in
18.268 + map3 mk_thms discI_thms not_disc_thms distinct_thmsss'
18.269 + |> `transpose
18.270 + end;
18.271 +
18.272 + val disc_exclus_thms =
18.273 + let
18.274 + fun mk_goal ((_, disc), (_, disc')) =
18.275 + Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v),
18.276 + HOLogic.mk_Trueprop (HOLogic.mk_not (disc' $ v))));
18.277 + fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac);
18.278 +
18.279 + val bundles = ms ~~ discD_thms ~~ discs;
18.280 + val half_pairss = mk_half_pairss bundles;
18.281 +
18.282 + val goal_halvess = map (map mk_goal) half_pairss;
18.283 + val half_thmss =
18.284 + map3 (fn [] => K (K [])
18.285 + | [(((m, discD), _), _)] => fn disc_thm => fn [goal] =>
18.286 + [prove (mk_half_disc_exclus_tac m discD disc_thm) goal])
18.287 + half_pairss (flat disc_thmss') goal_halvess;
18.288 +
18.289 + val goal_other_halvess = map (map (mk_goal o swap)) half_pairss;
18.290 + val other_half_thmss =
18.291 + map2 (map2 (prove o mk_other_half_disc_exclus_tac)) half_thmss goal_other_halvess;
18.292 + in
18.293 + interleave (flat half_thmss) (flat other_half_thmss)
18.294 + end;
18.295 +
18.296 + val disc_exhaust_thm =
18.297 + let
18.298 + fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (disc $ v)];
18.299 + val goal = fold Logic.all [p, v] (mk_imp_p (map mk_prem discs));
18.300 + in
18.301 + Skip_Proof.prove lthy [] [] goal (fn _ => mk_disc_exhaust_tac n exhaust_thm discI_thms)
18.302 + end;
18.303 +
18.304 + val ctr_sel_thms =
18.305 + let
18.306 + fun mk_goal ctr disc sels =
18.307 + Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v),
18.308 + mk_Trueprop_eq ((null sels ? swap)
18.309 + (Term.list_comb (ctr, map (fn sel => sel $ v) sels), v))));
18.310 + val goals = map3 mk_goal ctrs discs selss;
18.311 + in
18.312 + map4 (fn goal => fn m => fn discD => fn sel_thms =>
18.313 + Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
18.314 + mk_ctr_sel_tac ctxt m discD sel_thms))
18.315 + goals ms discD_thms sel_thmss
18.316 + end;
18.317 +
18.318 + val case_disc_thm =
18.319 + let
18.320 + fun mk_core f sels = Term.list_comb (f, map (fn sel => sel $ v) sels);
18.321 + fun mk_rhs _ [f] [sels] = mk_core f sels
18.322 + | mk_rhs (disc :: discs) (f :: fs) (sels :: selss) =
18.323 + Const (@{const_name If}, HOLogic.boolT --> B --> B --> B) $
18.324 + (disc $ v) $ mk_core f sels $ mk_rhs discs fs selss;
18.325 + val goal = mk_Trueprop_eq (caseofB_fs $ v, mk_rhs discs fs selss);
18.326 + in
18.327 + Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
18.328 + mk_case_disc_tac ctxt exhaust_thm' case_thms disc_thmss' sel_thmss)
18.329 + |> singleton (Proof_Context.export names_lthy lthy)
18.330 + end;
18.331 +
18.332 + val (case_cong_thm, weak_case_cong_thm) =
18.333 + let
18.334 + fun mk_prem xctr xs f g =
18.335 + fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (w, xctr),
18.336 + mk_Trueprop_eq (f, g)));
18.337 +
18.338 + val v_eq_w = mk_Trueprop_eq (v, w);
18.339 + val caseof_fs = mk_caseofB_term eta_fs;
18.340 + val caseof_gs = mk_caseofB_term eta_gs;
18.341 +
18.342 + val goal =
18.343 + Logic.list_implies (v_eq_w :: map4 mk_prem xctrs xss fs gs,
18.344 + mk_Trueprop_eq (caseof_fs $ v, caseof_gs $ w));
18.345 + val goal_weak =
18.346 + Logic.mk_implies (v_eq_w, mk_Trueprop_eq (caseof_fs $ v, caseof_fs $ w));
18.347 + in
18.348 + (Skip_Proof.prove lthy [] [] goal (fn _ => mk_case_cong_tac exhaust_thm' case_thms),
18.349 + Skip_Proof.prove lthy [] [] goal_weak (K (etac arg_cong 1)))
18.350 + |> pairself (singleton (Proof_Context.export names_lthy lthy))
18.351 + end;
18.352 +
18.353 + val (split_thm, split_asm_thm) =
18.354 + let
18.355 + fun mk_conjunct xctr xs f_xs =
18.356 + list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (v, xctr), q $ f_xs));
18.357 + fun mk_disjunct xctr xs f_xs =
18.358 + list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (v, xctr),
18.359 + HOLogic.mk_not (q $ f_xs)));
18.360 +
18.361 + val lhs = q $ (mk_caseofB_term eta_fs $ v);
18.362 +
18.363 + val goal =
18.364 + mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs));
18.365 + val goal_asm =
18.366 + mk_Trueprop_eq (lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj
18.367 + (map3 mk_disjunct xctrs xss xfs)));
18.368 +
18.369 + val split_thm =
18.370 + Skip_Proof.prove lthy [] [] goal
18.371 + (fn _ => mk_split_tac exhaust_thm' case_thms inject_thmss distinct_thmsss)
18.372 + |> singleton (Proof_Context.export names_lthy lthy)
18.373 + val split_asm_thm =
18.374 + Skip_Proof.prove lthy [] [] goal_asm (fn {context = ctxt, ...} =>
18.375 + mk_split_asm_tac ctxt split_thm)
18.376 + |> singleton (Proof_Context.export names_lthy lthy)
18.377 + in
18.378 + (split_thm, split_asm_thm)
18.379 + end;
18.380 +
18.381 + (* TODO: case syntax *)
18.382 + (* TODO: attributes (simp, case_names, etc.) *)
18.383 +
18.384 + val notes =
18.385 + [(case_congN, [case_cong_thm]),
18.386 + (case_discsN, [case_disc_thm]),
18.387 + (casesN, case_thms),
18.388 + (ctr_selsN, ctr_sel_thms),
18.389 + (discsN, (flat disc_thmss)),
18.390 + (disc_exclusN, disc_exclus_thms),
18.391 + (disc_exhaustN, [disc_exhaust_thm]),
18.392 + (distinctN, distinct_thms),
18.393 + (exhaustN, [exhaust_thm]),
18.394 + (injectN, (flat inject_thmss)),
18.395 + (nchotomyN, [nchotomy_thm]),
18.396 + (selsN, (flat sel_thmss)),
18.397 + (splitN, [split_thm]),
18.398 + (split_asmN, [split_asm_thm]),
18.399 + (weak_case_cong_thmsN, [weak_case_cong_thm])]
18.400 + |> map (fn (thmN, thms) =>
18.401 + ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
18.402 + in
18.403 + lthy |> Local_Theory.notes notes |> snd
18.404 + end;
18.405 + in
18.406 + (goals, after_qed, lthy')
18.407 + end;
18.408 +
18.409 +val parse_bindings = Parse.$$$ "[" |-- Parse.list Parse.binding --| Parse.$$$ "]";
18.410 +
18.411 +val parse_bindingss = Parse.$$$ "[" |-- Parse.list parse_bindings --| Parse.$$$ "]";
18.412 +
18.413 +val wrap_data_cmd = (fn (goalss, after_qed, lthy) =>
18.414 + Proof.theorem NONE after_qed (map (map (rpair [])) goalss) lthy) oo
18.415 + prepare_wrap Syntax.read_term;
18.416 +
18.417 +val _ =
18.418 + Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wraps an existing datatype"
18.419 + (((Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") -- Parse.term --
18.420 + Scan.optional (parse_bindings -- Scan.optional parse_bindingss []) ([], []))
18.421 + >> wrap_data_cmd);
18.422 +
18.423 +end;
19.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
19.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML Mon Sep 03 11:54:21 2012 +0200
19.3 @@ -0,0 +1,93 @@
19.4 +(* Title: HOL/Codatatype/Tools/bnf_wrap_tactics.ML
19.5 + Author: Jasmin Blanchette, TU Muenchen
19.6 + Copyright 2012
19.7 +
19.8 +Tactics for wrapping datatypes.
19.9 +*)
19.10 +
19.11 +signature BNF_WRAP_TACTICS =
19.12 +sig
19.13 + val mk_case_cong_tac: thm -> thm list -> tactic
19.14 + val mk_case_disc_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> tactic
19.15 + val mk_ctr_sel_tac: Proof.context -> int -> thm -> thm list -> tactic
19.16 + val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
19.17 + val mk_half_disc_exclus_tac: int -> thm -> thm -> tactic
19.18 + val mk_nchotomy_tac: int -> thm -> tactic
19.19 + val mk_other_half_disc_exclus_tac: thm -> tactic
19.20 + val mk_split_tac: thm -> thm list -> thm list list -> thm list list list -> tactic
19.21 + val mk_split_asm_tac: Proof.context -> thm -> tactic
19.22 +end;
19.23 +
19.24 +structure BNF_Wrap_Tactics : BNF_WRAP_TACTICS =
19.25 +struct
19.26 +
19.27 +open BNF_Util
19.28 +open BNF_Tactics
19.29 +open BNF_FP_Util
19.30 +
19.31 +fun triangle _ [] = []
19.32 + | triangle k (xs :: xss) = take k xs :: triangle (k + 1) xss
19.33 +
19.34 +fun mk_if_P_or_not_P thm =
19.35 + thm RS @{thm if_not_P} handle THM _ => thm RS @{thm if_P}
19.36 +
19.37 +fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms
19.38 +
19.39 +fun mk_nchotomy_tac n exhaust =
19.40 + (rtac allI THEN' rtac exhaust THEN'
19.41 + EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1;
19.42 +
19.43 +fun mk_half_disc_exclus_tac m discD disc'_thm =
19.44 + (dtac discD THEN'
19.45 + REPEAT_DETERM_N m o etac exE THEN'
19.46 + hyp_subst_tac THEN'
19.47 + rtac disc'_thm) 1;
19.48 +
19.49 +fun mk_other_half_disc_exclus_tac half_thm =
19.50 + (etac @{thm contrapos_pn} THEN' etac half_thm) 1;
19.51 +
19.52 +fun mk_disc_exhaust_tac n exhaust discIs =
19.53 + (rtac exhaust THEN'
19.54 + EVERY' (map2 (fn k => fn discI =>
19.55 + dtac discI THEN' select_prem_tac n (etac @{thm meta_mp}) k THEN' atac) (1 upto n) discIs)) 1;
19.56 +
19.57 +fun mk_ctr_sel_tac ctxt m discD sel_thms =
19.58 + (dtac discD THEN'
19.59 + (if m = 0 then
19.60 + atac
19.61 + else
19.62 + REPEAT_DETERM_N m o etac exE THEN'
19.63 + hyp_subst_tac THEN'
19.64 + SELECT_GOAL (Local_Defs.unfold_tac ctxt sel_thms) THEN'
19.65 + rtac refl)) 1;
19.66 +
19.67 +fun mk_case_disc_tac ctxt exhaust' case_thms disc_thmss' sel_thmss =
19.68 + (rtac exhaust' THEN'
19.69 + EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms => EVERY' [
19.70 + hyp_subst_tac THEN'
19.71 + SELECT_GOAL (Local_Defs.unfold_tac ctxt (if_disc_thms @ sel_thms)) THEN'
19.72 + rtac case_thm]) case_thms
19.73 + (map (map mk_if_P_or_not_P) (triangle 1 (map (fst o split_last) disc_thmss'))) sel_thmss)) 1;
19.74 +
19.75 +fun mk_case_cong_tac exhaust' case_thms =
19.76 + (rtac exhaust' THEN'
19.77 + EVERY' (maps (fn case_thm => [dtac sym, asm_simp_tac (ss_only [case_thm])]) case_thms)) 1;
19.78 +
19.79 +val naked_ctxt = Proof_Context.init_global @{theory HOL};
19.80 +
19.81 +fun mk_split_tac exhaust' case_thms injectss distinctsss =
19.82 + rtac exhaust' 1 THEN
19.83 + ALLGOALS (fn k =>
19.84 + (hyp_subst_tac THEN'
19.85 + simp_tac (ss_only (@{thms simp_thms} @ case_thms @ nth injectss (k - 1) @
19.86 + flat (nth distinctsss (k - 1))))) k) THEN
19.87 + ALLGOALS (blast_tac naked_ctxt);
19.88 +
19.89 +val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
19.90 +
19.91 +fun mk_split_asm_tac ctxt split =
19.92 + rtac (split RS trans) 1 THEN
19.93 + Local_Defs.unfold_tac ctxt split_asm_thms THEN
19.94 + rtac refl 1;
19.95 +
19.96 +end;