39 | Lam "rty" "name" "rtrm" |
39 | Lam "rty" "name" "rtrm" |
40 ML {* |
40 ML {* |
41 val thy1 = @{theory}; |
41 val thy1 = @{theory}; |
42 val info = Datatype.the_info @{theory} "Lift.rkind" |
42 val info = Datatype.the_info @{theory} "Lift.rkind" |
43 val number = 3; |
43 val number = 3; |
44 val binds = [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ], |
44 val binds = [[ [], [(NONE, 1, 2)]], |
45 [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ], |
45 [ [], [], [(NONE, 1, 2)] ], |
46 [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]]; |
46 [ [], [], [], [(NONE, 1, 2)]]]; |
47 val bvs = [] |
47 val bvs = [] |
48 val bv_simps = [] |
48 val bv_simps = [] |
49 |
49 |
50 val ntnames = [@{binding kind}, @{binding ty}, @{binding trm}] |
50 val ntnames = [@{binding kind}, @{binding ty}, @{binding trm}] |
51 val ncnames = ["TYP", "KPI", "TCONST", "TAPP", "TPI", "CONST", "VAR", "APP", "LAM"]*} *) |
51 val ncnames = ["TYP", "KPI", "TCONST", "TAPP", "TPI", "CONST", "VAR", "APP", "LAM"] |
52 |
52 |
53 datatype rtrm5 = |
53 (*datatype rtrm5 = |
54 rVr5 "name" |
54 rVr5 "name" |
55 | rAp5 "rtrm5" "rtrm5" |
55 | rAp5 "rtrm5" "rtrm5" |
56 | rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" |
56 | rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" |
57 and rlts = |
57 and rlts = |
58 rLnil |
58 rLnil |
62 rbv5 |
62 rbv5 |
63 where |
63 where |
64 "rbv5 rLnil = {}" |
64 "rbv5 rLnil = {}" |
65 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)" |
65 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)" |
66 |
66 |
67 ML Typedef.add_typedef |
67 ML |
68 |
|
69 ML {* |
|
70 val thy1 = @{theory}; |
68 val thy1 = @{theory}; |
71 val info = Datatype.the_info @{theory} "Lift.rtrm5" |
69 val info = Datatype.the_info @{theory} "Lift.rtrm5" |
72 val number = 2; |
70 val number = 2; |
73 val binds = [ [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] |
71 val binds = [ [[], [], [(SOME @{term rbv5}, 0, 1)]], [[], []] ] |
74 val bvs = [(@{term rbv5}, 1)] |
72 val bvs = [(@{term rbv5}, 1)] |
75 val bv_simps = @{thms rbv5.simps} |
73 val bv_simps = @{thms rbv5.simps} |
76 |
74 |
77 val ntnames = [@{binding trm5}, @{binding lts}] |
75 val ntnames = [@{binding trm5}, @{binding lts}] |
78 val ncnames = ["Vr5", "Ap5", "Lt5", "Lnil", "Lcons"] |
76 val ncnames = ["Vr5", "Ap5", "Lt5", "Lnil", "Lcons"]*) |
|
77 |
79 |
78 |
80 val descr = #descr info; |
79 val descr = #descr info; |
81 val sorts = #sorts info; |
80 val sorts = #sorts info; |
82 val nos = map fst descr |
81 val nos = map fst descr |
83 val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) nos |
82 val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) nos |
111 build_eqvts Binding.empty [t] [nth perms n] |
110 build_eqvts Binding.empty [t] [nth perms n] |
112 (bv_simps @ raw_perm_def) (nth inducts n) |
111 (bv_simps @ raw_perm_def) (nth inducts n) |
113 val (bv_eqvts, lthy3) = fold_map build_bv_eqvt bvs lthy2; |
112 val (bv_eqvts, lthy3) = fold_map build_bv_eqvt bvs lthy2; |
114 val (fv_eqvts, lthy4) = build_eqvts Binding.empty fv_ts_loc perms (fv_def_loc @ raw_perm_def) induct lthy3; |
113 val (fv_eqvts, lthy4) = build_eqvts Binding.empty fv_ts_loc perms (fv_def_loc @ raw_perm_def) induct lthy3; |
115 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy4; |
114 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy4; |
116 val alpha_eqvt = ProofContext.export lthy4 lthy1 alpha_eqvt_loc |
115 val alpha_eqvt = ProofContext.export lthy4 lthy1 alpha_eqvt_loc; |
117 val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy4; |
116 val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy4; |
118 val alpha_equivp = ProofContext.export lthy4 lthy1 alpha_equivp_loc |
117 val alpha_equivp = ProofContext.export lthy4 lthy1 alpha_equivp_loc |
119 val lthy5 = define_quotient_type |
118 val lthy5 = define_quotient_type |
120 (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((ntnames ~~ typs) ~~ alpha_ts)) |
119 (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((ntnames ~~ typs) ~~ alpha_ts)) |
121 (ALLGOALS (resolve_tac alpha_equivp)) lthy4; |
120 (ALLGOALS (resolve_tac alpha_equivp)) lthy4; |
124 map (fn (cname, dts) => |
123 map (fn (cname, dts) => |
125 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |
124 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |
126 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
125 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
127 val (csdefl, lthy6) = fold_map Quotient_Def.quotient_lift_const (ncnames ~~ consts) lthy5; |
126 val (csdefl, lthy6) = fold_map Quotient_Def.quotient_lift_const (ncnames ~~ consts) lthy5; |
128 val (cs, def) = split_list csdefl; |
127 val (cs, def) = split_list csdefl; |
129 val ((_, fv_rsp), lthy7) = prove_const_rsp Binding.empty fv_ts |
128 val (bvs_rsp', lthy7) = fold_map ( |
130 (fn _ => fvbv_rsp_tac alpha_induct fv_def 1) lthy6 |
|
131 val (bvs_rsp', lthy8) = fold_map ( |
|
132 fn (bv_t, i) => prove_const_rsp Binding.empty [bv_t] |
129 fn (bv_t, i) => prove_const_rsp Binding.empty [bv_t] |
133 (fn _ => fvbv_rsp_tac (nth alpha_inducts i) bv_simps 1)) bvs lthy7 |
130 (fn _ => fvbv_rsp_tac (nth alpha_inducts i) bv_simps 1)) bvs lthy6; |
134 val bvs_rsp = flat (map snd bvs_rsp') |
131 val ((_, fv_rsp), lthy8) = prove_const_rsp Binding.empty fv_ts |
|
132 (fn _ => fvbv_rsp_tac alpha_induct fv_def 1) lthy7; |
|
133 val bvs_rsp = flat (map snd bvs_rsp'); |
135 val (const_rsps, lthy9) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
134 val (const_rsps, lthy9) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
136 (fn _ => constr_rsp_tac alpha_inj (fv_rsp @ bvs_rsp) alpha_equivp 1)) consts lthy8 |
135 (fn _ => constr_rsp_tac alpha_inj (fv_rsp @ bvs_rsp) alpha_equivp 1)) consts lthy8 |
137 val (perms_rsp, lthy10) = prove_const_rsp Binding.empty perms |
136 val (perms_rsp, lthy10) = prove_const_rsp Binding.empty perms |
138 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy9; |
137 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy9; |
139 val thy3 = Local_Theory.exit_global lthy10; |
138 val thy3 = Local_Theory.exit_global lthy10; |
140 (* TODO: fix this hack... *) |
139 (* TODO: fix this hack... *) |
141 val tinfo = #abs_type (Typedef.the_info thy3 "Lift.trm5"); |
140 (*val tinfo = #abs_type (Typedef.the_info thy3 "Lift.trm5");*) |
142 (*val thy4 = define_lifted_perms ["Term1.trm1"] [("permute_trm1", @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"})] |
141 (*val thy4 = define_lifted_perms ["Term1.trm1"] [("permute_trm1", @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"})] |
143 @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append}*) |
142 @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append}*) |
144 val lthy11 = Theory_Target.init NONE thy3; |
143 val lthy11 = Theory_Target.init NONE thy3; |
145 val lift_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy11, induct)); |
144 val lift_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy11, induct)); |
146 val lthy12 = snd (Local_Theory.note ((@{binding lift_induct}, []), [lift_induct]) lthy11); |
145 val lthy12 = snd (Local_Theory.note ((@{binding lift_induct}, []), [lift_induct]) lthy11); |