435 |
435 |
436 val _ = trace_msg (K "Proving equality between fv and supp...") |
436 val _ = trace_msg (K "Proving equality between fv and supp...") |
437 val qfv_supp_thms = |
437 val qfv_supp_thms = |
438 prove_fv_supp qtys (flat qtrms) qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs |
438 prove_fv_supp qtys (flat qtrms) qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs |
439 qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC |
439 qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC |
|
440 |> map Drule.eta_contraction_rule |
440 |
441 |
441 (* postprocessing of eq and fv theorems *) |
442 (* postprocessing of eq and fv theorems *) |
442 val qeq_iffs' = qeq_iffs |
443 val qeq_iffs' = qeq_iffs |
443 |> map (simplify (HOL_basic_ss addsimps qfv_supp_thms)) |
444 |> map (simplify (HOL_basic_ss addsimps qfv_supp_thms)) |
444 |> map (simplify (HOL_basic_ss addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]})) |
445 |> map (simplify (HOL_basic_ss addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]})) |
445 |
446 |
|
447 (* filters the theormes that are of the form "qfv = supp" *) |
|
448 fun is_qfv_thm (@{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ _)) = member (op=) qfvs lhs |
|
449 | is_qfv_thm _ = false |
|
450 |
446 val qsupp_constrs = qfv_defs |
451 val qsupp_constrs = qfv_defs |
447 |> map (simplify (HOL_basic_ss addsimps (take (length qfvs) qfv_supp_thms))) |
452 |> map (simplify (HOL_basic_ss addsimps (filter (is_qfv_thm o prop_of) qfv_supp_thms))) |
448 |
453 |
449 val transform_thm = @{lemma "x = y \<Longrightarrow> a \<notin> x \<longleftrightarrow> a \<notin> y" by simp} |
454 val transform_thm = @{lemma "x = y \<Longrightarrow> a \<notin> x \<longleftrightarrow> a \<notin> y" by simp} |
450 val transform_thms = |
455 val transform_thms = |
451 [ @{lemma "a \<notin> (S \<union> T) \<longleftrightarrow> a \<notin> S \<and> a \<notin> T" by simp}, |
456 [ @{lemma "a \<notin> (S \<union> T) \<longleftrightarrow> a \<notin> S \<and> a \<notin> T" by simp}, |
452 @{lemma "a \<notin> (S - T) \<longleftrightarrow> a \<notin> S \<or> a \<in> T" by simp}, |
457 @{lemma "a \<notin> (S - T) \<longleftrightarrow> a \<notin> S \<or> a \<in> T" by simp}, |