equal
deleted
inserted
replaced
50 (** functions that define the raw binding functions **) |
50 (** functions that define the raw binding functions **) |
51 |
51 |
52 (* strip_bn_fun takes a rhs of a bn function: this can only contain unions or |
52 (* strip_bn_fun takes a rhs of a bn function: this can only contain unions or |
53 appends of elements; in case of recursive calls it returns also the applied |
53 appends of elements; in case of recursive calls it returns also the applied |
54 bn function *) |
54 bn function *) |
55 fun strip_bn_fun lthy args t = |
55 fun strip_bn_fun ctxt args t = |
56 let |
56 let |
57 fun aux t = |
57 fun aux t = |
58 case t of |
58 case t of |
59 Const (@{const_name sup}, _) $ l $ r => aux l @ aux r |
59 Const (@{const_name sup}, _) $ l $ r => aux l @ aux r |
60 | Const (@{const_name append}, _) $ l $ r => aux l @ aux r |
60 | Const (@{const_name append}, _) $ l $ r => aux l @ aux r |
63 | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y => |
63 | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y => |
64 (find_index (equal x) args, NONE) :: aux y |
64 (find_index (equal x) args, NONE) :: aux y |
65 | Const (@{const_name bot}, _) => [] |
65 | Const (@{const_name bot}, _) => [] |
66 | Const (@{const_name Nil}, _) => [] |
66 | Const (@{const_name Nil}, _) => [] |
67 | (f as Const _) $ (x as Var _) => [(find_index (equal x) args, SOME f)] |
67 | (f as Const _) $ (x as Var _) => [(find_index (equal x) args, SOME f)] |
68 | _ => error ("Unsupported binding function: " ^ (Syntax.string_of_term lthy t)) |
68 | _ => error ("Unsupported binding function: " ^ (Syntax.string_of_term ctxt t)) |
69 in |
69 in |
70 aux t |
70 aux t |
71 end |
71 end |
72 |
72 |
73 (** definition of the raw binding functions **) |
73 (** definition of the raw binding functions **) |
74 |
74 |
75 fun prep_bn_info lthy dt_names dts bn_funs eqs = |
75 fun prep_bn_info ctxt dt_names dts bn_funs eqs = |
76 let |
76 let |
77 fun process_eq eq = |
77 fun process_eq eq = |
78 let |
78 let |
79 val (lhs, rhs) = eq |
79 val (lhs, rhs) = eq |
80 |> HOLogic.dest_Trueprop |
80 |> HOLogic.dest_Trueprop |
83 val (_, ty) = dest_Const bn_fun |
83 val (_, ty) = dest_Const bn_fun |
84 val (ty_name, _) = dest_Type (domain_type ty) |
84 val (ty_name, _) = dest_Type (domain_type ty) |
85 val dt_index = find_index (fn x => x = ty_name) dt_names |
85 val dt_index = find_index (fn x => x = ty_name) dt_names |
86 val (cnstr_head, cnstr_args) = strip_comb cnstr |
86 val (cnstr_head, cnstr_args) = strip_comb cnstr |
87 val cnstr_name = Long_Name.base_name (fst (dest_Const cnstr_head)) |
87 val cnstr_name = Long_Name.base_name (fst (dest_Const cnstr_head)) |
88 val rhs_elements = strip_bn_fun lthy cnstr_args rhs |
88 val rhs_elements = strip_bn_fun ctxt cnstr_args rhs |
89 in |
89 in |
90 ((bn_fun, dt_index), (cnstr_name, rhs_elements)) |
90 ((bn_fun, dt_index), (cnstr_name, rhs_elements)) |
91 end |
91 end |
92 |
92 |
93 (* order according to constructor names *) |
93 (* order according to constructor names *) |
342 |
342 |
343 (*** raw permutation functions ***) |
343 (*** raw permutation functions ***) |
344 |
344 |
345 (** proves the two pt-type class properties **) |
345 (** proves the two pt-type class properties **) |
346 |
346 |
347 fun prove_permute_zero induct perm_defs perm_fns lthy = |
347 fun prove_permute_zero induct perm_defs perm_fns ctxt = |
348 let |
348 let |
349 val perm_types = map (body_type o fastype_of) perm_fns |
349 val perm_types = map (body_type o fastype_of) perm_fns |
350 val perm_indnames = Datatype_Prop.make_tnames perm_types |
350 val perm_indnames = Datatype_Prop.make_tnames perm_types |
351 |
351 |
352 fun single_goal ((perm_fn, T), x) = |
352 fun single_goal ((perm_fn, T), x) = |
354 |
354 |
355 val goals = |
355 val goals = |
356 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
356 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
357 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
357 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
358 |
358 |
359 val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs) |
359 val simpset = put_simpset HOL_basic_ss ctxt addsimps (@{thm permute_zero} :: perm_defs) |
360 |
360 |
361 val tac = (Datatype_Aux.ind_tac induct perm_indnames |
361 val tac = (Datatype_Aux.ind_tac induct perm_indnames |
362 THEN_ALL_NEW asm_simp_tac simps) 1 |
362 THEN_ALL_NEW asm_simp_tac simpset) 1 |
363 in |
363 in |
364 Goal.prove lthy perm_indnames [] goals (K tac) |
364 Goal.prove ctxt perm_indnames [] goals (K tac) |
365 |> Datatype_Aux.split_conj_thm |
365 |> Datatype_Aux.split_conj_thm |
366 end |
366 end |
367 |
367 |
368 |
368 |
369 fun prove_permute_plus induct perm_defs perm_fns lthy = |
369 fun prove_permute_plus induct perm_defs perm_fns ctxt = |
370 let |
370 let |
371 val p = Free ("p", @{typ perm}) |
371 val p = Free ("p", @{typ perm}) |
372 val q = Free ("q", @{typ perm}) |
372 val q = Free ("q", @{typ perm}) |
373 val perm_types = map (body_type o fastype_of) perm_fns |
373 val perm_types = map (body_type o fastype_of) perm_fns |
374 val perm_indnames = Datatype_Prop.make_tnames perm_types |
374 val perm_indnames = Datatype_Prop.make_tnames perm_types |
378 |
378 |
379 val goals = |
379 val goals = |
380 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
380 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
381 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
381 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
382 |
382 |
383 val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs) |
383 (* FIXME proper goal context *) |
|
384 val simpset = put_simpset HOL_basic_ss ctxt addsimps (@{thm permute_plus} :: perm_defs) |
384 |
385 |
385 val tac = (Datatype_Aux.ind_tac induct perm_indnames |
386 val tac = (Datatype_Aux.ind_tac induct perm_indnames |
386 THEN_ALL_NEW asm_simp_tac simps) 1 |
387 THEN_ALL_NEW asm_simp_tac simpset) 1 |
387 in |
388 in |
388 Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac) |
389 Goal.prove ctxt ("p" :: "q" :: perm_indnames) [] goals (K tac) |
389 |> Datatype_Aux.split_conj_thm |
390 |> Datatype_Aux.split_conj_thm |
390 end |
391 end |
391 |
392 |
392 |
393 |
393 fun mk_perm_eq ty_perm_assoc cnstr = |
394 fun mk_perm_eq ty_perm_assoc cnstr = |
456 (** equivarance proofs **) |
457 (** equivarance proofs **) |
457 |
458 |
458 val eqvt_apply_sym = @{thm eqvt_apply[symmetric]} |
459 val eqvt_apply_sym = @{thm eqvt_apply[symmetric]} |
459 |
460 |
460 fun subproof_tac const_names simps = |
461 fun subproof_tac const_names simps = |
461 SUBPROOF (fn {prems, context, ...} => |
462 SUBPROOF (fn {prems, context = ctxt, ...} => |
462 HEADGOAL |
463 HEADGOAL |
463 (simp_tac (HOL_basic_ss addsimps simps) |
464 (simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps) |
464 THEN' eqvt_tac context (eqvt_relaxed_config addexcls const_names) |
465 THEN' eqvt_tac ctxt (eqvt_relaxed_config addexcls const_names) |
465 THEN' simp_tac (HOL_basic_ss addsimps (prems @ [eqvt_apply_sym])))) |
466 THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps (prems @ [eqvt_apply_sym])))) |
466 |
467 |
467 fun prove_eqvt_tac insts ind_thms const_names simps ctxt = |
468 fun prove_eqvt_tac insts ind_thms const_names simps ctxt = |
468 HEADGOAL |
469 HEADGOAL |
469 (Object_Logic.full_atomize_tac |
470 (Object_Logic.full_atomize_tac |
470 THEN' (DETERM o (Induct_Tacs.induct_rules_tac ctxt insts ind_thms)) |
471 THEN' (DETERM o (Induct_Tacs.induct_rules_tac ctxt insts ind_thms)) |