nominal2: comparison Nominal/nominal_dt

equal deleted inserted replaced

-:040519ec99e9
+:b52e8651591f
 val exi_zero = @{lemma "P (0::perm) ==> (? x. P x)" by auto}
 fun cases_tac intros ctxt =
 let
-val prod_simps = @{thms split_conv prod_alpha_def prod_rel_def}
+val prod_simps = @{thms split_conv prod_alpha_def rel_prod_def}
 val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac
 val bound_tac =
 EVERY' [ rtac exi_zero,
 let
 val prems' = map (transform_prem1 context pred_names) prems
 in
 resolve_tac prems' 1
 end) ctxt
-val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel_def alphas}
+val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def rel_prod_def alphas}
 in
 EVERY'
 [ etac exi_neg,
 resolve_tac @{thms alpha_sym_eqvt},
 asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps),
 HEADGOAL (rtac exi_inst)
 end)
 fun non_trivial_cases_tac pred_names intros alpha_eqvt ctxt =
 let
-val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel_def}
+val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def rel_prod_def}
 in
 resolve_tac intros
 THEN_ALL_NEW (asm_simp_tac (put_simpset HOL_basic_ss ctxt) THEN'
 TRY o EVERY'   (* if binders are present *)
 [ etac @{thm exE},
 atac,
 aatac pred_names ctxt,
 eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl},
 asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ])
 end
 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
 val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) fvs
 val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) (bns @ fv_bns)
 val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns
 val simpset =
-put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps}
+put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_fv.simps set_simps append.simps}
 @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left})
 in
 alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_raw_induct
 (K (asm_full_simp_tac simpset)) ctxt
 end
 (HOLogic.size_const ty $ x, HOLogic.size_const ty $ y)
 val props = (alpha_trms @ alpha_bn_trms) ~~ (map mk_prop (alpha_tys @ alpha_bn_tys))
 val simpset =
-put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_alpha_def prod_rel_def
+put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_alpha_def rel_prod_def
-permute_prod_def prod.cases prod.recs})
+permute_prod_def prod.case prod.rec})
 val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac simpset
 in
 alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct (K tac) ctxt
 end
 (* respectfulness for constructors *)
 fun raw_constr_rsp_tac ctxt alpha_intros simps =
 let
-val pre_simpset = put_simpset HOL_ss ctxt addsimps @{thms fun_rel_def}
+val pre_simpset = put_simpset HOL_ss ctxt addsimps @{thms rel_fun_def}
-val post_simpset = put_simpset HOL_ss ctxt addsimps @{thms alphas prod_alpha_def prod_rel_def
+val post_simpset = put_simpset HOL_ss ctxt addsimps @{thms alphas prod_alpha_def rel_prod_def
-prod_fv.simps fresh_star_zero permute_zero prod.cases} @ simps
+prod_fv.simps fresh_star_zero permute_zero prod.case} @ simps
 in
 asm_full_simp_tac pre_simpset
 THEN' REPEAT o (resolve_tac @{thms allI impI})
 THEN' resolve_tac alpha_intros
 THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_simpset)
 fun lookup ty =
 case AList.lookup (op=) (alpha_tys ~~ alpha_trms) ty of
 NONE => HOLogic.eq_const ty
 | SOME alpha => alpha
-fun fun_rel_app (t1, t2) =
+fun rel_fun_app (t1, t2) =
-Const (@{const_name "fun_rel"}, dummyT) $ t1 $ t2
+Const (@{const_name "rel_fun"}, dummyT) $ t1 $ t2
 fun prep_goal trm =
 trm
 |> strip_type o fastype_of
 |> (fn (tys, ty) => tys @ [ty])
 |> map lookup
-|> foldr1 fun_rel_app
+|> foldr1 rel_fun_app
 |> (fn t => t $ trm $ trm)
 |> Syntax.check_term ctxt
 |> HOLogic.mk_Trueprop
 in
 map (fn constrs =>
 (* rsp lemmas for alpha_bn relations *)
 val rsp_equivp =
 @{lemma "[|equivp Q; !!x y. R x y ==> Q x y|] ==> (R ===> R ===> op =) Q Q"
-by (simp only: fun_rel_def equivp_def, metis)}
+by (simp only: rel_fun_def equivp_def, metis)}
 (* we have to reorder the alpha_bn_imps theorems in order
 to be in order with alpha_bn_trms *)
 fun raw_alpha_bn_rsp alpha_result alpha_bn_equivp alpha_bn_imps =
 (* rsp for permute_bn functions *)
 val perm_bn_rsp = @{lemma "(!x y p. R x y --> R (f p x) (f p y)) ==> (op= ===> R ===> R) f f"
-by (simp add: fun_rel_def)}
+by (simp add: rel_fun_def)}
 fun raw_prove_perm_bn_tac alpha_result simps ctxt =
 SUBPROOF (fn {prems, context, ...} =>
 let
 val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, ...} = alpha_result
 alpha_result
 val perm_bn_ty = range_type o range_type o fastype_of
 val ty_assoc = (alpha_tys @ alpha_bn_tys) ~~ (alpha_trms @ alpha_bn_trms)
 val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
 val p = Free (p, @{typ perm})
 fun mk_prop t =
 let
 val alpha_trm = lookup ty_assoc (perm_bn_ty t)
 (* transformation of the natural rsp-lemmas into standard form *)
 val fun_rsp = @{lemma
-"(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by (simp add: fun_rel_def)}
+"(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by (simp add: rel_fun_def)}
 fun mk_funs_rsp ctxt thm =
 thm
 |> atomize ctxt
 |> single
 |> curry (op OF) fun_rsp
 val permute_rsp = @{lemma
 "(!x y p. R x y --> R (permute p x) (permute p y))
-==> ((op =) ===> R ===> R) permute permute"  by (simp add: fun_rel_def)}
+==> ((op =) ===> R ===> R) permute permute"  by (simp add: rel_fun_def)}
 fun mk_alpha_permute_rsp ctxt thm =
 thm
 |> atomize ctxt
 |> single

changeset 3229	b52e8651591f
parent 3226	780b7a2c50b6
child 3239	67370521c09c