1 theory Lift |
1 theory Lift |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 atom_decl ident |
6 atom_decl ident |
7 |
7 |
8 datatype rtrm2 = |
8 datatype rtrm2 = |
9 rVr2 "name" |
9 rVr2 "name" |
10 | rAp2 "rtrm2" "rtrm2 list" |
10 | rAp2 "rtrm2" "rtrm2" |
11 | rLt2 "ras" "rtrm2" --"bind (bv2 l) in (r)" |
11 | rLt2 "ras" "rtrm2" --"bind (bv2 l) in (r)" |
12 and ras = |
12 and ras = |
13 rAs "name" "rtrm2" |
13 rAs "name" "rtrm2" |
14 |
14 |
15 primrec rbv2 where "rbv2 (rAs x t) = {atom x}" |
15 primrec rbv2 where "rbv2 (rAs x t) = {atom x}" |
16 |
16 |
|
17 ML {* |
|
18 val thy1 = @{theory}; |
|
19 val info = Datatype.the_info @{theory} "Lift.rtrm2" |
|
20 val number = 2; (* Number of defined types, rest are unfoldings *) |
|
21 val binds = [[[[]], [[], []], [[], [(SOME @{term rbv2}, 0)]]], |
|
22 [[[], []]] (*, [[], [[], []]] *) ]; |
|
23 val bvs = [(@{term rbv2}, 1)] (* Which type it operates on *) |
|
24 val bv_simps = @{thms rbv2.simps} |
17 |
25 |
18 ML {* |
26 val ntnames = [@{binding trm2}, @{binding as}] |
19 fun build_eqvts_ funs perms simps induct ctxt = |
27 val ncnames = ["Vr2", "Ap2", "Lt2", "As"] |
20 let |
|
21 val pi = Free ("pi", @{typ perm}); |
|
22 val types = map (domain_type o fastype_of) funs; |
|
23 val fv_indnames = Datatype_Prop.make_tnames (map body_type types); |
|
24 val args = map Free (fv_indnames ~~ types); |
|
25 val perm_at = Const (@{const_name permute}, @{typ "perm \<Rightarrow> atom set \<Rightarrow> atom set"}) |
|
26 fun eqvtc (fv, (arg, perm)) = |
|
27 HOLogic.mk_eq ((perm_at $ pi $ (fv $ arg)), (fv $ (perm $ pi $ arg))) |
|
28 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms)))) |
|
29 fun tac _ = (indtac induct fv_indnames THEN_ALL_NEW |
|
30 (asm_full_simp_tac (HOL_ss addsimps |
|
31 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))) 1 |
|
32 in |
|
33 Goal.prove ctxt ("pi" :: fv_indnames) [] gl tac |
|
34 end |
|
35 *} |
|
36 |
28 |
37 |
29 |
38 ML {* |
|
39 print_depth 500; |
|
40 val thy1 = @{theory}; |
|
41 val tnames = ["rtrm2", "ras"]; |
|
42 val ftname = "Lift.rtrm2" |
|
43 val ntnames = [(@{binding trm2}, @{typ rtrm2}), (@{binding as}, @{typ ras})] |
|
44 val binds = [[[[]], [[], []], [[], [(SOME @{term rbv2}, 0)]]], |
|
45 [[[], []]] (*, [[], [[], []]] *) ]; |
|
46 val bv_simps = @{thms rbv2.simps} |
|
47 val info = Datatype.the_info @{theory} ftname; |
|
48 *} |
|
49 |
30 |
50 . |
31 |
51 {* |
|
52 val descr = #descr info; |
32 val descr = #descr info; |
|
33 val sorts = #sorts info; |
|
34 val nos = map fst descr |
|
35 val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) nos |
|
36 val typs = List.take (all_typs, number) |
53 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
37 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
54 val full_tnames = List.take (all_full_tnames, length tnames); |
38 val full_tnames = List.take (all_full_tnames, number); |
55 val induct = #induct info; |
39 val induct = #induct info; |
56 val inducts = #inducts info; |
40 val inducts = #inducts info; |
57 val infos = map (Datatype.the_info @{theory}) all_full_tnames; |
41 val infos = map (Datatype.the_info thy1) all_full_tnames; |
58 val inject = flat (map #inject infos); |
42 val inject = flat (map #inject infos); |
59 val distinct = flat (map #distinct infos); |
43 val distinct = flat (map #distinct infos); |
60 val ((raw_perm_def, raw_perm_simps, perms), thy2) = define_raw_perms tnames full_tnames thy1; |
44 val ((raw_perm_def, raw_perm_simps, perms), thy2) = define_raw_perms info number thy1; |
61 val lthy1 = Theory_Target.init NONE thy2 |
45 val lthy1 = Theory_Target.init NONE thy2 |
62 val (((fv_ts_loc, fv_def_loc), alpha), lthy2) = define_fv_alpha ftname binds lthy1; |
46 val (((fv_ts_loc, fv_def_loc), alpha), lthy2) = define_fv_alpha info binds lthy1; |
63 val alpha_ts_loc = #preds alpha |
47 val alpha_ts_loc = #preds alpha |
64 val alpha_intros = #intrs alpha |
48 val alpha_intros = #intrs alpha |
65 val alpha_cases = #elims alpha |
49 val alpha_cases = #elims alpha |
66 val alpha_induct = #induct alpha |
50 val alpha_induct_loc = #induct alpha |
67 val alpha_inj = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy2 |
51 val [alpha_induct] = ProofContext.export lthy2 lthy1 [alpha_induct_loc] |
|
52 (* TODO replace when inducts is provided by the 2 lines below: *) |
|
53 val alpha_inducts = Project_Rule.projects lthy2 (1 upto number) alpha_induct |
|
54 (*val alpha_inducts_loc = #inducts alpha |
|
55 val alpha_inducts = ProofContext.export lthy2 lthy1 alpha_inducts_loc*) |
|
56 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy2 |
|
57 val alpha_inj = ProofContext.export lthy2 lthy1 alpha_inj_loc |
68 val fv_def = ProofContext.export lthy2 lthy1 fv_def_loc |
58 val fv_def = ProofContext.export lthy2 lthy1 fv_def_loc |
69 val morphism = ProofContext.export_morphism lthy2 lthy1 |
59 val morphism = ProofContext.export_morphism lthy2 lthy1 |
70 val fv_ts = map (Morphism.term morphism) fv_ts_loc |
60 val fv_ts = map (Morphism.term morphism) fv_ts_loc |
71 val alpha_ts = map (Morphism.term morphism) alpha_ts_loc |
61 val alpha_ts = map (Morphism.term morphism) alpha_ts_loc |
72 val (bv_eqvts, lthy3) = build_eqvts @{binding bv_eqvts} [@{term rbv2}] [hd (tl perms)] |
62 fun build_bv_eqvt (t, n) = |
73 (bv_simps @ raw_perm_def) @{thm rtrm2_ras.inducts(2)} lthy2; |
63 build_eqvts Binding.empty [t] [nth perms n] |
74 val (fv_eqvts, lthy4) = build_eqvts @{binding fv_eqvts} fv_ts_loc perms (fv_def_loc @ raw_perm_def) induct lthy3; |
64 (bv_simps @ raw_perm_def) (nth inducts n) |
75 val alpha_eqvt = build_alpha_eqvts alpha_ts_loc perms (raw_perm_def @ alpha_inj) alpha_induct lthy4; |
65 val (bv_eqvts, lthy3) = fold_map build_bv_eqvt bvs lthy2; |
76 val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct inject alpha_inj distinct alpha_cases alpha_eqvt lthy4; |
66 val (fv_eqvts, lthy4) = build_eqvts Binding.empty fv_ts_loc perms (fv_def_loc @ raw_perm_def) induct lthy3; |
|
67 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy4; |
|
68 val alpha_eqvt = ProofContext.export lthy4 lthy1 alpha_eqvt_loc |
|
69 val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy4; |
77 val alpha_equivp = ProofContext.export lthy4 lthy1 alpha_equivp_loc |
70 val alpha_equivp = ProofContext.export lthy4 lthy1 alpha_equivp_loc |
78 val lthy5 = define_quotient_type |
71 val lthy5 = define_quotient_type |
79 (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) (ntnames ~~ alpha_ts)) |
72 (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((ntnames ~~ typs) ~~ alpha_ts)) |
80 (ALLGOALS (resolve_tac alpha_equivp)) lthy4; |
73 (ALLGOALS (resolve_tac alpha_equivp)) lthy4; |
81 val ((c, def), lthy6) = Quotient_Def.quotient_lift_const ("Vr2", @{term rVr2}) lthy5 |
74 val consts = |
|
75 flat (map (fn (i, (_, _, l)) => |
|
76 map (fn (cname, dts) => |
|
77 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |
|
78 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
|
79 val (csdefl, lthy6) = fold_map Quotient_Def.quotient_lift_const (ncnames ~~ consts) lthy5; |
|
80 val (cs, def) = split_list csdefl; |
|
81 val ((_, fv_rsp), lthy7) = prove_const_rsp Binding.empty fv_ts |
|
82 (fn _ => fvbv_rsp_tac alpha_induct fv_def 1) lthy6 |
|
83 val (bvs_rsp', lthy8) = fold_map ( |
|
84 fn (bv_t, i) => prove_const_rsp Binding.empty [bv_t] |
|
85 (fn _ => fvbv_rsp_tac (nth alpha_inducts i) bv_simps 1)) bvs lthy7 |
|
86 val bvs_rsp = flat (map snd bvs_rsp') |
|
87 val (const_rsps, lthy9) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
|
88 (fn _ => constr_rsp_tac alpha_inj (fv_rsp @ bvs_rsp) alpha_equivp 1)) consts lthy8 |
|
89 val (perms_rsp, lthy10) = prove_const_rsp Binding.empty perms |
|
90 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy9; |
|
91 val lift_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy1, induct)); |
|
92 val lthy11 = snd (Local_Theory.note ((@{binding lift_induct}, []), [lift_induct]) lthy10) |
82 *} |
93 *} |
83 |
94 |
84 ML {* |
95 setup {* fn _ => Local_Theory.exit_global lthy11 *} |
85 val thyf = Local_Theory.exit_global lthy6; |
96 thm lift_induct |
86 *} |
|
87 setup {* fn _ => thyf *} |
|
88 print_theorems |
|
89 |
97 |
|
98 end |
90 |
99 |
91 |
|
92 |
|
93 ML {* |
|
94 val lthy5 = define_quotient_type |
|
95 (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) (ntnames ~~ alpha_ts)) |
|
96 (ALLGOALS (resolve_tac alpha_equivp)) lthy4 |
|
97 *} |
|
98 |
|
99 ML {* |
|
100 |
|
101 *} |
|
102 |
|
103 |
|