38 ML {* |
38 ML {* |
39 print_depth 500; |
39 print_depth 500; |
40 val thy1 = @{theory}; |
40 val thy1 = @{theory}; |
41 val tnames = ["rtrm2", "ras"]; |
41 val tnames = ["rtrm2", "ras"]; |
42 val ftname = "Lift.rtrm2" |
42 val ftname = "Lift.rtrm2" |
|
43 val ntnames = [(@{binding trm2}, @{typ rtrm2}), (@{binding as}, @{typ ras})] |
43 val binds = [[[[]], [[], []], [[], [(SOME @{term rbv2}, 0)]]], |
44 val binds = [[[[]], [[], []], [[], [(SOME @{term rbv2}, 0)]]], |
44 [[[], []]] (*, [[], [[], []]] *) ]; |
45 [[[], []]] (*, [[], [[], []]] *) ]; |
45 val bv_simps = @{thms rbv2.simps} |
46 val bv_simps = @{thms rbv2.simps} |
46 val info = Datatype.the_info @{theory} ftname; |
47 val info = Datatype.the_info @{theory} ftname; |
47 val descr = #descr info; |
48 val descr = #descr info; |
53 val inject = flat (map #inject infos); |
54 val inject = flat (map #inject infos); |
54 val distinct = flat (map #distinct infos); |
55 val distinct = flat (map #distinct infos); |
55 val ((raw_perm_def, raw_perm_simps, perms), thy2) = define_raw_perms tnames full_tnames thy1; |
56 val ((raw_perm_def, raw_perm_simps, perms), thy2) = define_raw_perms tnames full_tnames thy1; |
56 val lthy1 = Theory_Target.init NONE thy2 |
57 val lthy1 = Theory_Target.init NONE thy2 |
57 val (((fv_ts_loc, fv_def_loc), alpha), lthy2) = define_fv_alpha ftname binds lthy1; |
58 val (((fv_ts_loc, fv_def_loc), alpha), lthy2) = define_fv_alpha ftname binds lthy1; |
58 val alpha_ts = #preds alpha |
59 val alpha_ts_loc = #preds alpha |
59 val alpha_intros = #intrs alpha |
60 val alpha_intros = #intrs alpha |
60 val alpha_cases = #elims alpha |
61 val alpha_cases = #elims alpha |
61 val alpha_induct = #induct alpha |
62 val alpha_induct = #induct alpha |
62 val alpha_inj = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy2 |
63 val alpha_inj = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy2 |
63 val fv_def = ProofContext.export lthy2 lthy1 fv_def_loc |
64 val fv_def = ProofContext.export lthy2 lthy1 fv_def_loc |
64 val morphism = ProofContext.export_morphism lthy2 lthy1 |
65 val morphism = ProofContext.export_morphism lthy2 lthy1 |
65 val fv_ts = map (Morphism.term morphism) fv_ts_loc |
66 val fv_ts = map (Morphism.term morphism) fv_ts_loc |
|
67 val alpha_ts = map (Morphism.term morphism) alpha_ts_loc |
66 val (bv_eqvts, lthy3) = build_eqvts @{binding bv_eqvts} [@{term rbv2}] [hd (tl perms)] |
68 val (bv_eqvts, lthy3) = build_eqvts @{binding bv_eqvts} [@{term rbv2}] [hd (tl perms)] |
67 (bv_simps @ raw_perm_def) @{thm rtrm2_ras.inducts(2)} lthy2; |
69 (bv_simps @ raw_perm_def) @{thm rtrm2_ras.inducts(2)} lthy2; |
68 val (fv_eqvts, lthy4) = build_eqvts @{binding fv_eqvts} fv_ts_loc perms (fv_def_loc @ raw_perm_def) induct lthy3; |
70 val (fv_eqvts, lthy4) = build_eqvts @{binding fv_eqvts} fv_ts_loc perms (fv_def_loc @ raw_perm_def) induct lthy3; |
69 val alpha_eqvt = build_alpha_eqvts alpha_ts perms (raw_perm_def @ alpha_inj) alpha_induct lthy4; |
71 val alpha_eqvt = build_alpha_eqvts alpha_ts_loc perms (raw_perm_def @ alpha_inj) alpha_induct lthy4; |
70 val alpha_equivp = build_equivps alpha_ts induct alpha_induct inject alpha_inj distinct alpha_cases alpha_eqvt lthy4 |
72 val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct inject alpha_inj distinct alpha_cases alpha_eqvt lthy4; |
|
73 val alpha_equivp = ProofContext.export lthy4 lthy1 alpha_equivp_loc |
|
74 val lthy5 = define_quotient_type |
|
75 (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) (ntnames ~~ alpha_ts)) |
|
76 (ALLGOALS (resolve_tac alpha_equivp)) lthy4; |
|
77 val ((c, def), lthy6) = Quotient_Def.quotient_lift_const ("Vr2", @{term rVr2}) lthy5 |
|
78 *} |
|
79 |
|
80 ML {* |
|
81 val thyf = Local_Theory.exit_global lthy6; |
|
82 *} |
|
83 setup {* fn _ => thyf *} |
|
84 print_theorems |
|
85 |
|
86 |
|
87 |
|
88 |
|
89 ML {* |
|
90 val lthy5 = define_quotient_type |
|
91 (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) (ntnames ~~ alpha_ts)) |
|
92 (ALLGOALS (resolve_tac alpha_equivp)) lthy4 |
|
93 *} |
|
94 |
|
95 ML {* |
71 |
96 |
72 *} |
97 *} |
73 |
98 |
74 |
99 |
75 |
|
76 ML {* |
|
77 val thyf = Local_Theory.exit_global lthy4 |
|
78 *} |
|
79 setup {* fn _ => thyf *} |
|
80 print_theorems |
|
81 |
|
82 ML {* |
|
83 (*val thyn = @{theory} |
|
84 val lthy3 = Theory_Target.init NONE thyn;*) |
|
85 build_equivps alpha_ts induct alpha_induct inject alpha_inj distinct alpha_cases @{thms alpha2_eqvt} lthy2 |
|
86 |
|
87 *} |
|
88 |
|
89 |
|