# HG changeset patch # User blanchet # Date 1346852413 -7200 # Node ID 6407346b74c76f92b1b345a051ab87f9546460dd # Parent 2a361e09101bf4ca2c0051fe2cfadb77b7f966e0 ported "Misc_Data" to new syntax diff -r 2a361e09101b -r 6407346b74c7 src/HOL/Codatatype/Examples/Misc_Data.thy --- a/src/HOL/Codatatype/Examples/Misc_Data.thy Wed Sep 05 15:22:37 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Misc_Data.thy Wed Sep 05 15:40:13 2012 +0200 @@ -12,146 +12,139 @@ imports "../Codatatype" begin -data_raw simple: 'a = "unit + unit + unit + unit" +data simple = X1 | X2 | X3 | X4 + +data simple' = X1' unit | X2' unit | X3' unit | X4' unit -data_raw mylist: 'list = "unit + 'a \ 'list" +data 'a mylist = MyNil | MyCons 'a "'a mylist" -data_raw some_passive: 'a = "'a + 'b + 'c + 'd + 'e" +data ('b, 'c, 'd, 'e) some_passive = + SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e -data_raw lambda: - 'trm = "string + - 'trm \ 'trm + - string \ 'trm + - (string \ 'trm) fset \ 'trm" +data lambda = + Var string | + App lambda lambda | + Abs string lambda | + Let "(string \ lambda) fset" lambda -data_raw par_lambda: - 'trm = "'a + - 'trm \ 'trm + - 'a \ 'trm + - ('a \ 'trm) fset \ 'trm" +data 'a par_lambda = + PVar 'a | + PApp "'a par_lambda" "'a par_lambda" | + PAbs 'a "'a par_lambda" | + PLet "('a \ 'a par_lambda) fset" "'a par_lambda" (* ('a, 'b1, 'b2) F1 = 'a * 'b1 + 'a * 'b2 ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2 *) -data_raw F1: 'b1 = "'a \ 'b1 + 'a \ 'b2" -and F2: 'b2 = "unit + 'b1 * 'b2" +data 'a I1 = I11 'a "'a I1" | I12 'a "'a I2" + and 'a I2 = I21 | I22 "'a I1" "'a I2" -(* - 'a tree = Empty | Node of 'a * 'a forest ('b = unit + 'a * 'c) - 'a forest = Nil | Cons of 'a tree * 'a forest ('c = unit + 'b * 'c) -*) +data 'a tree = TEmpty | TNode 'a "'a forest" + and 'a forest = FNil | FCons "'a tree" "'a forest" -data_raw tree: 'tree = "unit + 'a \ 'forest" -and forest: 'forest = "unit + 'tree \ 'forest" +data 'a tree' = TEmpty' | TNode' "'a branch" "'a branch" + and 'a branch = Branch 'a "'a tree'" -(* - 'a tree = Empty | Node of 'a branch * 'a branch ('b = unit + 'c * 'c) -' a branch = Branch of 'a * 'a tree ('c = 'a * 'b) -*) +data ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp" + and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm" + and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp" -data_raw tree': 'tree = "unit + 'branch \ 'branch" -and branch: 'branch = "'a \ 'tree" +data_raw some_killing: 'A = "'a \ 'b \ ('A + 'B)" +and in_here: 'B = "'b \ 'a + 'c" -(* - exp = Sum of term * exp ('c = 'd + 'd * 'c) - term = Prod of factor * term ('d = 'e + 'e * 'd) - factor = C 'a | V 'b | Paren exp ('e = 'a + 'b + 'c) +(* FIXME +data ('a, 'b, 'c) some_killing = + SK "'a \ 'b \ ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here" + and ('a, 'b, 'c) in_here = + IH1 'b 'a | IH2 'c *) -data_raw EXPR: 'E = "'T + 'T \ 'E" -and TERM: 'T = "'F + 'F \ 'T" -and FACTOR: 'F = "'a + 'b + 'E" - -data_raw some_killing: 'a = "'b \ 'd \ ('a + 'c)" -and in_here: 'c = "'d \ 'b + 'e" - +(* FIXME data 'b nofail1 = NF11 "'a \ 'b" | NF12 'b *) 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" +data 'b nofail2 = NF2 "('b nofail2 \ 'b \ 'b nofail2 \ 'b) list" +data 'b nofail3 = NF3 "'b \ ('b nofail3 \ 'b \ 'b nofail3 \ 'b) fset" +data 'b nofail4 = NF4 "('b nofail3 \ ('b nofail3 \ 'b \ 'b nofail3 \ 'b) fset) list" (* -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" +data 'b fail = F "'b fail \ 'b \ 'b fail \ 'b list" +data 'b fail = F "'b fail \ 'b \ 'b fail \ 'b" +data 'b fail = F "'b fail \ 'b + 'b fail" +data 'b fail = F "'b fail \ 'b" *) -data_raw L1: 'L1 = "'L2 list" -and L2: 'L2 = "'L1 fset + 'L2" +data l1 = L1 "l2 list" + and l2 = L21 "l1 fset" | L22 l2 -data_raw K1: 'K1 = "'K2" -and K2: 'K2 = "'K3" -and K3: 'K3 = "'K1 list" +data kk1 = KK1 kk2 + and kk2 = KK2 kk3 + and kk3 = KK3 "kk1 list" -data_raw t1: 't1 = "'t3 + 't2" -and t2: 't2 = "'t1" -and t3: 't3 = "unit" +data t1 = T11 t3 | T12 t2 + and t2 = T2 t1 + and t3 = T3 -data_raw t1': 't1 = "'t2 + 't3" -and t2': 't2 = "'t1" -and t3': 't3 = "unit" +data t1' = T11' t2' | T12' t3' + and t2' = T2' t1' + and t3' = T3' (* -data_raw fail1: 'L1 = "'L2" -and fail2: 'L2 = "'L3" -and fail2: 'L3 = "'L1" +data fail1 = F1 fail2 + and fail2 = F2 fail3 + and fail3 = F3 fail1 -data_raw fail1: 'L1 = "'L2 list \ 'L2" -and fail2: 'L2 = "'L2 fset \ 'L3" -and fail2: 'L3 = "'L1" +data fail1 = F1 "fail2 list" fail2 + and fail2 = F2 "fail2 fset" fail3 + and fail3 = F3 fail1 -data_raw fail1: 'L1 = "'L2 list \ 'L2" -and fail2: 'L2 = "'L1 fset \ 'L1" +data fail1 = F1 "fail2 list" fail2 + and fail2 = F2 "fail1 fset" fail1 *) -(* SLOW -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" -and K5': 'K5 = "'K6" -and K6': 'K6 = "'K7" -and K7': 'K7 = "'K8" -and K8': 'K8 = "'K1 list" + +data ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list" + and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list" + and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5" + and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list" + and ('a, 'c) D5 = A5 "('a, 'c) D6" + and ('a, 'c) D6 = A6 "('a, 'c) D7" + and ('a, 'c) D7 = A7 "('a, 'c) D8" + and ('a, 'c) D8 = A8 "('a, 'c) D1 list" (*time comparison*) -datatype ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list" - and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list" - and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5" - and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list" - and ('a, 'c) D5 = A5 "('a, 'c) D6" - and ('a, 'c) D6 = A6 "('a, 'c) D7" - and ('a, 'c) D7 = A7 "('a, 'c) D8" - and ('a, 'c) D8 = A8 "('a, 'c) D1 list" -*) +datatype ('a, 'c) D1' = A1' "('a, 'c) D2'" | B1' "'a list" + and ('a, 'c) D2' = A2' "('a, 'c) D3'" | B2' "'c list" + and ('a, 'c) D3' = A3' "('a, 'c) D3'" | B3' "('a, 'c) D4'" | C3' "('a, 'c) D4'" "('a, 'c) D5'" + and ('a, 'c) D4' = A4' "('a, 'c) D5'" | B4' "'a list list list" + and ('a, 'c) D5' = A5' "('a, 'c) D6'" + and ('a, 'c) D6' = A6' "('a, 'c) D7'" + and ('a, 'c) D7' = A7' "('a, 'c) D8'" + and ('a, 'c) D8' = A8' "('a, 'c) D1' list" (* fail: -data_raw t1: 't1 = "'t2 * 't3 + 't2 * 't4" -and t2: 't2 = "unit" -and t3: 't3 = 't4 -and t4: 't4 = 't1 +data tt1 = TT11 tt2 tt3 | TT12 tt2 tt4 + and tt2 = TT2 + and tt3 = TT3 tt4 + and tt4 = TT4 tt1 *) -data_raw k1: 'k1 = "'k2 * 'k3 + 'k2 * 'k4" -and k2: 'k2 = unit -and k3: 'k3 = 'k4 -and k4: 'k4 = unit +data k1 = K11 k2 k3 | K12 k2 k4 + and k2 = K2 + and k3 = K3 k4 + and k4 = K4 -data_raw tt1: 'tt1 = "'tt3 * 'tt2 + 'tt2 * 'tt4" -and tt2: 'tt2 = unit -and tt3: 'tt3 = 'tt1 -and tt4: 'tt4 = unit -(* SLOW -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 -and s5: 's5 = unit -and s6: 's6 = "'s6 + 's1 * 's2 + 's6" -and s7: 's7 = "'s8 + 's5" -and s8: 's8 = nat -*) +data tt1 = TT11 tt3 tt2 | TT12 tt2 tt4 + and tt2 = TT2 + and tt3 = TT3 tt1 + and tt4 = TT4 + +data s1 = S11 s2 s3 s4 | S12 s3 | S13 s2 s6 | S14 s4 s2 | S15 s2 s2 + and s2 = S21 s7 s5 | S22 s5 s4 s6 + and s3 = S31 s1 s7 s2 | S32 s3 s3 | S33 s4 s5 + and s4 = S4 s5 + and s5 = S5 + and s6 = S61 s6 | S62 s1 s2 | S63 s6 + and s7 = S71 s8 | S72 s5 + and s8 = S8 nat end diff -r 2a361e09101b -r 6407346b74c7 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 05 15:22:37 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 05 15:40:13 2012 +0200 @@ -66,8 +66,10 @@ val _ = (case duplicates (op =) As of [] => () | T :: _ => error ("Duplicate type parameter " ^ quote (Syntax.string_of_typ lthy T))); + (* TODO: print timing information for sugar *) (* TODO: check that no type variables occur in the rhss that's not in the lhss *) (* TODO: use sort constraints on type args *) + (* TODO: use mixfix *) val N = length specs; diff -r 2a361e09101b -r 6407346b74c7 src/HOL/Codatatype/Tools/bnf_wrap.ML --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Wed Sep 05 15:22:37 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Wed Sep 05 15:40:13 2012 +0200 @@ -192,6 +192,9 @@ val missing_unique_disc_def = TrueI; (*arbitrary marker*) val missing_alternate_disc_def = FalseE; (*arbitrary marker*) + (* TODO: Allow use of same selector for several constructors *) + (* TODO: Allow use of same name for datatype and for constructor, e.g. "data L = L" *) + val (((raw_discs, raw_disc_defs), (raw_selss, raw_sel_defss)), (lthy', lthy)) = no_defs_lthy |> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_v_eq_ctr => @@ -301,7 +304,7 @@ map5 mk_thms ks xss goal_cases case_thms sel_defss end; - fun mk_unique_disc_def k = + fun mk_unique_disc_def () = let val m = the_single ms; val goal = mk_Trueprop_eq (mk_v_eq_v (), the_single exist_xs_v_eq_ctrs); @@ -329,7 +332,7 @@ val disc_defs' = map2 (fn k => fn def => - if Thm.eq_thm_prop (def, missing_unique_disc_def) then mk_unique_disc_def k + if Thm.eq_thm_prop (def, missing_unique_disc_def) then mk_unique_disc_def () else if Thm.eq_thm_prop (def, missing_alternate_disc_def) then mk_alternate_disc_def k else def) ks disc_defs; diff -r 2a361e09101b -r 6407346b74c7 src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML Wed Sep 05 15:22:37 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML Wed Sep 05 15:40:13 2012 +0200 @@ -89,8 +89,7 @@ fun mk_split_tac exhaust' case_thms injectss distinctsss = rtac exhaust' 1 THEN - ALLGOALS (fn k => - (hyp_subst_tac 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);