nominal2: comparison Nominal/nominal_dt

equal deleted inserted replaced

-:116f9ba4f59f
+:c537d43c09f1
 signature NOMINAL_DT_ALPHA =
 sig
 val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term
 val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list ->
-bclause list list list -> term list -> Proof.context ->
+bclause list list list -> term list -> Proof.context -> alpha_result * 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
 val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm ->
 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_prove_bn_imp: Proof.context -> alpha_result -> thm list
-val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list ->
+val raw_fv_bn_rsp_aux: Proof.context -> alpha_result -> term list -> term list -> term list ->
-term list -> thm -> thm list -> Proof.context -> thm list
+thm list -> thm list
-val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list
+val raw_size_rsp_aux: Proof.context -> alpha_result -> thm list -> thm list
-val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list
+val raw_constrs_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list
-val raw_alpha_bn_rsp: term list -> thm list -> thm list -> thm list
+val raw_alpha_bn_rsp: alpha_result -> thm list -> thm list -> thm list
-val raw_perm_bn_rsp: term list -> term list -> thm -> thm list -> thm list ->
+val raw_perm_bn_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list
-Proof.context -> thm list
 val mk_funs_rsp: thm -> thm
 val mk_alpha_permute_rsp: thm -> thm
 end
 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
+val alpha_tys = map (domain_type o fastype_of) alpha_trms
-|> map fastype_of
+val alpha_bn_tys = map (domain_type o fastype_of) alpha_bn_trms
-|> 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
+in
-val alpha_result = AlphaResult
+(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}
+alpha_raw_induct = alpha_raw_induct}, lthy')
-in
-(alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_raw_induct, alpha_result, lthy')
 end
 (** induction proofs **)
 end
 (* proves that alpha_raw implies alpha_bn *)
-fun raw_prove_bn_imp_tac pred_names alpha_intros ctxt =
+fun raw_prove_bn_imp_tac alpha_result ctxt =
 SUBPROOF (fn {prems, context, ...} =>
 let
+val AlphaResult {alpha_names, alpha_intros, ...} = alpha_result
 val prems' = flat (map Datatype_Aux.split_conj_thm prems)
-val prems'' = map (transform_prem1 context pred_names) prems'
+val prems'' = map (transform_prem1 context alpha_names) prems'
 in
 HEADGOAL
 (REPEAT_ALL_NEW
 (FIRST' [ rtac @{thm TrueI},
 rtac @{thm conjI},
 resolve_tac prems',
 resolve_tac prems'',
 resolve_tac alpha_intros ]))
 end) ctxt
-fun raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct ctxt =
-let
+fun raw_prove_bn_imp ctxt alpha_result =
+let
+val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_raw_induct, ...} = alpha_result
 val arg_ty = domain_type o fastype_of
-val alpha_names =  map (fst o dest_Const) alpha_trms
+val ty_assoc = alpha_tys ~~ alpha_trms
-val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms
 val props = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => t $ x $ y)) alpha_bn_trms
 in
-alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_induct
+alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct
-(raw_prove_bn_imp_tac alpha_names alpha_intros) ctxt
+(raw_prove_bn_imp_tac alpha_result) ctxt
 end
 (* respectfulness for fv_raw / bn_raw *)
-fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt =
+fun raw_fv_bn_rsp_aux ctxt alpha_result fvs bns fv_bns simps =
 let
-val arg_ty = fst o dest_Type o domain_type o fastype_of
+val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_raw_induct, ...} = alpha_result
-val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms
+val arg_ty = domain_type o fastype_of
+val ty_assoc = alpha_tys ~~ alpha_trms
 fun mk_eq' t x y = HOLogic.mk_eq (t $ x, t $ y)
 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 ss = HOL_ss 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_induct
+alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_raw_induct
 (K (asm_full_simp_tac ss)) ctxt
 end
 (* respectfulness for size *)
-fun raw_size_rsp_aux all_alpha_trms alpha_induct simps ctxt =
+fun raw_size_rsp_aux ctxt alpha_result simps =
 let
