equal
deleted
inserted
replaced
7 *) |
7 *) |
8 |
8 |
9 signature NOMINAL_DT_QUOT = |
9 signature NOMINAL_DT_QUOT = |
10 sig |
10 sig |
11 val define_qtypes: (string list * binding * mixfix) list -> typ list -> term list -> |
11 val define_qtypes: (string list * binding * mixfix) list -> typ list -> term list -> |
12 thm list -> local_theory -> Quotient_Info.quotdata_info list * local_theory |
12 thm list -> local_theory -> Quotient_Info.quotients list * local_theory |
13 |
13 |
14 val define_qconsts: typ list -> (string * term * mixfix) list -> local_theory -> |
14 val define_qconsts: typ list -> (string * term * mixfix) list -> local_theory -> |
15 Quotient_Info.qconsts_info list * local_theory |
15 Quotient_Info.quotconsts list * local_theory |
16 |
16 |
17 val define_qperms: typ list -> string list -> (string * sort) list -> |
17 val define_qperms: typ list -> string list -> (string * sort) list -> |
18 (string * term * mixfix) list -> thm list -> local_theory -> local_theory |
18 (string * term * mixfix) list -> thm list -> local_theory -> local_theory |
19 |
19 |
20 val define_qsizes: typ list -> string list -> (string * sort) list -> |
20 val define_qsizes: typ list -> string list -> (string * sort) list -> |
67 (* defines quotient constants *) |
67 (* defines quotient constants *) |
68 fun define_qconsts qtys consts_specs lthy = |
68 fun define_qconsts qtys consts_specs lthy = |
69 let |
69 let |
70 val (qconst_infos, lthy') = |
70 val (qconst_infos, lthy') = |
71 fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy |
71 fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy |
72 val phi = ProofContext.export_morphism lthy' lthy |
72 val phi = Proof_Context.export_morphism lthy' lthy |
73 in |
73 in |
74 (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy') |
74 (map (Quotient_Info.transform_quotconsts phi) qconst_infos, lthy') |
75 end |
75 end |
76 |
76 |
77 |
77 |
78 (* defines the quotient permutations and proves pt-class *) |
78 (* defines the quotient permutations and proves pt-class *) |
79 fun define_qperms qtys qfull_ty_names tvs perm_specs raw_perm_laws lthy = |
79 fun define_qperms qtys qfull_ty_names tvs perm_specs raw_perm_laws lthy = |
83 |> Local_Theory.exit_global |
83 |> Local_Theory.exit_global |
84 |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) |
84 |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) |
85 |
85 |
86 val (qs, lthy2) = define_qconsts qtys perm_specs lthy1 |
86 val (qs, lthy2) = define_qconsts qtys perm_specs lthy1 |
87 |
87 |
88 val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2 |
88 val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws (Local_Theory.target_of lthy2) |
89 |
89 |
90 val lifted_perm_laws = |
90 val lifted_perm_laws = |
91 map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws' |
91 map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws' |
92 |> Variable.exportT lthy3 lthy2 |
92 |> Variable.exportT lthy3 lthy2 |
93 |
93 |
183 val goal = mk_supports_goal ctxt qtrm |
183 val goal = mk_supports_goal ctxt qtrm |
184 val ctxt' = Variable.auto_fixes goal ctxt |
184 val ctxt' = Variable.auto_fixes goal ctxt |
185 in |
185 in |
186 Goal.prove ctxt' [] [] goal |
186 Goal.prove ctxt' [] [] goal |
187 (K (HEADGOAL (supports_tac ctxt perm_simps))) |
187 (K (HEADGOAL (supports_tac ctxt perm_simps))) |
188 |> singleton (ProofContext.export ctxt' ctxt) |
188 |> singleton (Proof_Context.export ctxt' ctxt) |
189 end |
189 end |
190 |
190 |
191 fun prove_supports ctxt perm_simps qtrms = |
191 fun prove_supports ctxt perm_simps qtrms = |
192 map (prove_supports_single ctxt perm_simps) qtrms |
192 map (prove_supports_single ctxt perm_simps) qtrms |
193 |
193 |
208 resolve_tac qsupports_thms, |
208 resolve_tac qsupports_thms, |
209 asm_simp_tac (HOL_ss addsimps @{thms finite_supp supp_Pair finite_Un}) ] |
209 asm_simp_tac (HOL_ss addsimps @{thms finite_supp supp_Pair finite_Un}) ] |
210 in |
210 in |
211 Goal.prove ctxt' [] [] goals |
211 Goal.prove ctxt' [] [] goals |
212 (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac))) |
212 (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac))) |
213 |> singleton (ProofContext.export ctxt' ctxt) |
213 |> singleton (Proof_Context.export ctxt' ctxt) |
214 |> Datatype_Aux.split_conj_thm |
214 |> Datatype_Aux.split_conj_thm |
215 |> map zero_var_indexes |
215 |> map zero_var_indexes |
216 end |
216 end |
217 |
217 |
218 |
218 |
352 val props = map2 mk_goal qperm_bns alpha_bns |
352 val props = map2 mk_goal qperm_bns alpha_bns |
353 val ss = @{thm id_def}::qperm_bn_simps @ qeq_iffs @ qalpha_refls |
353 val ss = @{thm id_def}::qperm_bn_simps @ qeq_iffs @ qalpha_refls |
354 val ss_tac = asm_full_simp_tac (HOL_ss addsimps ss) |
354 val ss_tac = asm_full_simp_tac (HOL_ss addsimps ss) |
355 in |
355 in |
356 induct_prove qtys props qinduct (K ss_tac) ctxt' |
356 induct_prove qtys props qinduct (K ss_tac) ctxt' |
357 |> ProofContext.export ctxt' ctxt |
357 |> Proof_Context.export ctxt' ctxt |
358 |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) |
358 |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) |
359 end |
359 end |
360 |
360 |
361 fun prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qbn_eqvts ctxt = |
361 fun prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qbn_eqvts ctxt = |
362 let |
362 let |
378 EVERY' [asm_full_simp_tac (HOL_basic_ss addsimps ss), |
378 EVERY' [asm_full_simp_tac (HOL_basic_ss addsimps ss), |
379 TRY o eqvt_tac ctxt' (eqvt_strict_config addpres qbn_eqvts), |
379 TRY o eqvt_tac ctxt' (eqvt_strict_config addpres qbn_eqvts), |
380 TRY o asm_full_simp_tac HOL_basic_ss] |
380 TRY o asm_full_simp_tac HOL_basic_ss] |
381 in |
381 in |
382 induct_prove qtys props qinduct (K ss_tac) ctxt' |
382 induct_prove qtys props qinduct (K ss_tac) ctxt' |
383 |> ProofContext.export ctxt' ctxt |
383 |> Proof_Context.export ctxt' ctxt |
384 |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) |
384 |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) |
385 end |
385 end |
386 |
386 |
387 |
387 |
388 |
388 |
576 conj_tac (DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)) ]) |
576 conj_tac (DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)) ]) |
577 |
577 |
578 (* proves goal "P" *) |
578 (* proves goal "P" *) |
579 val side_thm = Goal.prove ctxt'' [] [] (term_of concl) |
579 val side_thm = Goal.prove ctxt'' [] [] (term_of concl) |
580 (K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ])) |
580 (K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ])) |
581 |> singleton (ProofContext.export ctxt'' ctxt) |
581 |> singleton (Proof_Context.export ctxt'' ctxt) |
582 in |
582 in |
583 rtac side_thm 1 |
583 rtac side_thm 1 |
584 end) ctxt |
584 end) ctxt |
585 in |
585 in |
586 EVERY1 [rtac qexhaust_thm, RANGE (map2 aux_tac prems bclausess)] |
586 EVERY1 [rtac qexhaust_thm, RANGE (map2 aux_tac prems bclausess)] |
610 |
610 |
611 fun prove prems bclausess exhaust concl = |
611 fun prove prems bclausess exhaust concl = |
612 Goal.prove lthy'' [] prems concl (tac bclausess exhaust) |
612 Goal.prove lthy'' [] prems concl (tac bclausess exhaust) |
613 in |
613 in |
614 map4 prove premss bclausesss exhausts' main_concls |
614 map4 prove premss bclausesss exhausts' main_concls |
615 |> ProofContext.export lthy'' lthy |
615 |> Proof_Context.export lthy'' lthy |
616 end |
616 end |
617 |
617 |
618 |
618 |
619 |
619 |
620 (** strong induction theorems **) |
620 (** strong induction theorems **) |
695 |> map2 (prep_prem lthy'' c c_name c_ty) (flat bclausesss) |
695 |> map2 (prep_prem lthy'' c c_name c_ty) (flat bclausesss) |
696 |
696 |
697 fun pat_tac ctxt thm = |
697 fun pat_tac ctxt thm = |
698 Subgoal.FOCUS (fn {params, context, ...} => |
698 Subgoal.FOCUS (fn {params, context, ...} => |
699 let |
699 let |
700 val thy = ProofContext.theory_of context |
700 val thy = Proof_Context.theory_of context |
701 val ty_parms = map (fn (_, ct) => (fastype_of (term_of ct), ct)) params |
701 val ty_parms = map (fn (_, ct) => (fastype_of (term_of ct), ct)) params |
702 val vs = Term.add_vars (prop_of thm) [] |
702 val vs = Term.add_vars (prop_of thm) [] |
703 val vs_tys = map (Type.legacy_freeze_type o snd) vs |
703 val vs_tys = map (Type.legacy_freeze_type o snd) vs |
704 val vs_ctrms = map (cterm_of thy o Var) vs |
704 val vs_ctrms = map (cterm_of thy o Var) vs |
705 val assigns = map (lookup ty_parms) vs_tys |
705 val assigns = map (lookup ty_parms) vs_tys |
717 (fn {prems, context} => |
717 (fn {prems, context} => |
718 Induction_Schema.induction_schema_tac context prems |
718 Induction_Schema.induction_schema_tac context prems |
719 THEN RANGE (map (pat_tac context) exhausts) 1 |
719 THEN RANGE (map (pat_tac context) exhausts) 1 |
720 THEN prove_termination_ind context 1 |
720 THEN prove_termination_ind context 1 |
721 THEN ALLGOALS size_simp_tac) |
721 THEN ALLGOALS size_simp_tac) |
722 |> ProofContext.export lthy'' lthy |
722 |> Proof_Context.export lthy'' lthy |
723 end |
723 end |
724 |
724 |
725 |
725 |
726 end (* structure *) |
726 end (* structure *) |
727 |
727 |