1 theory NewParser |
1 theory NewParser |
2 imports "../Nominal-General/Nominal2_Base" |
2 imports "../Nominal-General/Nominal2_Base" |
3 "../Nominal-General/Nominal2_Eqvt" |
3 "../Nominal-General/Nominal2_Eqvt" |
4 "../Nominal-General/Nominal2_Supp" |
4 "../Nominal-General/Nominal2_Supp" |
5 "Perm" "NewFv" "NewAlpha" "Tacs" "Equivp" "Lift" |
5 "Perm" "NewAlpha" "Tacs" "Equivp" "Lift" |
6 begin |
6 begin |
|
7 |
7 |
8 |
8 section{* Interface for nominal_datatype *} |
9 section{* Interface for nominal_datatype *} |
9 |
10 |
10 |
11 |
11 ML {* |
12 ML {* |
152 fun rawify_bclauses dts_env cnstrs_env bn_fun_env bclauses = |
153 fun rawify_bclauses dts_env cnstrs_env bn_fun_env bclauses = |
153 let |
154 let |
154 fun rawify_bnds bnds = |
155 fun rawify_bnds bnds = |
155 map (apfst (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env))) bnds |
156 map (apfst (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env))) bnds |
156 |
157 |
157 fun rawify_bclause (BEmy n) = BEmy n |
158 fun rawify_bclause (BC (mode, bnds, bdys)) = BC (mode, rawify_bnds bnds, bdys) |
158 | rawify_bclause (BLst (bnds, bdys)) = BLst (rawify_bnds bnds, bdys) |
|
159 | rawify_bclause (BSet (bnds, bdys)) = BSet (rawify_bnds bnds, bdys) |
|
160 | rawify_bclause (BRes (bnds, bdys)) = BRes (rawify_bnds bnds, bdys) |
|
161 in |
159 in |
162 map (map (map rawify_bclause)) bclauses |
160 map (map (map rawify_bclause)) bclauses |
163 end |
161 end |
164 *} |
162 *} |
165 |
163 |
217 val unordered = AList.group (op=) (map aux eqs) |
215 val unordered = AList.group (op=) (map aux eqs) |
218 val unordered' = map (fn (x, y) => (x, AList.group (op=) y)) unordered |
216 val unordered' = map (fn (x, y) => (x, AList.group (op=) y)) unordered |
219 val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' |
217 val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' |
220 val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered) |
218 val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered) |
221 |
219 |
222 val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs)) |
220 (*val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs))*) |
223 (*val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs))*) |
221 (*val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs))*) |
224 val _ = tracing ("ordered'\n" ^ @{make_string} ordered') |
222 (*val _ = tracing ("ordered'\n" ^ @{make_string} ordered')*) |
225 in |
223 in |
226 ordered' |
224 ordered' |
227 end |
225 end |
228 *} |
226 *} |
229 |
227 |
261 |
259 |
262 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
260 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
263 fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l); |
261 fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l); |
264 val bn_funs_decls = map (export_fun (Morphism.term morphism_2_0)) raw_bns; |
262 val bn_funs_decls = map (export_fun (Morphism.term morphism_2_0)) raw_bns; |
265 in |
263 in |
266 (raw_dt_names, raw_bn_eqs, raw_bclauses, bn_funs_decls, lthy2) |
264 (raw_dt_names, raw_bn_eqs, raw_bclauses, bn_funs_decls, raw_bns, lthy2) |
267 end |
265 end |
268 *} |
266 *} |
269 |
267 |
270 lemma equivp_hack: "equivp x" |
268 lemma equivp_hack: "equivp x" |
271 sorry |
269 sorry |
370 |
368 |
371 ML {* |
369 ML {* |
372 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
370 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
373 let |
371 let |
374 (* definition of the raw datatypes and raw bn-functions *) |
372 (* definition of the raw datatypes and raw bn-functions *) |
375 val (raw_dt_names, raw_bn_eqs, raw_bclauses, raw_bns, lthy1) = |
373 val (raw_dt_names, raw_bn_eqs, raw_bclauses, raw_bns, raw_bns2, lthy1) = |
376 if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
374 if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
377 else raise TEST lthy |
375 else raise TEST lthy |
|
376 |
|
377 (*val _ = tracing ("exported: " ^ commas (map @{make_string} raw_bns))*) |
|
378 (*val _ = tracing ("plain: " ^ commas (map @{make_string} raw_bns2))*) |
378 |
379 |
379 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names) |
380 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names) |
380 val {descr, sorts, ...} = dtinfo |
381 val {descr, sorts, ...} = dtinfo |
381 val all_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr |
382 val all_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr |
382 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr |
383 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr |
406 val lthy3 = Theory_Target.init NONE thy; |
407 val lthy3 = Theory_Target.init NONE thy; |
407 val raw_bn_funs = map (fn (f, _, _) => f) raw_bns; |
408 val raw_bn_funs = map (fn (f, _, _) => f) raw_bns; |
408 |
409 |
409 val (fv, fvbn, fv_def, lthy3a) = |
410 val (fv, fvbn, fv_def, lthy3a) = |
410 if get_STEPS lthy2 > 3 |
411 if get_STEPS lthy2 > 3 |
411 then define_raw_fvs descr sorts raw_bns raw_bclauses lthy3 |
412 then define_raw_fvs descr sorts raw_bns raw_bns2 raw_bclauses lthy3 |
412 else raise TEST lthy3 |
413 else raise TEST lthy3 |
413 |
414 |
414 (* definition of raw alphas *) |
415 (* definition of raw alphas *) |
415 val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = |
416 val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = |
416 if get_STEPS lthy > 4 |
417 if get_STEPS lthy > 4 |
429 ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) |
430 ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) |
430 |
431 |
431 (* definition of raw_alpha_eq_iff lemmas *) |
432 (* definition of raw_alpha_eq_iff lemmas *) |
432 val alpha_eq_iff = build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4 |
433 val alpha_eq_iff = build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4 |
433 val alpha_eq_iff_simp = map remove_loop alpha_eq_iff; |
434 val alpha_eq_iff_simp = map remove_loop alpha_eq_iff; |
434 val _ = map tracing (map PolyML.makestring alpha_eq_iff_simp); |
435 |
|
436 (*val _ = map tracing (map PolyML.makestring alpha_eq_iff_simp);*) |
435 |
437 |
436 (* proving equivariance lemmas *) |
438 (* proving equivariance lemmas *) |
437 val _ = warning "Proving equivariance"; |
439 val _ = warning "Proving equivariance"; |
438 val (bv_eqvt, lthy5) = prove_eqvt all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) (map fst bns) lthy4 |
440 val (bv_eqvt, lthy5) = prove_eqvt all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) (map fst bns) lthy4 |
439 val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (fv_def @ raw_perm_defs) (fv @ fvbn) lthy5 |
441 val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (fv_def @ raw_perm_defs) (fv @ fvbn) lthy5 |
637 | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), index_lookup env x) |
639 | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), index_lookup env x) |
638 | _ => error ("The term " ^ bn_str ^ " is not allowed as binding function.") |
640 | _ => error ("The term " ^ bn_str ^ " is not allowed as binding function.") |
639 |
641 |
640 fun prep_body env bn_str = index_lookup env bn_str |
642 fun prep_body env bn_str = index_lookup env bn_str |
641 |
643 |
642 fun prep_mode "bind" = BLst |
644 fun prep_mode "bind" = Lst |
643 | prep_mode "bind_set" = BSet |
645 | prep_mode "bind_set" = Set |
644 | prep_mode "bind_res" = BRes |
646 | prep_mode "bind_res" = Res |
645 |
647 |
646 fun prep_bclause env (mode, binders, bodies) = |
648 fun prep_bclause env (mode, binders, bodies) = |
647 let |
649 let |
648 val binders' = map (prep_binder env) binders |
650 val binders' = map (prep_binder env) binders |
649 val bodies' = map (prep_body env) bodies |
651 val bodies' = map (prep_body env) bodies |
650 in |
652 in |
651 prep_mode mode (binders', bodies') |
653 BC (prep_mode mode, binders', bodies') |
652 end |
654 end |
653 |
655 |
654 fun prep_bclauses (annos, bclause_strs) = |
656 fun prep_bclauses (annos, bclause_strs) = |
655 let |
657 let |
656 val env = indexify annos (* for every label, associate the index *) |
658 val env = indexify annos (* for every label, associate the index *) |
686 get_cnstrs dt_strs |
685 get_cnstrs dt_strs |
687 |> map (map (fn (_, antys, _, _) => length antys)) |
686 |> map (map (fn (_, antys, _, _) => length antys)) |
688 |
687 |
689 fun complt n bcs = |
688 fun complt n bcs = |
690 let |
689 let |
691 fun add bcs i = (if included i bcs then [] else [BEmy i]) |
690 fun add bcs i = (if included i bcs then [] else [BC (Lst, [], [i])]) |
692 in |
691 in |
693 bcs @ (flat (map_range (add bcs) n)) |
692 bcs @ (flat (map_range (add bcs) n)) |
694 end |
693 end |
695 in |
694 in |
696 map2 (map2 complt) args bclauses |
695 map2 (map2 complt) args bclauses |