-val arg_tys = map (domain_type o fastype_of) all_alpha_trms
+val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_raw_induct, ...} =
+alpha_result
 fun mk_prop ty (x, y) = HOLogic.mk_eq
 (HOLogic.size_const ty $ x, HOLogic.size_const ty $ y)
-val props = map2 (fn trm => fn ty => (trm, mk_prop ty)) all_alpha_trms arg_tys
+val props = (alpha_trms @ alpha_bn_trms) ~~ (map mk_prop (alpha_tys @ alpha_bn_tys))
 val ss = HOL_ss addsimps (simps @ @{thms alphas prod_alpha_def prod_rel_def
 permute_prod_def prod.cases prod.recs})
 val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac ss
 in
-alpha_prove all_alpha_trms props alpha_induct (K tac) ctxt
+alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct (K tac) ctxt
 end
 (* respectfulness for constructors *)
 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_ss)
 end
-fun raw_constrs_rsp constrs alpha_trms alpha_intros simps ctxt =
+fun raw_constrs_rsp ctxt alpha_result constrs simps =
 let
-val alpha_arg_tys = map (domain_type o fastype_of) alpha_trms
+val AlphaResult {alpha_trms, alpha_tys, alpha_intros, ...} = alpha_result
 fun lookup ty =
-case AList.lookup (op=) (alpha_arg_tys ~~ alpha_trms) ty of
+case AList.lookup (op=) (alpha_tys ~~ alpha_trms) ty of
 NONE => HOLogic.eq_const ty
 | SOME alpha => alpha
 fun fun_rel_app (t1, t2) =
 Const (@{const_name "fun_rel"}, dummyT) $ t1 $ t2
 by (simp only: fun_rel_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_bn_trms alpha_bn_equivp alpha_bn_imps =
+fun raw_alpha_bn_rsp alpha_result alpha_bn_equivp alpha_bn_imps =
 let
+val AlphaResult {alpha_bn_trms, ...} = alpha_result
 fun mk_map thm =
 thm |> `prop_of
 |>> List.last  o snd o strip_comb
 |>> HOLogic.dest_Trueprop
 |>> head_of
 (* 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)}
-fun raw_prove_perm_bn_tac pred_names alpha_intros simps ctxt =
+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
 val prems' = flat (map Datatype_Aux.split_conj_thm prems)
-val prems'' = map (transform_prem1 context pred_names) prems'
+val prems'' = map (transform_prem1 context (alpha_names @ alpha_bn_names)) prems'
 in
 HEADGOAL
 (simp_tac (HOL_basic_ss addsimps (simps @ prems'))
 THEN' TRY o REPEAT_ALL_NEW
 (FIRST' [ rtac @{thm TrueI},
 resolve_tac prems',
 resolve_tac prems'',
 resolve_tac alpha_intros ]))
 end) ctxt
-fun raw_perm_bn_rsp alpha_trms perm_bns alpha_induct alpha_intros simps ctxt =
+fun raw_perm_bn_rsp ctxt alpha_result perm_bns simps =
 let
-val arg_ty = domain_type o fastype_of
+val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_raw_induct, ...} =
+alpha_result
 val perm_bn_ty = range_type o range_type o fastype_of
-val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms
+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 =
 val alpha_trm = lookup ty_assoc (perm_bn_ty t)
 in
 (alpha_trm, fn (x, y) => alpha_trm $ (t $ p $ x) $ (t $ p $ y))
 end
 val goals = map mk_prop perm_bns
-val alpha_names =  map (fst o dest_Const) alpha_trms
+in
+alpha_prove (alpha_trms @ alpha_bn_trms) goals alpha_raw_induct
-in
+(raw_prove_perm_bn_tac alpha_result simps) ctxt
-alpha_prove alpha_trms goals alpha_induct
-(raw_prove_perm_bn_tac alpha_names alpha_intros simps) ctxt
 |> ProofContext.export ctxt' ctxt
 |> map atomize
 |> map single
 |> map (curry (op OF) perm_bn_rsp)
 end

changeset 2928	c537d43c09f1
parent 2927	116f9ba4f59f
child 2957	01ff621599bc