# HG changeset patch # User Christian Urban # Date 1309385324 -3600 # Node ID 116f9ba4f59f83c3bbe97aa3f7030e58bf1775a3 # Parent 37c0d7953cbaf93fbee3a44882c1462a9d0274b0 combined distributed data for alpha in alpha_result (partially done) diff -r 37c0d7953cba -r 116f9ba4f59f Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Wed Jun 29 19:21:26 2011 +0100 +++ b/Nominal/Nominal2.thy Wed Jun 29 23:08:44 2011 +0100 @@ -232,7 +232,7 @@ (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3b val _ = trace_msg (K "Defining alpha relations...") - val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) = + val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, alpha_result, lthy4) = define_raw_alpha raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c val _ = tracing ("alpha_induct\n" ^ Syntax.string_of_term lthy3c (prop_of alpha_induct)) @@ -242,11 +242,10 @@ val _ = trace_msg (K "Proving distinct theorems...") val alpha_distincts = - raw_prove_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_dt_names + raw_prove_alpha_distincts lthy4 alpha_result raw_distinct_thms raw_dt_names val _ = trace_msg (K "Proving eq-iff theorems...") - val alpha_eq_iff = - raw_prove_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases + val alpha_eq_iff = raw_prove_alpha_eq_iff lthy4 alpha_result raw_distinct_thms raw_inject_thms val _ = trace_msg (K "Proving equivariance of bns, fvs, size and alpha...") val raw_bn_eqvt = @@ -273,19 +272,13 @@ val alpha_eqvt_norm = map (Nominal_ThmDecls.eqvt_transform lthy5) alpha_eqvt val _ = trace_msg (K "Proving equivalence of alpha...") - val alpha_refl_thms = - raw_prove_refl alpha_trms alpha_bn_trms alpha_intros raw_induct_thm lthy5 - - val alpha_sym_thms = - raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct alpha_eqvt_norm lthy5 - - val alpha_trans_thms = - raw_prove_trans (alpha_trms @ alpha_bn_trms) (raw_distinct_thms @ raw_inject_thms) - alpha_intros alpha_induct alpha_cases alpha_eqvt_norm lthy5 + val alpha_refl_thms = raw_prove_refl lthy5 alpha_result raw_induct_thm + val alpha_sym_thms = raw_prove_sym lthy5 alpha_result alpha_eqvt_norm + val alpha_trans_thms = + raw_prove_trans lthy5 alpha_result (raw_distinct_thms @ raw_inject_thms) alpha_eqvt_norm val (alpha_equivp_thms, alpha_bn_equivp_thms) = - raw_prove_equivp alpha_trms alpha_bn_trms alpha_refl_thms alpha_sym_thms - alpha_trans_thms lthy5 + raw_prove_equivp lthy5 alpha_result alpha_refl_thms alpha_sym_thms alpha_trans_thms val _ = trace_msg (K "Proving alpha implies bn...") val alpha_bn_imp_thms = diff -r 37c0d7953cba -r 116f9ba4f59f Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Wed Jun 29 19:21:26 2011 +0100 +++ b/Nominal/nominal_dt_alpha.ML Wed Jun 29 23:08:44 2011 +0100 @@ -11,7 +11,7 @@ val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list -> bclause list list list -> term list -> Proof.context -> - term list * term list * thm list * thm list * thm * local_theory + term list * term list * thm list * thm list * thm * alpha_result * local_theory val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> (Proof.context -> int -> tactic) -> Proof.context -> thm list @@ -19,19 +19,13 @@ val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> (Proof.context -> int -> tactic) -> Proof.context -> thm list - val raw_prove_alpha_distincts: Proof.context -> thm list -> thm list -> - term list -> string list -> thm list - - val raw_prove_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> - thm list -> thm list - - val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list - val raw_prove_sym: term list -> thm list -> thm -> thm list -> Proof.context -> thm list - val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> thm list -> - Proof.context -> thm list - val raw_prove_equivp: term list -> term list -> thm list -> thm list -> thm list -> - Proof.context -> thm list * thm list - + val raw_prove_alpha_distincts: Proof.context -> alpha_result -> thm list -> string list -> thm list + val raw_prove_alpha_eq_iff: Proof.context -> alpha_result -> thm list -> thm list -> thm list + val raw_prove_refl: Proof.context -> alpha_result -> thm -> thm list + val raw_prove_sym: Proof.context -> alpha_result -> thm list -> thm list + val raw_prove_trans: Proof.context -> alpha_result -> thm list -> thm list -> thm list + val raw_prove_equivp: Proof.context -> alpha_result -> thm list -> thm list -> thm list -> + thm list * thm list val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> term list -> thm -> thm list -> Proof.context -> thm list @@ -49,6 +43,7 @@ struct open Nominal_Permeq +open Nominal_Dt_Data fun lookup xs x = the (AList.lookup (op=) xs x) fun group xs = AList.group (op=) xs @@ -253,27 +248,50 @@ (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) - val (alphas, lthy') = Inductive.add_inductive_i + val (alpha_info, lthy') = Inductive.add_inductive_i {quiet_mode = true, verbose = false, alt_name = Binding.empty, coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} all_alpha_names [] all_alpha_intros [] lthy - val all_alpha_trms_loc = #preds alphas; - val alpha_induct_loc = #raw_induct alphas; - val alpha_intros_loc = #intrs alphas; - val alpha_cases_loc = #elims alphas; + val all_alpha_trms_loc = #preds alpha_info; + val alpha_raw_induct_loc = #raw_induct alpha_info; + val alpha_intros_loc = #intrs alpha_info; + val alpha_cases_loc = #elims alpha_info; val phi = ProofContext.export_morphism lthy' lthy; val all_alpha_trms = all_alpha_trms_loc |> map (Morphism.term phi) |> map Type.legacy_freeze - val alpha_induct = Morphism.thm phi alpha_induct_loc + val alpha_raw_induct = Morphism.thm phi alpha_raw_induct_loc val alpha_intros = map (Morphism.thm phi) alpha_intros_loc val alpha_cases = map (Morphism.thm phi) alpha_cases_loc val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms + val alpha_tys = + alpha_trms + |> map fastype_of + |> map domain_type + + val alpha_bn_tys = + alpha_bn_trms + |> map fastype_of + |> map domain_type + + val alpha_names = map (fst o dest_Const) alpha_trms + val alpha_bn_names = map (fst o dest_Const) alpha_bn_trms + + val alpha_result = AlphaResult + {alpha_names = alpha_names, + alpha_trms = alpha_trms, + alpha_tys = alpha_tys, + alpha_bn_names = alpha_bn_names, + alpha_bn_trms = alpha_bn_trms, + alpha_bn_tys = alpha_bn_tys, + alpha_intros = alpha_intros, + alpha_cases = alpha_cases, + alpha_raw_induct = alpha_raw_induct} in - (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy') + (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_raw_induct, alpha_result, lthy') end @@ -385,19 +403,21 @@ rtac notI THEN' eresolve_tac cases_thms THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms) -fun raw_prove_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_str = +fun raw_prove_alpha_distincts ctxt alpha_result raw_distinct_thms raw_dt_names = let - val ty_trm_assoc = alpha_str ~~ (map (fst o dest_Const) alpha_trms) + val AlphaResult {alpha_names, alpha_cases, ...} = alpha_result - fun mk_alpha_distinct distinct_trm = + val ty_trm_assoc = raw_dt_names ~~ alpha_names + + fun mk_alpha_distinct raw_distinct_trm = let - val goal = mk_distinct_goal ty_trm_assoc distinct_trm + val goal = mk_distinct_goal ty_trm_assoc raw_distinct_trm in Goal.prove ctxt [] [] goal - (K (distinct_tac cases_thms distinct_thms 1)) + (K (distinct_tac alpha_cases raw_distinct_thms 1)) end in - map (mk_alpha_distinct o prop_of) distinct_thms + map (mk_alpha_distinct o prop_of) raw_distinct_thms end @@ -429,11 +449,13 @@ else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps)) end; -fun raw_prove_alpha_eq_iff ctxt alpha_intros distinct_thms inject_thms alpha_elims = +fun raw_prove_alpha_eq_iff ctxt alpha_result raw_distinct_thms raw_inject_thms = let + val AlphaResult {alpha_intros, alpha_cases, ...} = alpha_result + val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt; val goals = map mk_alpha_eq_iff_goal thms_imp; - val tac = alpha_eq_iff_tac (distinct_thms @ inject_thms) alpha_intros alpha_elims 1; + val tac = alpha_eq_iff_tac (raw_distinct_thms @ raw_inject_thms) alpha_intros alpha_cases 1; val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; in Variable.export ctxt' ctxt thms @@ -459,23 +481,16 @@ resolve_tac intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac] end -fun raw_prove_refl alpha_trms alpha_bns alpha_intros raw_dt_induct ctxt = +fun raw_prove_refl ctxt alpha_result raw_dt_induct = let - val arg_tys = - alpha_trms - |> map fastype_of - |> map domain_type - - val arg_bn_tys = - alpha_bns - |> map fastype_of - |> map domain_type + val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_intros, ...} = + alpha_result val props = map (fn (ty, c) => (ty, fn x => c $ x $ x)) - ((arg_tys ~~ alpha_trms) @ (arg_bn_tys ~~ alpha_bns)) + ((alpha_tys ~~ alpha_trms) @ (alpha_bn_tys ~~ alpha_bn_trms)) in - induct_prove arg_tys props raw_dt_induct (cases_tac alpha_intros) ctxt + induct_prove alpha_tys props raw_dt_induct (cases_tac alpha_intros) ctxt end @@ -505,19 +520,21 @@ trans_prem_tac pred_names ctxt] end -fun raw_prove_sym alpha_trms alpha_intros alpha_induct alpha_eqvt ctxt = +fun raw_prove_sym ctxt alpha_result alpha_eqvt = let + val AlphaResult {alpha_names, alpha_trms, alpha_bn_names, alpha_bn_trms, + alpha_intros, alpha_raw_induct, ...} = alpha_result + + val alpha_trms = alpha_trms @ alpha_bn_trms + val alpha_names = alpha_names @ alpha_bn_names + val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms fun tac ctxt = - let - val alpha_names = map (fst o dest_Const) alpha_trms - in - resolve_tac alpha_intros THEN_ALL_NEW - FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names alpha_eqvt ctxt] - end + resolve_tac alpha_intros THEN_ALL_NEW + FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names alpha_eqvt ctxt] in - alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct tac ctxt + alpha_prove alpha_trms (alpha_trms ~~ props) alpha_raw_induct tac ctxt end @@ -560,14 +577,17 @@ asm_full_simp_tac (HOL_ss addsimps prod_simps) ]) end -fun prove_trans_tac pred_names raw_dt_thms intros cases alpha_eqvt ctxt = +fun prove_trans_tac alpha_result raw_dt_thms alpha_eqvt ctxt = let + val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, alpha_cases, ...} = alpha_result + val alpha_names = alpha_names @ alpha_bn_names + fun all_cases ctxt = asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms) - THEN' TRY o non_trivial_cases_tac pred_names intros alpha_eqvt ctxt + THEN' TRY o non_trivial_cases_tac alpha_names alpha_intros alpha_eqvt ctxt in EVERY' [ rtac @{thm allI}, rtac @{thm impI}, - ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ] + ecases_tac alpha_cases ctxt THEN_ALL_NEW all_cases ctxt ] end fun prep_trans_goal alpha_trm (arg1, arg2) = @@ -579,13 +599,17 @@ HOLogic.all_const arg_ty $ Abs ("z", arg_ty, HOLogic.mk_imp (mid, rhs)) end -fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases alpha_eqvt ctxt = +fun raw_prove_trans ctxt alpha_result raw_dt_thms alpha_eqvt = let - val alpha_names = map (fst o dest_Const) alpha_trms + val AlphaResult {alpha_names, alpha_trms, alpha_bn_names, alpha_bn_trms, + alpha_raw_induct, ...} = alpha_result + + val alpha_trms = alpha_trms @ alpha_bn_trms + val props = map prep_trans_goal alpha_trms in - alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct - (prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_cases alpha_eqvt) ctxt + alpha_prove alpha_trms (alpha_trms ~~ props) alpha_raw_induct + (prove_trans_tac alpha_result raw_dt_thms alpha_eqvt) ctxt end @@ -601,8 +625,10 @@ @{lemma "transp R == !x y. R x y --> (!z. R y z --> R x z)" by (rule eq_reflection, auto simp add: trans_def transp_def)} -fun raw_prove_equivp alphas alpha_bns refl symm trans ctxt = +fun raw_prove_equivp ctxt alpha_result refl symm trans = let + val AlphaResult {alpha_trms, alpha_bn_trms, ...} = alpha_result + val refl' = map (fold_rule [reflp_def'] o atomize) refl val symm' = map (fold_rule [symp_def'] o atomize) symm val trans' = map (fold_rule [transp_def'] o atomize) trans @@ -610,10 +636,10 @@ fun prep_goal t = HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) in - Goal.prove_multi ctxt [] [] (map prep_goal (alphas @ alpha_bns)) + Goal.prove_multi ctxt [] [] (map prep_goal (alpha_trms @ alpha_bn_trms)) (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac @{thm equivpI} THEN' RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans'])))) - |> chop (length alphas) + |> chop (length alpha_trms) end diff -r 37c0d7953cba -r 116f9ba4f59f Nominal/nominal_dt_data.ML --- a/Nominal/nominal_dt_data.ML Wed Jun 29 19:21:26 2011 +0100 +++ b/Nominal/nominal_dt_data.ML Wed Jun 29 23:08:44 2011 +0100 @@ -16,11 +16,24 @@ val the_info: Proof.context -> string -> info val register_info: (string * info) -> Context.generic -> Context.generic val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list + + datatype alpha_result = AlphaResult of + {alpha_names : string list, + alpha_trms : term list, + alpha_tys : typ list, + alpha_bn_names : string list, + alpha_bn_trms : term list, + alpha_bn_tys : typ list, + alpha_intros : thm list, + alpha_cases : thm list, + alpha_raw_induct : thm} + end structure Nominal_Dt_Data: NOMINAL_DT_DATA = struct + (* information generated by nominal_datatype *) type info = {inject : thm list, @@ -55,5 +68,16 @@ map aux ty_names end +datatype alpha_result = AlphaResult of + {alpha_names : string list, + alpha_trms : term list, + alpha_tys : typ list, + alpha_bn_names : string list, + alpha_bn_trms : term list, + alpha_bn_tys : typ list, + alpha_intros : thm list, + alpha_cases : thm list, + alpha_raw_induct : thm} + end \ No newline at end of file