# HG changeset patch # User Christian Urban # Date 1387080880 -39600 # Node ID 780b7a2c50b653ff6507cf9d208e8149be283976 # Parent b7b80d5640bb2f5ffb2a4aea76a7a57d59d51eaf updated to changes in Isabelle diff -r b7b80d5640bb -r 780b7a2c50b6 Nominal/FROOT.ML --- a/Nominal/FROOT.ML Mon Oct 14 11:23:18 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,10 +0,0 @@ - - -no_document use_thys - ["Nominal2", - "Atoms", - "Eqvt" - ]; - - - diff -r b7b80d5640bb -r 780b7a2c50b6 Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Mon Oct 14 11:23:18 2013 +0200 +++ b/Nominal/Nominal2.thy Sun Dec 15 15:14:40 2013 +1100 @@ -271,7 +271,8 @@ in raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps) (Local_Theory.restore lthy_tmp) - |> map (rewrite_rule @{thms permute_nat_def[THEN eq_reflection]}) + |> map (rewrite_rule (Local_Theory.restore lthy_tmp) + @{thms permute_nat_def[THEN eq_reflection]}) |> map (fn thm => thm RS @{thm sym}) end @@ -302,7 +303,7 @@ val raw_funs_rsp_aux = raw_fv_bn_rsp_aux lthy5 alpha_result raw_fvs raw_bns raw_fv_bns (raw_bn_defs @ raw_fv_defs) - val raw_funs_rsp = map (Drule.eta_contraction_rule o mk_funs_rsp) raw_funs_rsp_aux + val raw_funs_rsp = map (Drule.eta_contraction_rule o mk_funs_rsp lthy5) raw_funs_rsp_aux fun match_const cnst th = (fst o dest_Const o snd o dest_comb o HOLogic.dest_Trueprop o prop_of) th = @@ -315,12 +316,12 @@ val raw_size_rsp = raw_size_rsp_aux lthy5 alpha_result (raw_size_thms @ raw_size_eqvt) - |> map mk_funs_rsp + |> map (mk_funs_rsp lthy5) val raw_constrs_rsp = raw_constrs_rsp lthy5 alpha_result raw_all_cns (alpha_bn_imp_thms @ raw_funs_rsp_aux) - val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt + val alpha_permute_rsp = map (mk_alpha_permute_rsp lthy5) alpha_eqvt val alpha_bn_rsp = raw_alpha_bn_rsp alpha_result alpha_bn_equivp_thms alpha_bn_imp_thms @@ -744,4 +745,8 @@ (main_parser >> nominal_datatype2_cmd) *} + end + + + diff -r b7b80d5640bb -r 780b7a2c50b6 Nominal/Nominal2_Base.thy --- a/Nominal/Nominal2_Base.thy Mon Oct 14 11:23:18 2013 +0200 +++ b/Nominal/Nominal2_Base.thy Sun Dec 15 15:14:40 2013 +1100 @@ -272,7 +272,7 @@ lemma permute_diff [simp]: shows "(p - q) \ x = p \ - q \ x" - unfolding diff_minus by simp + using permute_plus [of p "- q" x] by simp lemma permute_minus_cancel [simp]: shows "p \ - p \ x = x" @@ -365,7 +365,7 @@ instance apply default apply (simp add: permute_perm_def) -apply (simp add: permute_perm_def diff_minus minus_add add_assoc) +apply (simp add: permute_perm_def algebra_simps) done end @@ -373,12 +373,12 @@ lemma permute_self: shows "p \ p = p" unfolding permute_perm_def - by (simp add: diff_minus add_assoc) + by (simp add: add_assoc) lemma pemute_minus_self: shows "- p \ p = p" unfolding permute_perm_def - by (simp add: diff_minus add_assoc) + by (simp add: add_assoc) subsection {* Permutations for functions *} @@ -870,7 +870,8 @@ fixes p q::"perm" shows "p \ (- q) = - (p \ q)" unfolding permute_perm_def - by (simp add: diff_minus minus_add add_assoc) + by (simp add: diff_add_eq_diff_diff_swap) + subsubsection {* Equivariance of Logical Operators *} diff -r b7b80d5640bb -r 780b7a2c50b6 Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Mon Oct 14 11:23:18 2013 +0200 +++ b/Nominal/nominal_dt_alpha.ML Sun Dec 15 15:14:40 2013 +1100 @@ -33,8 +33,8 @@ val raw_alpha_bn_rsp: alpha_result -> thm list -> thm list -> thm list val raw_perm_bn_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list - val mk_funs_rsp: thm -> thm - val mk_alpha_permute_rsp: thm -> thm + val mk_funs_rsp: Proof.context -> thm -> thm + val mk_alpha_permute_rsp: Proof.context -> thm -> thm end structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = @@ -623,9 +623,9 @@ 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 + val refl' = map (fold_rule ctxt [reflp_def'] o atomize ctxt) refl + val symm' = map (fold_rule ctxt [symp_def'] o atomize ctxt) symm + val trans' = map (fold_rule ctxt [transp_def'] o atomize ctxt) trans fun prep_goal t = HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) @@ -834,7 +834,7 @@ alpha_prove (alpha_trms @ alpha_bn_trms) goals alpha_raw_induct (raw_prove_perm_bn_tac alpha_result simps) ctxt |> Proof_Context.export ctxt' ctxt - |> map atomize + |> map (atomize ctxt) |> map single |> map (curry (op OF) perm_bn_rsp) end @@ -846,9 +846,9 @@ val fun_rsp = @{lemma "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by (simp add: fun_rel_def)} -fun mk_funs_rsp thm = +fun mk_funs_rsp ctxt thm = thm - |> atomize + |> atomize ctxt |> single |> curry (op OF) fun_rsp @@ -857,9 +857,9 @@ "(!x y p. R x y --> R (permute p x) (permute p y)) ==> ((op =) ===> R ===> R) permute permute" by (simp add: fun_rel_def)} -fun mk_alpha_permute_rsp thm = +fun mk_alpha_permute_rsp ctxt thm = thm - |> atomize + |> atomize ctxt |> single |> curry (op OF) permute_rsp diff -r b7b80d5640bb -r 780b7a2c50b6 Nominal/nominal_dt_quot.ML --- a/Nominal/nominal_dt_quot.ML Mon Oct 14 11:23:18 2013 +0200 +++ b/Nominal/nominal_dt_quot.ML Sun Dec 15 15:14:40 2013 +1100 @@ -338,7 +338,7 @@ end) in induct_prove qtys (goals1 @ goals2) qinduct tac ctxt - |> map atomize + |> map (atomize ctxt) |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms fun_eq_iff[symmetric]})) end @@ -591,14 +591,14 @@ (* for freshness conditions *) val tac1 = SOLVED' (EVERY' [ simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps peqs), - rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}), + rewrite_goal_tac ctxt'' (@{thms fresh_star_Un[THEN eq_reflection]}), conj_tac (DETERM o resolve_tac fprops') ]) (* for equalities between constructors *) val tac2 = SOLVED' (EVERY' [ rtac (@{thm ssubst} OF prems), - rewrite_goal_tac (map safe_mk_equiv eq_iff_thms), - rewrite_goal_tac (map safe_mk_equiv abs_eqs), + rewrite_goal_tac ctxt'' (map safe_mk_equiv eq_iff_thms), + rewrite_goal_tac ctxt'' (map safe_mk_equiv abs_eqs), conj_tac (DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)) ]) (* proves goal "P" *) diff -r b7b80d5640bb -r 780b7a2c50b6 Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Mon Oct 14 11:23:18 2013 +0200 +++ b/Nominal/nominal_dt_rawfuns.ML Sun Dec 15 15:14:40 2013 +1100 @@ -467,7 +467,7 @@ fun prove_eqvt_tac insts ind_thms const_names simps ctxt = HEADGOAL - (Object_Logic.full_atomize_tac + (Object_Logic.full_atomize_tac ctxt THEN' (DETERM o (Induct_Tacs.induct_rules_tac ctxt insts ind_thms)) THEN_ALL_NEW subproof_tac const_names simps ctxt) diff -r b7b80d5640bb -r 780b7a2c50b6 Nominal/nominal_function_common.ML --- a/Nominal/nominal_function_common.ML Mon Oct 14 11:23:18 2013 +0200 +++ b/Nominal/nominal_function_common.ML Sun Dec 15 15:14:40 2013 +1100 @@ -76,8 +76,11 @@ let fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of thy t)) in - Morphism.thm_morphism f $> Morphism.term_morphism term - $> Morphism.typ_morphism (Logic.type_map term) + Morphism.morphism "lift_morphism" + {binding = [], + typ = [Logic.type_map term], + term = [term], + fact = [map f]} end fun import_function_data t ctxt = diff -r b7b80d5640bb -r 780b7a2c50b6 Nominal/nominal_induct.ML --- a/Nominal/nominal_induct.ML Mon Oct 14 11:23:18 2013 +0200 +++ b/Nominal/nominal_induct.ML Sun Dec 15 15:14:40 2013 +1100 @@ -90,7 +90,7 @@ val cert = Thm.cterm_of thy; val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list; - val atomized_defs = map (map (Conv.fconv_rule Induct.atomize_cterm)) defs; + val atomized_defs = map (map (Conv.fconv_rule (Induct.atomize_cterm defs_ctxt))) defs; val finish_rule = split_all_tuples defs_ctxt @@ -104,7 +104,7 @@ (fn i => fn st => rules |> inst_mutual_rule ctxt insts avoiding - |> Rule_Cases.consume (flat defs) facts + |> Rule_Cases.consume ctxt (flat defs) facts |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) => (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j => (CONJUNCTS (ALLGOALS @@ -122,10 +122,10 @@ else Induct.arbitrary_tac defs_ctxt k xs) end) - THEN' Induct.inner_atomize_tac) j)) - THEN' Induct.atomize_tac) i st |> Seq.maps (fn st' => + THEN' Induct.inner_atomize_tac ctxt) j)) + THEN' Induct.atomize_tac ctxt) i st |> Seq.maps (fn st' => Induct.guess_instance ctxt - (finish_rule (Induct.internalize more_consumes rule)) i st' + (finish_rule (Induct.internalize ctxt more_consumes rule)) i st' |> Seq.maps (fn rule' => CASES (rule_cases ctxt rule' cases) (Tactic.rtac (rename_params_rule false [] rule') i THEN @@ -133,7 +133,7 @@ THEN_ALL_NEW_CASES ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac) else K all_tac) - THEN_ALL_NEW Induct.rulify_tac) + THEN_ALL_NEW Induct.rulify_tac ctxt) end; diff -r b7b80d5640bb -r 780b7a2c50b6 Nominal/nominal_library.ML --- a/Nominal/nominal_library.ML Mon Oct 14 11:23:18 2013 +0200 +++ b/Nominal/nominal_library.ML Sun Dec 15 15:14:40 2013 +1100 @@ -99,9 +99,9 @@ val transform_prem2: Proof.context -> string list -> thm -> thm (* transformation into the object logic *) - val atomize: thm -> thm - val atomize_rule: int -> thm -> thm - val atomize_concl: thm -> thm + val atomize: Proof.context -> thm -> thm + val atomize_rule: Proof.context -> int -> thm -> thm + val atomize_concl: Proof.context -> thm -> thm (* applies a tactic to a formula composed of conjunctions *) val conj_tac: (int -> tactic) -> int -> tactic @@ -492,10 +492,10 @@ (* transforms a theorem into one of the object logic *) -val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars; -fun atomize_rule i thm = - Conv.fconv_rule (Conv.concl_conv i Object_Logic.atomize) thm -fun atomize_concl thm = atomize_rule (length (prems_of thm)) thm +fun atomize ctxt = Conv.fconv_rule (Object_Logic.atomize ctxt) o forall_intr_vars; +fun atomize_rule ctxt i thm = + Conv.fconv_rule (Conv.concl_conv i (Object_Logic.atomize ctxt)) thm +fun atomize_concl ctxt thm = atomize_rule ctxt (length (prems_of thm)) thm (* applies a tactic to a formula composed of conjunctions *) diff -r b7b80d5640bb -r 780b7a2c50b6 Nominal/nominal_mutual.ML --- a/Nominal/nominal_mutual.ML Mon Oct 14 11:23:18 2013 +0200 +++ b/Nominal/nominal_mutual.ML Sun Dec 15 15:14:40 2013 +1100 @@ -335,12 +335,12 @@ [thm] => thm |> Drule.gen_all |> Thm.permute_prems 0 1 - |> (fn thm => atomize_rule (length (prems_of thm) - 1) thm) + |> (fn thm => atomize_rule ctxt' (length (prems_of thm) - 1) thm) | thms => thms |> map Drule.gen_all |> map (Rule_Cases.add_consumes 1) |> snd o Rule_Cases.strict_mutual_rule ctxt' - |> atomize_concl + |> atomize_concl ctxt' fun tac thm = rtac (Drule.gen_all thm) THEN_ALL_NEW atac in