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